content: module TypeChecking.Expressions
      ( typeCheck, typeCheckCtx
      ) where
  
  import Control.Monad
  import Data.Either
  import Data.List
  import Data.Void
  import Data.Bifunctor
  import Data.Bitraversable
  import Data.Traversable(sequenceA)
  
  import Syntax as S
  import Semantics
  import Semantics.Value as V
  import Semantics.Pattern as P
  import Syntax.ErrorDoc
  import TypeChecking.Monad
  import TypeChecking.Context as C
  import TypeChecking.Expressions.Utils
  import TypeChecking.Expressions.Patterns
  import TypeChecking.Expressions.Conditions
  import TypeChecking.Expressions.Coverage
  import Normalization
  
  type Context = Ctx String (Type Semantics) Void
  
  intType :: Type Semantics a
  intType = Type interval (TypeK NoLevel)
  
  pathExp :: Sort -> Semantics
  pathExp k = Semantics (Name Prefix $ Ident "Path") (Path k)
  
  pathImp :: Sort -> Semantics
  pathImp k = Semantics PathImp (Path k)
  
  sortPred :: Sort -> Sort
  sortPred Prop = Contr
  sortPred Set{} = Prop
  sortPred k = k
  
  prettyOpen' :: Ctx String (Type Semantics) Void a -> Term Semantics (Either k a) -> EDoc (Term Syntax)
  prettyOpen' ctx term = epretty $ fmap (pretty . either id absurd) $ close ctx $
      first syntax term >>= fmap Right . either (const $ capply $ Name Prefix $ Ident "?") return
  
  typeCheck :: Monad m => Term (Posn, Syntax) Void -> Maybe (Type Semantics Void) -> TCM m (Term Semantics Void, Type Semantics Void)
  typeCheck = typeCheckCtx C.Nil
  
  typeCheckCtx :: (Monad m, Eq a) => Context a -> Term (Posn, Syntax) Void
      -> Maybe (Type Semantics a) -> TCM m (Term Semantics a, Type Semantics a)
  typeCheckCtx ctx term mty = do
      (te, ty, _) <- typeCheckCtx' ctx term $ fmap (\(Type t k) -> Type (fmap Right t) k) mty
      return (te, ty)
  
  typeCheckCtx' :: (Monad m, Eq a) => Context a -> Term (Posn, Syntax) Void -> Maybe (Type Semantics (Either Argument a))
      -> TCM m (Term Semantics a, Type Semantics a, [(Argument, Term Semantics a)])
  typeCheckCtx' ctx (Apply (pos, Name ft var) ts) mty = typeCheckName ctx pos ft var ts mty
  typeCheckCtx' ctx (Apply (_, S.Lam []) [te]) mty = typeCheckCtx' ctx te mty
  typeCheckCtx' ctx (Apply (pos, S.Lam (v:vs)) [te]) (Just (Type (Apply p@(Semantics (S.Pi e _) (V.Pi k1 k2)) [a,b]) k3)) =
      case bitraverse Right id a of
          Left{} -> throwError [inferErrorMsg pos "the argument"]
          Right a' -> do
              (te', Type b' k2', tab) <- typeCheckCtx' (Snoc ctx v $ Type a' k1) (Apply (pos, S.Lam vs) [te]) $
                  Just $ Type (nf WHNF $ fmap sequenceA $ snd $ dropOnePi p a b) k2
              let te'' = case te' of
                      Apply (Semantics (S.Lam vs') _) [t] -> Apply (Semantics (S.Lam $ v:vs') V.Lam) [Lambda t]
                      _                                   -> Apply (Semantics (S.Lam [v]) V.Lam) [Lambda te']
                  tab' = tab >>= \(kp, term) -> case sequenceA term of
                                                      Bound -> []
                                                      Free t -> [(kp, t)]
              return (te'', Type (Apply (Semantics (S.Pi e [v]) $ V.Pi k1 k2') [a', Lambda b']) k3, tab')
  typeCheckCtx' ctx (Apply (pos, S.Lam{}) [_]) (Just (Type (Var Left{} _) _)) =
      throwError [inferErrorMsg pos "lambda expressions"]
  typeCheckCtx' ctx (Apply (pos, S.Lam{}) [_]) (Just (Type ty _)) =
      throwError [Error TypeMismatch $ emsgLC pos "" $ pretty "Expected type:" <+> prettyOpen' ctx ty
                                                    $$ pretty "But lambda expression has pi type"]
  typeCheckCtx' ctx (Apply (pos, S.Lam{}) _) _ = throwError [inferErrorMsg pos "the argument"]
  typeCheckCtx' ctx (Apply (pos, S.Pi e vs) (a:b:ts)) Nothing = do
      (a', Type ty1 _) <- typeCheckCtx ctx a Nothing
      k1 <- checkIsType ctx (termPos a) ty1
      (b', k2) <- extend ctx vs (Type a' k1)
      unless (null ts) $ warn [argsErrorMsg pos "A type"]
      let k = case (k1, k2) of
                  (_, Contr) -> Contr
                  (_, Prop) -> Prop
                  (Set l1, Set l2) -> Set (max l1 l2)
                  (TypeK l1, Set l2) -> Set (max l1 l2)
                  (_, Set l) -> Set l
                  (Set l1, TypeK l2) -> TypeK (max l1 l2)
                  (TypeK l1, TypeK l2) -> TypeK (max l1 l2)
                  (_, TypeK l) -> TypeK l
      return (Apply (Semantics (S.Pi e vs) (V.Pi k1 k2)) [a', b'], Type (universe k) $ succ k, [])
    where
      extend :: (Monad m, Eq a) => Context a -> [String] -> Type Semantics a -> TCM m (Term Semantics a, Sort)
      extend ctx [] _ = do
          (te, Type ty _) <- typeCheckCtx ctx b Nothing
          k <- checkIsType ctx (termPos b) ty
          return (te, k)
      extend ctx (v:vs) a = do
          (te, k) <- extend (Snoc ctx v a) vs (fmap Free a)
          return (Lambda te, k)
  typeCheckCtx' ctx (Apply (pos, PathImp) (a1:a2:ts)) Nothing = do
      unless (null ts) $ warn [argsErrorMsg pos "A type"]
      (r1, Type t1 k) <- typeCheckCtx ctx a1 Nothing
      (r2, _) <- typeCheckCtx ctx a2 $ Just $ Type (nf WHNF t1) k
      return (Apply (pathImp k) [Apply (Semantics (S.Lam ["_"]) V.Lam)
              [Lambda $ fmap Free t1], r1, r2], Type (universe $ sortPred k) $ succ $ sortPred k, [])
  typeCheckCtx' ctx (Apply (pos, S.At) (b:c:ts)) mty = do
      (r1, Type t1 k) <- typeCheckCtx ctx b Nothing
      (r2, _, tab1) <- typeCheckCtx' ctx c (Just intType)
      case nf WHNF t1 of
          Apply (Semantics _ Path{}) [a,b',c'] -> do
              (tes, ty, tab2) <- typeCheckApps pos (Just $ Operator "@") ctx ts (Type (apps a [r2]) k) mty
              return (Apply (Semantics S.At V.At) (b':c':r1:r2:tes), ty, tab1 ++ tab2)
          t1' -> throwError [Error TypeMismatch $ emsgLC pos "" $ pretty "Expected type: Path"
                                                               $$ pretty "Actual type:" <+> prettyOpen ctx t1']
  typeCheckCtx' ctx (Apply (pos, (S.Case (pat:pats))) (expr:terms)) mty = do
      (exprTerm, exprType) <- typeCheckCtx ctx expr Nothing
      let (term1:terms1,terms2) = splitAt (length pats + 1) terms
          typeCheckClause mtype (pat,term) = do
              (bf, TermInCtx ctx' pat' _) <- typeCheckPattern ctx exprType pat
              when bf $ warn [Error Other $ emsgLC (termPos pat) "Absurd patterns are not allowed in case constructions" enull]
              (te, Type ty k, tab) <- typeCheckCtx' (ctx C.+++ ctx') term $ fmap (fmap $ fmap $ liftBase ctx') mtype
              let tab' = tab >>= \(kp, t) -> case sequenceA $ fmap (toBase ctx') t of
                                              Nothing -> []
                                              Just t' -> [(kp, t')]
              return (P.Clause (Cons pat' P.Nil) te, Type (abstractTerm ctx' ty) k, tab')
      (clause, Type type1 k, tab1) <- typeCheckClause (if null terms2 then mty else Nothing) (pat,term1)
      type1' <- case isStationary type1 of
                  Nothing -> throwError [Error Other $
                      emsgLC pos "Type of expressions in case constructions cannot be dependent" enull]
                  Just r  -> return (Type r k)
      clauses <- mapM (liftM (\(p,_,_) -> p) . typeCheckClause (Just $ nfType WHNF $ fmap Right type1')) (zip pats terms1)
      (terms2', ty, tab2) <- if null terms2
          then return ([], type1', [])
          else typeCheckApps pos Nothing ctx terms2 type1' mty
      let clauseToSyntax (P.Clause pats _) p = bimap (\nm -> (termPos p, nm)) id $ head (patternsToTermsSyntax pats)
          cs = clause:clauses
          sem = Semantics (S.Case $ zipWith clauseToSyntax cs (pat:pats)) $ V.Case $ map (head . fst . clauseToEval) cs
          terms' = map (snd . clauseToEval) cs
          clauses' = zipWith (\p1 p2 -> (termPos p1, p2)) (pat:pats) cs
      warn $ coverageErrorMsg pos (checkCoverage clauses')
      warn $ checkConditions ctx (Lambda $ Apply sem $ bvar : map (fmap Free) terms') clauses'
      return (Apply sem $ exprTerm : terms' ++ terms2', ty, tab1 ++ tab2)
    where
      isStationary :: Term a b -> Maybe (Term a b)
      isStationary (Lambda t) = case sequenceA t of
          Bound -> Nothing
          Free t' -> isStationary t'
      isStationary t = Just t
  typeCheckCtx' ctx (Apply (pos, (S.FieldAcc _ pid@(PIdent fPos fName))) (expr:exprs)) mty = do
      (exprTerm, Type exprType _) <- typeCheckCtx ctx expr Nothing
      case nf WHNF exprType of
          Apply (Semantics _ (DataType dtID _)) params -> do
              mfInd <- lift (getField fName dtID)
              case mfInd of
                  Nothing -> throwError [notInScope fPos "record field" fName]
                  Just (fInd, conds, Closed (Type fType k)) -> do
                      fs <- lift (getFields dtID)
                      let lparams = length params
                          lfs = length fs
                          syn = S.FieldAcc lparams pid
                          fields = zipWith (\(_,e,_) i -> Apply (Semantics syn $ V.FieldAcc i lfs lparams e) $ exprTerm:params) fs [0..]
                      (terms, ty, tab) <- typeCheckApps pos Nothing ctx exprs (Type (apps fType $ params ++ fields) k) mty
                      return (Apply (Semantics syn $ V.FieldAcc fInd lfs lparams conds) (exprTerm : params ++ terms), ty, tab)
          _ -> throwError [Error TypeMismatch $ emsgLC pos "" $ pretty "Expected a record type"
                                                             $$ pretty "Actual type:" <+> prettyOpen ctx exprType]
  typeCheckCtx' ctx te (Just (Type ty _)) = do
      (te', Type ty' k') <- typeCheckCtx ctx te Nothing
      tab <- actExpType True ctx (fmap Right ty') ty (termPos te) (Just te')
      return (te', Type ty' k', tab)
  typeCheckCtx' _ _ _ = error "typeCheckCtx"
  
  typeCheckName :: (Monad m, Eq a) => Context a -> Posn -> Fixity -> Name -> [Term (Posn, Syntax) Void]
      -> Maybe (Type Semantics (Either Argument a)) -> TCM m (Term Semantics a, Type Semantics a, [(Argument, Term Semantics a)])
  typeCheckName ctx pos ft var ts mty = do
      when (nameToString var == "_") $ throwError [inferExprErrorMsg pos]
      eres <- case lookupCtx (nameToString var) ctx of
          Just (te,ty) -> return $ Left (te, [], [], ty)
          Nothing -> do
              let mdt = mty >>= \(Type ty _) -> dropPis ty
              mt <- lift $ getEntry var $ mdt >>= either (const Nothing) Just
              cons <- lift (getConstructor var Nothing)
              let cons' = map (\(c,_,_,_,_) -> c) cons
              case (mdt, cons', mt) of
                  (Just (Left wty), _:_, _) -> throwError [Error TypeMismatch $ emsgLC pos ""
                                                   $ pretty "Expected type:" <+> prettyOpen' ctx wty
                                                  $$ pretty ("But " ++ nameToPrefix var ++ " is a data type constructor")]
                  (Just (Right (dtID, _)), c:cs, []) -> do
                      dt <- lift (getDataTypeByID dtID)
                      throwError [Error TypeMismatch $ emsgLC pos ""
                           $ pretty ("Expected data type: " ++ nameToPrefix dt)
                          $$ if null cs
                              then pretty $ "Actual data type: " ++ nameToPrefix c
                              else pretty $ "Posible data types: " ++ intercalate ", " (map nameToPrefix cons')]
                  (_, _, []) -> liftM Right (typeCheckKeyword ctx pos (nameToString var) ts mty)
                  (_, _, [(te, conds, ty)]) ->
                      let te' = case te of
                                  Apply (Semantics (Constr k _) sem) ts -> Apply (Semantics (Constr k $ Name ft var) sem) ts
                                  Apply (Semantics _ sem) ts -> Apply (Semantics (Name ft var) sem) ts
                                  _ -> te
                      in case (sequenceA te', sequenceA ty) of
                          (Left kp, _) -> throwError (inferArgErrorMsg kp)
                          (_, Left kp) -> throwError (inferArgErrorMsg kp)
                          (Right te'', Right (Type Lambda{} _)) -> throwError [inferParamsErrorMsg pos $ nameToPrefix var]
                          (Right te'', Right ty') -> return $ Left (te'', conds, maybe [] (either (const []) snd) mdt, ty')
                  _ -> throwError [Error Other $ emsgLC pos ("Ambiguous identifier: " ++ show (nameToString var)) enull]
      case eres of
          Left (te, conds, params, ty) -> do
              (tes, ty', tab) <- typeCheckApps pos (Just var) ctx ts ty mty
              let lconds = length conds
                  msg = "Expected " ++ show lconds ++ " arguments to " ++ nameToPrefix var
              when (length tes < lconds) $ warn [Error Conditions $ emsgLC pos msg enull]
              when (lconds > 0) $
                  let (lefts,params') = partitionEithers (map sequenceA params)
                  in case lefts of
                      [] -> forM_ (zip tes conds) $ \(term,cs) -> forM_ cs $ \(ClauseInCtx ctx' cl) ->
                          case clauseToClauseEq $ instantiateClause ctx' (params' ++ tes) cl of
                              P.ClauseEq pats rhs ->
                                  let (ctx1,args1) = patsToTerms pats
                                      term' = apps (fmap (liftBase ctx1) term) args1
                                      actTerm = nf NF term'
                                      expTerm = nf NF rhs
                                  in unless (expTerm == actTerm) $
                                      warn [conditionsErrorMsg pos (ctx C.+++ ctx1) ([], term', actTerm, expTerm)]
                      _ -> warn (lefts >>= inferArgErrorMsg)
              return (apps te tes, ty', tab)
          Right res -> return res
    where
      dropPis :: Eq a => Term Semantics a -> Maybe (Either (Term Semantics a) (ID, [Term Semantics a]))
      dropPis (Apply (Semantics (S.Pi _ []) _) [_,t]) = dropPis (nf WHNF t)
      dropPis (Apply (Semantics (S.Pi _ (v:vs)) _) [_, Lambda t]) = case dropPis (nf WHNF t) of
          Just (Right (dtID, params)) -> Just $ Right (dtID, case sequenceA $ map sequenceA params of
                                                              Free params' -> params'
                                                              _            -> [])
          Just (Left t) -> Just $ Left $ t >>= \u -> case u of
                                                      Bound  -> capply $ Semantics (Name Prefix $ Ident v) (error "dropPis")
                                                      Free a -> return a
          Nothing -> Nothing
      dropPis (Apply (Semantics _ (DataType dtID _)) params) = Just $ Right (dtID, params)
      dropPis t@(Apply (Semantics _ v) _) | isInj v = Just (Left t)
      dropPis _ = Nothing
  
  typeCheckKeyword :: (Monad m, Eq a) => Context a -> Posn -> String -> [Term (Posn, Syntax) Void]
      -> Maybe (Type Semantics (Either Argument a)) -> TCM m (Term Semantics a, Type Semantics a, [(Argument, Term Semantics a)])
  typeCheckKeyword _ pos u as Nothing | (k,""):_ <- reads u = do
      unless (null as) $ warn [argsErrorMsg pos "A type"]
      return (universe k, Type (universe $ succ k) $ succ $ succ k, [])
  typeCheckKeyword ctx pos "contr" [] (Just (Type ty k)) = do
      case k of
          Contr   -> return ()
          _       -> warn [Error TypeMismatch $ emsgLC pos "" $ pretty "Expected a contractible type"
                                                             $$ pretty "Actual type:" <+> prettyOpen' ctx ty]
      case sequenceA ty of
          Left kp -> throwError (inferArgErrorMsg kp)
          Right ty' -> return (capply $ Semantics (Name Prefix $ Ident "contr") CCon, Type ty' k, [])
  typeCheckKeyword _ pos "contr" _ _ = throwError [inferErrorMsg pos "contr"]
  typeCheckKeyword _ pos "I" as Nothing = do
      unless (null as) $ warn [argsErrorMsg pos "A type"]
      return (interval, Type (universe $ TypeK NoLevel) $ TypeK $ Level 1, [])
  typeCheckKeyword _ pos "left" as Nothing = do
      unless (null as) $ warn [argsErrorMsg pos $ show "left"]
      return (iCon ILeft, intType, [])
  typeCheckKeyword _ pos "right" as Nothing = do
      unless (null as) $ warn [argsErrorMsg pos $ show "right"]
      return (iCon IRight, intType, [])
  typeCheckKeyword _ pos "Path" [] _ = throwError [expectedArgErrorMsg pos "Path"]
  typeCheckKeyword ctx pos "Path" (a:as) Nothing = do
      (r1, _, (v, t1)) <- typeCheckLambda ctx a intType
      k <- checkIsType (Snoc ctx v $ error "") (termPos a) t1
      let r1' c = apps r1 [iCon c]
          k' = sortPred k
          mkType t = Type t (succ k')
      case as of
          [] -> return (Apply (pathExp k) [r1], mkType $ Apply (Semantics (S.Pi Explicit []) $ V.Pi k $ succ k)
              [r1' ILeft, Apply (Semantics (S.Pi Explicit []) $ V.Pi k $ succ k) [r1' IRight, universe k']], [])
          [a2] -> do
              (r2, _) <- typeCheckCtx ctx a2 $ Just $ Type (nf WHNF $ r1' ILeft) k
              return (Apply (pathExp k) [r1,r2], mkType $ Apply (Semantics (S.Pi Explicit []) $ V.Pi k $ succ k) [r1' IRight, universe k'], [])
          a2:a3:as' -> do
              unless (null as') $ warn [argsErrorMsg pos "A type"]
              (r2, _) <- typeCheckCtx ctx a2 $ Just $ Type (nf WHNF $ r1' ILeft) k
              (r3, _) <- typeCheckCtx ctx a3 $ Just $ Type (nf WHNF $ r1' IRight) k
              return (Apply (pathExp k) [r1,r2,r3], mkType $ universe k', [])
  typeCheckKeyword _ pos "path" [] _ = throwError [expectedArgErrorMsg pos "path"]
  typeCheckKeyword ctx pos "path" (a:as) mty = do
      unless (null as) $ warn [argsErrorMsg pos "A path"]
      case mty of
          Nothing -> do
              (te, Type _ k, (_, ty)) <- typeCheckLambda ctx a intType
              return (path [te], Type (Apply (pathImp k) [Apply (Semantics (S.Lam ["_"]) V.Lam) [Lambda ty], apps te [iCon ILeft], apps te [iCon IRight]]) k, [])
          Just (Type (Var (Left kp) _) _) -> do
              (te, Type _ k, (_, ty)) <- typeCheckLambda ctx a intType
              let ty' = Apply (pathImp k) [Apply (Semantics (S.Lam ["_"]) V.Lam) [Lambda ty], apps te [iCon ILeft], apps te [iCon IRight]]
              return (path [te], Type ty' k, [(kp,ty')])
          Just (Type ety@(Apply (Semantics _ (Path k1)) [t1,_,_]) k) -> do
              let sem = Semantics (S.Pi Explicit ["i"]) $ V.Pi (TypeK NoLevel) k1
                  aty = Apply sem [interval, Lambda $ apps (fmap Free t1) [bvar]]
              (r, Type ty' _, tab1) <- typeCheckCtx' ctx a $ Just (Type aty k1)
              case nf WHNF ty' of
                  Apply (Semantics (S.Pi e vs) p) [ta, tb] -> do
                      let tb' = case tb of
                                  Lambda t@Lambda{} -> Apply (Semantics (S.Lam ["i"]) V.Lam)
                                      [Lambda $ Apply (Semantics (S.Pi e $ tail vs) p) [fmap Free ta, t]]
                                  Lambda{} -> Apply (Semantics (S.Lam ["i"]) V.Lam) [tb]
                                  _ -> Apply (Semantics (S.Lam ["_"]) V.Lam) [Lambda $ fmap Free tb]
                          aty = Apply (pathImp k1) [tb', apps r [iCon ILeft], apps r [iCon IRight]]
                          res = path [r]
                      tab2 <- actExpType True ctx (fmap Right aty) ety pos (Just res)
                      return (res, Type aty k, tab1 ++ tab2)
                  _ -> error "typeCheckKeyword: path"
          Just (Type ty _) -> throwError [Error TypeMismatch $ emsgLC pos "" $ pretty "Expected type:" <+> prettyOpen' ctx ty
                                                                            $$ pretty "Actual type: Path"]
  typeCheckKeyword _ pos "coe" [] _ = throwError [expectedArgErrorMsg pos "coe"]
  typeCheckKeyword ctx pos "coe" (a1:as) Nothing = do
      (r1, _, (v, t1)) <- typeCheckLambda ctx a1 intType
      k <- checkIsType (Snoc ctx v $ error "") (termPos a1) t1
      let res = Apply (Semantics (S.Pi Explicit ["r"]) $ V.Pi (TypeK NoLevel) k) [interval, Lambda $ apps (fmap Free r1) [bvar]]
          coe = Semantics (Name Prefix $ Ident "coe") Coe
      case as of
          [] -> return (Apply coe [r1], Type (Apply (Semantics (S.Pi Explicit ["l"]) $ V.Pi (TypeK NoLevel) k) [interval, Lambda $
              Apply (Semantics (S.Pi Explicit []) $ V.Pi k k) [apps (fmap Free r1) [bvar], fmap Free res]]) k, [])
          a2:as1 -> do
              (r2, _, tab2) <- typeCheckCtx' ctx a2 (Just intType)
              case as1 of
                  [] -> return (Apply coe [r1,r2], Type (Apply (Semantics (S.Pi Explicit []) $ V.Pi k k) [apps r1 [r2], res]) k, [])
                  a3:as2 -> do
                      (r3, _) <- typeCheckCtx ctx a3 $ Just $ Type (nf WHNF $ apps r1 [r2]) k
                      case as2 of
                          [] -> return (Apply coe [r1,r2,r3], Type res k, [])
                          a4:as3 -> do
                              (r4, _, tab4) <- typeCheckCtx' ctx a4 (Just intType)
                              (tes, ty, _) <- typeCheckApps pos Nothing ctx as3 (Type (apps r1 [r4]) k) Nothing
                              return (Apply coe $ [r1,r2,r3,r4] ++ tes, ty, tab2 ++ tab4)
  typeCheckKeyword ctx pos "iso" (a1:a2:a3:a4:a5:a6:as) Nothing = do
      (r1, Type t1 _) <- typeCheckCtx ctx a1 Nothing
      (r2, Type t2 _) <- typeCheckCtx ctx a2 Nothing
      let t1' = nf WHNF t1
          t2' = nf WHNF t2
      k1 <- checkIsType ctx (termPos a1) t1'
      k2 <- checkIsType ctx (termPos a2) t2'
      let k = dmax k1 k2
      (r3, _) <- typeCheckCtx ctx a3 $ Just $ Type (Apply (Semantics (S.Pi Explicit []) $ V.Pi k1 k2) [r1,r2]) k
      (r4, _) <- typeCheckCtx ctx a4 $ Just $ Type (Apply (Semantics (S.Pi Explicit []) $ V.Pi k2 k1) [r2,r1]) k
      let h e s1 s3 s4 tk = typeCheckCtx ctx e $ Just $ Type (Apply (Semantics (S.Pi Explicit ["x"]) $ V.Pi tk tk) [s1, Lambda $
              Apply (pathImp tk) [Apply (Semantics (S.Lam ["_"]) V.Lam) [Lambda $ fmap (Free . Free) s1],
                  apps (fmap Free s4) [apps (fmap Free s3) [bvar]], bvar]]) tk
          iso = Semantics (Name Prefix $ Ident "iso") Iso
      (r5, _) <- h a5 r1 r3 r4 k1
      (r6, _) <- h a6 r2 r4 r3 k2
      case as of
          [] -> return (Apply iso [r1,r2,r3,r4,r5,r6],
              Type (Apply (Semantics (S.Pi Explicit []) $ V.Pi (TypeK NoLevel) $ succ k) [interval, universe k]) $ succ k, [])
          a7:as' -> do
              unless (null as') $ warn [argsErrorMsg pos "A type"]
              (r7, _, tab7) <- typeCheckCtx' ctx a7 (Just intType)
              return (Apply iso [r1,r2,r3,r4,r5,r6,r7], Type (universe k) $ succ k, tab7)
  typeCheckKeyword _ pos "iso" _ Nothing =
      throwError [Error NotEnoughArgs $ emsgLC pos "Expected at least 6 arguments to \"iso\"" enull]
  typeCheckKeyword ctx pos "squeeze" as Nothing =
      let mkType t = Apply (Semantics (S.Pi Explicit []) $ V.Pi (TypeK NoLevel) $ TypeK NoLevel) [interval, t]
          squeeze = Semantics (Name Prefix $ Ident "squeeze") Squeeze
      in case as of
          [] -> return (capply squeeze, Type (mkType $ mkType interval) $ TypeK NoLevel, [])
          [a1] -> do
              (r1, _, tab) <- typeCheckCtx' ctx a1 (Just intType)
              return (Apply squeeze [r1], Type (mkType interval) $ TypeK NoLevel, tab)
          [a1,a2] -> do
              (r1, _, tab1) <- typeCheckCtx' ctx a1 (Just intType)
              (r2, _, tab2) <- typeCheckCtx' ctx a2 (Just intType)
              return (Apply squeeze [r1,r2], intType, tab1 ++ tab2)
          _ -> throwError [argsErrorMsg pos "squeeze _ _"]
  typeCheckKeyword ctx pos var ts (Just (Type ty _)) = do
      (te', Type ty' k', _) <- typeCheckKeyword ctx pos var ts Nothing
      tab <- actExpType True ctx (fmap Right ty') ty pos (Just te')
      return (te', Type ty' k', tab)
  typeCheckKeyword _ pos var _ _ = throwError [notInScope pos "" var]
  
  actExpType :: (Monad m, Eq a) => Bool -> Context a -> Term Semantics (Either Argument a)
      -> Term Semantics (Either Argument a) -> Posn -> Maybe (Term Semantics a) -> EDocM m [(Argument, Term Semantics a)]
  actExpType w ctx act exp pos mterm = do
      let act' = nf NF act
          exp' = nf NF exp
          (mo,(l1,l2)) = pcmpTerms act' exp'
          l = if w then l2 else l1
      unless (mo == Just EQ || mo == Just LT) $
          throwError [Error TypeMismatch $ emsgLC pos "" $ pretty "Expected type:" <+> prettyOpen' ctx exp'
                                                        $$ pretty "Actual type:  " <+> prettyOpen' ctx act'
                                                        $$ maybe enull (\t -> pretty "Term:" <+> prettyOpen ctx t) mterm]
      return l
  
  typeCheckApps :: (Monad m, Eq a) => Posn -> Maybe Name -> Context a -> [Term (Posn, Syntax) Void]
      -> Type Semantics a -> Maybe (Type Semantics (Either Argument a))
      -> TCM m ([Term Semantics a], Type Semantics a, [(Argument, Term Semantics a)])
  typeCheckApps pos mname ctx allTerms ty mety = go 0 [] [] (map (\t -> (Explicit, Left t)) allTerms) nty
    where
      nty = nfType WHNF (fmap Right ty)
      mterm terms = fmap (\name -> Apply (Semantics (Name Prefix name) $ error "") terms) mname
      dropAndInstantiate t (Semantics (S.Pi _ [_]) _) a (Lambda b) = instantiate1 t b
      dropAndInstantiate t (Semantics (S.Pi e (_:vs)) s) a (Lambda b) = Apply (Semantics (S.Pi e vs) s) [a, instantiate1 t b]
      dropAndInstantiate _ _ _ b = b
      
      go n acc rest ((e1, term@(Left (Apply (pos', Name _ (Ident "_")) []))) : terms) (Type (Apply p@(Semantics (S.Pi e2 _) (V.Pi _ k2)) [a,b]) _) | e1 == e2 =
          go (n + 1) (Left (inferArgErrorMsg $ Argument n pos' mname) : acc) ((e1,term):rest) terms $
          Type (nf WHNF $ dropAndInstantiate (cvar $ Left (Argument n pos' mname)) p a b) k2
      go n acc rest ((e1,term):terms) (Type (Apply p@(Semantics (S.Pi e2 _) (V.Pi k1 k2)) [a,b]) _) | e1 == e2 = do
          mres <- case term of
                      Left t -> let catchErrs = catchErrorType [Inference]
                                in liftM (\(a,b,c) -> Right ((termPos t, a), Just b, c))
                                  (typeCheckCtx' ctx t $ Just $ Type (nf WHNF a) k1) `catchErrs` (return . Left)
                      Right (pte, maty) -> do
                          tab <- case maty of
                                  Just (Type aty _) -> actExpType True ctx (fmap Right aty) a (fst pte) $ Just (snd pte)
                                  Nothing -> return []
                          return $ Right (pte, maty, tab)
          case mres of
              Left errs -> go (n + 1) (Left errs : acc) ((e1,term):rest) terms $
                  Type (nf WHNF $ dropAndInstantiate (cvar $ Left $ NoArgument n errs) p a b) k2
              Right (pterm', mty, tab) ->
                  let ty' = Right (pterm', mty)
                  in if useful tab
                      then go 0 [] [] (replaceTerms (reverse rest ++ [(e1, ty')] ++ terms) tab) nty
                      else go (n + 1) (ty' : acc) ((e1, ty') : rest) terms $
                          Type (nf WHNF $ dropAndInstantiate (fmap Right $ snd pterm') p a b) k2
      go n acc rest terms (Type (Apply p@(Semantics (S.Pi Implicit _) (V.Pi _ k2)) [a,b]) _) =
          go (n + 1) (Left (inferArgErrorMsg $ Argument n pos mname) : acc)
              ((Implicit, Left (capply (pos, Name Prefix $ Ident "_"))) : rest) terms $
              Type (nf WHNF $ dropAndInstantiate (cvar $ Left (Argument n pos mname)) p a b) k2
      go n acc rest [] (Type aty k) =
          let checkAty = case sequenceA aty of
                          Left kp -> throwError (inferArgErrorMsg kp)
                          Right aty' -> case partitionEithers (reverse acc) of
                                          ([], rights) -> return (map (snd . fst) rights, Type aty' k, [])
                                          (lefts, _)   -> throwError (concat lefts)
          in case mety of
              Just (Type ety _) -> do
                  tab <- actExpType False ctx aty ety pos Nothing
                  if useful tab
                  then go 0 [] [] (replaceTerms (reverse rest) tab) nty
                  else do
                      (acc', Type aty' k', _) <- checkAty
                      tab' <- actExpType True ctx (fmap Right aty') ety pos (mterm acc')
                      return (acc', Type aty' k', tab')
              Nothing -> checkAty
      go _ _ _ _ (Type (Var (Left kp) _) _) = throwError (inferArgErrorMsg kp)
      go _ _ _ _ (Type ty _) = throwError [Error TypeMismatch $ emsgLC pos ""
           $ pretty "Expected pi type"
          $$ pretty "Actual type:" <+> prettyOpen' ctx ty]
      
      replaceTerms :: [(e, Either (Term (Posn, Syntax) Void) ((Posn, s), Maybe u))]
          -> [(Argument, s)] -> [(e, Either (Term (Posn, Syntax) Void) ((Posn, s), Maybe u))]
      replaceTerms ts [] = ts
      replaceTerms ts ((arg, t):tab) = case splitAt (argumentIndex arg) (replaceTerms ts tab) of
          (ts1, []) -> ts1
          (ts1, t2:ts2) -> ts1 ++ [(fst t2, Right ((either termPos (fst . fst) (snd t2), t), Nothing))] ++ ts2
      
      useful :: [(Argument,a)] -> Bool
      useful = not . null
  
  typeCheckLambda :: (Monad m, Eq a) => Context a -> Term (Posn, Syntax) Void -> Type Semantics a
      -> TCM m (Term Semantics a, Type Semantics a, (String, Term Semantics (Scoped a)))
  typeCheckLambda ctx (Apply (pos, S.Lam (v:vs)) [te]) (Type ty k) = do
      (te', Type ty' k') <- typeCheckCtx (Snoc ctx v $ Type ty k) (if null vs then te else Apply (pos, S.Lam vs) [te]) Nothing
      let te'' = case te' of
                  Apply (Semantics (S.Lam vs') _) [te''] -> Apply (Semantics (S.Lam $ v:vs') V.Lam) [Lambda te'']
                  _ -> Apply (Semantics (S.Lam [v]) V.Lam) [Lambda te']
      return (te'', Type (Apply (Semantics (S.Pi Explicit [v]) (V.Pi k k')) [ty, Lambda ty']) $ dmax k k', (v, ty'))
  typeCheckLambda ctx te ty = do
      (te', Type ty' k') <- typeCheckCtx ctx te Nothing
      case nf WHNF ty' of
          ty''@(Apply p@(Semantics sp (V.Pi ka kb)) [a,b]) ->
              let na = nf NF a
                  Type nty kty = nfType NF ty
              in if (nty `lessOrEqual` na)
                  then return (te', Type ty'' k', dropOnePi p a b)
                  else throwError [Error TypeMismatch $ emsgLC (termPos te) ""
                           $ pretty "Expected type:" <+> prettyOpen ctx (Apply (Semantics sp $ V.Pi kty kb) [nty,b])
                          $$ pretty "Actual type:  " <+> prettyOpen ctx (Apply p [na,b])
                          $$ pretty "Term:" <+> prettyOpen ctx te']
          _ -> throwError [Error TypeMismatch $ emsgLC (termPos te) "" $ pretty "Expected pi type"
                                                                      $$ pretty "Actual type:" <+> prettyOpen ctx ty'
                                                                      $$ pretty "Term:" <+> prettyOpen ctx te']
  