Delicate solve order
Should we successfully infer a type for
f x = [h x, [x]]
h :: forall b. F b -> b?
(x::alpha) and we instantiate
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.
Note [Orientation of equalities with fmvs] in
TcFlatten for why we don't defer solving (2).