Print UnquoteError names rather than just name "UnquoteFailed"

typechecker · Aug 12, 2024 · 4f0866d · 4f0866d
1 parent 0375073
commit 4f0866d
Show file tree

Hide file tree

Showing 6 changed files with 43 additions and 29 deletions.
diff --git a/src/full/Agda/TypeChecking/Errors.hs b/src/full/Agda/TypeChecking/Errors.hs
@@ -288,7 +288,6 @@ errorString = \case
   SolvedButOpenHoles{}                     -> "SolvedButOpenHoles"
   IllegalInstanceVariableInPatternSynonym _ -> "IllegalInstanceVariableInPatternSynonym"
   UnusedVariableInPatternSynonym _         -> "UnusedVariableInPatternSynonym"
-  UnquoteFailed{}                          -> "UnquoteFailed"
   DeBruijnIndexOutOfScope{}                -> "DeBruijnIndexOutOfScope"
   TooFewPatternsInWithClause{}             -> "TooFewPatternsInWithClause"
   TooManyPatternsInWithClause{}            -> "TooManyPatternsInWithClause"
@@ -344,6 +343,7 @@ errorString = \case
   InteractionError err                     -> "Interaction." ++ interactionErrorString err
   NicifierError err                        -> "Syntax." ++ declarationExceptionString err
   OptionError{}                            -> "OptionError"
+  UnquoteFailed err                        -> "Unquote." ++ unquoteErrorString err
 
 ghcBackendErrorString :: GHCBackendError -> String
 ghcBackendErrorString = \case
@@ -361,6 +361,17 @@ interactionErrorString = \case
   NoSuchInteractionPoint{}                 -> "NoSuchInteractionPoint"
   UnexpectedWhere{}                        -> "UnexpectedWhere"
 
+unquoteErrorString :: UnquoteError -> String
+unquoteErrorString = \case
+  BadVisibility        {} -> "BadVisibility"
+  ConInsteadOfDef      {} -> "ConInsteadOfDef"
+  DefInsteadOfCon      {} -> "DefInsteadOfCon"
+  NonCanonical         {} -> "NonCanonical"
+  BlockedOnMeta        {} -> "BlockedOnMeta"
+  PatLamWithoutClauses {} -> "PatLamWithoutClauses"
+  UnquotePanic         {} -> "UnquotePanic"
+
+
 instance PrettyTCM TCErr where
   prettyTCM err = case err of
     -- Gallais, 2016-05-14
@@ -1377,29 +1388,7 @@ instance PrettyTCM TypeError where
             vcat [ prettyTCM term <?> text "was ruled out because"
                  , prettyTCM err ]
 
-    UnquoteFailed e -> case e of
-      BadVisibility msg arg -> fsep $
-        pwords $ "Unable to unquote the argument. It should be `" ++ msg ++ "'."
-
-      ConInsteadOfDef x def con -> fsep $
-        pwords ("Use " ++ con ++ " instead of " ++ def ++ " for constructor") ++
-        [prettyTCM x]
-
-      DefInsteadOfCon x def con -> fsep $
-        pwords ("Use " ++ def ++ " instead of " ++ con ++ " for non-constructor")
-        ++ [prettyTCM x]
-
-      NonCanonical kind t ->
-        fwords ("Cannot unquote non-canonical " ++ kind)
-        $$ nest 2 (prettyTCM t)
-
-      BlockedOnMeta _ m -> fsep $
-        pwords $ "Unquote failed because of unsolved meta variables."
-
-      PatLamWithoutClauses _ -> fsep $
-        pwords "Cannot unquote pattern lambda without clauses. Use a single `absurd-clause` for absurd lambdas."
-
-      UnquotePanic err -> __IMPOSSIBLE__
+    UnquoteFailed e -> prettyTCM e
 
     DeBruijnIndexOutOfScope i EmptyTel [] -> fsep $
         pwords $ "de Bruijn index " ++ show i ++ " is not in scope in the empty context"
@@ -1818,6 +1807,31 @@ instance PrettyTCM InteractionError where
 
     UnexpectedWhere -> fwords "`where' clauses are not supported in holes"
 
+instance PrettyTCM UnquoteError where
+  prettyTCM = \case
+
+    BadVisibility msg arg -> fsep $
+      pwords $ "Unable to unquote the argument. It should be `" ++ msg ++ "'."
+
+    ConInsteadOfDef x def con -> fsep $
+      pwords ("Use " ++ con ++ " instead of " ++ def ++ " for constructor") ++
+      [prettyTCM x]
+
+    DefInsteadOfCon x def con -> fsep $
+      pwords ("Use " ++ def ++ " instead of " ++ con ++ " for non-constructor")
+      ++ [prettyTCM x]
+
+    NonCanonical kind t ->
+      fwords ("Cannot unquote non-canonical " ++ kind)
+      $$ nest 2 (prettyTCM t)
+
+    BlockedOnMeta _ m -> fsep $
+      pwords $ "Unquote failed because of unsolved meta variables."
+
+    PatLamWithoutClauses _ -> fsep $
+      pwords "Cannot unquote pattern lambda without clauses. Use a single `absurd-clause` for absurd lambdas."
+
+    UnquotePanic err -> __IMPOSSIBLE__
 
 notCmp :: MonadPretty m => Comparison -> m Doc
 notCmp cmp = "!" <> prettyTCM cmp

diff --git a/test/Fail/Issue1228.err b/test/Fail/Issue1228.err
@@ -1,2 +1,2 @@
-Issue1228.agda:40,1-45: error: [UnquoteFailed]
+Issue1228.agda:40,1-45: error: [Unquote.DefInsteadOfCon]
 Use def instead of con for non-constructor tt
diff --git a/test/Fail/Issue1228b.err b/test/Fail/Issue1228b.err
@@ -1,2 +1,2 @@
-Issue1228b.agda:40,1-45: error: [UnquoteFailed]
+Issue1228b.agda:40,1-45: error: [Unquote.ConInsteadOfDef]
 Use con instead of def for constructor refl
diff --git a/test/Fail/Issue7326.err b/test/Fail/Issue7326.err
@@ -1,4 +1,4 @@
-Issue7326.agda:13,7-12: error: [UnquoteFailed]
+Issue7326.agda:13,7-12: error: [Unquote.PatLamWithoutClauses]
 Cannot unquote pattern lambda without clauses. Use a single
 'absurd-clause' for absurd lambdas.
 when checking that the expression unquote magic has type ⊥ → ⊤
diff --git a/test/Fail/PostulateMacro.err b/test/Fail/PostulateMacro.err
@@ -1,4 +1,4 @@
-PostulateMacro.agda:15,8-19: error: [UnquoteFailed]
+PostulateMacro.agda:15,8-19: error: [Unquote.NonCanonical]
 Cannot unquote non-canonical type checking computation
   stuck
 when checking that the expression unquote not-so-good has type Nat
diff --git a/test/Fail/StrangeRecursiveUnquote.err b/test/Fail/StrangeRecursiveUnquote.err
@@ -1,4 +1,4 @@
-StrangeRecursiveUnquote.agda:12,13-33: error: [UnquoteFailed]
+StrangeRecursiveUnquote.agda:12,13-33: error: [Unquote.NonCanonical]
 Cannot unquote non-canonical term
   f n
 when checking that the expression unquote (give (f n)) has type