testsuite/tests/patsyn/should_compile/T14058a.hs


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
module T14058a (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 #-}