content: module TypeEq(main) where
  
  foo :: forall a . (a ~ Bool) => a -> a
  foo = not
  
  data Exp a
    = (a ~ Int)  => Int Int
    | (a ~ Int)  => Add (Exp Int) (Exp Int)
    | (a ~ Bool) => Equ (Exp Int) (Exp Int)
    |               Iff (Exp Bool) (Exp a) (Exp a)
  
  eval :: forall a . Exp a -> a
  eval (Int i) = i
  eval (Add e1 e2) = eval e1 + eval e2
  eval (Equ e1 e2) = eval e1 == eval e2
  eval (Iff c e1 e2) = if eval c then eval e1 else eval e2
  
  e1 :: Exp Int
  e1 = Iff (Add (Int 1) (Int 2) `Equ` Int 3) (Int 1) (Int 999)
  
  data GExp a where
    GInt :: Int -> GExp Int
    GAdd :: GExp Int -> GExp Int -> GExp Int
    GEqu :: GExp Int -> GExp Int -> GExp Bool
    GIff :: GExp Bool -> GExp a -> GExp a -> GExp a
  
  geval :: GExp a -> a
  geval (GInt i) = i
  geval (GAdd e1 e2) = geval e1 + geval e2
  geval (GEqu e1 e2) = geval e1 == geval e2
  geval (GIff c e1 e2) = if geval c then geval e1 else geval e2
  
  ge1 :: GExp Int
  ge1 = GIff (GAdd (GInt 1) (GInt 2) `GEqu` GInt 3) (GInt 1) (GInt 999)
  
  data ParenResult a where
    ParenResult :: a -> (ParenResult a)
  
  data Foo c a where
    Foo :: a -> Foo c a
  
  unFoo :: Foo c a -> a
  unFoo (Foo a) = a
  
  data Bar b a where
    Bar :: Bar a a
  
  bar :: Bar b a -> a -> b
  bar c x = case c of Bar -> x
  
  data Tree a where
    Leaf :: a -> Tree a
    Branch :: Tree a -> Tree a -> Tree a
  
  toList :: Tree a -> [a]
  toList t = go t []
    where
      go (Leaf x) xs = x:xs
      go (Branch l r) xs = go l (go r xs)
  
  data R a where
    Pure :: a -> R a
    Map :: (a -> b) -> R a -> R b
    Alt :: R a -> R a -> R a
  
  instance (Show a) => Show (R a) where
    show (Pure a) = "Pure " ++ show a
  
  splat :: R a -> [R a]
  splat t = go t []
    where
      go (Alt l r) ts = go l (go r ts)
      go t ts = t:ts
  
  main :: IO ()
  main = do
    print (foo True)
    print (eval e1)
    print (geval ge1)
    print (unFoo (Foo (2::Int)))
    print (toList (Branch (Leaf (1::Int)) (Branch (Leaf 2) (Leaf 3))))
    print (splat (Alt (Pure 'a') (Pure 'b')))
  