How does Idris know where to insert Force and Delay?

Question

According to the Idris crash course:

The Idris type checker knows about the Lazy type, and inserts conversions where necessary between Lazy a and a, and vice versa.

For example, b1 && b2 is converted into b1 && Delay b2. What are the specific rules that Idris uses when deciding where to place these implicit conversions?

Answer 1

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.