Opened 7 months ago
Last modified 4 months ago
#13910 new bug
Inlining a definition causes GHC to panic (repSplitTyConApp_maybe)
Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 8.2.1-rc2 |
Keywords: | TypeInType | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | Compile-time crash or panic | Test Case: | |
Blocked By: | #14119 | Blocking: | |
Related Tickets: | #13877, #14038, #14175 | Differential Rev(s): | |
Wiki Page: |
Description
Here is a program which I believe should typecheck:
{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind import Data.Type.Equality data family Sing (a :: k) class SingKind k where type Demote k = (r :: *) | r -> k fromSing :: Sing (a :: k) -> Demote k toSing :: Demote k -> SomeSing k data SomeSing k where SomeSing :: Sing (a :: k) -> SomeSing k withSomeSing :: forall k r . SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r withSomeSing x f = case toSing x of SomeSing x' -> f x' data TyFun :: * -> * -> * type a ~> b = TyFun a b -> * infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 type a @@ b = Apply a b infixl 9 @@ data FunArrow = (:->) | (:~>) class FunType (arr :: FunArrow) where type Fun (k1 :: Type) arr (k2 :: Type) :: Type class FunType arr => AppType (arr :: FunArrow) where type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2 type FunApp arr = (FunType arr, AppType arr) instance FunType (:->) where type Fun k1 (:->) k2 = k1 -> k2 $(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter instance AppType (:->) where type App k1 (:->) k2 (f :: k1 -> k2) x = f x instance FunType (:~>) where type Fun k1 (:~>) k2 = k1 ~> k2 $(return []) instance AppType (:~>) where type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x infixr 0 -?> type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2 data instance Sing (z :: a :~: b) where SRefl :: Sing Refl instance SingKind (a :~: b) where type Demote (a :~: b) = a :~: b fromSing SRefl = Refl toSing Refl = SomeSing SRefl (~>:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y ~> Type). Sing r -> p @@ Refl -> p @@ r (~>:~:) SRefl pRefl = pRefl type WhyReplacePoly (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr) (y :: t) (e :: from :~: y) = App t arr Type p y data WhyReplacePolySym (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr) :: forall (y :: t). from :~: y ~> Type type instance Apply (WhyReplacePolySym arr from p :: from :~: y ~> Type) x = WhyReplacePoly arr from p y x replace :: forall (t :: Type) (from :: t) (to :: t) (p :: t -> Type). p from -> from :~: to -> p to replace = replacePoly @(:->) replaceTyFun :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type). p @@ from -> from :~: to -> p @@ to replaceTyFun = replacePoly @(:~>) @_ @_ @_ @p replacePoly :: forall (arr :: FunArrow) (t :: Type) (from :: t) (to :: t) (p :: (t -?> Type) arr). FunApp arr => App t arr Type p from -> from :~: to -> App t arr Type p to replacePoly from eq = withSomeSing eq $ \(singEq :: Sing r) -> (~>:~:) @t @from @to @r @(WhyReplacePolySym arr from p) singEq from type WhyLeibnizPoly (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t) (z :: t) = App t arr Type f a -> App t arr Type f z data WhyLeibnizPolySym (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t) :: t ~> Type type instance Apply (WhyLeibnizPolySym arr f a) z = WhyLeibnizPoly arr f a z leibnizPoly :: forall (arr :: FunArrow) (t :: Type) (f :: (t -?> Type) arr) (a :: t) (b :: t). FunApp arr => a :~: b -> App t arr Type f a -> App t arr Type f b leibnizPoly = replaceTyFun @t @a @b @(WhyLeibnizPolySym arr f a) id leibniz :: forall (t :: Type) (f :: t -> Type) (a :: t) (b :: t). a :~: b -> f a -> f b leibniz = replaceTyFun @t @a @b @(WhyLeibnizPolySym (:->) f a) id -- The line above is what you get if you inline the definition of leibnizPoly. -- It causes a panic, however. -- -- An equivalent implementation is commented out below, which does *not* -- cause GHC to panic. -- -- leibniz = leibnizPoly @(:->) leibnizTyFun :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t). a :~: b -> f @@ a -> f @@ b leibnizTyFun = leibnizPoly @(:~>) @_ @f
GHC 8.2.1 and HEAD panic on the definition of leibniz
, however:
$ /opt/ghc/8.2.1/bin/ghci Bug.hs GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) ghc: panic! (the 'impossible' happened) (GHC version 8.2.0.20170623 for x86_64-unknown-linux): repSplitTyConApp_maybe (f_a5vT[sk:2] |> Sym (Trans (Sym (D:R:Funk1:->k2[0] <k1>_N <k2>_N)) (D:R:Funk1:->k2[0] <t>_N <*>_N))) a_a5vU[sk:2] (f_a5vT[sk:2] |> Sym (Trans (Sym (D:R:Funk1:->k2[0] <k1>_N <k2>_N)) (D:R:Funk1:->k2[0] <t>_N <*>_N))) a_a5vU[sk:2] k2_a5l0 Call stack: CallStack (from HasCallStack): prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable pprPanic, called at compiler/types/Type.hs:1122:5 in ghc:Type Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
Interestingly, GHC 8.0.1 and 8.0.2 do not give the same panic—they give the panic from #13877:
$ /opt/ghc/8.0.2/bin/ghci Bug.hs GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:134:64: error:ghc: panic! (the 'impossible' happened) (GHC version 8.0.2 for x86_64-unknown-linux): No skolem info: k2_a4KV Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
Change History (8)
comment:1 Changed 7 months ago by
Keywords: | TypeInType added |
---|
comment:2 Changed 5 months ago by
Blocked By: | 14119 added |
---|---|
Related Tickets: | #13877 → #13877, #14038 |
comment:3 Changed 5 months ago by
Humorously enough, the panic is now different on GHC HEAD (likely due to commit a6c448b403dbe8720178ca82100f34baedb1f47e, Small refactor of getRuntimeRep
):
$ ghc4/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.3.20170828: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.3.20170828 for x86_64-unknown-linux): getRuntimeRep (f_a5yC[sk:2] |> Sym (Sym (D:R:Funk1:->k2[0] <k1_a5n2>_N <k2_a5n3>_N) ; D:R:Funk1:->k2[0] <t1_a5yB[sk:2]>_N <*>_N)) a_a5yD[sk:2] :: k2_a5n3 Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable pprPanic, called at compiler/types/Type.hs:1982:18 in ghc:Type
comment:4 Changed 5 months ago by
Related Tickets: | #13877, #14038 → #13877, #14038, #14175 |
---|
See #14175 for a much simpler program that gives the same two panics on GHC 8.2.1/HEAD.
comment:5 Changed 5 months ago by
Richard, I need your help on this.
I don't know whtether this problem is ultimately the source of the crash, but with my stage-1 compiler I get a earlier ASSERT failure, and some investigation shows that a type-family reduction is leading to an entirely bogus result. It's like this. We have an axiom
forall (k1 :: Type) (k2 :: Type) (f :: k1 ~> k2) (x :: k1). App k1 (':~>) k2 (f |> Sym (D:R:Funk1:~>k2{tc r14K}[0] <k1>_N <k2>_N)) x = @@ k1 k2 f x
But then we come across a call which we give to reduceTyFamApp_maybe
:
App w_a2c6 (':~>) Type ((p :: t ~> Type) |> HoleCo {a2cb}) w_a2c6
This is alraedy odd. I expected the arguments to be zonked before this attempt to do type-family reduction, but they aren't. In this case w_a2c6
is already unified with p
.
But it gets worse. When we reduce the application, we get a result looking like
@@ w_a2c6 Type (p |> Sym (Sym (D:R:Funk1:~>k2 <k1>_N <k2>_N) ; Sym (HoleCo {a2cb}))) w_a2ca
Yes, you saw it right. The k1
and k2
from the LHS of the axiom have shown up in the result!!!
Turns out that this is because of the treatment of casts in matching. In Unify.hs
we see
unify_ty env ty1 ty2 kco -- TODO: More commentary needed here | CastTy ty1' co <- ty1 = unify_ty env ty1' ty2 (co `mkTransCo` kco) | CastTy ty2' co <- ty2 = unify_ty env ty1 ty2' (kco `mkTransCo` mkSymCo co)
So coercions from the LHS and RHS both end up mixed together in that kco
; and it ultimately shows up in the result subsitution.
I'm not sure what the fix is. Maybe we can just apply the ambient substition to the co
; but what if template variables it mentions have not yet been bound yet? Or maybe we need to take the fixpoint of the returned substitution; we do this for unification, maybe we need it for matching too?
comment:6 Changed 5 months ago by
Simon and I met over lunch at ICFP on this one, and I think he solved the immediate problem here... but then ran into another gorilla behind this one. I wait with bated breath to see what shape that gorilla has!
After some analysis, I'm pretty sure this is #14038 again. Or, at least, that bug is preventing me from seeing this one clearly. Because #14038 is blocked by #14119, so is this one.