Skip to content

GitLab

Open
Opened by Iavor S. Diatchki@yavDeveloper

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:

Edited by Simon Peyton Jones