add basic support for error messages during misuse

Author: andrevidela

src/Core/Context.idr

@@ -836,6 +836,8 @@ HasNames Error where
   full gam (OperatorBindingMismatch {print} fc expected actual (Right opName) rhs candidates)
       = OperatorBindingMismatch {print} fc expected actual
           <$> (Right <$> full gam opName) <*> pure rhs <*> pure candidates
+  full gam (BindingApplicationMismatch fc used bind others)
+      = BindingApplicationMismatch fc used <$> traverse (full gam) bind <*> traverse (full gam) others
 
   resolved gam (Fatal err) = Fatal <$> resolved gam err
   resolved _ (CantConvert fc gam rho s t)
@@ -934,7 +936,8 @@ HasNames Error where
   resolved gam (OperatorBindingMismatch {print} fc expected actual (Right opName) rhs candidates)
       = OperatorBindingMismatch {print} fc expected actual
           <$> (Right <$> resolved gam opName) <*> pure rhs <*> pure candidates
-
+  resolved gam (BindingApplicationMismatch fc used bind others)
+      = BindingApplicationMismatch fc used <$> traverse (resolved gam) bind <*> traverse (resolved gam) others
 export
 HasNames Totality where
   full gam (MkTotality t c) = pure $ MkTotality !(full gam t) !(full gam c)

src/Core/Core.idr

@@ -175,6 +175,12 @@ data Error : Type where
          FC -> (expectedFixity : FixityDeclarationInfo) -> (use_site : OperatorLHSInfo a) ->
          -- left: backticked, right: op symbolds
          (opName : Either Name Name) -> (rhs : a) -> (candidates : List String) -> Error
+     BindingApplicationMismatch :
+       FC ->
+       (bindingUsed : BindingModifier) ->
+       (bindingCandidates : List Name) ->
+       (nonBindingCandidates : List Name) ->
+       Error
      TTCError : TTCErrorMsg -> Error
      FileErr : String -> FileError -> Error
      CantFindPackage : String -> Error
@@ -414,6 +420,8 @@ Show Error where
   show (OperatorBindingMismatch fc UndeclaredFixity actual opName rhs _)
        = show fc ++ ": Operator " ++ show opName ++ " has no declared fixity"
        ++ " but used as a " ++ show actual ++ " operator"
+  show (BindingApplicationMismatch fc used binding notBinding)
+       = show fc ++ ": Application used \{show used} syntax but no such function exists"
 
 export
 getWarningLoc : Warning -> FC
@@ -505,6 +513,7 @@ getErrorLoc (InRHS _ _ err) = getErrorLoc err
 getErrorLoc (MaybeMisspelling err _) = getErrorLoc err
 getErrorLoc (WarningAsError warn) = Just (getWarningLoc warn)
 getErrorLoc (OperatorBindingMismatch loc _ _ _ _ _) = Just loc
+getErrorLoc (BindingApplicationMismatch loc _ _ _) = Just loc
 
 export
 killWarningLoc : Warning -> Warning
@@ -596,7 +605,8 @@ killErrorLoc (MaybeMisspelling err xs) = MaybeMisspelling (killErrorLoc err) xs
 killErrorLoc (WarningAsError wrn) = WarningAsError (killWarningLoc wrn)
 killErrorLoc (OperatorBindingMismatch {print} fc expected actual opName rhs candidates)
              = OperatorBindingMismatch {print} emptyFC expected actual opName rhs candidates
-
+killErrorLoc (BindingApplicationMismatch _ a b c)
+  = BindingApplicationMismatch emptyFC a b c
 
 -- Core is a wrapper around IO that is specialised for efficiency.
 export

src/Idris/Error.idr

@@ -628,7 +628,7 @@ perrorRaw (GenericMsgSol fc header solutionHeader solutions)
        <+> indent 1 (vsep (map (\s => "-" <++> pretty0 s) solutions))
 perrorRaw (OperatorBindingMismatch fc {print=p} expected actual opName rhs candidates)
     = pure $ "Operator" <++> pretty0 !(getFullName (fromEither opName)) <++> "is"
-       <++> printBindingInfo expected-- .bindingInfo
+       <++> printBindingInfo expected
        <++> "operator, but is used as" <++> printBindingModifier actual.getBinder
        <++> "operator."
        <+> line <+> !(ploc fc)
@@ -703,7 +703,23 @@ perrorRaw (OperatorBindingMismatch fc {print=p} expected actual opName rhs candi
       printBindingInfo : FixityDeclarationInfo -> Doc IdrisAnn
       printBindingInfo UndeclaredFixity = "a regular"
       printBindingInfo (DeclaredFixity x) = printBindingModifier x.bindingInfo
-
+perrorRaw (BindingApplicationMismatch fc used bind others)
+   = pure $ errorDesc $ reflow "Using \{show used} syntax but no function in scope is marked \{show used}"
+   <+> line
+   <+> !(ploc fc)
+   <+> line
+   <+> footer bind others
+   where
+     footer : List Name -> List Name -> Doc IdrisAnn
+     footer [] [] = reflow "There are no functions in scope that could match the current situation"
+     footer [] (x :: xs) =
+       reflow "Did you mean any of:"
+       <++> concatWith (surround (comma <+> space)) (map (code . pretty0) xs)
+       <+> comma <++> "or" <++> code (pretty0 x) <+> "?"
+     footer (x :: xs) ns1 =
+       reflow "Did you mean any of:"
+       <++> concatWith (surround (comma <+> space)) (map (code . pretty0) xs)
+       <+> comma <++> "or" <++> code (pretty0 x) <+> "?"
 
 perrorRaw (TTCError msg)
     = pure $ errorDesc (reflow "Error in TTC file" <+> colon <++> byShow msg)

src/TTImp/Elab/BindingApp.idr

@@ -9,33 +9,53 @@ import Core.Metadata
 import Core.Name
 import Core.Normalise
 
+import Data.List
+
 import TTImp.Elab.Check
 import TTImp.Elab.App
 import TTImp.TTImp
 
 import Idris.REPL.Opts
 import Idris.Syntax
 
-keepBinding : BindingModifier -> List GlobalDef -> List GlobalDef
-keepBinding mode = filter (\x => x.bindingMode == mode)
 
-parameters (originalName : WithFC Name) {auto c : Ref Ctxt Defs}
-  checkUnique : List GlobalDef -> Core GlobalDef
-  checkUnique [ def ] = pure def
-  checkUnique [] = throw $ UndefinedName originalName.fc originalName.val
-  checkUnique defs = throw $ AmbiguousName originalName.fc (map fullname defs)
+
+record BindingModes (a : Type) where
+  constructor MkBindingModes
+  everythingMatches : List a
+  bindingDoesNotMatch : List a
+  notBinding : List a
+
+keepBinding : BindingModifier -> List GlobalDef -> BindingModes GlobalDef
+keepBinding mode = foldl sortBinding (MkBindingModes [] [] [])
+  where
+    sortBinding : BindingModes GlobalDef -> GlobalDef -> BindingModes GlobalDef
+    sortBinding modes def = if def.bindingMode == mode
+                               then {everythingMatches $= (def ::)} modes
+                               else if def.bindingMode == NotBinding
+                               then {notBinding $= (def ::)} modes
+                               else {bindingDoesNotMatch $= (def ::)} modes
+
+
+parameters (originalName : WithFC Name) (mode : BindingModifier) {auto c : Ref Ctxt Defs}
+  checkUnique : BindingModes GlobalDef -> Core GlobalDef
+  checkUnique (MkBindingModes [ def ] _ _ ) = pure def
+  checkUnique (MkBindingModes [] may others) = do
+      coreLift $ putStrLn (show $ map fullname others)
+      throw $ BindingApplicationMismatch originalName.fc mode (map fullname may) (map fullname others)
+  checkUnique (MkBindingModes defs _ _) = throw $ AmbiguousName originalName.fc (map fullname defs)
 
   typecheckCandidates : List GlobalDef -> Core (List GlobalDef)
-  typecheckCandidates xs = pure xs -- todo
+  typecheckCandidates xs = pure xs -- todo: emit errors when the type doesn't match
 
-  checkBinding : (mode : BindingModifier) -> (candidates : List GlobalDef) -> Core GlobalDef
-  checkBinding mode candidates = do
+  checkBinding : (candidates : List GlobalDef) -> Core GlobalDef
+  checkBinding candidates = do
     log "elab.bindApp"  10 $ "Potential candidates for binding identifer : \{show (map fullname candidates)}"
     log "elab.bindApp"  10 $ "Checking if candidates have binding \{show mode}"
-    let bindingCandidates = keepBinding mode candidates
-    log "elab.bindApp"  10 $ "Final list of binding identifers : \{show (map fullname bindingCandidates)}"
-    wellTypedCandidates <- typecheckCandidates bindingCandidates
-    checkUnique bindingCandidates
+    let candidates = keepBinding mode candidates
+    log "elab.bindApp"  10 $ "Final list of binding identifers : \{show (map fullname candidates.everythingMatches)}"
+    -- wellTypedCandidates <- typecheckCandidates bindingCandidates
+    checkUnique candidates
 
 typeForBinder : BindingInfo RawImp -> FC -> RawImp
 typeForBinder (BindType name type) = const type

tests/idris2/basic/binding003/expected

@@ -1,8 +1,30 @@
 1/1: Building Test (Test.idr)
-SHould warn about declaring typebind instead of autobind
+Should warn about declaring typebind instead of autobind
 1/1: Building Test2 (Test2.idr)
-Shouwl warn about autobind instead of typebind
+[]
+Error: While processing right hand side of List. Using autobind syntax but no function in scope is marked autobind
+
+Test2:12:10--12:15
+ 08 |   p2 : sy p1
+ 09 |
+ 10 |
+ 11 | List : Type -> Type
+ 12 | List a = Sigma (n <- Nat) | Fin n -> a
+               ^^^^^
+
+Did you mean to write: `Sigma (x : range)` using `Sigma` from module `Test3` on line 6?
 1/1: Building Test3 (Test3.idr)
-should warn about using typebind insteaf of autobind
+[Prelude.Interfaces.for]
+Error: While processing right hand side of main. Using typebind syntax but no function in scope is marked typebind
+
+Test3:10:8--10:11
+ 06 | range : List Nat
+ 07 | range = [1 .. 10]
+ 08 |
+ 09 | main : IO ()
+ 10 | main = for (x : range) | printLn x
+             ^^^
+
+Did you mean to write: `for (x <- range)` using `for` from module `Test3` on line 4?
 1/1: Building Test4 (Test4.idr)
-should warn about declaring auto instead of typebind
+Should warn about declaring autobind instead of typebind