[ Proposal ] Search only appropriate operator

src/Core/TT.idr

@@ -201,18 +201,18 @@ data FixityDeclarationInfo = UndeclaredFixity | DeclaredFixity FixityInfo
 -- - not autobind, a regular operator
 -- - binding types, such that `(nm : ty) =@ fn nm` desugars into `(=@) ty (\(nm : ty) => fn nm)`
 -- - binding expressing with an inferred type such that
---   `(nm := exp) =@ fn nm` desugars into `(=@) exp (\(nm : ?) => fn nm)`
+--   `(nm <- exp) =@ fn nm` desugars into `(=@) exp (\(nm : ?) => fn nm)`
 -- - binding both types and expression such that
---   `(nm : ty := exp) =@ fn nm` desugars into `(=@) exp (\(nm : ty) => fn nm)`
+--   `(nm : ty <- exp) =@ fn nm` desugars into `(=@) exp (\(nm : ty) => fn nm)`
 public export
 data OperatorLHSInfo : tm -> Type where
   -- Traditional operator wihtout binding, carries the lhs
   NoBinder : (lhs : tm) -> OperatorLHSInfo tm
   -- (nm : ty) =@ fn x
   BindType : (name : tm) -> (ty : tm) -> OperatorLHSInfo tm
-  -- (nm := exp) =@ fn nm
+  -- (nm <- exp) =@ fn nm
   BindExpr : (name : tm) -> (expr : tm) -> OperatorLHSInfo tm
-  -- (nm : ty := exp) =@ fn nm
+  -- (nm : ty <- exp) =@ fn nm
   BindExplicitType : (name : tm) ->  (type, expr : tm) -> OperatorLHSInfo tm
 
 export

src/Idris/Desugar.idr

@@ -116,43 +116,76 @@ mkPrec Prefix = Prefix
   show ((x, DeclaredFixity y), _) = show x ++ " at " ++ show y.fc
   show ((x, UndeclaredFixity), _) = show x
 
+checkConflictingBinding : Ref Ctxt Defs =>
+                          Ref Syn SyntaxInfo =>
+                          WithFC OpStr -> (foundFixity : FixityInfo) ->
+                          (usage : OperatorLHSInfo PTerm) -> (rhs : PTerm) -> Core ()
+checkConflictingBinding opName foundFixity use_site rhs
+    = if isCompatible foundFixity use_site
+         then pure ()
+         else throw $ OperatorBindingMismatch
+             {print = byShow} opName.fc (DeclaredFixity foundFixity) use_site (opNameToEither opName.val) rhs !candidates
+    where
+
+      isCompatible : FixityInfo -> OperatorLHSInfo PTerm -> Bool
+      isCompatible fixInfo (NoBinder lhs) = fixInfo.bindingInfo == NotBinding
+      isCompatible fixInfo (BindType name ty) = fixInfo.bindingInfo == Typebind
+      isCompatible fixInfo (BindExpr name expr) = fixInfo.bindingInfo == Autobind
+      isCompatible fixInfo (BindExplicitType name type expr) = fixInfo.bindingInfo == Autobind
+
+      keepCompatibleBinding : BindingModifier -> (Name, GlobalDef) -> Core Bool
+      keepCompatibleBinding compatibleBinder (name, def) = do
+        fixities <- getFixityInfo (nameRoot name)
+        let compatible = any (\(_, fx) => fx.bindingInfo == use_site.getBinder) fixities
+        pure compatible
+
+      candidates : Core (List String)
+      candidates = do Just (nm, cs) <- getSimilarNames {keepPredicate = Just (keepCompatibleBinding foundFixity.bindingInfo)} opName.val.toName
+                        | Nothing => pure []
+                      ns <- currentNS <$> get Ctxt
+                      pure (showSimilarNames ns opName.val.toName nm cs)
+
 -- Check that an operator does not have any conflicting fixities in scope.
 -- Each operator can have its fixity defined multiple times across multiple
 -- modules as long as the fixities are consistent. If they aren't, the fixity
 -- can be hidden with %hide, this is handled by `removeFixity`.
 -- Once conflicts are handled we return the operator precedence we found.
 checkConflictingFixities : {auto s : Ref Syn SyntaxInfo} ->
                            {auto c : Ref Ctxt Defs} ->
-                           (isPrefix : Bool) ->
+                           (side : Side) ->
+                           (usageType : Maybe (OperatorLHSInfo PTerm, PTerm)) -> -- `Nothing` for prefix
                            WithFC (OpStr' Name) -> Core (OpPrec, FixityDeclarationInfo)
-checkConflictingFixities isPrefix opn
+checkConflictingFixities side usageType opn
   = do let op = nameRoot opn.val.toName
-       foundFixities <- getFixityInfo op
-       let (pre, inf) = partition ((== Prefix) . fix . snd) foundFixities
-       case (isPrefix, pre, inf) of
-            -- If we do not find any fixity, and it is a backticked operator, then we
-            -- return the default fixity and associativity for backticked operators
-            -- Otherwise, it's an unknown operator.
-            (_, [], []) => case opn.val of
-                              OpSymbols _ => throw (GenericMsg opn.fc "Unknown operator '\{op}'")
-                              Backticked _ =>  pure (NonAssoc 1, UndeclaredFixity) -- Backticks are non associative by default
-
-            (True, ((fxName, fx) :: _), _) => do
-                -- in the prefix case, remove conflicts with infix (-)
-                let extraFixities = pre ++ (filter (\(nm, _) => not $ nameRoot nm == "-") inf)
-                unless (isCompatible fx extraFixities) $ warnConflict fxName extraFixities
-                pure (mkPrec fx.fix fx.precedence, DeclaredFixity fx)
-            -- Could not find any prefix operator fixities, there may still be conflicts with
-            -- the infix ones.
-            (True, [] , _) => throw (GenericMsg opn.fc $ "'\{op}' is not a prefix operator")
-
-            (False, _, ((fxName, fx) :: _)) => do
-                -- In the infix case, remove conflicts with prefix (-)
-                let extraFixities = (filter (\(nm, _) => not $ nm == UN (Basic "-")) pre) ++ inf
-                unless (isCompatible fx extraFixities) $ warnConflict fxName extraFixities
-                pure (mkPrec fx.fix fx.precedence, DeclaredFixity fx)
-            -- Could not find any infix operator fixities, there may be prefix ones
-            (False, _, []) => throw (GenericMsg opn.fc $ "'\{op}' is not an infix operator")
+       foundFixities@(_::_) <- getFixityInfo op
+         | [] => do
+           -- If we do not find any fixity, and it is a backticked operator, then we
+           -- return the default fixity and associativity for backticked operators
+           -- Otherwise, it's an unknown operator.
+           case opn.val of
+              OpSymbols _ => throw (GenericMsg opn.fc "Unknown operator '\{op}'")
+              Backticked _ =>  pure (NonAssoc 1, UndeclaredFixity) -- Backticks are non associative by default
+
+       let (opType, f) : (String, _) = case usageType of
+                                         Nothing     => ("a prefix", (== Prefix) . fix)
+                                         Just (b, _) => do
+                                           let b = b.getBinder
+                                           ("a \{show b} infix", \op => op.fix /= Prefix && (op.bindingInfo == b || side == LHS))
+       let ops = filter (f . snd) foundFixities
+
+       case ops of
+         [] => do
+           unless (side == LHS) $ -- do not check for conflicting fixity on the LHS
+                                  -- This is because we do not parse binders on the lhs
+                                  -- and so, if we check, we will find uses of regular
+                                  -- operator when binding is expected.
+             whenJust usageType $ \(l, r) => do
+               whenJust (head' $ filter ((/= Prefix) . fix . snd) foundFixities) $ \(_, fx) =>
+                 checkConflictingBinding opn fx l r
+           throw (GenericMsg opn.fc $ "'\{op}' is not \{opType} operator")
+         (fxName, fx) :: _ => do
+           unless (isCompatible fx ops) $ warnConflict fxName ops
+           pure (mkPrec fx.fix fx.precedence, DeclaredFixity fx)
   where
     -- Fixities are compatible with all others of the same name that share the same
     -- fixity, precedence, and binding information
@@ -172,41 +205,6 @@ checkConflictingFixities isPrefix opn
                    For example: %hide \{show fxName}
                    """
 
-checkConflictingBinding : Ref Ctxt Defs =>
-                          Ref Syn SyntaxInfo =>
-                          WithFC OpStr -> (foundFixity : FixityDeclarationInfo) ->
-                          (usage : OperatorLHSInfo PTerm) -> (rhs : PTerm) -> Core ()
-checkConflictingBinding opName foundFixity use_site rhs
-    = if isCompatible foundFixity use_site
-         then pure ()
-         else throw $ OperatorBindingMismatch
-             {print = byShow} opName.fc foundFixity use_site (opNameToEither opName.val) rhs !candidates
-    where
-
-      isCompatible : FixityDeclarationInfo -> OperatorLHSInfo PTerm -> Bool
-      isCompatible UndeclaredFixity (NoBinder lhs) = True
-      isCompatible UndeclaredFixity _ = False
-      isCompatible (DeclaredFixity fixInfo) (NoBinder lhs) = fixInfo.bindingInfo == NotBinding
-      isCompatible (DeclaredFixity fixInfo) (BindType name ty) = fixInfo.bindingInfo == Typebind
-      isCompatible (DeclaredFixity fixInfo) (BindExpr name expr) = fixInfo.bindingInfo == Autobind
-      isCompatible (DeclaredFixity fixInfo) (BindExplicitType name type expr)
-          = fixInfo.bindingInfo == Autobind
-
-      keepCompatibleBinding : BindingModifier -> (Name, GlobalDef) -> Core Bool
-      keepCompatibleBinding compatibleBinder (name, def) = do
-        fixities <- getFixityInfo (nameRoot name)
-        let compatible = any (\(_, fx) => fx.bindingInfo == use_site.getBinder) fixities
-        pure compatible
-
-      candidates : Core (List String)
-      candidates = do let DeclaredFixity fxInfo = foundFixity
-                        | _ => pure [] -- if there is no declared fixity we can't know what's
-                                       -- supposed to go there.
-                      Just (nm, cs) <- getSimilarNames {keepPredicate = Just (keepCompatibleBinding fxInfo.bindingInfo)} opName.val.toName
-                        | Nothing => pure []
-                      ns <- currentNS <$> get Ctxt
-                      pure (showSimilarNames ns opName.val.toName nm cs)
-
 checkValidFixity : BindingModifier -> Fixity -> Nat -> Bool
 
 -- If the fixity declaration is not binding, there are no restrictions
@@ -231,16 +229,11 @@ parameters (side : Side)
               {auto c : Ref Ctxt Defs} ->
               PTerm -> Core (List (Tok ((OpStr, FixityDeclarationInfo), Maybe (OperatorLHSInfo PTerm)) PTerm))
   toTokList (POp fc (MkWithData _ l) opn r)
-      = do (precInfo, fixInfo) <- checkConflictingFixities False opn
-           unless (side == LHS) -- do not check for conflicting fixity on the LHS
-                                -- This is because we do not parse binders on the lhs
-                                -- and so, if we check, we will find uses of regular
-                                -- operator when binding is expected.
-                  (checkConflictingBinding opn fixInfo l r)
+      = do (precInfo, fixInfo) <- checkConflictingFixities side (Just (l, r)) opn
            rtoks <- toTokList r
            pure (Expr l.getLhs :: Op fc opn.fc ((opn.val, fixInfo), Just l) precInfo :: rtoks)
   toTokList (PPrefixOp fc opn arg)
-      = do (precInfo, fixInfo) <- checkConflictingFixities True opn
+      = do (precInfo, fixInfo) <- checkConflictingFixities side Nothing opn
            rtoks <- toTokList arg
            pure (Op fc opn.fc ((opn.val, fixInfo), Nothing) precInfo :: rtoks)
   toTokList t = pure [Expr t]

tests/idris2/misc/namespace005/expected

@@ -34,21 +34,6 @@ MainFail:7:27--7:30
                                ^^^
 
 2/2: Building Main3 (Main3.idr)
-Warning: operator fixity is ambiguous, we are picking Main3.prefix.(%%%) out of :
- - Main3.prefix.(%%%), precedence level 4
- - Lib1.infixr.(%%%), precedence level 5
-
-To remove this warning, use `%hide` with the fixity to remove
-For example: %hide Main3.prefix.(%%%)
-
-Main3:12:29--12:32
- 08 | (%%%) : Nat -> Nat
- 09 | (%%%) = S
- 10 | 
- 11 | main : IO ()
- 12 | main = do printLn (the Nat (%%% 4))
-                                  ^^^
-
 Warning: operator fixity is ambiguous, we are picking Prelude.Ops.infixl.(-) out of :
  - Prelude.Ops.infixl.(-), precedence level 8
  - Main3.infixr.(-), precedence level 8

tests/idris2/operators/operators013/Neg.idr

@@ -0,0 +1,10 @@
+private prefix 0 *&*&*&*&*&*&*&*&*
+
+badRegular : Nat
+badRegular = 5 *&*&*&*&*&*&*&*&* 6
+
+badTypebind : Nat
+badTypebind = (x : Nat) *&*&*&*&*&*&*&*&* 6
+
+badAutobind : Nat
+badAutobind = (x <- 5) *&*&*&*&*&*&*&*&* 6

tests/idris2/operators/operators013/Pos0.idr

@@ -0,0 +1,9 @@
+import Data.Vect
+
+export typebind infixr 0 *
+
+(*) : (a : Type) -> (a -> Type) -> Type
+(*) = DPair
+
+aPair : (n : Nat) * Vect n Nat
+aPair = (_ ** [1, 2, 3, 4, 5])

tests/idris2/operators/operators013/Pos1.idr

@@ -0,0 +1,19 @@
+import Data.Vect
+
+export typebind infixr 0 ***
+export infix 1 ***
+
+namespace DPairType
+
+  public export
+  (***) : (a : Type) -> (a -> Type) -> Type
+  (***) = DPair
+
+namespace DPairVal
+
+  public export
+  (***) : {0 f : _} -> (x : a) -> f x -> (x : a) *** f x
+  (***) = MkDPair
+
+anotherPair : (a : Type) *** (n : Nat) *** Vect n a
+anotherPair = Nat *** (5 *** [1, 2, 3, 4, 5])

tests/idris2/operators/operators013/Pos2.idr

@@ -0,0 +1,20 @@
+import Data.Vect
+
+namespace DPairType
+
+  export typebind infixr 0 ***
+
+  public export
+  (***) : (a : Type) -> (a -> Type) -> Type
+  (***) = DPair
+
+namespace DPairVal
+
+  export infixr 0 ***
+
+  public export
+  (***) : {0 f : _} -> (x : a) -> f x -> (x : a) *** f x
+  (***) = MkDPair
+
+anotherPair : (a : Type) *** (n : Nat) *** Vect n a
+anotherPair = Nat *** 5 *** [1, 2, 3, 4, 5]

tests/idris2/operators/operators013/expected

@@ -0,0 +1,33 @@
+1/1: Building Pos0 (Pos0.idr)
+1/1: Building Pos1 (Pos1.idr)
+1/1: Building Pos2 (Pos2.idr)
+1/1: Building Neg (Neg.idr)
+Error: '*&*&*&*&*&*&*&*&*' is not a regular infix operator
+
+Neg:4:16--4:33
+ 1 | private prefix 0 *&*&*&*&*&*&*&*&*
+ 2 | 
+ 3 | badRegular : Nat
+ 4 | badRegular = 5 *&*&*&*&*&*&*&*&* 6
+                    ^^^^^^^^^^^^^^^^^
+
+Error: '*&*&*&*&*&*&*&*&*' is not a typebind infix operator
+
+Neg:7:25--7:42
+ 3 | badRegular : Nat
+ 4 | badRegular = 5 *&*&*&*&*&*&*&*&* 6
+ 5 | 
+ 6 | badTypebind : Nat
+ 7 | badTypebind = (x : Nat) *&*&*&*&*&*&*&*&* 6
+                             ^^^^^^^^^^^^^^^^^
+
+Error: '*&*&*&*&*&*&*&*&*' is not a autobind infix operator
+
+Neg:10:24--10:41
+ 06 | badTypebind : Nat
+ 07 | badTypebind = (x : Nat) *&*&*&*&*&*&*&*&* 6
+ 08 | 
+ 09 | badAutobind : Nat
+ 10 | badAutobind = (x <- 5) *&*&*&*&*&*&*&*&* 6
+                             ^^^^^^^^^^^^^^^^^
+

tests/idris2/operators/operators013/run

@@ -0,0 +1,6 @@
+. ../../../testutils.sh
+
+check Pos0.idr
+check Pos1.idr
+check Pos2.idr
+check Neg.idr