[GHC] #15693: Abstracting out pattern into a pattern synonym fails with scary error
#15693: Abstracting out pattern into a pattern synonym fails with scary error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Keywords: | Operating System: Unknown/Multiple PatternSynonyms | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This '''works''' {{{#!hs {-# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #-} import Data.Kind data Ctx :: Type -> Type where E :: Ctx(Type) (:&:) :: a -> Ctx(as) -> Ctx(a -> as) data ApplyT(kind::Type) :: kind -> Ctx(kind) -> Type where AO :: a -> ApplyT(Type) a E AS :: ApplyT(ks) (f a) ctx -> ApplyT(k -> ks) f (a:&:ctx) foo :: ApplyT(Type -> Type -> Type) Either a -> () foo (ASSO (Left a)) = () pattern ASSO a = AS (AS (AO a)) }}} but then you might think, let's give a name (pattern synonym) to `ASSO (Left a)` This '''fails''' {{{#!hs {-# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #-} import Data.Kind data Ctx :: Type -> Type where E :: Ctx(Type) (:&:) :: a -> Ctx(as) -> Ctx(a -> as) data ApplyT(kind::Type) :: kind -> Ctx(kind) -> Type where AO :: a -> ApplyT(Type) a E AS :: ApplyT(ks) (f a) ctx -> ApplyT(k -> ks) f (a:&:ctx) pattern ASSO a = AS (AS (AO a)) pattern ASSOLeft a = ASSO (Left a) }}} {{{ $ ghci -ignore-dot-ghci 464.hs GHCi, version 8.7.20180828: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( hs/464.hs, interpreted ) hs/464.hs:16:22: error: • Couldn't match type ‘k1’ with ‘*’ ‘k1’ is a rigid type variable bound by the signature for pattern synonym ‘ASSOLeft’ at hs/464.hs:16:1-34 Expected type: ApplyT kind a b Actual type: ApplyT (* -> * -> *) Either (a1 ':&: (a20 ':&: 'E)) • In the expression: ASSO (Left a) In an equation for ‘ASSOLeft’: ASSOLeft a = ASSO (Left a) | 16 | pattern ASSOLeft a = ASSO (Left a) | ^^^^^^^^^^^^^ hs/464.hs:16:28: error: • Could not deduce: k1 ~ * from the context: (kind ~ (k -> ks), a ~~ f, b ~~ (a2 ':&: ctx), ks ~ (k1 -> ks1), f a2 ~~ f1, ctx ~~ (a3 ':&: ctx1), ks1 ~ *, f1 a3 ~~ a4, ctx1 ~~ 'E) bound by a pattern with pattern synonym: ASSO :: forall kind (a :: kind) (b :: Ctx kind). () => forall ks k (f :: k -> ks) (a1 :: k) (ctx :: Ctx ks) ks1 k1 (f1 :: k1 -> ks1) (a2 :: k1) (ctx1 :: Ctx ks1) a3. (kind ~ (k -> ks), a ~~ f, b ~~ (a1 ':&: ctx), ks ~ (k1 -> ks1), f a1 ~~ f1, ctx ~~ (a2 ':&: ctx1), ks1 ~ *, f1 a2 ~~ a3, ctx1 ~~ 'E) => a3 -> ApplyT kind a b, in a pattern synonym declaration at hs/464.hs:16:22-34 ‘k1’ is a rigid type variable bound by a pattern with pattern synonym: ASSO :: forall kind (a :: kind) (b :: Ctx kind). () => forall ks k (f :: k -> ks) (a1 :: k) (ctx :: Ctx ks) ks1 k1 (f1 :: k1 -> ks1) (a2 :: k1) (ctx1 :: Ctx ks1) a3. (kind ~ (k -> ks), a ~~ f, b ~~ (a1 ':&: ctx), ks ~ (k1 -> ks1), f a1 ~~ f1, ctx ~~ (a2 ':&: ctx1), ks1 ~ *, f1 a2 ~~ a3, ctx1 ~~ 'E) => a3 -> ApplyT kind a b, in a pattern synonym declaration at hs/464.hs:16:22-34 When matching types a3 :: k1 b0 :: * Expected type: a4 Actual type: Either a1 b0 • In the pattern: Left a In the pattern: ASSO (Left a) In the declaration for pattern synonym ‘ASSOLeft’ | 16 | pattern ASSOLeft a = ASSO (Left a) | ^^^^^^ Failed, no modules loaded. Prelude> }}} ---- Can I, as a user, assume that any valid pattern `foo (ASSO (Left a)) = ...` can be abstracted into a pattern synonym? There error message is too scary for me to sensibly know what to expect -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15693> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15693: Abstracting out pattern into a pattern synonym fails with scary error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: | PatternSynonyms 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): If users can not always abstract patterns into synonyms, are there any rules of thumbs for when that is possible -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15693#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15693: Abstracting out pattern into a pattern synonym fails with scary error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: | PatternSynonyms 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): Initial thoughts. 1. Always start by writing a pattern signature if GADTs are involved. 2. I started to do this, and discovered en route that the signature inferred for `ASSO` is absurd {{{ pattern ASSO :: forall kind (a :: kind) (b :: Ctx kind). () => forall ks k (f :: k -> ks) (a1 :: k) (ctx :: Ctx ks) ks1 k1 (f1 :: k1 -> ks1) (a2 :: k1) (ctx1 :: Ctx ks1) a3. (kind ~ (k -> ks), a ~~ f, b ~~ (a1 ':&: ctx), ks ~ (k1 -> ks1), f a1 ~~ f1, ctx ~~ (a2 ':&: ctx1), ks1 ~ *, f1 a2 ~~ a3, ctx1 ~~ 'E) => forall k ks a1 a2 ctx. (kind ~ (k -> ks), b ~ (a1 :&: (a2 :&: ctx))) => a a1 a2 -> ApplyT kind a b }}} There is no need to quantify over so much, or to have all those redundant constraints. 3. I manually simplifed the signature to {{{ pattern ASSO :: forall kind (a :: kind) (b :: Ctx kind). () => forall k ks a1 a2 ctx. (kind ~ (k -> ks), b ~ (a1 :&: (a2 :&: ctx))) => a a1 a2 -> ApplyT kind a b }}} Is that a correct sigature? Anyway it crashes GHC {{{ WARNING: file compiler/types/TyCoRep.hs, line 2486 in_scope InScope {a_aWo a1_aWp a2_aWq k_aWr ks_aWs ctx_aWt a_aYo} tenv [aWo :-> a_aWo[sk:0], aWp :-> a1_aWp[sk:0], aWq :-> a2_aWq[sk:0], aWr :-> k_aWr[sk:0], aWs :-> ks_aWs[sk:0], aWt :-> ctx_aWt[sk:0]] cenv [] tys [a_aWo[sk:1] a1_aWp[sk:1] a2_aWq[sk:1] -> ApplyT (k_aWr[sk:1] -> ks_aWs[sk:1]) (a_aWo[sk:1] |> <k_aWr[sk:1]>_N ->_N Sym {co_aYt}) (a1_aWp[sk:1] ':&: (a2_aWq[sk:1] ':&: ctx_aWt[sk:1]) |> (Ctx (<k_aWr[sk:1]>_N ->_N Sym {co_aYu}))_N)] cos [] needInScope [aYo :-> a_aYo[sk:1], aYt :-> co_aYt, aYu :-> co_aYu] ghc-stage1: panic! (the 'impossible' happened) (GHC version 8.7.20181003 for x86_64-unknown-linux): ASSERT failed! Type-correct unfilled coercion hole {co_aYt} Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcHsSyn.hs:1805:99 in ghc:TcHsSyn Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug simonpj@cam-05-unx:~/tmp$ ~/5builds/HEAD-4/inplace/bin/ghc-stage1 -c T15693.hs -ddump-types WARNING: file compiler/types/TyCoRep.hs, line 2486 in_scope InScope {kind_aWo a_aWp b_aWq k_aWr ks_aWs a1_aWt a2_aWu ctx_aWv k_aYw k_aYz} tenv [aWo :-> kind_aWo[sk:0], aWp :-> a_aWp[sk:0], aWq :-> b_aWq[sk:0], aWr :-> k_aWr[sk:0], aWs :-> ks_aWs[sk:0], aWt :-> a1_aWt[sk:0], aWu :-> a2_aWu[sk:0], aWv :-> ctx_aWv[sk:0]] cenv [] tys [kind_aWo[sk:1] ~ (k_aWr[sk:2] -> ks_aWs[sk:2]), b_aWq[sk:1] ~ (a1_aWt[sk:2] ':&: (a2_aWu[sk:2] ':&: ctx_aWv[sk:2]) |> (Ctx (Sym {co_aYy}))_N)] cos [] needInScope [aYw :-> k_aYw[sk:2], aYy :-> co_aYy, aYz :-> k_aYz[sk:2]] WARNING: file compiler/types/TyCoRep.hs, line 2486 in_scope InScope {kind_aWo a_aWp b_aWq k_aWr ks_aWs a1_aWt a2_aWu ctx_aWv k_aYw k_aYz} tenv [aWo :-> kind_aWo[sk:0], aWp :-> a_aWp[sk:0], aWq :-> b_aWq[sk:0], aWr :-> k_aWr[sk:0], aWs :-> ks_aWs[sk:0], aWt :-> a1_aWt[sk:0], aWu :-> a2_aWu[sk:0], aWv :-> ctx_aWv[sk:0]] cenv [] tys [(a_aWp[sk:1] |> {co_aYy}) a1_aWt[sk:2] a2_aWu[sk:2] -> ApplyT kind_aWo[sk:1] a_aWp[sk:1] b_aWq[sk:1]] cos [] needInScope [aYw :-> k_aYw[sk:2], aYy :-> co_aYy, aYz :-> k_aYz[sk:2]] WARNING: file compiler/types/TyCoRep.hs, line 2486 in_scope InScope {kind_aWo a_aWp b_aWq k_aZT k_aZU k_aZV ks_aZW a1_aZX a2_aZY ctx_aZZ} tenv [aWr :-> k_aZV[tau:4], aWs :-> ks_aZW[tau:4], aWt :-> a1_aZX[tau:4], aWu :-> a2_aZY[tau:4], aWv :-> ctx_aZZ[tau:4], aYw :-> k_aZU[tau:4], aYz :-> k_aZT[tau:4]] cenv [] tys [kind_aWo[sk:0] ~ (k_aWr[sk:0] -> ks_aWs[sk:0]), b_aWq[sk:0] ~ (a1_aWt[sk:0] ':&: (a2_aWu[sk:0] ':&: ctx_aWv[sk:0]) |> (Ctx (Sym {co_aYy}))_N)] cos [] needInScope [aWo :-> kind_aWo[sk:0], aWq :-> b_aWq[sk:0], aYy :-> co_aYy] ghc-stage1: panic! (the 'impossible' happened) (GHC version 8.7.20181003 for x86_64-unknown-linux): ASSERT failed! Type-correct unfilled coercion hole {co_aYy} Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcHsSyn.hs:1805:99 in ghc:TcHsSyn Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} 4. I GADT-ified it thus {{{ pattern ASSO :: a a1 a2 -> ApplyT (k -> ks) a (a1 :&: (a2 :&: ctx)) }}} (NB: as the manual says, this isn't quite the same as the form with equality constraints.) But that crashed GHC too {{{ WARNING: file compiler/types/TyCoRep.hs, line 2486 in_scope InScope {a_aWo a1_aWp a2_aWq k_aWr ks_aWs ctx_aWt a_aYo} tenv [aWo :-> a_aWo[sk:0], aWp :-> a1_aWp[sk:0], aWq :-> a2_aWq[sk:0], aWr :-> k_aWr[sk:0], aWs :-> ks_aWs[sk:0], aWt :-> ctx_aWt[sk:0]] cenv [] tys [a_aWo[sk:1] a1_aWp[sk:1] a2_aWq[sk:1] -> ApplyT (k_aWr[sk:1] -> ks_aWs[sk:1]) (a_aWo[sk:1] |> <k_aWr[sk:1]>_N ->_N Sym {co_aYt}) (a1_aWp[sk:1] ':&: (a2_aWq[sk:1] ':&: ctx_aWt[sk:1]) |> (Ctx (<k_aWr[sk:1]>_N ->_N Sym {co_aYu}))_N)] cos [] needInScope [aYo :-> a_aYo[sk:1], aYt :-> co_aYt, aYu :-> co_aYu] ghc-stage1: panic! (the 'impossible' happened) (GHC version 8.7.20181003 for x86_64-unknown-linux): ASSERT failed! Type-correct unfilled coercion hole {co_aYt} Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable assertPprPanic, called at compiler/typecheck/TcHsSyn.hs:1805:99 in ghc:TcHsSyn Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug }}} So we have multiple issues here * GHC should not crash * We should not infer such a redundant signature. What signature do you expect? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15693#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15693: Abstracting out pattern into a pattern synonym fails with scary error -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.6.1 Resolution: | Keywords: | PatternSynonyms 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): Ah.. I guess #15694 is reporting the crashes, I missed that. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15693#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC