update error message for infixr

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

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

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 =@`