From 4cb8dc507bea38b1eadfc7f2d8ca344e2efa059c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9=20Videla?= <andre.videla@gmail.com>
Date: Thu, 14 Dec 2023 21:34:16 +0000
Subject: [PATCH] update error message for infixr

---
 src/Idris/Desugar.idr                        |  6 ++---
 src/Idris/Error.idr                          |  5 ++++
 tests/idris2/operators/operators003/expected | 24 ++++++++++----------
 3 files changed, 20 insertions(+), 15 deletions(-)

diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr
index 51049cc7e..b91ba7c84 100644
--- a/src/Idris/Desugar.idr
+++ b/src/Idris/Desugar.idr
@@ -1178,9 +1178,9 @@ mutual
   desugarDecl ps (PFixity fc vis binding fix prec opName)
       = do unless (checkValidFixity binding fix prec)
              (throw $ GenericMsgSol fc
-                 "invalid fixity, \{binding} operator must be infixr 0."
-                 ["write `\{binding} infixr 0 \{show opName}`"
-                 , "remove the binding keyword `\{fix} \{show prec} \{show opName}`"
+                 "Invalid fixity, \{binding} operator must be infixr 0."
+                 [ "Make it `infixr 0`: `\{binding} infixr 0 \{show opName}`"
+                 , "Remove the binding keyword: `\{fix} \{show prec} \{show opName}`"
                  ])
            ctx <- get Ctxt
            -- We update the context of fixities by adding a namespaced fixity
diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr
index fa0dcbd87..5880b2c22 100644
--- a/src/Idris/Error.idr
+++ b/src/Idris/Error.idr
@@ -620,6 +620,11 @@ perrorRaw (BadRunElab fc env script desc)
 perrorRaw (RunElabFail e)
     = pure $ reflow "Error during reflection" <+> colon <++> !(perrorRaw e)
 perrorRaw (GenericMsg fc str) = pure $ pretty0 str <+> line <+> !(ploc fc)
+perrorRaw (GenericMsgSol fc header solutions)
+    = pure $ pretty0 header <+> line <+> !(ploc fc)
+       <+> line
+       <+> "Possible solutions:" <+> line
+       <+> indent 1 (vsep (map (\s => "-" <++> pretty0 s) solutions))
 perrorRaw (OperatorBindingMismatch fc {print=p} expected actual opName rhs)
     = pure $ "Operator" <++> pretty0 !(getFullName opName) <++> "is"
        <++> printBindingInfo expected
diff --git a/tests/idris2/operators/operators003/expected b/tests/idris2/operators/operators003/expected
index 5bae83e6a..1b262ce82 100644
--- a/tests/idris2/operators/operators003/expected
+++ b/tests/idris2/operators/operators003/expected
@@ -1,8 +1,5 @@
 1/1: Building Error1 (Error1.idr)
-Error: invalid fixity, typebind operator must be infixr 0.
-Possible solutions:
-- write `typebind infixr 0 =@`
-- remove the binding keyword `infixl 0 =@`
+Error: Invalid fixity, typebind operator must be infixr 0.
 
 Error1:3:10--3:21
  1 | module Error1
@@ -10,11 +7,11 @@ Error1:3:10--3:21
  3 | typebind infixl 0 =@
               ^^^^^^^^^^^
 
-1/1: Building Error2 (Error2.idr)
-Error: invalid fixity, typebind operator must be infixr 0.
 Possible solutions:
-- write `typebind infixr 0 =@`
-- remove the binding keyword `infixr 3 =@`
+ - Make it `infixr 0`: `typebind infixr 0 =@`
+ - Remove the binding keyword: `infixl 0 =@`
+1/1: Building Error2 (Error2.idr)
+Error: Invalid fixity, typebind operator must be infixr 0.
 
 Error2:3:10--3:21
  1 | module Error2
@@ -22,11 +19,11 @@ Error2:3:10--3:21
  3 | typebind infixr 3 =@
               ^^^^^^^^^^^
 
-1/1: Building Error3 (Error3.idr)
-Error: invalid fixity, typebind operator must be infixr 0.
 Possible solutions:
-- write `typebind infixr 0 =@`
-- remove the binding keyword `infixl 3 =@`
+ - Make it `infixr 0`: `typebind infixr 0 =@`
+ - Remove the binding keyword: `infixr 3 =@`
+1/1: Building Error3 (Error3.idr)
+Error: Invalid fixity, typebind operator must be infixr 0.
 
 Error3:3:10--3:21
  1 | module Error3
@@ -34,3 +31,6 @@ Error3:3:10--3:21
  3 | typebind infixl 3 =@
               ^^^^^^^^^^^
 
+Possible solutions:
+ - Make it `infixr 0`: `typebind infixr 0 =@`
+ - Remove the binding keyword: `infixl 3 =@`