Opened 5 months ago
Last modified 3 weeks ago
#14270 new bug
GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal
Reported by: | hvr | Owned by: | bgamari |
---|---|---|---|
Priority: | high | Milestone: | 8.6.1 |
Component: | Compiler | Version: | 8.3 |
Keywords: | Typeable | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | Compile-time crash or panic | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #14236 | Differential Rev(s): | |
Wiki Page: |
Description
When doing a default build of GHC HEAD (i.e. without mk/build.mk
), GHC panics:
$ make V=0 ===--- building phase 0 make --no-print-directory -f ghc.mk phase=0 phase_0_builds make[1]: Nothing to be done for 'phase_0_builds'. ===--- building phase 1 make --no-print-directory -f ghc.mk phase=1 phase_1_builds make[1]: Nothing to be done for 'phase_1_builds'. ===--- building final phase make --no-print-directory -f ghc.mk phase=final all HC [stage 1] libraries/base/dist-install/build/Data/Typeable/Internal.o ghc-stage1: panic! (the 'impossible' happened) (GHC version 8.3.20170922 for x86_64-unknown-linux): Template variable unbound in rewrite rule Variable: cobox_a3S9 Rule "SC:mkTrApp0" Rule bndrs: [k1_X4g7, b_X4gb, k1_a3RW, a_a3RX, k1_X426, b_X42a, b_a3RY, sc_s7Yv, sc_s7Yr, sc_s7Ys, sc_s7Yt, cobox_a3S9, cobox_a3RZ, cobox_X42x, cobox_a3S8] LHS args: [TYPE: TYPE (b_a3RY |> Nth:2 (Sym cobox_a3S8)), TYPE: TYPE (b_X42a |> Nth:2 (Sym cobox_X42x)) -> *, TYPE: (->), TYPE: (b_X4gb |> Sym (cobox_a3S9 (Coh (Sym (Coh <b_a3RY>_N (Nth:2 (Sym cobox_a3S8)))) (Nth:2 (Sym cobox_a3S8)) ; Coh <b_a3RY>_N (Nth:2 (Sym cobox_a3S8))) ; Sym cobox_a3RZ)), TrTyCon @ (TYPE (b_a3RY |> Nth:2 (Sym cobox_a3S8)) -> TYPE (b_X42a |> Nth:2 (Sym cobox_X42x)) -> *) @ (->) sc_s7Yr sc_s7Ys $tc(->) sc_s7Yt, sc_s7Yv] Actual args: [TYPE: TYPE (b_a3RY |> Nth:2 (Sym cobox_a3S8)), TYPE: TYPE (b_X42a |> Nth:2 (Sym cobox_X42x)) -> *, TYPE: (->), TYPE: (b_X4gb |> Sym (cobox_a3S9 (Coh (Sym (Coh <b_a3RY>_N (Nth:2 (Sym cobox_a3S8)))) (Nth:2 (Sym cobox_a3S8)) ; Coh <b_a3RY>_N (Nth:2 (Sym cobox_a3S8))) ; Sym cobox_a3RZ)), TrTyCon @ (TYPE (b_a3RY |> Nth:2 (Sym cobox_a3S8)) -> TYPE (b_X42a |> Nth:2 (Sym cobox_X42x)) -> *) @ (->) dt_a2Vb dt_a2Vc $tc(->) kind_vars_X37r, ...
You can see a more complete error in the build log at
This panic seems to be causally connected to cc6be3a2f23c9b2e04f9f491099149e1e1d4d20b (which addressed #14236) because reverting that commit allows me to avoid the panic.
Change History (26)
comment:1 Changed 5 months ago by
Owner: | set to bgamari |
---|
comment:2 Changed 5 months ago by
The unbound binder in question is a coercion variable of type,
cobox_a3S9 :: (TYPE :: (RuntimeRep -> *)) ~# (a_a3RX :: (k1_a3RW -> *))
This feels a bit like #13410, but there the the binders were of type t~t
.
comment:3 Changed 5 months ago by
Ahh, so it seems like the coercion variables in question only occur in types. However, match_ty
doesn't contribute to the RuleSubst
's id substitution. Consequently the variables never make it into the substitution.
comment:4 Changed 5 months ago by
I tried extending the rule matching substitution with the CvSubst from the unification. Unfortunately, it seems as though the unifier returns an empty CvSubst. Perhaps this is because of the fact that the template variable appears both in the LHS of the rule and the argument being matched. Consequently the unifier may not extend its CvSubst when unifying, since doing so would mean adding a substitution cobox_a3S9 :-> cobox_a3S9
to the substitution. This would violate the invariant of matching that none of the template variables appear in the range of the resulting substitution (as described in, e.g., Note [Matching in the presence of casts]
).
Also, for future reference: The coercions in question come in to scope as the result of a pattern match on an HRefl
,
case ds_d4wx of { HRefl cobox_a3S8 cobox_a3S9 -> ...
comment:5 Changed 5 months ago by
Ahh, I see what is going on here: When Unify.unify_ty
needs to match a type CastTy ty co
with something else, it doesn't even attempt to match co
(on account of Note [Matching in the presence of casts]
). Instead, it simply matches ty
(adjusting the kind coercion accordingly). Consequently, template variables that occur only in co
will never be matched.
The solution to this is not at all obvious to me.
comment:6 Changed 5 months ago by
Unfortunately, as long as this bug persists, the nightly-ish GHC HEAD ppa packages can't be built. If the fix takes longer than a few days, can we revert cc6be3a2f23c9b2e04f9f491099149e1e1d4d20b (and reopen #14236) until there's a proper fix?
comment:7 Changed 5 months ago by
Uck. This is nasty. And I'm sure it's actually my fault, not Ben's.
I think we should revert the offending commit while sorting this out, as I'm not convinced that this will have an easy fix.
Ben, could you paste here what the offending rule is? I know that GHC already does some faffing about with rules to make sure their LHSs are convenient to match with (see, e.g., DsBinds.decomposeRuleLhs
and Desugar.unfold_coerce
); maybe we can extend that algorithm to handle this case.
The long-term solution is, I believe comment:9:ticket:14119.
comment:9 Changed 5 months ago by
The rule in question is,
RULES: "SC:mkTrApp0" forall (sc_s7Wy :: TypeRep (b_a44F |> cobox_a3RZ ; Sym cobox_a3S9 (Sym (Coh <b_a3RY>_N (Nth:2 (Sym cobox_a3S8))) ; Sym (Coh (Sym (Coh <b_a3RY>_N (Nth:2 (Sym cobox_a3S8)))) (Nth:2 (Sym cobox_a3S8)))))) (sc_s7Wv :: Word#) (sc_s7Ww :: Word#). mkTrApp_XkG @ (TYPE (b_a3RY |> Nth:2 (Sym cobox_a3S8))) @ (TYPE (b_X42a |> Nth:2 (Sym cobox_X42x)) -> *) @ (->) @ (b_a44F |> Sym (cobox_a3S9 (Coh (Sym (Coh <b_a3RY>_N (Nth:2 (Sym cobox_a3S8)))) (Nth:2 (Sym cobox_a3S8)) ; Coh <b_a3RY>_N (Nth:2 (Sym cobox_a3S8))) ; Sym cobox_a3RZ)) (Data.Typeable.Internal.TrTyCon @ (TYPE (b_a3RY |> Nth:2 (Sym cobox_a3S8)) -> TYPE (b_X42a |> Nth:2 (Sym cobox_X42x)) -> *) @ (->) sc_s7Wv sc_s7Ww GHC.Types.$tc(->) kind_vars_X37r) sc_s7Wy = $smkTrApp_s7Wz sc_s7Wy sc_s7Wv sc_s7Ww]
comment:10 Changed 5 months ago by
Wow. That looks fun to munch on later. But in the meantime, where is this RULE in the source? I sadly can't find it.
comment:11 Changed 5 months ago by
I have not reproduced this, but the RULE comes from SpecConstr
. Presumably it sees a call to
mkTrApp @(b_a3RY |> blah) ... (TrTyCon @(b_a3RY |> blah) e1 ...)
and creates a specialised copy of mkTrApp
, something like
$smkTrApp sc1 sc2 sc3 = <body of mkTrApp applied to suitable args>
along with a RULE to convert calls to mkTrApp
into calls to $smkTrApp
, something like
RULE "SC:mkTrApp0" forall sc1 sc2 sc3. mkTrApp @(b_a3RY |> blah) ... = $smkTrApp sc1 sc2 sc3
So that's how those casts end up on the LHS of a RULE.
I have not yet figured out why we put a coercion variable in the template variables.
comment:12 Changed 5 months ago by
I have not yet figured out why we put a coercion variable in the template variables.
Is "a coercion variable shall not appear as a template variable" an invariant of Rule
? This wasn't clear to me.
comment:13 Changed 5 months ago by
Is "a coercion variable shall not appear as a template variable" an invariant of Rule? This wasn't clear to me.
In effect, yes. Matching the LHS will never bind coercion variables (certainly not ones used in types), so they'd better not appear on the RHS.
Boiling out a small test case would be jolly useful.
comment:14 Changed 5 months ago by
For the record, I tried adding an assertion for the coercion variable matching invariant in Phab:D4035 but it doesn't appear to be an invariant that we respect. Perhaps we should tighten this up a bit.
comment:15 Changed 5 months ago by
I attempted to create a minimal example of this bug. This is as small as I was able to make it (~110 lines):
{-# LANGUAGE TypeInType #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE TypeApplications #-} module DataTypeableInternal (pattern App) where import Data.Kind (Type) import GHC.Fingerprint (Fingerprint, fingerprintFingerprints) import GHC.Types (RuntimeRep, TYPE, TyCon) data (a :: k1) :~~: (b :: k2) where HRefl :: a :~~: a data TypeRep (a :: k) where TrTyCon :: {-# UNPACK #-} !Fingerprint -> !TyCon -> [SomeTypeRep] -> TypeRep (a :: k) TrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1). {-# UNPACK #-} !Fingerprint -> TypeRep (a :: k1 -> k2) -> TypeRep (b :: k1) -> TypeRep (a b) TrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (a :: TYPE r1) (b :: TYPE r2). {-# UNPACK #-} !Fingerprint -> TypeRep a -> TypeRep b -> TypeRep (a -> b) data SomeTypeRep where SomeTypeRep :: forall k (a :: k). !(TypeRep a) -> SomeTypeRep typeRepFingerprint :: TypeRep a -> Fingerprint typeRepFingerprint = undefined mkTrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1). TypeRep (a :: k1 -> k2) -> TypeRep (b :: k1) -> TypeRep (a b) mkTrApp rep@(TrApp _ (TrTyCon _ con _) (x :: TypeRep x)) (y :: TypeRep y) | con == funTyCon -- cheap check first , Just (IsTYPE (rx :: TypeRep rx)) <- isTYPE (typeRepKind x) , Just (IsTYPE (ry :: TypeRep ry)) <- isTYPE (typeRepKind y) , Just HRefl <- withTypeable x $ withTypeable rx $ withTypeable ry $ typeRep @((->) x :: TYPE ry -> Type) `eqTypeRep` rep = undefined mkTrApp a b = TrApp fpr a b where fpr_a = typeRepFingerprint a fpr_b = typeRepFingerprint b fpr = fingerprintFingerprints [fpr_a, fpr_b] pattern App :: forall k2 (t :: k2). () => forall k1 (a :: k1 -> k2) (b :: k1). (t ~ a b) => TypeRep a -> TypeRep b -> TypeRep t pattern App f x <- (splitApp -> Just (IsApp f x)) where App f x = mkTrApp f x data IsApp (a :: k) where IsApp :: forall k k' (f :: k' -> k) (x :: k'). () => TypeRep f -> TypeRep x -> IsApp (f x) splitApp :: forall k (a :: k). () => TypeRep a -> Maybe (IsApp a) splitApp (TrApp _ f x) = Just (IsApp f x) splitApp rep@(TrFun _ a b) = Just (IsApp (mkTrApp arr a) b) where arr = bareArrow rep splitApp (TrTyCon{}) = Nothing withTypeable :: forall a r. TypeRep a -> (Typeable a => r) -> r withTypeable = undefined eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b) eqTypeRep = undefined typeRepKind :: TypeRep (a :: k) -> TypeRep k typeRepKind = undefined bareArrow :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (a :: TYPE r1) (b :: TYPE r2). () => TypeRep (a -> b) -> TypeRep ((->) :: TYPE r1 -> TYPE r2 -> Type) bareArrow = undefined data IsTYPE (a :: Type) where IsTYPE :: forall (r :: RuntimeRep). TypeRep r -> IsTYPE (TYPE r) isTYPE :: TypeRep (a :: Type) -> Maybe (IsTYPE a) isTYPE = undefined class Typeable (a :: k) where typeRep :: Typeable a => TypeRep a typeRep = undefined funTyCon :: TyCon funTyCon = undefined instance (Typeable f, Typeable a) => Typeable (f a) instance Typeable ((->) :: TYPE r -> TYPE s -> Type) instance Typeable TYPE
I wasn't able to reproduce the exact panic in this ticket, but if you compile with -O1
and -dcore-lint
, then you do experience a Core Lint that is very reminiscent of the panic:
$ /opt/ghc/8.2.1/bin/ghc -O1 -fforce-recomp Bug.hs -dcore-lint [1 of 1] Compiling DataTypeableInternal ( Bug.hs, Bug.o ) *** Core Lint errors : in result of Float out(FOS {Lam = Just 0, Consts = True, OverSatApps = True}) *** <no location info>: warning: In the type ‘forall (a :: TYPE r1) k1. (k1 :: *) ~# (* :: *) => TypeRep ((->) a |> <TYPE r2>_N ->_N Sym cobox)’ cobox_a2ym :: (k2_aVY :: *) ~# (* :: *) [LclId[CoVarId]] is out of scope *** Offending Program *** <elided> *** End of Offense *** <no location info>: error: Compilation had errors
cobox_a2ym
appears in $mApp
(the matcher for the App
pattern synonym).
I've reproduced this with GHC 8.0.2 and HEAD.
comment:16 Changed 5 months ago by
Crumbs. comment:15 exposes a completely new bug in float-out. I have a fix validating. The relevant Note is
{- Note [Floating and kind casts] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this case x of K (co :: * ~# k) -> let v :: Int |> co v = e in blah Then, even if we are abstracting over Ids, or if e is bottom, we can't float v outside the 'co' binding. Reason: if we did we'd get v' :: forall k. (Int ~# Age) => Int |> co and now 'co' isn't in scope in that type. The underlying reason is that 'co' is a value-level thing and we can't abstract over that in a type. So if v's /type/ mentions 'co' we can't float it out beyond the binding site of 'co'. That's why we have this as_far_as_poss stuff. Usually as_far_as_poss is just tOP_LEVEL; but occasionally a coercion variable (which is an Id) mentioned in type prevents this. Example Trac #14270 comment:15.
However this is not the original bug for this ticket.
comment:19 Changed 5 months ago by
Here is what is happening. The bug happens in SpecConstr
when compiling libraries/base/./Data/Typeable/Internal.hs
with -O2
. When I re-apply the patch "Typeable: Allow App to match arrow types" I get a Lint error as before. Here's why:
We have
mkTrApp_Xjt [Occ=LoopBreaker] :: forall k1 k2 (a :: k1 -> k2) (b :: k1). TypeRep a -> TypeRep b -> TypeRep (a b)
and an application thereof looking like
mkTrApp_Xjt @ (TYPE (b_a3TI |> Nth:2 (Sym cobox_a3TS))) @ (TYPE (b_X444 |> Nth:2 (Sym cobox_X44r)) -> *) @ (->) @ (b_X4hY |> Sym (cobox_a3TT (Coh (Sym (Coh <b_a3TI>_N (Nth:2 (Sym cobox_a3TS)))) (Nth:2 (Sym cobox_a3TS)) ; Coh <b_a3TI>_N (Nth:2 (Sym cobox_a3TS))) ; Sym cobox_a3TJ)) (Data.Typeable.Internal.TrTyCon @ (TYPE (b_a3TI |> Nth:2 (Sym cobox_a3TS)) -> TYPE (b_X444 |> Nth:2 (Sym cobox_X44r)) -> *) @ (->) dt_a2Xi dt_a2Xj GHC.Types.$tc(->) kind_vars_X3a2) (ds_X4ZX `cast` (<blah> :: (TypeRep b_X4hY :: *) ~R# (TypeRep (b_X4hY |> cobox_a3TJ ; Sym cobox_a3TT (Sym (Coh <b_a3TI>_N (Nth:2 (Sym cobox_a3TS))) ; Sym (Coh (Sym (Coh <b_a3TI>_N (Nth:2 (Sym cobox_a3TS)))) (Nth:2 (Sym cobox_a3TS))))) :: *)))
So SpecConstr
tries to specialise mkTrApp_Xjt
for this call; in particular the TrTyCon
argument. Very good.
But the rule we get is this
RULES: "SC:mkTrApp0" forall (@ k1_X4hU) (@ (b_X4hY :: k1_X4hU)) (@ k1_X440) (@ (b_X444 :: k1_X440)) (@ k1_a3TG) (@ (b_a3TI :: k1_a3TG)) (sc_s7Yv :: TypeRep (b_X4hY |> cobox_a3TJ ; Sym cobox_a3TT (Sym (Coh <b_a3TI>_N (Nth:2 (Sym cobox_a3TS))) ; Sym (Coh (Sym (Coh <b_a3TI>_N (Nth:2 (Sym cobox_a3TS)))) (Nth:2 (Sym cobox_a3TS)))))) (cobox_X44r :: (RuntimeRep -> * :: *) ~# (k1_X440 -> * :: *)) (sc_s7Yr :: Word#) (sc_s7Ys :: Word#) (sc_s7Yt :: [SomeTypeRep]) (cobox_a3TS :: (RuntimeRep -> * :: *) ~# (k1_a3TG -> * :: *)). mkTrApp_Xjt @ (TYPE (b_a3TI |> <(type pat) k1_a3TG, RuntimeRep>)) @ (TYPE (b_X444 |> <(type pat) k1_X440, RuntimeRep>) -> *) @ (->) @ (b_X4hY |> <(type pat) k1_X4hU, TYPE (b_a3TI |> Nth:2 (Sym cobox_a3TS))>) (Data.Typeable.Internal.TrTyCon @ (TYPE (b_a3TI |> Nth:2 (Sym cobox_a3TS)) -> TYPE (b_X444 |> Nth:2 (Sym cobox_X44r)) -> *) @ (->) sc_s7Yr sc_s7Ys GHC.Types.$tc(->) sc_s7Yt) sc_s7Yv = $smkTrApp_s7Ze @ k1_X4hU @ b_X4hY @ k1_X440 @ b_X444 @ k1_a3TG @ b_a3TI sc_s7Yv @~ (cobox_X44r :: (RuntimeRep -> * :: *) ~# (k1_X440 -> * :: *)) sc_s7Yr sc_s7Ys sc_s7Yt @~ (cobox_a3TS :: (RuntimeRep -> * :: *) ~# (k1_a3TG -> * :: *))]
This is no good in at least two ways
- We mention
cobox_a3TS
in the kind ofsc_s7Yv
, but don't bind it until later in the telescope. - Matching against the LHS will not bind those
cobox
variables, because the type matcher discards casts (and rightly so).
So that's the problem.
comment:22 Changed 5 months ago by
OK so we are good on this, apart from the "doesn't feel like the final word to me" part of the patch in comment:20.
I'd like Richard's thoughts.
I don't know if it's worth merging to 8.2.
comment:23 Changed 5 months ago by
I think comment:9:ticket:14119 is the answer to this problem. Let's structurally remove the possibility of matching on types with structured coercions, and then this just won't be possible.
comment:24 Changed 5 months ago by
I think comment:9:ticket:14119 is the answer to this problem.
Maybe so... but the specifics still elude me. It'd be good to actually do it!
comment:25 Changed 6 weeks ago by
Keywords: | Typeable added |
---|
Hmm, alright; I'll try to look into this seeing as I broke it.