diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4d54fd653..696665016 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,22 +3,18 @@ Changes since Idris 2 v0.1.0
 
 The implementation is now self-hosted. To initialise the build, either use
 the [bootstrapping version of Idris2](https://github.com/edwinb/Idris2-boot)
-or build fromt the generated Scheme, using `make bootstrap`.
+or build from the generated Scheme, using `make bootstrap`.
 
-Compiler updates:
-
-* Data types with a single constructor, with a single unerased arguments,
-  are translated to just that argument, to save repeated packing and unpacking.
-  (c.f. `newtype` in Haskell)
-  + A data type can opt out of this behaviour by specifying `noNewtype` in its
-    options list. `noNewtype` allows code generators to apply special handling
-    to the generated constructor/deconstructor, for a newtype-like data type,
-    that would otherwise be optimised away.
-* 0-multiplicity constructor arguments are now properly erased, not just
-  given a placeholder null value.
-
-Language extensions:
+Language changes:
 
+* `total`, `covering` and `partial` flags on functions now have an effect.
+* Fields of records can be accessed (and updated) using the dot syntax,
+  such as `r.field1.field2` or `record { field1.field2 = 42 }`.
+  For details, see https://idris2.readthedocs.io/en/latest/reference/records.html
+* New function flag `%tcinline` which means that the function should be
+  inlined for the purposes of totality checking (but otherwise not inlined).
+  This can be used as a hint for totality checking, to make the checker look
+  inside functions that it otherwise might not.
 * %transform directive, for declaring transformation rules on runtime
   expressions. Transformation rules are automatically added for top level
   implementations of interfaces.
@@ -33,22 +29,27 @@ Library additions:
 * New modules in `contrib` for JSON (`Language.JSON.*`); random numbers
   (`System.Random`)
 
+Compiler updates:
+
+* Data types with a single constructor, with a single unerased arguments,
+  are translated to just that argument, to save repeated packing and unpacking.
+  (c.f. `newtype` in Haskell)
+  + A data type can opt out of this behaviour by specifying `noNewtype` in its
+    options list. `noNewtype` allows code generators to apply special handling
+    to the generated constructor/deconstructor, for a newtype-like data type,
+    that would otherwise be optimised away.
+* 0-multiplicity constructor arguments are now properly erased, not just
+  given a placeholder null value.
+
 Other improvements:
 
 * Various performance improvements in the typechecker:
   + Noting which metavariables are blocking unification constraints, so that
     they only get retried if those metavariables make progress.
   + Evaluating `fromInteger` at compile time.
-  + In the run-time, reuse the old heap after garbage collection if it
-    hasn't been resized, to avoid unnecessary system calls.
-
 * Extend Idris2's literate mode to support reading Markdown and OrgMode files.
   For more details see: https://idris2.readthedocs.io/en/latest/reference/literate.html
 
-* Fields of records can be accessed (and updated) using the dot syntax,
-  such as `r.field1.field2` or `record { field1.field2 = 42 }`.
-  For details, see https://idris2.readthedocs.io/en/latest/reference/records.html
-
 Changes since Idris 1
 ---------------------
 
diff --git a/libs/contrib/Text/Parser/Core.idr b/libs/contrib/Text/Parser/Core.idr
index eea627a0d..c62bdba96 100644
--- a/libs/contrib/Text/Parser/Core.idr
+++ b/libs/contrib/Text/Parser/Core.idr
@@ -29,7 +29,7 @@ data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
 ||| guaranteed to consume some input. If the first one consumes input, the
 ||| second is allowed to be recursive (because it means some input has been
 ||| consumed and therefore the input is smaller)
-public export %inline
+public export %inline %tcinline
 (>>=) : {c1, c2 : Bool} ->
         Grammar tok c1 a ->
         inf c1 (a -> Grammar tok c2 b) ->
diff --git a/src/Core/Context.idr b/src/Core/Context.idr
index 12566428f..097145b04 100644
--- a/src/Core/Context.idr
+++ b/src/Core/Context.idr
@@ -170,6 +170,9 @@ data DefFlag
          -- should evaluate the RHS, with reduction limits on the given names,
          -- and ensure the name has made progress in doing so (i.e. has reduced
          -- at least once)
+    | AllGuarded -- safe to treat as a constructor for the purposes of
+         -- productivity checking. All clauses are guarded by constructors,
+         -- and there are no other function applications
 
 export
 Eq DefFlag where
@@ -181,6 +184,7 @@ Eq DefFlag where
     (==) BlockedHint BlockedHint = True
     (==) Macro Macro = True
     (==) (PartialEval x) (PartialEval y) = x == y
+    (==) AllGuarded AllGuarded = True
     (==) _ _ = False
 
 export
@@ -193,6 +197,7 @@ Show DefFlag where
   show BlockedHint = "blockedhint"
   show Macro = "macro"
   show (PartialEval _) = "partialeval"
+  show AllGuarded = "allguarded"
 
 public export
 data SizeChange = Smaller | Same | Unknown
diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr
index 58b3152a6..8d1db399b 100644
--- a/src/Core/Normalise.idr
+++ b/src/Core/Normalise.idr
@@ -107,7 +107,7 @@ parameters (defs : Defs, topopts : EvalOpts)
     eval env locs (Bind fc x (Lam r _ ty) scope) (thunk :: stk)
         = eval env (thunk :: locs) scope stk
     eval env locs (Bind fc x b@(Let r val ty) scope) stk
-        = if holesOnly topopts || argHolesOnly topopts
+        = if holesOnly topopts || argHolesOnly topopts && not (tcInline topopts)
              then do b' <- traverse (\tm => eval env locs tm []) b
                      pure $ NBind fc x b'
                         (\defs', arg => evalWithOpts defs' topopts
@@ -595,8 +595,10 @@ mutual
            pure (TDelay fc r tyQ argQ)
     where
       toHolesOnly : Closure vs -> Closure vs
-      toHolesOnly (MkClosure _ locs env tm)
-          = MkClosure withHoles locs env tm
+      toHolesOnly (MkClosure opts locs env tm)
+          = MkClosure (record { holesOnly = True,
+                                argHolesOnly = True } opts)
+                      locs env tm
       toHolesOnly c = c
   quoteGenNF q defs bound env (NForce fc r arg args)
       = do args' <- quoteArgs q defs bound env args
diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr
index 4e0d92986..f19f06a67 100644
--- a/src/Core/TTC.idr
+++ b/src/Core/TTC.idr
@@ -865,6 +865,7 @@ TTC DefFlag where
   toBuf b BlockedHint = tag 7
   toBuf b Macro = tag 8
   toBuf b (PartialEval x) = tag 9 -- names not useful any more
+  toBuf b AllGuarded = tag 10
 
   fromBuf b
       = case !getTag of
@@ -876,6 +877,7 @@ TTC DefFlag where
              7 => pure BlockedHint
              8 => pure Macro
              9 => pure (PartialEval [])
+             10 => pure AllGuarded
              _ => corrupt "DefFlag"
 
 export
diff --git a/src/Core/Termination.idr b/src/Core/Termination.idr
index 454b3e49e..b8e47f029 100644
--- a/src/Core/Termination.idr
+++ b/src/Core/Termination.idr
@@ -34,6 +34,55 @@ totRefsIn : {auto c : Ref Ctxt Defs} ->
             Defs -> Term vars -> Core Terminating
 totRefsIn defs ty = totRefs defs (keys (getRefs (Resolved (-1)) ty))
 
+-- Check if all branches end up as constructor arguments, with no other
+-- function application, and set 'AllGuarded' if so.
+-- This is to check whether a function can be considered a constructor form
+-- for the sake of termination checking (and might have other uses...)
+export
+checkIfGuarded : {auto c : Ref Ctxt Defs} ->
+                 FC -> Name -> Core ()
+checkIfGuarded fc n
+    = do defs <- get Ctxt
+         Just (PMDef _ _ _ _ pats) <- lookupDefExact n (gamma defs)
+              | _ => pure ()
+         t <- allGuarded pats
+         when t $ setFlag fc n AllGuarded
+  where
+    guardedNF : {vars : _} -> Defs -> Env Term vars -> NF vars -> Core Bool
+    guardedNF defs env (NDCon _ _ _ _ args) = pure True
+    guardedNF defs env (NApp _ (NRef _ n) args)
+        = do Just gdef <- lookupCtxtExact n (gamma defs)
+                  | Nothing => pure False
+             pure (AllGuarded `elem` flags gdef)
+    guardedNF defs env _ = pure False
+
+    checkNotFn : Defs -> Name -> Core Bool
+    checkNotFn defs n
+        = do Just gdef <- lookupCtxtExact n (gamma defs)
+                  | Nothing => pure False
+             case definition gdef of
+                  DCon _ _ _ => pure True
+                  _ => pure (multiplicity gdef == erased
+                              || (AllGuarded `elem` flags gdef))
+
+    guarded : {vars : _} -> Env Term vars -> Term vars -> Core Bool
+    guarded env tm
+        = do defs <- get Ctxt
+             empty <- clearDefs defs
+             tmnf <- nf empty env tm
+             if !(guardedNF defs env tmnf)
+                then do Just gdef <- lookupCtxtExact n (gamma defs)
+                             | Nothing => pure False
+                        allM (checkNotFn defs) (keys (refersTo gdef))
+                else pure False
+
+    allGuarded : List (vs ** (Env Term vs, Term vs, Term vs)) -> Core Bool
+    allGuarded [] = pure True
+    allGuarded ((_ ** (env, lhs, rhs)) :: ps)
+        = if !(guarded env rhs)
+             then allGuarded ps
+             else pure False
+
 -- Equal for the purposes of size change means, ignoring as patterns, all
 -- non-metavariable positions are equal
 scEq : Term vars -> Term vars -> Bool
@@ -79,8 +128,13 @@ mutual
   -- If we're Guarded and find a Delay, continue with the argument as InDelay
   findSC defs env Guarded pats (TDelay _ _ _ tm)
       = findSC defs env InDelay pats tm
+  findSC defs env g pats (TDelay _ _ _ tm)
+      = findSC defs env g pats tm
   findSC defs env g pats tm
-      = case (g, getFnArgs tm) of
+      = do let (fn, args) = getFnArgs tm
+           fn' <- conIfGuarded fn -- pretend it's a data constructor if
+                                  -- it has the AllGuarded flag
+           case (g, fn', args) of
     -- If we're InDelay and find a constructor (or a function call which is
     -- guaranteed to return a constructor; AllGuarded set), continue as InDelay
              (InDelay, Ref fc (DataCon _ _) cn, args) =>
@@ -91,6 +145,9 @@ mutual
              (InDelay, _, args) =>
                  do scs <- traverse (findSC defs env Unguarded pats) args
                     pure (concat scs)
+             (Guarded, Ref fc (DataCon _ _) cn, args) =>
+                 do scs <- traverse (findSC defs env Guarded pats) args
+                    pure (concat scs)
              (Toplevel, Ref fc (DataCon _ _) cn, args) =>
                  do scs <- traverse (findSC defs env Guarded pats) args
                     pure (concat scs)
@@ -103,6 +160,16 @@ mutual
              (_, f, args) =>
                  do scs <- traverse (findSC defs env Unguarded pats) args
                     pure (concat scs)
+      where
+        conIfGuarded : Term vars -> Core (Term vars)
+        conIfGuarded (Ref fc Func n)
+            = do defs <- get Ctxt
+                 Just gdef <- lookupCtxtExact n (gamma defs)
+                      | Nothing => pure $ Ref fc Func n
+                 if AllGuarded `elem` flags gdef
+                    then pure $ Ref fc (DataCon 0 0) n
+                    else pure $ Ref fc Func n
+        conIfGuarded tm = pure tm
 
   -- Expand the size change argument list with 'Nothing' to match the given
   -- arity (i.e. the arity of the function we're calling) to ensure that
diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr
index e0edbdadf..f7118ed7c 100644
--- a/src/Idris/Elab/Implementation.idr
+++ b/src/Idris/Elab/Implementation.idr
@@ -185,7 +185,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
                fns <- topMethTypes [] impName methImps impsp (params cdata)
                                       (map fst (methods cdata))
                                       (methods cdata)
-               traverse (processDecl [] nest env) (map mkTopMethDecl fns)
+               traverse_ (processDecl [] nest env) (map mkTopMethDecl fns)
 
                -- 3. Build the record for the implementation
                let mtops = map (Builtin.fst . snd) fns
diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index 2db3deea1..a3e52de50 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -1174,6 +1174,9 @@ fnDirectOpt fname
   <|> do pragma "inline"
          commit
          pure $ IFnOpt Inline
+  <|> do pragma "tcinline"
+         commit
+         pure $ IFnOpt TCInline
   <|> do pragma "extern"
          pure $ IFnOpt ExternFn
   <|> do pragma "macro"
diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr
index 0644c84a3..745533417 100644
--- a/src/Idris/REPL.idr
+++ b/src/Idris/REPL.idr
@@ -69,6 +69,7 @@ showInfo (n, idx, d)
                                show !(traverse getFullName (keys (refersTo d))))
          coreLift $ putStrLn ("Refers to (runtime): " ++
                                show !(traverse getFullName (keys (refersToRuntime d))))
+         coreLift $ putStrLn ("Flags: " ++ show (flags d))
          when (not (isNil (sizeChange d))) $
             let scinfo = map (\s => show (fnCall s) ++ ": " ++
                                     show (fnArgs s)) !(traverse toFullNames (sizeChange d)) in
diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr
index b0e2e8897..ba1f55ca4 100644
--- a/src/TTImp/Elab/Case.idr
+++ b/src/TTImp/Elab/Case.idr
@@ -226,7 +226,15 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
          -- Start with empty nested names, since we've extended the rhs with
          -- ICaseLocal so they'll get rebuilt with the right environment
          let nest' = MkNested []
+         ust <- get UST
+         -- We don't want to keep rechecking delayed elaborators in the
+         -- case block, because they're not going to make progress until
+         -- we come out again, so save them
+         let olddelayed = delayedElab ust
+         put UST (record { delayedElab = [] } ust)
          processDecl [InCase] nest' [] (IDef fc casen alts')
+         ust <- get UST
+         put UST (record { delayedElab = olddelayed } ust)
 
          pure (appTm, gnf env caseretty)
   where
diff --git a/src/TTImp/Elab/Delayed.idr b/src/TTImp/Elab/Delayed.idr
index 5f076dd6b..7be3068a1 100644
--- a/src/TTImp/Elab/Delayed.idr
+++ b/src/TTImp/Elab/Delayed.idr
@@ -71,7 +71,7 @@ delayOnFailure fc rig env expected pred pri elab
          handle (elab False)
           (\err =>
               do est <- get EST
-                 if pred err && delayDepth est < !getAmbigLimit
+                 if pred err
                     then
                       do nm <- genName "delayed"
                          (ci, dtm) <- newDelayed fc linear env nm !(getTerm expected)
@@ -99,19 +99,16 @@ delayElab : {vars : _} ->
             Core (Term vars, Glued vars)
 delayElab {vars} fc rig env exp pri elab
     = do est <- get EST
-         if delayDepth est >= !getAmbigLimit
-            then elab
-            else do
-             nm <- genName "delayed"
-             expected <- mkExpected exp
-             (ci, dtm) <- newDelayed fc linear env nm !(getTerm expected)
-             logGlueNF 5 ("Postponing elaborator " ++ show nm ++
-                          " for") env expected
-             ust <- get UST
-             put UST (record { delayedElab $=
-                     ((pri, ci, mkClosedElab fc env (deeper elab)) :: ) }
-                             ust)
-             pure (dtm, expected)
+         nm <- genName "delayed"
+         expected <- mkExpected exp
+         (ci, dtm) <- newDelayed fc linear env nm !(getTerm expected)
+         logGlueNF 5 ("Postponing elaborator " ++ show nm ++
+                      " for") env expected
+         ust <- get UST
+         put UST (record { delayedElab $=
+                 ((pri, ci, mkClosedElab fc env elab) :: ) }
+                         ust)
+         pure (dtm, expected)
   where
     mkExpected : Maybe (Glued vars) -> Core (Glued vars)
     mkExpected (Just ty) = pure ty
@@ -132,14 +129,69 @@ ambiguous (InRHS _ _ err) = ambiguous err
 ambiguous (WhenUnifying _ _ _ _ err) = ambiguous err
 ambiguous _ = False
 
+mutual
+  mismatchNF : {vars : _} ->
+               Defs -> NF vars -> NF vars -> Core Bool
+  mismatchNF defs (NTCon _ xn xt _ xargs) (NTCon _ yn yt _ yargs)
+      = if xn /= yn
+           then pure True
+           else anyM (mismatch defs) (zip xargs yargs)
+  mismatchNF defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)
+      = if xt /= yt
+           then pure True
+           else anyM (mismatch defs) (zip xargs yargs)
+  mismatchNF defs (NPrimVal _ xc) (NPrimVal _ yc) = pure (xc /= yc)
+  mismatchNF defs (NDelayed _ _ x) (NDelayed _ _ y) = mismatchNF defs x y
+  mismatchNF defs (NDelay _ _ _ x) (NDelay _ _ _ y)
+      = mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)
+  mismatchNF _ _ _ = pure False
+
+  mismatch : {vars : _} ->
+             Defs -> (Closure vars, Closure vars) -> Core Bool
+  mismatch defs (x, y)
+      = mismatchNF defs !(evalClosure defs x) !(evalClosure defs y)
+
+contra : {vars : _} ->
+               Defs -> NF vars -> NF vars -> Core Bool
+-- Unlike 'impossibleOK', any mismatch indicates an unrecoverable error
+contra defs (NTCon _ xn xt xa xargs) (NTCon _ yn yt ya yargs)
+    = if xn /= yn
+         then pure True
+         else anyM (mismatch defs) (zip xargs yargs)
+contra defs (NDCon _ _ xt _ xargs) (NDCon _ _ yt _ yargs)
+    = if xt /= yt
+         then pure True
+         else anyM (mismatch defs) (zip xargs yargs)
+contra defs (NPrimVal _ x) (NPrimVal _ y) = pure (x /= y)
+contra defs (NDCon _ _ _ _ _) (NPrimVal _ _) = pure True
+contra defs (NPrimVal _ _) (NDCon _ _ _ _ _) = pure True
+contra defs x y = pure False
+
+-- Errors that might be recoverable later if we try again. Generally -
+-- ambiguity errors, type inference errors
+export
+recoverable : {auto c : Ref Ctxt Defs} ->
+              Error -> Core Bool
+recoverable (CantConvert _ env l r)
+   = do defs <- get Ctxt
+        pure $ not !(contra defs !(nf defs env l) !(nf defs env r))
+recoverable (CantSolveEq _ env l r)
+   = do defs <- get Ctxt
+        pure $ not !(contra defs !(nf defs env l) !(nf defs env r))
+recoverable (UndefinedName _ _) = pure False
+recoverable (InType _ _ err) = recoverable err
+recoverable (InCon _ _ err) = recoverable err
+recoverable (InLHS _ _ err) = recoverable err
+recoverable (InRHS _ _ err) = recoverable err
+recoverable (WhenUnifying _ _ _ _ err) = recoverable err
+recoverable _ = pure True
+
 data RetryError
-     = NoError
-     | AmbigError
+     = RecoverableErrors
      | AllErrors
 
 Show RetryError where
-  show NoError = "NoError"
-  show AmbigError = "AmbigError"
+  show RecoverableErrors = "RecoverableErrors"
   show AllErrors = "AllErrors"
 
 -- Try all the delayed elaborators. If there's a failure, we want to
@@ -178,9 +230,8 @@ retryDelayed' errmode acc (d@(_, i, elab) :: ds)
            (\err => do log 5 $ show errmode ++ ":Error in " ++ show !(getFullName (Resolved i))
                                 ++ "\n" ++ show err
                        case errmode of
-                         NoError => retryDelayed' errmode (d :: acc) ds
-                         AmbigError =>
-                            if ambiguous err -- give up on ambiguity
+                         RecoverableErrors =>
+                            if not !(recoverable err)
                                then throw err
                                else retryDelayed' errmode (d :: acc) ds
                          AllErrors => throw err)
@@ -195,8 +246,7 @@ retryDelayed : {vars : _} ->
                Core ()
 retryDelayed ds
     = do est <- get EST
-         ds <- retryDelayed' NoError [] ds -- try everything again
-         ds <- retryDelayed' AmbigError [] ds -- fail on ambiguity error
+         ds <- retryDelayed' RecoverableErrors [] ds -- try everything again
          retryDelayed' AllErrors [] ds -- fail on all errors
          pure ()
 
diff --git a/src/TTImp/Elab/Local.idr b/src/TTImp/Elab/Local.idr
index 2cb0e6337..917f4590e 100644
--- a/src/TTImp/Elab/Local.idr
+++ b/src/TTImp/Elab/Local.idr
@@ -37,7 +37,15 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls scope expty
                                            -- fixes bug #115
          let nest' = record { names $= (names' ++) } nest
          let env' = dropLinear env
+         -- We don't want to keep rechecking delayed elaborators in the
+         -- locals  block, because they're not going to make progress until
+         -- we come out again, so save them
+         ust <- get UST
+         let olddelayed = delayedElab ust
+         put UST (record { delayedElab = [] } ust)
          traverse (processDecl [] nest' env') (map (updateName nest') nestdecls)
+         ust <- get UST
+         put UST (record { delayedElab = olddelayed } ust)
          check rig elabinfo nest' env scope expty
   where
     -- For the local definitions, don't allow access to linear things
diff --git a/src/TTImp/Elab/Utils.idr b/src/TTImp/Elab/Utils.idr
index 5567a38dd..2ca7080b0 100644
--- a/src/TTImp/Elab/Utils.idr
+++ b/src/TTImp/Elab/Utils.idr
@@ -7,6 +7,7 @@ import Core.Normalise
 import Core.TT
 import Core.Value
 
+import TTImp.Elab.Check
 import TTImp.TTImp
 
 detagSafe : Defs -> NF [] -> Core Bool
@@ -64,3 +65,9 @@ updateErasable n
          addDef n (record { eraseArgs = es,
                             safeErase = dtes } gdef)
          pure ()
+export
+wrapErrorC : List ElabOpt -> (Error -> Error) -> Core a -> Core a
+wrapErrorC opts err
+    = if InCase `elem` opts
+         then id
+         else wrapError err
diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr
index 1a6b1ba67..448175669 100644
--- a/src/TTImp/ProcessData.idr
+++ b/src/TTImp/ProcessData.idr
@@ -92,7 +92,7 @@ checkCon {vars} opts nest env vis tn_in tn (MkImpTy fc cn_in ty_raw)
          Nothing <- lookupCtxtExact cn (gamma defs)
              | Just gdef => throw (AlreadyDefined fc cn)
          ty <-
-             wrapError (InCon fc cn) $
+             wrapErrorC opts (InCon fc cn) $
                    checkTerm !(resolveName cn) InType opts nest env
                               (IBindHere fc (PI erased) ty_raw)
                               (gType fc)
@@ -255,7 +255,7 @@ processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw)
              | Just gdef => throw (AlreadyDefined fc n)
 
          (ty, _) <-
-             wrapError (InCon fc n) $
+             wrapErrorC eopts (InCon fc n) $
                     elabTerm !(resolveName n) InType eopts nest env
                               (IBindHere fc (PI erased) ty_raw)
                               (Just (gType dfc))
@@ -289,7 +289,7 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
          log 1 $ "Processing " ++ show n
          defs <- get Ctxt
          (ty, _) <-
-             wrapError (InCon fc n) $
+             wrapErrorC eopts (InCon fc n) $
                     elabTerm !(resolveName n) InType eopts nest env
                               (IBindHere fc (PI erased) ty_raw)
                               (Just (gType dfc))
diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr
index 349f9b34c..bc5a77c5d 100644
--- a/src/TTImp/ProcessDef.idr
+++ b/src/TTImp/ProcessDef.idr
@@ -18,6 +18,7 @@ import Core.UnifyState
 import TTImp.BindImplicits
 import TTImp.Elab
 import TTImp.Elab.Check
+import TTImp.Elab.Utils
 import TTImp.Impossible
 import TTImp.PartialEval
 import TTImp.TTImp
@@ -252,7 +253,7 @@ checkLHS {vars} trans mult hashit n opts nest env fc lhs_in
                           then InTransform
                           else InLHS mult
          (lhstm, lhstyg) <-
-             wrapError (InLHS fc !(getFullName (Resolved n))) $
+             wrapErrorC opts (InLHS fc !(getFullName (Resolved n))) $
                      elabTerm n lhsMode opts nest env
                                 (IBindHere fc PATTERN lhs) Nothing
          logTerm 5 "Checked LHS term" lhstm
@@ -387,7 +388,7 @@ checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
          log 5 $ "Checking RHS " ++ show rhs
          logEnv 5 "In env" env'
 
-         rhstm <- wrapError (InRHS fc !(getFullName (Resolved n))) $
+         rhstm <- wrapErrorC opts (InRHS fc !(getFullName (Resolved n))) $
                        checkTermSub n rhsMode opts nest' env' env sub' rhs (gnf env' lhsty')
          clearHoleLHS
 
@@ -411,7 +412,7 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs
          let wmode
                = if isErased mult then InType else InExpr
 
-         (wval, gwvalTy) <- wrapError (InRHS fc !(getFullName (Resolved n))) $
+         (wval, gwvalTy) <- wrapErrorC opts (InRHS fc !(getFullName (Resolved n))) $
                 elabTermSub n wmode opts nest' env' env sub' wval_raw Nothing
          clearHoleLHS
 
@@ -471,7 +472,7 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs
                          map (maybe wval_raw (\pn => IVar fc (snd pn))) wargNames)
 
          log 3 $ "Applying to with argument " ++ show rhs_in
