first attempt at suggesting different operators

src/Core/Context.idr

@@ -821,8 +821,9 @@ HasNames Error where
   full gam (InRHS fc n err) = InRHS fc <$> full gam n <*> full gam err
   full gam (MaybeMisspelling err xs) = MaybeMisspelling <$> full gam err <*> pure xs
   full gam (WarningAsError wrn) = WarningAsError <$> full gam wrn
-  full gam (OperatorBindingMismatch {print} fc expected actual opName rhs)
+  full gam (OperatorBindingMismatch {print} fc expected actual opName rhs candidates)
-      = OperatorBindingMismatch {print} fc expected actual <$> full gam opName <*> pure rhs
+      = OperatorBindingMismatch {print} fc expected actual
+          <$> full gam opName <*> pure rhs <*> pure candidates
 
   resolved gam (Fatal err) = Fatal <$> resolved gam err
   resolved _ (CantConvert fc gam rho s t)
@@ -915,8 +916,9 @@ HasNames Error where
   resolved gam (InRHS fc n err) = InRHS fc <$> resolved gam n <*> resolved gam err
   resolved gam (MaybeMisspelling err xs) = MaybeMisspelling <$> resolved gam err <*> pure xs
   resolved gam (WarningAsError wrn) = WarningAsError <$> resolved gam wrn
-  resolved gam (OperatorBindingMismatch {print} fc expected actual opName rhs)
+  resolved gam (OperatorBindingMismatch {print} fc expected actual opName rhs candidates)
-      = OperatorBindingMismatch {print} fc expected actual <$> resolved gam opName <*> pure rhs
+      = OperatorBindingMismatch {print} fc expected actual
+          <$> resolved gam opName <*> pure rhs <*> pure candidates
 
 export
 HasNames Totality where

src/Core/Core.idr

@@ -166,7 +166,7 @@ data Error : Type where
      GenericMsgSol : FC -> (message : String) -> (solutions : List String) -> Error
      OperatorBindingMismatch : {a : Type} -> {print : a -> Doc ()} ->
          FC -> (expectedFixity : BacktickOrOperatorFixity) -> (use_site : OperatorLHSInfo a) ->
-         (opName : Name) -> (rhs : a) -> Error
+         (opName : Name) -> (rhs : a) -> (candidates : List String) -> Error
      TTCError : TTCErrorMsg -> Error
      FileErr : String -> FileError -> Error
      CantFindPackage : String -> Error
@@ -400,10 +400,10 @@ Show Error where
            (n ::: []) => ": " ++ n ++ "?"
            _ => " any of: " ++ showSep ", " (map show (forget ns)) ++ "?"
   show (WarningAsError w) = show w
-  show (OperatorBindingMismatch fc (DeclaredFixity expected) actual opName rhs)
+  show (OperatorBindingMismatch fc (DeclaredFixity expected) actual opName rhs _)
        = show fc ++ ": Operator " ++ show opName ++ " is " ++ show expected
        ++ " but used as a " ++ show actual ++ " operator"
-  show (OperatorBindingMismatch fc Backticked actual opName rhs)
+  show (OperatorBindingMismatch fc Backticked actual opName rhs _)
        = show fc ++ ": Operator " ++ show opName ++ " has no declared fixity"
        ++ " but used as a " ++ show actual ++ " operator"
 
@@ -496,7 +496,7 @@ getErrorLoc (InLHS _ _ err) = getErrorLoc err
 getErrorLoc (InRHS _ _ err) = getErrorLoc err
 getErrorLoc (MaybeMisspelling err _) = getErrorLoc err
 getErrorLoc (WarningAsError warn) = Just (getWarningLoc warn)
-getErrorLoc (OperatorBindingMismatch fc _ _ _ _) = Just fc
+getErrorLoc (OperatorBindingMismatch fc _ _ _ _ _) = Just fc
 
 export
 killWarningLoc : Warning -> Warning
@@ -586,8 +586,8 @@ killErrorLoc (InLHS fc x err) = InLHS emptyFC x (killErrorLoc err)
 killErrorLoc (InRHS fc x err) = InRHS emptyFC x (killErrorLoc err)
 killErrorLoc (MaybeMisspelling err xs) = MaybeMisspelling (killErrorLoc err) xs
 killErrorLoc (WarningAsError wrn) = WarningAsError (killWarningLoc wrn)
-killErrorLoc (OperatorBindingMismatch {print} fc expected actual opName rhs)
+killErrorLoc (OperatorBindingMismatch {print} fc expected actual opName rhs candidates)
-             = OperatorBindingMismatch {print} emptyFC expected actual opName rhs
+             = OperatorBindingMismatch {print} emptyFC expected actual opName rhs candidates
 
 
 -- Core is a wrapper around IO that is specialised for efficiency.

src/Idris/Desugar.idr

