{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE IncoherentInstances #-} -- TypeEq requires incoherent instances
 
-- type-level boolean
data T = T
data F = F
 
-- type-level type equality
class TypeEq' () x y b => TypeEq x y b | x y -> b where
  type'eq :: x -> y -> b
  type'eq _ _ = undefined::b
class TypeEq' q x y b | q x y -> b
class TypeEq'' q x y b | q x y -> b
instance TypeEq' () x y b => TypeEq x y b
instance b ~ T => TypeEq' () x x b
instance TypeEq'' q x y b => TypeEq' q x y b
instance TypeEq'' () x y F
 
-- recursion binder and variable
data Rec n u = Rec n u deriving Show
data Var n = Var n deriving Show
 
-- folding
class RecFold m u r | m u -> r  where fold' :: m -> u -> r
instance RecFold m (Var n) (Var n) where fold' _ v = v 
instance (TypeEq m n b, RecFoldCont b m n a r) => RecFold m (Rec n a) r where -- fold if m = n
  fold' m (Rec n a) = fold'cont (type'eq m n) m n a
 
class RecFoldCont b m n a r | b m n a -> r where
   fold'cont :: b -> m -> n -> a -> r
instance RecFoldCont T m n a (Var m) where -- fold
   fold'cont b m n a = Var m
instance (RecFold m a r)
      => RecFoldCont F m n a (Rec n r) where -- do not fold
   fold'cont b m n a =  Rec n (fold' m a)
 
 
-- unfolding
class RecUnfold m r s u | m r s -> u where
  unfold' :: m -> r -> s -> u
instance (RecFold n s s', RecUnfold m a s' a') => RecUnfold m (Rec n a) s (Rec n a') where
  unfold' m (Rec n a) s = Rec n (unfold' m a (fold' n s))
instance (TypeEq m n b, RecUnfoldCont b m n s a) => RecUnfold m (Var n) s a where -- unfold if m = n
  unfold' m (Var n) s = unfoldCont (type'eq m n) m n s
 
class RecUnfoldCont b m n s a | b m n s -> a where
  unfoldCont :: b -> m -> n -> s -> a
instance RecUnfoldCont T m m s (Rec m s) where -- unfold
  unfoldCont _ m _ s = Rec m s
instance RecUnfoldCont F m n s (Var n) where -- do not unfold
  unfoldCont _ _ n _ = Var n
 
-- type level numerals
data Z = Z
data S n = S n
instance Show Z where show _ = "Z"
instance Show n => Show (S n) where show ~(S n) = "(S "++show n++")"
 
-- assign a natural number to each binder
class RecNumbering n r
instance (RecNumbering (S n) u1, m ~ n) => RecNumbering n (Rec m u1) where
instance RecNumbering n (Var m)
 
num :: RecNumbering (S Z) r => Rec Z r -> Rec Z r
num = id
 
rec :: (RecFold n u r, RecUnfold n r r u) => u -> Rec n r -- RecUnfold ensures that our fold/unfold is isomorphic
rec x = (\n -> Rec n (fold' n x)) undefined
 
unfold :: (RecFold m u r, RecUnfold m r r u) => Rec m r -> u
unfold (Rec m r) = unfold' m r r 
 
-- 再帰させたい型
data A x = A x deriving Show
data B x = B x deriving Show
data C x y = C x y deriving Show
unA (A x) = x; unB (B x) = x; unC1 (C x _) = x; unC2 (C _ y) = y
 
instance RecFold m x x' => RecFold m (A x) (A x') where
  fold' m (A x) = A (fold' m x)
instance RecFold m x x' => RecFold m (B x) (B x') where
  fold' m (B x) = B (fold' m x)
instance (RecFold m x x', RecFold m y y') => RecFold m (C x y) (C x' y') where
  fold' m (C x y) = C (fold' m x) (fold' m y)
instance RecUnfold m u s u' => RecUnfold m (A u) s (A u') where
  unfold' m (A u) s = A (unfold' m u s)
instance RecUnfold m u s u' => RecUnfold m (B u) s (B u') where
  unfold' m (B u) s = B (unfold' m u s)
instance (RecUnfold m u s u', RecUnfold m v s v') => RecUnfold m (C u v) s (C u' v') where
  unfold' m (C u v) s = C (unfold' m u s) (unfold' m v s)
instance RecNumbering n u => RecNumbering n (A u)
instance RecNumbering n u => RecNumbering n (B u)
instance (RecNumbering n u, RecNumbering n v) => RecNumbering n (C u v)
 
 
 
-- *Main> let x = rec (A y) ; y = rec (B (C x y)); _ = num x
-- *Main> :t x
-- x :: Rec Z (A (Rec (S Z) (B (C (Var Z) (Var (S Z))))))
-- *Main> x
-- Rec Z (A (Rec (S Z) (B (C (Var Z) (Var (S Z))))))
-- 
-- *Main> unfold x
-- A (Rec (S Z) (B (C (Rec Z (A (Var (S Z)))) (Var (S Z)))))
-- *Main> :t unfold x
-- unfold x
--   :: A (Rec (S Z) (B (C (Rec Z (A (Var (S Z)))) (Var (S Z)))))
-- 
-- *Main> unC1 $ unB $ unfold $ unA $ unfold x
-- Rec Z (A (Rec (S Z) (B (C (Var Z) (Var (S Z))))))
-- *Main> :t unC1 $ unB $ unfold $ unA $ unfold x
-- unC1 $ unB $ unfold $ unA $ unfold x
--   :: Rec Z (A (Rec (S Z) (B (C (Var Z) (Var (S Z))))))