#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 nfrisby): Replying to [comment:5 simonpj]:
I took a look. Turns out that it is what I guessed:
I don't say that it's perfectly implemented (eg I'm a bit worried about whether it's sensitive to whether the constraint looks like a ~ b or b ~ a)
We end up with {{{ Implic { TcLevel = 2 Skolems = a_a2do[sk:2] p_a2dt[sk:2] No-eqs = True Status = Unsolved Given = Wanted = WC {wc_impl = Implic { TcLevel = 3 Skolems = b_a2dp[ssk:3] No-eqs = True Status = Unsolved Given = $d~_a2dq :: (b_a2dp[ssk:3] :: *) ~ (a_a2do[tau:2] :: *) Wanted = WC {wc_simple = [WD] hole{co_a2dE} {1}:: (p_a2dt[sk:2] :: *) GHC.Prim.~# (Bool :: *) (CNonCanonical) [WD] hole{co_a2dR} {1}:: (a_a2do[sk:2] :: *) GHC.Prim.~# (Bool :: *) (CNonCanonical)} a pattern with constructor: MkT1 :: forall b a. ((b :: *) ~ (a :: *)) => b -> T1 a }}}
How is it that {{{a_a2do}}} occurs both as {{{a_a2do[sk:2]}}} and also as {{{a_a2do[tau:2]}}} in this implication tree? I'm still working on a response to your suggested edit of the Note, but while I was rereading your comments I noticed the above. I'm surprised to see the same type variable (by unique at least) occurring with two different forms of `Details`. Seems like I'm missing some relevant concept. The Notes in TcType didn't seem relevant or didn't discuss it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15009#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler