content: {-|
  Module      : Idris.Elab.Term
  Description : Code to elaborate terms.
  
  License     : BSD3
  Maintainer  : The Idris Community.
  -}
  {-# LANGUAGE LambdaCase, PatternGuards, ViewPatterns #-}
  {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
  module Idris.Elab.Term where
  
  import Idris.AbsSyntax
  import Idris.Core.CaseTree (SC'(STerm), findCalls)
  import Idris.Core.Elaborate hiding (Tactic(..))
  import Idris.Core.Evaluate
  import Idris.Core.ProofTerm (getProofTerm)
  import Idris.Core.TT
  import Idris.Core.Typecheck (check, converts, isType, recheck)
  import Idris.Core.Unify
  import Idris.Core.WHNF (whnf)
  import Idris.Coverage (genClauses, recoverableCoverage)
  import Idris.Delaborate
  import Idris.Elab.Quasiquote (extractUnquotes)
  import Idris.Elab.Rewrite
  import Idris.Elab.Utils
  import Idris.Error
  import Idris.ErrReverse (errReverse)
  import Idris.Options
  import Idris.ProofSearch
  import Idris.Reflection
  import Idris.Termination (buildSCG, checkDeclTotality, checkPositive)
  
  import Control.Monad
  import Control.Monad.State.Strict
  import Data.Foldable (for_)
  import Data.List
  import qualified Data.Map as M
  import Data.Maybe (fromMaybe, mapMaybe, maybeToList)
  import qualified Data.Set as S
  import Debug.Trace
  
  data ElabMode = ETyDecl | ETransLHS | ELHS | EImpossible | ERHS
    deriving Eq
  
  
  data ElabResult = ElabResult {
      -- | The term resulting from elaboration
      resultTerm :: Term
      -- | Information about new metavariables
    , resultMetavars :: [(Name, (Int, Maybe Name, Type, [Name]))]
      -- | Deferred declarations as the meaning of case blocks
    , resultCaseDecls :: [PDecl]
      -- | The potentially extended context from new definitions
    , resultContext :: Context
      -- | Meta-info about the new type declarations
    , resultTyDecls :: [RDeclInstructions]
      -- | Saved highlights from elaboration
    , resultHighlighting :: S.Set (FC', OutputAnnotation)
      -- | The new global name counter
    , resultName :: Int
    }
  
  
  
  -- | Using the elaborator, convert a term in raw syntax to a fully
  -- elaborated, typechecked term.
  --
  -- If building a pattern match, we convert undeclared variables from
  -- holes to pattern bindings.
  --
  -- Also find deferred names in the term and their types
  build :: IState
        -> ElabInfo
        -> ElabMode
        -> FnOpts
        -> Name
        -> PTerm
        -> ElabD ElabResult
  build ist info emode opts fn tm
      = do elab ist info emode opts fn tm
           let inf = case lookupCtxt fn (idris_tyinfodata ist) of
                          [TIPartial] -> True
                          _ -> False
  
           hs <- get_holes
           ivs <- get_implementations
           ptm <- get_term
           -- Resolve remaining interfaces. Two passes - first to get the
           -- default Num implementations, second to clean up the rest
           when (not pattern) $
                mapM_ (\n -> when (n `elem` hs) $
                               do focus n
                                  g <- goal
                                  try (resolveTC' True True 10 g fn ist)
                                      (movelast n)) ivs
           ivs <- get_implementations
           hs <- get_holes
           when (not pattern) $
                mapM_ (\n -> when (n `elem` hs) $
                               do focus n
                                  g <- goal
                                  ptm <- get_term
                                  resolveTC' True True 10 g fn ist) ivs
  
           when (not pattern) $ solveAutos ist fn False
  
           tm <- get_term
           ctxt <- get_context
           probs <- get_probs
           u <- getUnifyLog
           hs <- get_holes
  
           when (not pattern) $
             traceWhen u ("Remaining holes:\n" ++ show hs ++ "\n" ++
                          "Remaining problems:\n" ++ qshow probs) $
               do unify_all; matchProblems True; unifyProblems
  
           when (not pattern) $ solveAutos ist fn True
  
           probs <- get_probs
           case probs of
              [] -> return ()
              ((_,_,_,_,e,_,_):es) -> traceWhen u ("Final problems:\n" ++ qshow probs ++ "\nin\n" ++ show tm) $
                                       if inf then return ()
                                              else lift (Error e)
  
           when tydecl (do mkPat
                           update_term liftPats
                           update_term orderPats)
           EState is _ impls highlights _ _ <- getAux
           tt <- get_term
           ctxt <- get_context
           let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []
           log <- getLog
           g_nextname <- get_global_nextname
           if log /= ""
              then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
              else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
    where pattern = emode == ELHS || emode == EImpossible
          tydecl = emode == ETyDecl
  
          mkPat = do hs <- get_holes
                     tm <- get_term
                     case hs of
                        (h: hs) -> do patvar h; mkPat
                        [] -> return ()
  
  -- | Build a term autogenerated as an interface method definition.
  --
  -- (Separate, so we don't go overboard resolving things that we don't
  -- know about yet on the LHS of a pattern def)
  
  buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name ->
           [Name] -> -- Cached names in the PTerm, before adding PAlternatives
           PTerm ->
           ElabD ElabResult
  buildTC ist info emode opts fn ns tm
      = do let inf = case lookupCtxt fn (idris_tyinfodata ist) of
                          [TIPartial] -> True
                          _ -> False
           -- set name supply to begin after highest index in tm
           initNextNameFrom ns
           elab ist info emode opts fn tm
           probs <- get_probs
           tm <- get_term
           case probs of
              [] -> return ()
              ((_,_,_,_,e,_,_):es) -> if inf then return ()
                                             else lift (Error e)
           dots <- get_dotterm
           -- 'dots' are the PHidden things which have not been solved by
           -- unification
           when (not (null dots)) $
              lift (Error (CantMatch (getInferTerm tm)))
           EState is _ impls highlights _ _ <- getAux
           tt <- get_term
           ctxt <- get_context
           let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []
           log <- getLog
           g_nextname <- get_global_nextname
           if (log /= "")
              then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
              else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
  
  -- | return whether arguments of the given constructor name can be
  -- matched on. If they're polymorphic, no, unless the type has beed
  -- made concrete by the time we get around to elaborating the
  -- argument.
  getUnmatchable :: Context -> Name -> [Bool]
  getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon
     = case lookupTyExact n ctxt of
            Nothing -> []
            Just ty -> checkArgs [] [] ty
    where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool]
          checkArgs env ns (Bind n (Pi _ _ t _) sc)
              = let env' = case t of
                                TType _ -> n : env
                                _ -> env in
                    checkArgs env' (intersect env (refsIn t) : ns)
                              (instantiate (P Bound n t) sc)
          checkArgs env ns t
              = map (not . null) (reverse ns)
  
  getUnmatchable ctxt n = []
  
  data ElabCtxt = ElabCtxt { e_inarg :: Bool,
                             e_isfn :: Bool, -- ^ Function part of application
                             e_guarded :: Bool,
                             e_intype :: Bool,
                             e_qq :: Bool,
                             e_nomatching :: Bool -- ^ can't pattern match
                           }
  
  initElabCtxt = ElabCtxt False False False False False False
  
  goal_polymorphic :: ElabD Bool
  goal_polymorphic =
     do ty <- goal
        case ty of
             P _ n _ -> do env <- get_env
                           case lookupBinder n env of
                                Nothing -> return False
                                _ -> return True
             _ -> return False
  
  -- | Returns the set of declarations we need to add to complete the
  -- definition (most likely case blocks to elaborate) as well as
  -- declarations resulting from user tactic scripts (%runElab)
  elab :: IState
       -> ElabInfo
       -> ElabMode
       -> FnOpts
       -> Name
       -> PTerm
       -> ElabD ()
  elab ist info emode opts fn tm
      = do let loglvl = opt_logLevel (idris_options ist)
           when (loglvl > 5) $ unifyLog True
           compute -- expand type synonyms, etc
           elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)
           est <- getAux
           sequence_ (get_delayed_elab est)
           end_unify
           when (pattern || intransform) $
                -- convert remaining holes to pattern vars
                do unify_all
                   matchProblems False -- only the ones we matched earlier
                   unifyProblems
                   mkPat
                   update_term liftPats
           ptm <- get_term
           when pattern $
                -- Look for Rig1 (linear) pattern bindings
                do let pnms = findLinear Rig1 ist [] ptm
                   update_term (setLinear pnms)
    where
      pattern = emode == ELHS || emode == EImpossible
      eimpossible = emode == EImpossible
      intransform = emode == ETransLHS
      bindfree = emode == ETyDecl || emode == ELHS || emode == ETransLHS
                 || emode == EImpossible
      autoimpls = opt_autoimpls (idris_options ist)
  
      get_delayed_elab est =
          let ds = delayed_elab est in
              map snd $ sortBy (\(p1, _) (p2, _) -> compare p1 p2) ds
  
      tcgen = Dictionary `elem` opts
      reflection = Reflection `elem` opts
  
      isph arg = case getTm arg of
          Placeholder -> (True, priority arg)
          tm -> (False, priority arg)
  
      mkPat = do hs <- get_holes
                 tm <- get_term
                 case hs of
                    (h: hs) -> do patvar h; mkPat
                    [] -> return ()
  
      elabRec = elabE initElabCtxt Nothing
  
      -- | elabE elaborates an expression, possibly wrapping implicit coercions
      -- and forces/delays.  If you make a recursive call in elab', it is
      -- normally correct to call elabE - the ones that don't are `desugarings
      -- typically
      elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
      elabE ina fc' t =
       do solved <- get_recents
          as <- get_autos
          hs <- get_holes
          -- If any of the autos use variables which have recently been solved,
          -- have another go at solving them now.
          mapM_ (\(a, (failc, ns)) ->
                         if any (\n -> n `elem` solved) ns && head hs /= a
                                then solveAuto ist fn False (a, failc)
                                else return ()) as
  
          apt <- expandToArity t
          itm <- if not pattern then insertImpLam ina apt else return apt
          ct <- insertCoerce ina itm
          t' <- insertLazy ina ct
          g <- goal
          tm <- get_term
          ps <- get_probs
          hs <- get_holes
  
          --trace ("Elaborating " ++ show t' ++ " in " ++ show g
          --         ++ "\n" ++ show tm
          --         ++ "\nholes " ++ show hs
          --         ++ "\nproblems " ++ show ps
          --         ++ "\n-----------\n") $
          --trace ("ELAB " ++ show t') $
          env <- get_env
          let fc = fileFC "Force"
          handleError (forceErr t' env)
              (elab' ina fc' t')
              (elab' ina fc' (PApp fc (PRef fc [] (sUN "Force"))
                               [pimp (sUN "t") Placeholder True,
                                pimp (sUN "a") Placeholder True,
                                pexp ct]))
  
      forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)
         | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
              ht == txt "Delayed" = notDelay orig
      forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)
         | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),
              ht == txt "Delayed" = notDelay orig
      forceErr orig env (InfiniteUnify _ t _)
         | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
              ht == txt "Delayed" = notDelay orig
      forceErr orig env (Elaborating _ _ _ t) = forceErr orig env t
      forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t
      forceErr orig env (At _ t) = forceErr orig env t
      forceErr orig env t = False
  
      notDelay t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = False
      notDelay _ = True
  
      elab' :: ElabCtxt  -- ^ (in an argument, guarded, in a type, in a quasiquote)
            -> Maybe FC -- ^ The closest FC in the syntax tree, if applicable
            -> PTerm -- ^ The term to elaborate
            -> ElabD ()
      elab' ina fc (PNoImplicits t) = elab' ina fc t -- skip elabE step
      elab' ina fc (PType fc')       =
        do apply RType []
           solve
           highlightSource fc' (AnnType "Type" "The type of types")
      elab' ina fc (PUniverse fc' u)   =
        do unless (UniquenessTypes `elem` idris_language_extensions ist
                    || e_qq ina) $
             lift $ tfail $ At fc' (Msg "You must turn on the UniquenessTypes extension to use UniqueType or AnyType")
           apply (RUType u) []
           solve
           highlightSource fc' (AnnType (show u) "The type of unique types")
  --  elab' (_,_,inty) (PConstant c)
  --     | constType c && pattern && not reflection && not inty
  --       = lift $ tfail (Msg "Typecase is not allowed")
      elab' ina fc tm@(PConstant fc' c)
           | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
             && isTypeConst c
                = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
           | pattern && not reflection && not (e_qq ina) && e_nomatching ina
                = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
           | otherwise = do apply (RConstant c) []
                            solve
                            highlightSource fc' (AnnConst c)
      elab' ina fc (PQuote r)     = do fill r; solve
      elab' ina _ (PTrue fc _)   =
         do compute
            g <- goal
            case g of
              TType _ -> elab' ina (Just fc) (PRef fc [] unitTy)
              UType _ -> elab' ina (Just fc) (PRef fc [] unitTy)
              _ -> elab' ina (Just fc) (PRef fc [] unitCon)
      elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent interfaces
         = do g <- goal; resolveTC False False 5 g fn elabRec ist
      elab' ina fc (PResolveTC fc')
          = do c <- getNameFrom (sMN 0 "__interface")
               implementationArg c
      -- Elaborate the equality type first homogeneously, then
      -- heterogeneously as a fallback
      elab' ina _ (PApp fc (PRef _ _ n) args)
         | n == eqTy, [Placeholder, Placeholder, l, r] <- map getTm args
         = try (do tyn <- getNameFrom (sMN 0 "aqty")
                   claim tyn RType
                   movelast tyn
                   elab' ina (Just fc) (PApp fc (PRef fc [] eqTy)
                                [pimp (sUN "A") (PRef NoFC [] tyn) True,
                                 pimp (sUN "B") (PRef NoFC [] tyn) False,
                                 pexp l, pexp r]))
               (do atyn <- getNameFrom (sMN 0 "aqty")
                   btyn <- getNameFrom (sMN 0 "bqty")
                   claim atyn RType
                   movelast atyn
                   claim btyn RType
                   movelast btyn
                   elab' ina (Just fc) (PApp fc (PRef fc [] eqTy)
                     [pimp (sUN "A") (PRef NoFC [] atyn) True,
                      pimp (sUN "B") (PRef NoFC [] btyn) False,
                      pexp l, pexp r]))
  
      elab' ina _ (PPair fc hls _ l r)
          = do compute
               g <- goal
               let (tc, _) = unApply g
               case g of
                  TType _ -> elab' ina (Just fc) (PApp fc (PRef fc hls pairTy)
                                                        [pexp l,pexp r])
                  UType _ -> elab' ina (Just fc) (PApp fc (PRef fc hls upairTy)
                                                        [pexp l,pexp r])
                  _ -> case tc of
                          P _ n _ | n == upairTy
                            -> elab' ina (Just fc) (PApp fc (PRef fc hls upairCon)
                                                  [pimp (sUN "A") Placeholder False,
                                                   pimp (sUN "B") Placeholder False,
                                                   pexp l, pexp r])
                          _ -> elab' ina (Just fc) (PApp fc (PRef fc hls pairCon)
                                                  [pimp (sUN "A") Placeholder False,
                                                   pimp (sUN "B") Placeholder False,
                                                   pexp l, pexp r])
      elab' ina _ (PDPair fc hls p l@(PRef nfc hl n) t r)
              = case p of
                  IsType -> asType
                  IsTerm -> asValue
                  TypeOrTerm ->
                     do compute
                        g <- goal
                        case g of
                           TType _ -> asType
                           _ -> asValue
           where asType = elab' ina (Just fc) (PApp fc (PRef NoFC hls sigmaTy)
                                          [pexp t,
                                           pexp (PLam fc n nfc Placeholder r)])
                 asValue = elab' ina (Just fc) (PApp fc (PRef fc hls sigmaCon)
                                           [pimp (sMN 0 "a") t False,
                                            pimp (sMN 0 "P") Placeholder True,
                                            pexp l, pexp r])
  
      elab' ina _ (PDPair fc hls p l t r) = elab' ina (Just fc) (PApp fc (PRef fc hls sigmaCon)
                                                    [pimp (sMN 0 "a") t False,
                                                     pimp (sMN 0 "P") Placeholder True,
                                                     pexp l, pexp r])
      elab' ina fc (PAlternative ms (ExactlyOne delayok) as)
          = do as_pruned <- doPrune as
               -- Finish the mkUniqueNames job with the pruned set, rather than
               -- the full set.
               uns <- get_usedns
               let as' = map (mkUniqueNames (uns ++ map snd ms) ms) as_pruned
               ~(h : hs) <- get_holes
               ty <- goal
               case as' of
                    [] -> do hds <- mapM showHd as
                             lift $ tfail $ NoValidAlts hds
                    [x] -> elab' ina fc x
                    -- If there's options, try now, and if that fails, postpone
                    -- to later.
                    _ -> handleError isAmbiguous
                             (do hds <- mapM showHd as'
                                 tryAll (zip (map (elab' ina fc) as')
                                             hds))
                          (do movelast h
                              delayElab 5 $ do
                                hs <- get_holes
                                when (h `elem` hs) $ do
                                    focus h
                                    as'' <- doPrune as'
                                    case as'' of
                                         [x] -> elab' ina fc x
                                         _ -> do hds <- mapM showHd as''
                                                 tryAll' False (zip (map (elab' ina fc) as'')
                                                                    hds))
          where showHd (PApp _ (PRef _ _ (UN l)) [_, _, arg])
                   | l == txt "Delay" = showHd (getTm arg)
                showHd (PApp _ (PRef _ _ n) _) = return n
                showHd (PRef _ _ n) = return n
                showHd (PApp _ h _) = showHd h
                showHd (PHidden h) = showHd h
                showHd x = getNameFrom (sMN 0 "_") -- We probably should do something better than this here
  
                doPrune as =
                    do compute -- to get 'Delayed' if it's there
                       ty <- goal
                       ctxt <- get_context
                       env <- get_env
                       let ty' = unDelay ty
                       let (tc, _) = unApply ty'
                       return $ pruneByType eimpossible env tc ty' ist as
  
                unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,
                            l == txt "Delayed" = unDelay arg
                          | otherwise = t
  
                isAmbiguous (CantResolveAlts _) = delayok
                isAmbiguous (Elaborating _ _ _ e) = isAmbiguous e
                isAmbiguous (ElaboratingArg _ _ _ e) = isAmbiguous e
                isAmbiguous (At _ e) = isAmbiguous e
                isAmbiguous _ = False
  
      elab' ina fc (PAlternative ms FirstSuccess as_in)
          = do -- finish the mkUniqueNames job
               uns <- get_usedns
               let as = map (mkUniqueNames (uns ++ map snd ms) ms) as_in
               trySeq as
          where -- if none work, take the error from the first
                trySeq (x : xs) = let e1 = elab' ina fc x in
                                      try' e1 (trySeq' e1 xs) True
                trySeq [] = fail "Nothing to try in sequence"
                trySeq' deferr [] = do deferr; unifyProblems
                trySeq' deferr (x : xs)
                    = try' (tryCatch (do elab' ina fc x
                                         solveAutos ist fn False
                                         unifyProblems)
                               (\_ -> trySeq' deferr []))
                           (trySeq' deferr xs) True
      elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do
          env <- get_env
          compute
          ty <- goal
          let doelab = elab' ina fc orig
          tryCatch doelab
              (\err ->
                  if recoverableErr err
                     then -- trace ("NEED IMPLICIT! " ++ show orig ++ "\n" ++
                          --      show alts ++ "\n" ++
                          --      showQuick err) $
                      -- Prune the coercions so that only the ones
                      -- with the right type to fix the error will be tried!
                      case pruneAlts err alts env of
                           [] -> lift $ tfail err
                           alts' -> do
                               try' (elab' ina fc (PAlternative ms (ExactlyOne False) alts'))
                                    (lift $ tfail err) -- take error from original if all fail
                                    True
                     else lift $ tfail err)
        where
          recoverableErr (CantUnify _ _ _ _ _ _) = True
          recoverableErr (TooManyArguments _) = False
          recoverableErr (CantSolveGoal _ _) = False
          recoverableErr (CantResolveAlts _) = False
          recoverableErr (NoValidAlts _) = True
          recoverableErr (ProofSearchFail (Msg _)) = True
          recoverableErr (ProofSearchFail _) = False
          recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e
          recoverableErr (At _ e) = recoverableErr e
          recoverableErr (ElabScriptDebug _ _ _) = False
          recoverableErr _ = True
  
          pruneAlts (CantUnify _ (inc, _) (outc, _) _ _ _) alts env
              = case unApply (normalise (tt_ctxt ist) env inc) of
                     (P (TCon _ _) n _, _) -> filter (hasArg n env) alts
                     (Constant _, _) -> alts
                     _ -> filter isLend alts -- special case hack for 'Borrowed'
          pruneAlts (ElaboratingArg _ _ _ e) alts env = pruneAlts e alts env
          pruneAlts (At _ e) alts env = pruneAlts e alts env
          pruneAlts (NoValidAlts as) alts env = alts
          pruneAlts err alts _ = filter isLend alts
  
          hasArg n env ap | isLend ap = True -- special case hack for 'Borrowed'
          hasArg n env (PApp _ (PRef _ _ a) _)
               = case lookupTyExact a (tt_ctxt ist) of
                      Just ty -> let args = map snd (getArgTys (normalise (tt_ctxt ist) env ty)) in
                                     any (fnIs n) args
                      Nothing -> False
          hasArg n env (PAlternative _ _ as) = any (hasArg n env) as
          hasArg n _ tm = False
  
          isLend (PApp _ (PRef _ _ l) _) = l == sNS (sUN "lend") ["Ownership"]
          isLend _ = False
  
          fnIs n ty = case unApply ty of
                           (P _ n' _, _) -> n == n'
                           _ -> False
  
      elab' ina _ (PPatvar fc n) | bindfree
          = do patvar n
               update_term liftPats
               highlightSource fc (AnnBoundName n False)
  --    elab' (_, _, inty) (PRef fc f)
  --       | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
  --          = lift $ tfail (Msg "Typecase is not allowed")
      elab' ec fc' tm@(PRef fc hls n)
        | pattern && not reflection && not (e_qq ec) && not (e_intype ec)
              && isTConName n (tt_ctxt ist)
                = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
        | pattern && not reflection && not (e_qq ec) && e_nomatching ec
                = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
        | (pattern || intransform || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)
          = do ty <- goal
               testImplicitWarning fc n ty
               let ina = e_inarg ec
               ctxt <- get_context
               env <- get_env
  
               -- If the name is defined, globally or locally, elaborate it
               -- as a reference, otherwise it might end up as a pattern var.
               let defined = case lookupTy n ctxt of
                                 [] -> case lookupTyEnv n env of
                                            Just _ -> True
                                            _ -> False
                                 _ -> True
  
               -- this is to stop us resolving interfaces recursively
               if (tcname n && ina && not intransform)
                 then erun fc $
                        do patvar n
                           update_term liftPats
                           highlightSource fc (AnnBoundName n False)
                 else if defined -- finally, ordinary PRef elaboration
                         then elabRef ec fc' fc hls n tm
                         else try (do apply (Var n) []
                                      annot <- findHighlight n
                                      solve
                                      highlightSource fc annot)
                                  (do patvar n
                                      update_term liftPats
                                      highlightSource fc (AnnBoundName n False))
        where inparamBlock n = case lookupCtxtName n (inblock info) of
                                  [] -> False
                                  _ -> True
              bindable (NS _ _) = False
              bindable (MN _ _) = True
              bindable n = implicitable n && autoimpls
      elab' ina _ f@(PInferRef fc hls n) = elab' ina (Just fc) (PApp NoFC f [])
      elab' ina fc' tm@(PRef fc hls n)
            | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
              && isTConName n (tt_ctxt ist)
                = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
            | pattern && not reflection && not (e_qq ina) && e_nomatching ina
                = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
            | otherwise = elabRef ina fc' fc hls n tm
      elab' ina _ (PLam _ _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"
      elab' ina _ (PLam fc n nfc Placeholder sc)
            = do -- if n is a type constructor name, this makes no sense...
                 ctxt <- get_context
                 when (isTConName n ctxt) $
                      lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
                 checkPiGoal n
                 attack; intro (Just n);
                 addPSname n -- okay for proof search
                 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
                 elabE (ina { e_inarg = True } ) (Just fc) sc; solve
                 highlightSource nfc (AnnBoundName n False)
      elab' ec _ (PLam fc n nfc ty sc)
            = do tyn <- getNameFrom (sMN 0 "lamty")
                 -- if n is a type constructor name, this makes no sense...
                 ctxt <- get_context
                 when (isTConName n ctxt) $
                      lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
                 checkPiGoal n
                 claim tyn RType
                 explicit tyn
                 attack
                 ptm <- get_term
                 hs <- get_holes
                 introTy (Var tyn) (Just n)
                 addPSname n -- okay for proof search
                 focus tyn
  
                 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty
                 elabE (ec { e_inarg = True }) (Just fc) sc
                 solve
                 highlightSource nfc (AnnBoundName n False)
      elab' ina fc (PPi p n nfc Placeholder sc)
            = do attack;
                 case pcount p of
                      RigW -> return ()
                      _ -> unless (LinearTypes `elem` idris_language_extensions ist
                                         || e_qq ina) $
                             lift $ tfail $ At nfc (Msg "You must turn on the LinearTypes extension to use a count")
                 arg n (pcount p) (is_scoped p) (sMN 0 "phTy")
                 addAutoBind p n
                 addPSname n -- okay for proof search
                 elabE (ina { e_inarg = True, e_intype = True }) fc sc
                 solve
                 highlightSource nfc (AnnBoundName n False)
      elab' ina fc (PPi p n nfc ty sc)
            = do attack; tyn <- getNameFrom (sMN 0 "piTy")
                 claim tyn RType
                 n' <- case n of
                          MN _ _ -> unique_hole n
                          _ -> return n
                 case pcount p of
                      RigW -> return ()
                      _ -> unless (LinearTypes `elem` idris_language_extensions ist
                                         || e_qq ina) $
                             lift $ tfail $ At nfc (Msg "You must turn on the LinearTypes extension to use a linear argument")
                 forAll n' (pcount p) (is_scoped p) (Var tyn)
                 addAutoBind p n'
                 addPSname n' -- okay for proof search
                 focus tyn
                 let ec' = ina { e_inarg = True, e_intype = True }
                 elabE ec' fc ty
                 elabE ec' fc sc
                 solve
                 highlightSource nfc (AnnBoundName n False)
      elab' ina _ tm@(PLet fc rig n nfc ty val sc)
            = do attack
                 ivs <- get_implementations
                 tyn <- getNameFrom (sMN 0 "letty")
                 claim tyn RType
                 valn <- getNameFrom (sMN 0 "letval")
                 claim valn (Var tyn)
                 explicit valn
                 letbind n rig (Var tyn) (Var valn)
                 addPSname n
                 case ty of
                     Placeholder -> return ()
                     _ -> do focus tyn
                             explicit tyn
                             elabE (ina { e_inarg = True, e_intype = True })
                                   (Just fc) ty
                 focus valn
                 elabE (ina { e_inarg = True, e_intype = True })
                       (Just fc) val
                 ivs' <- get_implementations
                 env <- get_env
                 elabE (ina { e_inarg = True }) (Just fc) sc
                 when (not (pattern || intransform)) $
                     mapM_ (\n -> do focus n
                                     g <- goal
                                     hs <- get_holes
                                     if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
                                      then handleError (tcRecoverable emode)
                                             (resolveTC True False 10 g fn elabRec ist)
                                             (movelast n)
                                      else movelast n)
                           (ivs' \\ ivs)
                 -- HACK: If the name leaks into its type, it may leak out of
                 -- scope outside, so substitute in the outer scope.
                 expandLet n (case lookupBinder n env of
                                   Just (Let rig t v) -> v
                                   other -> error ("Value not a let binding: " ++ show other))
                 solve
                 highlightSource nfc (AnnBoundName n False)
      elab' ina _ (PGoal fc r n sc) = do
           rty <- goal
           attack
           tyn <- getNameFrom (sMN 0 "letty")
           claim tyn RType
           valn <- getNameFrom (sMN 0 "letval")
           claim valn (Var tyn)
           letbind n RigW (Var tyn) (Var valn)
           focus valn
           elabE (ina { e_inarg = True, e_intype = True }) (Just fc) (PApp fc r [pexp (delab ist rty)])
           env <- get_env
           computeLet n
           elabE (ina { e_inarg = True }) (Just fc) sc
           solve
  --          elab' ina fc (PLet n Placeholder
  --              (PApp fc r [pexp (delab ist rty)]) sc)
      elab' ina _ tm@(PApp fc (PInferRef _ _ f) args) = do
           rty <- goal
           ds <- get_deferred
           ctxt <- get_context
           -- make a function type a -> b -> c -> ... -> rty for the
           -- new function name
           env <- get_env
           argTys <- claimArgTys env args
           fn <- getNameFrom (sMN 0 "inf_fn")
           let fty = fnTy argTys rty
  --             trace (show (ptm, map fst argTys)) $ focus fn
              -- build and defer the function application
           attack; deferType (mkN f) fty (map fst argTys); solve
           -- elaborate the arguments, to unify their types. They all have to
           -- be explicit.
           mapM_ elabIArg (zip argTys args)
         where claimArgTys env [] = return []
               claimArgTys env (arg : xs) | Just n <- localVar env (getTm arg)
                                    = do nty <- get_type (Var n)
                                         ans <- claimArgTys env xs
                                         return ((n, (False, forget nty)) : ans)
               claimArgTys env (_ : xs)
                                    = do an <- getNameFrom (sMN 0 "inf_argTy")
                                         aval <- getNameFrom (sMN 0 "inf_arg")
                                         claim an RType
                                         claim aval (Var an)
                                         ans <- claimArgTys env xs
                                         return ((aval, (True, (Var an))) : ans)
               fnTy [] ret  = forget ret
               fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi RigW Nothing xt RType) (fnTy xs ret)
  
               localVar env (PRef _ _ x)
                             = case lookupBinder x env of
                                    Just _ -> Just x
                                    _ -> Nothing
               localVar env _ = Nothing
  
               elabIArg ((n, (True, ty)), def) =
                 do focus n; elabE ina (Just fc) (getTm def)
               elabIArg _ = return () -- already done, just a name
  
               mkN n@(NS _ _) = n
               mkN n@(SN _) = n
               mkN n = case namespace info of
                            xs@(_:_) -> sNS n xs
                            _ -> n
  
      elab' ina _ (PMatchApp fc fn)
         = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of
                               [(n, args)] -> return (n, map (const True) args)
                               _ -> lift $ tfail (NoSuchVariable fn)
              ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
              solve
      -- if f is local, just do a simple_app
      -- FIXME: Anyone feel like refactoring this mess? - EB
      elab' ina topfc tm@(PApp fc (PRef ffc hls f) args_in)
        | pattern && not reflection && not (e_qq ina) && e_nomatching ina
                = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
        | otherwise = implicitApp $
           do env <- get_env
              ty <- goal
              fty <- get_type (Var f)
              ctxt <- get_context
              let dataCon = isDConName f ctxt
              annot <- findHighlight f
              knowns_m <- mapM getKnownImplicit args_in
              let knowns = mapMaybe id knowns_m
              args <- insertScopedImps fc f knowns (normalise ctxt env fty) args_in
  
              let unmatchableArgs = if pattern
                                       then getUnmatchable (tt_ctxt ist) f
                                       else []
  --             trace ("BEFORE " ++ show f ++ ": " ++ show ty) $
              when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)
                            && isTConName f (tt_ctxt ist)) $
                lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
  --             trace (show (f, args_in, args)) $
              if (f `elem` map fstEnv env && length args == 1 && length args_in == 1)
                 then -- simple app, as below
                      do simple_app False
                                    (elabE (ina { e_isfn = True }) (Just fc) (PRef ffc hls f))
                                    (elabE (ina { e_inarg = True,
                                                  e_guarded = dataCon }) (Just fc) (getTm (head args)))
                                    (show tm)
                         solve
                         mapM (uncurry highlightSource) $
                           (ffc, annot) : map (\f -> (f, annot)) hls
                         return []
                 else
                   do ivs <- get_implementations
                      ps <- get_probs
                      -- HACK: we shouldn't resolve interfaces if we're defining an implementation
                      -- function or default definition.
                      let isinf = f == inferCon || tcname f
                      -- if f is an interface, we need to know its arguments so that
                      -- we can unify with them
                      case lookupCtxt f (idris_interfaces ist) of
                          [] -> return ()
                          _ -> do mapM_ setInjective (map getTm args)
                                  -- maybe more things are solvable now
                                  unifyProblems
  --                    trace ("args is " ++ show args) $ return ()
                      ns <- apply (Var f) (map isph args)
  --                    trace ("ns is " ++ show ns) $ return ()
                      -- mark any interface arguments as injective
  --                     when (not pattern) $
                      mapM_ checkIfInjective (map snd ns)
                      unifyProblems -- try again with the new information,
                                    -- to help with disambiguation
                      ulog <- getUnifyLog
  
                      annot <- findHighlight f
                      mapM (uncurry highlightSource) $
                        (ffc, annot) : map (\f -> (f, annot)) hls
  
                      elabArgs ist (ina { e_inarg = e_inarg ina || not isinf,
                                          e_guarded = dataCon })
                             [] fc False f
                               (zip ns (unmatchableArgs ++ repeat False))
                               (f == sUN "Force")
                               (map (\x -> getTm x) args) -- TODO: remove this False arg
                      imp <- if (e_isfn ina) then
                                do guess <- get_guess
                                   env <- get_env
                                   case safeForgetEnv (map fstEnv env) guess of
                                        Nothing ->
                                           return []
                                        Just rguess -> do
                                           gty <- get_type rguess
                                           let ty_n = normalise ctxt env gty
                                           return $ getReqImps ty_n
                                else return []
                      -- Now we find out how many implicits we needed at the
                      -- end of the application by looking at the goal again
                      -- - Have another go, but this time add the
                      -- implicits (can't think of a better way than this...)
                      case imp of
                           rs@(_:_) | not pattern -> return rs -- quit, try again
                           _ -> do solve
                                   hs <- get_holes
                                   ivs' <- get_implementations
                                   -- Attempt to resolve any interfaces which have 'complete' types,
                                   -- i.e. no holes in them
                                   when (not pattern || (e_inarg ina && not tcgen)) $
                                      mapM_ (\n -> do focus n
                                                      g <- goal
                                                      env <- get_env
                                                      hs <- get_holes
                                                      if all (\n -> not (n `elem` hs)) (freeNames g)
                                                       then handleError (tcRecoverable emode)
                                                                (resolveTC False False 10 g fn elabRec ist)
                                                                (movelast n)
                                                       else movelast n)
                                            (ivs' \\ ivs)
                                   return []
        where
              -- Run the elaborator, which returns how many implicit
              -- args were needed, then run it again with those args. We need
              -- this because we have to elaborate the whole application to
              -- find out whether any computations have caused more implicits
              -- to be needed.
              implicitApp :: ElabD [ImplicitInfo] -> ElabD ()
              implicitApp elab
                | pattern || intransform = do elab; return ()
                | otherwise
                  = do s <- get
                       imps <- elab
                       case imps of
                            [] -> return ()
                            es -> do put s
                                     elab' ina topfc (PAppImpl tm es)
  
              getKnownImplicit imp
                   | UnknownImp `elem` argopts imp
                      = return Nothing -- lift $ tfail $ UnknownImplicit (pname imp) f
                   | otherwise = return (Just (pname imp))
  
              getReqImps (Bind x (Pi _ (Just i) ty _) sc)
                   = i : getReqImps sc
              getReqImps _ = []
  
              checkIfInjective n = do
                  env <- get_env
                  case lookupBinder n env of
                       Nothing -> return ()
                       Just b ->
                         case unApply (normalise (tt_ctxt ist) env (binderTy b)) of
                              (P _ c _, args) ->
                                  case lookupCtxtExact c (idris_interfaces ist) of
                                     Nothing -> return ()
                                     Just ci -> -- interface, set as injective
                                          do mapM_ setinjArg (getDets 0 (interface_determiners ci) args)
                                          -- maybe we can solve more things now...
                                             ulog <- getUnifyLog
                                             probs <- get_probs
                                             inj <- get_inj
                                             traceWhen ulog ("Injective now " ++ show args ++ "\nAll: " ++ show inj
                                                              ++ "\nProblems: " ++ qshow probs) $
                                               unifyProblems
                                             probs <- get_probs
                                             traceWhen ulog (qshow probs) $ return ()
                              _ -> return ()
  
              setinjArg (P _ n _) = setinj n
              setinjArg _ = return ()
  
              getDets i ds [] = []
              getDets i ds (a : as) | i `elem` ds = a : getDets (i + 1) ds as
                                    | otherwise = getDets (i + 1) ds as
  
              setInjective (PRef _ _ n) = setinj n
              setInjective (PApp _ (PRef _ _ n) _) = setinj n
              setInjective _ = return ()
  
      elab' ina _ tm@(PApp fc f [arg]) =
              erun fc $
               do simple_app (not $ headRef f)
                             (elabE (ina { e_isfn = True }) (Just fc) f)
                             (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))
                                  (show tm)
                  solve
          where headRef (PRef _ _ _) = True
                headRef (PApp _ f _) = headRef f
                headRef (PAlternative _ _ as) = all headRef as
                headRef _ = False
  
      elab' ina fc (PAppImpl f es) = do appImpl (reverse es) -- not that we look...
                                        solve
          where appImpl [] = elab' (ina { e_isfn = False }) fc f -- e_isfn not set, so no recursive expansion of implicits
                appImpl (e : es) = simple_app False
                                              (appImpl es)
                                              (elab' ina fc Placeholder)
                                              (show f)
      elab' ina fc Placeholder
          = do ~(h : hs) <- get_holes
               movelast h
      elab' ina fc (PMetavar nfc n) =
            do ptm <- get_term
               -- When building the metavar application, leave out the unique
               -- names which have been used elsewhere in the term, since we
               -- won't be able to use them in the resulting application.
               env <- get_env
               let unique_used = getUniqueUsed (tt_ctxt ist) ptm
               let lin_used = getLinearUsed (tt_ctxt ist) ptm
               let n' = metavarName (namespace info) n
               attack
               psns <- getPSnames
               n' <- defer unique_used lin_used n'
               solve
               highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)
      elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts
      elab' ina fc (PTactics ts)
          | not pattern = do mapM_ (runTac False ist fc fn) ts
          | otherwise = elab' ina fc Placeholder
      elab' ina fc (PElabError e) = lift $ tfail e
      elab' ina mfc (PRewrite fc substfn rule sc newg)
          = elabRewrite (elab' ina mfc) ist fc substfn rule sc newg
      -- A common error case if trying to typecheck an autogenerated case block
      elab' ina _ c@(PCase fc Placeholder opts)
          = lift $ tfail (Msg "No expression for the case to inspect.\nYou need to replace the _ with an expression.")
      elab' ina _ c@(PCase fc scr opts)
          = do attack
  
               tyn <- getNameFrom (sMN 0 "scty")
               claim tyn RType
               valn <- getNameFrom (sMN 0 "scval")
               scvn <- getNameFrom (sMN 0 "scvar")
               claim valn (Var tyn)
               env <- get_env
  
               let scrnames = allNamesIn scr
               letbind scvn (letrig scrnames env) (Var tyn) (Var valn)
  
               -- Start filling in the scrutinee type, if we can work one
               -- out from the case options
               let scrTy = getScrType (map fst opts)
               case scrTy of
                    Nothing -> return ()
                    Just ty -> do focus tyn
                                  elabE ina (Just fc) ty
  
               focus valn
               elabE (ina { e_inarg = True }) (Just fc) scr
               -- Solve any remaining implicits - we need to solve as many
               -- as possible before making the 'case' type
               unifyProblems
               matchProblems True
               args <- get_env
               envU <- mapM (getKind args) args
  
               -- Drop the unique arguments used in the term already
               -- and in the scrutinee (since it's
               -- not valid to use them again anyway)
               --
               -- Also drop unique arguments which don't appear explicitly
               -- in either case branch so they don't count as used
               -- unnecessarily (can only do this for unique things, since we
               -- assume they don't appear implicitly in types)
               ptm <- get_term
               let inOpts = (filter (/= scvn) (map fstEnv args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)
  
               let argsDropped = filter (\t -> isUnique envU t || isNotLift args t)
                                     (nub $ scrnames ++ inApp ptm ++
                                      inOpts)
               let lin_used = getLinearUsed (tt_ctxt ist) ptm
  
               let args' = filter (\(n, _, _) -> n `notElem` argsDropped) args
  
               -- trace (show lin_used ++ "\n" ++ show args ++ "\n" ++ show ptm) attack
               attack
               cname' <- defer argsDropped lin_used (mkN (mkCaseName fc fn))
               solve
  
               -- if the scrutinee is one of the 'args' in env, we should
               -- inspect it directly, rather than adding it as a new argument
               let newdef = PClauses fc [] cname'
                               (caseBlock fc cname' scr
                                  (map (isScr scr) (reverse args')) opts)
               -- elaborate case
               updateAux (\e -> e { case_decls = (cname', newdef) : case_decls e } )
               -- if we haven't got the type yet, hopefully we'll get it later!
               movelast tyn
               solve
          where mkCaseName fc (NS n ns) = NS (mkCaseName fc n) ns
                mkCaseName fc n = SN (CaseN (FC' fc) n)
  --               mkCaseName (UN x) = UN (x ++ "_case")
  --               mkCaseName (MN i x) = MN i (x ++ "_case")
                mkN n@(NS _ _) = n
                mkN n = case namespace info of
                          xs@(_:_) -> sNS n xs
                          _ -> n
  
                -- If any variables in the scrutinee are in the environment with
                -- multiplicity other than RigW, let bind the scrutinee variable
                -- with the smallest multiplicity
                letrig ns [] = RigW
                letrig ns env = letrig' Rig1 ns env
  
                letrig' def ns [] = def
                letrig' def ns ((n, r, _) : env)
                     | n `elem` ns = letrig' (rigMult def r) ns env
                     | otherwise = letrig' def ns env
  
                getScrType [] = Nothing
                getScrType (f : os) = maybe (getScrType os) Just (getAppType f)
  
                getAppType (PRef _ _ n) =
                   case lookupTyName n (tt_ctxt ist) of
                        [(n', ty)] | isDConName n' (tt_ctxt ist) ->
                           case unApply (getRetTy ty) of
                             (P _ tyn _, args) ->
                                 Just (PApp fc (PRef fc [] tyn)
                                      (map pexp (map (const Placeholder) args)))
                             _ -> Nothing
                        _ -> Nothing -- ambiguity is no help to us!
                getAppType (PApp _ t as) = getAppType t
                getAppType _ = Nothing
  
                inApp (P _ n _) = [n]
                inApp (App _ f a) = inApp f ++ inApp a
                inApp (Bind n (Let _ _ v) sc) = inApp v ++ inApp sc
                inApp (Bind n (Guess _ v) sc) = inApp v ++ inApp sc
                inApp (Bind n b sc) = inApp sc
                inApp _ = []
  
                isUnique envk n = case lookup n envk of
                                       Just u -> u
                                       _ -> False
  
                getKind env (n, _, _)
                    = case lookupBinder n env of
                           Nothing -> return (n, False) -- can't happen, actually...
                           Just b ->
                              do ty <- get_type (forget (binderTy b))
                                 case ty of
                                      UType UniqueType -> return (n, True)
                                      UType AllTypes -> return (n, True)
                                      _ -> return (n, False)
  
                isNotLift env n
                   = case lookupBinder n env of
                          Just ty ->
                               case unApply (binderTy ty) of
                                    (P _ n _, _) -> n `elem` noCaseLift info
                                    _ -> False
                          _ -> False
  
      elab' ina fc (PUnifyLog t) = do unifyLog True
                                      elab' ina fc t
                                      unifyLog False
      elab' ina fc (PQuasiquote t goalt)
          = do -- First extract the unquoted subterms, replacing them with fresh
               -- names in the quasiquoted term. Claim their reflections to be
               -- an inferred type (to support polytypic quasiquotes).
               finalTy <- goal
               (t, unq) <- extractUnquotes 0 t
               let unquoteNames = map fst unq
               mapM_ (\uqn -> claim uqn (forget finalTy)) unquoteNames
  
               -- Save the old state - we need a fresh proof state to avoid
               -- capturing lexically available variables in the quoted term.
               ctxt <- get_context
               datatypes <- get_datatypes
               g_nextname <- get_global_nextname
               saveState
               updatePS (const .
                         newProof (sMN 0 "q") (constraintNS info) ctxt datatypes g_nextname $
                         P Ref (reflm "TT") Erased)
  
               -- Re-add the unquotes, letting Idris infer the (fictional)
               -- types. Here, they represent the real type rather than the type
               -- of their reflection.
               mapM_ (\n -> do ty <- getNameFrom (sMN 0 "unqTy")
                               claim ty RType
                               movelast ty
                               claim n (Var ty)
                               movelast n)
                     unquoteNames
  
               -- Determine whether there's an explicit goal type, and act accordingly
               -- Establish holes for the type and value of the term to be
               -- quasiquoted
               qTy <- getNameFrom (sMN 0 "qquoteTy")
               claim qTy RType
               movelast qTy
               qTm <- getNameFrom (sMN 0 "qquoteTm")
               claim qTm (Var qTy)
  
               -- Let-bind the result of elaborating the contained term, so that
               -- the hole doesn't disappear
               nTm <- getNameFrom (sMN 0 "quotedTerm")
               letbind nTm RigW (Var qTy) (Var qTm)
  
               -- Fill out the goal type, if relevant
               case goalt of
                 Nothing  -> return ()
                 Just gTy -> do focus qTy
                                elabE (ina { e_qq = True }) fc gTy
  
               -- Elaborate the quasiquoted term into the hole
               focus qTm
               elabE (ina { e_qq = True }) fc t
               end_unify
  
               -- We now have an elaborated term. Reflect it and solve the
               -- original goal in the original proof state, preserving highlighting
               env <- get_env
               EState _ _ _ hs _ _ <- getAux
               loadState
               updateAux (\aux -> aux { highlighting = hs })
  
               let quoted = fmap (explicitNames . binderVal) $ lookupBinder nTm env
                   isRaw = case unApply (normaliseAll ctxt env finalTy) of
                             (P _ n _, []) | n == reflm "Raw" -> True
                             _ -> False
               case quoted of
                 Just q -> do ctxt <- get_context
                              (q', _, _) <- lift $ recheck (constraintNS info) ctxt [(uq, RigW, Lam RigW Erased) | uq <- unquoteNames] (forget q) q
                              if pattern
                                then if isRaw
                                        then reflectRawQuotePattern unquoteNames (forget q')
                                        else reflectTTQuotePattern unquoteNames q'
                                else do if isRaw
                                          then -- we forget q' instead of using q to ensure rechecking
                                               fill $ reflectRawQuote unquoteNames (forget q')
                                          else fill $ reflectTTQuote unquoteNames q'
                                        solve
  
                 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"
  
               -- Finally fill in the terms or patterns from the unquotes. This
               -- happens last so that their holes still exist while elaborating
               -- the main quotation.
               mapM_ elabUnquote unq
        where elabUnquote (n, tm)
                  = do focus n
                       elabE (ina { e_qq = False }) fc tm
  
  
      elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"
      elab' ina fc (PQuoteName n False nfc) =
        do fill $ reflectName n
           solve
      elab' ina fc (PQuoteName n True nfc) =
        do ctxt <- get_context
           env <- get_env
           case lookupBinder n env of
             Just _ -> do fill $ reflectName n
                          solve
                          highlightSource nfc (AnnBoundName n False)
             Nothing ->
               case lookupNameDef n ctxt of
                 [(n', _)] -> do fill $ reflectName n'
                                 solve
                                 highlightSource nfc (AnnName n' Nothing Nothing Nothing)
                 [] -> lift . tfail . NoSuchVariable $ n
                 more -> lift . tfail . CantResolveAlts $ map fst more
      elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"
      elab' ina fc (PHidden t)
        | reflection = elab' ina fc t
        | otherwise
          = do ~(h : hs) <- get_holes
               -- Dotting a hole means that either the hole or any outer
               -- hole (a hole outside any occurrence of it)
               -- must be solvable by unification as well as being filled
               -- in directly.
               -- Delay dotted things to the end, then when we elaborate them
               -- we can check the result against what was inferred
               movelast h
               ~(h' : hs) <- get_holes
               -- If we're at the end anyway, do it now
               if h == h' then elabHidden h
                          else delayElab 10 $ elabHidden h
       where
        elabHidden h = do hs <- get_holes
                          when (h `elem` hs) $ do
                              focus h
                              dotterm
                              elab' ina fc t
      elab' ina fc (PRunElab fc' tm ns) =
        do unless (ElabReflection `elem` idris_language_extensions ist) $
             lift $ tfail $ At fc' (Msg "You must turn on the ElabReflection extension to use %runElab")
           attack
           let elabName = sNS (sUN "Elab") ["Elab", "Reflection", "Language"]
           n <- getNameFrom (sMN 0 "tacticScript")
           let scriptTy = RApp (Var elabName) (Var unitTy)
           claim n scriptTy
           focus n
           elabUnit <- goal
           attack -- to get an extra hole
           elab' ina (Just fc') tm
           script <- get_guess
           fullyElaborated script
           solve -- eliminate the hole. Because there are no references, the script is only in the binding
           ctxt <- get_context
           env <- get_env
           (scriptTm, scriptTy) <- lift $ check ctxt [] (forget script)
           lift $ converts ctxt env elabUnit scriptTy
           env <- get_env
           runElabAction info ist (maybe fc' id fc) env script ns
           solve
      elab' ina fc (PConstSugar constFC tm) =
        -- Here we elaborate the contained term, then calculate
        -- highlighting for constFC.  The highlighting is the
        -- highlighting for the outermost constructor of the result of
        -- evaluating the elaborated term, if one exists (it always
        -- should, but better to fail gracefully for something silly
        -- like highlighting info). This is how implicit applications of
        -- fromInteger get highlighted.
        do saveState -- so we don't pollute the elaborated term
           n <- getNameFrom (sMN 0 "cstI")
           n' <- getNameFrom (sMN 0 "cstIhole")
           g <- forget <$> goal
           claim n' g
           movelast n'
           -- In order to intercept the elaborated value, we need to
           -- let-bind it.
           attack
           letbind n RigW g (Var n')
           focus n'
           elab' ina fc tm
           env <- get_env
           ctxt <- get_context
           let v = fmap (normaliseAll ctxt env . finalise . binderVal)
                        (lookupBinder n env)
           loadState -- we have the highlighting - re-elaborate the value
           elab' ina fc tm
           case v of
             Just val -> highlightConst constFC val
             Nothing -> return ()
         where highlightConst fc (P _ n _) =
                 highlightSource fc (AnnName n Nothing Nothing Nothing)
               highlightConst fc (App _ f _) =
                 highlightConst fc f
               highlightConst fc (Constant c) =
                 highlightSource fc (AnnConst c)
               highlightConst _ _ = return ()
      elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
  
      -- delay elaboration of 't', with priority 'pri' until after everything
      -- else is done.
      -- The delayed things with lower numbered priority will be elaborated
      -- first. (In practice, this means delayed alternatives, then PHidden
      -- things.)
      delayElab pri t
         = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })
  
      -- If the variable in the environment is the scrutinee of the case,
      -- and has multiplicity W, keep it available
      isScr :: PTerm -> (Name, RigCount, Binder Term) -> (Name, (Bool, Binder Term))
      isScr (PRef _ _ n) (n', RigW, b) = (n', (n == n', b))
      isScr _ (n', _, b) = (n', (False, b))
  
      caseBlock :: FC -> Name
                   -> PTerm -- original scrutinee
                   -> [(Name, (Bool, Binder Term))] -> [(PTerm, PTerm)] -> [PClause]
      caseBlock fc n scr env opts
          = let args' = findScr env
                args = map mkarg (map getNmScr args') in
                map (mkClause args) opts
  
         where -- Find the variable we want as the scrutinee and mark it as
               -- 'True'. If the scrutinee is available in the environment,
               -- match on that otherwise match on the new argument we're adding.
               findScr ((n, (True, t)) : xs)
                          = (n, (True, t)) : scrName n xs
               findScr [(n, (_, t))] = [(n, (True, t))]
               findScr (x : xs) = x : findScr xs
               -- [] can't happen since scrutinee is in the environment!
               findScr [] = error "The impossible happened - the scrutinee was not in the environment"
  
               -- To make sure top level pattern name remains in scope, put
               -- it at the end of the environment
               scrName n []  = []
               scrName n [(_, t)] = [(n, t)]
               scrName n (x : xs) = x : scrName n xs
  
               getNmScr (n, (s, _)) = (n, s)
  
               mkarg (n, s) = (PRef fc [] n, s)
               -- may be shadowed names in the new pattern - so replace the
               -- old ones with an _
               -- Also, names which don't appear on the rhs should not be
               -- fixed on the lhs, or this restricts the kind of matching
               -- we can do to non-dependent types.
               mkClause args (l, r)
                     = let args' = map (shadowed (allNamesIn l)) args
                           args'' = map (implicitable (allNamesIn r ++
                                                       keepscrName scr)) args'
                           lhs = PApp (getFC fc l) (PRef NoFC [] n)
                                   (map (mkLHSarg l) args'') in
                              PClause (getFC fc l) n lhs [] r []
  
               -- Keep scrutinee available if it's just a name (this makes
               -- the names in scope look better when looking at a hole on
               -- the rhs of a case)
               keepscrName (PRef _ _ n) = [n]
               keepscrName _ = []
  
               mkLHSarg l (tm, True) = pexp l
               mkLHSarg l (tm, False) = pexp tm
  
               shadowed new (PRef _ _ n, s) | n `elem` new = (Placeholder, s)
               shadowed new t = t
  
               implicitable rhs (PRef _ _ n, s) | n `notElem` rhs = (Placeholder, s)
               implicitable rhs t = t
  
  
      getFC d (PApp fc _ _) = fc
      getFC d (PRef fc _ _) = fc
      getFC d (PAlternative _ _ (x:_)) = getFC d x
      getFC d x = d
  
      -- Fail if a term is not yet fully elaborated (e.g. if it contains
      -- case block functions that don't yet exist)
      fullyElaborated :: Term -> ElabD ()
      fullyElaborated (P _ n _) =
        do estate <- getAux
           case lookup n (case_decls estate) of
             Nothing -> return ()
             Just _  -> lift . tfail $ ElabScriptStaging n
      fullyElaborated (Bind n b body) = fullyElaborated body >> for_ b fullyElaborated
      fullyElaborated (App _ l r) = fullyElaborated l >> fullyElaborated r
      fullyElaborated (Proj t _) = fullyElaborated t
      fullyElaborated _ = return ()
  
      -- If the goal type is a "Lazy", then try elaborating via 'Delay'
      -- first. We need to do this brute force approach, rather than anything
      -- more precise, since there may be various other ambiguities to resolve
      -- first.
      insertLazy :: ElabCtxt -> PTerm -> ElabD PTerm
      insertLazy ina t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t
      insertLazy ina t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t
      insertLazy ina (PCoerced t) = return t
      -- Don't add a delay to top level pattern variables, since they
      -- can be forced on the rhs if needed
      insertLazy ina t@(PPatvar _ _) | pattern && not (e_guarded ina) = return t
      insertLazy ina t =
          do ty <- goal
             env <- get_env
             let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)
             let tries = [mkDelay env t, t]
             case tyh of
                  P _ (UN l) _ | l == txt "Delayed"
                      -> return (PAlternative [] FirstSuccess tries)
                  _ -> return t
        where
          mkDelay env (PAlternative ms b xs) = PAlternative ms b (map (mkDelay env) xs)
          mkDelay env t
              = let fc = fileFC "Delay" in
                    addImplBound ist (map fstEnv env) (PApp fc (PRef fc [] (sUN "Delay"))
                                                      [pexp t])
  
  
      -- Don't put implicit coercions around applications which are marked
      -- as '%noImplicit', or around case blocks, otherwise we get exponential
      -- blowup especially where there are errors deep in large expressions.
      notImplicitable (PApp _ f _) = notImplicitable f
      -- TMP HACK no coercing on bind (make this configurable)
      notImplicitable (PRef _ _ n)
          | [opts] <- lookupCtxt n (idris_flags ist)
              = NoImplicit `elem` opts
      notImplicitable (PAlternative _ _ as) = any notImplicitable as
      -- case is tricky enough without implicit coercions! If they are needed,
      -- they can go in the branches separately.
      notImplicitable (PCase _ _ _) = True
      notImplicitable _ = False
  
      -- Elaboration works more smoothly if we expand function applications
      -- to their full arity and elaborate it all at once (better error messages
      -- in particular)
      expandToArity tm@(PApp fc f a) = do
         env <- get_env
         case fullApp tm of
              -- if f is global, leave it alone because we've already
              -- expanded it to the right arity
              PApp fc ftm@(PRef _ _ f) args | Just aty <- lookupBinder f env ->
                 do let a = length (getArgTys (normalise (tt_ctxt ist) env (binderTy aty)))
                    return (mkPApp fc a ftm args)
              _ -> return tm
      expandToArity t = return t
  
      fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
      fullApp x = x
  
      -- See if the name is listed as an implicit. If it is, return it, and
      -- drop it from the rest of the list
      findImplicit :: Name -> [PArg] -> (Maybe PArg, [PArg])
      findImplicit n [] = (Nothing, [])
      findImplicit n (i@(PImp _ _ _ n' _) : args)
          | n == n' = (Just i, args)
      findImplicit n (i@(PTacImplicit _ _ n' _ _) : args)
          | n == n' = (Just i, args)
      findImplicit n (x : xs) = let (arg, rest) = findImplicit n xs in
                                    (arg, x : rest)
  
      insertScopedImps :: FC -> Name -> [Name] -> Type -> [PArg] -> ElabD [PArg]
      insertScopedImps fc f knowns ty xs =
           do mapM_ (checkKnownImplicit (map fst (getArgTys ty) ++ knowns)) xs
              doInsert ty xs
        where
          doInsert ty@(Bind n (Pi _ im@(Just i) _ _) sc) xs
            | (Just arg, xs') <- findImplicit n xs,
              not (toplevel_imp i)
                = liftM (arg :) (doInsert sc xs')
            | tcimplementation i && not (toplevel_imp i)
                = liftM (pimp n (PResolveTC fc) True :) (doInsert sc xs)
            | not (toplevel_imp i)
                = liftM (pimp n Placeholder True :) (doInsert sc xs)
          doInsert (Bind n (Pi _ _ _ _) sc) (x : xs)
                = liftM (x :) (doInsert sc xs)
          doInsert ty xs = return xs
  
          -- Any implicit in the application needs to have the name of a
          -- scoped implicit or a top level implicit, otherwise report an error
          checkKnownImplicit ns imp@(PImp{})
               | pname imp `elem` ns = return ()
               | otherwise = lift $ tfail $ At fc $ UnknownImplicit (pname imp) f
          checkKnownImplicit ns _ = return ()
  
      insertImpLam ina t =
          do ty <- goal
             env <- get_env
             let ty' = normalise (tt_ctxt ist) env ty
             addLam ty' t
        where
          -- just one level at a time
          addLam goal@(Bind n (Pi _ (Just _) _ _) sc) t =
                   do impn <- unique_hole n -- (sMN 0 "scoped_imp")
                      return (PLam emptyFC impn NoFC Placeholder t)
          addLam _ t = return t
  
      insertCoerce ina t@(PCase _ _ _) = return t
      insertCoerce ina t | notImplicitable t = return t
      insertCoerce ina t =
          do ty <- goal
             -- Check for possible coercions to get to the goal
             -- and add them as 'alternatives'
             env <- get_env
             let ty' = normalise (tt_ctxt ist) env ty
             let cs = getCoercionsTo ist ty'
             let t' = case (t, cs) of
                           (PCoerced tm, _) -> tm
                           (_, []) -> t
                           (_, cs) -> PAlternative [] TryImplicit
                                           (t : map (mkCoerce env t) cs)
             return t'
         where
           mkCoerce env (PAlternative ms aty tms) n
               = PAlternative ms aty (map (\t -> mkCoerce env t n) tms)
           mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in
                                  addImplBound ist (map fstEnv env)
                                    (PApp fc (PRef fc [] n) [pexp (PCoerced t)])
  
      elabRef :: ElabCtxt -> Maybe FC -> FC -> [FC] -> Name -> PTerm -> ElabD ()
      elabRef ina fc' fc hls n tm =
                 do fty <- get_type (Var n) -- check for implicits
                    ctxt <- get_context
                    env <- get_env
                    a' <- insertScopedImps fc n [] (normalise ctxt env fty) []
                    if null a'
                       then erun fc $
                              do apply (Var n) []
                                 hilite <- findHighlight n
                                 solve
                                 mapM_ (uncurry highlightSource) $
                                   (fc, hilite) : map (\f -> (f, hilite)) hls
                       else elab' ina fc' (PApp fc tm [])
  
      -- | Elaborate the arguments to a function
      elabArgs :: IState -- ^ The current Idris state
               -> ElabCtxt -- ^ (in an argument, guarded, in a type, in a qquote)
               -> [Bool]
               -> FC -- ^ Source location
               -> Bool
               -> Name -- ^ Name of the function being applied
               -> [((Name, Name), Bool)] -- ^ (Argument Name, Hole Name, unmatchable)
               -> Bool -- ^ under a 'force'
               -> [PTerm] -- ^ argument
               -> ElabD ()
      elabArgs ist ina failed fc retry f [] force _ = return ()
      elabArgs ist ina failed fc r f (((argName, holeName), unm):ns) force (t : args)
          = do hs <- get_holes
               if holeName `elem` hs then
                  do focus holeName
                     case t of
                        Placeholder -> do movelast holeName
                                          elabArgs ist ina failed fc r f ns force args
                        _ -> elabArg t
                  else elabArgs ist ina failed fc r f ns force args
        where elabArg t =
                do -- solveAutos ist fn False
                   now_elaborating fc f argName
                   wrapErr f argName $ do
                     hs <- get_holes
                     tm <- get_term
                     -- No coercing under an explicit Force (or it can Force/Delay
                     -- recursively!)
                     let elab = if force then elab' else elabE
                     failed' <- -- trace (show (n, t, hs, tm)) $
                                -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
                                do focus holeName;
                                   g <- goal
                                   -- Can't pattern match on polymorphic goals
                                   poly <- goal_polymorphic
                                   ulog <- getUnifyLog
                                   traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $
                                    elab (ina { e_nomatching = unm && poly }) (Just fc) t
                                   return failed
                     done_elaborating_arg f argName
                     elabArgs ist ina failed fc r f ns force args
              wrapErr f argName action =
                do elabState <- get
                   while <- elaborating_app
                   let while' = map (\(x, y, z)-> (y, z)) while
                   (result, newState) <- case runStateT action elabState of
                                           OK (res, newState) -> return (res, newState)
                                           Error e -> do done_elaborating_arg f argName
                                                         lift (tfail (elaboratingArgErr while' e))
                   put newState
                   return result
      elabArgs _ _ _ _ _ _ (((arg, hole), _) : _) _ [] =
        fail $ "Can't elaborate these args: " ++ show arg ++ " " ++ show hole
  
      addAutoBind :: Plicity -> Name -> ElabD ()
      addAutoBind (Imp _ _ _ _ False _) n
           = updateAux (\est -> est { auto_binds = n : auto_binds est })
      addAutoBind _ _ = return ()
  
      testImplicitWarning :: FC -> Name -> Type -> ElabD ()
      testImplicitWarning fc n goal
         | implicitable n && emode == ETyDecl
             = do env <- get_env
                  est <- getAux
                  when (n `elem` auto_binds est) $
                      tryUnify env (lookupTyName n (tt_ctxt ist))
         | otherwise = return ()
        where
          tryUnify env [] = return ()
          tryUnify env ((nm, ty) : ts)
               = do inj <- get_inj
                    hs <- get_holes
                    case unify (tt_ctxt ist) env (ty, Nothing) (goal, Nothing)
                            inj hs [] [] of
                      OK _ ->
                         updateAux (\est -> est { implicit_warnings =
                                            (fc, nm) : implicit_warnings est })
                      _ -> tryUnify env ts
  
  -- For every alternative, look at the function at the head. Automatically resolve
  -- any nested alternatives where that function is also at the head
  
  pruneAlt :: [PTerm] -> [PTerm]
  pruneAlt xs = map prune xs
    where
      prune (PApp fc1 (PRef fc2 hls f) as)
          = PApp fc1 (PRef fc2 hls f) (fmap (fmap (choose f)) as)
      prune t = t
  
      choose f (PAlternative ms a as)
          = let as' = fmap (choose f) as
                fs = filter (headIs f) as' in
                case fs of
                   [a] -> a
                   _ -> PAlternative ms a as'
  
      choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)
      choose f t = t
  
      headIs f (PApp _ (PRef _ _ f') _) = f == f'
      headIs f (PApp _ f' _) = headIs f f'
      headIs f _ = True -- keep if it's not an application
  
  -- | Use the local elab context to work out the highlighting for a name
  findHighlight :: Name -> ElabD OutputAnnotation
  findHighlight n = do ctxt <- get_context
                       env <- get_env
                       case lookupBinder n env of
                         Just _ -> return $ AnnBoundName n False
                         Nothing -> case lookupTyExact n ctxt of
                                      Just _ -> return $ AnnName n Nothing Nothing Nothing
                                      Nothing -> lift . tfail . InternalMsg $
                                                   "Can't find name " ++ show n
  
  -- Try again to solve auto implicits
  solveAuto :: IState -> Name -> Bool -> (Name, [FailContext]) -> ElabD ()
  solveAuto ist fn ambigok (n, failc)
    = do hs <- get_holes
         when (not (null hs)) $ do
          env <- get_env
          g <- goal
          handleError cantsolve (when (n `elem` hs) $ do
                          focus n
                          isg <- is_guess -- if it's a guess, we're working on it recursively, so stop
                          when (not isg) $
                            proofSearch' ist True ambigok 100 True Nothing fn [] [])
               (lift $ Error (addLoc failc
                     (CantSolveGoal g (map (\(n, _, b) -> (n, binderTy b)) env))))
          return ()
    where addLoc (FailContext fc f x : prev) err
             = At fc (ElaboratingArg f x
                     (map (\(FailContext _ f' x') -> (f', x')) prev) err)
          addLoc _ err = err
  
          cantsolve (CantSolveGoal _ _) = True
          cantsolve (InternalMsg _) = True
          cantsolve (At _ e) = cantsolve e
          cantsolve (Elaborating _ _ _ e) = cantsolve e
          cantsolve (ElaboratingArg _ _ _ e) = cantsolve e
          cantsolve _ = False
  
  solveAutos :: IState -> Name -> Bool -> ElabD ()
  solveAutos ist fn ambigok
             = do autos <- get_autos
                  mapM_ (solveAuto ist fn ambigok) (map (\(n, (fc, _)) -> (n, fc)) autos)
  
  -- Return true if the given error suggests an interface failure is
  -- recoverable
  tcRecoverable :: ElabMode -> Err -> Bool
  tcRecoverable ERHS (CantResolve f g _) = f
  tcRecoverable ETyDecl (CantResolve f g _) = f
  tcRecoverable e (ElaboratingArg _ _ _ err) = tcRecoverable e err
  tcRecoverable e (At _ err) = tcRecoverable e err
  tcRecoverable _ _ = True
  
  trivial' ist
      = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
  trivialHoles' psn h ist
      = trivialHoles psn h (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
  proofSearch' ist rec ambigok depth prv top n psns hints
      = do unifyProblems
           proofSearch rec prv ambigok (not prv) depth
                       (elab ist toplevel ERHS [] (sMN 0 "tac")) top n psns hints ist
  resolveTC' di mv depth tm n ist
      = resolveTC di mv depth tm n (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
  
  collectDeferred :: Maybe Name -> [Name] -> Context ->
                     Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term
  collectDeferred top casenames ctxt tm = cd [] tm
    where
      cd env (Bind n (GHole i psns t) app) =
          do ds <- get
             t' <- collectDeferred top casenames ctxt t
             when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t', psns))])
             cd env app
      cd env (Bind n b t)
           = do b' <- cdb b
                t' <- cd ((n, b) : env) t
                return (Bind n b' t')
        where
          cdb (Let rig t v) = liftM2 (Let rig) (cd env t) (cd env v)
          cdb (Guess t v) = liftM2 Guess (cd env t) (cd env v)
          cdb b           = do ty' <- cd env (binderTy b)
                               return (b { binderTy = ty' })
      cd env (App s f a) = liftM2 (App s) (cd env f)
                                          (cd env a)
      cd env t = return t
  
  -- | Compute the appropriate name for a top-level metavariable
  metavarName :: [String] -> Name -> Name
  metavarName _          n@(NS _ _) = n
  metavarName (ns@(_:_)) n          = sNS n ns
  metavarName _          n          = n
  
  runElabAction :: ElabInfo -> IState -> FC -> Env -> Term -> [String] -> ElabD Term
  runElabAction info ist fc env tm ns = do tm' <- eval tm
                                           runTacTm tm'
  
    where
      eval tm = do ctxt <- get_context
                   return $ normaliseAll ctxt env (finalise tm)
  
      returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased)
  
      patvars :: [(Name, Term)] -> Term -> ([(Name, Term)], Term)
      patvars ns (Bind n (PVar _ t) sc) = patvars ((n, t) : ns) (instantiate (P Bound n t) sc)
      patvars ns tm                   = (ns, tm)
  
      pullVars :: (Term, Term) -> ([(Name, Term)], Term, Term)
      pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs
  
      requireError :: Err -> ElabD a -> ElabD ()
      requireError orErr elab =
        do state <- get
           case runStateT elab state of
             OK (_, state') -> lift (tfail orErr)
             Error e -> return ()
  
      -- create a fake TT term for the LHS of an impossible case
      fakeTT :: Raw -> Term
      fakeTT (Var n) =
        case lookupNameDef n (tt_ctxt ist) of
          [(n', TyDecl nt _)] -> P nt n' Erased
          _ -> P Ref n Erased
      fakeTT (RBind n b body) = Bind n (fmap fakeTT b) (fakeTT body)
      fakeTT (RApp f a) = App Complete (fakeTT f) (fakeTT a)
      fakeTT RType = TType (UVar [] (-1))
      fakeTT (RUType u) = UType u
      fakeTT (RConstant c) = Constant c
  
      defineFunction :: RFunDefn Raw -> ElabD ()
      defineFunction (RDefineFun n clauses) =
        do ctxt <- get_context
           ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt
           let info = CaseInfo True True False -- TODO document and figure out
           clauses' <- forM clauses (\case
                                        RMkFunClause lhs rhs ->
                                          do (lhs', lty) <- lift $ check ctxt [] lhs
                                             (rhs', rty) <- lift $ check ctxt [] rhs
                                             lift $ converts ctxt [] lty rty
                                             return $ Right (lhs', rhs')
                                        RMkImpossibleClause lhs ->
                                          do requireError (Msg "Not an impossible case") . lift $
                                               check ctxt [] lhs
                                             return $ Left (fakeTT lhs))
           let clauses'' = map (\case Right c -> pullVars c
                                      Left lhs -> let (ns, lhs') = patvars [] lhs
                                                  in (ns, lhs', Impossible))
                              clauses'
           let clauses''' = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses''
           let argtys = map (\x -> (x, isCanonical x ctxt))
                            (map snd (getArgTys (normalise ctxt [] ty)))
           ctxt'<- lift $
                    addCasedef n (const [])
                               info False (STerm Erased)
                               True False -- TODO what are these?
                               argtys [] -- TODO inaccessible types
                               clauses'
                               clauses'''
                               clauses'''
                               ty
                               ctxt
           set_context ctxt'
           updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}
           return ()
  
  
      checkClosed :: Raw -> Elab' aux (Term, Type)
      checkClosed tm = do ctxt <- get_context
                          (val, ty) <- lift $ check ctxt [] tm
                          return $! (finalise val, finalise ty)
  
      -- | Add another argument to a Pi
      mkPi :: RFunArg -> Raw -> Raw
      mkPi arg rTy = RBind (argName arg) (Pi RigW Nothing (argTy arg) (RUType AllTypes)) rTy
  
      mustBeType ctxt tm ty =
        case normaliseAll ctxt [] (finalise ty) of
          UType _ -> return ()
          TType _ -> return ()
          ty'    -> lift . tfail . InternalMsg $
                       show tm ++ " is not a type: it's " ++ show ty'
  
      mustNotBeDefined ctxt n =
        case lookupDefExact n ctxt of
          Just _ -> lift . tfail . InternalMsg $
                      show n ++ " is already defined."
          Nothing -> return ()
  
      -- | Prepare a constructor to be added to a datatype being defined here
      prepareConstructor :: Name -> RConstructorDefn -> ElabD (Name, [PArg], Type)
      prepareConstructor tyn (RConstructor cn args resTy) =
        do ctxt <- get_context
           -- ensure the constructor name is not qualified, and
           -- construct a qualified one
           notQualified cn
           let qcn = qualify cn
  
           -- ensure that the constructor name is not defined already
           mustNotBeDefined ctxt qcn
  
           -- construct the actual type for the constructor
           let cty = foldr mkPi resTy args
           (checkedTy, ctyTy) <- lift $ check ctxt [] cty
           mustBeType ctxt checkedTy ctyTy
  
           -- ensure that the constructor builds the right family
           case unApply (getRetTy (normaliseAll ctxt [] (finalise checkedTy))) of
             (P _ n _, _) | n == tyn -> return ()
             t -> lift . tfail . Msg $ "The constructor " ++ show cn ++
                                       " doesn't construct " ++ show tyn ++
                                       " (return type is " ++ show t ++ ")"
  
           -- add temporary type declaration for constructor (so it can
           -- occur in later constructor types)
           set_context (addTyDecl qcn (DCon 0 0 False) checkedTy ctxt)
  
           -- Save the implicits for high-level Idris
           let impls = map rFunArgToPArg args
  
           return (qcn, impls, checkedTy)
  
        where
          notQualified (NS _ _) = lift . tfail . Msg $ "Constructor names may not be qualified"
          notQualified _ = return ()
  
          qualify n = case tyn of
                        (NS _ ns) -> NS n ns
                        _ -> n
  
          getRetTy :: Type -> Type
          getRetTy (Bind _ (Pi _ _ _ _) sc) = getRetTy sc
          getRetTy ty = ty
  
      elabScriptStuck :: Term -> ElabD a
      elabScriptStuck x = lift . tfail $ ElabScriptStuck x
  
  
      -- Should be dependent
      tacTmArgs :: Int -> Term -> [Term] -> ElabD [Term]
      tacTmArgs l t args | length args == l = return args
                         | otherwise        = elabScriptStuck t -- Probably should be an argument size mismatch internal error
  
  
      -- | Do a step in the reflected elaborator monad. The input is the
      -- step, the output is the (reflected) term returned.
      runTacTm :: Term -> ElabD Term
      runTacTm tac@(unApply -> (P _ n _, args))
        | n == tacN "Prim__Solve"
        = do ~[] <- tacTmArgs 0 tac args -- patterns are irrefutable because `tacTmArgs` returns lists of exactly the size given to it as first argument
             solve
             returnUnit
        | n == tacN "Prim__Goal"
        = do ~[] <- tacTmArgs 0 tac args
             hs <- get_holes
             case hs of
               (h : _) -> do t <- goal
                             fmap fst . checkClosed $
                               rawPair (Var (reflm "TTName"), Var (reflm "TT"))
                                       (reflectName h,        reflect t)
               [] -> lift . tfail . Msg $
                       "Elaboration is complete. There are no goals."
  
        | n == tacN "Prim__Holes"
        = do ~[] <- tacTmArgs 0 tac args
             hs <- get_holes
             fmap fst . checkClosed $
               mkList (Var $ reflm "TTName") (map reflectName hs)
        | n == tacN "Prim__Guess"
        = do ~[] <- tacTmArgs 0 tac args
             g <- get_guess
             fmap fst . checkClosed $ reflect g
        | n == tacN "Prim__LookupTy"
        = do ~[name] <- tacTmArgs 1 tac args
             n' <- reifyTTName name
             ctxt <- get_context
             let getNameTypeAndType = \case Function ty _       -> (Ref, ty)
                                            TyDecl nt ty        -> (nt, ty)
                                            Operator ty _ _     -> (Ref, ty)
                                            CaseOp _ ty _ _ _ _ -> (Ref, ty)
                 -- Idris tuples nest to the right
                 reflectTriple (x, y, z) =
                   raw_apply (Var pairCon) [ Var (reflm "TTName")
                                           , raw_apply (Var pairTy) [Var (reflm "NameType"), Var (reflm "TT")]
                                           , x
                                           , raw_apply (Var pairCon) [ Var (reflm "NameType"), Var (reflm "TT")
                                                                     , y, z]]
             let defs = [ reflectTriple (reflectName n, reflectNameType nt, reflect ty)
                          | (n, def) <- lookupNameDef n' ctxt
                          , let (nt, ty) = getNameTypeAndType def ]
             fmap fst . checkClosed $
               rawList (raw_apply (Var pairTy) [ Var (reflm "TTName")
                                               , raw_apply (Var pairTy) [ Var (reflm "NameType")
                                                                         , Var (reflm "TT")]])
                       defs
        | n == tacN "Prim__LookupDatatype"
        = do ~[name] <- tacTmArgs 1 tac args
             n' <- reifyTTName name
             datatypes <- get_datatypes
             ctxt <- get_context
             fmap fst . checkClosed $
               rawList (Var (tacN "Datatype"))
                       (map reflectDatatype (buildDatatypes ist n'))
        | n == tacN "Prim__LookupFunDefn"
        = do ~[name] <- tacTmArgs 1 tac args
             n' <- reifyTTName name
             fmap fst . checkClosed $
               rawList (RApp (Var $ tacN "FunDefn") (Var $ reflm "TT"))
                 (map reflectFunDefn (buildFunDefns ist n'))
        | n == tacN "Prim__LookupArgs"
        = do ~[name] <- tacTmArgs 1 tac args
             n' <- reifyTTName name
             let listTy = Var (sNS (sUN "List") ["List", "Prelude"])
                 listFunArg = RApp listTy (Var (tacN "FunArg"))
              -- Idris tuples nest to the right
             let reflectTriple (x, y, z) =
                   raw_apply (Var pairCon) [ Var (reflm "TTName")
                                           , raw_apply (Var pairTy) [listFunArg, Var (reflm "Raw")]
                                           , x
                                           , raw_apply (Var pairCon) [listFunArg, Var (reflm "Raw")
                                                                     , y, z]]
             let out =
                   [ reflectTriple (reflectName fn, reflectList (Var (tacN "FunArg")) (map reflectArg args), reflectRaw res)
                   | (fn, pargs) <- lookupCtxtName n' (idris_implicits ist)
                   , (args, res) <- getArgs pargs . forget <$>
                                     maybeToList (lookupTyExact fn (tt_ctxt ist))
                   ]
  
             fmap fst . checkClosed $
               rawList (raw_apply (Var pairTy) [Var (reflm "TTName")
                                               , raw_apply (Var pairTy) [ RApp listTy
                                                                               (Var (tacN "FunArg"))
                                                                        , Var (reflm "Raw")]])
                       out
        | n == tacN "Prim__SourceLocation"
        = do ~[] <- tacTmArgs 0 tac args
             fmap fst . checkClosed $
               reflectFC fc
        | n == tacN "Prim__Namespace"
        = do ~[] <- tacTmArgs 0 tac args
             fmap fst . checkClosed $
               rawList (RConstant StrType) (map (RConstant . Str) ns)
        | n == tacN "Prim__Env"
        = do ~[] <- tacTmArgs 0 tac args
             env <- get_env
             fmap fst . checkClosed $ reflectEnv env
        | n == tacN "Prim__Fail"
        = do ~[_a, errs] <- tacTmArgs 2 tac args
             errs' <- eval errs
             parts <- reifyReportParts errs'
             lift . tfail $ ReflectionError [parts] (Msg "")
        | n == tacN "Prim__PureElab"
        = do ~[_a, tm] <- tacTmArgs 2 tac args
             return tm
        | n == tacN "Prim__BindElab"
        = do ~[_a, _b, first, andThen] <- tacTmArgs 4 tac args
             first' <- eval first
             res <- eval =<< runTacTm first'
             next <- eval (App Complete andThen res)
             runTacTm next
        | n == tacN "Prim__Try"
        = do ~[_a, first, alt] <- tacTmArgs 3 tac args
             first' <- eval first
             alt' <- eval alt
             try' (runTacTm first') (runTacTm alt') True
        | n == tacN "Prim__TryCatch"
        = do ~[_a, first, f] <- tacTmArgs 3 tac args
             first' <- eval first
             f' <- eval f
             tryCatch (runTacTm first') $ \err ->
               do (err', _) <- checkClosed (reflectErr err)
                  f' <- eval (App Complete f err')
                  runTacTm f'
        | n == tacN "Prim__Fill"
        = do ~[raw] <- tacTmArgs 1 tac args
             raw' <- reifyRaw =<< eval raw
             apply raw' []
             returnUnit
        | n == tacN "Prim__Apply" || n == tacN "Prim__MatchApply"
        = do ~[raw, argSpec] <- tacTmArgs 2 tac args
             raw' <- reifyRaw =<< eval raw
             argSpec' <- map (\b -> (b, 0)) <$> reifyList reifyBool argSpec
             let op = if n == tacN "Prim__Apply"
                         then apply
                         else match_apply
             ns <- op raw' argSpec'
             fmap fst . checkClosed $
               rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TTName"))
                       [ rawPair (Var $ reflm "TTName", Var $ reflm "TTName")
                                 (reflectName n1, reflectName n2)
                       | (n1, n2) <- ns
                       ]
        | n == tacN "Prim__Gensym"
        = do ~[hint] <- tacTmArgs 1 tac args
             hintStr <- eval hint
             case hintStr of
               Constant (Str h) -> do
                 n <- getNameFrom (sMN 0 h)
                 fmap fst $ get_type_val (reflectName n)
               _ -> fail "no hint"
        | n == tacN "Prim__Claim"
        = do ~[n, ty] <- tacTmArgs 2 tac args
             n' <- reifyTTName n
             ty' <- reifyRaw ty
             claim n' ty'
             returnUnit
        | n == tacN "Prim__Check"
        = do ~[env', raw] <- tacTmArgs 2 tac args
             env <- reifyEnv env'
             raw' <- reifyRaw =<< eval raw
             ctxt <- get_context
             (tm, ty) <- lift $ check ctxt env raw'
             fmap fst . checkClosed $
               rawPair (Var (reflm "TT"), Var (reflm "TT"))
                       (reflect tm,       reflect ty)
        | n == tacN "Prim__Attack"
        = do ~[] <- tacTmArgs 0 tac args
             attack
             returnUnit
        | n == tacN "Prim__Rewrite"
        = do ~[rule] <- tacTmArgs 1 tac args
             r <- reifyRaw rule
             rewrite r
             returnUnit
        | n == tacN "Prim__Focus"
        = do ~[what] <- tacTmArgs 1 tac args
             n' <- reifyTTName what
             hs <- get_holes
             if elem n' hs
                then focus n' >> returnUnit
                else lift . tfail . Msg $ "The name " ++ show n' ++ " does not denote a hole"
        | n == tacN "Prim__Unfocus"
        = do ~[what] <- tacTmArgs 1 tac args
             n' <- reifyTTName what
             movelast n'
             returnUnit
        | n == tacN "Prim__Intro"
        = do ~[mn] <- tacTmArgs 1 tac args
             n <- case fromTTMaybe mn of
                    Nothing -> return Nothing
                    Just name -> fmap Just $ reifyTTName name
             intro n
             returnUnit
        | n == tacN "Prim__Forall"
        = do ~[n, ty] <- tacTmArgs 2 tac args
             n' <- reifyTTName n
             ty' <- reifyRaw ty
             forAll n' RigW Nothing ty'
             returnUnit
        | n == tacN "Prim__PatVar"
        = do ~[n] <- tacTmArgs 1 tac args
             n' <- reifyTTName n
             patvar' n'
             returnUnit
        | n == tacN "Prim__PatBind"
        = do ~[n] <- tacTmArgs 1 tac args
             n' <- reifyTTName n
             patbind n' RigW
             returnUnit
        | n == tacN "Prim__LetBind"
        = do ~[n, ty, tm] <- tacTmArgs 3 tac args
             n' <- reifyTTName n
             ty' <- reifyRaw ty
             tm' <- reifyRaw tm
             letbind n' RigW ty' tm'
             returnUnit
        | n == tacN "Prim__Compute"
        = do ~[] <- tacTmArgs 0 tac args; compute ; returnUnit
        | n == tacN "Prim__Normalise"
        = do ~[env, tm] <- tacTmArgs 2 tac args
             env' <- reifyEnv env
             tm' <- reifyTT tm
             ctxt <- get_context
             let out = normaliseAll ctxt env' (finalise tm')
             fmap fst . checkClosed $ reflect out
        | n == tacN "Prim__Whnf"
        = do ~[tm] <- tacTmArgs 1 tac args
             tm' <- reifyTT tm
             ctxt <- get_context
             fmap fst . checkClosed . reflect $ whnf ctxt [] tm'
        | n == tacN "Prim__Converts"
        = do ~[env, tm1, tm2] <- tacTmArgs 3 tac args
             env' <- reifyEnv env
             tm1' <- reifyTT tm1
             tm2' <- reifyTT tm2
             ctxt <- get_context
             lift $ converts ctxt env' tm1' tm2'
             returnUnit
        | n == tacN "Prim__DeclareType"
        = do ~[decl] <- tacTmArgs 1 tac args
             (RDeclare n args res) <- reifyTyDecl decl
             ctxt <- get_context
             let rty = foldr mkPi res args
             (checked, ty') <- lift $ check ctxt [] rty
             mustBeType ctxt checked ty'
             mustNotBeDefined ctxt n
             let decl = TyDecl Ref checked
                 ctxt' = addCtxtDef n decl ctxt
             set_context ctxt'
             updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
                                                 new_tyDecls e }
             returnUnit
        | n == tacN "Prim__DefineFunction"
        = do ~[decl] <- tacTmArgs 1 tac args
             defn <- reifyFunDefn decl
             defineFunction defn
             returnUnit
        | n == tacN "Prim__DeclareDatatype"
        = do ~[decl] <- tacTmArgs 1 tac args
             RDeclare n args resTy <- reifyTyDecl decl
             ctxt <- get_context
             let tcTy = foldr mkPi resTy args
             (checked, ty') <- lift $ check ctxt [] tcTy
             mustBeType ctxt checked ty'
             mustNotBeDefined ctxt n
             let ctxt' = addTyDecl n (TCon 0 0) checked ctxt
             set_context ctxt'
             updateAux $ \e -> e { new_tyDecls = RDatatypeDeclInstrs n (map rFunArgToPArg args) : new_tyDecls e }
             returnUnit
        | n == tacN "Prim__DefineDatatype"
        = do ~[defn] <- tacTmArgs 1 tac args
             RDefineDatatype n ctors <- reifyRDataDefn defn
             ctxt <- get_context
             tyconTy <- case lookupTyExact n ctxt of
                          Just t -> return t
                          Nothing -> lift . tfail . Msg $ "Type not previously declared"
             datatypes <- get_datatypes
             case lookupCtxtName n datatypes of
               [] -> return ()
               _  -> lift . tfail . Msg $ show n ++ " is already defined as a datatype."
             -- Prepare the constructors
             ctors' <- mapM (prepareConstructor n) ctors
             ttag <- do ES (ps, aux) str prev <- get
                        let i = global_nextname ps
                        put $ ES (ps { global_nextname = global_nextname ps + 1 },
                                  aux)
                                 str
                                 prev
                        return i
             let ctxt' = addDatatype (Data n ttag tyconTy False (map (\(cn, _, cty) -> (cn, cty)) ctors')) ctxt
             set_context ctxt'
             -- the rest happens in a bit
             updateAux $ \e -> e { new_tyDecls = RDatatypeDefnInstrs n tyconTy ctors' : new_tyDecls e }
             returnUnit
        | n == tacN "Prim__AddImplementation"
        = do ~[cls, impl] <- tacTmArgs 2 tac args
             interfaceName <- reifyTTName cls
             implName <- reifyTTName impl
             updateAux $ \e -> e { new_tyDecls = RAddImplementation interfaceName implName :
                                                 new_tyDecls e }
             returnUnit
        | n == tacN "Prim__IsTCName"
        = do ~[n] <- tacTmArgs 1 tac args
             n' <- reifyTTName n
             case lookupCtxtExact n' (idris_interfaces ist) of
               Just _ -> fmap fst . checkClosed $ Var (sNS (sUN "True") ["Bool", "Prelude"])
               Nothing -> fmap fst . checkClosed $ Var (sNS (sUN "False") ["Bool", "Prelude"])
        | n == tacN "Prim__ResolveTC"
        = do ~[fn] <- tacTmArgs 1 tac args
             g <- goal
             fn <- reifyTTName fn
             resolveTC' False True 100 g fn ist
             returnUnit
        | n == tacN "Prim__Search"
        = do ~[depth, hints] <- tacTmArgs 2 tac args
             d <- eval depth
             hints' <- eval hints
             case (d, unList hints') of
               (Constant (I i), Just hs) ->
                 do actualHints <- mapM reifyTTName hs
                    unifyProblems
                    let psElab = elab ist toplevel ERHS [] (sMN 0 "tac")
                    proofSearch True True False False i psElab Nothing (sMN 0 "search ") [] actualHints ist
                    returnUnit
               (Constant (I _), Nothing ) ->
                 lift . tfail . InternalMsg $ "Not a list: " ++ show hints'
               (_, _) -> lift . tfail . InternalMsg $ "Can't reify int " ++ show d
        | n == tacN "Prim__RecursiveElab"
        = do ~[goal, script] <- tacTmArgs 2 tac args
             goal' <- reifyRaw goal
             ctxt <- get_context
             script <- eval script
             (goalTT, goalTy) <- lift $ check ctxt [] goal'
             lift $ isType ctxt [] goalTy
             recH <- getNameFrom (sMN 0 "recElabHole")
             aux <- getAux
             datatypes <- get_datatypes
             env <- get_env
             g_next <- get_global_nextname
  
             (ctxt', ES (p, aux') _ _) <-
                do (ES (current_p, _) _ _) <- get
                   lift $ runElab aux
                               (do runElabAction info ist fc [] script ns
                                   ctxt' <- get_context
                                   return ctxt')
                               ((newProof recH (constraintNS info) ctxt datatypes g_next goalTT)
                                { nextname = nextname current_p })
             set_context ctxt'
  
             let tm_out = getProofTerm (pterm p)
             do (ES (prf, _) s e) <- get
                let p' = prf { nextname = nextname p
                             , global_nextname = global_nextname p
                             }
                put (ES (p', aux') s e)
             env' <- get_env
             (tm, ty, _) <- lift $ recheck (constraintNS info) ctxt' env (forget tm_out) tm_out
             let (tm', ty') = (reflect tm, reflect ty)
             fmap fst . checkClosed $
               rawPair (Var $ reflm "TT", Var $ reflm "TT")
                       (tm', ty')
        | n == tacN "Prim__Metavar"
        = do ~[n] <- tacTmArgs 1 tac args
             n' <- reifyTTName n
             ctxt <- get_context
             ptm <- get_term
             -- See documentation above in the elab case for PMetavar
             let unique_used = getUniqueUsed ctxt ptm
             let lin_used = getLinearUsed ctxt ptm
             let mvn = metavarName ns n'
             attack
             defer unique_used lin_used mvn
             solve
             returnUnit
        | n == tacN "Prim__Fixity"
        = do ~[op'] <- tacTmArgs 1 tac args
             opTm <- eval op'
             case opTm of
               Constant (Str op) ->
                 let opChars = ":!#$%&*+./<=>?@\\^|-~"
                     invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"]
                     fixities = idris_infixes ist
                 in if not (all (flip elem opChars) op) || elem op invalidOperators
                       then lift . tfail . Msg $ "'" ++ op ++ "' is not a valid operator name."
                       else case nub [f | Fix f someOp <- fixities, someOp == op] of
                              []   -> lift . tfail . Msg $ "No fixity found for operator '" ++ op ++ "'."
                              [f]  -> fmap fst . checkClosed $ reflectFixity f
                              many -> lift . tfail . InternalMsg $ "Ambiguous fixity for '" ++ op ++ "'!  Found " ++ show many
               _ -> lift . tfail . Msg $ "Not a constant string for an operator name: " ++ show opTm
        | n == tacN "Prim__Debug"
        = do ~[ty, msg] <- tacTmArgs 2 tac args
             msg' <- eval msg
             parts <- reifyReportParts msg
             debugElaborator parts
      runTacTm x = elabScriptStuck x
  
  -- Running tactics directly
  -- if a tactic adds unification problems, return an error
  
  runTac :: Bool -> IState -> Maybe FC -> Name -> PTactic -> ElabD ()
  runTac autoSolve ist perhapsFC fn tac
      = do env <- get_env
           g <- goal
           let tac' = fmap (addImplBound ist (map fstEnv env)) tac
           if autoSolve
              then runT tac'
              else no_errors (runT tac')
                     (Just (CantSolveGoal g (map (\(n, _, b) -> (n, binderTy b)) env)))
    where
      runT (Intro []) = do g <- goal
                           attack; intro (bname g)
        where
          bname (Bind n _ _) = Just n
          bname _ = Nothing
      runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs
      runT Intros = do g <- goal
                       attack;
                       intro (bname g)
                       try' (runT Intros)
                            (return ()) True
        where
          bname (Bind n _ _) = Just n
          bname _ = Nothing
      runT (Exact tm) = do elab ist toplevel ERHS [] (sMN 0 "tac") tm
                           when autoSolve solveAll
      runT (MatchRefine fn)
          = do fnimps <-
                 case lookupCtxtName fn (idris_implicits ist) of
                      [] -> do a <- envArgs fn
                               return [(fn, a)]
                      ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns)
               let tacs = map (\ (fn', imps) ->
                                   (match_apply (Var fn') (map (\x -> (x, 0)) imps),
                                       fn')) fnimps
               tryAll tacs
               when autoSolve solveAll
         where envArgs n = do e <- get_env
                              case lookupBinder n e of
                                 Just t -> return $ map (const False)
                                                        (getArgTys (binderTy t))
                                 _ -> return []
      runT (Refine fn [])
          = do fnimps <-
                 case lookupCtxtName fn (idris_implicits ist) of
                      [] -> do a <- envArgs fn
                               return [(fn, a)]
                      ns -> return (map (\ (n, a) -> (n, map isImp a)) ns)
               let tacs = map (\ (fn', imps) ->
                                   (apply (Var fn') (map (\x -> (x, 0)) imps),
                                       fn')) fnimps
               tryAll tacs
               when autoSolve solveAll
         where isImp (PImp _ _ _ _ _) = True
               isImp _ = False
               envArgs n = do e <- get_env
                              case lookupBinder n e of
                                 Just t -> return $ map (const False)
                                                        (getArgTys (binderTy t))
                                 _ -> return []
      runT (Refine fn imps) = do ns <- apply (Var fn) (map (\x -> (x,0)) imps)
                                 when autoSolve solveAll
      runT DoUnify = do unify_all
                        when autoSolve solveAll
      runT (Claim n tm) = do tmHole <- getNameFrom (sMN 0 "newGoal")
                             claim tmHole RType
                             claim n (Var tmHole)
                             focus tmHole
                             elab ist toplevel ERHS [] (sMN 0 "tac") tm
                             focus n
      runT (Equiv tm) -- let bind tm, then
                = do attack
                     tyn <- getNameFrom (sMN 0 "ety")
                     claim tyn RType
                     valn <- getNameFrom (sMN 0 "eqval")
                     claim valn (Var tyn)
                     letn <- getNameFrom (sMN 0 "equiv_val")
                     letbind letn RigW (Var tyn) (Var valn)
                     focus tyn
                     elab ist toplevel ERHS [] (sMN 0 "tac") tm
                     focus valn
                     when autoSolve solveAll
      runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that
                = do attack; -- (h:_) <- get_holes
                     tyn <- getNameFrom (sMN 0 "rty")
                     -- start_unify h
                     claim tyn RType
                     valn <- getNameFrom (sMN 0 "rval")
                     claim valn (Var tyn)
                     letn <- getNameFrom (sMN 0 "rewrite_rule")
                     letbind letn RigW (Var tyn) (Var valn)
                     focus valn
                     elab ist toplevel ERHS [] (sMN 0 "tac") tm
                     rewrite (Var letn)
                     when autoSolve solveAll
      runT (LetTac n tm)
                = do attack
                     tyn <- getNameFrom (sMN 0 "letty")
                     claim tyn RType
                     valn <- getNameFrom (sMN 0 "letval")
                     claim valn (Var tyn)
                     letn <- unique_hole n
                     letbind letn RigW (Var tyn) (Var valn)
                     focus valn
                     elab ist toplevel ERHS [] (sMN 0 "tac") tm
                     when autoSolve solveAll
      runT (LetTacTy n ty tm)
                = do attack
                     tyn <- getNameFrom (sMN 0 "letty")
                     claim tyn RType
                     valn <- getNameFrom (sMN 0 "letval")
                     claim valn (Var tyn)
                     letn <- unique_hole n
                     letbind letn RigW (Var tyn) (Var valn)
                     focus tyn
                     elab ist toplevel ERHS [] (sMN 0 "tac") ty
                     focus valn
                     elab ist toplevel ERHS [] (sMN 0 "tac") tm
                     when autoSolve solveAll
      runT Compute = compute
      runT Trivial = do trivial' ist; when autoSolve solveAll
      runT TCImplementation = runT (Exact (PResolveTC emptyFC))
      runT (ProofSearch rec prover depth top psns hints)
           = do proofSearch' ist rec False depth prover top fn psns hints
                when autoSolve solveAll
      runT (Focus n) = focus n
      runT Unfocus = do hs <- get_holes
                        case hs of
                          []      -> return ()
                          (h : _) -> movelast h
      runT Solve = solve
      runT (Try l r) = do try' (runT l) (runT r) True
      runT (TSeq l r) = do runT l; runT r
      runT (ApplyTactic tm) = do tenv <- get_env -- store the environment
                                 tgoal <- goal -- store the goal
                                 attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...
                                 script <- getNameFrom (sMN 0 "script")
                                 claim script scriptTy
                                 scriptvar <- getNameFrom (sMN 0 "scriptvar" )
                                 letbind scriptvar RigW scriptTy (Var script)
                                 focus script
                                 elab ist toplevel ERHS [] (sMN 0 "tac") tm
                                 (script', _) <- get_type_val (Var scriptvar)
                                 -- now that we have the script apply
                                 -- it to the reflected goal and context
                                 restac <- getNameFrom (sMN 0 "restac")
                                 claim restac tacticTy
                                 focus restac
                                 fill (raw_apply (forget script')
                                                 [reflectEnv tenv, reflect tgoal])
                                 restac' <- get_guess
                                 solve
                                 -- normalise the result in order to
                                 -- reify it
                                 ctxt <- get_context
                                 env <- get_env
                                 let tactic = normalise ctxt env restac'
                                 runReflected tactic
          where tacticTy = Var (reflm "Tactic")
                listTy = Var (sNS (sUN "List") ["List", "Prelude"])
                scriptTy = (RBind (sMN 0 "__pi_arg")
                                  (Pi RigW Nothing (RApp listTy envTupleType) RType)
                                      (RBind (sMN 1 "__pi_arg")
                                             (Pi RigW Nothing (Var $ reflm "TT") RType) tacticTy))
      runT (ByReflection tm) -- run the reflection function 'tm' on the
                             -- goal, then apply the resulting reflected Tactic
          = do tgoal <- goal
               attack
               script <- getNameFrom (sMN 0 "script")
               claim script scriptTy
               scriptvar <- getNameFrom (sMN 0 "scriptvar" )
               letbind scriptvar RigW scriptTy (Var script)
               focus script
               ptm <- get_term
               env <- get_env
               let denv = map (\(n, _, b) -> (n, binderTy b)) env
               elab ist toplevel ERHS [] (sMN 0 "tac")
                    (PApp emptyFC tm [pexp (delabTy' ist [] denv tgoal True True True)])
               (script', _) <- get_type_val (Var scriptvar)
               -- now that we have the script apply
               -- it to the reflected goal
               restac <- getNameFrom (sMN 0 "restac")
               claim restac tacticTy
               focus restac
               fill (forget script')
               restac' <- get_guess
               solve
               -- normalise the result in order to
               -- reify it
               ctxt <- get_context
               env <- get_env
               let tactic = normalise ctxt env restac'
               runReflected tactic
        where tacticTy = Var (reflm "Tactic")
              scriptTy = tacticTy
  
      runT (Reflect v) = do attack -- let x = reflect v in ...
                            tyn <- getNameFrom (sMN 0 "letty")
                            claim tyn RType
                            valn <- getNameFrom (sMN 0 "letval")
                            claim valn (Var tyn)
                            letn <- getNameFrom (sMN 0 "letvar")
                            letbind letn RigW (Var tyn) (Var valn)
                            focus valn
                            elab ist toplevel ERHS [] (sMN 0 "tac") v
                            (value, _) <- get_type_val (Var letn)
                            ctxt <- get_context
                            env <- get_env
                            let value' = normalise ctxt env value
                            runTac autoSolve ist perhapsFC fn (Exact $ PQuote (reflect value'))
      runT (Fill v) = do attack -- let x = fill x in ...
                         tyn <- getNameFrom (sMN 0 "letty")
                         claim tyn RType
                         valn <- getNameFrom (sMN 0 "letval")
                         claim valn (Var tyn)
                         letn <- getNameFrom (sMN 0 "letvar")
                         letbind letn RigW (Var tyn) (Var valn)
                         focus valn
                         elab ist toplevel ERHS [] (sMN 0 "tac") v
                         (value, _) <- get_type_val (Var letn)
                         ctxt <- get_context
                         env <- get_env
                         let value' = normalise ctxt env value
                         rawValue <- reifyRaw value'
                         runTac autoSolve ist perhapsFC fn (Exact $ PQuote rawValue)
      runT (GoalType n tac) = do g <- goal
                                 case unApply g of
                                      (P _ n' _, _) ->
                                         if nsroot n' == sUN n
                                            then runT tac
                                            else fail "Wrong goal type"
                                      _ -> fail "Wrong goal type"
      runT ProofState = do g <- goal
                           return ()
      runT Skip = return ()
      runT (TFail err) = lift . tfail $ ReflectionError [err] (Msg "")
      runT SourceFC =
        case perhapsFC of
          Nothing -> lift . tfail $ Msg "There is no source location available."
          Just fc ->
            do fill $ reflectFC fc
               solve
      runT Qed = lift . tfail $ Msg "The qed command is only valid in the interactive prover"
      runT x = fail $ "Not implemented " ++ show x
  
      runReflected t = do t' <- reify ist t
                          runTac autoSolve ist perhapsFC fn t'
  
  elaboratingArgErr :: [(Name, Name)] -> Err -> Err
  elaboratingArgErr [] err = err
  elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
    where rewrite (ElaboratingArg _ _ _ _) = Nothing
          rewrite (ProofSearchFail e) = fmap ProofSearchFail (rewrite e)
          rewrite (At fc e) = fmap (At fc) (rewrite e)
          rewrite err = Just (ElaboratingArg f x during err)
  
  
  withErrorReflection :: Idris a -> Idris a
  withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
      where handle :: Err -> Idris Err
            handle e@(ReflectionError _ _)  = do logElab 3 "Skipping reflection of error reflection result"
                                                 return e -- Don't do meta-reflection of errors
            handle e@(ReflectionFailed _ _) = do logElab 3 "Skipping reflection of reflection failure"
                                                 return e
            -- At and Elaborating are just plumbing - error reflection shouldn't rewrite them
            handle e@(At fc err) = do logElab 3 "Reflecting body of At"
                                      err' <- handle err
                                      return (At fc err')
            handle e@(Elaborating what n ty err) = do logElab 3 "Reflecting body of Elaborating"
                                                      err' <- handle err
                                                      return (Elaborating what n ty err')
            handle e@(ElaboratingArg f a prev err) = do logElab 3 "Reflecting body of ElaboratingArg"
                                                        hs <- getFnHandlers f a
                                                        err' <- if null hs
                                                                   then handle err
                                                                   else applyHandlers err hs
                                                        return (ElaboratingArg f a prev err')
            -- ProofSearchFail is an internal detail - so don't expose it
            handle (ProofSearchFail e) = handle e
            -- TODO: argument-specific error handlers go here for ElaboratingArg
            handle e = do ist <- getIState
                          logElab 2 "Starting error reflection"
                          logElab 5 (show e)
                          let handlers = idris_errorhandlers ist
                          applyHandlers e handlers
            getFnHandlers :: Name -> Name -> Idris [Name]
            getFnHandlers f arg = do ist <- getIState
                                     let funHandlers = maybe M.empty id .
                                                       lookupCtxtExact f .
                                                       idris_function_errorhandlers $ ist
                                     return . maybe [] S.toList . M.lookup arg $ funHandlers
  
  
            applyHandlers e handlers =
                        do ist <- getIState
                           let err = fmap (errReverse ist) e
                           logElab 3 $ "Using reflection handlers " ++
                                      concat (intersperse ", " (map show handlers))
                           let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
  
                           -- Typecheck error handlers - if this fails, most
                           -- likely something which is needed by it has not
                           -- been imported, so keep the original error.
                           handlers <- case mapM (check (tt_ctxt ist) []) reports of
                                         Error _ -> return [] -- ierror $ ReflectionFailed "Type error while constructing reflected error" e
                                         OK hs   -> return hs
  
                           -- Normalize error handler terms to produce the new messages
                           -- Need to use 'normaliseAll' since we have to reduce private
                           -- names in error handlers too
                           ctxt <- getContext
                           let results = map (normaliseAll ctxt []) (map fst handlers)
                           logElab 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))
  
                           -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent
                           let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
                           errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of
                                           Left err -> ierror err
                                           Right ok -> return ok
                           return $ case errorparts of
                                      []    -> e
                                      parts -> ReflectionError errorparts e
  
  solveAll = try (do solve; solveAll) (return ())
  
  -- | Do the left-over work after creating declarations in reflected
  -- elaborator scripts
  processTacticDecls :: ElabInfo -> [RDeclInstructions] -> Idris ()
  processTacticDecls info steps =
    -- The order of steps is important: type declarations might
    -- establish metavars that later function bodies resolve.
    forM_ (reverse steps) $ \case
      RTyDeclInstrs n fc impls ty ->
        do logElab 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
           logElab 3 $ "  It has impls " ++ show impls
           updateIState $ \i -> i { idris_implicits =
                                      addDef n impls (idris_implicits i) }
           addIBC (IBCImp n)
           ds <- checkDef info fc (\_ e -> e) True [(n, (-1, Nothing, ty, []))]
           addIBC (IBCDef n)
           ctxt <- getContext
           case lookupDef n ctxt of
             (TyDecl _ _ : _) ->
               -- If the function isn't defined at the end of the elab script,
               -- then it must be added as a metavariable. This needs guarding
               -- to prevent overwriting case defs with a metavar, if the case
               -- defs come after the type decl in the same script!
               let ds' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True, True))) ds
               in addDeferred ds'
             _ -> return ()
      RDatatypeDeclInstrs n impls ->
        do addIBC (IBCDef n)
           updateIState $ \i -> i { idris_implicits = addDef n impls (idris_implicits i) }
           addIBC (IBCImp n)
  
      RDatatypeDefnInstrs tyn tyconTy ctors ->
        do let cn (n, _, _) = n
               cty (_, _, t) = t
           addIBC (IBCDef tyn)
           mapM_ (addIBC . IBCDef . cn) ctors
           ctxt <- getContext
           let params = findParams tyn (normalise ctxt [] tyconTy) (map cty ctors)
           let typeInfo = TI (map cn ctors) False [] params [] False
           -- implicit precondition to IBCData is that idris_datatypes on the IState is populated.
           -- otherwise writing the IBC just fails silently!
           updateIState $ \i -> i { idris_datatypes =
                                      addDef tyn typeInfo (idris_datatypes i) }
           addIBC (IBCData tyn)
  
  
           ttag <- getName -- from AbsSyntax.hs, really returns a disambiguating Int
  
           let metainf = DataMI params
           addIBC (IBCMetaInformation tyn metainf)
           updateContext (setMetaInformation tyn metainf)
  
           for_ ctors $ \(cn, impls, _) ->
             do updateIState $ \i -> i { idris_implicits = addDef cn impls (idris_implicits i) }
                addIBC (IBCImp cn)
  
           for_ ctors $ \(ctorN, _, _) ->
             do totcheck (NoFC, ctorN)
                ctxt <- tt_ctxt <$> getIState
                case lookupTyExact ctorN ctxt of
                  Just cty -> do checkPositive (tyn : map cn ctors) (ctorN, cty)
                                 return ()
                  Nothing -> return ()
  
           case ctors of
              [ctor] -> do setDetaggable (cn ctor); setDetaggable tyn
                           addIBC (IBCOpt (cn ctor)); addIBC (IBCOpt tyn)
              _ -> return ()
           -- TODO: inaccessible
  
      RAddImplementation interfaceName implName ->
        do -- The interface resolution machinery relies on a special
           logElab 2 $ "Adding elab script implementation " ++ show implName ++
                       " for " ++ show interfaceName
           addImplementation False True interfaceName implName
           addIBC (IBCImplementation False True interfaceName implName)
      RClausesInstrs n cs ->
        do logElab 3 $ "Pattern-matching definition from tactics: " ++ show n
           solveDeferred emptyFC n
           let lhss = map (\(ns, lhs, _) -> (map fst ns, lhs)) cs
           let fc = fileFC "elab_reflected"
           pmissing <-
             do ist <- getIState
                possible <- genClauses fc n lhss
                                       (map (\ (ns, lhs) ->
                                          delab' ist lhs True True) lhss)
                missing <- filterM (checkPossible n) possible
                let undef = filter (noMatch ist (map snd lhss)) missing
                return undef
           let tot = if null pmissing
                        then Unchecked -- still need to check recursive calls
                        else Partial NotCovering -- missing cases implies not total
           setTotality n tot
           updateIState $ \i -> i { idris_patdefs =
                                      addDef n (cs, pmissing) $ idris_patdefs i }
           addIBC (IBCDef n)
  
           ctxt <- getContext
           case lookupDefExact n ctxt of
             Just (CaseOp _ _ _ _ _ cd) ->
               -- Here, we populate the call graph with a list of things
               -- we refer to, so that if they aren't total, the whole
               -- thing won't be.
               let (scargs, sc) = cases_compiletime cd
                   calls = map fst $ findCalls sc scargs
               in do logElab 2 $ "Called names in reflected elab: " ++ show calls
                     addCalls n calls
                     addIBC $ IBCCG n
             Just _ -> return () -- TODO throw internal error
             Nothing -> return ()
  
           -- checkDeclTotality requires that the call graph be present
           -- before calling it.
           -- TODO: reduce code duplication with Idris.Elab.Clause
           buildSCG (fc, n)
  
           -- Actually run the totality checker. In the main clause
           -- elaborator, this is deferred until after. Here, we run it
           -- now to get totality information as early as possible.
           tot' <- checkDeclTotality (fc, n)
           setTotality n tot'
           when (tot' /= Unchecked) $ addIBC (IBCTotal n tot')
    where
      -- TODO: see if the code duplication with Idris.Elab.Clause can be
      -- reduced or eliminated.
      -- These are always cases generated by genClauses
      checkPossible :: Name -> PTerm -> Idris Bool
      checkPossible fname lhs_in =
         do ctxt <- getContext
            ist <- getIState
            let lhs = addImplPat ist lhs_in
            let fc = fileFC "elab_reflected_totality"
            case elaborate (constraintNS info) ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "refPatLHS") infP initEState
                  (erun fc (buildTC ist info EImpossible [] fname (allNamesIn lhs_in)
                                                                  (infTerm lhs))) of
              OK (ElabResult lhs' _ _ _ _ _ name', _) ->
                do -- not recursively calling here, because we don't
                   -- want to run infinitely many times
                   let lhs_tm = orderPats (getInferTerm lhs')
                   updateIState $ \i -> i { idris_name = name' }
                   case recheck (constraintNS info) ctxt [] (forget lhs_tm) lhs_tm of
                        OK _ -> return True
                        err -> return False
              -- if it's a recoverable error, the case may become possible
              Error err -> return (recoverableCoverage ctxt err)
  
  
      -- TODO: Attempt to reduce/eliminate code duplication with Idris.Elab.Clause
      noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of
                                     Right _ -> False
                                     Left  _ -> True) cs
  