Messing around with type elaboration from ADT -> GADT

gistfile1.txt

data AT
data BT
data CT

type AAttrs = Int
type BAttrs = Int
type CAttrs = Int

data Elem eltype c where
  A :: (Eq c, Show c) => AAttrs -> c -> Elem AT c
  B :: (Eq c, Show c) => BAttrs -> c -> Elem BT c
  C :: (Eq c, Show c) => CAttrs -> c -> Elem CT c

Witness.hs

{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE TypeFamilies  #-}
{-# LANGUAGE RankNTypes  #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE TypeSynonymInstances  #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE ExistentialQuantification  #-}
{-# LANGUAGE GADTs  #-}

module Witness where
-- https://gist.github.com/sacundim/5386823

-- http://augustss.blogspot.ca/2009/06/more-llvm-recently-someone-asked-me-on.html

-- import Data.Reflection
import Data.Maybe
import Control.Monad
-- import Data.Proxy      -- from tagged

data UExp
  = UDbl Double
  | UBol Bool
  | UString String
    deriving (Show, Eq)

data TTyp a where
  TTBol ::                     TTyp Bool
  TTDbl ::                     TTyp Double
  TTString ::                  TTyp String
  TTArr :: TTyp a -> TTyp b -> TTyp (a->b)

deriving instance Show (TTyp a)
deriving instance Eq (TTyp a)

data TExp a where
  TDbl    :: Double  -> TExp Double
  TBol    :: Bool    -> TExp Bool
  TString :: String  -> TExp String

deriving instance Show (TExp a)
deriving instance Eq (TExp a)

data ATExp = forall a . TExp a ::: TTyp a
deriving instance Show ATExp

typeCheckExp :: UExp -> Maybe ATExp
typeCheckExp (UDbl d) =
  return $ TDbl d ::: TTDbl
typeCheckExp (UBol b) =
  return $ TBol b ::: TTBol
typeCheckExp (UString s) =
  return $ TString s ::: TTString

data Equal a b where
  Eq :: Equal a a

class Type a where
  theType :: TTyp a
instance Type Double where
  theType = TTDbl
instance Type Bool where
  theType = TTBol
instance Type String where
  theType = TTString

test :: TTyp a -> TTyp b -> Maybe (Equal a b)
test TTBol TTBol = return Eq
test TTDbl TTDbl = return Eq
test TTString TTString = return Eq
test _ _ = Nothing

uxp :: UExp
uxp = UBol True

texp :: TExp Bool
texp = TBol True

aexp :: ATExp
aexp = texp ::: TTBol

extract :: TTyp a -> ATExp -> Maybe (TExp a)
extract s (e ::: t) = do
  Eq <- test t s
  return e

extractExp :: (Type a) => ATExp -> Maybe (TExp a)
extractExp = extract theType

toTExp :: (Type a) => UExp -> Maybe (TExp a)
toTExp = extractExp <=< typeCheckExp

compileExp :: TExp a -> a
compileExp (TDbl d) = d
compileExp (TBol b) = b
compileExp (TString s) = s

compile :: (Type a) => UExp -> a
compile = compileExp . fromJust . toTExp

compileAExp :: (Type a) => TTyp a -> ATExp -> a
compileAExp t = compileExp . fromJust . extract t

matchU :: UExp -> IO ()
matchU u =
  case typeCheckExp u of
    Nothing -> print "oops"
    Just (_ ::: t) -> case show t of
      "TTBol" -> print $ not (compile u)
      -- "TTBol" -> print $ not (compile u)
      "TTDbl" -> print $ 10.2 * (compile u :: Double)
      "TTString" -> print $ reverse (compile u :: String)

main :: IO ()
main = do
  matchU $ UString "woah"
  matchU $ UDbl 2.0
  matchU $ UBol True