Merge pull request #3315 from andrevidela/fix-3302

Emit error when unbound fixity is hidden

src/Core/Context.idr

@@ -796,7 +796,7 @@ HasNames Error where
   full gam (BadRunElab fc rho s desc) = BadRunElab fc <$> full gam rho <*> full gam s <*> pure desc
   full gam (RunElabFail e) = RunElabFail <$> full gam e
   full gam (GenericMsg fc x) = pure (GenericMsg fc x)
-  full gam (GenericMsgSol fc x y) = pure (GenericMsgSol fc x y)
+  full gam (GenericMsgSol fc x y z) = pure (GenericMsgSol fc x y z)
   full gam (TTCError x) = pure (TTCError x)
   full gam (FileErr x y) = pure (FileErr x y)
   full gam (CantFindPackage x) = pure (CantFindPackage x)
@@ -894,7 +894,7 @@ HasNames Error where
   resolved gam (BadRunElab fc rho s desc) = BadRunElab fc <$> resolved gam rho <*> resolved gam s <*> pure desc
   resolved gam (RunElabFail e) = RunElabFail <$> resolved gam e
   resolved gam (GenericMsg fc x) = pure (GenericMsg fc x)
-  resolved gam (GenericMsgSol fc x y) = pure (GenericMsgSol fc x y)
+  resolved gam (GenericMsgSol fc x y z) = pure (GenericMsgSol fc x y z)
   resolved gam (TTCError x) = pure (TTCError x)
   resolved gam (FileErr x y) = pure (FileErr x y)
   resolved gam (CantFindPackage x) = pure (CantFindPackage x)

src/Core/Core.idr

@@ -163,7 +163,8 @@ data Error : Type where
                   FC -> Env Term vars -> Term vars -> (description : String) -> Error
      RunElabFail : Error -> Error
      GenericMsg : FC -> String -> Error
-     GenericMsgSol : FC -> (message : String) -> (solutions : List String) -> Error
+     GenericMsgSol : FC -> (message : String) ->
+                           (solutionHeader : String) -> (solutions : List String) -> Error
      OperatorBindingMismatch : {a : Type} -> {print : a -> Doc ()} ->
          FC -> (expectedFixity : FixityDeclarationInfo) -> (use_site : OperatorLHSInfo a) ->
          -- left: backticked, right: op symbolds
@@ -356,7 +357,7 @@ Show Error where
   show (BadRunElab fc env script desc) = show fc ++ ":Bad elaborator script " ++ show script ++ " (" ++ desc ++ ")"
   show (RunElabFail e) = "Error during reflection: " ++ show e
   show (GenericMsg fc str) = show fc ++ ":" ++ str
-  show (GenericMsgSol fc msg sols) = show fc ++ ":" ++ msg ++ " Solutions: " ++ show sols
+  show (GenericMsgSol fc msg solutionHeader sols) = show fc ++ ":" ++ msg ++ " \{solutionHeader}: " ++ show sols
   show (TTCError msg) = "Error in TTC file: " ++ show msg
   show (FileErr fname err) = "File error (" ++ fname ++ "): " ++ show err
   show (CantFindPackage fname) = "Can't find package " ++ fname
@@ -472,7 +473,7 @@ getErrorLoc (BadImplicit loc _) = Just loc
 getErrorLoc (BadRunElab loc _ _ _) = Just loc
 getErrorLoc (RunElabFail e) = getErrorLoc e
 getErrorLoc (GenericMsg loc _) = Just loc
-getErrorLoc (GenericMsgSol loc _ _) = Just loc
+getErrorLoc (GenericMsgSol loc _ _ _) = Just loc
 getErrorLoc (TTCError _) = Nothing
 getErrorLoc (FileErr _ _) = Nothing
 getErrorLoc (CantFindPackage _) = Nothing
@@ -562,7 +563,7 @@ killErrorLoc (BadImplicit fc x) = BadImplicit emptyFC x
 killErrorLoc (BadRunElab fc x y description) = BadRunElab emptyFC x y description
 killErrorLoc (RunElabFail e) = RunElabFail $ killErrorLoc e
 killErrorLoc (GenericMsg fc x) = GenericMsg emptyFC x
-killErrorLoc (GenericMsgSol fc x y) = GenericMsgSol emptyFC x y
+killErrorLoc (GenericMsgSol fc x y z) = GenericMsgSol emptyFC x y z
 killErrorLoc (TTCError x) = TTCError x
 killErrorLoc (FileErr x y) = FileErr x y
 killErrorLoc (CantFindPackage x) = CantFindPackage x

src/Core/Name.idr

@@ -8,6 +8,8 @@ import Libraries.Text.PrettyPrint.Prettyprinter
 import Libraries.Text.PrettyPrint.Prettyprinter.Util
 import Libraries.Utils.String
 
+import Libraries.Text.Distance.Levenshtein as Distance
+
 import public Core.Name.Namespace
 
 %default total
@@ -464,3 +466,27 @@ next (MN n i) = MN n (i + 1)
 next (UN n) = MN (show n) 0
 next (NS ns n) = NS ns (next n)
 next n = MN (show n) 0
+
+||| levenstein distance that needs to be reached in order for a
+||| namespace path to closely match another one.
+closeNamespaceDistance : Nat
+closeNamespaceDistance = 3
+
+||| Check if two strings are close enough to be similar, using the namespace
+||| distance criteria.
+closeDistance : String -> String -> IO Bool
+closeDistance s1 s2 = pure (!(Distance.compute s1 s2) < closeNamespaceDistance)
+
+||| Check if the test closely match the reference.
+||| We only check for namespaces and user-defined names.
+export
+closeMatch : (test, reference : Name) -> IO Bool
+closeMatch (NS pathTest nameTest) (NS pathRef nameRef)
+  = let extractNameString = toList . (map snd . isUN >=> isBasic)
+        unfoldedTest = unsafeUnfoldNamespace pathTest ++ extractNameString nameTest
+        unfoldedRef = unsafeUnfoldNamespace pathRef ++ extractNameString nameRef
+        tests : IO (List Nat) = traverse (uncurry Distance.compute) (zip unfoldedTest unfoldedRef)
+    in map ((<= closeNamespaceDistance) . sum) tests
+closeMatch (UN (Basic test)) (UN (Basic ref)) = closeDistance test ref
+closeMatch _ _ = pure False
+

src/Idris/Desugar.idr

@@ -1219,7 +1219,7 @@ mutual
   desugarDecl ps fx@(PFixity fc vis binding fix prec opName)
       = do unless (checkValidFixity binding fix prec)
              (throw $ GenericMsgSol fc
-                 "Invalid fixity, \{binding} operator must be infixr 0."
+                 "Invalid fixity, \{binding} operator must be infixr 0." "Possible solutions"
                  [ "Make it `infixr 0`: `\{binding} infixr 0 \{show opName}`"
                  , "Remove the binding keyword: `\{fix} \{show prec} \{show opName}`"
                  ])
@@ -1306,7 +1306,7 @@ mutual
   desugarDecl ps (PDirective fc d)
       = case d of
              Hide (HideName n) => pure [IPragma fc [] (\nest, env => hide fc n)]
-             Hide (HideFixity fx n) => pure [IPragma fc [] (\_, _ => removeFixity fx n)]
+             Hide (HideFixity fx n) => pure [IPragma fc [] (\_, _ => removeFixity fc fx n)]
              Unhide n => pure [IPragma fc [] (\nest, env => unhide fc n)]
              Logging i => pure [ILog ((\ i => (topics i, verbosity i)) <$> i)]
              LazyOn a => pure [IPragma fc [] (\nest, env => lazyActive a)]

src/Idris/Error.idr

@@ -111,7 +111,7 @@ Eq Error where
   BadRunElab fc1 rho1 s1 d1 == BadRunElab fc2 rho2 s2 d2 = fc1 == fc2 && d1 == d2
   RunElabFail e1 == RunElabFail e2 = e1 == e2
   GenericMsg fc1 x1 == GenericMsg fc2 x2 = fc1 == fc2 && x1 == x2
-  GenericMsgSol fc1 x1 y1 == GenericMsgSol fc2 x2 y2 = fc1 == fc2 && x1 == x2 && y1 == y2
+  GenericMsgSol fc1 x1 y1 z1 == GenericMsgSol fc2 x2 y2 z2 = fc1 == fc2 && x1 == x2 && y1 == y2 && z1 == z2
   TTCError x1 == TTCError x2 = x1 == x2
   FileErr x1 y1 == FileErr x2 y2 = x1 == x2 && y1 == y2
   CantFindPackage x1 == CantFindPackage x2 = x1 == x2
@@ -621,10 +621,10 @@ 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)
+perrorRaw (GenericMsgSol fc header solutionHeader solutions)
     = pure $ pretty0 header <+> line <+> !(ploc fc)
        <+> line
-       <+> "Possible solutions:" <+> line
+       <+> fromString "\{solutionHeader}:" <+> line
        <+> 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"

src/Idris/Syntax.idr

@@ -1035,11 +1035,29 @@ addModDocInfo mi doc reexpts
                  , modDocexports $= insert mi reexpts
                  , modDocstrings $= insert mi doc }
 
--- remove a fixity from the context
+||| Remove a fixity from the context
 export
 removeFixity :
-    {auto s : Ref Syn SyntaxInfo} -> Fixity -> Name -> Core ()
-removeFixity _ key = update Syn ({fixities $= removeExact key })
+  {auto s : Ref Syn SyntaxInfo} -> FC -> Fixity -> Name -> Core ()
+removeFixity loc _ key = do
+  fixityInfo <- fixities <$> get Syn
+  if isJust $ lookupExact key fixityInfo
+     then -- When the fixity is found, simply remove it
+       update Syn ({ fixities $= removeExact key })
+     else -- When the fixity is not found, find close matches
+       let fixityNames : List Name = map fst (toList fixityInfo)
+           closeNames = !(filterM (coreLift . closeMatch key) fixityNames)
+           sameName : List Name = fst <$> lookupName (dropAllNS key) fixityInfo
+           similarNamespaces = nub (closeNames ++ sameName)
+       in if null similarNamespaces
+             then
+               throw $ GenericMsg loc "Fixity \{show key} not found"
+             else
+               throw $ GenericMsgSol loc "Fixity \{show key} not found" "Did you mean"
+                 $ map printFixityHide similarNamespaces
+  where
+    printFixityHide : Name -> String
+    printFixityHide nm = "%hide \{show nm}"
 
 ||| Return all fixity declarations for an operator name
 export

src/Libraries/Utils/Shunting.idr

@@ -96,13 +96,13 @@ higher : Interpolation op => (showLoc : Show op) => FC -> op -> OpPrec -> op ->
 higher loc opx op opy (Prefix p) = pure False
 higher loc opx (NonAssoc x) opy oy
     = if x == getPrec oy
-         then throw (GenericMsgSol loc ( "Operator \{opx} is non-associative")
+         then throw (GenericMsgSol loc "Operator \{opx} is non-associative" "Possible solutions"
                                        [ "Add brackets around every use of \{opx}"
                                        , "Change the fixity of \{show opx} to `infixl` or `infixr`"])
          else pure (x > getPrec oy)
 higher loc opx ox opy (NonAssoc y)
     = if getPrec ox == y
-         then throw (GenericMsgSol loc ( "Operator \{opy} is non-associative")
+         then throw (GenericMsgSol loc "Operator \{opy} is non-associative" "Possible solutions"
                                        [ "Add brackets around every use of \{opy}"
                                        , "Change the fixity of \{show opy} to `infixl` or `infixr`"])
          else pure (getPrec ox > y)

tests/idris2/operators/operators011/Module.idr

@@ -0,0 +1,3 @@
+module Module
+
+export infixl 7 &&++

tests/idris2/operators/operators011/Test.idr

@@ -0,0 +1,2 @@
+
+%hide DoesNotExist.infixl.(+-+)

tests/idris2/operators/operators011/Test1.idr

@@ -0,0 +1,3 @@
+import Module
+
+%hide Modul.infixl.(&&++)

tests/idris2/operators/operators011/Test2.idr

@@ -0,0 +1,3 @@
+import Module
+
+%hide Module.infixr.(&&++)

tests/idris2/operators/operators011/Test3.idr

@@ -0,0 +1,3 @@
+import Module
+
+%hide Module.infixl.(&&+*)

tests/idris2/operators/operators011/Test4.idr

@@ -0,0 +1,4 @@
+
+import Module
+
+%hide DoesNotExist.infixl.(&&++)

tests/idris2/operators/operators011/expected

@@ -0,0 +1,54 @@
+1/1: Building Test (Test.idr)
+Error: Fixity DoesNotExist.infixl.(+-+) not found
+
+Test:2:1--2:32
+ 1 | 
+ 2 | %hide DoesNotExist.infixl.(+-+)
+     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+1/2: Building Module (Module.idr)
+2/2: Building Test1 (Test1.idr)
+Error: Fixity Modul.infixl.(&&++) not found
+
+Test1:3:1--3:26
+ 1 | import Module
+ 2 | 
+ 3 | %hide Modul.infixl.(&&++)
+     ^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Did you mean:
+ - %hide Module.infixl.(&&++)
+2/2: Building Test2 (Test2.idr)
+Error: Fixity Module.infixr.(&&++) not found
+
+Test2:3:1--3:27
+ 1 | import Module
+ 2 | 
+ 3 | %hide Module.infixr.(&&++)
+     ^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Did you mean:
+ - %hide Module.infixl.(&&++)
+2/2: Building Test3 (Test3.idr)
+Error: Fixity Module.infixl.(&&+*) not found
+
+Test3:3:1--3:27
+ 1 | import Module
+ 2 | 
+ 3 | %hide Module.infixl.(&&+*)
+     ^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Did you mean:
+ - %hide Module.infixl.(&&++)
+2/2: Building Test4 (Test4.idr)
+Error: Fixity DoesNotExist.infixl.(&&++) not found
+
+Test4:4:1--4:33
+ 1 | 
+ 2 | import Module
+ 3 | 
+ 4 | %hide DoesNotExist.infixl.(&&++)
+     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Did you mean:
+ - %hide Module.infixl.(&&++)

tests/idris2/operators/operators011/run

@@ -0,0 +1,7 @@
+. ../../../testutils.sh
+
+check Test.idr
+check Test1.idr
+check Test2.idr
+check Test3.idr
+check Test4.idr