Float equalities past local equalities
Consider the two datatypes
data T1 a where
MkT1 :: a ~ b => b > T1 a
data T2 a where
MkT2 :: a > T2 a
To me, these look like two ways of writing the same thing. Yet they participate quite differently in type inference. If I say
f (MkT1 a) = not a
g (MkT2 a) = not a
then g
is accepted (with type T2 Bool > Bool
) while f
is rejected as GHC mutters about untouchable type variables.
Of course, GHC's notion of untouchable type variables is a Good Thing, with arguments I won't rehearse here. It all boils down to this rule:
(*) Information that arises in the context of an equality constraint cannot force unification of a unification variable born outside that context.
I think this rule is a bit too strict, though. I propose a new rule:
(%) Information that arises in the context of a nonpurelylocal equality constraint cannot force unification of a unification variable born outside that context.
where
Definition: An equality constraint is purely local if every type variable free in the constraint has the same scope as the constraint itself.
That is, if an equality constraint mentions only variables freshly brought into scope  and no others  then we can still unify outer unification variables.
Happy consequences of this choice:

f
above could be accepted, as the equality inMkT1
is purely local.  Rule (%) allows users to effectively letbind type variables, like this:
f :: forall a. (a ~ SOME REALLY LONG TYPE) => Maybe a > Maybe a > Either a a
Currently, this kind of definition (if it's, say, within a
where
clause) triggers rule (*) in the body of the function, and thus causes type inference to produce a different result than just inliningSOME REALLY LONG TYPE
.
 We could theoretically simplify our treatment of GADTs. Right now, if you say
data G a b c where
MkG :: MkG d Int [e]
GHC has to cleverly figure out that
d
is a universal variable and thate
is an existential, producing the following Core:
data G a b c where
MkG :: forall d b c. forall e. (b ~ Int, c ~ [e]) => MkG d b c
If we use rule (%), then I believe the following Core would behave identically:
data G a b c where
MkG :: forall a b c. forall d e. (a ~ d, b ~ Int, c ~ [e]). MkG a b c
This treatment is more uniform and easier to implement. (Note that the equality constraints themselves are unboxed, so there's no change in runtime performance.)
What are the downsides of (%)? I don't think there are any, save an easy extra line or two in GHC to check for locality. Rule (*) exists because, without it, GHC can infer nonprincipal types. However, I conjecture that Rule (%) also serves to require inference of only principal types, while being more permissive than Rule (*).
I'm curious for your thoughts on this proposal. (I am making it here, as this is really an implementation concern, with no discernible effect on, say, the user manual, although it would allow GHC to accept more programs.)
Trac metadata
Trac field  Value 

Version  8.2.2 
Type  FeatureRequest 
TypeOfFailure  OtherFailure 
Priority  normal 
Resolution  Unresolved 
Component  Compiler 
Test case  
Differential revisions  
BlockedBy  
Related  
Blocking  
CC  
Operating system  
Architecture 