#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:/compiler/types/OptCoercion.hs#l414
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: