{-# LANGUAGE
      FlexibleContexts,
      GeneralizedNewtypeDeriving,
      ParallelListComp,
      PatternGuards,
      RankNTypes,
      RelaxedPolyRec #-}
module TypeRel (
  -- * Type operations
  -- ** Equality and subtyping
  AType(..), subtype, jointype,
  -- ** Queries and conversions
  qualConst, abstractTyCon,
  -- ** Tycon substitutions
  TyConSubst, makeTyConSubst,
  applyTyConSubst, applyTyConSubstInTyCon,
  replaceTyCon, replaceTyCons,
  substTyCons, substTyCon,
  -- * Tests
  tests,
) where

import Env
import ErrorST
import Ppr ()
import Type
import Util
import Viewable

import qualified Control.Monad.Reader as CMR
import Control.Monad.Error
import Data.Generics (Data, everywhere, mkT, extT)
import Data.Monoid
import qualified Data.Map as M
import qualified Data.Set as S

import qualified Test.HUnit as T

-- | Remove the concrete portions of a type constructor.
abstractTyCon :: TyCon -> TyCon
abstractTyCon tc = tc { tcCons = ([], empty), tcNext = Nothing }

-- | A substitution mapping type constructors to other type
--   constructors
newtype TyConSubst = TyConSubst { unTyConSubst :: M.Map Int TyCon }
  deriving Monoid

-- | Construct a tycon substitution from a list of tycons and a list
--   to map them to.
makeTyConSubst :: [TyCon] -> [TyCon] -> TyConSubst
makeTyConSubst tcs tcs' =
  TyConSubst (M.fromList [ (tcId tc, tc') | tc <- tcs | tc' <- tcs' ])

-- | Apply a tycon substitution to any SYB data.
applyTyConSubst :: Data a => TyConSubst -> a -> a
applyTyConSubst subst = loop where
  loop :: Data a => a -> a
  loop  = everywhere (mkT tycon `extT` tyapp)
  --
  tycon :: TyCon -> TyCon
  tycon tc
    | Just tc' <- M.lookup (tcId tc) (unTyConSubst subst)
                = applyTyConSubstInTyCon subst tc'
    | otherwise = tc
  --
  tyapp :: Type -> Type
  tyapp (TyApp tc ts _) = tyApp tc ts
  tyapp t               = t

-- | Apply a tycon substitution "inside" the right-hand side of
--   a tycon, but don't replace the tycon itself.
applyTyConSubstInTyCon :: TyConSubst -> TyCon -> TyCon
applyTyConSubstInTyCon subst tc =
  tc {
    tcNext = applyTyConSubst subst (tcNext tc),
    tcCons = applyTyConSubst subst (tcCons tc)
  }

-- | Given a list of type constructors and something traversable,
--   find all constructors with the same identity as the given type one, and
--   replace them.  We can use this for type abstraction by redacting
--   data constructor or synonym expansions.  It also replaces within
--   the list of type constructors themselves, which ties the knot for
--   recursive type constructors.
replaceTyCons :: Data a => [TyCon] -> a -> a
replaceTyCons tcs0 = substTyCons tcs0 tcs0

replaceTyCon :: Data a => TyCon -> a -> a
replaceTyCon tc = replaceTyCons [tc]

-- Give a list of tycons to replace and a list of tycons to replace them
-- with, replaces them all recursively, including knot-tying
substTyCons :: Data a => [TyCon] -> [TyCon] -> a -> a
substTyCons tcs tcs' = applyTyConSubst (makeTyConSubst tcs tcs')

-- | Replace all occurrences of the first tycon with the second
substTyCon :: Data a => TyCon -> TyCon -> a -> a
substTyCon tc tc' = substTyCons [tc] [tc']

-- | The constant bound on the qualifier of a type
qualConst :: Type -> QLit
qualConst  = qConstBound . qualifier

-- | A fresh type for defining alpha equality up to mu.
newtype AType = AType { unAType :: Type }

-- | On AType, we define simple alpha equality, up to mu and operator
--   reduction, which we then use
--   to keep track of where we've been when we define type equality
--   that understands mu and reduction.
instance Eq AType where
  te1 == te2 = compare te1 te2 == EQ

instance Ord AType where
  te1 `compare` te2 = unAType te1 =?= unAType te2
    where
      (=?=) :: Type -> Type -> Ordering
      TyApp tc ts _ =?= TyApp tc' ts' _
        = tc `compare` tc'
           `thenCmp` map AType ts `compare` map AType ts'
      TyVar x       =?= TyVar x'
        = x `compare` x'
      TyFun q t1 t2 =?= TyFun q' t1' t2'
        = q `compare` q'
           `thenCmp` t1 =?= t1'
           `thenCmp` t2 =?= t2'
      TyQu u x t    =?= TyQu u' x' t'
        = u `compare` u'
           `thenCmp` tvqual x `compare` tvqual x'
           `thenCmp` tysubst x a t =?= tysubst x' a t'
              where a = TyVar (fastFreshTyVar x (maxtv (t, t')))
      TyMu x t    =?= TyMu x' t'
        = tvqual x `compare` tvqual x'
           `thenCmp` tysubst x a t =?= tysubst x' a t'
              where a = TyVar (fastFreshTyVar x (maxtv (t, t')))
      TyApp _ _ _   =?= _           = LT
      _             =?= TyApp _ _ _ = GT
      TyVar _       =?= _           = LT
      _             =?= TyVar _     = GT
      TyFun _ _ _   =?= _           = LT
      _             =?= TyFun _ _ _ = GT
      TyQu _ _ _    =?= _           = LT
      _             =?= TyQu _ _ _  = GT

type UT s t a = CMR.ReaderT (TCS s t) (ST t String) a

-- | An environment mapping mu-bound type variables to their
--   definition for unrolling ('Left') or forall-bound variables
--   to a pair of lower and upper bounds, for instantiation ('Right')
type UEnv t = M.Map TyVarR (UVar t)
type UVar t = (Int, STRef t (Type, Type))

data TCS s t = TCS {
  -- | Pairs of types previously seen, and thus considered related
  --   if seen again.
  tcsSeen    :: STRef t (M.Map (AType, AType) s),
  -- | A supply of fresh type variables
  tcsSupply  :: STRef t [QLit -> TyVarR],
  -- | The number of instantiated foralls we are currently under
  tcsLevel   :: Int,
  -- | The environment for the left side of the relation
  tcsEnv1    :: UEnv t,
  -- | The environment for the right side of the relation
  tcsEnv2    :: UEnv t
}

data Field s t = Field {
  get    :: TCS s t -> UEnv t,
  update :: TCS s t -> UEnv t -> TCS s t
}

env1, env2 :: Field s t
env1 = Field tcsEnv1 (\tcs e -> tcs { tcsEnv1 = e })
env2 = Field tcsEnv2 (\tcs e -> tcs { tcsEnv2 = e })

runUT  :: forall s a m. MonadError String m =>
          (forall t. UT s t a) -> S.Set TyVarR -> m a
runUT m set =
  runST $ do
    seen   <- newTransSTRef M.empty
    supply <- newSTRef [ f | f <- tvalphabet
                       , f Qu `S.notMember` set
                       , f Qa `S.notMember` set ]
    CMR.runReaderT m TCS {
      tcsSeen   = seen,
      tcsSupply = supply,
      tcsLevel  = 1,
      tcsEnv1   = M.empty,
      tcsEnv2   = M.empty
    }

getVar :: TyVarR -> Field s t -> UT s t (Maybe (UVar t))
getVar tv field = CMR.asks (M.lookup tv . get field)

-- | To add some unification variables to the scope, run the body,
--   and return a map containing their lower and upper bounds.
--   Unification variables are assumed to be fresh with respect to
--   existing variables.  In particular, the initial set of unification
--   variables precedes any other bindings, and all subsequent foralls
--   are renamed using fresh type variables.
withUVars :: [TyVarR] -> Field s t -> UT s t a -> UT s t (a, [Type])
withUVars tvs field body = do
  level <- CMR.asks tcsLevel
  refs  <- lift $ sequence
    [ do ref <- newTransSTRef (tyBot, tyTop (tvqual tv))
         return (tv, (level, ref))
    | tv <- tvs ]
  res   <- CMR.local
    (\st -> update field st (M.fromList refs `M.union` get field st))
    body
  typs  <- sequence
    [ do
        (lower, upper) <- lift $ readSTRef ref
        if lower <: upper
          then return $
            -- This is a heuristic -- we prefer to return something
            -- with information, meaning not top or bottom, but if
            -- the choice is between top and bottom, we go with bottom
            if isBotType lower
              then if upper == tyUn || upper == tyAf then lower else upper
              else lower
          else throwError $
            "Unification cannot solve:\n" ++
            show lower ++ " <: " ++ show upper
    | (_, (_, ref)) <- refs ]
  return (res, typs)

-- | Bump up the quantification nesting level
incU :: UT s t a -> UT s t a
incU  = CMR.local (\st -> st { tcsLevel = tcsLevel st + 1 })

-- | Try to assert an upper bound on a unification variable.
upperBoundUVar :: STRef t (Type, Type) -> Type -> UT s t ()
upperBoundUVar ref t = do
  (lower, upper) <- lift $ readSTRef ref
  unless (upper <: t) $ do
    upper' <- t /\? upper
    lift $ writeSTRef ref (lower, upper')


-- | Try to assert a lower bound on a unification variable.
lowerBoundUVar :: STRef t (Type, Type) -> Type -> UT s t ()
lowerBoundUVar ref t = do
  (lower, upper) <- lift $ readSTRef ref
  unless (t <: lower) $ do
    lower' <- t \/? lower
    lift $ writeSTRef ref (lower', upper)

-- | Get maps of the left and right uvars
getUVars :: UT s t (TyVarR -> Maybe (Int, STRef t (Type, Type)),
                    TyVarR -> Maybe (Int, STRef t (Type, Type)))
getUVars = do
  st <- CMR.ask
  return (flip M.lookup (tcsEnv1 st), flip M.lookup (tcsEnv2 st))

-- | Check if two types have been seen before.  If so, return the
--   previously stored answer.  If not, temporarily store the given
--   answer, then run a block, and finally replace the stored answer
--   with the result of the block.
chkU :: Type -> Type -> s -> UT s t s -> UT s t s
chkU t1 t2 s body = do
  st   <- CMR.ask
  let key = (AType t2, AType t1)
      ref = tcsSeen st
  seen <- lift $ readSTRef ref
  case M.lookup key seen of
    Just s' -> return s'
    Nothing -> do
      lift $ modifySTRef ref (M.insert key s)
      res <- body
      lift $ modifySTRef ref (M.insert key res)
      return res

-- | Flip the left and right sides of the relation in the given block.
flipU :: UT s t a -> UT s t a
flipU body = CMR.local flipSt body where
  flipSt (TCS seen level supply e1 e2) =
    TCS seen level supply e2 e1

-- | Get a fresh type variable from the supply.
freshU :: QLit -> UT s t TyVarR
freshU qlit = do
  ref <- CMR.ask >>! tcsSupply
  f:supply <- lift $ readSTRef ref
  lift $ writeSTRef ref supply
  return (f qlit)

-- | Print a debug message
-- pM :: Show b => b -> UT s t ()
-- pM = lift . unsafeIOToST . print
-- pM = const $ return ()

subtype :: MonadError String m =>
           Int -> [TyVarR] -> Type -> [TyVarR] -> Type ->
           m ([Type], [Type])
subtype limit uvars1 t1i uvars2 t2i =
  runUT start (S.fromList uvars1 `S.union`
               S.fromList uvars2 `S.union`
               alltv (t1i, t2i))
  where
    start :: UT () t ([Type], [Type])
    start = liftM (first snd) $
              withUVars uvars2 env2 $
                withUVars uvars1 env1 $
                  cmp t1i t2i
    --
    cmp :: Type -> Type -> UT () t ()
    cmp t u = chkU t u () $ case (t, u) of
      -- Handle top
      (_ , TyApp tcu _ _)
        | tcu == tcUn && qualConst t <: Qu
        -> return ()
      (_ , TyApp tcu _ _)
        | tcu == tcAf
        -> return ()
      -- Handle bottom
      (TyApp tct _ _, _)
        | tct == tcBot
        -> return ()
      -- Variables
      (TyVar vt, TyVar vu) -> do
        mt' <- getVar vt env1
        mu' <- getVar vu env2
        case (mt', mu') of
          (Just (_, t'), Nothing) -> upperBoundUVar t' u
          (Nothing, Just (_, u')) -> lowerBoundUVar u' t
          (Just (lt, t'), Just (lu, u'))
            | lt > lu             -> upperBoundUVar t' u
            | lt < lu             -> lowerBoundUVar u' t
          _                       -> unless (vt == vu) $ giveUp t u
      (TyVar vt, _) -> do
        mt' <- getVar vt env1
        case mt' of
          Just (_, t') -> upperBoundUVar t' u
          Nothing      -> giveUp t u
      (_, TyVar vu) -> do
        mu' <- getVar vu env2
        case mu' of
          Just (_, u') -> lowerBoundUVar u' t
          Nothing      -> giveUp t u
      -- Type applications
      (TyApp tct ts _, TyApp tcu us _)
        | tct == tcu,
          isHeadNormalType t, isHeadNormalType u ->
        cmpList (tcArity tct) ts us
      (TyApp tct ts _, TyApp tcu us _)
        | tct == tcu ->
        cmpList (tcArity tct) ts us `catchError` \_ -> do
          t' <- hn t
          u' <- hn u
          cmp t' u'
      (TyApp _ _ _, _)
        | not (isHeadNormalType t)
        -> (`cmp` u) =<< hn t
      (_, TyApp _ _ _)
        | not (isHeadNormalType u)
        -> (t `cmp`) =<< hn u
      -- Arrows
      (TyFun qt t1 t2, TyFun qu u1 u2) -> do
        subkind qt qu $ giveUp t u
        revCmp t1 u1
        cmp t2 u2
      -- Quantifiers
      (TyQu Forall tvt t1, _) -> do
        tv' <- freshU (tvqual tvt)
        incU $
          withUVars [tv'] env1 $
            cmp (tysubst tvt (TyVar tv') t1) u
        return ()
      (_, TyQu Exists tvu u1) -> do
        tv' <- freshU (tvqual tvu)
        incU $
          withUVars [tv'] env2 $
            cmp t (tysubst tvu (TyVar tv') u1)
        return ()
      (_, TyQu Forall tvu u1) -> do
        tv' <- freshU (tvqual tvu)
        cmp t (tysubst tvu (TyVar tv') u1)
      (TyQu Exists tvt t1, _) -> do
        tv' <- freshU (tvqual tvt)
        cmp (tysubst tvt (TyVar tv') t1) u
      -- Recursion
      (TyMu tvt t1, _) -> cmp (tysubst tvt t t1) u
      (_, TyMu tvu u1) -> cmp t (tysubst tvu u u1)
      -- Failure
      _ -> giveUp t u
    --
    giveUp t u = 
      throwError $
        "Got type `" ++ show t ++ "' where type `" ++
        show u ++ "' expected"
    --
    revCmp u t = flipU (cmp t u)
    --
    hn t = headNormalizeTypeM limit t
    --
    cmpList arity ts us =
      sequence_
        [ case var of
            1  -> cmp tj uj
            -1 -> revCmp tj uj
            _  -> do cmp tj uj; revCmp tj uj
        | var      <- arity
        | tj       <- ts
        | uj       <- us ]
    --
    -- XXX This is woefully insufficient
    subkind qd1 qd2 orElse =
      if qd1 <: qd2 then return () else do
        (m1, m2) <- getUVars
        case (view $ qRepresent qd1, view $ qRepresent qd2) of
          (QeVar tv1, QeVar tv2)
            | Just (_, ref) <- m1 tv1, Nothing <- m2 tv2
            -> upperBoundUVar ref (TyVar tv2)
            | Nothing <- m1 tv1, Just (_, ref) <- m2 tv2
            -> lowerBoundUVar ref (TyVar tv1)
          (QeVar tv1, QeLit qlit)
            | Just (_, ref) <- m1 tv1
            -> upperBoundUVar ref (tyTop qlit)
          (QeLit qlit, QeVar tv2)
            | Just (_, ref) <- m2 tv2
            -> lowerBoundUVar ref (tyTop qlit)
          _ -> orElse

jointype :: MonadError String m => Int -> Bool -> Type -> Type -> m Type
jointype limit b t1i t2i =
  liftM clean $ runUT (cmp (b, True) t1i t2i) (alltv (t1i, t2i))
  where
  cmp, revCmp :: (Bool, Bool) -> Type -> Type -> UT Type t Type
  cmp m t u = do
    let (direction, _) = m
    tv   <- freshU (qualConst t \/ qualConst u)
    catchTop m t u $
      chkU t u (TyVar tv) $
        TyMu tv `liftM`
          case (t, u) of
      -- Handle top and bottom
      _ | Just t' <- points direction t u -> return t'
        | Just t' <- points direction u t -> return t'
      -- Type applications
      (TyApp tct ts _, TyApp tcu us _)
        | tct == tcu,
          isHeadNormalType t, isHeadNormalType u ->
        tyApp tct `liftM`
          cmpList (tcArity tct) (direction, True) ts us
      (TyApp tct ts _, TyApp tcu us _)
        | tct == tcu
        -> liftM (tyApp tct)
                 (cmpList (tcArity tct) (direction, False) ts us)
             `catchError` \_ -> do
               t' <- hn t
               u' <- hn u
               cmp m t' u'
      (TyApp _ _ _, _)
        | not (isHeadNormalType t) -> do
        t' <- hn t
        cmp m t' u
      (_, TyApp _ _ _)
        | not (isHeadNormalType u) -> do
        u' <- hn u
        cmp m t u'
      -- Variables
      (TyVar vt, TyVar ut)
        | vt == ut ->
        return t
      -- Arrows
      (TyFun qt t1 t2, TyFun qu u1 u2) -> do
        q'  <- ifMJ direction qt qu
        t1' <- revCmp m t1 u1
        t2' <- cmp m t2 u2
        return (TyFun q' t1' t2')
      -- Quantifiers
      (TyQu qt tvt t1, TyQu qu tvu u1)
        | qt == qu -> do
        q'  <- ifMJ direction (tvqual tvt) (tvqual tvu)
        tv' <- freshU q'
        liftM (TyQu qt tv') $
          cmp m (tysubst tvt (TyVar tv') t1)
                (tysubst tvu (TyVar tv') u1)
      -- Recursion
      (TyMu tvt t1, _) ->
        cmp m (tysubst tvt t t1) u
      (_, TyMu tvu u1) ->
        cmp m t (tysubst tvu u u1)
      -- Failure
      _ ->
        throwError $
          "Could not " ++ (if direction then "join" else "meet") ++
          " types `" ++ show t ++
          "' and `" ++ show u ++ "'"
  --
  hn t = headNormalizeTypeM limit t
  --
  cmpList arity m ts us =
    sequence
      [ case var of
          1  -> cmp m tj uj
          -1 -> revCmp m tj uj
          _  -> if tj == uj
                  then return tj
                  else throwError $
                    "Could not unify types `" ++ show tj ++
                    "' and `" ++ show uj ++ "'"
      | var      <- arity
      | tj       <- ts
      | uj       <- us ]
  --
  points True  t u@(TyApp tc _ _)
    | tc == tcAf                    = Just u
    | tc == tcUn, qualConst t <: Qu = Just u
    | tc == tcBot                   = Just t
  points False t u@(TyApp tc _ _)
    | tc == tcAf                    = Just t
    | tc == tcUn, qualConst t <: Qu = Just t
    | tc == tcBot                   = Just u
  points _     _   _                = Nothing
  --
  revCmp (direction, lossy) t u = cmp (not direction, lossy) t u
  --
  catchTop (True, True)  t u body = body
    `catchError` \_ -> return (tyTop (qualConst t \/ qualConst u))
  {-
  catchTop (False, True) _ _ body = body
    `catchError` \_ -> return tyBot
  -}
  catchTop _             _ _ body = body
  --
  clean :: Type -> Type
  clean (TyApp tc ts _)  = tyApp tc (map clean ts)
  clean (TyVar a)        = TyVar a
  clean (TyFun q t1 t2)  = TyFun q (clean t1) (clean t2)
  clean (TyQu u a t)     = TyQu u a (clean t)
  clean (TyMu a t)
    | a `S.member` ftv t = TyMu a (clean t)
    | otherwise          = clean t

-- | Helper to force 'Either' to the right type
runEither :: (String -> r) -> (a -> r) -> Either String a -> r
runEither  = either

-- | The Type partial order
instance Eq Type where
  t1 == t2 = t1 <: t2 && t2 <: t1

instance PO Type where
  t1 <: t2     = runEither (const False) (const True)
                           (subtype 100 [] t1 [] t2)
  ifMJ b t1 t2 = runEither (throwError . strMsg) return
                           (jointype 100 b t1 t2)

subtypeTests, joinTests, uvarsTests :: T.Test

subtypeTests = T.test
  [ tyUnit  <:! tyUnit
  , tyUnit !<:  tyInt
  , tyInt   <:! tyInt
  , tyInt  .->. tyInt   <:! tyInt .->. tyInt
  , tyInt  .->. tyInt   <:! tyInt .-*. tyInt
  , tyInt  .-*. tyInt   <:! tyInt .-*. tyInt
  , tyInt  .-*. tyInt  !<:  tyInt .->. tyInt
  , tyUnit .->. tyInt  !<:  tyInt .->. tyInt
  , (tyInt .-*. tyInt) .->. tyInt .->. tyInt <:!
    (tyInt .->. tyInt) .->. tyInt .-*. tyInt 
  , tyInt .->. tyInt  <:! tyUn
  , tyInt .->. tyInt  <:! tyAf
  , tyInt .-*. tyInt !<:  tyUn
  , tyInt .-*. tyInt  <:! tyAf
  , tyUn  <:! tyAf
  , tyAf !<:  tyUn
  , tyRecv tyInt  <:! tyRecv tyInt
  , tyRecv tyInt !<:  tyRecv tyUnit
  , tyRecv tyInt !<:  tySend tyInt
  , tyRecv (tyInt .-*. tyInt)  <:! tyRecv (tyInt .->. tyInt)
  , tyRecv (tyInt .->. tyInt) !<:  tyRecv (tyInt .-*. tyInt)
  , tySend (tyInt .-*. tyInt) !<:  tySend (tyInt .->. tyInt)
  , tySend (tyInt .->. tyInt)  <:! tySend (tyInt .-*. tyInt)
  , tyIdent tyInt  <:! tyIdent tyInt
  , tyIdent tyInt !<:  tyIdent tyUnit
  , tyInt          <:! tyIdent tyInt
  , tyIdent tyInt  <:! tyInt
  , tyInt         !<:  tyIdent tyUnit
  , tyIdent tyInt !<:  tyUnit
  , tyConst tyInt  <:! tyConst tyInt
  , tyConst tyInt  <:! tyConst tyUnit
  , tyConst tyInt  <:! tyUnit
  , tyUnit         <:! tyConst tyInt
  , tyUnit .->. tyInt <:! tyIdent (tyConst (tySend tyInt) .-*. tyInt)
  , tyInt .->. tyInt !<:  tyIdent (tyConst (tySend tyInt) .-*. tyInt)
  , tyDual (tyRecv tyInt .:. tySend tyUnit .:. tyUnit) <:!
    tyDual (tyRecv tyInt .:. tySend tyUnit .:. tyUnit)
  , tyDual (tyRecv tyInt .:. tySend tyUnit .:. tyUnit) <:!
    tySend tyInt .:. tyDual (tySend tyUnit .:. tyUnit) 
  , tyDual (tyRecv tyInt .:. tySend tyUnit .:. tyUnit) <:!
    tySend tyInt .:. tyRecv tyUnit .:. tyUnit 
  , tyBot  <:! tyInt .->. tyInt
  , tyInt .->. tyInt !<:  tyBot
  , TyVar a  <:! TyVar a
  , TyVar a !<:  TyVar b
  , tyAll a (tyInt .->. TyVar a)  <:! tyAll b (tyInt .->. TyVar b)
  , tyAll a (tyInt .->. TyVar a)  <:! tyAll b (tyInt .->. TyVar a)
  , tyAll c (TyVar c .->. tyInt)  <:! tyAll a (TyVar a .-*. tyInt)
  , tyAll a (TyVar a .->. tyInt) !<:  tyAll c (TyVar c .-*. tyInt)
  , tyAll a (tyAll b (TyVar a .*. TyVar b))  <:!
    tyAll b (tyAll a (TyVar b .*. TyVar a))
  , tyAll a (tyAll b (TyVar a .*. TyVar b))  <:!
    tyAll b (tyAll a (TyVar a .*. TyVar b))
  , tyAll a (tyAll a (TyVar a .*. TyVar b)) !<:
    tyAll b (tyAll a (TyVar a .*. TyVar b))
  , tyAll a (tyAll a (TyVar a .*. TyVar b))  <:!
    tyAll a (tyAll a (TyVar a .*. TyVar b))
  , TyMu a (tyInt .->. TyVar a)  <:!
    TyMu b (tyInt .->. TyVar b)
  , TyMu a (tyInt .->. TyVar a)  <:!
    TyMu b (tyInt .->. tyInt .->. TyVar b)
  , TyMu a (tyInt .->. TyVar a)  <:!
    TyMu b (tyInt .->. tyInt .-*. TyVar b)
  , TyMu a (tyInt .->. TyVar a) !<:
    TyMu b (tyInt .->. tyUnit .-*. TyVar b)
  , TyMu a (TyVar a .*. tyInt .*. tyInt) <:!
    TyMu a (TyVar a .*. tyInt .*. tyInt) .*. tyInt 
  , TyMu a (TyVar a .*. tyInt .*. tyUnit) <:!
    TyMu a (TyVar a .*. tyUnit .*. tyInt) .*. tyUnit 
  , tyAll c (TyMu a (TyVar a .*. tyInt .*. TyVar c))  <:!
    tyAll d (TyMu a (TyVar a .*. TyVar d .*. tyInt) .*. TyVar d)
  , tyAll c (TyMu a (TyVar a .*. tyInt .*. TyVar c)) !<:
    tyAll d (TyMu a (TyVar d .*. TyVar a .*. tyInt) .*. TyVar d)
  , TyMu a (tyAll c ((tyInt .-*. TyVar c) .->. TyVar a)) !<:
    TyMu b (tyAll d ((tyInt .->. TyVar d) .->. TyVar c))
  , TyMu a (tyAll c (tyInt .-*. TyVar c) .->. TyVar a)  <:!
    TyMu b (tyAll d (tyInt .->. TyVar d) .->. TyVar b)
  , TyMu a (tyAll c (TyVar a .-*. TyVar c) .->. TyVar a) <:!
    TyMu b (tyAll d (TyVar b .->. TyVar d) .->. TyVar b)
  , tyAll a (TyVar a .*. tyInt) .->. TyVar a  <:!
    tyAll b (TyVar b .*. tyInt) .->. TyVar a 
  , tyAll a (TyVar a .*. tyInt) .->. TyVar a !<:
    tyAll b (TyVar b .*. tyInt) .->. TyVar b 
  -- Universal instantiation tests
  , tyAll a (TyVar a .->. TyVar a)  <:! tyInt .->. tyInt
  , tyAll a (TyVar a .->. TyVar a) !<:  tyInt .->. tyUnit
  , tyInt .->. tyInt !<: tyAll a (TyVar a .->. TyVar a)
  , tyAll a (TyVar a .->. tyInt)  <:! tyInt .->. tyInt
  , tyAll a (tyInt   .->. tyInt)  <:! tyInt .->. tyInt
  , tyInt .->. tyAll a (TyVar a .->. TyVar a) <:!
    tyInt .->.          tyInt   .->. tyInt
  , TyMu a (TyVar a .*. (tyAll a (TyVar a .->. TyVar a)))  <:!
    TyMu a (TyVar a .*.          (tyInt   .->. tyInt))
  , TyMu a (TyVar a .*. (tyAll a (tyInt   .->. TyVar a)))  <:!
    TyMu a (TyVar a .*.          (tyInt   .->. tyInt))
  , TyMu b (TyVar b .*. (tyAll a (TyVar a .->. TyVar a)))  <:!
    TyMu a (TyVar a .*.          (tyInt   .->. tyInt))
  , TyMu b (TyVar b .*. (tyAll a (tyInt   .->. TyVar a)))  <:!
    TyMu a (TyVar a .*.          (tyInt   .->. tyInt))
  , TyMu a (tyAll b (TyVar b .->. TyVar a))  <:!
    TyMu a          (tyInt   .->. TyVar a)
  , tyAll a (TyVar a .*. tyInt)    <:! TyMu a (TyVar a .*. tyInt)
  , tyAll a (TyVar a .*. TyVar a) !<: TyMu a (TyVar a .*. tyInt)
  , tyAll a (TyMu b (TyVar a .->. TyVar b))  <:!
    TyMu b (tyInt .->. TyVar b)
  , tyAll a (TyMu a (tyInt .->. TyVar a))   !<:
    TyMu b (tyInt .->. tyInt)
  , tyAll a (tyInt .->. TyVar a) .->. tyInt !<:
    (tyInt .->. tyInt) .->. tyInt
  , (tyInt .->. tyInt) .->. tyInt            <:!
    tyAll a (tyInt .->. TyVar a) .->. tyInt
  , tyAll a (tyInt .->. TyVar a) !<: tyInt .->. tyInt .-*. tyInt
  -- This is now true, but should it be?:
  , TyMu a (tyAll c (tyInt .->. tyAll d (TyVar c .->. TyVar a))) <:!
    tyAll c (tyInt .->.
             TyMu a (tyAll d (TyVar c .->.
                              tyAll c (tyInt .->. TyVar a))))
  -- This is now true, but should it be?:
  , tyAll c (tyInt .->.
             TyMu a (tyAll d (TyVar c .->.
                              tyAll c (tyInt .->. TyVar a)))) <:!
    TyMu a (tyAll c (tyInt .->. tyAll d (TyVar c .->. TyVar a)))
  , tyInt <:! tyEx a (TyVar a)
  , tyInt <:! tyEx a tyInt
  , tyInt .*. tyInt <:! tyEx a (TyVar a .*. tyInt)
  , tyInt .*. tyInt <:! tyEx a (tyInt .*. TyVar a)
  , tyInt .*. tyInt <:! tyEx a (TyVar a .*. TyVar a)
  , tyInt .*. tyInt <:! tyEx a (tyEx b (TyVar a .*. TyVar a))
  , tyInt .*. tyInt <:! tyEx a (tyEx b (TyVar b .*. TyVar a))
  , tyUn .->. tyUn !<:  TyVar a .->. TyVar a
  -- These are potentially sketchy, but useful:
  , tyInt  <:! tyAll a tyInt
  , tyInt !<:  tyAll a (TyVar a)
  , tyEx a tyInt      <:! tyInt
  , tyEx a (TyVar a) !<: tyInt
  , tyEx a (TyVar a) !<: TyVar a
  ]
  where
  t1  <:! t2 = T.assertBool (show t1 ++ " <: " ++ show t2) (t1 <: t2)
  t1 !<:  t2 = T.assertBool (show t1 ++ " /<: " ++ show t2) (t1 /<: t2)
  infix 4 <:!, !<:
  a = tvUn "a"; b = tvUn "b"; c = tvAf "c"; d = tvAf "d"

joinTests = T.test
  [ tyUnit  \/! tyUnit ==! tyUnit
  , tyUnit  /\! tyUnit ==! tyUnit
  , tyInt   /\! tyInt  ==! tyInt
  , tyUnit  \/! tyInt  ==! tyUn
  , tyUnit !/\  tyInt
  , tyInt .->. tyInt  \/! tyInt .->. tyInt  ==! tyInt .->. tyInt
  , tyInt .->. tyInt  \/! tyInt .-*. tyInt  ==! tyInt .-*. tyInt
  , tyInt .-*. tyInt  \/! tyInt .-*. tyInt  ==! tyInt .-*. tyInt
  , tyInt .-*. tyInt  \/! tyInt .->. tyInt  ==! tyInt .-*. tyInt
  , tyInt .->. tyInt  /\! tyInt .->. tyInt  ==! tyInt .->. tyInt
  , tyInt .->. tyInt  /\! tyInt .-*. tyInt  ==! tyInt .->. tyInt
  , tyInt .-*. tyInt  /\! tyInt .-*. tyInt  ==! tyInt .-*. tyInt
  , tyInt .-*. tyInt  /\! tyInt .->. tyInt  ==! tyInt .->. tyInt
  , tyInt .->. tyInt  \/! tyInt .->. tyUnit ==! tyInt .->. tyUn
  , tyInt .->. tyInt  \/! tyUnit .->. tyInt ==! tyUn
  , tyInt .-*. tyInt  \/! tyUnit .->. tyInt ==! tyAf
  , tyInt .->. tyInt !/\  tyInt .->. tyUnit
  , tyInt .->. tyInt  /\! tyUnit .->. tyInt ==! tyUn .->. tyInt
  , tyInt .-*. tyInt  /\! tyUnit .->. tyInt ==! tyUn .->. tyInt
  , (tyInt .-*. tyInt) .-*. tyInt /\! tyUnit .->. tyInt
      ==! tyAf .->. tyInt
  , tyInt .->. tyInt  \/! tyUn ==! tyUn
  , tyInt .->. tyInt  \/! tyAf ==! tyAf
  , tyInt .-*. tyInt  \/! tyUn ==! tyAf
  , tyInt .-*. tyInt  \/! tyAf ==! tyAf
  , tyInt .->. tyInt  /\! tyUn ==! tyInt .->. tyInt
  , tyInt .->. tyInt  /\! tyAf ==! tyInt .->. tyInt
  , tyInt .-*. tyInt !/\  tyUn -- could do better
  , tyInt .-*. tyInt  /\! tyAf ==! tyInt .-*. tyInt
  , tyRecv tyInt \/! tyRecv tyInt  ==! tyRecv tyInt
  , tySend tyInt \/! tySend tyUnit ==! tySend tyUn
  , tyRecv tyInt \/! tySend tyInt  ==! tyUn
  , tyRecv (tyInt .-*. tyInt) \/!
    tyRecv (tyInt .->. tyInt) ==!
    tyRecv (tyInt .->. tyInt)
  , tyRecv (tyInt .->. tyInt) \/!
    tyRecv (tyInt .-*. tyInt) ==!
    tyRecv (tyInt .->. tyInt)
  , tySend (tyInt .-*. tyInt) \/!
    tySend (tyInt .->. tyInt) ==!
    tySend (tyInt .-*. tyInt)
  , tySend (tyInt .->. tyInt) \/!
    tySend (tyInt .-*. tyInt) ==!
    tySend (tyInt .-*. tyInt)
  , tyRecv (tyInt .-*. tyInt) /\!
    tyRecv (tyInt .->. tyInt) ==!
    tyRecv (tyInt .-*. tyInt)
  , tyRecv (tyInt .->. tyInt) /\!
    tyRecv (tyInt .-*. tyInt) ==!
    tyRecv (tyInt .-*. tyInt)
  , tySend (tyInt .-*. tyInt) /\!
    tySend (tyInt .->. tyInt) ==!
    tySend (tyInt .->. tyInt)
  , tySend (tyInt .->. tyInt) /\!
    tySend (tyInt .-*. tyInt) ==!
    tySend (tyInt .->. tyInt)
  , tyIdent tyInt  \/! tyIdent tyInt  ==! tyIdent tyInt
  , tyIdent tyInt  \/! tyIdent tyUnit ==! tyUn
  , tyInt          \/! tyIdent tyInt  ==! tyInt
  , tyInt          \/! tyIdent tyUnit ==! tyUn
  , tyIdent tyInt  /\! tyIdent tyInt  ==! tyIdent tyInt
  , tyIdent tyInt !/\  tyIdent tyUnit
  , tyInt          /\! tyIdent tyInt  ==! tyInt
  , tyInt         !/\  tyIdent tyUnit
  , tyIdent (tyIdent tyInt) \/! tyIdent tyInt            ==! tyIdent tyInt
  , tyIdent (tyConst tyInt) \/! tyIdent (tyConst tyUnit) ==! tyIdent tyUnit
  , tyConst tyInt  \/! tyConst tyInt   ==! tyConst tyInt
  , tyConst tyInt  \/! tyConst tyUnit  ==! tyUnit
  , tyConst tyInt  /\! tyConst tyInt   ==! tyConst tyInt
  , tyConst tyInt  /\! tyConst tyUnit  ==! tyUnit
  , tyUnit .->. tyInt  \/! tyIdent (tyConst (tySend tyInt) .-*. tyInt)
      ==! tyUnit .-*. tyInt
  , tyInt .->. tyInt   \/! tyIdent (tyConst (tySend tyInt) .-*. tyInt)
      ==! tyAf
  , tyUnit .->. tyInt  /\! tyIdent (tyConst (tySend tyInt) .-*. tyInt)
      ==! tyUnit .->. tyInt
  , tyInt .->. tyInt   /\! tyIdent (tyConst (tySend tyInt) .-*. tyInt)
      ==! tyUn .->. tyInt
  , tyDual (tyRecv tyInt .:. tySend tyUnit .:. tyUnit) \/!
    tyDual (tyRecv tyInt .:. tySend tyUnit .:. tyUnit) ==!
    tyDual (tyRecv tyInt .:. tySend tyUnit .:. tyUnit)
  , tyDual (tyRecv tyInt .:. tySend tyUnit .:. tyUnit) \/!
    tySend tyInt .:. tyDual (tySend tyUnit .:. tyUnit)  ==!
    tySend tyInt .:. tyDual (tySend tyUnit .:. tyUnit) 
  , tyDual (tyRecv tyInt .:. tySend tyUnit .:. tyUnit) \/!
    tySend tyInt .:. tyRecv tyUnit .:. tyUnit  ==!
    tySend tyInt .:. tyRecv tyUnit .:. tyUnit 
  , tyDual (tyRecv tyInt .:. tySend tyUnit .:. tyUnit) /\!
    tyDual (tyRecv tyInt .:. tySend tyUnit .:. tyUnit) ==!
    tyDual (tyRecv tyInt .:. tySend tyUnit .:. tyUnit)
  , tyDual (tyRecv tyInt .:. tySend tyUnit .:. tyUnit) /\!
    tySend tyInt .:. tyDual (tySend tyUnit .:. tyUnit)  ==!
    tySend tyInt .:. tyDual (tySend tyUnit .:. tyUnit) 
  , tyDual (tyRecv tyInt .:. tySend tyUnit .:. tyUnit) /\!
    tySend tyInt .:. tyRecv tyUnit .:. tyUnit  ==!
    tySend tyInt .:. tyRecv tyUnit .:. tyUnit 
  , tyBot  \/! tyInt .->. tyInt ==! tyInt .->. tyInt
  , tyInt .->. tyInt  /\! tyBot ==! tyAll b (TyVar b)
  , TyVar a  \/! TyVar a ==! TyVar a
  , TyVar a  \/! TyVar b ==! tyUn
  , TyVar a  \/! TyVar c ==! tyAf
  , TyVar a  /\! TyVar a ==! TyVar a
  , TyVar a !/\  TyVar b
  , TyVar a !/\  TyVar c
  , tyAll a (tyInt .->. TyVar a)  \/!  tyAll b (tyInt .->. TyVar b)
      ==! tyAll a (tyInt .->. TyVar a)
  , tyAll a (tyInt .->. TyVar a)  \/!  tyAll b (tyInt .->. TyVar a)
      ==! tyAll a (tyInt .->. tyUn)
  , tyAll c (TyVar c .->. tyInt)  \/! tyAll a (TyVar a .-*. tyInt)
      ==! tyAll d (TyVar d .-*. tyInt)
  , tyAll a (tyInt .->. TyVar a)  /\!  tyAll b (tyInt .->. TyVar b)
      ==! tyAll a (tyInt .->. TyVar a)
  , tyAll a (tyInt .->. TyVar a) !/\   tyAll b (tyInt .->. TyVar a)
  , tyAll c (TyVar c .->. tyInt)  /\!
    tyAll a (TyVar a .-*. tyInt)  ==!
    tyAll b (TyVar b .->. tyInt)
  , tyAll a (tyAll b (TyVar a .*. TyVar b))  \/!
    tyAll b (tyAll a (TyVar b .*. TyVar a))  ==!
    tyAll b (tyAll a (TyVar b .*. TyVar a))
  , tyAll a (tyAll b (TyVar a .*. TyVar b))  \/!
    tyAll b (tyAll a (TyVar a .*. TyVar b))  ==!
    tyAll b (tyAll a (tyUn .*. tyUn))
  , tyAll c (tyAll c (TyVar c .*. TyVar d))  \/!
    tyAll d (tyAll c (TyVar c .*. TyVar d))  ==!
    tyAll d (tyAll d (TyVar d .*. tyAf))
  , tyAll a (tyAll a (TyVar a .*. TyVar b))  \/!
    tyAll a (tyAll a (TyVar a .*. TyVar b))  ==!
    tyAll a (tyAll a (TyVar a .*. TyVar b))
  , tyAll a (tyAll b (TyVar a .*. TyVar b))  /\!
    tyAll b (tyAll a (TyVar b .*. TyVar a))  ==!
    tyAll b (tyAll a (TyVar b .*. TyVar a))
  , tyAll a (tyAll b (TyVar a .*. TyVar b)) !/\
    tyAll b (tyAll a (TyVar a .*. TyVar b))
  , tyAll c (tyAll c (TyVar c .*. TyVar d)) !/\
    tyAll d (tyAll c (TyVar c .*. TyVar d))
  , tyAll a (tyAll a (TyVar a .*. TyVar b))  /\!
    tyAll a (tyAll a (TyVar a .*. TyVar b))  ==!
    tyAll a (tyAll a (TyVar a .*. TyVar b))
  , TyMu a (tyInt .->. TyVar a)  \/!
    TyMu b (tyInt .->. TyVar b)  ==!
    TyMu b (tyInt .->. TyVar b)
  , TyMu a (tyInt .->. TyVar a)  /\!
    TyMu b (tyInt .->. TyVar b)  ==!
    TyMu b (tyInt .->. TyVar b)
  , TyMu a (tyInt .->. TyVar a)            \/!
    TyMu b (tyInt .->. tyInt .->. TyVar b) ==!
    TyMu a (tyInt .->. TyVar a)
  , TyMu a (tyInt .->. TyVar a)            /\!
    TyMu b (tyInt .->. tyInt .->. TyVar b) ==!
    TyMu a (tyInt .->. TyVar a)
  , TyMu a (tyInt .->. TyVar a)            \/!
    TyMu b (tyInt .->. tyInt .-*. TyVar b) ==!
    TyMu b (tyInt .->. tyInt .-*. TyVar b)
  , TyMu a (tyInt .->. TyVar a)            /\!
    TyMu b (tyInt .->. tyInt .-*. TyVar b) ==!
    TyMu b (tyInt .->. TyVar b)
  , TyMu a (tyInt .->. TyVar a)             \/!
    TyMu b (tyInt .->. tyUnit .-*. TyVar b) ==!
    tyInt .->. tyAf
  , TyMu a (tyInt .->. TyVar a)             /\!
    TyMu b (tyInt .->. tyUnit .-*. TyVar b) ==!
    TyMu a (tyInt .->. tyUn .->. TyVar a)
  , TyMu a (TyVar a .*. tyInt .*. tyInt)           \/!
    TyMu a (TyVar a .*. tyInt .*. tyInt) .*. tyInt ==!
    TyMu a (TyVar a .*. tyInt)
  , TyMu a (TyVar a .*. tyInt .*. tyInt)           /\!
    TyMu a (TyVar a .*. tyInt .*. tyInt) .*. tyInt ==!
    TyMu a (TyVar a .*. tyInt)
  , TyMu a (TyVar a .*. tyInt .*. tyUnit)            \/!
    TyMu a (TyVar a .*. tyUnit .*. tyInt) .*. tyUnit ==!
    TyMu b (TyVar b .*. tyInt .*. tyUnit)
  , TyMu a (TyVar a .*. tyInt .*. tyUnit)            /\!
    TyMu a (TyVar a .*. tyUnit .*. tyInt) .*. tyUnit ==!
    TyMu b (TyVar b .*. tyInt .*. tyUnit)
  , tyAll c (TyMu a (TyVar a .*. tyInt .*. TyVar c))             \/!
    tyAll d (TyMu a (TyVar a .*. TyVar d .*. tyInt) .*. TyVar d) ==!
    tyAll c (TyMu b (TyVar b .*. tyInt .*. TyVar c))
  , tyAll c (TyMu a (TyVar a .*. tyInt .*. TyVar c))             /\!
    tyAll d (TyMu a (TyVar a .*. TyVar d .*. tyInt) .*. TyVar d) ==!
    tyAll c (TyMu b (TyVar b .*. tyInt .*. TyVar c))
  , tyAll c (TyMu a (TyVar a .*. tyInt .*. TyVar c))             \/!
    tyAll d (TyMu a (TyVar d .*. TyVar a .*. tyInt) .*. TyVar d) ==!
    tyAll c (tyAf .*. tyAf .*. tyInt .*. TyVar c)
  , tyAll c (TyMu a (TyVar a .*. tyInt .*. TyVar c))            !/\
    tyAll d (TyMu a (TyVar d .*. TyVar a .*. tyInt) .*. TyVar d)
  , TyMu a (tyAll c (tyInt .-*. TyVar c) .->. TyVar a)           \/!
    TyMu b (tyAll d (tyInt .->. TyVar d) .->. TyVar c)           ==!
    tyAll d (tyInt .->. TyVar d) .->. tyAf
  , TyMu a (tyAll c (tyInt .-*. TyVar c) .->. TyVar a)          !/\
    TyMu b (tyAll d (tyInt .->. TyVar d) .->. TyVar c)
  , TyMu a (tyAll c (tyInt .-*. TyVar c) .->. TyVar a)           \/!
    TyMu b (tyAll d (tyInt .->. TyVar d) .->. TyVar b)           ==!
    TyMu b (tyAll c (tyInt .->. TyVar c) .->. TyVar b)
  , TyMu a (tyAll c (tyInt .-*. TyVar c) .->. TyVar a)           /\!
    TyMu b (tyAll d (tyInt .->. TyVar d) .->. TyVar b)           ==!
    TyMu b (tyAll c (tyInt .-*. TyVar c) .->. TyVar b)
  , TyMu a (tyAll c (TyVar a .-*. TyVar c) .->. TyVar a)         \/!
    TyMu b (tyAll d (TyVar b .->. TyVar d) .->. TyVar b)         ==!
    TyMu b (tyAll d (TyVar b .->. TyVar d) .->. TyVar b)
  , TyMu a (tyAll c (TyVar a .-*. TyVar c) .->. TyVar a)         /\!
    TyMu b (tyAll d (TyVar b .->. TyVar d) .->. TyVar b)         ==!
    TyMu b (tyAll d (TyVar b .-*. TyVar d) .->. TyVar b)
  , tyAll a (TyVar a .*. tyInt) .->. TyVar a  \/!
    tyAll b (TyVar b .*. tyInt) .->. TyVar a  ==!
    tyAll b (TyVar b .*. tyInt) .->. TyVar a 
  , tyAll a (TyVar a .*. tyInt) .->. TyVar a  /\!
    tyAll b (TyVar b .*. tyInt) .->. TyVar a  ==!
    tyAll b (TyVar b .*. tyInt) .->. TyVar a 
  , tyAll a (TyVar a .*. tyInt) .->. TyVar a  \/!
    tyAll b (TyVar b .*. tyInt) .->. TyVar b  ==!
    tyAll b (TyVar b .*. tyInt) .->. tyUn
  , tyAll a (TyVar a .*. tyInt) .->. TyVar a !/\
    tyAll b (TyVar b .*. tyInt) .->. TyVar b 
  , tyBot  \/! TyVar b ==! TyVar b
  , tyIdent tyBot \/! TyVar b ==! TyVar b
  ]
  where
  t1 \/! t2 = Left (t1, t2)
  t1 /\! t2 = Right (t1, t2)
  Left  (t1, t2) ==! t =
    tassertSuccess (show t1 ++ " \\/ " ++ show t2 ++ " = " ++ show t)
                   t (t1 \/? t2)
  Right (t1, t2) ==! t =
    tassertSuccess (show t1 ++ " /\\ " ++ show t2 ++ " = " ++ show t)
                   t (t1 /\? t2)
  t1 !/\ t2 =
    tassertFailure (show t1 ++ " /\\ " ++ show t2 ++ " DNE")
                   (t1 /\? t2)
  infix 2 ==!
  infix 4 \/!, /\!, !/\
  a = tvUn "a"; b = tvUn "b"; c = tvAf "c"; d = tvAf "d"

uvarsTests = T.test
  [ tyInt   !<:  tyUnit
  , tyInt    <:! tyInt   ==! (noU, noU, noA, noA)
  , TyVar a  <:! tyInt   ==! (tyInt, noU, noA, noA)
  , TyVar c  <:! tyInt   ==! (noU, noU, tyInt, noA)
  , tyInt   !<:  TyVar a
  , TyVar a .*. TyVar a   <:! tyInt .*. tyInt
      ==! (tyInt, noU, noA, noA)
  , TyVar a .*. TyVar a  !<:  tyInt .*. tyUnit
  , TyVar a .*. TyVar a   <:! (tyInt .->. tyInt) .*. (tyInt .-*. tyInt)
      ==! (tyInt .->. tyInt, noU, noA, noA)
  , TyVar a .*. TyVar a   <:! (tyUnit .->. tyInt) .*. (tyInt .-*. tyInt)
      ==! (tyUn .->. tyInt, noU, noA, noA)
  , TyVar a .->. tyInt    <:! tyInt .->. tyInt
      ==! (tyInt, noU, noA, noA)
  , TyVar a .->. TyVar a  <:! tyInt .->. tyInt
      ==! (tyInt, noU, noA, noA)
  , TyVar a .->. TyVar a !<:  tyFloat .->. tyInt
  , TyVar a .->. TyVar a !<:  (tyInt .->. tyInt) .-*. (tyInt .-*. tyInt)
  , TyVar c .->. TyVar c  <:! (tyInt .->. tyInt) .-*. (tyInt .-*. tyInt)
      ==! (noU, noU, tyInt .->. tyInt, noA)
  , TyVar c .->. TyVar c !<:  (tyInt .-*. tyInt) .-*. (tyInt .->. tyInt)
  , TyVar c .-*. TyVar c !<:  (tyInt .->. tyInt) .->. (tyInt .-*. tyInt)
  , TyVar a .*.  TyVar a  <:! tyDual (tyRecv tyInt .:. tyUnit) .*.
                                     (tySend tyInt .:. tyUnit)
      ==! (tySend tyInt .:. tyUnit, noU, noA, noA)
  , TyVar a .*.  TyVar a !<:  tyDual (tyRecv tyInt .:. tyUnit) .*.
                                     (tySend tyInt .:. tyInt)
  , TyVar a .*.  tyAll a (TyVar a .->. tyInt)  <:!
    tyInt   .*.  tyAll b (TyVar b .->. tyInt)
      ==!  (tyInt, noU, noA, noA)
  , TyVar a .*.  tyAll a (TyVar a .->. tyInt)  <:!
    tyInt   .*.  tyAll b (tyInt   .->. tyInt)
      ==!  (tyInt, noU, noA, noA)
  , tyAll a (TyVar a .->. tyInt)  <:!
    tyAll a (tyInt   .->. tyInt)
      ==!  (noU, noU, noA, noA)
  , TyVar a <:! tyInt .->. TyMu a (tyInt .->. TyVar a)
      ==!  (TyMu b (tyInt .->. TyVar b), noU, noA, noA)
  , TyVar a .->. TyVar b <:! tyInt .->. TyMu a (tyInt .->. TyVar a)
      ==!  (tyInt, TyMu b (tyInt .->. TyVar b), noA, noA)
  , TyVar a .->. TyVar b <:! TyMu a (tyInt .->. TyVar a)
      ==!  (tyInt, TyMu b (tyInt .->. TyVar b), noA, noA)
  , TyVar a >:! tyInt
      ==!  (tyInt, noU, noA, noA)
  , TyVar a .-*. TyVar a  >:! tyInt .->. tyInt
      ==!  (tyInt, noU, noA, noA)
  , TyVar a .->. TyVar a !>:  tyInt .-*. tyInt
  , TyVar a .-*. TyVar a  >:! tyUn  .->. tyInt
      ==!  (tyInt, noU, noA, noA)
  , TyFun (qInterpret (qeVar c)) tyInt tyInt <:! tyInt .-*. tyInt
      ==!  (noU, noU, noA, noA)
  , TyFun (qInterpret (qeVar c)) tyInt tyInt <:! tyInt .->. tyInt
      ==!  (noU, noU, noA, noA)
  , (TyVar c .->. TyVar d .-*. TyVar d) .*. TyVar d .*. tyRecv (TyVar c)
    <:!
    (TyVar e .->. TyVar f .-*. TyVar f) .*. TyVar f .*. tyRecv (TyVar e)
      ==! (noU, noU, TyVar e, TyVar f)
  , tyConst (TyVar a) <:! tyConst (tyInt)
      ==! (tyInt, noU, noA, noA) -- suboptimal
  , tyConst (TyVar a .*. tyUnit) <:! tyConst (tyInt .*. tyInt)
      ==! (noU, noU, noA, noA)
  , tyRecv (TyVar c) .*. tyRecv (TyVar c)  >:!
    tyRecv (TyVar e) .*. tyAll f (tyRecv (TyVar f))
      ==! (noU, noU, TyVar e, noA)
  , tyRecv (TyVar c) .*. tyRecv (TyVar c)  >:!
    tyRecv (TyVar e) .*. tyRecv (TyVar e)
      ==! (noU, noU, TyVar e, noA)
  , tyRecv (TyVar c) .*. tyRecv (TyVar c) !>:
    tyRecv (TyVar e) .*. tyRecv (TyVar f)
  , tassertFailure "'<c `supertype` '<d = ERROR"
                   (subtype 100 [c] (TyVar c) [d] (TyVar d))
  , tyFollow (TyVar a) (TyVar b) >:!
    tyFollow tyUnit (tyRecv tyInt .:.
                     TyMu e (tyFollow tyUnit (tyRecv tyInt .:.
                                              TyVar e)))
      ==! (tyUnit, (tyRecv tyInt .:.
                     TyMu e (tyFollow tyUnit (tyRecv tyInt .:.
                                              TyVar e))), noA, noA)
  , tyFollow (TyVar a) (TyVar b) >:!
    TyMu e (tyFollow tyUnit (tyRecv tyInt .:. TyVar e))
      ==! (tyUnit, (tyRecv tyInt .:.
                     TyMu e (tyFollow tyUnit (tyRecv tyInt .:.
                                              TyVar e))), noA, noA)
  ]
  where
  t1 <:! t2 = Left (t1, t2)
  t1 >:! t2 = Right (t1, t2)
  Left (t1, t2) ==! (ta, tb, tc, td) =
    tassertSuccess (show t1 ++ " `subtype` " ++ show t2)
                   ([ta, tb, tc, td], [])
                   (subtype 100 set t1 [] t2)
  Right (t1, t2) ==! (ta, tb, tc, td) =
    tassertSuccess (show t1 ++ " `supertype` " ++ show t2)
                   ([], [ta, tb, tc, td])
                   (subtype 100 [] t2 set t1)
  t1 !<: t2 =
    tassertFailure (show t1 ++ " `subtype` " ++ show t2 ++ " = ERROR")
                   (subtype 100 set t1 [] t2)
  t1 !>: t2 =
    tassertFailure (show t1 ++ " `supertype` " ++ show t2 ++ " = ERROR")
                   (subtype 100 [] t2 set t1)
  infix 2 ==!
  infix 4 <:!, !<:, >:!, !>:
  noU = tyBot; noA = tyBot
  set = [a, b, c, d]
  a   = tvUn "a"; b = tvUn "b"; c = tvAf "c"; d = tvAf "d"
  e   = tvAf "e"; f = tvAf "f"

tassertSuccess :: (Eq a, Show a) =>
                  String -> a -> Either String a -> T.Assertion
tassertSuccess msg = T.assertEqual msg . Right

tassertFailure :: String -> Either String a -> T.Assertion
tassertFailure msg = either (\_ -> return ()) (\_ -> T.assertFailure msg)

tests :: IO ()
tests = do
  T.runTestTT subtypeTests
  T.runTestTT joinTests
  T.runTestTT uvarsTests
  return ()