@@ -1,4 +1,4 @@
1−{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeOperators, TypeFamilies, PolyKinds, EmptyDataDecls #-}
1+{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeOperators, TypeFamilies, PolyKinds, EmptyDataDecls, StandaloneDeriving #-}
22{-# OPTIONS_GHC -fplugin=TySet #-}
33
44import GHC.TypeLits
@@ -6,18 +6,34 @@ import TySet
66
77data Container (a :: *) where
88 Empty :: Container (Set '[])
9− Ext :: a -> Container (Set s) -> Container (Set (Union '[a] s))
9+ Ext :: Show a => a -> Container (Set s) -> Container (Set (Union '[a] s))
10+
11+instance Show (Container a) where
12+ show Empty = "Empty"
13+ show (Ext x xs) = "Ext " ++ show x ++ " " ++ show xs
1014
1115data Natural (a :: Nat) where
1216 Z :: Natural 0
1317 S :: Natural n -> Natural (n + 1)
1418
19+instance Show (Natural a) where
20+ show Z = "Z"
21+ show (S n) = "S " ++ (show n)
22+
1523-- Should be typeable with the plugin
16−{-
17−foo :: Container (Set '[Natural 1, Natural 2, Natural 3])
24+
25+foo :: Container (Set '[Natural 3, Natural 2, Natural 1])
1826foo = Ext (S $ S Z) (Ext (S Z) (Ext (S $ S $ S Z) Empty))
19−-}
2027
28+foo2 :: Container (Set '[Natural 2, Natural 1])
29+foo2 = Ext (S $ S Z) (Ext (S Z) Empty)
30+
31+bar :: (Container (Set '[Natural 2, Natural 1])) -> Container (Set '[Natural 1])
32+bar (Ext (S (S Z)) (Ext (S Z) Empty)) = Ext (S Z) Empty
33+bar (Ext (S Z) (Ext (S (S Z)) Empty)) = Ext (S Z) Empty
34+
35+{-
2136dup :: Container (Set s) -> Container (Set (Union s s))
2237dup Empty = Empty
23−dup (Ext x xs) = Ext x (Ext x (dup xs))
38+dup (Ext x xs) = Ext x (Ext x (dup xs))
39+-}