#15725: Core Lint error: Trans coercion mis-match -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #15703 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): After much digging this morning, I've finally found my way out of this rabbit hole. It turns out that the culprit is the [http://git.haskell.org/ghc.git/blob/d728c3c578cc9e9205def2c1e96934487b364b7b... InstCo] case of `opt_co4`: {{{#!hs -- See Note [Optimising InstCo] opt_co4 env sym rep r (InstCo co1 arg) -- forall over type... | Just (tv, kind_co, co_body) <- splitForAllCo_ty_maybe co1 = opt_co4_wrap (extendLiftingContext env tv (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) arg')) -- kind_co :: k1 ~ k2 -- arg' :: (t1 :: k1) ~ (t2 :: k2) -- tv |-> (t1 :: k1) ~ (((t2 :: k2) |> (sym kind_co)) :: k1) sym rep r co_body }}} In particular, the bug lies within an optimization where `co1` is of the form `forall (tv :: kind_co). co_body`, as explained in `Note [Optimising InstCo]`. As explained in the comment, we need to extend the `LiftingContext` such that `tv` maps to `(t1 :: k1) ~ (((t2 :: k2) |> (sym kind_co)) :: k1)`, which we accomplish by way of `mkCoherenceRightCo`. The [http://git.haskell.org/ghc.git/blob/4eeeb51d5f51083d0ae393009a7fd246223e9791... Haddocks] state that given `mkCoherenceRightCo r ty co co2`, the following invariants must hold: {{{ ty :: k1 co :: k1 ~ k2 co2 :: ty' ~ ty }}} That is, it must be the case that `typeKind ty ~ fst (coercionKind co)` and `ty ~ snd (coercionKind co2)`. Through some `pprTrace` sleuthing, I discovered that these were the things being used to instantiate `ty`, `co`, and `co2`, respectively: {{{ ty = t2 = (From1 Identity a x |> D:R:Rep1Identity[0] <a>_N) :: Par1 a co = mkSymCo kind_co = Sym (Sym (D:R:Rep1Identity[0]) <a>_N) :: Rep1 Identity a ~ Par1 a co2 = arg' = GRefl nominal (From1 Identity a x) (D:R:Rep1Identity[0] <a>_N) :: From1 Identity a x ~ (From1 Identity a x |> D:R:Rep1Identity[0] <a>_N) }}} This does uphold the invariant that `ty ~ snd (coercionKind co2)`, but it does //not// uphold the invariant that `typeKind ty ~ fst (coercionKind co)`, since: * `typeKind ty ~ Par1 a` * `fst (coercionKind co) ~ Rep1 Identity a` My best guess as to why this happens is that `arg'` is computed [http://git.haskell.org/ghc.git/blob/d728c3c578cc9e9205def2c1e96934487b364b7b... like so]: {{{#!hs arg' = opt_co4_wrap env sym False Nominal arg }}} In particular, we pass `opt_co4_wrap` the `sym` flag which, in the program above, happens to be `True`, so an outer `Sym` is applied to the result of the whole optimized coercion. `mkSymCo kind_co`, on the other hand, was not the result of calling `opt_co4_wrap env sym` (since it comes from `co1`, not `co1'`), which means that it does //not// have the same outer `Sym` that `arg'` has. This causes a "polarity mismatch" between the two, leading to disaster. Here is one way to fix this issue: {{{#!diff diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs index 8a44b86..c52e11e 100644 --- a/compiler/types/OptCoercion.hs +++ b/compiler/types/OptCoercion.hs @@ -377,7 +377,7 @@ opt_co4 env sym rep r (InstCo co1 arg) -- forall over type... | Just (tv, kind_co, co_body) <- splitForAllCo_ty_maybe co1 = opt_co4_wrap (extendLiftingContext env tv - (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) arg')) + (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) sym_arg')) -- kind_co :: k1 ~ k2 -- arg' :: (t1 :: k1) ~ (t2 :: k2) -- tv |-> (t1 :: k1) ~ (((t2 :: k2) |> (sym kind_co)) :: k1) @@ -396,14 +396,14 @@ opt_co4 env sym rep r (InstCo co1 arg) -- forall over type... | Just (tv', kind_co', co_body') <- splitForAllCo_ty_maybe co1' = opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv' - (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co') arg')) + (mkCoherenceRightCo Nominal t2' (mkSymCo kind_co') arg')) False False r' co_body' -- forall over coercion... | Just (cv', kind_co', co_body') <- splitForAllCo_co_maybe co1' - , CoercionTy h1 <- t1 - , CoercionTy h2 <- t2 - = let new_co = mk_new_co cv' kind_co' h1 h2 + , CoercionTy h1' <- t1' + , CoercionTy h2' <- t2' + = let new_co = mk_new_co cv' kind_co' h1' h2' in opt_co4_wrap (extendLiftingContext (zapLiftingContext env) cv' new_co) False False r' co_body' @@ -412,7 +412,9 @@ opt_co4 env sym rep r (InstCo co1 arg) co1' = opt_co4_wrap env sym rep r co1 r' = chooseRole rep r arg' = opt_co4_wrap env sym False Nominal arg - Pair t1 t2 = coercionKind arg' + sym_arg' = wrapSym sym arg' + Pair t1 t2 = coercionKind sym_arg' + Pair t1' t2' = coercionKind arg' mk_new_co cv kind_co h1 h2 = let -- h1 :: (t1 ~ t2) }}} Essentially, we wrap `arg'` with another `Sym` to cancel out an extra `Sym` that `opt_co4_wrap env sym` might provide. Of course, this should only apply to the two cases where we inspect `co1` (which did not come from `opt_co4_wrap`); for the two cases where we instead inspect `co1'`, we continue to use plain old `arg'`. Patch incoming. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15725#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler