[GHC] #15009: Float equalities past local equalities

[GHC]

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

Comment (by simonpj):

 I think you are referring to `Note [Let-bound skolems]` in `TcSMonad`?
 Suppose we have
 {{{
 data T where
   MkT :: (a ~ Int) => a -> T
 }}}
 Here `a` is existentially bound, but it's really just a let-binding;
 we may as well have written
 {{{
 data T where
   MkT :: Int -> T
 }}}
 Now consider type inference on this, where we try `f :: alpha -> T ->
 beta`.
 {{{
 f x y = case y of MkT -> x
 }}}
 We'll get an implication constraint
 {{{
 forall[2] a. (a~Int) => alpha[1] ~ beta[1]
 }}}
 Can we float that equality out, and unify `alpha := beta`?  We say
 yes, because of `Note [Let-bound skolems]`.

 You ask whether the `a` needs to be bound at the same level
 (i.e. in the same implication) as the `(a ~ Int)`.  I think it does.
 Consider
 {{{
 data S a where
   MkS :: (a ~ Int) => S a

 g :: forall a. S a -> a -> blah
 g x y = let h = \z. ( z :: Int
                     , case x of
                          MkS -> [y,z])
         in ...
 }}}
 When doing inference on `h` we'll assign `y :: alpha[1]`, say.
 Then from the body of the lambda we'll get
 {{{
 alpha[1] ~ Int                         -- From z::Int
 forall[2]. (a ~ Int) => alpha[1] ~ a   -- From [y,z]
 }}}
 Now, suppose we decide to float `alpha ~ a` out of the implication
 and then unify `alpha := a`.  Now we are stuck!  But if treat
 `alpha ~ Int` first, and unify `alpha := Int`, all is fine.
 But we absolutely cannot float that equality or we will get stuck.

 Does that help explain? I could add this to the Note.

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