{-# LANGUAGE GADTs
           , TypeFamilies
           , TypeOperators
           , KindSignatures
           , MultiParamTypeClasses
           , EmptyDataDecls
           , FlexibleInstances
           #-}

module TreeRep where

import Generics.MultiRec.Elems.Many

data Tree a b = Leaf a | Branch (Tree a b) b (Tree a b) deriving Show

data TreeU :: (* -> *) -> * -> * -> * where
    Tree :: TreeU (a :|: b :|: Nil) (Tree a b) Zero

data Leaf
instance Constructor Leaf where
  conName _ = "Leaf"

data Branch
instance Constructor Branch where
  conName _ = "Branch"

type instance PF TreeU = (    C Leaf   (I (Elem Zero)) 
                          :+: C Branch (I (Rec Zero) :*: I (Elem (Suc Zero)) :*: I (Rec Zero))
                         ) :>: Zero

instance Fam TreeU (a :|: b :|: Nil) where
    from Tree (Leaf a)       = Tag (L (C (I (CL (Z a)))))
    from Tree (Branch l b r) = Tag (R (C (I (CR (R0 Tree l)) :*: I (CL (S (Z b))) :*: I (CR (R0 Tree r)))))
    to Tree (Tag (L (C (I (CL (Z a)))))) = Leaf a
    to Tree (Tag (R (C (I (CR (R0 Tree l)) :*: I (CL (S (Z b))) :*: I (CR ((R0 Tree r))))))) = Branch l b r

instance El (Proof (TreeU (a :|: b :|: Nil))) Zero where
    proof = Proof Tree

instance EqS (Proof (TreeU (a :|: b :|: Nil))) where
    eqS (Proof Tree) (Proof Tree) = Just Refl

instance EqS2 (TreeU (a :|: b :|: Nil)) where
    eqS2 Tree Tree = Just (Refl, Refl)