-         rhs <- wrapError (InRHS fc !(getFullName (Resolved n))) $
+         rhs <- wrapErrorC opts (InRHS fc !(getFullName (Resolved n))) $
              checkTermSub n wmode opts nest' env' env sub' rhs_in
                           (gnf env' reqty)
 
@@ -720,6 +721,7 @@ processDef opts nest env fc n_in cs_in
              do calcRefs False atotal (Resolved nidx)
                 sc <- calculateSizeChange fc n
                 setSizeChange fc n sc
+                checkIfGuarded fc n
 
          md <- get MD -- don't need the metadata collected on the coverage check
          cov <- checkCoverage nidx ty mult cs
diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr
index 1ee74759c..87d659e5d 100644
--- a/src/TTImp/ProcessType.idr
+++ b/src/TTImp/ProcessType.idr
@@ -33,6 +33,8 @@ processFnOpt : {auto c : Ref Ctxt Defs} ->
                FC -> Name -> FnOpt -> Core ()
 processFnOpt fc ndef Inline
     = setFlag fc ndef Inline
+processFnOpt fc ndef TCInline
+    = setFlag fc ndef TCInline
 processFnOpt fc ndef (Hint d)
     = do defs <- get Ctxt
          Just ty <- lookupTyExact ndef (gamma defs)
@@ -264,7 +266,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
               | Just _ => throw (AlreadyDefined fc n)
 
          ty <-
-             wrapError (InType fc n) $
+             wrapErrorC eopts (InType fc n) $
                    checkTerm idx InType (HolesOkay :: eopts) nest env
                              (IBindHere fc (PI erased) ty_raw)
                              (gType fc)
diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr
index 681416a2f..8de68096d 100644
--- a/src/TTImp/TTImp.idr
+++ b/src/TTImp/TTImp.idr
@@ -179,6 +179,7 @@ mutual
   public export
   data FnOpt : Type where
        Inline : FnOpt
+       TCInline : FnOpt
        -- Flag means the hint is a direct hint, not a function which might
        -- find the result (e.g. chasing parent interface dictionaries)
        Hint : Bool -> FnOpt
@@ -196,6 +197,7 @@ mutual
   export
   Show FnOpt where
     show Inline = "%inline"
+    show TCInline = "%tcinline"
     show (Hint t) = "%hint " ++ show t
     show (GlobalHint t) = "%globalhint " ++ show t
     show ExternFn = "%extern"
@@ -210,6 +212,7 @@ mutual
   export
   Eq FnOpt where
     Inline == Inline = True
+    TCInline == TCInline = True
     (Hint x) == (Hint y) = x == y
     (GlobalHint x) == (GlobalHint y) = x == y
     ExternFn == ExternFn = True
@@ -895,6 +898,7 @@ mutual
   export
   TTC FnOpt where
     toBuf b Inline = tag 0
+    toBuf b TCInline = tag 11
     toBuf b (Hint t) = do tag 1; toBuf b t
     toBuf b (GlobalHint t) = do tag 2; toBuf b t
     toBuf b ExternFn = tag 3
@@ -919,6 +923,7 @@ mutual
                8 => pure (Totality PartialOK)
                9 => pure Macro
                10 => do ns <- fromBuf b; pure (SpecArgs ns)
+               11 => pure TCInline
                _ => corrupt "FnOpt"
 
   export
diff --git a/tests/idris2/basic039/expected b/tests/idris2/basic039/expected
index a593c1f94..6901349f9 100644
--- a/tests/idris2/basic039/expected
+++ b/tests/idris2/basic039/expected
@@ -8,6 +8,7 @@ Inferrable args: []
 Compiled: Constructor tag Just 0 arity 1 (newtype by 0)
 Refers to: []
 Refers to (runtime): []
+Flags: []
 Main> Main.MkBar ==> DataCon 0 1
 RigW
 Erasable args: []
@@ -17,4 +18,5 @@ Inferrable args: []
 Compiled: Constructor tag Just 0 arity 1
 Refers to: []
 Refers to (runtime): []
+Flags: []
 Main> Bye for now!
diff --git a/tests/idris2/total006/expected b/tests/idris2/total006/expected
index 08e4f2636..ea47712ea 100644
--- a/tests/idris2/total006/expected
+++ b/tests/idris2/total006/expected
@@ -1,6 +1,6 @@
 1/1: Building Total (Total.idr)
 Main> Main.count is total
-Main> Main.badCount is possibly not terminating due to recursive path Main.badCount -> Prelude.Functor implementation at Prelude.idr:1010:1--1015:1 -> Prelude.map
+Main> Main.badCount is possibly not terminating due to recursive path Main.badCount
 Main> Main.process is total
 Main> Main.badProcess is possibly not terminating due to recursive path Main.badProcess -> Main.badProcess -> Main.badProcess
 Main> Main.doubleInt is total