[GHC] #15009: Float equalities past local equalities

[GHC]

#15009: Float equalities past local equalities
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:  (none)
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:  8.4.3
          Component:  Compiler       |           Version:  8.2.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Consider the two datatypes

 {{{#!hs
 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

 {{{#!hs
 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:

 {{{#!hs
 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

 {{{#!hs
 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:

 {{{#!hs
 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:

 {{{#!hs
 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.)

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15009>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler