How does Idris know where to insert Force and Delay?
IIRC it's simply based on the unification of the provided type and the expected type. (&&) has type Bool -> Lazy Bool -> Bool. Unifying the second argument with y: Bool converts it to (delay y) value. On the other hand, if you'd pass x : Lazy Bool as the first argument, it converts to (force x). And this will be done with any values/function with Lazy a types.