[GHC] #15346: Core Lint error in GHC 8.6.1: From-type of Cast differs from type of enclosed expression
#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 | Version: 8.5 (Type checker) | 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: -------------------------------------+------------------------------------- The following program typechecks on GHC 8.6.1-alpha1: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module SGenerics where import Data.Kind import Data.Type.Equality import Data.Void ----- -- singletons machinery ----- data family Sing :: forall k. k -> Type data instance Sing :: () -> Type where STuple0 :: Sing '() type Refuted a = a -> Void data Decision a = Proved a | Disproved (Refuted a) ----- -- A stripped down version of GHC.Generics ----- data U1 = MkU1 data instance Sing (z :: U1) where SMkU1 :: Sing MkU1 ----- class Generic (a :: Type) where type Rep a :: Type from :: a -> Rep a to :: Rep a -> a class PGeneric (a :: Type) where type PFrom (x :: a) :: Rep a type PTo (x :: Rep a) :: a class SGeneric k where sFrom :: forall (a :: k). Sing a -> Sing (PFrom a) sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k) sTof :: forall (a :: k). Sing a -> PTo (PFrom a) :~: a sFot :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a ----- instance Generic () where type Rep () = U1 from () = MkU1 to MkU1 = () instance PGeneric () where type PFrom '() = MkU1 type PTo 'MkU1 = '() instance SGeneric () where sFrom STuple0 = SMkU1 sTo SMkU1 = STuple0 sTof STuple0 = Refl sFot SMkU1 = Refl ----- class SDecide k where -- | Compute a proof or disproof of equality, given two singletons. (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b) default (%~) :: forall (a :: k) (b :: k). (SGeneric k, SDecide (Rep k)) => Sing a -> Sing b -> Decision (a :~: b) s1 %~ s2 = case sFrom s1 %~ sFrom s2 of Proved (Refl :: PFrom a :~: PFrom b) -> let r :: PTo (PFrom a) :~: PTo (PFrom b) r = Refl sTof1 :: PTo (PFrom a) :~: a sTof1 = sTof s1 sTof2 :: PTo (PFrom b) :~: b sTof2 = sTof s2 in Proved (sym sTof1 `trans` r `trans` sTof2) Disproved contra -> Disproved (\Refl -> contra Refl) instance SDecide U1 where SMkU1 %~ SMkU1 = Proved Refl instance SDecide () }}} However, it throws a Core Lint error with `-dcore-lint`. The full error is absolutely massive, so I'll attach it separately. Here is the top-level bit: {{{ *** Core Lint errors : in result of Simplifier *** <no location info>: warning: In the expression: <elided> From-type of Cast differs from type of enclosed expression From-type: U1 Type of enclosed expr: Rep () Actual enclosed expr: PFrom a_a1Fm Coercion used in cast: Sym (D:R:Rep()[0]) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15346 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * Attachment "core-lint-error.txt" added. -dcore-lint error output -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15346 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): That being said, `Rep ()` should be equivalent to `U1`, so I don't understand why the Core Lint error happens in the first place. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15346#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 monoidal): Here's a smaller version: {{{ #!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeApplications #-} module SGenerics where import Data.Kind import Data.Proxy ----- type family Rep (a :: Type) :: Type type instance Rep () = () type family PFrom (x :: a) :: Rep a ----- class SDecide k where test :: forall (a :: k). Proxy a instance SDecide () where test = undefined test1 :: forall (a :: k). SDecide (Rep k) => Proxy a test1 = seq (test @_ @(PFrom a)) Proxy test2 :: forall (a :: ()). Proxy a test2 = test1 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15346#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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):
Thanks, monoidal. Your program also exhibits the same Core Lint error in
GHC 8.4, unlike the original program.
I think it's actually easier to see what goes wrong if you add a second
method to `SDecide` so that there's not as many coercions cluttering up
the `-dcore-lint` output:
{{{#!hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeApplications #-}
module SGenerics where
import Data.Kind
import Data.Proxy
-----
type family Rep (a :: Type) :: Type
type instance Rep () = ()
type family PFrom (x :: a) :: Rep a
-----
class SDecide k where
test :: forall (a :: k). Proxy a
dummy :: k
instance SDecide () where
test = undefined
dummy = undefined
test1 :: forall (a :: k). SDecide (Rep k) => Proxy a
test1 = seq (test @_ @(PFrom a)) Proxy
test2 :: forall (a :: ()). Proxy a
test2 = test1
}}}
{{{
$ /opt/ghc/8.6.1/bin/ghci Bug.hs -dcore-lint -ddump-tc
<elided>
[1 of 1] Compiling SGenerics ( Bug.hs, interpreted )
TYPE SIGNATURES
dummy :: forall k. SDecide k => k
test :: forall k (a :: k). SDecide k => Proxy a
test1 :: forall k (a :: k). SDecide (Rep k) => Proxy a
test2 :: forall (a :: ()). Proxy a
TYPE CONSTRUCTORS
type family PFrom (x :: a) :: Rep a open
type family Rep a :: * open
class SDecide k where
test :: forall (a :: k). Proxy a
dummy :: k
{-# MINIMAL test, dummy #-}
COERCION AXIOMS
axiom SGenerics.D:R:Rep() :: Rep () = () -- Defined at Bug.hs:15:15
INSTANCES
instance SDecide () -- Defined at Bug.hs:25:10
FAMILY INSTANCES
type instance Rep ()
Dependent modules: []
Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
integer-gmp-1.0.2.0]
==================== Typechecker ====================
<elided>
*** Core Lint errors : in result of Simplifier ***
Bug.hs:32:1: warning:
[in body of lambda with binder a_a1UE :: ()]
Kind application error in
coercion ‘(Proxy (Sym (D:R:Rep()[0]))
#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): Phab:D4940 changes the Core Lint error for kind coercions, as suggested in the bottom of comment:3. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15346#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 Ryan Scott
#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]))
#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 goldfire): Wow. Good sleuthing. Yes, you're right about TPush. I'm boggled that we've gotten this far with that mistake in there. I may have time tomorrow to continue. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15346#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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):
As far as the other Core Lint error goes, I think I've narrowed it down to
[http://git.haskell.org/ghc.git/blob/671537364ae09dc65d4bb1c646aa80e9c8f808df...
pushCoDataCon] (which implements the `S_KPush` rule from //System FC with
Explicit Kind Equality//), as that's the function that annotates `$ctest`
with the coercion `forall (a :: Sym (D:R:Rep()[0])). (Proxy (Sym
(D:R:Rep()[0])) <a>_P)_R`.
I tried tracing through the steps of `S_KPush` to see if this coercion is
what should have been produced, but I'm uncertain in my results simply
because the way that GHC represents type abstraction congruence coercions
is slightly different than the way they're represented in the paper.
In the paper, a type abstraction congruence coercion is of the form:
{{{
∀_η (a_1, a_2, c). γ
}}}
Where `η` is a kind coercion, `a_1` and `a_2` are two fresh type variables
inhabiting the from- and to-kinds of `η`, respectively, and `c` is a fresh
coercion variable witnessing `a_1 ~ a_2`. See the `CT_AllT` rule in Figure
4 for a complete presentation of how it's typed.
Since the type of `$ctest` is `∀(a : k). Proxy k a`, applying `Ψ` to this
type (where `Ψ` is defined in Section 5 of the paper) should produce:
{{{
∀_(Sym (D:R:Rep()[0])) (a_1, a_2, c). <Proxy> (Sym (D:R:Rep()[0])) c
}}}
This does look a bit different than the coercion that GHC is actually
producing, since the last argument to `<Proxy>` is `c` instead of `<a>`.
However, it's quite hard for me to determine if this difference is
intentional, especially after reading GHC's
[http://git.haskell.org/ghc.git/blob/671537364ae09dc65d4bb1c646aa80e9c8f808df:/compiler/types/TyCoRep.hs#l1038
Note [Forall coercions]], which presents the typing rule as:
{{{
kind_co : k1 ~ k2
tv1:k1 |- co : t1 ~ t2
-------------------------------------------------------------------
ForAllCo tv1 kind_co co : all tv1:k1. t1 ~
all tv1:k2. (t2[tv1 |-> tv1 |> sym kind_co])
}}}
This presentation is quite different from the `CT_AllT` typing rule in the
paper, as it does not introduce two fresh type variables of different
kinds equated by a coercion variable. Instead, it uses the same type
variable in both sides of the `ForAllCo`, and tries to fix up the kind of
the type variable in the to-type with this strange `tv1 |> sym kind_co`
coercion.
GHC's unusual treatment of this typing rule at least explains why the kind
of the coercion we see in this program is `(forall (a :: ()). Proxy () a)
~R# (forall (a :: Rep ()). Proxy (Rep ()) (a |> D:R:Rep()[0]))`. Still, I
find it difficult to convince myself that this alternate treatment is
correct. After all, the type `forall (a :: Rep ()). Proxy (Rep ()) (a |>
D:R:Rep()[0])` looks blatantly ill kinded to me, since `(a |>
D:R:Rep()[0])` is of kind `()`, not `Rep ()` as it claims.
Richard, do you have any insights here?
--
Ticket URL:
#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 Ryan Scott
#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: #15419 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #15419 Comment: I believe #15419 is a symptom of this bug. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15346#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: #15419 | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Richard Eisenberg
#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: merge Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | dependent/should_compile/T15346 Blocked By: | Blocking: Related Tickets: #15419 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => merge * testcase: => dependent/should_compile/T15346 Comment: This should be merged -- it's a downright bug with a tiny patch. Thanks. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15346#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: merge Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | dependent/should_compile/T15346 Blocked By: | Blocking: Related Tickets: #15419 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Note to Ben: the commit in comment:11 depends on commit 55a3f8552c9dc9b84e204ec6623c698912795347 (`Refactor coercion rule`), which is not present in the GHC 8.6 branch. Moreover, it's a fairly hefty commit, so I'm not sure we'd want to backport it, either. If you don't want to backport that commit, the following patch should also work, without needing `GRefl`. (I've left out the test cases here for the sake of brevity.) {{{#!diff diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs index 8684c84..11cbd1e 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. diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs index 2ca5151..1557ce0 100644 --- a/compiler/types/Coercion.hs +++ b/compiler/types/Coercion.hs @@ -1812,7 +1812,7 @@ liftCoSubstVarBndrUsing fun lc@(LC subst cenv) old_var Pair k1 _ = coercionKind eta new_var = uniqAway (getTCvInScope subst) (setVarType old_var k1) - lifted = Refl (TyVarTy new_var) + lifted = mkNomReflCo (TyVarTy new_var) `mkCoherenceRightCo` eta new_cenv = extendVarEnv cenv old_var lifted -- | Is a var in the domain of a lifting context? }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15346#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: closed Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Compile-time | Test Case: crash or panic | dependent/should_compile/T15346 Blocked By: | Blocking: Related Tickets: #15419 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: comment:13 merged in 06c29ddc113e5225ebc0aa37a81d9d1cf0b7f15a, testcase in f579162afbacc21a264d0fe7a117bc9c241220bb. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15346#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC