Typed terms with type promotion and "type categories", in reply to https://groups.google.com/forum/#!topic/haskellers-montreal/cmn24NLaAgU

Main.hs

{-# LANGUAGE GADTs, StandaloneDeriving, TypeFamilies, MultiParamTypeClasses #-}
module Main where

import Data.Word


type family Promote a b where
  Promote Word8  Word16 = Word16
  Promote Word16 Word8  = Word16
  Promote a a = a

data Expr cat a where
  Const8 :: Word8 -> Expr Int Word8
  Const16 :: Word16 -> Expr Int Word16
  ConstFloat :: Float -> Expr Float Float
  Add :: Expr cat a -> Expr cat b -> Expr cat (Promote a b)

deriving instance Show (Expr cat a)


class HEq a b where
  heq :: a -> b -> Bool

instance HEq (Expr cat a) (Expr cat b) where
  heq (Const8 x) (Const8 x') = x == x'
  heq (Const16 x) (Const16 x') = x == x'
  heq (ConstFloat x) (ConstFloat x') = x == x'
  heq (Add x y) (Add x' y') = x `heq` x' && y `heq` y'
  heq _ _ = False

instance Eq (Expr cat a) where
  (==) = heq


main = putStrLn "typechecks."