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 Iceland_jack

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

comment:2 Changed 12 months ago by simonpj

Initial thoughts.

  1. Always start by writing a pattern signature if GADTs are involved.
  1. 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.
  1. 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
  1. 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?

comment:3 Changed 12 months ago by simonpj

Ah.. I guess #15694 is reporting the crashes, I missed that.

Note: See TracTickets for help on using tickets.