#15346: Core Lint error in GHC 8.6.1: From-type of Cast differs from type of
enclosed expression
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: 8.6.1
Component: Compiler (Type | Version: 8.5
checker) |
Resolution: | Keywords: TypeInType
Operating System: Unknown/Multiple | Architecture:
Type of failure: Compile-time | Unknown/Multiple
crash or panic | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by RyanGlScott):
I've had quite an adventure debugging this one. I haven't quite fixed
everything, but I have discovered one surprising fact: GHC incorrectly
implements the `S_TPush` rule from //System FC with Explicit Kind
Equality//. In particular, we have:
{{{
Γ ⊢_co γ : ∀ a: κ_1. σ_1 ~ ∀ a: κ_2. σ_2
γ' = sym (nth^1 γ)
τ' = τ ⊳ γ'
----------------------------------------- S_TPush
(ν ⊳ γ) τ --> (ν τ') ⊳ γ@(<τ> ⊳ γ')
}}}
But in `CoreOpt`, GHC implements this rule as:
{{{#!hs
pushCoTyArg :: CoercionR -> Type -> Maybe (Type, MCoercionR)
pushCoTyArg co ty
...
| isForAllTy tyL
= ASSERT2( isForAllTy tyR, ppr co $$ ppr ty )
Just (ty `mkCastTy` mkSymCo co1, MCo co2)
...
where
Pair tyL tyR = coercionKind co
-- co :: tyL ~ tyR
-- tyL = forall (a1 :: k1). ty1
-- tyR = forall (a2 :: k2). ty2
co1 = mkNthCo Nominal 0 co
-- co1 :: k1 ~N k2
co2 = mkInstCo co (mkCoherenceLeftCo (mkNomReflCo ty) co1)
-- co2 :: ty1[ (ty|>co1)/a1 ] ~ ty2[ ty/a2 ]
}}}
Here, `co2` is supposed to correspond to `γ@(<τ> ⊳ γ')`, or equivalently,
`γ@(<τ> ⊳ sym (nth^1 γ))`. But note that this definition isn't correct:
`co2` actually calculates `γ@(<τ> ⊳ nth^1 γ)`, not `γ@(<τ> ⊳ sym (nth^1
γ))`! To fix this, all one needs to do is apply this patch:
{{{#!diff
diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs
index 0353ab6..5e37fee 100644
--- a/compiler/coreSyn/CoreOpt.hs
+++ b/compiler/coreSyn/CoreOpt.hs
@@ -979,7 +979,7 @@ pushCoTyArg co ty
| isForAllTy tyL
= ASSERT2( isForAllTy tyR, ppr co $$ ppr ty )
- Just (ty `mkCastTy` mkSymCo co1, MCo co2)
+ Just (ty `mkCastTy` co1, MCo co2)
| otherwise
= Nothing
@@ -989,8 +989,8 @@ pushCoTyArg co ty
-- tyL = forall (a1 :: k1). ty1
-- tyR = forall (a2 :: k2). ty2
- co1 = mkNthCo Nominal 0 co
- -- co1 :: k1 ~N k2
+ co1 = mkSymCo (mkNthCo Nominal 0 co)
+ -- co1 :: k2 ~N k1
-- Note that NthCo can extract a Nominal equality between the
-- kinds of the types related by a coercion between forall-types.
-- See the NthCo case in CoreLint.
}}}
That fixes one of the Core Lint errors in comment:3, which is nice. But
one remains even after applying that patch:
{{{
*** Core Lint errors : in result of Simplifier ***
Bug.hs:32:1: warning:
[in body of lambda with binder a_a1qX :: ()]
Kind application error in
coercion ‘(Proxy (Sym (D:R:Rep()[0]))