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 non-purely-local 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 in MkT1 is purely local.
• Rule (%) allows users to effectively let-bind 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 inlining SOME 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 that e 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 non-principal 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