## 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).