Remove some noise from error messages

There's no point in wrapping all the case blocks, since this is an
internal detail, and it distracts from the proper location of the error.

CHANGELOG.md

@@ -3,7 +3,7 @@ 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:
 

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

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))

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)
 

src/TTImp/ProcessType.idr

@@ -264,7 +264,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)