#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