@@ -0,0 +1,23 @@
1+{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeOperators, TypeFamilies, PolyKinds, EmptyDataDecls #-}
2+{-# OPTIONS_GHC -fplugin=TySet #-}
3+
4+import GHC.TypeLits
5+import TySet
6+
7+data Container (a :: *) where
8+ Empty :: Container (Set '[])
9+ Ext :: a -> Container (Set s) -> Container (Set (Union '[a] s))
10+
11+data Natural (a :: Nat) where
12+ Z :: Natural 0
13+ S :: Natural n -> Natural (n + 1)
14+
15+-- Should be typeable with the plugin
16+{-
17+foo :: Container (Set '[Natural 1, Natural 2, Natural 3])
18+foo = Ext (S $ S Z) (Ext (S Z) (Ext (S $ S $ S Z) Empty))
19+-}
20+
21+dup :: Container (Set s) -> Container (Set (Union s s))
22+dup Empty = Empty
23+dup (Ext x xs) = Ext x (Ext x (dup xs))