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
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.
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:
fabove could be accepted, as the equality in
MkT1is 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
whereclause) 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
dis a universal variable and that
eis 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.)