From 6494241c11e923343f9b34f0bf3708198c4e07a6 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Fri, 22 May 2020 14:14:09 +0100
Subject: [PATCH] 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              | 2 +-
 src/TTImp/Elab/Utils.idr  | 7 +++++++
 src/TTImp/ProcessData.idr | 6 +++---
 src/TTImp/ProcessDef.idr  | 9 +++++----
 src/TTImp/ProcessType.idr | 2 +-
 5 files changed, 17 insertions(+), 9 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a57353657..eb0616ba2 100644
--- a/CHANGELOG.md
+++ b/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:
 
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..8322f918a 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)
 
diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr
index 1ee74759c..27becefe8 100644
--- a/src/TTImp/ProcessType.idr
+++ b/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)