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']