From 31ea83039c1ee9627b603bce5267bd5b236752bf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andr=C3=A9=20Videla?= Date: Sat, 20 Jan 2024 16:59:57 +0000 Subject: [PATCH] first attempt at suggesting different operators --- src/Core/Context.idr | 10 ++++++---- src/Core/Core.idr | 12 ++++++------ src/Idris/Desugar.idr | 13 +++++++++++-- src/Idris/Error.idr | 11 +++++++++-- tests/idris2/operators/operators007/Test.idr | 11 +++++++++++ tests/idris2/operators/operators007/expected | 17 +++++++++++++++++ tests/idris2/operators/operators007/run | 3 +++ 7 files changed, 63 insertions(+), 14 deletions(-) create mode 100644 tests/idris2/operators/operators007/Test.idr create mode 100644 tests/idris2/operators/operators007/expected create mode 100755 tests/idris2/operators/operators007/run diff --git a/src/Core/Context.idr b/src/Core/Context.idr index eae47cc22..d7d52015b 100644 --- a/src/Core/Context.idr +++ b/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) - = OperatorBindingMismatch {print} fc expected actual <$> full gam opName <*> pure rhs + full gam (OperatorBindingMismatch {print} fc expected actual opName rhs candidates) + = 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) - = OperatorBindingMismatch {print} fc expected actual <$> resolved gam opName <*> pure rhs + resolved gam (OperatorBindingMismatch {print} fc expected actual opName rhs candidates) + = OperatorBindingMismatch {print} fc expected actual + <$> resolved gam opName <*> pure rhs <*> pure candidates export HasNames Totality where diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 0fc0eaee3..8eaa16b60 100644 --- a/src/Core/Core.idr +++ b/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) - = OperatorBindingMismatch {print} emptyFC expected actual opName rhs +killErrorLoc (OperatorBindingMismatch {print} fc expected actual opName rhs candidates) + = OperatorBindingMismatch {print} emptyFC expected actual opName rhs candidates -- Core is a wrapper around IO that is specialised for efficiency. diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 79e25dcbd..21782b898 100644 --- a/src/Idris/Desugar.idr +++ b/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 diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 0426135b1..e855cb9e3 100644 --- a/src/Idris/Error.idr +++ b/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." diff --git a/tests/idris2/operators/operators007/Test.idr b/tests/idris2/operators/operators007/Test.idr new file mode 100644 index 000000000..61049346d --- /dev/null +++ b/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) diff --git a/tests/idris2/operators/operators007/expected b/tests/idris2/operators/operators007/expected new file mode 100644 index 000000000..85f117972 --- /dev/null +++ b/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 '>>' ? diff --git a/tests/idris2/operators/operators007/run b/tests/idris2/operators/operators007/run new file mode 100755 index 000000000..d35387bb3 --- /dev/null +++ b/tests/idris2/operators/operators007/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Test.idr