#15009: Float equalities past local equalities -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.4.3 Component: Compiler | Version: 8.2.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by 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 }}} After expanding superclases etc, that Given `b_a2dp ~ a_a2do` turns into {{{ [G] (a_a2do[tau:2] :: *) GHC.Prim.~# (b_a2dp[ssk:3] :: *) }}} with the unification variable carefully placed on the left (see `TcUnify.swapOverTyVars`. But alas `TcSMonad.getNoGivenEqs` only looks on the left in the test `skolem_bound_here`. So it conservatively says "this implication may bind non-local equalities" and we lose. I see two ways to fix this 1. Make `getNoGivenEqs` look on the right as well as the left. That, a Given `CTyEqCan` equality `b ~# a` would not count as a "given equality" if `a` is a skolem bound by this implication. 2. Change `swapOverTyVars` so that puts the skolem (not the meta-tyvar) on the left for Givens. (No change for Wanteds.) I think (2) is better. I think (1) won't help at all. Consider doing type inference for `f`: {{{ data T1 a where MkT1 :: a ~ b => b -> T1 a f (MkT1 a) = not a }}} We decide (roughly) that `f :: T alpha[1] -> beta[1]`, and then simplify this implication {{{ forall[2] b. (alpha[1] ~# b) => alpha[1] ~# Bool, beta[1] ~# Bool }}} (The `[1]` and `[2]` are the level numbers; `alpha[1]` is untouchable inside the `[2]` implication.) If we orient the Given as shown, with `alpha[1]` on the left, we'll rewrite the Wanteds thus: {{{ forall[2] b. (alpha[1] ~# b) => b ~# Bool, beta[1] ~# Bool }}} And now, ''even if we say that the Given doesn't count as a "given equality"'', we still can't solve that `b ~# Bool`. (We could float and solve `beta[1] ~# Bool`, but that's only half the problem.) What we want is to orient the Given the other way round `b ~# alpha[1]`. Then we could float out ''both'' Wanteds. Another way to think about putting `b` on the left is that it helps to eliminate occurrences of skolems, which might prevent floating. Richard, any thoughts? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15009#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler