[GHC] #15693: Abstracting out pattern into a pattern synonym fails with scary error

30 Sep 2018

      #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