Skip to content

Instantly share code, notes, and snippets.

@emilaxelsson
Last active August 29, 2015 14:01
Show Gist options
  • Save emilaxelsson/ed5ffd25f11e56e6ccfc to your computer and use it in GitHub Desktop.
Save emilaxelsson/ed5ffd25f11e56e6ccfc to your computer and use it in GitHub Desktop.
{-# 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"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment