[GHC] #14554: Core Lint error mixing
#14554: Core Lint error mixing -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- While trying to deeply embed ''Singletons''-style defunctionalization symbol application using the code from [http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=comp... System FC with Explicit Kind Equality], I ran into the following `-dcore- lint` error: {{{#!hs {-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-} import Data.Kind import Data.Proxy type a ~> b = (a, b) -> Type type family (@@) (f::k ~> k') (a::k)::k' data IdSym0 :: Type ~> Type type instance IdSym0 @@ a = a data KIND = X | FNARR KIND KIND data TY :: KIND -> Type where ID :: TY (FNARR X X) FNAPP :: TY (FNARR k k') -> TY k -> TY k' data TyRep (kind::KIND) :: TY kind -> Type where TID :: TyRep (FNARR X X) ID TFnApp :: TyRep (FNARR k k') f -> TyRep k a -> TyRep k' (FNAPP f a) type family IK (kind::KIND) :: Type where IK X = Type IK (FNARR k k') = IK k ~> IK k' type family IT (ty::TY kind) :: IK kind where IT ID = IdSym0 IT (FNAPP f x) = IT f @@ IT x zero :: TyRep X a -> IT a zero = \case TFnApp TID a -> undefined }}} {{{ $ ghci -ignore-dot-ghci -dcore-lint ~/hs/123-bug.hs GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( /home/baldur/hs/123-bug.hs, interpreted ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.3.20171122 for x86_64-unknown-linux): ASSERT failed! Bad coercion hole {a2UN}: (IT (a_a1S5 |> Sym (TY (Sym co_a2UC))_N) |> D:R:IK[0]) (IT (a_a1S5 |> Sym (TY (Sym co_a2UC))_N) |> D:R:IK[0]) nominal <(IT (a_a1S5 |> Sym (TY (Sym co_a2UC))_N) |> D:R:IK[0])>_N IT (a_a1S5 |> Sym (TY (Sym co_a2UC))_N) IT (a_a1S5[ssk:3] |> Sym (TY (Sym co_a2UC))_N) nominal Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1205:22 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1203:5 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcMType.hs:305:105 in ghc:TcMType Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14554> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14554: Core Lint error mixing -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType, | PolyKinds Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14556 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * keywords: => TypeInType, PolyKinds * related: => #14556 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14554#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14554: Core Lint error mixing -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType, | PolyKinds Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14556 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): It's worth noting that what you've posted is a failed `ASSERT`, not a Core Lint error. Nevertheless, you _do_ experience a Core Lint error if you use a build that doesn't have `ASSERT`ions enabled. Here's what I get with GHC 8.2.2: {{{ [1 of 1] Compiling Main ( Bug.hs, interpreted ) *** Core Lint errors : in result of Desugar (after optimization) *** <no location info>: warning: [in body of letrec with binders $dIP_a2S7 :: HasCallStack] Bad axiom application (check_ki1 D:R:@@TYPETYPEIdSym0a[0] <IT (a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N)>_N IK 'X a_a1wo *) D:R:@@TYPETYPEIdSym0a[0] <IT (a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N)>_N <no location info>: warning: [in body of letrec with binders $dIP_a2S7 :: HasCallStack] Bad axiom application (check_ki2 D:R:@@TYPETYPEIdSym0a[0] <IT (a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N)>_N IK 'X a_a1wo *) D:R:@@TYPETYPEIdSym0a[0] <IT (a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N)>_N <no location info>: warning: [in body of letrec with binders $dIP_a2S7 :: HasCallStack] Kind application error in coercion ‘((@@) (Sym (D:R:IK[0])) (Sym (D:R:IK[0])) (Trans (Sym (Coh <IdSym0>_N (Trans (((,) (Sym (D:R:IK[0])) (Sym (D:R:IK[0])))_N ->_N <*>_N) (Sym (D:R:IK[1] <'X>_N <'X>_N))))) (Sym (Coh (D:R:IT[0]) (D:R:IK[1] <'X>_N <'X>_N)))) <IT (a |> (TY (Nth:0 cobox))_N)>_N)_R’ Function kind = forall k k'. (k ~> k') -> k -> k' Arg kinds = [(*, *), (*, *), (IdSym0, (*, *) -> *), (IT (a_a1PD |> (TY (Nth:0 cobox))_N), IK 'X)] *** Offending Program *** zero :: forall (a :: TY 'X). TyRep 'X a -> (IT a |> D:R:IK[0]) [LclIdX] zero = \ (@ (a_a1Pz :: TY 'X)) -> break<1>() \ (ds_d2U1 :: TyRep 'X a_a1Pz) -> join { fail_d2UH :: Void# -> (IT a_a1Pz |> D:R:IK[0]) [LclId[JoinId(1)]] fail_d2UH _ [Occ=Dead, OS=OneShot] = patError @ 'LiftedRep @ (IT a_a1Pz |> D:R:IK[0]) "Bug.hs:(37,8)-(38,27)|case"# } in case ds_d2U1 of { __DEFAULT -> jump fail_d2UH void#; TFnApp @ k_a1PB @ f_a1PC @ a_a1PD cobox_a1PE ds_d2UG _ [Occ=Dead] -> case ds_d2UG of { __DEFAULT -> jump fail_d2UH void#; TID cobox_a1PF cobox_a1PG -> let { $dIP_a2S7 :: HasCallStack [LclId] $dIP_a2S7 = (pushCallStack (unpackCString# "undefined"#, SrcLoc (unpackCString# "main"#) (unpackCString# "Main"#) (unpackCString# "Bug.hs"#) (I# 38#) (I# 19#) (I# 38#) (I# 28#)) ((emptyCallStack `cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N) :: (CallStack :: *) ~R# ((?callStack::CallStack) :: Constraint)) ) `cast` (N:IP[0] <"callStack">_N <CallStack>_N :: ((?callStack::CallStack) :: Constraint) ~R# (CallStack :: *))) ) `cast` (Sym (N:IP[0] <"callStack">_N <CallStack>_N) :: (CallStack :: *) ~R# ((?callStack::CallStack) :: Constraint)) } in (break<0>() undefined @ 'LiftedRep @ (IT (a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N) |> D:R:IK[0]) $dIP_a2S7) `cast` (Sym (<(IT (a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N) |> D:R:IK[0])>_R |> Sym D:R :IK[0]) ; Sub (Sym (D:R:@@TYPETYPEIdSym0a[0] <IT (a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N)>_N)) ; ((@@) (Sym (D:R:IK[0])) (Sym (D:R:IK[0])) (Trans (Sym (Coh (Sym <IdSym0>_N) (Trans (((,) (Sym (D:R:IK[0])) (Sym (D:R:IK[0])))_N ->_N <*>_N) (Sym (D:R:IK[1] <'X>_N <'X>_N))))) (Sym (Coh (D:R:IT[0]) (D:R:IK[1] <'X>_N <'X>_N)))) <IT (a |> (TY (Nth:0 cobox))_N)>_N)_R ; Sub (Sym (D:R:IT[1] <'X>_N <'X>_N <'ID>_N <(a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N)>_N)) ; (IT <'X>_N (Trans ('FNAPP <'X>_N (Nth:0 (Sym cobox)) (Trans (Sym (Coh (Sym (Coh <'ID>_N (TY ('FNARR <'X>_N (Nth:1 (Nth:0 (Sym (Kind cobox)))))_ N)_N)) (Sym (Kind cobox)))) (Coh (Sym cobox) (Sym (Kind cobox)))) (Coh <a>_N (TY (Nth:0 cobox))_N))_N (Sym cobox)))_R ; Sym (<IT a_a1Pz>_R |> D:R:IK[0]) :: ((IT (a_a1PD |> Sym (TY (Sym (Nth:0 cobox)))_N) |> D:R:IK[0]) :: *) ~R# ((IT a1_a1Pz |> D:R:IK[0]) :: *)) } } $trModule :: Module [LclIdX] $trModule = Module (TrNameS "main"#) (TrNameS "Main"#) $krep_a2TJ [InlPrag=[~]] :: KindRep [LclId] $krep_a2TJ = $WKindRepVar (I# 1#) $krep_a2TB [InlPrag=[~]] :: KindRep [LclId] $krep_a2TB = $WKindRepVar (I# 0#) $krep_a2U0 [InlPrag=[~]] :: KindRep [LclId] $krep_a2U0 = KindRepTyConApp $tc(,) (: @ KindRep krep$* (: @ KindRep krep$* ([] @ KindRep))) $krep_a2TZ [InlPrag=[~]] :: KindRep [LclId] $krep_a2TZ = KindRepFun $krep_a2U0 krep$* $krep_a2TK [InlPrag=[~]] :: KindRep [LclId] $krep_a2TK = $WKindRepVar (I# 2#) $krep_a2TN [InlPrag=[~]] :: KindRep [LclId] $krep_a2TN = $WKindRepVar (I# 3#) $tcIdSym0 :: TyCon [LclIdX] $tcIdSym0 = TyCon 1961622809926585738## 3423181666860199358## $trModule (TrNameS "IdSym0"#) 0# $krep_a2TZ $tcKIND :: TyCon [LclIdX] $tcKIND = TyCon 9515352812269918203## 11516430088381478906## $trModule (TrNameS "KIND"#) 0# krep$* $krep_a2TR [InlPrag=[~]] :: KindRep [LclId] $krep_a2TR = KindRepTyConApp $tcKIND ([] @ KindRep) $tc'X :: TyCon [LclIdX] $tc'X = TyCon 5225325308912582631## 14983302646393556978## $trModule (TrNameS "'X"#) 0# $krep_a2TR $krep_a2TE [InlPrag=[~]] :: KindRep [LclId] $krep_a2TE = KindRepTyConApp $tc'X ([] @ KindRep) $krep_a2TQ [InlPrag=[~]] :: KindRep [LclId] $krep_a2TQ = KindRepFun $krep_a2TR krep$* $krep_a2TY [InlPrag=[~]] :: KindRep [LclId] $krep_a2TY = KindRepFun $krep_a2TR $krep_a2TR $krep_a2TX [InlPrag=[~]] :: KindRep [LclId] $krep_a2TX = KindRepFun $krep_a2TR $krep_a2TY $tc'FNARR :: TyCon [LclIdX] $tc'FNARR = TyCon 840343631093516326## 18087347551297534695## $trModule (TrNameS "'FNARR"#) 0# $krep_a2TX $krep_a2TI [InlPrag=[~]] :: KindRep [LclId] $krep_a2TI = KindRepTyConApp $tc'FNARR (: @ KindRep $krep_a2TJ (: @ KindRep $krep_a2TB ([] @ KindRep))) $krep_a2TD [InlPrag=[~]] :: KindRep [LclId] $krep_a2TD = KindRepTyConApp $tc'FNARR (: @ KindRep $krep_a2TE (: @ KindRep $krep_a2TE ([] @ KindRep))) $tcTY :: TyCon [LclIdX] $tcTY = TyCon 11778282896417043628## 9463294164882319066## $trModule (TrNameS "TY"#) 0# $krep_a2TQ $krep_a2TA [InlPrag=[~]] :: KindRep [LclId] $krep_a2TA = KindRepTyConApp $tcTY (: @ KindRep $krep_a2TB ([] @ KindRep)) $krep_a2Tz [InlPrag=[~]] :: KindRep [LclId] $krep_a2Tz = KindRepFun $krep_a2TA krep$* $krep_a2TW [InlPrag=[~]] :: KindRep [LclId] $krep_a2TW = KindRepTyConApp $tcTY (: @ KindRep $krep_a2TJ ([] @ KindRep)) $krep_a2TV [InlPrag=[~]] :: KindRep [LclId] $krep_a2TV = KindRepFun $krep_a2TW $krep_a2TA $krep_a2TU [InlPrag=[~]] :: KindRep [LclId] $krep_a2TU = KindRepTyConApp $tcTY (: @ KindRep $krep_a2TI ([] @ KindRep)) $krep_a2TT [InlPrag=[~]] :: KindRep [LclId] $krep_a2TT = KindRepFun $krep_a2TU $krep_a2TV $tc'FNAPP :: TyCon [LclIdX] $tc'FNAPP = TyCon 7529990373351007495## 105093863811657267## $trModule (TrNameS "'FNAPP"#) 2# $krep_a2TT $krep_a2TP [InlPrag=[~]] :: KindRep [LclId] $krep_a2TP = KindRepTyConApp $tc'FNAPP (: @ KindRep $krep_a2TB (: @ KindRep $krep_a2TJ (: @ KindRep $krep_a2TK (: @ KindRep $krep_a2TN ([] @ KindRep))))) $krep_a2TS [InlPrag=[~]] :: KindRep [LclId] $krep_a2TS = KindRepTyConApp $tcTY (: @ KindRep $krep_a2TD ([] @ KindRep)) $tc'ID :: TyCon [LclIdX] $tc'ID = TyCon 9233083350606244650## 12129174132981040339## $trModule (TrNameS "'ID"#) 0# $krep_a2TS $krep_a2TF [InlPrag=[~]] :: KindRep [LclId] $krep_a2TF = KindRepTyConApp $tc'ID ([] @ KindRep) $tcTyRep :: TyCon [LclIdX] $tcTyRep = TyCon 5846413146588040822## 5032305887285000310## $trModule (TrNameS "TyRep"#) 1# $krep_a2Tz $krep_a2TO [InlPrag=[~]] :: KindRep [LclId] $krep_a2TO = KindRepTyConApp $tcTyRep (: @ KindRep $krep_a2TB (: @ KindRep $krep_a2TP ([] @ KindRep))) $krep_a2TM [InlPrag=[~]] :: KindRep [LclId] $krep_a2TM = KindRepTyConApp $tcTyRep (: @ KindRep $krep_a2TJ (: @ KindRep $krep_a2TN ([] @ KindRep))) $krep_a2TL [InlPrag=[~]] :: KindRep [LclId] $krep_a2TL = KindRepFun $krep_a2TM $krep_a2TO $krep_a2TH [InlPrag=[~]] :: KindRep [LclId] $krep_a2TH = KindRepTyConApp $tcTyRep (: @ KindRep $krep_a2TI (: @ KindRep $krep_a2TK ([] @ KindRep))) $krep_a2TG [InlPrag=[~]] :: KindRep [LclId] $krep_a2TG = KindRepFun $krep_a2TH $krep_a2TL $tc'TFnApp :: TyCon [LclIdX] $tc'TFnApp = TyCon 8894026854411027209## 15109781203596368126## $trModule (TrNameS "'TFnApp"#) 4# $krep_a2TG $krep_a2TC [InlPrag=[~]] :: KindRep [LclId] $krep_a2TC = KindRepTyConApp $tcTyRep (: @ KindRep $krep_a2TD (: @ KindRep $krep_a2TF ([] @ KindRep))) $tc'TID :: TyCon [LclIdX] $tc'TID = TyCon 15519646662091825967## 1580287496060878## $trModule (TrNameS "'TID"#) 0# $krep_a2TC *** End of Offense *** }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14554#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14554: Core Lint error mixing -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType, | PolyKinds Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14556 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"b1ea0475894713b9fc753bf288589e0dc3175083/ghc" b1ea047/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="b1ea0475894713b9fc753bf288589e0dc3175083" Fix an outright bug in the unflattener Trac #14554 showed up an outright bug in the unflattening code in TcFlatten. I was filling in a coercion with the wrong coercion (a Syn in the wrong place). Result: "Bad coercion hole" assertion failures, and Core Lint Errors. Easily fixed, and the code is simpler too. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14554#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14554: Core Lint error mixing -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: fixed | Keywords: TypeInType, | PolyKinds Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: indexed- | types/should_compile/T14554 Blocked By: | Blocking: Related Tickets: #14556 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * testcase: => indexed-types/should_compile/T14554 * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14554#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC