content: module E.TypeCheck(
      canBeBox,
      eAp,
      inferType,
      infertype,
      typecheck,
      match,
      sortSortLike,
      sortKindLike,
      sortTermLike,
      sortTypeLike,
      typeInfer,
      typeInfer'
      ) where
  
  import Control.Monad.Reader
  import Control.Monad.Writer
  import qualified Data.Map as Map
  
  import Doc.DocLike
  import Doc.PPrint
  import Doc.Pretty
  import E.E
  import E.Eval(strong)
  import E.Subst
  import GenUtil
  import Name.Id
  import Name.Name
  import Name.Names
  import Support.CanType
  import Util.ContextMonad
  import Util.SetLike
  import qualified Util.Seq as Seq
  import {-# SOURCE #-} DataConstructors
  import {-# SOURCE #-} E.Show
  
  {-@Internals
  
  # Ajhc Core Type System
  
  Ajhc's core is based on a pure type system. A pure type system (also called a
  PTS) is actually a parameterized set of type systems. Ajhc's version is
  described by the following.
  
      Sorts  = (*, !, **, #, (#), ##, □)
      Axioms = (*:**, #:##, !:**, **:□, ##:□)
  
      -- sort kind
      *   is the kind of boxed values
      !   is the kind of boxed strict values
      #   is the kind of unboxed values
      (#) is the kind of unboxed tuples
      -- sort superkind
      **  is the superkind of all boxed value
      ##  is the superkind of all unboxed values
      -- sort box
      □   superkinds inhabit this
  
      in addition there exist user defined kinds, which are always of supersort ##
  
  The following Rules table shows what sort of abstractions are allowed, a rule
  of the form (A,B,C) means you can have functions of things of sort A to things
  of sort B and the result is something of sort C. _Function_ in this context
  subsumes both term and type level abstractions.
  
  Notice that functions are always boxed, but may be strict if they take an
  unboxed tuple as an argument.  When a function is strict it means that it is
  represented by a pointer to code directly, it cannot be a suspended value that
  evaluates to a function.
  
  These type system rules apply to lambda abstractions. It is possible that data
  constructors might exist that cannot be given a type on their own with these
  rules, even though when fully applied it has a well formed type. An example
  would be unboxed tuples. This presents no difficulty as one concludes correctly
  that it is a type error for these constructors to ever appear when not fully
  saturated with arguments.
  
      as a shortcut we will use *# to mean every combination involving * and #, and so forth.
      for instance, (*#,*#,*) means the set (*,*,*) (#,*,*) (*,#,*) (#,#,*)
  
      Rules =
         (*#!,*#!,*)  -- functions from values to values are boxed and lazy
         (*#!,(#),*)  -- functions from values to unboxed tuples are boxed and lazy
         ((#),*#!,!)  -- functions from unboxed tuples to values are boxed and strict
         ((#),(#),!)  -- functions from unboxed tuples to unboxed tuples are boxed and strict
         (**,*,*)     -- may have a function from an unboxed type to a value
         (**,#,*)
         (**,!,*)
         (**,**,**)  -- we have functions from types to types
         (**,##,##)  -- MutArray_ :: * -> #
         (##,##,##)  -- Complex_ :: # -> #
  
      The defining feature of boxed values is
  
      _|_ :: t iff t::*
  
      This PTS is functional but not injective
  
  The PTS can be considered stratified into the following levels
  
      □                - sort box
      **,##,           - sort superkind
      *,#,(#),!        - sort kind
      Int,Bits32_,Char - sort type
      3,True,"bob"     - sort value
  
  ## On boxed kinds
  
  The boxed kinds (* and !) represent types that have a uniform run time
  representation. Due to this, functions may be written that are polymorphic in types of these kinds.
  Hence the rules of the form (**,?,?), allowing taking types of boxed kinds as arguments.
  
  the unboxed kind # is inhabited with types that have their own specific run
  time representation. Hence you cannot write functions that are polymorphic in
  unboxed types
  
  ## On sort box, the unboxed tuple, and friends
  
  Although sort box does not appear in the code, it is useful from a theoretical
  point of view to talk about certain types such as the types of unboxed tuples.
  Unboxed tuples may have boxed and unboxed arguments, without sort box it would
  be impossible to express this since it must be superkind polymorphic. sort box
  allows one to express this as (in the case of the unboxed 2-tuple)
  
      ∀s1:□ ∀s2:□ ∀k1:s1 ∀k2:s2 ∀t1:k1 ∀t2:k2 . (# t1, t2 #)
  
  However, although this is a valid typing of what it would mean if a unboxed
  tuple were not fully applied, since we do not have any rules of form (##,?,?) or
  (□,?,?) this type obviously does not typecheck. Which is what enforces the
  invarient that unboxed tuples are always fully applied, and is also why we do
  not need a code representation of sort box.
  
  ### Do we need a superbox?
  
  You will notice that if you look at the axioms involving the sorts, you end up
  with a disjoint graph
  
               □             - the box
              / \
            **   ##          - superkind
            /\     \
           *  !     #   (#)  - kind
  
  This is simply due to the fact that nothing is polymorphic in unboxed tuples of
  kind (#) so we never need to refer to any super-sorts of them. We can add sorts
  (##),(□) and □□ to fill in the gaps, but since these sorts will never appear in
  code or discourse, we will ignore them from now on.
  
                 □□            - sort superbox
                /  \
               □    (□)        - sort box
              / \      \
            **   ##     (##)   - sort superkind
            /\     \    |
           *  !     #   (#)    - sort kind
  
  -}
  
  ptsAxioms :: Map.Map ESort ESort
  ptsAxioms = Map.fromList [
      (EStar,EStarStar),
      (EBang,EStarStar),
      (EHash,EHashHash),
      (ETuple,EHashHash)
      ]
  
  ptsRulesMap :: Map.Map (ESort,ESort) ESort
  ptsRulesMap = Map.fromList [ ((a,b),c) | (as,bs,c) <- ptsRules, a <- as, b <- bs  ] where
      starHashBang = [EStar,EHash,EBang]
      ptsRules = [
          (starHashBang,ETuple:starHashBang,EStar),
          ([ETuple],ETuple:starHashBang,EBang),
          ([EStarStar],starHashBang,EStar),
          ([EStarStar],[EStarStar],EStarStar),
          ([EStarStar],[EHashHash],EHashHash),
          ([EHashHash],[EHashHash],EHashHash)
          ]
  
  canBeBox x | getType (getType x) == ESort EStarStar = True
  canBeBox _ = False
  
  tBox = mktBox eStar
  
  monadicLookup key m = case Map.lookup key m of
      Just x  -> return x
      Nothing -> fail "Key not found"
  
  -- Fast (and lazy, and perhaps unsafe) typeof
  instance CanType E where
      type TypeOf E = E
      getType (ESort s) = ESort $ getType s
      getType (ELit l) = getType l
      getType (EVar v) =  getType v
      getType e@(EPi TVr { tvrType = a } b)
          | isUnknown typa || isUnknown typb = Unknown
          | otherwise = maybe (error $ "E.TypeCheck.getType: " ++ show (e,getType a,getType b)) ESort $ do
              ESort s1 <- return $ getType a
              ESort s2 <- return $ getType b
              monadicLookup (s1,s2) ptsRulesMap
          where typa = getType a; typb = getType b
      getType (EAp (ELit LitCons { litType = EPi tvr a }) b) = getType (subst tvr b a)
      getType (EAp (ELit lc@LitCons { litAliasFor = Just af }) b) = getType (foldl eAp af (litArgs lc ++ [b]))
      getType (EAp (EPi tvr a) b) = getType (subst tvr b a)
      getType e@(EAp a b) = ans where
          ans = if isUnknown typa then Unknown else if a == tBox || typa == tBox then tBox else (case a of
              (ELit LitCons {}) -> error $ "getType: application of type alias " ++ (render $ parens $ ePretty e)
              _ -> eAp typa b)
          typa = getType a
      getType (ELam (TVr { tvrIdent = x, tvrType =  a}) b) = EPi (tVr x a) (getType b)
      getType (ELetRec _ e) = getType e
      getType ECase {eCaseType = ty} = ty
      getType (EError _ e) = e
      getType (EPrim _ _ t) = t
      getType Unknown = Unknown
  
  instance CanType ESort where
      type TypeOf ESort = ESort
      getType (ESortNamed _) = EHashHash
      getType s = case Map.lookup s ptsAxioms of
          Just s -> s
          Nothing -> error $ "getType: " ++ show s
  instance CanType TVr where
      type TypeOf TVr = E
      getType = tvrType
  instance CanType (Lit x t) where
      type TypeOf (Lit x t) = t
      getType l = litType l
  instance CanType e => CanType (Alt e) where
      type TypeOf (Alt e) = TypeOf e
      getType (Alt _ e) = getType e
  
  sortSortLike (ESort s) = isEHashHash s || isEStarStar s
  sortSortLike _ = False
  
  sortKindLike (ESort s) =  not (isEHashHash s) && not (isEStarStar s)
  sortKindLike e = sortSortLike (getType e)
  
  sortTypeLike ESort {} = False
  sortTypeLike e = sortKindLike (getType e)
  
  sortTermLike ESort {} = False
  sortTermLike e = sortTypeLike (getType e)
  
  withContextDoc s a = withContext (render s) a
  
  -- | Perform a full typecheck, evaluating type terms as necessary.
  
  inferType :: (ContextMonad m, ContextOf m ~ String) => DataTable -> [(TVr,E)] -> E -> m E
  inferType dataTable ds e = rfc e where
      inferType' ds e = inferType dataTable ds e
      prettyE = ePretty
      rfc e =  withContextDoc (text "fullCheck:" </> prettyE e) (fc e >>= strong')
      rfc' nds e = withContextDoc (text "fullCheck':" </> prettyE e) (inferType' nds e)
      strong' e = withContextDoc (parens $ text "Strong:" </> prettyE e) $ strong ds e
      fc s@(ESort _) = return $ getType s
      fc (ELit lc@LitCons {}) | let lc' = updateLit dataTable lc, litAliasFor lc /= litAliasFor lc' = fail $ "Alias not correct: " ++ show (lc, litAliasFor lc')
      fc (ELit LitCons { litName = n, litArgs = es, litType =  t}) | nameType n == TypeConstructor, Just _ <- fromUnboxedNameTuple n = do
          withContext ("Checking Unboxed Tuple: " ++ show n) $ do
          -- we omit kind checking for unboxed tuples
          valid t
          es' <- mapM rfc es
          strong' t
      fc e@(ELit LitCons { litName = n, litArgs = es, litType =  t}) = do
          withContext ("Checking Constructor: " ++ show e) $ do
          valid t
          es' <- mapM rfc es
          t' <- strong' t
          let sts = slotTypes dataTable n t
              les = length es
              lsts = length sts
          withContext ("Checking Args: " ++ show (sts,es')) $ do
          unless (les == lsts || (les < lsts && isEPi t')) $ do
              fail "constructor with wrong number of arguments"
          zipWithM_ eq sts es'
          return t'
      fc e@(ELit _) = let t = getType e in valid t >> return t
      fc (EVar (TVr { tvrIdent = eid })) | eid == emptyId = fail "variable with nothing!"
      fc (EVar (TVr { tvrType =  t})) = valid t >> strong' t
      fc (EPi (TVr { tvrIdent = n, tvrType =  at}) b) = do
          ESort a <- rfc at
          ESort b <- rfc' [ d | d@(v,_) <- ds, tvrIdent v /= n ] b
          liftM ESort $ monadicLookup (a,b) ptsRulesMap
          --valid at >> rfc' [ d | d@(v,_) <- ds, tvrIdent v /= n ] b
      --fc (ELam tvr@(TVr n at) b) = valid at >> rfc' [ d | d@(v,_) <- ds, tvrIdent v /= n ] b >>= \b' -> (strong' $ EPi tvr b')
      fc (ELam tvr@(TVr { tvrIdent = n, tvrType =  at}) b) = do
          withContext "Checking Lambda" $ do
          valid at
          b' <- withContext "Checking Lambda Body" $ rfc' [ d | d@(v,_) <- ds, tvrIdent v /= n ] b
          withContext "Checking lambda pi" $ strong' $ EPi tvr b'
      fc (EAp (EPi tvr e) b) = rfc (subst tvr b e)
      fc (EAp (ELit lc@LitCons { litAliasFor = Just af }) b) = rfc (EAp (foldl eAp af (litArgs lc)) b)
      fc (EAp a b) = do
          withContextDoc (text "EAp:" </> parens (prettyE a) </> parens (prettyE b)) $ do
              a' <- rfc a
              if a' == tBox then return tBox else strong' (eAp a' b)
      fc (ELetRec vs e) = do
          let ck (TVr { tvrIdent = eid },_) | eid == emptyId = fail "binding of empty var"
              ck (tv@(TVr { tvrType =  t}),e) = withContextDoc (hsep [text "Checking Let: ", parens (pprint tv),text  " = ", parens $ prettyE e ])  $ do
                  when (getType t == eHash && not (isEPi t)) $ fail $ "Let binding unboxed value: " ++ show (tv,e)
                  valid' nds t
                  fceq nds e t
              nds = vs ++ ds
          mapM_ ck vs
          when (hasRepeatUnder (tvrIdent . fst) vs) $ fail "Repeat Variable in ELetRec"
          inferType' nds e
          --et <- inferType' nds e
          --strong nds et
      fc (EError _ e) = valid e >> (strong'  e)
      fc (EPrim _ ts t) = mapM_ valid ts >> valid t >> ( strong' t)
      fc ec@ECase { eCaseScrutinee = e@ELit {}, eCaseBind = b, eCaseAlts = as, eCaseType = dt } | sortTypeLike e = do   -- TODO - this is a hack to get around case of constants.
          withContext "Checking typelike pattern binding case" $ do
          et <- rfc e
          withContext "Checking typelike default binding" $ eq et (getType b)
          verifyPats (casePats ec)
          -- skip checking alternatives
          ps <- mapM (strong' . getType) $ casePats ec
          withContext "Checking typelike pattern equality" $  eqAll (et:ps)
          strong' dt
      fc ec@ECase {eCaseScrutinee = e, eCaseBind = b, eCaseAlts = as, eCaseType = dt } | sortTypeLike e  = do   -- TODO - we should substitute the tested for value into the default type.
          withContext "Checking typelike binding case" $ do
          et <- rfc e
          withContext "Checking typelike default binding" $ eq et (getType b)
          --dt <- rfc d
          --bs <- mapM rfc (caseBodies ec)  -- these should be specializations of dt
          withContext "Checking typelike alternatives" $ mapM_ (calt e) as
          --eqAll bs
          verifyPats (casePats ec)
          ps <- withContext "Getting pattern types" $ mapM (strong' . getType) $ casePats ec
          withContext "checking typelike pattern equality" $ eqAll (et:ps)
          withContext "Evaluating Case Type" $ strong' dt
      fc ec@ECase { eCaseScrutinee =e, eCaseBind = b } = do
          withContext "Checking plain case" $ do
          et <- rfc e
          withContext "Checking default binding" $ eq et (getType b)
          bs <- withContext "Checking case bodies" $ mapM rfc (caseBodies ec)
          ect <- strong' (eCaseType ec)
          withContext "Checking case bodies have equal types" $ eqAll (ect:bs)
          verifyPats (casePats ec)
          ps <- mapM (strong' . getType) $ casePats ec
          withContext "checking pattern equality" $ eqAll (et:ps)
          return ect
      fc Unknown = return Unknown
      --fc e = failDoc $ text "what's this? " </> (prettyE e)
      calt (EVar v) (Alt l e) = do
          let nv =  followAliases undefined (patToLitEE l)
          rfc (subst' v nv e)
      calt _ (Alt _ e) = rfc e
      verifyPats xs = do
          mapM_ verifyPats' xs
          when (hasRepeatUnder litHead xs) $ fail "Duplicate case alternatives"
  
      verifyPats' LitCons { litArgs = xs } = when (hasRepeatUnder id (filter (/= emptyId) $ map tvrIdent xs)) $ fail "Case pattern is non-linear"
      verifyPats' _ = return ()
  
      eqAll ts = withContextDoc (text "eqAll" </> list (map prettyE ts)) $ foldl1M_ eq ts
      valid s = valid' ds s
      valid' nds ESort {} = return ()
      valid' nds s
          | Unknown <- s = return ()
          | otherwise =  withContextDoc (text "valid:" <+> prettyE s) (do t <- inferType' nds s;  valid' nds t)
      eq box t2 | boxCompat box t2 = return t2
      eq t1 box | boxCompat box t1 = return t1
     -- box == tBox, canBeBox t2 = return t2
     -- eq t1 box | box == tBox, canBeBox t1 = return t1
      eq Unknown t2 = return t2
      eq t1 Unknown = return t1
      eq t1 t2 = eq' ds t1 t2
      eq' nds t1 t2 = do
          e1 <- strong nds (t1)
          e2 <- strong nds (t2)
          case typesCompatable e1 e2 of
              Just () -> return (e1)
              Nothing -> failDoc $ text "eq:" <+> align $ vcat [ prettyE (e1), prettyE (e2) ]
      fceq nds e1 t2 = do
          withContextDoc (hsep [text "fceq:", align $ vcat [parens $ prettyE e1,  parens $ prettyE t2]]) $ do
          t1 <- inferType' nds e1
          eq' nds t1 t2
      boxCompat (ELit (LitCons { litName = n }))  t | Just e <- fromConjured modBox n =  e == getType t
      boxCompat _ _ = False
  
  -- This should perform a full typecheck and may take any extra information needed as an extra parameter
  class CanTypeCheck a where
      typecheck :: Monad m => DataTable -> a -> m E
  
  infertype :: CanTypeCheck a => DataTable -> a -> E
  infertype env a = case typecheck env a of
      Left s -> error $ "infertype: " ++ s
      Right x -> x
  
  instance CanTypeCheck E where
      typecheck dataTable e = case runContextEither $ typeInfer'' dataTable [] e of
          Left ss -> fail $ "\n>>> internal error:\n" ++ unlines ss
          Right v -> return v
  
  instance CanTypeCheck TVr where
      typecheck dt tvr = do
          typecheck dt (getType tvr)
          return $ getType tvr
  
  instance CanTypeCheck (Lit a E) where
      typecheck  dt LitCons { litType = t } = typecheck dt t >> return t
      typecheck  dt LitInt  { litType = t } = typecheck dt t >> return t
  
  -- TODO, types might be bound in scrutinization
  instance CanTypeCheck (Alt E) where
      typecheck dt (Alt l e) = typecheck dt l >> typecheck dt e
  
  -- | Determine type of term using full algorithm with substitutions. This
  -- should be used instead of 'typ' when let-bound type variables exist or you
  -- wish a more thorough checking of types.
  
  typeInfer :: DataTable -> E -> E
  typeInfer dataTable e = case runContextEither $ typeInfer'' dataTable [] e of
      Left ss -> error $ "\n>>> internal error:\n" ++ unlines (tail ss)
      Right v -> v
  
  typeInfer' :: DataTable -> [(TVr,E)] -> E -> E
  typeInfer' dataTable ds e = case runContextEither $ typeInfer'' dataTable ds e of
      Left ss -> error $ "\n>>> internal error:\n" ++ unlines (tail ss)
      Right v -> v
  
  data TcEnv = TcEnv {
      --tcDefns :: [(TVr,E)],
      tcContext :: [String]
      --tcDataTable :: DataTable
      }
  
  tcContext_u f r@TcEnv{tcContext  = x} = r{tcContext = f x}
  
  newtype Tc a = Tc (Reader TcEnv a)
      deriving(Monad,Functor,MonadReader TcEnv)
  
  instance ContextMonad Tc where
      type ContextOf Tc = String
      withContext s = local (tcContext_u (s:))
  
  {-
  tcE :: E -> Tc E
  tcE e = rfc e where
      rfc e =  withContextDoc (text "tcE:" </> ePretty e) (fc e >>=  strong')
      strong' e = do
          ds <- asks tcDefns
          withContextDoc (text "tcE.strong:" </> ePretty e) $ strong ds e
  
      fc s@ESort {} = return $ getType s
      fc (ELit LitCons { litType = t }) = strong' t
      fc e@ELit {} = strong' (getType e)
      fc (EVar TVr { tvrIdent = eid }) | eid == emptyId = fail "variable with nothing!"
      fc (EVar TVr { tvrType =  t}) =  strong' t
      fc (EPi TVr { tvrIdent = n, tvrType = at} b) =  do
          ESort a <- rfc at
          ESort b <- local (tcDefns_u (\ds -> [ d | d@(v,_) <- ds, tvrIdent v /= n ])) $ rfc b
          liftM ESort $ monadicLookup (a,b) ptsRulesMap
      fc (ELam tvr@TVr { tvrIdent = n, tvrType =  at} b) = do
          at' <- strong' at
          b' <- local (tcDefns_u (\ds -> [ d | d@(v,_) <- ds, tvrIdent v /= n ])) $ rfc b
          return (EPi (tVr n at') b')
      fc (EAp (EPi tvr e) b) = do
          b <- strong' b
          rfc (subst tvr b e)
      fc (EAp (ELit lc@LitCons { litAliasFor = Just af }) b) = fc (EAp (foldl eAp af (litArgs lc)) b)
      fc (EAp a b) = do
          a' <- rfc a
          if a' == tBox then return tBox else strong' (eAp a' b)
      fc (ELetRec vs e) = local (tcDefns_u (vs ++)) $ rfc e
      fc (EError _ e) = strong' e
      fc (EPrim _ ts t) = strong' t
      fc ECase { eCaseType = ty } = do
          strong' ty
      fc Unknown = return Unknown
      fc e = failDoc $ text "what's this? " </> (ePretty e)
  -}
  
  typeInfer'' :: (ContextMonad m, ContextOf m ~ String) => DataTable -> [(TVr,E)] -> E -> m E
  typeInfer'' dataTable ds e = rfc e where
      inferType' ds e = typeInfer'' dataTable ds e
      rfc e =  withContextDoc (text "fullCheck':" </> ePretty e) (fc e >>= strong')
      rfc' nds e =  withContextDoc (text "fullCheck':" </> ePretty e) (inferType' nds e)
      strong' e = withContextDoc (text "Strong':" </> ePretty e) $ strong ds e
      fc s@ESort {} = return $ getType s
      fc (ELit LitCons { litType = t }) = strong' t
      fc e@ELit {} = strong' (getType e)
      fc (EVar TVr { tvrIdent = eid }) | eid == emptyId = fail "variable with nothing!"
      fc (EVar TVr { tvrType =  t}) =  strong' t
      fc (EPi TVr { tvrIdent = n, tvrType = at} b) =  do
          ESort a <- rfc at
          ESort b <- rfc' [ d | d@(v,_) <- ds, tvrIdent v /= n ] b
          liftM ESort $ monadicLookup (a,b) ptsRulesMap
      fc (ELam tvr@TVr { tvrIdent = n, tvrType =  at} b) = do
          at' <- strong' at
          b' <- rfc' [ d | d@(v,_) <- ds, tvrIdent v /= n ] b
          return (EPi (tVr n at') b')
      fc (EAp (EPi tvr e) b) = do
          b <- strong' b
          rfc (subst tvr b e)
      fc (EAp (ELit lc@LitCons { litAliasFor = Just af }) b) = fc (EAp (foldl eAp af (litArgs lc)) b)
      fc (EAp a b) = do
          a' <- rfc a
          if a' == tBox then return tBox else strong' (eAp a' b)
      fc (ELetRec vs e) = do
          let nds = vs ++ ds
          --et <- inferType' nds e
          --strong nds et
          inferType' nds e
      fc (EError _ e) = strong' e
      fc (EPrim _ ts t) = strong' t
      fc ECase { eCaseType = ty } = do
          strong' ty
      fc Unknown = return Unknown
      --fc e = failDoc $ text "what's this? " </> (ePretty e)
  
  -- | find substitution that will transform the left term into the right one,
  -- only substituting for the vars in the list
  
  match :: Monad m =>
      (Id -> Maybe E)      -- ^ function to look up values in the environment
      -> [TVr]              -- ^ vars which may be substituted
      -> E                  -- ^ pattern to match
      -> E                  -- ^ input expression
      -> m [(TVr,E)]
  match lup vs = \e1 e2 -> liftM Seq.toList $ execWriterT (un e1 e2 etherealIds) where
      bvs :: IdSet
      bvs = fromList (map tvrIdent vs)
  
      un (EAp a b) (EAp a' b') c = do
          un a a' c
          un b b' c
      un (ELam va ea) (ELam vb eb) c = lam va ea vb eb c
      un (EPi va ea) (EPi vb eb) c = lam va ea vb eb c
      un (EPi va ea) (ELit LitCons { litName = ar, litArgs = [x,y], litType = lt}) c | ar == tc_Arrow = do
          un (tvrType va) x c
          un ea y c
      un (EPrim s xs t) (EPrim s' ys t') c | length xs == length ys = do
          sequence_ [ un x y c | x <- xs | y <- ys]
          un t t' c
      un (ESort x) (ESort y) c | x == y = return ()
      un (ELit (LitInt x t1))  (ELit (LitInt y t2)) c | x == y = un t1 t2 c
      un (ELit LitCons { litName = n, litArgs = xs, litType = t })  (ELit LitCons { litName = n', litArgs = ys, litType =  t'}) c | n == n' && length xs == length ys = do
          sequence_ [ un x y c | x <- xs | y <- ys]
          un t t' c
  
      un (EVar TVr { tvrIdent = i, tvrType =  t}) (EVar TVr {tvrIdent = j, tvrType =  u}) c | i == j = un t u c
      un (EVar TVr { tvrIdent = i, tvrType =  t}) (EVar TVr {tvrIdent = j, tvrType =  u}) c | isEtherealId i || isEtherealId j   = fail "Expressions don't match"
      un (EAp a b) (ELit lc@LitCons { litArgs = bas@(_:_), litType = t }) c = do
          let (al:as) = reverse bas
          un a (ELit lc { litArgs = reverse as, litType = ePi tvr { tvrType = getType al } t }) c
          un b al c
      un (EAp a b) (EPi TVr { tvrType = a1 } a2) c = do
          un a (ELit litCons { litArgs = [a1], litName = tc_Arrow, litType = EPi tvr { tvrType = getType a2 } (getType a1) }) c
          un b a2 c
      un (EVar tvr@TVr { tvrIdent = i, tvrType = t}) b c
          | i `member` bvs = tell (Seq.single (tvr,b))
          | otherwise = fail $ "Expressions do not unify: " ++ show tvr ++ show b
      un a (EVar tvr) c | Just b <- lup (tvrIdent tvr), not $ isEVar b = un a b c
      --un a b c | Just a' <- followAlias undefined a = un a' b c
      un a b c | Just b' <- followAlias undefined b = un a b' c
  
      un a b _ = fail $ "Expressions do not unify: " ++ show a ++ show b
      lam va ea vb eb (c:cs) = do
          un (tvrType va) (tvrType vb) (c:cs)
          un (subst va (EVar va { tvrIdent = c }) ea) (subst vb (EVar vb { tvrIdent = c }) eb) cs
      lam _ _ _ _ _ = error "TypeCheck.match: bad."
  