[GHC] #14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: (none) Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: Compile-time Unknown/Multiple | crash or panic Test Case: | Blocked By: Blocking: | Related Tickets: #14236 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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 https://launchpadlibrarian.net/337888338/buildlog_ubuntu-trusty-amd64 .ghc-head_8.3.20170922+git.0.5a8b843-7~14.04_BUILDING.txt.gz This panic seems to be causally connected to cc6be3a2f23c9b2e04f9f491099149e1e1d4d20b (which addressed #14236) because reverting that commit allows me to avoid the panic. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * owner: (none) => bgamari Comment: Hmm, alright; I'll try to look into this seeing as I broke it. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): 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`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): 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`, {{{#!hs case ds_d4wx of { HRefl cobox_a3S8 cobox_a3S9 -> ... }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by hvr): 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? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Herbert Valerio Riedel <hvr@…>): In [changeset:"9c7d0657e2d6c626c6aa7aac061820e8828b857e/ghc" 9c7d065/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="9c7d0657e2d6c626c6aa7aac061820e8828b857e" Revert "Typeable: Allow App to match arrow types" This reverts commit cc6be3a2f23c9b2e04f9f491099149e1e1d4d20b. because it caused the regression #14270 which according to Richard probably doesn't have an easy fix. So this one goes back to the drawning board. This reopens #14236 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): 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] }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari):
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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:13> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari): 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:14> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I attempted to create a minimal example of this bug. This is as small as I was able to make it (~110 lines): {{{#!hs {-# 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:15> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:16> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"4bb54a4522d44a81b2c47233f48252bd73c38279/ghc" 4bb54a45/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="4bb54a4522d44a81b2c47233f48252bd73c38279" Avoid creating dependent types in FloatOut This bug was exposed by Trac #14270. The problem and its cure is described in SetLevels, Note [Floating and kind casts]. It's simple and will affect very few programs. But the very fact that it was so unexpected is discomforting. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:17> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): OK I have fixed commment:15 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:18> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): 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 of `sc_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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:19> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"3de788c4eaa0592165bf1fb9e9a6d5b8e2c27554/ghc" 3de788c/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="3de788c4eaa0592165bf1fb9e9a6d5b8e2c27554" Re-apply "Typeable: Allow App to match arrow types" This re-applies commit cc6be3a2f23c9b2e04f9f491099149e1e1d4d20b Author: Ben Gamari <bgamari.foss@gmail.com> Date: Tue Sep 19 18:57:38 2017 -0400 Typeable: Allow App to match arrow types which was reverted because of Trac #14270. Now the latter is fixed we can re-apply it. The original ticket was Trac #14236 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:21> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"fb050a330ad202c1eb43038dc18cca2a5be26f4a/ghc" fb050a3/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="fb050a330ad202c1eb43038dc18cca2a5be26f4a" Do not bind coercion variables in SpecConstr rules Trac #14270 showed that SpecConstr could cause nasty Lint failures if it generates a RULE that binds coercion varables. See * Note [SpecConstr and casts], and * the test simplCore/should_compile/T14270. This doesn't feel like the final word to me, because somehow the specialisation "ought" to work. So I left in a debug WARN to yell if the new check acutally fires. Meanwhile, it stops the erroneous specialisation. binding coercion }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:20> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:22> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): 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. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:23> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
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! -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:24> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.4.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => Typeable -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:25> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.6.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.4.1 => 8.6.1 Comment: We should try to address this for 8.6. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:26> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14270: GHC HEAD's ghc-stage1 panics on Data.Typeable.Internal -------------------------------------+------------------------------------- Reporter: hvr | Owner: bgamari Type: bug | Status: new Priority: high | Milestone: 8.8.1 Component: Compiler | Version: 8.3 Resolution: | Keywords: Typeable Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple crash or panic | Test Case: Blocked By: 14119 | Blocking: Related Tickets: #14236 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * blockedby: => 14119 * milestone: 8.6.1 => 8.8.1 Comment: Given that there's no sign of motion on #14119, I think it's unlikely that this will happen for 8.8. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14270#comment:27> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC