{-# LANGUAGE CPP, PatternGuards #-}

module Agda.TypeChecking.Rules.Term where

import Control.Applicative
import Control.Monad.Trans
import Control.Monad.Reader
import Control.Monad.Error
import Data.Maybe
import Data.List hiding (sort)
import qualified Agda.Utils.IO.Locale as LocIO
import qualified Data.Map as Map
import qualified Data.Set as Set

import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Abstract.Views as A
import qualified Agda.Syntax.Info as A
import Agda.Syntax.Common
import Agda.Syntax.Fixity
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Generic
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Abstract.Views

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Free

import Agda.Utils.Fresh
import Agda.Utils.Tuple
import Agda.Utils.Permutation

import {-# SOURCE #-} Agda.TypeChecking.Empty (isEmptyTypeC)
import {-# SOURCE #-} Agda.TypeChecking.Rules.Decl (checkSectionApplication)
import {-# SOURCE #-} Agda.TypeChecking.Rules.Def (checkFunDef)

import Agda.Utils.Monad
import Agda.Utils.Size

#include "../../undefined.h"
import Agda.Utils.Impossible

---------------------------------------------------------------------------
-- * Types
---------------------------------------------------------------------------

-- | Check that an expression is a type.
isType :: A.Expr -> Sort -> TCM Type
isType e s =
    traceCall (IsTypeCall e s) $ do
    v <- checkExpr e (sort s)
    return $ El s v

-- | Check that an expression is a type without knowing the sort.
isType_ :: A.Expr -> TCM Type
isType_ e =
    traceCall (IsType_ e) $ do
    s <- newSortMeta
    isType e s


-- | Force a type to be a Pi. Instantiates if necessary. The 'Hiding' is only
--   used when instantiating a meta variable.
forcePi :: MonadTCM tcm => Hiding -> String -> Type -> tcm (Type, Constraints)
forcePi h name (El s t) =
    do	t' <- reduce t
	case t' of
	    Pi _ _	-> return (El s t', [])
	    Fun _ _	-> return (El s t', [])
            _           -> do
                sa <- newSortMeta
                sb <- newSortMeta
                let s' = sLub sa sb

                a <- newTypeMeta sa
                x <- freshName_ name
		let arg = Arg h a
                b <- addCtx x arg $ newTypeMeta sb
                let ty = El s' $ Pi arg (Abs (show x) b)
                cs <- equalType (El s t') ty
                ty' <- reduce ty
                return (ty', cs)


---------------------------------------------------------------------------
-- * Telescopes
---------------------------------------------------------------------------

-- | Type check a telescope. Binds the variables defined by the telescope.
checkTelescope :: A.Telescope -> (Telescope -> TCM a) -> TCM a
checkTelescope [] ret = ret EmptyTel
checkTelescope (b : tel) ret =
    checkTypedBindings b $ \tel1 ->
    checkTelescope tel   $ \tel2 ->
	ret $ abstract tel1 tel2


-- | Check a typed binding and extends the context with the bound variables.
--   The telescope passed to the continuation is valid in the original context.
checkTypedBindings :: A.TypedBindings -> (Telescope -> TCM a) -> TCM a
checkTypedBindings (A.TypedBindings i h bs) ret =
    thread (checkTypedBinding h) bs $ \bss ->
    ret $ foldr (\(x,t) -> ExtendTel (Arg h t) . Abs x) EmptyTel (concat bss)

checkTypedBinding :: Hiding -> A.TypedBinding -> ([(String,Type)] -> TCM a) -> TCM a
checkTypedBinding h (A.TBind i xs e) ret = do
    t <- isType_ e
    addCtxs xs (Arg h t) $ ret $ mkTel xs t
    where
	mkTel [] t     = []
	mkTel (x:xs) t = (show $ nameConcrete x,t) : mkTel xs (raise 1 t)
checkTypedBinding h (A.TNoBind e) ret = do
    t <- isType_ e
    ret [("_",t)]


---------------------------------------------------------------------------
-- * Literal
---------------------------------------------------------------------------

checkLiteral :: Literal -> Type -> TCM Term
checkLiteral lit t = do
    t' <- litType lit
    v  <- blockTerm t (Lit lit) $ leqType t' t
    return v

litType :: Literal -> TCM Type
litType l = case l of
    LitLevel _ _  -> el <$> primLevel
    LitInt _ _	  -> el <$> primNat
    LitFloat _ _  -> el <$> primFloat
    LitChar _ _   -> el <$> primChar
    LitString _ _ -> el <$> primString
  where
    el t = El (mkType 0) t

---------------------------------------------------------------------------
-- * Terms
---------------------------------------------------------------------------

-- TODO: move somewhere suitable
reduceCon :: MonadTCM tcm => QName -> tcm QName
reduceCon c = do
  Con c [] <- constructorForm =<< reduce (Con c [])
  return c

checkArguments' exph r args t0 t e k = do
  z <- runErrorT $ checkArguments exph r args t0 t
  case z of
    Right (vs, t1, cs) -> k vs t1 cs
    Left t0 -> do
      let unblock = do
            t0 <- reduceB $ unEl t0
            case t0 of
              Blocked{}          -> return False
              NotBlocked MetaV{} -> return False
              _                  -> return True
      postponeTypeCheckingProblem e t unblock

-- | Type check an expression.
checkExpr :: A.Expr -> Type -> TCM Term
checkExpr e t =
    traceCall (CheckExpr e t) $ localScope $ do
    reportSDoc "tc.term.expr.top" 15 $
        text "Checking" <+> sep
	  [ fsep [ prettyTCM e, text ":", prettyTCM t ]
	  , nest 2 $ text "at " <+> (text . show =<< getCurrentRange)
	  ]
    t <- reduce t
    reportSDoc "tc.term.expr.top" 15 $
        text "    --> " <+> prettyTCM t
    let scopedExpr (A.ScopedExpr scope e) = setScope scope >> scopedExpr e
	scopedExpr e			  = return e

        unScope (A.ScopedExpr scope e) = unScope e
        unScope e                      = e

    e <- scopedExpr e
    case e of

	-- Insert hidden lambda if appropriate
	_   | not (hiddenLambdaOrHole e)
	    , FunV (Arg Hidden _) _ <- funView (unEl t) -> do
		x <- freshName r (argName t)
                reportSLn "tc.term.expr.impl" 15 $ "Inserting implicit lambda"
		checkExpr (A.Lam (A.ExprRange $ getRange e) (A.DomainFree Hidden x) e) t
	    where
		r = case rStart $ getRange e of
                      Nothing  -> noRange
                      Just pos -> posToRange pos pos

                hiddenLambdaOrHole (A.AbsurdLam _ Hidden)                                  = True
		hiddenLambdaOrHole (A.Lam _ (A.DomainFree Hidden _) _)			   = True
		hiddenLambdaOrHole (A.Lam _ (A.DomainFull (A.TypedBindings _ Hidden _)) _) = True
		hiddenLambdaOrHole (A.QuestionMark _)					   = True
		hiddenLambdaOrHole _							   = False

	-- Variable or constant application
	_   | Application (HeadCon cs@(_:_:_)) args <- appView e -> do
                -- First we should figure out which constructor we want.
                reportSLn "tc.check.term" 40 $ "Ambiguous constructor: " ++ show cs

                -- Get the datatypes of the various constructors
                let getData Constructor{conData = d} = d
                    getData _                        = __IMPOSSIBLE__
                reportSLn "tc.check.term" 40 $ "  ranges before: " ++ show (getRange cs)
                cs  <- zipWith setRange (map getRange cs) <$> mapM reduceCon cs
                reportSLn "tc.check.term" 40 $ "  ranges after: " ++ show (getRange cs)
                reportSLn "tc.check.term" 40 $ "  reduced: " ++ show cs
                dcs <- mapM (\c -> (getData /\ const c) . theDef <$> getConstInfo c) cs

                -- Lets look at the target type at this point
                let getCon = do
                      t <- normalise t
                      let TelV _ t1 = telView t
                      t1 <- reduceB $ unEl t1
                      reportSDoc "tc.check.term.con" 40 $ nest 2 $
                        text "target type: " <+> prettyTCM t1
                      case t1 of
                        NotBlocked (Def d _) -> do
                          let dataOrRec = case [ c | (d', c) <- dcs, d == d' ] of
                                c:_ -> return (Just c)
                                []  -> typeError $ DoesNotConstructAnElementOf
                                                     (head cs) (Def d [])
                          defn <- theDef <$> getConstInfo d
                          case defn of
                            Datatype{} -> dataOrRec
                            Record{}   -> dataOrRec
                            _ -> typeError $ DoesNotConstructAnElementOf (head cs) (ignoreBlocking t1)
                        NotBlocked (MetaV _ _)  -> return Nothing
                        Blocked{} -> return Nothing
                        _ -> typeError $ DoesNotConstructAnElementOf (head cs) (ignoreBlocking t1)
                let unblock = isJust <$> getCon
                mc <- getCon
                case mc of
                  Just c  -> checkHeadApplication e t (HeadCon [c]) args
                  Nothing -> postponeTypeCheckingProblem e t unblock

            | Application hd args <- appView e -> checkHeadApplication e t hd args

	A.WithApp _ e es -> typeError $ NotImplemented "type checking of with application"

        A.App i s (Arg NotHidden l)
          | A.Set _ 0 <- unScope s ->
          ifM (not <$> hasUniversePolymorphism)
              (typeError $ GenericError "Use --universe-polymorphism to enable level arguments to Set")
          $ do
            lvl <- primLevel
            suc <- do s <- primLevelSuc
                      return $ \x -> s `apply` [Arg NotHidden x]
            n   <- checkExpr (namedThing l) (El (mkType 0) lvl)
            reportSDoc "tc.univ.poly" 10 $
              text "checking Set " <+> prettyTCM n <+> text "against" <+> prettyTCM t
            blockTerm t (Sort $ Type n) $ leqType (sort $ Type $ suc n) t

	A.App i e arg -> do
	    (v0, t0)	 <- inferExpr e
	    checkArguments' ExpandLast (getRange e) [arg] t0 t e $ \vs t1 cs ->
	      blockTerm t (apply v0 vs) $ (cs ++) <$> leqType t1 t

        A.AbsurdLam i h -> do
          t <- reduceB =<< instantiateFull t
          case t of
            Blocked{}                 -> postponeTypeCheckingProblem_ e $ ignoreBlocking t
            NotBlocked (El _ MetaV{}) -> postponeTypeCheckingProblem_ e $ ignoreBlocking t
            NotBlocked t' -> case funView $ unEl t' of
              FunV (Arg h' a) _
                | h == h' && not (null $ foldTerm metas a) ->
                    postponeTypeCheckingProblem e (ignoreBlocking t) $
                      null . foldTerm metas <$> instantiateFull a
                | h == h' -> do
                  cs' <- isEmptyTypeC a
                  -- Add helper function
                  top <- currentModule
                  let name = "absurd"
                  aux <- qualify top <$> freshName (getRange i) name
                  reportSDoc "tc.term.absurd" 10 $ vcat
                    [ text "Adding absurd function" <+> prettyTCM aux
                    , nest 2 $ text "of type" <+> prettyTCM t'
                    ]
                  addConstant aux $ Defn aux t' (defaultDisplayForm aux) 0
                                  $ Function
                                    { funClauses        =
                                        [Clause { clauseRange = getRange e
                                                , clauseTel   = EmptyTel
                                                , clausePerm  = Perm 0 []
                                                , clausePats  = [Arg h $ VarP "()"]
                                                , clauseBody  = NoBody
                                                }
                                        ]
                                    , funDelayed        = NotDelayed
                                    , funInv            = NotInjective
                                    , funAbstr          = ConcreteDef
                                    , funPolarity       = [Covariant]
                                    , funArgOccurrences = [Unused]
                                    }
                  blockTerm t' (Def aux []) $ return cs'
                | otherwise -> typeError $ WrongHidingInLambda t'
              _ -> typeError $ ShouldBePi t'
          where
            metas (MetaV m _) = [m]
            metas _           = []

	A.Lam i (A.DomainFull b) e -> do
	    (v, cs) <- checkTypedBindings b $ \tel -> do
	        t1 <- newTypeMeta_
                cs <- escapeContext (size tel) $ leqType (telePi tel t1) t
                v <- checkExpr e t1
                return (teleLam tel v, cs)
	    blockTerm t v (return cs)
	    where
		name (Arg h (x,_)) = Arg h x

	A.Lam i (A.DomainFree h x) e0 -> do
	    -- (t',cs) <- forcePi h (show x) t
            t <- reduceB t
            case t of
              Blocked{}                 -> postponeTypeCheckingProblem_ e $ ignoreBlocking t
              NotBlocked (El _ MetaV{}) -> postponeTypeCheckingProblem_ e $ ignoreBlocking t
              NotBlocked t' -> case funView $ unEl t' of
		FunV arg0@(Arg h' a) _
		    | h == h' -> do
			v <- addCtx x arg0 $ do
                              let arg = Arg h (Var 0 [])
                                  tb  = raise 1 t' `piApply` [arg]
                              v <- checkExpr e0 tb
                              return $ Lam h $ Abs (show x) v
			-- blockTerm t v (return cs)
                        return v
		    | otherwise ->
			typeError $ WrongHidingInLambda t'
		_   -> typeError $ ShouldBePi t'

	A.QuestionMark i -> do
	    setScope (A.metaScope i)
	    newQuestionMark  t
	A.Underscore i   -> do
	    setScope (A.metaScope i)
	    newValueMeta t

	A.Lit lit    -> checkLiteral lit t
	A.Let i ds e -> checkLetBindings ds $ checkExpr e t
	A.Pi _ tel e -> do
	    t' <- checkTelescope tel $ \tel -> do
                    t   <- instantiateFull =<< isType_ e
                    tel <- instantiateFull tel
                    return $ telePi_ tel t
            s  <- return $ getSort t'
            when (s == Inf) $ reportSDoc "tc.term.sort" 20 $
              vcat [ text ("reduced to omega:")
                   , nest 2 $ text "t   =" <+> prettyTCM t'
                   , nest 2 $ text "cxt =" <+> (prettyTCM =<< getContextTelescope)
                   ]
	    blockTerm t (unEl t') $ leqType (sort s) t
	A.Fun _ (Arg h a) b -> do
	    a' <- isType_ a
	    b' <- isType_ b
	    let s = getSort a' `sLub` getSort b'
	    blockTerm t (Fun (Arg h a') b') $ leqType (sort s) t
	A.Set _ n    -> do
          n <- ifM typeInType (return 0) (return n)
	  blockTerm t (Sort (mkType n)) $ leqType (sort $ mkType $ n + 1) t
	A.Prop _     -> do
          s <- ifM typeInType (return $ mkType 0) (return Prop)
	  blockTerm t (Sort Prop) $ leqType (sort $ mkType 1) t

	A.Rec _ fs  -> do
	  t <- normalise t
	  case unEl t of
	    Def r vs  -> do
	      (hs, xs) <- unzip <$> getRecordFieldNames r
	      ftel     <- getRecordFieldTypes r
              con      <- getRecordConstructor r
              scope    <- getScope
              let meta = A.Underscore $ A.MetaInfo (getRange e) scope Nothing
	      es   <- orderFields r meta xs fs
	      let tel = ftel `apply` vs
	      (args, cs) <- checkArguments_ ExpandLast (getRange e)
			      (zipWith (\h e -> Arg h (unnamed e)) hs es) tel
	      blockTerm t (Con con args) $ return cs
            MetaV _ _ -> do
              reportSDoc "tc.term.expr.rec" 10 $ sep
                [ text "Postponing type checking of"
                , nest 2 $ prettyA e <+> text ":" <+> prettyTCM t
                ]
              postponeTypeCheckingProblem_ e t
	    _         -> typeError $ ShouldBeRecordType t

	A.Var _    -> __IMPOSSIBLE__
	A.Def _    -> __IMPOSSIBLE__
	A.Con _    -> __IMPOSSIBLE__

        A.ETel _   -> __IMPOSSIBLE__

	A.ScopedExpr scope e -> setScope scope >> checkExpr e t

-- | Infer the type of a head thing (variable, function symbol, or constructor)
inferHead :: Head -> TCM (Args -> Term, Type)
inferHead (HeadVar x) = do -- traceCall (InferVar x) $ do
  (u, a) <- getVarInfo x
  return (apply u, a)
inferHead (HeadDef x) = do
  (u, a) <- inferDef Def x
  return (apply u, a)
inferHead (HeadCon [c]) = do

  -- Constructors are polymorphic internally so when building the constructor
  -- term we should throw away arguments corresponding to parameters.

  -- First, inferDef will try to apply the constructor to the free parameters
  -- of the current context. We ignore that.
  (u, a) <- inferDef (\c _ -> Con c []) c

  -- Next get the number of parameters in the current context.
  Constructor{conPars = n} <- theDef <$> (instantiateDef =<< getConstInfo c)

  verboseS "tc.term.con" 7 $ do
    liftIO $ LocIO.putStrLn $ unwords [show c, "has", show n, "parameters."]

  -- So when applying the constructor throw away the parameters.
  return (apply u . genericDrop n, a)
inferHead (HeadCon _) = __IMPOSSIBLE__  -- inferHead will only be called on unambiguous constructors

inferDef :: (QName -> Args -> Term) -> QName -> TCM (Term, Type)
inferDef mkTerm x =
    traceCall (InferDef (getRange x) x) $ do
    d  <- instantiateDef =<< getConstInfo x
    vs <- freeVarsToApply x
    verboseS "tc.term.def" 10 $ do
      ds <- mapM prettyTCM vs
      dx <- prettyTCM x
      dt <- prettyTCM $ defType d
      liftIO $ LocIO.putStrLn $ "inferred def " ++ unwords (show dx : map show ds) ++ " : " ++ show dt
    return (mkTerm x vs, defType d)

-- | @checkHeadApplication e t hd args@ checks that @e@ has type @t@,
-- assuming that @e@ has the form @hd args@. The corresponding
-- type-checked term is returned.
--
-- If the head term @hd@ is a coinductive constructor, then a
-- top-level definition @fresh tel = hd args@ (where the clause is
-- delayed) is added, where @tel@ corresponds to the current
-- telescope. The returned term is @fresh tel@.
--
-- Precondition: The head @hd@ has to be unambiguous, and there should
-- not be any need to insert hidden lambdas.
checkHeadApplication :: A.Expr -> Type -> A.Head -> [NamedArg A.Expr] -> TCM Term
checkHeadApplication e t hd args = do
  replacing <- envReplace <$> ask
  if not replacing
   then local (\e -> e { envReplace = True }) defaultResult
   else case hd of
    HeadCon [c] -> do
      info <- getConstInfo c
      case conInd $ theDef info of
        Inductive   -> do
          (f, t0) <- inferHead hd
          checkArguments' ExpandLast (getRange hd) args t0 t e $ \vs t1 cs -> do
            TelV eTel eType <- telView <$> normalise t
            TelV fTel fType <- telView <$> normalise t1
            blockTerm t (f vs) $ (cs ++) <$> do
              -- We know that the target type of the constructor (fType)
              -- does not depend on fTel so we can compare fType and eType
              -- first.
                                             -- This will fail
              when (size eTel > size fTel) $ compareTel CmpLeq eTel fTel >> return ()

              -- If the expected type is a metavariable we have to make
              -- sure it's instantiated to the proper pi type
              let (fTel0, fTel1) = telFromList -*- telFromList
                                 $ splitAt (size eTel)
                                 $ telToList fTel
                  fType' = abstract fTel1 fType

              cs1 <- addCtxTel eTel $ leqType fType' eType
              cs2 <- compareTel CmpLeq eTel fTel0
              return $ cs1 ++ cs2
        CoInductive -> do
          -- TODO: Handle coinductive constructors under lets.
          lets <- envLetBindings <$> ask
          unless (Map.null lets) $
            typeError $ NotImplemented
              "coinductive constructor in the scope of a let-bound variable"

          -- The name of the fresh function.
          i <- fresh :: TCM Integer
          let name = filter (/= '_') (show $ A.qnameName c) ++ "-" ++ show i
          c' <- liftM2 qualify currentModule (freshName_ name)

          -- The application of the fresh function to the relevant
          -- arguments.
          e' <- Def c' <$> getContextArgs

          -- Add the type signature of the fresh function to the
          -- signature.
          i   <- currentMutualBlock
          tel <- getContextTelescope
          addConstant c' (Defn c' t (defaultDisplayForm c') i $ Axiom Nothing)

          -- Define and type check the fresh function.
          ctx <- getContext
          let info   = A.mkDefInfo (A.nameConcrete $ A.qnameName c') defaultFixity
                                   PublicAccess ConcreteDef noRange
              pats   = map (fmap $ \(n, _) -> Named Nothing (A.VarP n)) $
                           reverse ctx
              clause = A.Clause (A.LHS (A.LHSRange noRange) c' pats [])
                                (A.RHS $ unAppView (A.Application hd args))
                                []

          reportSDoc "tc.term.expr.coind" 15 $ vcat $
              [ text "The coinductive constructor application"
              , nest 2 $ prettyTCM e
              , text "was translated into the application"
              , nest 2 $ prettyTCM e'
              , text "and the function"
              , nest 2 $ prettyTCM c' <+> text ":"
              , nest 4 $ prettyTCM (telePi tel t)
              , nest 2 $ prettyA clause <> text "."
              ]

          local (\e -> e { envReplace = False }) $
            escapeContext (size ctx) $ checkFunDef Delayed info c' [clause]

          reportSDoc "tc.term.expr.coind" 15 $ do
            def <- theDef <$> getConstInfo c'
            text "The definition is" <+> text (show $ funDelayed def) <>
              text "."

          return e'
    HeadCon _  -> __IMPOSSIBLE__
    HeadVar {} -> defaultResult
    HeadDef {} -> defaultResult
  where
  defaultResult = do
    (f, t0) <- inferHead hd
    checkArguments' ExpandLast (getRange hd) args t0 t e $ \vs t1 cs ->
      blockTerm t (f vs) $ (cs ++) <$> leqType t1 t

data ExpandHidden = ExpandLast | DontExpandLast

instance Error Type where
  strMsg _ = __IMPOSSIBLE__
  noMsg = __IMPOSSIBLE__

traceCallE :: Error e => (Maybe r -> Call) -> ErrorT e TCM r -> ErrorT e TCM r
traceCallE call m = do
  z <- lift $ traceCall call' $ runErrorT m
  case z of
    Right e  -> return e
    Left err -> throwError err
  where
    call' Nothing          = call Nothing
    call' (Just (Left _))  = call Nothing
    call' (Just (Right x)) = call (Just x)

-- | Check a list of arguments: @checkArgs args t0 t1@ checks that
--   @t0 = Delta -> t0'@ and @args : Delta@. Inserts hidden arguments to
--   make this happen. Returns @t0'@ and any constraints that have to be
--   solve for everything to be well-formed.
--   TODO: doesn't do proper blocking of terms
checkArguments :: ExpandHidden -> Range -> [NamedArg A.Expr] -> Type -> Type -> ErrorT Type TCM (Args, Type, Constraints)
checkArguments DontExpandLast _ [] t0 t1 = return ([], t0, [])
checkArguments exh r [] t0 t1 =
    traceCallE (CheckArguments r [] t0 t1) $ do
	t0' <- lift $ reduce t0
	t1' <- lift $ reduce t1
	case funView $ unEl t0' of -- TODO: clean
	    FunV (Arg Hidden a) _ | notHPi $ unEl t1'  -> do
		v  <- lift $ newValueMeta a
		let arg = Arg Hidden v
		(vs, t0'',cs) <- checkArguments exh r [] (piApply t0' [arg]) t1'
		return (arg : vs, t0'',cs)
	    _ -> return ([], t0', [])
    where
	notHPi (Pi  (Arg Hidden _) _) = False
	notHPi (Fun (Arg Hidden _) _) = False
	notHPi _		      = True

checkArguments exh r args0@(Arg h e : args) t0 t1 =
    traceCallE (CheckArguments r args0 t0 t1) $ do
      t0b <- lift $ reduceB t0
      case t0b of
        Blocked{}                 -> throwError $ ignoreBlocking t0b
        NotBlocked (El _ MetaV{}) -> throwError $ ignoreBlocking t0b
        NotBlocked t0' -> do
          -- (t0', cs) <- forcePi h (name e) t0
          e' <- return $ namedThing e
          case (h, funView $ unEl t0') of
              (NotHidden, FunV (Arg Hidden a) _) -> insertUnderscore
              (Hidden, FunV (Arg Hidden a) _)
                  | not $ sameName (nameOf e) (nameInPi $ unEl t0') -> insertUnderscore
              (_, FunV (Arg h' a) _) | h == h' -> do
                  u  <- lift $ checkExpr e' a
                  let arg = Arg h u
                  (us, t0'', cs') <- checkArguments exh (fuseRange r e) args (piApply t0' [arg]) t1
                  return (arg : us, t0'', cs')
              (Hidden, FunV (Arg NotHidden _) _) ->
                  lift $ typeError $ WrongHidingInApplication t0'
              _ -> lift $ typeError $ ShouldBePi t0'
    where
	insertUnderscore = do
	  scope <- lift $ getScope
	  let m = A.Underscore $ A.MetaInfo
		  { A.metaRange  = r
		  , A.metaScope  = scope
		  , A.metaNumber = Nothing
		  }
	  checkArguments exh r (Arg Hidden (unnamed m) : args0) t0 t1

	name (Named _ (A.Var x)) = show x
	name (Named (Just x) _)    = x
	name _			   = "x"

	sameName Nothing _  = True
	sameName n1	 n2 = n1 == n2

	nameInPi (Pi _ b)  = Just $ absName b
	nameInPi (Fun _ _) = Nothing
	nameInPi _	   = __IMPOSSIBLE__


-- | Check that a list of arguments fits a telescope.
checkArguments_ :: ExpandHidden -> Range -> [NamedArg A.Expr] -> Telescope -> TCM (Args, Constraints)
checkArguments_ exh r args tel = do
    z <- runErrorT $ checkArguments exh r args (telePi tel $ sort Prop) (sort Prop)
    case z of
      Right (args, _, cs) -> return (args, cs)
      Left _              -> __IMPOSSIBLE__


-- | Infer the type of an expression. Implemented by checking agains a meta
--   variable.
inferExpr :: A.Expr -> TCM (Term, Type)
inferExpr e = do
    t <- newTypeMeta_
    v <- checkExpr e t
    return (v,t)

---------------------------------------------------------------------------
-- * Let bindings
---------------------------------------------------------------------------

checkLetBindings :: [A.LetBinding] -> TCM a -> TCM a
checkLetBindings = foldr (.) id . map checkLetBinding

checkLetBinding :: A.LetBinding -> TCM a -> TCM a
checkLetBinding b@(A.LetBind i x t e) ret =
  traceCallCPS_ (CheckLetBinding b) ret $ \ret -> do
    t <- isType_ t
    v <- checkExpr e t
    addLetBinding x v t ret
checkLetBinding (A.LetApply i x tel m args rd rm) ret = do
  -- Any variables in the context that doesn't belong to the current
  -- module should go with the new module.
  -- fv   <- getDefFreeVars =<< (qnameFromList . mnameToList) <$> currentModule
  fv   <- getModuleFreeVars =<< currentModule
  n    <- size <$> getContext
  let new = n - fv
  reportSLn "tc.term.let.apply" 10 $ "Applying " ++ show m ++ " with " ++ show new ++ " free variables"
  reportSDoc "tc.term.let.apply" 20 $ vcat
    [ text "context =" <+> (prettyTCM =<< getContextTelescope)
    , text "module  =" <+> (prettyTCM =<< currentModule)
    , text "fv      =" <+> (text $ show fv)
    ]
  checkSectionApplication i x tel m args rd rm
  withAnonymousModule x new ret
-- LetOpen is only used for highlighting and has no semantics
checkLetBinding A.LetOpen{} ret = ret