Skip to content

Delicate solve order

Should we successfully infer a type for f:

f x = [h x, [x]]

assuming h :: forall b. F b -> b?

Assuming (x::alpha) and we instantiate h at beta, we get the constraints

 (1)  beta ~ [alpha]		from the list [h x, [x]]
 (2)  alpha ~ F beta		from the call of h

Now if we happen to unify the constraint (1) first, beta := [alpha], then we successfully infer

f :: forall a. (a ~ F [a]) => a -> [[a]]

But if we unify the constraint (2) first, alpha := F beta, we get

f :: forall b.  (b ~ [F b]) => F b -> [[F b]]

which looks ambiguous. It isn't ambiguous, in fact, but the solver has to work hard to prove it. It actually succeeds here, but in the more complicated example in indexed-types/should_compile/IndTypesPerfMerge, it didn't. There the function merge has (a slightly more complicated form of) this delicately-balanced situation.

But see Note [Orientation of equalities with fmvs] in TcFlatten for why we don't defer solving (2).

Edited by Simon Peyton Jones
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information