Pattern synonym can't unify types within type-level list

Question

I'm getting an error when trying to define a pattern synonym based on a GADT that has a type-level list.

I managed to boil it down to this example:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PatternSynonyms #-}
module Example where

data L (as :: [*]) where
  L :: a -> L '[a]

pattern LUnit = L ()

Gives me:

Example.hs:11:17:
    Couldn't match type ‘a’ with ‘()’
      ‘a’ is a rigid type variable bound by
          the type signature for Example.$bLUnit :: (t ~ '[a]) => L t
          at Example.hs:11:17
    Expected type: L t
      Actual type: L '[()]
    In the expression: L ()
    In an equation for ‘$bLUnit’: $bLUnit = L ()

Example.hs:11:19:
    Could not deduce (a ~ ())
    from the context (t ~ '[a])
      bound by a pattern with constructor
                 L :: forall a. a -> L '[a],
               in a pattern synonym declaration
      at Example.hs:11:17-20
      ‘a’ is a rigid type variable bound by
          a pattern with constructor
            L :: forall a. a -> L '[a],
          in a pattern synonym declaration
          at Example.hs:11:17
    In the pattern: ()
    In the pattern: L ()

Is this a bug, or am I doing something wrong?

Gulgee

I think you at least need a pattern signature, but the documentation doesn't seem to make it very clear whether it's possible to make the type of a pattern synonym for a GADT constructor as polymorphic as the constructor itself. – Kapor

Answer 1

Thanks to dfeuer's comment and this ticket, I was able to get my example code to compile by adding a type signature to the pattern definition:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PatternSynonyms #-}
module Example where

data L (as :: [*]) where
  L :: a -> L '[a]

pattern LUnit :: L '[()]
pattern LUnit = L ()

Which also generalizes nicely to polymorphic patterns

data F (fs :: [* -> *]) a where
  F :: f a -> F '[f] a

pattern FId :: a -> F '[Identity] a
pattern FId a = F (Identity a)

Gulgee