@@ -170,12 +170,15 @@ checkConflictingFixities isPrefix exprFC opn
                    For example: %hide \{show fxName}
                    """
 
-checkConflictingBinding : Side -> FC -> Name -> (foundFixity : BacktickOrOperatorFixity) -> (usage : OperatorLHSInfo PTerm) -> (rhs : PTerm) -> Core ()
+checkConflictingBinding : Ref Ctxt Defs =>
+                          Side -> FC -> Name -> (foundFixity : BacktickOrOperatorFixity) ->
+                          (usage : OperatorLHSInfo PTerm) -> (rhs : PTerm) -> Core ()
 checkConflictingBinding LHS fc opName foundFixity use_site rhs = pure () -- don't check if we're on the LHS
 checkConflictingBinding side fc opName foundFixity use_site rhs
     = if isCompatible foundFixity use_site
          then pure ()
-         else throw $ OperatorBindingMismatch {print = byShow} fc foundFixity use_site opName rhs
+         else throw $ OperatorBindingMismatch
+             {print = byShow} fc foundFixity use_site opName rhs !candidates
     where
       isCompatible : BacktickOrOperatorFixity -> OperatorLHSInfo PTerm -> Bool
       isCompatible Backticked (NoBinder lhs) = True
@@ -186,6 +189,12 @@ checkConflictingBinding side fc opName foundFixity use_site rhs
       isCompatible (DeclaredFixity fixInfo) (BindExplicitType name type expr)
           = fixInfo.bindingInfo == Autobind
 
+      candidates : Core (List String)
+      candidates = do Just (nm, cs) <- getSimilarNames opName
+                        | Nothing => pure []
+                      ns <- currentNS <$> get Ctxt
+                      pure (showSimilarNames ns opName nm cs)
+
 checkValidFixity : BindingModifier -> Fixity -> Nat -> Bool
 
 -- If the fixity declaration is not binding, there are no restrictions

src/Idris/Error.idr

@@ -625,7 +625,7 @@ perrorRaw (GenericMsgSol fc header solutions)
        <+> line
        <+> "Possible solutions:" <+> line
        <+> indent 1 (vsep (map (\s => "-" <++> pretty0 s) solutions))
-perrorRaw (OperatorBindingMismatch fc {print=p} expected actual opName rhs)
+perrorRaw (OperatorBindingMismatch fc {print=p} expected actual opName rhs candidates)
     = pure $ "Operator" <++> pretty0 !(getFullName opName) <++> "is"
        <++> printBindingInfo expected
        <++> "operator, but is used as" <++> printBindingModifier actual.getBinder
@@ -638,8 +638,15 @@ perrorRaw (OperatorBindingMismatch fc {print=p} expected actual opName rhs)
        <+> line <+> line
        <+> "Possible solutions:" <+> line
        <+> indent 1 (vsep (map ("-" <++>)
-           (expressionDiagnositc ++ [fixityDiagnostic, moduleDiagnostic])))
+           (expressionDiagnositc ++ [fixityDiagnostic, moduleDiagnostic] ++ spellingCandidates)))
     where
+      spellingCandidates : List (Doc IdrisAnn)
+      spellingCandidates = if null candidates
+                              then []
+                              else ["did you mean one of:" <++> hcat (punctuate ", "
+                                       (map byShow candidates))]
+
+
       moduleDiagnostic : Doc IdrisAnn
       moduleDiagnostic = case expected of
                               Backticked => "Import a module that exports a suitable fixity."

tests/idris2/operators/operators007/Test.idr

@@ -0,0 +1,11 @@
+
+import Data.Fin
+
+autobind infixr 0 >>
+infixr 0 !>
+
+(>>) : Monad m => m a -> (a -> m b) -> m b
+(>>) = (>>=)
+
+both : Maybe (Nat, Nat) -> Maybe Nat
+both m = (MkPair x y := m) !> Just (x + y)

tests/idris2/operators/operators007/expected

@@ -0,0 +1,17 @@
+1/1: Building Test (Test.idr)
+Error: Operator !> is a regular operator, but is used as an automatically-binding (autobind) operator.
+
+Test:11:28--11:30
+ 07 | (>>) : Monad m => m a -> (a -> m b) -> m b
+ 08 | (>>) = (>>=)
+ 09 |
+ 10 | both : Maybe (Nat, Nat) -> Maybe Nat
+ 11 | both m = (MkPair x y := m) !> Just (x + y)
+                                 ^^
+Explanation: regular, typebind and autobind operators all use a slightly different syntax, typebind looks like this: '(name : type) !> expr', autobind looks like this: '(name := expr) !> expr'.
+
+Possible solutions:
+ - Write the expression using regular syntax: 'm !> Just (x + y)'.
+ - Change the fixity defined at Test:5:1--5:12 to 'export autobind infixr 0 !>'.
+ - Hide or remove the fixity at Test:5:1--5:12 and import a module that exports a compatible fixity.
+ - Did you mean '>>' ?

tests/idris2/operators/operators007/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check Test.idr