T150.hs

module T150 where

import Control.Monad.Trans.Class
import Data.Kind
import Data.Singletons.TH
import Data.Singletons.TH.Options
import Singletons.Nat

$(withOptions defaultOptions{genSingKindInsts = False} $
    singletons $ lift
    [d| data Fin :: Nat -> Type where
          FZ :: Fin (Succ n)
          FS :: Fin n -> Fin (Succ n)

        data Foo :: Type -> Type where
          MkFoo1 :: Foo Bool
          MkFoo2 :: Foo Ordering

        data Vec :: Nat -> Type -> Type where
          VNil  :: Vec Zero a
          VCons :: a -> Vec n a -> Vec (Succ n) a

        headVec :: Vec (Succ n) a -> a
        headVec (VCons x _) = x

        tailVec :: Vec (Succ n) a -> Vec n a
        tailVec (VCons _ xs) = xs

        (!) :: Vec n a -> Fin n -> a
        VCons x _  ! FZ   = x
        VCons _ xs ! FS n = xs ! n
        VNil       ! n    = case n of {}

        mapVec :: (a -> b) -> Vec n a -> Vec n b
        mapVec _ VNil         = VNil
        mapVec f (VCons x xs) = VCons (f x) (mapVec f xs)

        data Equal :: Type -> Type -> Type where
          Reflexive :: Equal a a

        symmetry :: Equal a b -> Equal b a
        symmetry Reflexive = Reflexive

        transitivity :: Equal a b -> Equal b c -> Equal a c
        transitivity Reflexive Reflexive = Reflexive

        data HList :: [Type] -> Type where
          HNil  :: HList '[]
          HCons :: x -> HList xs -> HList (x:xs)

        data Obj :: Type where
          Obj :: a -> Obj
    |])