{-# LANGUAGE
      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 Type
import Util
import Viewable

import qualified Control.Monad.Reader as CMR
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 })

lift :: (CMR.MonadTrans t, Monad m) => m a -> t m a
lift  = CMR.lift

runUT  :: forall s a m. Monad m =>
          (forall t. UT s t a) -> S.Set TyVarR -> m a
runUT m set =
  either fail return $
    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 fail $
            "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 :: Monad 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 = 
      fail $
        "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 ]
    --
    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 :: Monad 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
      _ ->
        fail $
          "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 fail $
                    "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 = 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 =
    T.assertEqual (show t1 ++ " \\/ " ++ show t2 ++ " = " ++ show t)
                  (Just t) (t1 \/? t2)
  Right (t1, t2) ==! t =
    T.assertEqual (show t1 ++ " /\\ " ++ show t2 ++ " = " ++ show t)
                  (Just t) (t1 /\? t2)
  t1 !/\ t2 =
    T.assertEqual (show t1 ++ " /\\ " ++ show t2 ++ " DNE")
                  Nothing (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)
  , T.assertEqual "'<c `supertype` '<d = ERROR"
      Nothing (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) =
    T.assertEqual (show t1 ++ " `subtype` " ++ show t2)
      (Right ([ta, tb, tc, td], []))
      (runEither Left Right $ subtype 100 set t1 [] t2)
  Right (t1, t2) ==! (ta, tb, tc, td) =
    T.assertEqual (show t1 ++ " `supertype` " ++ show t2)
      (Right ([], [ta, tb, tc, td]))
      (runEither Left Right $ subtype 100 [] t2 set t1)
  t1 !<: t2 =
    T.assertEqual (show t1 ++ " `subtype` " ++ show t2 ++ " = ERROR")
                  Nothing (subtype 100 set t1 [] t2)
  t1 !>: t2 =
    T.assertEqual (show t1 ++ " `supertype` " ++ show t2 ++ " = ERROR")
                  Nothing (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"

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