[GHC] #15725: Core Lint error: Trans coercion mis-match
#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 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: -------------------------------------+------------------------------------- I discovered this when debugging #15703. The following code fails to compile with `-dcore-lint`: {{{#!hs {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Bug where import Data.Functor.Identity (Identity(..)) import Data.Kind (Type) import GHC.Exts (Any) ----- -- The important bits ----- type instance Meth (x :: Identity a) = GenericMeth x instance SC Identity ------------------------------------------------------------------------------- data family Sing :: forall k. k -> Type data instance Sing :: forall a. Identity a -> Type where SIdentity :: Sing x -> Sing ('Identity x) newtype Par1 p = Par1 p data instance Sing :: forall p. Par1 p -> Type where SPar1 :: Sing x -> Sing ('Par1 x) type family Rep1 (f :: Type -> Type) :: Type -> Type class PGeneric1 (f :: Type -> Type) where type From1 (z :: f a) :: Rep1 f a type To1 (z :: Rep1 f a) :: f a class SGeneric1 (f :: Type -> Type) where sFrom1 :: forall (a :: Type) (z :: f a). Sing z -> Sing (From1 z) sTo1 :: forall (a :: Type) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a) type instance Rep1 Identity = Par1 instance PGeneric1 Identity where type From1 ('Identity x) = 'Par1 x type To1 ('Par1 x) = 'Identity x instance SGeneric1 Identity where sFrom1 (SIdentity x) = SPar1 x sTo1 (SPar1 x) = SIdentity x type family GenericMeth (x :: f a) :: f a where GenericMeth x = To1 (Meth (From1 x)) type family Meth (x :: f a) :: f a class SC f where sMeth :: forall a (x :: f a). Sing x -> Sing (Meth x) default sMeth :: forall a (x :: f a). ( SGeneric1 f, SC (Rep1 f) , Meth x ~ GenericMeth x ) => Sing x -> Sing (Meth x) sMeth sx = sTo1 (sMeth (sFrom1 sx)) dummy :: f a -> () dummy _ = () type instance Meth (x :: Par1 p) = x instance SC Par1 where sMeth x = x }}} {{{ $ /opt/ghc/8.6.1/bin/ghc -fforce-recomp Bug.hs -dcore-lint [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) *** Core Lint errors : in result of Simplifier *** <no location info>: warning: [in body of letrec with binders x_s1Nw :: Sing (From1 x_a1Jc)] Trans coercion mis-match: D:R:Rep1Identity[0] <a_a1Jb>_N ; Sym (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N) Rep1 Identity a_a1Jb Par1 a_a1Jb Rep1 Identity a_a1Jb Par1 a_a1Jb *** Offending Program *** <elided> $csMeth_a1J9 [Occ=LoopBreaker] :: forall a (x :: Identity a). Sing x -> Sing (Meth x) [LclId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 100 60}] $csMeth_a1J9 = \ (@ a_a1Jb) (@ (x_a1Jc :: Identity a_a1Jb)) -> case heq_sel @ (Identity a_a1Jb) @ (Identity a_a1Jb) @ (Meth x_a1Jc) @ (GenericMeth x_a1Jc) (($d~_s1Nz @ a_a1Jb @ x_a1Jc) `cast` (((~) <Identity a_a1Jb>_N ((To1 <Identity>_N <a_a1Jb>_N (Coh (Sym (D:R:MethTYPEPar1px[0] <a_a1Jb>_N (Coh (Sym (Coh <From1 x_a1Jc>_N (D:R:Rep1Identity[0] <a_a1Jb>_N))) (D:R:Rep1Identity[0] <a_a1Jb>_N)))) (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N) ; (Meth <*>_N (Sym (D:R:Rep1Identity[0])) <a_a1Jb>_N (Coh <From1 x_a1Jc>_N (D:R:Rep1Identity[0] <a_a1Jb>_N)))_N))_N ; (Sym (D:R:GenericMeth[0] <Identity>_N <a_a1Jb>_N <x_a1Jc>_N) ; Sym (D:R:MethTYPEIdentityax[0] <a_a1Jb>_N <x_a1Jc>_N))) ((To1 <Identity>_N <a_a1Jb>_N (Coh (Sym (Coh (Sym (Coh <From1 x_a1Jc>_N (D:R:Rep1Identity[0] <a_a1Jb>_N))) (D:R:Rep1Identity[0] <a_a1Jb>_N))) (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N) ; (Sym (D:R:MethTYPEPar1px[0] <a_a1Jb>_N (Coh (Sym (Coh <From1 x_a1Jc>_N (D:R:Rep1Identity[0] <a_a1Jb>_N))) (D:R:Rep1Identity[0] <a_a1Jb>_N))) ; (Meth <*>_N (Sym (D:R:Rep1Identity[0])) <a_a1Jb>_N (Coh <From1 x_a1Jc>_N (D:R:Rep1Identity[0] <a_a1Jb>_N)))_N)))_N ; Sym (D:R:GenericMeth[0] <Identity>_N <a_a1Jb>_N <x_a1Jc>_N)))_R ; N:~[0] <Identity a_a1Jb>_N <Meth x_a1Jc>_N <GenericMeth x_a1Jc>_N :: (To1 (From1 x_a1Jc) ~ To1 (From1 x_a1Jc)) ~R# (Meth x_a1Jc ~~ GenericMeth x_a1Jc))) of co_a1Kd { __DEFAULT -> (\ (sx_aEZ :: Sing x_a1Jc) -> let { x_s1Nw :: Sing (From1 x_a1Jc) [LclId] x_s1Nw = $csFrom1_a1Jz @ a_a1Jb @ x_a1Jc sx_aEZ } in case x_s1Nw `cast` ((Sing (D:R:Rep1Identity[0] <a_a1Jb>_N) (Coh (Sym (Coh <From1 x_a1Jc>_N (D:R:Rep1Identity[0] <a_a1Jb>_N ; Sym (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N)))) (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N)))_R ; (Nth:3 (Inst (forall (x :: Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N). (Sing (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N) (Sym (Coh <x>_N (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N))))_R ->_R (Sing (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N) (Sym (D:R:MethTYPEPar1px[0] <a_a1Jb>_N <x>_N) ; (Meth <*>_N (Sym (D:R:Rep1Identity[0])) <a_a1Jb>_N (Sym (Coh <x>_N (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N))))_N))_R) (Coh <From1 x_a1Jc>_N (Sym (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N)))) ; ((Sing (D:R:Rep1Identity[0] <a_a1Jb>_N))_R ; D:R:SingPar10[0] <a_a1Jb>_N) (Sym (Coh <Meth (From1 x_a1Jc)>_N (D:R:Rep1Identity[0] <a_a1Jb>_N)))) :: Sing (From1 x_a1Jc |> Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N) ~R# R:SingPar1 a_a1Jb (Meth (From1 x_a1Jc) |> D:R:Rep1Identity[0] <a_a1Jb>_N)) of { SPar1 @ x_a1JZ co_a1K0 x_a195 -> ($WSIdentity @ a_a1Jb @ x_a1JZ x_a195) `cast` ((Sing <Identity a_a1Jb>_N (Sym (D:R:To1IdentityaPar1[0] <a_a1Jb>_N <x_a1JZ>_N) ; (To1 <Identity>_N <a_a1Jb>_N (Sym (Coh (Sym (Coh <'Par1 x_a1JZ>_N (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N))) (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N)) ; (Coh <'Par1 x_a1JZ>_N (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N) ; (Sym co_a1K0 ; Coh <Meth (From1 x_a1Jc)>_N (D:R:Rep1Identity[0] <a_a1Jb>_N)))))_N))_R :: Sing ('Identity x_a1JZ) ~R# Sing (To1 (Meth (From1 x_a1Jc)))) }) `cast` (<Sing x_a1Jc>_R ->_R (Sing <Identity a_a1Jb>_N (Sym (D:R:GenericMeth[0] <Identity>_N <a_a1Jb>_N <x_a1Jc>_N) ; Sym co_a1Kd))_R :: (Sing x_a1Jc -> Sing (To1 (Meth (From1 x_a1Jc)))) ~R# (Sing x_a1Jc -> Sing (Meth x_a1Jc))) } end Rec } }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15725> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#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): It appears that `simplCoercion` is the thing that's producing this ill- formed coercion. Here is the input coercion: {{{ Sym (Nth:2 (Inst (forall (x1 :: Sym (Bug.D:R:Rep1Identity[0]) <a>_N). (Bug.Sing (Sym (Bug.D:R:Rep1Identity[0]) <a>_N) (GRefl nominal x1 (Sym (Bug.D:R:Rep1Identity[0]) <a>_N)))_R ->_R (Bug.Sing (Sym (Bug.D:R:Rep1Identity[0]) <a>_N) (Sym (Bug.D:R:MethTYPEPar1px[0] <a>_N <x1>_N) ; (Bug.Meth <*>_N (Sym (Bug.D:R:Rep1Identity[0])) <a>_N (GRefl nominal x1 (Sym (Bug.D:R:Rep1Identity[0]) <a>_N)))_N))_R) (Sym (GRefl nominal (Bug.From1 x) (Sym (Sym (Bug.D:R:Rep1Identity[0]) <a>_N)))))) }}} And here is the output coercion: {{{ Nth:2 ((Bug.Sing (Bug.D:R:Rep1Identity[0] <a>_N) (Sym (GRefl nominal (Bug.From1 x) ((Bug.D:R:Rep1Identity[0] <a>_N ; Sym (Sym (Bug.D:R:Rep1Identity[0]) <a>_N)) ; Sym (Bug.D:R:Rep1Identity[0]) <a>_N))))_R ->_R (Bug.Sing (Bug.D:R:Rep1Identity[0] <a>_N) ((Bug.Meth <*>_N (Bug.D:R:Rep1Identity[0]) <a>_N (Sym (GRefl nominal (Bug.From1 x) ((Bug.D:R:Rep1Identity[0] <a>_N ; Sym (Sym (Bug.D:R:Rep1Identity[0]) <a>_N)) ; Sym (Bug.D:R:Rep1Identity[0]) <a>_N))))_N ; Bug.D:R:MethTYPEPar1px[0] <a>_N (GRefl nominal (Bug.From1 x) (Bug.D:R:Rep1Identity[0] <a>_N ; Sym (Sym (Bug.D:R:Rep1Identity[0]) <a>_N)))))_R) }}} I haven't dug deeper than that. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15725#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#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): Some slightly more precise tracing reveals the following: {{{ opt_co4_wrap } Co: GRefl nominal x_X1Gk (Sym (D:R:Rep1Identity[0]) <a_a1FN>_N) coercionType(Co): (x_X1Gk :: Par1 a_a1FN) ~# ((x_X1Gk |> Sym (D:R:Rep1Identity[0]) <a_a1FN>_N) :: Rep1 Identity a_a1FN) --- Result: Sym (GRefl nominal (From1 Identity a_a1FN x_a1FO) ((D:R:Rep1Identity[0] <a_a1FN>_N ; Sym (Sym (D:R:Rep1Identity[0]) <a_a1FN>_N)) ; Sym (D:R:Rep1Identity[0]) <a_a1FN>_N)) coercionType(Result): (From1 Identity a_a1FN x_a1FO :: Rep1 Identity a_a1FN) ~# (From1 Identity a_a1FN x_a1FO :: Rep1 Identity a_a1FN) }}} Next step: figure out why `GRefl` is being optimized so crap-tacularly. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15725#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#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
#15725: Core Lint error: Trans coercion mis-match -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch 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): Phab:D5217 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D5217 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15725#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15725: Core Lint error: Trans coercion mis-match -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch 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): Phab:D5217 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Great sleuthing! Is the bug in [https://www.microsoft.com/en-us/research/publication /evidence-normalization-system-fc-2/ the paper], or just in the implementation? If the former we should fix the paper. I have not studied the details of your patch, but I'm sure Richard will. Thank you for doing this. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15725#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15725: Core Lint error: Trans coercion mis-match -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch 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): Phab:D5217 Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:5 simonpj]:
Is the bug in [https://www.microsoft.com/en-us/research/publication /evidence-normalization-system-fc-2/ the paper], or just in the implementation?
I'm not sure. Having skimmed the paper, it looks like the code I changed roughly corresponds to the RedInstTy reduction rule from Figure 7 (when you have `InstCo (ForAllCo (a:eta). gamma) phi`). But the RedInstTy rule that is shown in the paper is much simpler than the thing that's actually implemented in GHC, since the paper doesn't distinguish between the cases where `a` is a type variable or coercion variable, nor does it include any details of the "lifting context" business from //System FC with Explicit Kind Equality//. So I can't really make any kind of judgment on whether //Evidence Normalisation in System FC// is correct or not. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15725#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15725: Core Lint error: Trans coercion mis-match -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch 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): Phab:D5217 Wiki Page: | -------------------------------------+------------------------------------- Comment (by monoidal): If this helps, I reduced to {{{ #!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind (Type) newtype Identity a = Identity a newtype Par1 a = Par1 a data family Sing :: forall k. k -> Type data instance Sing :: forall k. k -> Type type family Rep1 (f :: Type -> Type) :: Type -> Type type instance Rep1 Identity = Par1 type family From1 (z :: f a) :: Rep1 f a type instance From1 ('Identity x) = 'Par1 x und :: a und = und f :: forall (a :: Type) (x :: Identity a). Sing x f = g where g :: forall (a :: Type) (f :: Type -> Type) (x :: f a). Sing x g = seq (und :: Sing (From1 x)) und }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15725#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15725: Core Lint error: Trans coercion mis-match -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch 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): Phab:D5217 Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Thanks for your tireless efforts to minimize these bugs, monoidal. They're very much appreciated. In this particular example, I think you might have minimized it too well! That's because that program trips up Core Lint even with the patch in Phab:D5217. In fact, I think this program has an entirely different bug from the one described in this ticket. Here is the Core Lint error for your program: {{{ *** Core Lint errors : in result of Simplifier *** Bug.hs:25:1: warning: [in body of lambda with binder x_a19R :: Identity a_a19Q] Kind application error in coercion ‘(Sing (D:R:Rep1Identity[0] <a_a19Q>_N) <From1 x_a19R>_N)_R’ Function kind = forall k. k -> * Arg kinds = [(Par1 a_a19Q, *), (From1 x_a19R, Rep1 Identity a_a19Q)] Fun: Par1 a_a19Q (From1 x_a19R, Rep1 Identity a_a19Q) Bug.hs:25:1: warning: [in body of lambda with binder x_a19R :: Identity a_a19Q] Kind application error in coercion ‘D:R:Singk0[0] <Par1 a_a19Q>_N <From1 x_a19R>_N’ Function kind = Par1 a_a19Q -> * Arg kinds = [(From1 x_a19R, Rep1 Identity a_a19Q)] Fun: Par1 a_a19Q (From1 x_a19R, Rep1 Identity a_a19Q) Bug.hs:25:1: warning: [in body of lambda with binder x_a19R :: Identity a_a19Q] Kind application error in coercion ‘D:R:Singk0[0] <Par1 a_a19Q>_N <From1 x_a19R>_N’ Function kind = Par1 a_a19Q -> * Arg kinds = [(From1 x_a19R, Rep1 Identity a_a19Q)] Fun: Par1 a_a19Q (From1 x_a19R, Rep1 Identity a_a19Q) <no location info>: warning: In the type ‘R:Singk (Par1 a_a19Q) (From1 x_a19R)’ Kind application error in type ‘R:Singk (Par1 a_a19Q) (From1 x_a19R)’ Function kind = forall k -> k -> * Arg kinds = [(Par1 a_a19Q, *), (From1 x_a19R, Rep1 Identity a_a19Q)] Fun: Par1 a_a19Q (From1 x_a19R, Rep1 Identity a_a19Q) <no location info>: warning: In the type ‘R:Singk (Par1 a_a19Q) (From1 x_a19R)’ Kind application error in type ‘R:Singk (Par1 a_a19Q) (From1 x_a19R)’ Function kind = forall k -> k -> * Arg kinds = [(Par1 a_a19Q, *), (From1 x_a19R, Rep1 Identity a_a19Q)] Fun: Par1 a_a19Q (From1 x_a19R, Rep1 Identity a_a19Q) }}} My suspicion is that this program suffers from the same problems that afflict the program in #15549, since (1) the errors look very similar, and (2) `seq` is being used here, and I identified the `improveSeq` function as being responsible for an incorrect optimization in #15549. I'll put this program over in that ticket as another test case. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15725#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15725: Core Lint error: Trans coercion mis-match -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch 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): Phab:D5217 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Krzysztof Gogolewski <krz.gogolewski@…>): In [changeset:"48efbc04bd45d806c52376641e1a7ed7278d1ec7/ghc" 48efbc0/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="48efbc04bd45d806c52376641e1a7ed7278d1ec7" Fix #15725 with an extra Sym Summary: We were adding a `Sym` to one argument in the `InstCo` case of `optCoercion` but not another, leading to the two arguments to misaligned when combined via `Trans`. This fixes the issue with a well targeted use of `wrapSym`. Test Plan: make test TEST=T15725 Reviewers: goldfire, ningning, bgamari Reviewed By: goldfire, ningning Subscribers: rwbarton, carter GHC Trac Issues: #15725 Differential Revision: https://phabricator.haskell.org/D5217 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15725#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15725: Core Lint error: Trans coercion mis-match -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.1 Resolution: fixed | 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): Phab:D5217 Wiki Page: | -------------------------------------+------------------------------------- Changes (by monoidal): * status: patch => closed * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15725#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC