Opened 12 months ago

Last modified 12 months ago

## #15693 new bug

# Abstracting out pattern into a pattern synonym fails with scary error

Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | 8.6.1 |

Component: | Compiler | Version: | 8.6.1 |

Keywords: | PatternSynonyms | Cc: | |

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | None/Unknown | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### Description

This **works**

{-# 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**

{-# 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

### Change History (3)

### comment:1 Changed 12 months ago by

### comment:2 Changed 12 months ago by

Initial thoughts.

- Always start by writing a pattern signature if GADTs are involved.

- I started to do this, and discovered en route that the signature inferred for
`ASSO`

is absurdpattern 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.

- 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

- 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 tooWARNING: 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?

**Note:**See TracTickets for help on using tickets.

If users can not always abstract patterns into synonyms, are there any rules of thumbs for when that is possible