{-# LANGUAGE GADTs
           , TemplateHaskell
           , KindSignatures
           , ScopedTypeVariables
           , TypeOperators
  #-}

module LCTyped where

import Unbound.LocallyNameless
import Data.Type.Equality

import Unsafe.Coerce (unsafeCoerce)



------------------------------------------------------------

data Res1 c a where
  Result1   :: Rep b => a :=: (c b) -> Res1 c a
  NoResult1 :: Res1 c a

destr1 :: R a -> R (c d) -> Res1 c a
destr1 (Data (DT s1 ((_ :: R b) :+: MNil)) _)
       (Data (DT s2 _) _)
  | s1 == s2  = Result1 (unsafeCoerce Refl :: a :=: (c b))
  | otherwise = NoResult1
destr1 _ _ = NoResult1

data Res2 c2 a where
  Result2   :: (Rep d, Rep e) => a :=: (c2 d e) -> Res2 c2 a
  NoResult2 :: Res2 c2 a

destr2 :: R a -> R (c2 d e) -> Res2 c2 a
destr2 (Data (DT s1 ((_ :: R d) :+: (_ :: R e) :+: MNil)) _)
       (Data (DT s2 _) _)
  | s1 == s2  = Result2 (unsafeCoerce Refl :: a :=: (c2 d e))
  | otherwise = NoResult2
destr2 _ _ = NoResult2

------------------------------------------------------------


data V :: * -> * -> * where
  VZ :: V (a,env) a
  VS :: V env a -> V (b,env) a

data Tm :: * -> * -> * where
  Var :: V env a -> Tm env a
  Lam :: Tm (a,env) b -> Tm env (a -> b)
  App :: Tm env (a -> b) -> Tm env a -> Tm env b

$(derive [''V, ''Tm])