content: module TypeChecker where
  
  import Control.Applicative
  import Control.Monad
  import Control.Monad.Except
  import Control.Monad.Reader
  import Control.Monad.Gen
  import qualified Data.Map as Map
  import qualified Data.Traversable as T
  
  import Cartesian
  import CTT
  import Eval
  
  -- Type checking monad
  type Typing a = ReaderT TEnv (ExceptT String (GenT Int IO)) a
  
  -- Environment for type checker
  data TEnv =
    TEnv { names   :: [String] -- generated names
         , indent  :: Int
         , env     :: Env
         , verbose :: Bool  -- Should it be verbose and print what it typechecks?
         } deriving (Eq)
  
  verboseEnv, silentEnv :: TEnv
  verboseEnv = TEnv [] 0 emptyEnv True
  silentEnv  = TEnv [] 0 emptyEnv False
  
  -- Trace function that depends on the verbosity flag
  trace :: String -> Typing ()
  trace s = do
    b <- asks verbose
    when b $ liftIO (putStrLn s)
  
  -- Helper functions for eval
  evalTC :: Env -> Ter -> Typing Val
  evalTC rho t = lift $ lift $ eval rho t
  
  appTC :: Val -> Val -> Typing Val
  appTC u v = lift $ lift $ app u v
  
  convTC :: Convertible a => [String] -> a -> a -> Typing Bool
  convTC ns u v = lift $ lift $ conv ns u v
  
  normalTC :: Normal a => [String] -> a -> Typing a
  normalTC ns u = lift $ lift $ normal ns u
  
  (@@@) :: ToII a => Val -> a -> Typing Val
  v @@@ r = lift $ lift $ v @@ toII r
  
  -------------------------------------------------------------------------------
  -- | Functions for running computations in the type checker monad
  
  runTyping :: TEnv -> Typing a -> IO (Either String a)
  runTyping env t = runGenT $ runExceptT $ runReaderT t env
  
  runDecls :: TEnv -> Decls -> IO (Either String TEnv)
  runDecls tenv d = runTyping tenv $ do
    checkDecls d
    return $ addDecls d tenv
  
  runDeclss :: TEnv -> [Decls] -> IO (Maybe String,TEnv)
  runDeclss tenv []     = return (Nothing, tenv)
  runDeclss tenv (d:ds) = do
    x <- runDecls tenv d
    case x of
      Right tenv' -> runDeclss tenv' ds
      Left s      -> return (Just s, tenv)
  
  runInfer :: TEnv -> Ter -> IO (Either String Val)
  runInfer lenv e = runTyping lenv (infer e)
  
  -------------------------------------------------------------------------------
  -- | Modifiers for the environment
  
  addTypeVal :: (Ident,Val) -> TEnv -> TEnv
  addTypeVal (x,a) (TEnv ns ind rho v) =
    let w@(VVar n _) = mkVarNice ns x a
    in TEnv (n:ns) ind (upd (x,w) rho) v
  
  addSub :: (Name,II) -> TEnv -> TEnv
  addSub iphi (TEnv ns ind rho v) = TEnv ns ind (sub iphi rho) v
  
  addSubs :: [(Name,II)] -> TEnv -> TEnv
  addSubs = flip $ foldr addSub
  
  addType :: (Ident,Ter) -> TEnv -> Typing TEnv
  addType (x,a) tenv@(TEnv _ _ rho _) = do
    va <- evalTC rho a
    return $ addTypeVal (x,va) tenv
  
  addBranch :: [(Ident,Val)] -> Env -> TEnv -> TEnv
  addBranch nvs env (TEnv ns ind rho v) =
    TEnv ([n | (_,VVar n _) <- nvs] ++ ns) ind (upds nvs rho) v
  
  addDecls :: Decls -> TEnv -> TEnv
  addDecls d (TEnv ns ind rho v) = TEnv ns ind (def d rho) v
  
  addTele :: Tele -> TEnv -> Typing TEnv
  addTele xas lenv = foldM (flip addType) lenv xas
  
  -- Only works for equations in a system (so of shape (Name,II))
  faceEnv :: Eqn -> TEnv -> Typing TEnv
  faceEnv ir tenv = do
    tenv' <- lift $ lift $ env tenv `face` ir
    return $ tenv{env=tenv'}
  
  -------------------------------------------------------------------------------
  -- | Various useful functions
  
  -- Extract the type of a label as a closure
  getLblType :: LIdent -> Val -> Typing (Tele, Env)
  getLblType c (Ter (Sum _ _ cas) r) = case lookupLabel c cas of
    Just as -> return (as,r)
    Nothing -> throwError ("getLblType: " ++ show c ++ " in " ++ show cas)
  getLblType c (Ter (HSum _ _ cas) r) = case lookupLabel c cas of
    Just as -> return (as,r)
    Nothing -> throwError ("getLblType: " ++ show c ++ " in " ++ show cas)
  getLblType c u = throwError ("expected a data type for the constructor "
                               ++ c ++ " but got " ++ show u)
  
  -- Monadic version of unless
  unlessM :: Monad m => m Bool -> m () -> m ()
  unlessM mb x = mb >>= flip unless x
  
  mkVars :: [String] -> Tele -> Env -> Typing [(Ident,Val)]
  mkVars _ [] _ = return []
  mkVars ns ((x,a):xas) nu = do
    va <- evalTC nu a
    let w@(VVar n _) = mkVarNice ns x va
    xs <- mkVars (n:ns) xas (upd (x,w) nu)
    return $ (x,w) : xs
  
  -- Test if two values are convertible
  (===) :: Convertible a => a -> a -> Typing Bool
  u === v = do
    ns <- asks names
    convTC ns u v
  
  -- eval in the typing monad
  evalTyping :: Ter -> Typing Val
  evalTyping t = do
    rho <- asks env
    evalTC rho t
  
  -------------------------------------------------------------------------------
  -- | The bidirectional type checker
  
  -- Check that t has type a
  check :: Val -> Ter -> Typing ()
  check a t = case (a,t) of
    (_,Undef{}) -> return ()
    (_,Hole l)  -> do
        rho <- asks env
        let e = unlines (reverse (contextOfEnv rho))
        ns <- asks names
        na <- normalTC ns a
        trace $ "\nHole at " ++ show l ++ ":\n\n" ++
                e ++ replicate 80 '-' ++ "\n" ++ show na ++ "\n"
    (_,Con c es) -> do
      (bs,nu) <- getLblType c a
      checks (bs,nu) es
    (VU,Pi f)       -> checkFam f
    (VU,Sigma f)    -> checkFam f
    (VU,Sum _ _ bs) -> forM_ bs $ \lbl -> case lbl of
      OLabel _ tele -> checkTele tele
      PLabel _ tele is ts ->
        throwError $ "check: no path constructor allowed in " ++ show t
    (VU,HSum _ _ bs) -> forM_ bs $ \lbl -> case lbl of
      OLabel _ tele -> checkTele tele
      PLabel _ tele is ts -> do
        checkTele tele
        rho <- asks env
        unless (all (`elem` is) (eqnSupport ts)) $
          throwError "names in path label system" -- TODO
        mapM_ checkFresh is
        let iis = zip is (map Name is)
        local (addSubs iis) $ localM (addTele tele) $ do
          checkSystemWith ts $ \alpha talpha ->
            localM (faceEnv alpha) $
              -- NB: the type doesn't depend on is
              check (Ter t rho) talpha
          rho' <- asks env
          ts' <- lift $ lift $ evalSystem rho' ts
          checkCompSystem ts'
    (VPi va@(Ter (Sum _ _ cas) nu) f,Split _ _ ty ces) -> do
      check VU ty
      rho <- asks env
      ty' <- evalTC rho ty    
      unlessM (a === ty') $ throwError "check: split annotations"
      if map labelName cas == map branchName ces
         then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho) va
                        | (brc, lbl) <- zip ces cas ]
         else throwError "case branches does not match the data type"
    (VPi va@(Ter (HSum _ _ cas) nu) f,Split _ _ ty ces) -> do
      check VU ty
      rho <- asks env
      ty' <- evalTC rho ty
      unlessM (a === ty') $ throwError "check: split annotations"
      if map labelName cas == map branchName ces
         then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho) va
                        | (brc, lbl) <- zip ces cas ]
         else throwError "case branches does not match the data type"
    (VPi a f,Lam x a' t)  -> do
      check VU a'
      ns <- asks names
      rho <- asks env
      a'' <- evalTC rho a'
      na <- normalTC ns a
      unlessM (a === a'') $
        throwError $ "check: lam types don't match"
          ++ "\nlambda type annotation: " ++ show a'
          ++ "\ndomain of Pi: " ++ show a
          ++ "\nnormal form of type: " ++ show na
      let var = mkVarNice ns x a
      local (addTypeVal (x,a)) $ do
        f' <- appTC f var
        check f' t
    (VSigma a f, Pair t1 t2) -> do
      check a t1
      v <- evalTyping t1
      f' <- appTC f v
      check f' t2
    (_,Where e d) -> do
      local (\tenv@TEnv{indent=i} -> tenv{indent=i + 2}) $ checkDecls d
      local (addDecls d) $ check a e
    (VU,PathP a e0 e1) -> do
      (a0,a1) <- checkPLam (constPath VU) a
      check a0 e0
      check a1 e1
    (VPathP p a0 a1,PLam _ e) -> do
      (u0,u1) <- checkPLam p t
      ns <- asks names
      (nu0,nu1) <- normalTC ns (u0,u1)
      (na0,na1) <- normalTC ns (a0,a1)
      unlessM (convTC ns a0 u0) $
        throwError $ "Left endpoints don't match for \n" ++ show e ++ "\ngot\n" ++
                     show u0 ++ "\nbut expected\n" ++ show a0 ++
                     "\n\nNormal forms:\n" ++ show nu0 ++ "\nand\n" ++ show na0
      unlessM (convTC ns a1 u1) $
        throwError $ "Right endpoints don't match for \n" ++ show e ++ "\ngot\n" ++
                     show u1 ++ "\nbut expected\n" ++ show a1 ++
                     "\n\nNormal forms:\n" ++ show nu1 ++ "\nand\n" ++ show na1
    (VU,LineP a) -> do
      checkPLam (constPath VU) a
      return ()
    (VLineP a,PLam _ e) -> do
      checkPLam a t
      return ()
    (VU,V r a b e) -> do
      checkII r
      check VU b
      localM (faceEnv (eqn (r,0))) $ do
        check VU a
        va <- evalTyping a
        vb <- evalTyping b
        checkEquiv va vb e
    (VV i a b e,Vin s m n) -> do
      checkII s
      unless (Name i == s) $
        throwError $ "The names " ++ show i ++ " " ++ show s ++ " do not match in Vin"
      check b n
      localM (faceEnv (eqn (s,0))) $ do
        check a m
        vm <- evalTyping m
        vn <- evalTyping n
        ns <- asks names
        evm <- appTC (equivFun e) vm
        unlessM (convTC ns evm vn) $
          throwError $ "Vin does not match V type"
    -- (VU,Glue a ts) -> do
    --   check VU a
    --   rho <- asks env
    --   checkGlue (eval rho a) ts
    -- (VGlue va ts,GlueElem u us) -> do
    --   check va u
    --   vu <- evalTyping u
    --   checkGlueElem vu ts us
    -- (VCompU va ves,GlueElem u us) -> do
    --   check va u
    --   vu <- evalTyping u
    --   checkGlueElemU vu ves us
    _ -> do
      v <- infer t
      unlessM (v === a) $
        throwError $ "check conv:\n" ++ show v ++ "\n/=\n" ++ show a
  
  
  -- Check a list of declarations
  checkDecls :: Decls -> Typing ()
  checkDecls (MutualDecls _ []) = return ()
  checkDecls (MutualDecls l d)  = do
    a <- asks env
    let (idents,tele,ters) = (declIdents d,declTele d,declTers d)
    ind <- asks indent
    trace (replicate ind ' ' ++ "Checking: " ++ unwords idents)
    checkTele tele
    local (addDecls (MutualDecls l d)) $ do
      rho <- asks env
      checks (tele,rho) ters
  checkDecls (OpaqueDecl _)      = return ()
  checkDecls (TransparentDecl _) = return ()
  checkDecls TransparentAllDecl  = return ()
  
  localM :: (TEnv -> Typing TEnv) -> Typing a -> Typing a
  localM f r = do
    e <- ask
    a <- f e
    local (const a) r
  
  -- Check a telescope
  checkTele :: Tele -> Typing ()
  checkTele []          = return ()
  checkTele ((x,a):xas) = do
    check VU a
    localM (addType (x,a)) $ checkTele xas
  
  -- Check a family
  checkFam :: Ter -> Typing ()
  checkFam (Lam x a b) = do
    check VU a
    localM (addType (x,a)) $ check VU b
  checkFam x = throwError $ "checkFam: " ++ show x
  
  -- Check that a system is compatible
  checkCompSystem :: System Val -> Typing ()
  checkCompSystem vus = do
    ns <- asks names
    b <- lift $ lift $ isCompSystem ns vus
    unless b (throwError $ "Incompatible system " ++ show vus)
  
  -- -- Check the values at corresponding faces with a function, assumes
  -- -- systems have the same faces
  -- checkSystemsWith :: (Show a, Show b) => System a -> System b -> (Eqn -> a -> b -> Typing c) -> Typing ()
  -- checkSystemsWith (Sys us) (Sys vs) f = sequence_ $ Map.elems $ Map.intersectionWithKey f us vs
  -- checkSystemsWith (Triv u) (Triv v) f = f (eqn (0,0)) u v >> return () -- TODO: Does it make sense to use the trivial equation here?
  -- checkSystemsWith x y  _= throwError $ "checkSystemsWith: cannot compare " ++ show x ++ " and " ++ show y
  
  -- Check the faces of a system
  checkSystemWith :: System a -> (Eqn -> a -> Typing b) -> Typing ()
  checkSystemWith (Sys us) f = sequence_ $ Map.elems $ Map.mapWithKey f us
  checkSystemWith (Triv u) f = f (eqn (0,0)) u >> return () -- TODO: Does it make sense to use the trivial equation here?
  
  -- Check a glueElem
  -- checkGlueElem :: Val -> System Val -> System Ter -> Typing ()
  -- checkGlueElem vu ts us = do
  --   unless (keys ts == keys us)
  --     (throwError ("Keys don't match in " ++ show ts ++ " and " ++ show us))
  --   rho <- asks env
  --   checkSystemsWith ts us
  --     (\alpha vt u -> local (faceEnv alpha) $ check (equivDom vt) u)
  --   let vus = evalSystem rho us
  --   checkSystemsWith ts vus (\alpha vt vAlpha ->
  --     unlessM (app (equivFun vt) vAlpha === (vu `subst` alpha)) $
  --       throwError $ "Image of glue component " ++ show vAlpha ++
  --                    " doesn't match " ++ show vu)
  --   checkCompSystem vus
  
  -- Check a glueElem against VComp _ ves
  -- checkGlueElemU :: Val -> System Val -> System Ter -> Typing ()
  -- checkGlueElemU vu ves us = do
  --   unless (keys ves == keys us)
  --     (throwError ("Keys don't match in " ++ show ves ++ " and " ++ show us))
  --   rho <- asks env
  --   checkSystemsWith ves us
  --     (\alpha ve u -> local (faceEnv alpha) $ check (ve @@ One) u)
  --   let vus = evalSystem rho us
  --   checkSystemsWith ves vus (\alpha ve vAlpha ->
  --     unlessM (eqFun ve vAlpha === (vu `subst` alpha)) $
  --       throwError $ "Transport of glueElem (for compU) component " ++ show vAlpha ++
  --                    " doesn't match " ++ show vu)
  --   checkCompSystem vus
  
  -- checkGlue :: Val -> System Ter -> Typing ()
  -- checkGlue va ts = do
  --   checkSystemWith ts (\alpha tAlpha -> checkEquiv (va `subst` alpha) tAlpha)
  --   rho <- asks env
  --   checkCompSystem (evalSystem rho ts)
  
  -- An iso for a type b is a five-tuple: (a,f,g,s,t)   where
  --  a : U
  --  f : a -> b
  --  g : b -> a
  --  s : forall (y : b), f (g y) = y
  --  t : forall (x : a), g (f x) = x
  -- mkIso :: Val -> Val
  -- mkIso vb = eval rho $
  --   Sigma $ Lam "a" U $
  --   Sigma $ Lam "f" (Pi (Lam "_" a b)) $
  --   Sigma $ Lam "g" (Pi (Lam "_" b a)) $
  --   Sigma $ Lam "s" (Pi (Lam "y" b $ PathP (PLam (N "_") b) (App f (App g y)) y)) $
  --     Pi (Lam "x" a $ PathP (PLam (N "_") a) (App g (App f x)) x)
  --   where [a,b,f,g,x,y] = map Var ["a","b","f","g","x","y"]
  --         rho = upd ("b",vb) emptyEnv
  
  -- An equivalence for a type a is a triple (t,f,p) where
  -- t : U
  -- f : t -> a
  -- p : (x : a) -> isContr ((y:t) * Id a x (f y))
  -- with isContr c = (z : c) * ((z' : C) -> Id c z z')
  -- mkEquiv :: Val -> Val
  -- mkEquiv va = eval rho $
  --   Sigma $ Lam "t" U $
  --   Sigma $ Lam "f" (Pi (Lam "_" t a)) $
  --   Pi (Lam "x" a $ iscontrfib)
  --   where [a,b,f,x,y,s,t,z] = map Var ["a","b","f","x","y","s","t","z"]
  --         rho = upd ("a",va) emptyEnv
  --         fib = Sigma $ Lam "y" t (PathP (PLam (N "_") a) x (App f y))
  --         iscontrfib = Sigma $ Lam "s" fib $
  --                      Pi $ Lam "z" fib $ PathP (PLam (N "_") fib) s z
  
  -- RedPRL style equiv between A and B:
  -- f : A -> B
  -- p : (x : B) -> isContr ((y : A) * Path B (f y) x)
  -- with isContr C = (s : C) * ((z : C) -> Path C z s)
  mkEquiv :: Val -> Val -> Typing Val
  mkEquiv va vb = evalTC rho $
    Sigma $ Lam "f" (Pi (Lam "_" a b)) $
    Pi (Lam "x" b iscontrfib)
    where [a,b,f,x,y,s,z] = map Var ["a","b","f","x","y","s","z"]
          rho = upd ("a",va) (upd ("b",vb) emptyEnv)
          fib = Sigma $ Lam "y" a (PathP (PLam (N "_") b) (App f y) x)
          iscontrfib = Sigma $ Lam "s" fib $
                       Pi $ Lam "z" fib $ PathP (PLam (N "_") fib) z s
  
  
  -- Part 3 style equiv between A and B:
  -- f : A -> B
  -- p : (x : B) -> isContr ((y : A) * Path B (f y) x)
  -- with isContr C = C * ((c c' : C) -> Path C c c')
  -- mkEquiv :: Val -> Val -> Typing Val
  -- mkEquiv va vb = evalTC rho $
  --   Sigma $ Lam "f" (Pi (Lam "_" a b)) $
  --   Pi (Lam "x" b iscontrfib)
  --   where [a,b,f,x,y,s,z] = map Var ["a","b","f","x","y","s","z"]
  --         rho = upd ("a",va) (upd ("b",vb) emptyEnv)
  --         fib = Sigma $ Lam "y" a (PathP (PLam (N "_") b) (App f y) x)
  --         iscontrfib = Sigma $ Lam "_" fib $
  --                      Pi $ Lam "s" fib $ Pi $ Lam "z" fib $ PathP (PLam (N "_") fib) s z
  
  checkEquiv :: Val -> Val -> Ter -> Typing ()
  checkEquiv va vb equiv = do
    e <- mkEquiv va vb
    check e equiv
  
  -- checkIso :: Val -> Ter -> Typing ()
  -- checkIso vb iso = check (mkIso vb) iso
  
  checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Val -> Typing ()
  checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do
    ns' <- asks names
    ns'' <- mkVars ns' tele nu
    let us = map snd ns''
    local (addBranch (zip ns us) nu) $ do
      f' <- appTC f (VCon c us)
      check f' e
  checkBranch (PLabel _ tele is ts,nu) f (PBranch c ns js e) g va = do
    ns' <- asks names
    -- mapM_ checkFresh js
    us <- mkVars ns' tele nu
    let vus  = map snd us
        js'  = map Name js
    vts <- lift $ lift $ evalSystem (subs (zip is js') (upds us nu)) ts
    vgts <- lift $ lift $ runSystem $ intersectWith app (border g vts) vts
    local (addSubs (zip js js') . addBranch (zip ns vus) nu) $ do
      f' <- appTC f (VPCon c va vus js')
      check f' e
      ve  <- evalTyping e -- TODO: combine with next two lines?
      let veborder = border ve vts :: System Val
      unlessM (veborder === vgts) $
        throwError $ "Faces in branch for " ++ show c ++ " don't match:"
                     ++ "\ngot\n" ++ show veborder ++ "\nbut expected\n"
                     -- ++ show vgts
  
  checkII :: II -> Typing ()
  checkII phi = do
    rho <- asks env
    let dom = domainEnv rho
    unless (all (`elem` dom) (supportII phi)) $
      throwError $ "checkII: " ++ show phi
  
  checkFresh :: Name -> Typing ()
  checkFresh i = do
    rho <- asks env
    when (i `occurs` rho)
      (throwError $ show i ++ " is already declared")
  
  -- Check that a term is a PLam and output the source and target
  checkPLam :: Val -> Ter -> Typing (Val,Val)
  checkPLam v (PLam i a) = do
    rho <- asks env
    -- checkFresh i
    local (addSub (i,Name i)) $ do
      vi <- v @@@ i
      check vi a
    (,) <$> evalTC (sub (i,Dir 0) rho) a <*> evalTC (sub (i,Dir 1) rho) a
  checkPLam v t = do
    vt <- infer t
    case vt of
      VPathP a a0 a1 -> do
        unlessM (a === v) $ throwError (
          "checkPLam\n" ++ show v ++ "\n/=\n" ++ show a)
        return (a0,a1)
      VLineP a -> do
        unlessM (a === v) $ throwError (
          "checkPLam\n" ++ show v ++ "\n/=\n" ++ show a)
        -- vt0 <- vt @@@ Dir Zero
        -- vt1 <- vt @@@ Dir One
        return (VAppII vt 0,VAppII vt 1)
      _ -> throwError $ show vt ++ " is not a path"
  
  checkPLamSystem :: II -> Ter -> Val -> System Ter -> Typing ()
  checkPLamSystem r u0 va (Sys us) = do
    T.sequence $ Map.mapWithKey (\eqn u ->
      localM (faceEnv eqn) $ do
        rhoeqn <- asks env
        va' <- lift $ lift $ va `face` eqn
        checkPLam va' u
        vu <- evalTC rhoeqn u
        vur <- vu @@@ evalII rhoeqn r
        vu0 <- evalTC rhoeqn u0
        unlessM (vur === vu0) $
          throwError $ "\nThe face " ++ show eqn ++ " of the system\n" ++
                       show (Sys us) ++ "\nat " ++ show r ++ " is " ++ show vur ++
                       "\nwhich does not match the cap " ++ show vu0) us
    -- Check that the system ps is compatible.
    rho <- asks env
    us' <- lift $ lift $ evalSystem rho (Sys us)
    checkCompSystem us'
  checkPLamSystem r u0 va (Triv u) = do
    rho <- asks env
    checkPLam va u
    vu <- evalTC rho u
    vur <- vu @@@ evalII rho r
    vu0 <- evalTC rho u0
    unlessM (vur === vu0) $
      throwError ("Trivial system " ++ show vur ++ " at " ++ show r ++
                  "\ndoes not match the cap " ++ show vu0)
  
  checks :: (Tele,Env) -> [Ter] -> Typing ()
  checks ([],_)         []     = return ()
  checks ((x,a):xas,nu) (e:es) = do
    va <- evalTC nu a
    check va e
    v' <- evalTyping e
    checks (xas,upd (x,v') nu) es
  checks _ _ = throwError "checks: incorrect number of arguments"
  
  -- infer the type of e
  infer :: Ter -> Typing Val
  infer e = case e of
    U           -> return VU  -- U : U
    Var n       -> do
      rho <- asks env
      lift $ lift $ lookType n rho
    App t u -> do
      c <- infer t
      case c of
        VPi a f -> do
          check a u
          v <- evalTyping u
          appTC f v
        _       -> throwError $ show c ++ " is not a product"
    Fst t -> do
      c <- infer t
      case c of
        VSigma a f -> return a
        _          -> throwError $ show c ++ " is not a sigma-type"
    Snd t -> do
      c <- infer t
      case c of
        VSigma a f -> do
          v <- evalTyping t
          appTC f (fstVal v)
        _          -> throwError $ show c ++ " is not a sigma-type"
    Where t d -> do
      checkDecls d
      local (addDecls d) $ infer t
    Vproj r o a b e -> do
      check VU (V r a b e)
      v <- evalTyping (V r a b e)
      check v o
      evalTyping b
    -- UnGlueElem e a ts -> do
    --   check VU (Glue a ts)
    --   vgl <- evalTyping (Glue a ts)
    --   check vgl e
    --   va <- evalTyping a
    --   return va
    AppII e r -> do
      checkII r
      t <- infer e
      case t of
        VPathP a _ _ -> a @@@ r
        VLineP a -> a @@@ r
        _ -> throwError (show e ++ " is not a path")
    HCom r s a us u0 -> do
      checkII r
      checkII s
      check VU a
      va <- evalTyping a
      check va u0
      -- check that it's a system
      checkPLamSystem r u0 (constPath va) us
      return va
    Com r s a us u0 -> do
      checkII r
      checkII s
      checkPLam (constPath VU) a
      va <- evalTyping a
      var <- va @@@ r
      check var u0
      checkPLamSystem r u0 va us
      va @@@ s
    Coe r s a u -> do
      checkII r
      checkII s
      checkPLam (constPath VU) a
      va <- evalTyping a
      var <- va @@@ r
      check var u
      va @@@ s
    PCon c a es phis -> do
      check VU a
      va <- evalTyping a
      (bs,nu) <- getLblType c va
      checks (bs,nu) es
      mapM_ checkII phis
      return va
    _ -> throwError ("infer " ++ show e)
  
  -- Not used since we have U : U
  --
  -- (=?=) :: Typing Ter -> Ter -> Typing ()
  -- m =?= s2 = do
  --   s1 <- m
  --   unless (s1 == s2) $ throwError (show s1 ++ " =/= " ++ show s2)
  --
  -- checkTs :: [(String,Ter)] -> Typing ()
  -- checkTs [] = return ()
  -- checkTs ((x,a):xas) = do
  --   checkType a
  --   local (addType (x,a)) (checkTs xas)
  --
  -- checkType :: Ter -> Typing ()
  -- checkType t = case t of
  --   U              -> return ()
  --   Pi a (Lam x b) -> do
  --     checkType a
  --     local (addType (x,a)) (checkType b)
  --   _ -> infer t =?= U
  