[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
#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
#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
participants (1)
-
GHC