[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])) <a_a1Dx>_P)_R’ Function kind = forall k. k -> * Arg kinds = [(Rep (), *), (a_a1Dx, ())] Fun: Rep () (a_a1Dx, ()) Bug.hs:32:1: warning: [in body of lambda with binder a_a1UE :: ()] From-type of Cast differs from type of enclosed expression From-type: () Type of enclosed expr: Rep () Actual enclosed expr: PFrom a_a1UE Coercion used in cast: Sym (D:R:Rep()[0]) *** Offending Program *** <elided> test2 :: forall (a :: ()). Proxy a [LclIdX, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 10 10}] test2 = \ (@ (a_a1UE :: ())) -> break<1>() break<0>() case ($ctest_a1UM @ (PFrom a_a1UE |> D:R:Rep()[0])) `cast` (Inst (forall (a :: Sym (D:R:Rep()[0])). (Proxy (Sym (D:R:Rep()[0])) <a>_P)_R) (Coh <PFrom a_a1UE>_N (Sym (D:R:Rep()[0]))) :: Proxy (PFrom a_a1UE |> Sym (D:R:Rep()[0])) ~R# Proxy (PFrom a_a1UE |> D:R:Rep()[0])) of { Proxy -> Proxy @ () @ a_a1UE } }}} Here, we can see exactly what goes wrong: * In the definition of `test2, we have the casted type `Proxy (PFrom a_a1UE |> Sym (D:R:Rep()[0]))`, where `a_a1UE :: ()`. * As can be seen in the `-ddump-tc` output, `D:R:Rep()[0] :: Rep () ~# ()`. Therefore, `Sym (D:R:Rep()[0]) :: () ~# Rep ()`. * However, `PFrom a_a1UE :: Rep ()`, so the coercion `Sym (D:R:Rep()[0])` is oriented the wrong way! ----- There's another tiny buglet here in that Core Lint is calling `PFrom a_a1UE` an exclosed "expression", but it's actually a type. This is probably worth fixing separately. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15346#comment:3> 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): 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 <ryan.gl.scott@…>): In [changeset:"18cedbb55c7a0bdbfade4d28d3bb8927277df8d8/ghc" 18cedbb5/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="18cedbb55c7a0bdbfade4d28d3bb8927277df8d8" Make a variant of mkCastErr for kind coercions Summary: I discovered when debugging #15346 that the Core Lint error message for ill typed casts always mentions types of enclosed //expressions//, even if the thing being casted is actually a type. This generalizes `mkCastErr` a bit to allow it to give the proper labelling for kind coercions. Test Plan: Run on failing program in #15346, read the Core Lint error Reviewers: goldfire, bgamari, simonpj Reviewed By: simonpj Subscribers: simonpj, rwbarton, thomie, carter Differential Revision: https://phabricator.haskell.org/D4940 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15346#comment:5> 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): 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])) <a_avO>_P)_R’ Function kind = forall k. k -> Type Arg kinds = [(Rep (), Type), (a_avO, ())] Fun: Rep () (a_avO, ()) }}} It appears that we shouldn't be constructed the coercion `(Proxy (Sym (D:R:Rep()[0])) <a_avO>_P)_R`, as it's ill kinded. Using `-ddump-rule- rewrites`, we can see that this coercion is generated here: {{{ Rule fired Rule: Class op test Module: (BUILTIN) Before: SGenerics.test TyArg SGenerics.Rep () ValArg SGenerics.$fSDecide() `cast` ((SGenerics.SDecide (Sym (SGenerics.D:R:Rep()[0])))_R :: SGenerics.SDecide () ~R# SGenerics.SDecide (SGenerics.Rep ())) After: $ctest_a1r5 `cast` (forall (a :: Sym (SGenerics.D:R:Rep()[0])). (Data.Proxy.Proxy (Sym (SGenerics.D:R:Rep()[0])) <a>_P)_R :: (forall (a :: ()). Data.Proxy.Proxy a) ~R# (forall (a :: SGenerics.Rep ()). Data.Proxy.Proxy (a |> SGenerics.D:R:Rep()[0]))) Cont: ApplyToTy (SGenerics.PFrom a_a1qX) Select nodup wild_Xj Stop[RhsCtxt] Data.Proxy.Proxy a_a1qX }}} That's as far as I've come debugging thus far. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15346#comment:6> 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 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... 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: <http://ghc.haskell.org/trac/ghc/ticket/15346#comment:8> 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 <ryan.gl.scott@…>): In [changeset:"6595bee749ddb49d9058ed47ab7c1b6e7558ae17/ghc" 6595bee/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="6595bee749ddb49d9058ed47ab7c1b6e7558ae17" Define an Outputable MCoercion instance Summary: I needed this when debugging #15346. Test Plan: Does it compile? It does? Cool. Reviewers: bgamari, mpickering Reviewed By: mpickering Subscribers: rwbarton, thomie, carter GHC Trac Issues: #15311 Differential Revision: https://phabricator.haskell.org/D4944 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15346#comment:9> 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: | -------------------------------------+------------------------------------- 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 <rae@…>): In [changeset:"af624071fa063158d6e963e171280676f9c0a0b0/ghc" af624071/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="af624071fa063158d6e963e171280676f9c0a0b0" Fix some casts. This fixes #15346, and is a team effort between Ryan Scott and myself (mostly Ryan). We discovered two errors related to FC's "push" rules, one in the TPush rule (as implemented in pushCoTyArg) and one in KPush rule (it shows up in liftCoSubstVarBndr). The solution: do what the paper says, instead of whatever random thoughts popped into my head as I was actually implementing. Also fixes #15419, which is actually the same underlying problem. Test case: dependent/should_compile/T{15346,15419}. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15346#comment:11> 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: | -------------------------------------+------------------------------------- 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