gistfile1.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}

import Data.Type.Equality
import GHC.TypeLits

import Data.Syntactic
import Data.Syntactic.TypeUniverse



newtype Zq (q :: Nat) = Zq Int

data ZqType a
  where
    ZqType :: KnownNat q => Proxy q -> ZqType (Full (Zq q))

instance (ZqType :<: t, KnownNat q) => Typeable t (Zq q)
  where
    typeRep' = inj (ZqType Proxy)

instance TypeEq ZqType t
  where
    typeEqSym (ZqType p, Nil) (ZqType q, Nil) = do
        Refl <- sameNat p q
        return Dict

t1 = typeRep :: TypeRep (IntType :+: ZqType :+: BoolType) (Zq 1)
t2 = typeRep :: TypeRep (IntType :+: ZqType :+: BoolType) (Zq 2)

test = do
    check t1 t1
    check t1 t2
  where
    check a b = case typeEq a b of
      Nothing -> print "different"
      _       -> print "same"