## Relax local equality check

Consider the following example:

```
{-# Language RankNTypes, TypeFamilies #-}
type family F a
q :: (forall b. (F b ~ Int) => (a,b)) -> ()
q _ = ()
```

Currently GHC rejects this program as ambiguous. The reason is that during the ambiguity check, GHC needs to solve a constraint of the form:

`forall a. forall b. (F b ~ Int) => (a ~ alpha)`

where `alpha`

is a unification variable corresponding to the type parameter of `q`

when used. At present, this constraint
cannot be solved, as the local assumption `F B ~ Int`

causes `alpha`

to be untouchable. In general, this is the safe thing to do, as in the presence of local assumptions unifying `alpha`

with `a`

might not be the most general solution (and, in fact, there may be *no* most general solution).

However, in this case it seems that the current rules are bit too conservative: the local assumption cannot affect the goal in any way, so `q`

is not really ambiguous, and perhaps we can relax the current restrictions a bit. @simonpj proposed the following possible refinements [1]:

- (A) An implication is considered to “bind local equalities” iff it has at least one given equality whose free variables are not all bound by the same implication.

That loosens up `Note [Let-bound skolems]`

in `TcSMonad`

, perhaps significantly. In particular, it woudl accept the example above.

The same email [1] proposed a second possiblity, (B), but it looks dodgy. So this ticket is about implementing (A).

References:

- [1] https://mail.haskell.org/pipermail/ghc-devs/2019-May/017669.html
- [2] Note [Let-bound skolems] in
`TcSMonad`