GitLab

I'd like to write this code:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo (Sing(.., SCons)) where

data family Sing (a :: k)

data instance Sing (z :: [a]) where
  SNil :: Sing '[]
  (:%) :: Sing x -> Sing xs -> Sing (x:xs)

pattern SCons :: forall a (z :: [a]). ()
              => forall (x :: a) (xs :: [a]). z ~ (x:xs)
              => Sing x -> Sing xs -> Sing z
pattern SCons x xs = (:%) x xs
{-# COMPLETE SNil, SCons #-}

But alas, GHC will not let me:

$ ghci Bug.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo              ( Bug.hs, interpreted )

Bug.hs:7:13: error:
    • Pattern synonyms can be bundled only with datatypes.
    • In the pattern synonym: SCons
      In the export: Sing(.., SCons)
  |
7 | module Foo (Sing(.., SCons)) where
  |             ^^^^^^^^^^^^^^^
Failed, 0 modules loaded.

Can this restriction be lifted for data families?

Trac metadata

Trac field	Value
Version	8.2.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	mpickering
Operating system
Architecture