[GHC] #14552: GHC panic on pattern synonym
#14552: GHC panic on pattern synonym -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Keywords: | Operating System: Unknown/Multiple PatternSynonyms, TypeInType, | ViewPatterns | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs {-# Language RankNTypes, ViewPatterns, PatternSynonyms, TypeOperators, KindSignatures, PolyKinds, DataKinds, TypeFamilies, TypeInType, GADTs #-} import Data.Kind data family Sing a type a --> b = (a, b) -> Type type family (@@) (f::a --> b) (x::a) :: b data Proxy a = Proxy newtype Limit' :: (k --> Type) -> Type where Limit' :: (forall xx. Proxy xx -> f@@xx) -> Limit' f data Exp :: [Type] -> Type -> Type where TLam' :: Proxy f -> (forall aa. Proxy aa -> Exp xs (f @@ aa)) -> Exp xs (Limit' f) pattern FOO f <- TLam' Proxy (($ Proxy) -> f) }}} ---> {{{ $ ghci -ignore-dot-ghci 119-bug.hs GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( 119-bug.hs, interpreted ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.3.20171122 for x86_64-unknown-linux): ASSERT failed! in_scope InScope {a_a1Mh b_a1Mi rep_a1MB r_a1MC} tenv [a1MC :-> r_a1MC] cenv [] tys [k_a1Mj[ssk:3]] cos [] needInScope [a1Mj :-> k_a1Mj[ssk:3]] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1205:22 in ghc:Outputable assertPprPanic, called at compiler/types/TyCoRep.hs:2136:51 in ghc:TyCoRep checkValidSubst, called at compiler/types/TyCoRep.hs:2159:29 in ghc:TyCoRep substTy, called at compiler/types/TyCoRep.hs:2364:41 in ghc:TyCoRep substTyVarBndr, called at compiler/coreSyn/CoreSubst.hs:571:10 in ghc:CoreSubst 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/types/TyCoRep.hs:2136:51 in ghc:TyCoRep checkValidSubst, called at compiler/types/TyCoRep.hs:2159:29 in ghc:TyCoRep substTy, called at compiler/types/TyCoRep.hs:2364:41 in ghc:TyCoRep substTyVarBndr, called at compiler/coreSyn/CoreSubst.hs:571:10 in ghc:CoreSubst Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
}}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14552> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14552: GHC panic on pattern synonym -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | PatternSynonyms, TypeInType, | ViewPatterns Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): If you don't have a build with `ASSERT`ions enabled, then you can also trigger a Core Lint with this program as well: {{{ $ /opt/ghc/8.2.2/bin/ghci Bug.hs -dcore-lint GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) *** Core Lint errors : in result of Desugar (after optimization) *** <no location info>: warning: In the type ‘forall (r :: TYPE rep) (a :: [*]) b (aa :: k). Exp a b -> (forall k1 (f :: k1 --> *). (b :: *) ~# (Limit' f :: *) => Exp a (f @@ aa) -> r) -> (Void# -> r) -> r’ @ k_a1K2[ssk:3] is out of scope *** Offending Program *** $mFOO :: forall (r :: TYPE rep) (a :: [*]) b (aa :: k). Exp a b -> (forall k1 (f :: k1 --> *). (b :: *) ~# (Limit' f :: *) => Exp a (f @@ aa) -> r) -> (Void# -> r) -> r [LclIdX] $mFOO = \ (@ (rep_a1Kn :: RuntimeRep)) (@ (r_a1Ko :: TYPE rep_a1Kn)) (@ (a_a1K0 :: [*])) (@ b_a1K1) (@ (aa_a1Kc :: k_a1K2[ssk:3])) (scrut_a1Kq :: Exp a_a1K0 b_a1K1) (cont_a1Kr :: forall k1 (f :: k1 --> *). (b_a1K1 :: *) ~# (Limit' f :: *) => Exp a_a1K0 (f @@ aa_a1Kc) -> r_a1Ko) _ [Occ=Dead] -> break<0>(scrut_a1Kq,cont_a1Kr) case scrut_a1Kq of { TLam' @ k_a1K2 @ f_a1K3 cobox_a1K4 ds_d1Lm ds_d1Ln -> case ds_d1Lm of { Proxy -> cont_a1Kr @ k_a1K2 @ f_a1K3 @~ (cobox_a1K4 :: (b_a1K1 :: *) ~# (Limit' f_a1K3 :: *)) ((\ (ds_d1Lp [OS=OneShot] :: Proxy aa_a1Kc -> Exp a_a1K0 (f_a1K3 @@ aa_a1Kc)) -> $ @ 'LiftedRep @ (Proxy aa_a1Kc) @ (Exp a_a1K0 (f_a1K3 @@ aa_a1Kc)) ds_d1Lp (Proxy @ k_a1K2 @ aa_a1Kc)) (ds_d1Ln @ aa_a1Kc)) } } $trModule :: Module [LclIdX] $trModule = Module (TrNameS "main"#) (TrNameS "Main"#) $krep_a1Lc [InlPrag=[~]] :: KindRep [LclId] $krep_a1Lc = KindRepTyConApp $tc[] (: @ KindRep krep$* ([] @ KindRep)) $krep_a1Lb [InlPrag=[~]] :: KindRep [LclId] $krep_a1Lb = KindRepFun $krep_a1Lc krep$*Arr* $krep_a1Lg [InlPrag=[~]] :: KindRep [LclId] $krep_a1Lg = $WKindRepVar (I# 0#) $krep_a1Lh [InlPrag=[~]] :: KindRep [LclId] $krep_a1Lh = KindRepFun $krep_a1Lg krep$* $krep_a1Lf [InlPrag=[~]] :: KindRep [LclId] $krep_a1Lf = KindRepTyConApp $tc(,) (: @ KindRep $krep_a1Lg (: @ KindRep krep$* ([] @ KindRep))) $krep_a1Le [InlPrag=[~]] :: KindRep [LclId] $krep_a1Le = KindRepFun $krep_a1Lf krep$* $krep_a1Ld [InlPrag=[~]] :: KindRep [LclId] $krep_a1Ld = KindRepFun $krep_a1Le krep$* $krep_a1Lj [InlPrag=[~]] :: KindRep [LclId] $krep_a1Lj = $WKindRepVar (I# 1#) $tcSing :: TyCon [LclIdX] $tcSing = TyCon 18130532723012807500## 591365583239837277## $trModule (TrNameS "Sing"#) 0# krep$*Arr* $tcProxy :: TyCon [LclIdX] $tcProxy = TyCon 637564349063008466## 16772998216715059205## $trModule (TrNameS "Proxy"#) 1# $krep_a1Lh $krep_a1Li [InlPrag=[~]] :: KindRep [LclId] $krep_a1Li = KindRepTyConApp $tcProxy (: @ KindRep $krep_a1Lg (: @ KindRep $krep_a1Lj ([] @ KindRep))) $tc'Proxy :: TyCon [LclIdX] $tc'Proxy = TyCon 10313009608267148799## 11340514327723585599## $trModule (TrNameS "'Proxy"#) 2# $krep_a1Li $tcLimit' :: TyCon [LclIdX] $tcLimit' = TyCon 15980210257158400910## 15895439795101193324## $trModule (TrNameS "Limit'"#) 1# $krep_a1Ld $tcExp :: TyCon [LclIdX] $tcExp = TyCon 14856342479466933336## 11891426334869696372## $trModule (TrNameS "Exp"#) 0# $krep_a1Lb *** End of Offense *** }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14552#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14552: GHC panic on pattern synonym -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | PatternSynonyms, TypeInType, | ViewPatterns Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Simon asked me to take a look at this pattern synonym, as there are deeper issues here. Here is a much simpler scenario with similar issues: {{{#!hs data T where T :: (forall a. Int -> a -> a) -> T pattern PT x <- T (($ 3) -> x) }}} What type should `PT` have? Here are two possibilities: (renaming for clarity, but both have the same definition) {{{#!hs pattern PT1 :: forall a. (a -> a) -> T pattern PT2 :: (forall a. a -> a) -> T }}} These synonyms correspond to the following two matchers: {{{#!hs matcher1 :: forall r a. T -> ((a -> a) -> r) -> r matcher1 (T f) k = k (f 3) matcher2 :: forall r. T -> ((forall a. a -> a) -> r) -> r matcher2 (T f) k = k (f 3) }}} Both type-check. The second is more general than the first, even though the first is what GHC infers for the definition if given the chance. So, which matcher should we generate for `PT`? However, I've just played a trick on you. Notice that I inlined the use of `($)` in my matchers. Interestingly, `matcher2` does not type check without this inlining: {{{#!hs matcher2 (T (($ 3) -> x)) k = k x -- does not type-check }}} This fails because it contains an unsaturated use of `($)`, and unsaturated uses of `($)` do not get the pseudo-impredicative magic that saturated uses of `($)` get. So, really, `matcher1` is the only possibility. (Indeed, GHC infers a pattern type of `forall a. (a -> a) -> T` for `PT`.) In the original program, the question above (where to generalize) isn't properly formed. That's because the equivalent of the `a` here (called `aa` in the example) has an existentially-bound kind, so it can't possibly scope over the whole matcher type. (In other words, it can't be like `matcher1`.) As I've already argued, it also can't be like `matcher2` (because `($)` isn't impredicative in this scenario). So, it must be like `matcher3`: {{{#!hs matcher3 :: forall r. T -> ((Any -> Any) -> r) -> r matcher3 (T (($ 3) -> x)) k = k x }}} This is a bit silly, but it's the best we can do if we can't generalize over `a`. In the original program, this is really {{{#!hs matcher :: Exp xs t -> (forall k (f :: k --> Type). Exp xs (f @@ Any) -> r) -> r matcher (TLam (Proxy :: Proxy this_f) (($ (Proxy @Any)) -> z)) k = k @_ @this_f z }}} Probably not what the user wanted, but I don't see how we can do better without an impredicative unsaturated `($)`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14552#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14552: GHC panic on pattern synonym -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | PatternSynonyms, TypeInType, | ViewPatterns Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): This is crazy. Does it make a difference if `($ 3)` got expanded `(\f -> f 3)`? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14552#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14552: GHC panic on pattern synonym -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | PatternSynonyms, TypeInType, | ViewPatterns Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Let's make it even simpler. Use Richard's data type `T`, and consider {{{ {-# LANGUAGE ViewPatterns, RankNTypes, GADTs #-} module Foo where data T where T :: (forall a. Int -> a -> a) -> T g1 (T f) = (f 3 'c', f 3 True) g2 (T f) = let h = f 3 in (h 'c', h True) g3 (T (id -> f)) = (f 3 'c', f 3 True) g4 (T ((\f -> f 3) -> h)) = (h 'c', h True) }}} Here we get * `g1` typechecks because `f` is bound to a polymorphic function. * `g2` does not typecheck, because the binding of `h` is not generalised (we have `MonoLocalBinds` when `GADTs` is on). So `h` is monomorphic. * `g3` does not typecheck for the same reason. It's akin to `g2` with `h = id f`; it desugars to something like {{{ g3 (T ff) = let f = id ff in (f 3 'c', f 3 True) }}} * `g4` does not typecheck for the same reason. It desugars to something like {{{ g4 (T ff) = let h = (\f -> f 3) ff in (h 'c', h True) }}} So I don't think this has anything to do with the impredicativity magic for `($)`. It's just that binding a polymorphic variable in a pattern is a very delicate business. One could imagine generalising those extra let-bindings in the desugarings of `g3` and `g4`, but would be hard to do reliably -- that is why we have `MonoLocalBinds`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14552#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14552: GHC panic on pattern synonym -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | PatternSynonyms, TypeInType, | ViewPatterns Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): PS
Interestingly, matcher2 does not type check without this inlining:
It does for me! {{{ matcher3 (T (($ 3) -> x)) k = k x }}} typechecks just fine with inferred type {{{ matcher3 :: forall a t. T -> ((a -> a) -> t) -> t }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14552#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14552: GHC panic on pattern synonym -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | PatternSynonyms, TypeInType, | ViewPatterns Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"e2998d720c6b6bf72c86201d816f256a8ba704e6/ghc" e2998d72/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="e2998d720c6b6bf72c86201d816f256a8ba704e6" Stop double-stacktrace in ASSERT failures We were getting the stack trace printed twice in assertion failures (e.g. see the Description of Trac #14552). This fixes it, by deleting code. (c.f. Trac #14635 which reports the same bug in documentation). }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14552#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14552: GHC panic on pattern synonym -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | PatternSynonyms, TypeInType, | ViewPatterns Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones <simonpj@…>): In [changeset:"307d1dfe1d705379eafad6dba65e651ae3465cda/ghc" 307d1df/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="307d1dfe1d705379eafad6dba65e651ae3465cda" Fix deep, dark corner of pattern synonyms Trac #14552 showed a very obscure case where we can't infer a good pattern-synonym type. The error message is horrible, but at least we no longer crash and burn. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14552#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14552: GHC panic on pattern synonym -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | PatternSynonyms, TypeInType, | ViewPatterns Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | testsuite/tests/patsyn/should_fail/T14552 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => testsuite/tests/patsyn/should_fail/T14552 Comment: OK the main fix here is comment:7. I'm not terribly happy with the error message, but it's better than a crash. Iceland Jack: ok? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14552#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14552: GHC panic on pattern synonym -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: infoneeded Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | PatternSynonyms, TypeInType, | ViewPatterns Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | testsuite/tests/patsyn/should_fail/T14552 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => infoneeded -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14552#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14552: GHC panic on pattern synonym -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: infoneeded Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: | Keywords: | PatternSynonyms, TypeInType, | ViewPatterns Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | testsuite/tests/patsyn/should_fail/T14552 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Yeah this is OK -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14552#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14552: GHC panic on pattern synonym -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: fixed | Keywords: | PatternSynonyms, TypeInType, | ViewPatterns Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | testsuite/tests/patsyn/should_fail/T14552 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: infoneeded => closed * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14552#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#14552: GHC panic on pattern synonym -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.3 Resolution: fixed | Keywords: | PatternSynonyms, TypeInType, | ViewPatterns Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | testsuite/tests/patsyn/should_fail/T14552 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg <rae@…>): In [changeset:"5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3/ghc" 5e45ad10/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3" Finish fix for #14880. The real change that fixes the ticket is described in Note [Naughty quantification candidates] in TcMType. Fixing this required reworking candidateQTyVarsOfType, the function that extracts free variables as candidates for quantification. One consequence is that we now must be more careful when quantifying: any skolems around must be quantified manually, and quantifyTyVars will now only quantify over metavariables. This makes good sense, as skolems are generally user-written and are listed in the AST. As a bonus, we now have more control over the ordering of such skolems. Along the way, this commit fixes #15711 and refines the fix to #14552 (by accepted a program that was previously rejected, as we can now accept that program by zapping variables to Any). This commit also does a fair amount of rejiggering kind inference of datatypes. Notably, we now can skip the generalization step in kcTyClGroup for types with CUSKs, because we get the kind right the first time. This commit also thus fixes #15743 and #15592, which both concern datatype kind generalisation. (#15591 is also very relevant.) For this aspect of the commit, see Note [Required, Specified, and Inferred in types] in TcTyClsDecls. Test cases: dependent/should_fail/T14880{,-2}, dependent/should_fail/T15743[cd] dependent/should_compile/T15743{,e} ghci/scripts/T15743b polykinds/T15592 dependent/should_fail/T15591[bc] ghci/scripts/T15591 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14552#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC