Merge pull request #3120 from andrevidela/autobind

[ feature ] Typebind & autobind using Pi-like syntax

CHANGELOG_NEXT.md

@@ -26,6 +26,10 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 ### Language changes
 
+* Autobind and Typebind modifier on operators allow the user to
+  customise the syntax of operator to look more like a binder.
+  See [#3113](https://github.com/idris-lang/Idris2/issues/3113).
+
 ### Backend changes
 
 #### RefC

docs/source/reference/builtins.rst

@@ -47,7 +47,7 @@ To ensure that a type is optimized to an ``Integer``, use ``%builtin Natural`` i
     data MyNat
         = Succ MyNat
         | Zero
-    
+
     %builtin Natural MyNat
 
 Casting between natural numbers and integer
@@ -106,7 +106,7 @@ that a function is correct. It is your responsibility to make sure this is corre
     data ComplexNat
         = Zero
         | Succ ComplexNat
-    
+
     integerToMaybeNat : Integer -> Maybe ComplexNat
     integerToMaybeNat _ = ...
 

docs/source/reference/index.rst

@@ -22,6 +22,7 @@ This is a placeholder, to get set up with readthedocs.
    records
    literate
    overloadedlit
+   operators
    strings
    pragmas
    builtins

docs/source/reference/operators.rst

@@ -0,0 +1,341 @@
+.. _operators:
+
+*********
+Operators
+*********
+
+Idris2 does not have syntax blocs (like in Idris1) or mixfix operators (like in Agda).
+Instead, it expands on the abilities of infix operators to enable library designers
+to write Domain Specific Languages (DSLs) while keeping error messages under control.
+
+Because operators are not linked to function definitions, they are also part of the
+file namespacing and follow the same rules as other defintions.
+
+.. warning::
+   Operators can and will make some code less legible. Use with taste and caution.
+   This document is meant to be mainly used by library authors and advanced users.
+   If you are on the fence about using operators, err on the side of caution and
+   avoid them.
+
+Basics
+======
+
+Before we jump into the fancy features, let us explain how operators work
+for most users.
+
+When you see an expression
+
+
+.. code-block:: idris
+
+    1 + n
+
+It means that there is a function ``(+)`` and a *fixity* declaration
+in scope. A fixity for this operator looks like this
+
+.. code-block:: idris
+
+    infixl 8 +
+
+It starts with a fixity keyword, you have the choice to use either ``infixl``,
+``infixr``, ``infix`` or ``prefix``.
+
+``infixl`` means the operator is left-associative, so that successive applications
+of the operator will bracket to the left: ``n + m + 3 + x = (((n + m) + 3) + x)```.
+Similarly, ``infixr`` is right-associative, and ``infix`` is non-associative, so the
+brackets are mandatory. Here, we chose for ``+`` to be left-associative, hence ``infixl``.
+
+The number after the fixity indicate the *precedence level* of the operator, that is, if it should
+be bracketed before, or after, other operators used in the same expression. For example,
+we want ``*`` to *take precedence* over ``+`` we write:
+
+.. code-block:: idris
+
+    infixl 9 *
+
+This way, the expression ``n + m * x`` is correctly interpreted as ``n + (m * x)``.
+
+Fixity declarations are optional and change how a file is parsed, but you can
+use any function defined with operator symbols with parenthesis around it:
+
+.. code-block:: idris
+
+   -- those two are the same
+   n + 3
+   (+) n 3
+
+Because fixities are separated from the function definitions, a single operator
+can have 0 or multiple fixity definitions. In the next section, we explain how to
+deal with multiple fixity definitions.
+
+Fixity & Precedence Namespacing
+===============================
+Sometimes it could be that you need to import two libraries that export
+conflicting fixities. If that is the case, the compiler will emit a warning
+and pick one of the fixities to parse the file. If that happens, you should
+hide the fixity definitions that you do not wish to use. For this, use the
+``%hide`` directive, just like you would to hide a function definition, but
+use the fixity and the operator to hide at the end. Let's work through an
+example:
+
+.. code-block:: idris
+
+   module A
+   export infixl 8 -
+
+.. code-block:: idris
+
+   module B
+   export infixr 5 -
+
+.. code-block:: idris
+
+   module C
+
+   import A
+   import B
+
+   test : Int
+   test = 1 - 3 - 10
+
+This program will raise a warning on the last line of module ``C`` because
+there are two conflicting fixities in scope. Should we parse the expression
+as ``(1 - 3) - 10`` or as ``1 - (3 - 10)``? In those cases, you can hide
+the extra fixity you do not wish to use by using ``%hide``:
+
+.. code-block:: idris
+
+   module C
+
+   import A
+   import B
+
+   %hide A.infixl.(-)
+
+   test : Int
+   test = 1 - 3 - 10 -- all good, no error
+
+In which case the program will be parsed as ``1 - (3 - 10)`` and not emit
+any errors.
+
+Export modifiers on fixities
+----------------------------
+
+Just like other top-level declarations in the language, fixities can be exported
+with the ``export`` access modifier, or kept private with ``private``.
+
+A ``private`` fixity will remain in scope for the rest of the file but will not be
+visible to users that import the module. Because fixities and operators are
+separate, this does not mean you cannot use the functions that have this operator
+name, it merely means that you cannot use it in infix position. But you can use
+it as a regular function application using brackets. Let us see what this
+looks like
+
+.. code-block:: idris
+
+   module A
+
+   private infixl &&& 8
+
+   -- a binary function making use of our fixity definition
+   export
+   (&&&) : ...
+
+.. code-block:: idris
+
+   module B
+
+   import A
+
+   main : IO ()
+   main = do print (a &&& b) -- won't work
+             print ((&&&) a b) -- ok
+
+In what follows, we have two examples of programs that benefit from
+declaring a fixity ``private`` rather than ``export``.
+
+Private record fixity pattern
+-----------------------------
+
+Private fixity declarations are useful in conjuction with records. When
+you declare a record with operators as fields, it is helpful to write
+them in infix position. However, the compiler will also synthesize a
+projection function for the field that takes as first argument the
+a value of the record to project from. This makes using the operator
+as a binary infix operator impossible, since it now has 3 arguments.
+
+.. code-block:: idris
+
+
+   infixl 7 <@>
+
+   record SomeRelation (a : Type) where
+     (<@>) : a -> a -> Type
+     -- we use the field here in infix position
+     compose : {x, y, z : a} -> x <@> y -> y <@> z -> x <@> z
+
+   lteRel : SomeRelation Nat
+   lteRel = ...
+
+   -- we want to use <@> in infix position here as well but we cannot
+   natRel : Nat -> Nat -> Type
+   natRel x y = (<@>) lteRel x y
+
+What we really want to write is ``natRel x y = (<@>) x y`` but
+``(<@>)`` now has type ``SomeRelation a -> a -> a -> Type``.
+
+The solution is to define a private field with a private fixity
+and a public one which relies on proof search to find the appropriate
+argument:
+
+.. code-block:: idris
+
+   private infixl 7 <!@>
+   export  infixl 7 <@>
+
+   record SomeRelation (a : Type) where
+     (<!@>) : a -> a -> Type
+     compose : {x, y, z : a} -> x <!@> y -> y <!@> z -> x <!@> z
+
+   export
+   (<@>) : (rel : SomeRelation a) => a -> a -> Type
+   x <@> y = (<!@>) rel x y
+
+   %hint
+   lteRel : SomeRelation Nat
+   lteRel = ...
+
+   natRel : Nat -> Nat -> Type
+   natRel x y = x <@> y
+
+We define ``(<@>)`` as a projection function with an implicit parameter
+allowing it to be used as a binary operator once again.
+
+Private Local definition
+------------------------
+
+Private fixity definitions are useful when redefining an operator fixity
+in a module. This happens when multiple DSLs are imported as the same time
+and you do not want to expose conflicting fixity declarations:
+
+.. code-block:: idris
+
+   module Coproduct
+
+   import Product
+
+   -- mark this as private since we don't want to clash
+   -- with the Prelude + when importing the module
+   private infixr 5 +
+
+   data (+) : a -> a -> Type where
+     ...
+
+   distrib1 : {x, y, z : a} -> x + y + z -> (x + y) + z
+
+Here ``distrib1`` makes explicit use of the operator being defined as
+right-associative.
+
+Typebind Operators
+==================
+
+In dependently-typed programming, we have the ability define constructors which
+first argument is a type and the second is a type indexed over the first argument.
+A typical example of this is the dependent linear arrow:
+
+ .. code-block:: idris
+
+    infixr 0 =@
+    0 (=@) : (x : Type) -> (x -> Type) -> Type
+    (=@) x f = (1 v : x) -> f v
+
+
+However, when trying to use it in infix position, we have to use a lambda to populate the
+second argument:
+
+.. code-block:: idris
+
+   linearSingleton : Nat =@ (\x => Singleton x)
+   linearSingleton = ...
+
+What we really want to write, is something like the dependent arrow ``->`` but
+for linear types:
+
+.. code-block:: idris
+
+   linearSingleton : (x : Nat) =@ Singleton x
+   linearSingleton = ...
+
+The above syntax is allowed if the operator is declared as ``typebind``. For
+this, simply add the ``typebind`` keyword in front of the fixity declaration.
+
+.. code-block:: idris
+
+   typebind infixr 0 =@
+
+``typebind`` is a modifier like ``export`` and both can be used at the same time.
+
+
+An operator defined as ``typebind`` cannot be used in regular position anymore,
+writing ``Nat =@ (\x => Singleton x)`` will raise an error.
+
+This new syntax is purely syntax sugar and converts any instance of
+``(name : type) op expr`` into ``type op (\name : type => expr)``
+
+Because of its left-to-right binding structure, typebind operators can
+only ever be ``infixr`` with precedence 0.
+
+
+Autobind Operators
+==================
+
+Typebind operators allow to bind a *type* on the left side of an operator, so that is can
+be used as the index of the second argument. But sometimes, there is no dependency
+between the first and second argument, yet we still want to use binding syntax. For those
+cases, we use ``autobind``.
+
+An example of this is a DSL for a dependently-typed programming language
+where the constructor for ``Pi`` takes terms on the left and lambdas on the right:
+
+.. code-block:: idris
+
+    VPi : Value -> (Value -> Value) -> Value
+
+    sig : Value
+    sig = VPi VStar                 (\fstTy -> VPi
+          (VPi fstTy (const VStar)) (\sndTy -> VPi
+          fstTy                     (\val1 -> VPi
+          (sndTy `vapp` val1)       (\val2 ->
+          VSigma fstTy sndTy)))))
+
+We would like to use a custom operator to build values using ``VPi``, but its
+signature does not follow the pattern that ``typebind`` uses. Instead, we use
+``autobind`` to tell the compiler that the type of the lambda must be inferred.
+For this we use ``:=`` instead of ``:``:
+
+.. code-block:: idris
+
+    autobind infixr 0 =>>
+    (=>>) : Value -> (Value -> Value) -> Value
+    (=>>) = VPi
+
+
+    sig : Value
+    sig =
+        (fstTy := VStar) =>>
+        (sndTy := (_ := fstTy) =>> VStar) =>>
+        (val1 := fstTy) =>>
+        (val2 := sndTy `vapp` val1) =>>
+        VSigma fstTy sndTy
+
+This new syntax is much closer to what the code is meant to look like for users
+accustomed to dependently-typed programming languages.
+
+More technically, any ``autobind`` operator is called with the syntax
+``(name := expr) op body`` and is desugared into ``expr op (\name : ? => body)``.
+If you want, or need, to give the type explicitly, you can still do so by using
+the full syntax: ``(name : type := expr) op body`` which is desugared into
+``expr op (\name : type => body)``.
+
+Like ``typebind``, ``autobind`` operators cannot be used as regular operators anymore
+, additionally an ``autobind`` operator cannot use the ``typebind`` syntax either.

src/Core/Binary.idr

@@ -29,7 +29,7 @@ import public Libraries.Utils.Binary
 ||| version number if you're changing the version more than once in the same day.
 export
 ttcVersion : Int
-ttcVersion = 2023_09_08_00
+ttcVersion = 2024_01_23_00
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Core/Context.idr

@@ -796,6 +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 (TTCError x) = pure (TTCError x)
   full gam (FileErr x y) = pure (FileErr x y)
   full gam (CantFindPackage x) = pure (CantFindPackage x)
@@ -820,6 +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 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)
@@ -887,6 +891,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 (TTCError x) = pure (TTCError x)
   resolved gam (FileErr x y) = pure (FileErr x y)
   resolved gam (CantFindPackage x) = pure (CantFindPackage x)
@@ -911,6 +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 candidates)
+      = OperatorBindingMismatch {print} fc expected actual
+          <$> resolved gam opName <*> pure rhs <*> pure candidates
 
 export
 HasNames Totality where
@@ -1123,7 +1131,10 @@ getFieldNames ctxt recNS
 -- Find similar looking names in the context
 export
 getSimilarNames : {auto c : Ref Ctxt Defs} ->
-                   Name -> Core (Maybe (String, List (Name, Visibility, Nat)))
+                  -- Predicate run to customise the behavior of looking for similar names
+                  -- Sometime we might want to hide names that we know make no sense.
+                  {default Nothing keepPredicate : Maybe ((Name, GlobalDef) -> Core Bool)} ->
+                  Name -> Core (Maybe (String, List (Name, Visibility, Nat)))
 getSimilarNames nm = case show <$> userNameRoot nm of
   Nothing => pure Nothing
   Just str => if length str <= 1 then pure (Just (str, [])) else
@@ -1137,6 +1148,9 @@ getSimilarNames nm = case show <$> userNameRoot nm of
                    | False => pure Nothing
                Just def <- lookupCtxtExact nm (gamma defs)
                    | Nothing => pure Nothing -- should be impossible
+               let predicate = fromMaybe (\_ => pure True) keepPredicate
+               True <- predicate (nm, def)
+                   | False => pure Nothing
                pure (Just (collapseDefault $ visibility def, dist))
        kept <- NameMap.mapMaybeM @{CORE} test (resolvedAs (gamma defs))
        pure $ Just (str, toList kept)

src/Core/Core.idr

@@ -10,6 +10,7 @@ import Data.Vect
 import Libraries.Data.IMaybe
 import Libraries.Text.PrettyPrint.Prettyprinter
 import Libraries.Text.PrettyPrint.Prettyprinter.Util
+import Libraries.Text.PrettyPrint.Prettyprinter.Doc
 import Libraries.Data.Tap
 
 import public Data.IORef
@@ -162,6 +163,10 @@ 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
+     OperatorBindingMismatch : {a : Type} -> {print : a -> Doc ()} ->
+         FC -> (expectedFixity : BacktickOrOperatorFixity) -> (use_site : OperatorLHSInfo a) ->
+         (opName : Name) -> (rhs : a) -> (candidates : List String) -> Error
      TTCError : TTCErrorMsg -> Error
      FileErr : String -> FileError -> Error
      CantFindPackage : String -> Error
@@ -350,6 +355,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 (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
@@ -390,10 +396,16 @@ Show Error where
          show err
 
   show (MaybeMisspelling err ns)
-     = show err ++ "\nDid you mean" ++ case ns of
+       = show err ++ "\nDid you mean" ++ case ns of
-         (n ::: []) => ": " ++ n ++ "?"
+           (n ::: []) => ": " ++ n ++ "?"
-         _ => " any of: " ++ showSep ", " (map show (forget ns)) ++ "?"
+           _ => " any of: " ++ showSep ", " (map show (forget ns)) ++ "?"
   show (WarningAsError w) = show w
+  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 fc ++ ": Operator " ++ show opName ++ " has no declared fixity"
+       ++ " but used as a " ++ show actual ++ " operator"
 
 export
 getWarningLoc : Warning -> FC
@@ -459,6 +471,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 (TTCError _) = Nothing
 getErrorLoc (FileErr _ _) = Nothing
 getErrorLoc (CantFindPackage _) = Nothing
@@ -483,6 +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
 
 export
 killWarningLoc : Warning -> Warning
@@ -547,6 +561,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 (TTCError x) = TTCError x
 killErrorLoc (FileErr x y) = FileErr x y
 killErrorLoc (CantFindPackage x) = CantFindPackage x
@@ -571,6 +586,9 @@ 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 candidates)
+             = OperatorBindingMismatch {print} emptyFC expected actual opName rhs candidates
+
 
 -- Core is a wrapper around IO that is specialised for efficiency.
 export

src/Core/TT.idr

@@ -15,6 +15,7 @@ import Decidable.Equality
 import Libraries.Data.NameMap
 import Libraries.Text.PrettyPrint.Prettyprinter
 import Libraries.Text.PrettyPrint.Prettyprinter.Util
+import Libraries.Text.Bounded
 import Libraries.Data.String.Extra
 
 import Libraries.Data.SnocList.SizeOf
@@ -101,6 +102,136 @@ Ord Visibility where
   compare Public Private = GT
   compare Public Export = GT
 
+public export
+data Fixity = InfixL | InfixR | Infix | Prefix
+
+export
+Show Fixity where
+  show InfixL = "infixl"
+  show InfixR = "infixr"
+  show Infix  = "infix"
+  show Prefix = "prefix"
+
+export
+Interpolation Fixity where
+  interpolate = show
+
+export
+Eq Fixity where
+  InfixL == InfixL = True
+  InfixR == InfixR = True
+  Infix == Infix = True
+  Prefix == Prefix = True
+  _ == _ = False
+
+
+public export
+data BindingModifier = NotBinding | Autobind | Typebind
+
+export
+Eq BindingModifier where
+  NotBinding == NotBinding = True
+  Autobind == Autobind = True
+  Typebind == Typebind = True
+  _ == _ = False
+
+export
+Show BindingModifier where
+  show NotBinding = "regular"
+  show Typebind = "typebind"
+  show Autobind = "autobind"
+
+export
+Interpolation BindingModifier where
+  interpolate = show
+
+-- A record to hold all the information about a fixity
+public export
+record FixityInfo where
+  constructor MkFixityInfo
+  fc : FC
+  vis : Visibility
+  bindingInfo : BindingModifier
+  fix : Fixity
+  precedence : Nat
+
+export
+Show FixityInfo where
+  show fx = "fc: \{show fx.fc}, visibility: \{show fx.vis}, binding: \{show fx.bindingInfo}, fixity: \{show fx.fix}, precedence: \{show fx.precedence}"
+
+
+export
+Eq FixityInfo where
+  x == y = x.fc == y.fc
+        && x.vis == y.vis
+        && x.bindingInfo == y.bindingInfo
+        && x.fix == y.fix
+        && x.precedence == y.precedence
+
+||| Whenever we read an operator from the parser, we don't know if it's a backticked expression with no fixity
+||| declaration, or if it has a fixity declaration. If it does not have a declaration, we represent this state
+||| with `Backticked`.
+||| Note that a backticked expression can have a fixity declaration, in which case it is represented with
+||| `DeclaredFixity`.
+public export
+data BacktickOrOperatorFixity = Backticked | DeclaredFixity FixityInfo
+
+-- Left-hand-side information for operators, carries autobind information
+-- an operator can either be
+-- - 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)`
+-- - binding both types and expression such that
+--   `(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
+  BindExpr : (name : tm) -> (expr : tm) -> OperatorLHSInfo tm
+  -- (nm : ty := exp) =@ fn nm
+  BindExplicitType : (name : tm) ->  (type, expr : tm) -> OperatorLHSInfo tm
+
+export
+Show (OperatorLHSInfo tm) where
+  show (NoBinder lhs)                    = "regular"
+  show (BindType name ty)                = "type-binding (typebind)"
+  show (BindExpr name expr)              = "automatically-binding (autobind)"
+  show (BindExplicitType name type expr) = "automatically-binding (autobind)"
+
+%name OperatorLHSInfo opInfo
+
+export
+Functor OperatorLHSInfo where
+  map f (NoBinder lhs) = NoBinder $ f lhs
+  map f (BindType nm lhs) = BindType (f nm) (f lhs)
+  map f (BindExpr nm lhs) = BindExpr (f nm) (f lhs)
+  map f (BindExplicitType nm ty lhs) = BindExplicitType (f nm) (f ty) (f lhs)
+
+export
+(.getLhs) : OperatorLHSInfo tm -> tm
+(.getLhs) (NoBinder lhs) = lhs
+(.getLhs) (BindExpr _ lhs) = lhs
+(.getLhs) (BindType _ lhs) = lhs
+(.getLhs) (BindExplicitType _ _ lhs) = lhs
+
+export
+(.getBoundPat) : OperatorLHSInfo tm -> Maybe tm
+(.getBoundPat) (NoBinder lhs) = Nothing
+(.getBoundPat) (BindType name ty) = Just name
+(.getBoundPat) (BindExpr name expr) = Just name
+(.getBoundPat) (BindExplicitType name type expr) = Just name
+
+export
+(.getBinder) : OperatorLHSInfo tm -> BindingModifier
+(.getBinder) (NoBinder lhs) = NotBinding
+(.getBinder) (BindType name ty) = Typebind
+(.getBinder) (BindExpr name expr) = Autobind
+(.getBinder) (BindExplicitType name type expr) = Autobind
+
 public export
 data TotalReq = Total | CoveringOnly | PartialOK
 %name TotalReq treq

src/Idris/Desugar.idr

@@ -105,6 +105,14 @@ mkPrec InfixR = AssocR
 mkPrec Infix  = NonAssoc
 mkPrec Prefix = Prefix
 
+-- This is used to print the error message for fixities
+[interpName] Interpolation ((Name, BacktickOrOperatorFixity), b) where
+  interpolate ((x, _), _) = show x
+
+[showWithLoc] Show ((Name, BacktickOrOperatorFixity), b) where
+  show ((x, DeclaredFixity y), _) = show x ++ " at " ++ show y.fc
+  show ((x, Backticked), _) = show x
+
 -- 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
@@ -113,39 +121,43 @@ mkPrec Prefix = Prefix
 checkConflictingFixities : {auto s : Ref Syn SyntaxInfo} ->
                            {auto c : Ref Ctxt Defs} ->
                            (isPrefix : Bool) ->
-                           FC -> Name -> Core OpPrec
+                           FC -> Name -> Core (OpPrec, BacktickOrOperatorFixity)
 checkConflictingFixities isPrefix exprFC opn
-  = do syn <- get Syn
+  = do let op = nameRoot opn
-       let op = nameRoot opn
+       foundFixities <- getFixityInfo op
-       let foundFixities : List (Name, FixityInfo) = lookupName (UN (Basic op)) (fixities syn)
        let (pre, inf) = partition ((== Prefix) . fix . snd) foundFixities
        case (isPrefix, pre, inf) of
             -- If we do not find any fixity for this operator we check that it uses operator
             -- characters, if not, it must be a backticked expression.
             (_, [], []) => if any isOpChar (fastUnpack op)
                               then throw (GenericMsg exprFC "Unknown operator '\{op}'")
-                              else pure (NonAssoc 1) -- Backticks are non associative by default
+                              else pure (NonAssoc 1, Backticked) -- 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)
+                pure (mkPrec fx.fix fx.precedence, DeclaredFixity fx)
-            -- Could not find any prefix operator fixities, there may be infix ones
+            -- Could not find any prefix operator fixities, there may still be conflicts with
+            -- the infix ones.
             (True, [] , _) => throw (GenericMsg exprFC $ "'\{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)
+                pure (mkPrec fx.fix fx.precedence, DeclaredFixity fx)
             -- Could not find any infix operator fixities, there may be prefix ones
             (False, _, []) => throw (GenericMsg exprFC $ "'\{op}' is not an infix operator")
   where
-    -- Fixities are compatible with all others of the same name that share the same fixity and precedence
+    -- Fixities are compatible with all others of the same name that share the same
+    -- fixity, precedence, and binding information
     isCompatible :  FixityInfo -> (fixities : List (Name, FixityInfo)) -> Bool
     isCompatible fx
-      = all (\fx' => fx.fix == fx'.fix && fx.precedence == fx'.precedence) . map snd
+      = all (\fx' => fx.fix == fx'.fix
+                  && fx.precedence == fx'.precedence
+                  && fx.bindingInfo == fx'.bindingInfo) . map snd
 
     -- Emits a warning using the fixity that we picked and the list of all conflicting fixities
     warnConflict : (picked : Name) -> (conflicts : List (Name, FixityInfo)) -> Core ()
@@ -157,18 +169,77 @@ checkConflictingFixities isPrefix exprFC opn
                    For example: %hide \{show fxName}
                    """
 
-toTokList : {auto s : Ref Syn SyntaxInfo} ->
+checkConflictingBinding : Ref Ctxt Defs =>
-            {auto c : Ref Ctxt Defs} ->
+                          Ref Syn SyntaxInfo =>
-            PTerm -> Core (List (Tok OpStr PTerm))
+                          FC -> Name -> (foundFixity : BacktickOrOperatorFixity) ->
-toTokList (POp fc opFC opn l r)
+                          (usage : OperatorLHSInfo PTerm) -> (rhs : PTerm) -> Core ()
-    = do precInfo <- checkConflictingFixities False fc opn
+checkConflictingBinding fc opName foundFixity use_site rhs
-         rtoks <- toTokList r
+    = if isCompatible foundFixity use_site
-         pure (Expr l :: Op fc opFC opn precInfo :: rtoks)
+         then pure ()
-toTokList (PPrefixOp fc opFC opn arg)
+         else throw $ OperatorBindingMismatch
-    = do precInfo <- checkConflictingFixities True fc opn
+             {print = byShow} fc foundFixity use_site opName rhs !candidates
-         rtoks <- toTokList arg
+    where
-         pure (Op fc opFC opn precInfo :: rtoks)
+      isCompatible : BacktickOrOperatorFixity -> OperatorLHSInfo PTerm -> Bool
-toTokList t = pure [Expr t]
+      isCompatible Backticked (NoBinder lhs) = True
+      isCompatible Backticked _ = 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
+                        | 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
+checkValidFixity NotBinding _ _ = True
+
+-- If the fixity declaration is not binding, either typebind or autobind
+-- the fixity can only be `infixr` with precedence `0`. We might want
+-- to revisit that in the future, but as of right now we want to be
+-- conservative and avoid abuse.
+-- having multiple precedence levels would mean that if
+-- =@ has higher precedence than -@
+-- the expression (x : a) =@ b -@ (y : List a) =@ List b
+-- would be bracketed as ((x : a) =@ b) -@ (y : List a) =@ List b
+-- instead of (x : a) =@ (b -@ ((y : List a) =@ List b))
+checkValidFixity _ InfixR 0 = True
+
+-- If it's binding but not infixr precedence 0, raise an error
+checkValidFixity _ _ _ = False
+
+parameters (side : Side)
+  toTokList : {auto s : Ref Syn SyntaxInfo} ->
+              {auto c : Ref Ctxt Defs} ->
+              PTerm -> Core (List (Tok ((OpStr, BacktickOrOperatorFixity), Maybe (OperatorLHSInfo PTerm)) PTerm))
+  toTokList (POp fc opFC l opn r)
+      = do (precInfo, fixInfo) <- checkConflictingFixities False fc 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 opFC opn fixInfo l r)
+           rtoks <- toTokList r
+           pure (Expr l.getLhs :: Op fc opFC ((opn, fixInfo), Just l) precInfo :: rtoks)
+  toTokList (PPrefixOp fc opFC opn arg)
+      = do (precInfo, fixInfo) <- checkConflictingFixities True fc opn
+           rtoks <- toTokList arg
+           pure (Op fc opFC ((opn, fixInfo), Nothing) precInfo :: rtoks)
+  toTokList t = pure [Expr t]
 
 record BangData where
   constructor MkBangData
@@ -308,12 +379,16 @@ mutual
                      [apply (IVar fc (UN $ Basic "===")) [l', r'],
                       apply (IVar fc (UN $ Basic "~=~")) [l', r']]
   desugarB side ps (PBracketed fc e) = desugarB side ps e
-  desugarB side ps (POp fc opFC op l r)
+  desugarB side ps (POp fc opFC l op r)
-      = do ts <- toTokList (POp fc opFC op l r)
+      = do ts <- toTokList side (POp fc opFC l op r)
-           desugarTree side ps !(parseOps ts)
+           tree <- parseOps @{interpName} @{showWithLoc} ts
+           unop <- desugarTree side ps (mapFst (\((x, _), y) => (x, y)) tree)
+           desugarB side ps unop
   desugarB side ps (PPrefixOp fc opFC op arg)
-      = do ts <- toTokList (PPrefixOp fc opFC op arg)
+      = do ts <- toTokList side (PPrefixOp fc opFC op arg)
-           desugarTree side ps !(parseOps ts)
+           tree <- parseOps @{interpName} @{showWithLoc} ts
+           unop <- desugarTree side ps (mapFst (\((x, _), y) => (x, y)) tree)
+           desugarB side ps unop
   desugarB side ps (PSectionL fc opFC op arg)
       = do syn <- get Syn
            -- It might actually be a prefix argument rather than a section
@@ -322,12 +397,12 @@ mutual
                 [] =>
                     desugarB side ps
                         (PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc)
-                            (POp fc opFC op (PRef fc (MN "arg" 0)) arg))
+                            (POp fc opFC (NoBinder (PRef fc (MN "arg" 0))) op arg))
                 (prec :: _) => desugarB side ps (PPrefixOp fc opFC op arg)
   desugarB side ps (PSectionR fc opFC arg op)
       = desugarB side ps
           (PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc)
-              (POp fc opFC op arg (PRef fc (MN "arg" 0))))
+              (POp fc opFC (NoBinder arg) op (PRef fc (MN "arg" 0))))
   desugarB side ps (PSearch fc depth) = pure $ ISearch fc depth
   desugarB side ps (PPrimVal fc (BI x))
       = case !fromIntegerName of
@@ -714,27 +789,48 @@ mutual
            rule' <- desugarDo side ps ns rule
            pure $ IRewrite fc rule' rest'
 
+  -- Replace all operator by function application
   desugarTree : {auto s : Ref Syn SyntaxInfo} ->
                 {auto b : Ref Bang BangData} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto u : Ref UST UState} ->
                 {auto m : Ref MD Metadata} ->
                 {auto o : Ref ROpts REPLOpts} ->
-                Side -> List Name -> Tree OpStr PTerm -> Core RawImp
+                Side -> List Name -> Tree (OpStr, Maybe $ OperatorLHSInfo PTerm) PTerm ->
-  desugarTree side ps (Infix loc eqFC (UN $ Basic "=") l r) -- special case since '=' is special syntax
+                Core PTerm
+  desugarTree side ps (Infix loc eqFC (UN $ Basic "=", _) l r) -- special case since '=' is special syntax
+      = pure $ PEq eqFC !(desugarTree side ps l) !(desugarTree side ps r)
+
+  desugarTree side ps (Infix loc _ (UN $ Basic "$", _) l r) -- special case since '$' is special syntax
       = do l' <- desugarTree side ps l
            r' <- desugarTree side ps r
-           pure (IAlternative loc FirstSuccess
+           pure (PApp loc l' r')
-                     [apply (IVar eqFC eqName) [l', r'],
+  -- normal operators
-                      apply (IVar eqFC heqName) [l', r']])
+  desugarTree side ps (Infix loc opFC (op, Just (NoBinder lhs)) l r)
-  desugarTree side ps (Infix loc _ (UN $ Basic "$") l r) -- special case since '$' is special syntax
       = do l' <- desugarTree side ps l
            r' <- desugarTree side ps r
-           pure (IApp loc l' r')
+           pure (PApp loc (PApp loc (PRef opFC op) l') r')
-  desugarTree side ps (Infix loc opFC op l r)
+  -- (x : ty) =@ f x ==>> (=@) ty (\x : ty => f x)
+  desugarTree side ps (Infix loc opFC (op, Just (BindType pat lhs)) l r)
       = do l' <- desugarTree side ps l
-           r' <- desugarTree side ps r
+           body <- desugarTree side ps r
-           pure (IApp loc (IApp loc (IVar opFC op) l') r')
+           pure $ PApp loc (PApp loc (PRef opFC op) l')
+                      (PLam loc top Explicit pat l' body)
+  -- (x := exp) =@ f x ==>> (=@) exp (\x : ? => f x)
+  desugarTree side ps (Infix loc opFC (op, Just (BindExpr pat lhs)) l r)
+      = do l' <- desugarTree side ps l
+           body <- desugarTree side ps r
+           pure $ PApp loc (PApp loc (PRef opFC op) l')
+                      (PLam loc top Explicit pat (PInfer opFC) body)
+
+  -- (x : ty := exp) =@ f x ==>> (=@) exp (\x : ty => f x)
+  desugarTree side ps (Infix loc opFC (op, Just (BindExplicitType pat ty expr)) l r)
+      = do l' <- desugarTree side ps l
+           body <- desugarTree side ps r
+           pure $ PApp loc (PApp loc (PRef opFC op) l')
+                      (PLam loc top Explicit pat ty body)
+  desugarTree side ps (Infix loc opFC (op, Nothing) _ r)
+      = throw $ InternalError "illegal fixity: Parsed as infix but no binding information"
 
   -- negation is a special case, since we can't have an operator with
   -- two meanings otherwise
@@ -742,7 +838,7 @@ mutual
   -- Note: In case of negated signed integer literals, we apply the
   -- negation directly. Otherwise, the literal might be
   -- truncated to 0 before being passed on to `negate`.
-  desugarTree side ps (Pre loc opFC (UN $ Basic "-") $ Leaf $ PPrimVal fc c)
+  desugarTree side ps (Pre loc opFC (UN $ Basic "-", _) $ Leaf $ PPrimVal fc c)
     = let newFC    = fromMaybe EmptyFC (mergeFC loc fc)
           continue = desugarTree side ps . Leaf . PPrimVal newFC
        in case c of
@@ -756,16 +852,16 @@ mutual
             -- not a signed integer literal. proceed by desugaring
             -- and applying to `negate`.
             _     => do arg' <- desugarTree side ps (Leaf $ PPrimVal fc c)
-                        pure (IApp loc (IVar opFC (UN $ Basic "negate")) arg')
+                        pure (PApp loc (PRef opFC (UN $ Basic "negate")) arg')
 
-  desugarTree side ps (Pre loc opFC (UN $ Basic "-") arg)
+  desugarTree side ps (Pre loc opFC (UN $ Basic "-", _) arg)
     = do arg' <- desugarTree side ps arg
-         pure (IApp loc (IVar opFC (UN $ Basic "negate")) arg')
+         pure (PApp loc (PRef opFC (UN $ Basic "negate")) arg')
 
-  desugarTree side ps (Pre loc opFC op arg)
+  desugarTree side ps (Pre loc opFC (op, _) arg)
       = do arg' <- desugarTree side ps arg
-           pure (IApp loc (IVar opFC op) arg')
+           pure (PApp loc (PRef opFC op) arg')
-  desugarTree side ps (Leaf t) = desugarB side ps t
+  desugarTree side ps (Leaf t) = pure t
 
   desugarType : {auto s : Ref Syn SyntaxInfo} ->
                 {auto c : Ref Ctxt Defs} ->
@@ -1109,8 +1205,14 @@ mutual
           NS ns (DN str (MN ("__mk" ++ str) 0))
       mkConName n = DN (show n) (MN ("__mk" ++ show n) 0)
 
-  desugarDecl ps (PFixity fc vis fix prec opName)
+  desugarDecl ps (PFixity fc vis binding fix prec opName)
-      = do ctx <- get Ctxt
+      = do unless (checkValidFixity binding fix prec)
+             (throw $ GenericMsgSol fc
+                 "Invalid fixity, \{binding} operator must be infixr 0."
+                 [ "Make it `infixr 0`: `\{binding} infixr 0 \{show opName}`"
+                 , "Remove the binding keyword: `\{fix} \{show prec} \{show opName}`"
+                 ])
+           ctx <- get Ctxt
            -- We update the context of fixities by adding a namespaced fixity
            -- given by the current namespace and its fixity name.
            -- This allows fixities to be stored along with the namespace at their
@@ -1118,7 +1220,7 @@ mutual
            let updatedNS = NS (mkNestedNamespace (Just ctx.currentNS) (show fix))
                               (UN $ Basic $ nameRoot opName)
 
-           update Syn { fixities $= addName updatedNS (MkFixityInfo fc vis fix prec) }
+           update Syn { fixities $= addName updatedNS (MkFixityInfo fc vis binding fix prec) }
            pure []
   desugarDecl ps d@(PFail fc mmsg ds)
       = do -- save the state: the content of a failing block should be discarded
@@ -1230,4 +1332,5 @@ mutual
             {auto u : Ref UST UState} ->
             {auto o : Ref ROpts REPLOpts} ->
             Side -> List Name -> PTerm -> Core RawImp
+
   desugar s ps tm = desugarDo s ps Nothing tm

src/Idris/Desugar/Mutual.idr

@@ -29,7 +29,7 @@ getDecl AsType (PRecord fc doc vis mbtot (MkPRecord n ps _ _ _))
     mkRecType : List (Name, RigCount, PiInfo PTerm, PTerm) -> PTerm
     mkRecType [] = PType fc
     mkRecType ((n, c, p, t) :: ts) = PPi fc c p (Just n) t (mkRecType ts)
-getDecl AsType d@(PFixity _ _ _ _ _) = Just d
+getDecl AsType d@(PFixity _ _ _ _ _ _) = Just d
 getDecl AsType d@(PDirective _ _) = Just d
 getDecl AsType d = Nothing
 
@@ -37,7 +37,7 @@ getDecl AsDef (PClaim _ _ _ _ _) = Nothing
 getDecl AsDef d@(PData _ _ _ _ (MkPLater _ _ _)) = Just d
 getDecl AsDef (PInterface _ _ _ _ _ _ _ _ _) = Nothing
 getDecl AsDef d@(PRecord _ _ _ _ (MkPRecordLater _ _)) = Just d
-getDecl AsDef (PFixity _ _ _ _ _) = Nothing
+getDecl AsDef (PFixity _ _ _ _ _ _) = Nothing
 getDecl AsDef (PDirective _ _) = Nothing
 getDecl AsDef d = Just d
 

src/Idris/Doc/Keywords.idr

@@ -458,6 +458,55 @@ namespaceblock = vcat $
     You can use `export` or `public export` to control whether a function
     declared in a namespace is available outside of it.
     """]
+autobindDoc : Doc IdrisDocAnn
+autobindDoc = """
+  Autobind
+
+    `autobind` is a modifier for operator precedence and fixity declaration.
+    It tells the parser that this operator behaves like a binding operator,
+    allowing you to give a name to the left-hand-side of the operator and
+    use it on the right-hand-side.
+
+    `autobind` differs from `typebind` in the syntax it allows and the way
+    it desugars. Delcaring an operator as `autobind infixr 0 =|>` allows
+    you to use it with the syntax `(x := e) =|> f x`, `(x : t := e) =|> f x`.
+
+
+    You will need to use `autobind` instead of `typebind` whenever the
+    type of the lambda of the function called by the operator has a type
+    that is not equal to the argument given on the left side of the operator.
+
+    `autobind` only applies to `infixr` operators and cannot be used as
+    operator sections.
+
+    `autobind` operators are desugared as a lambda:
+    `(x := expr) =|> fn x` -> `(expr =|> (\x : ? => fn x))`
+    `(x : ty := expr) =|> fn x` -> `(expr =|> (\x : ty => fn x))`
+  """
+typebindDoc : Doc IdrisDocAnn
+typebindDoc = """
+  Typebind
+
+    `typebind` is a modifier for operator precedence and fixity declaration.
+    It tells the parser that this operator behaves like a binding operator,
+    allowing you to give a name to the left-hand-side of the operator and
+    use it on the right-hand-side.
+
+    A typical example of a typebind operator is `(**)` the type constructor
+    for dependent pairs. It is used like this: `(x : Nat) ** Vect x String`
+
+    If you declare a new operator to be typebind you can use it the same
+    way.
+
+    Start by defining `typebind infixr 0 =@`, and then you can use it
+    like so: `(n : Nat) =@ f n`
+
+    `typebind` only applies to `infixr` operators and cannot be used as
+    operator sections.
+
+    `typebind` operators are desugared as a lambda:
+    `(x : ty) =@ fn x` -> `ty =@ (\x : ty =@ fn x)`
+  """
 
 rewriteeq : Doc IdrisDocAnn
 rewriteeq = vcat $
@@ -487,8 +536,7 @@ withabstraction = vcat $
     If we additionally need to remember that the link between the patterns and
     the intermediate computation we can use the `proof` keyword to retain an
     equality proof.
-    """, "",
+
-    """
     In the following example we want to implement a `filter` function that not
     only returns values that satisfy the input predicate but also proofs that
     they do. The `with (p x)` construct introduces a value of type `Bool`
@@ -564,6 +612,8 @@ keywordsDoc =
   :: "else" ::= ifthenelse
   :: "forall" ::= forallquantifier
   :: "rewrite" ::= rewriteeq
+  :: "typebind" ::= autobindDoc
+  :: "autobind" ::= autobindDoc
   :: "using" ::= ""
   :: "interface" ::= interfacemechanism
   :: "implementation" ::= interfacemechanism

src/Idris/Error.idr

@@ -110,6 +110,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
   TTCError x1 == TTCError x2 = x1 == x2
   FileErr x1 y1 == FileErr x2 y2 = x1 == x2 && y1 == y2
   CantFindPackage x1 == CantFindPackage x2 = x1 == x2
@@ -619,6 +620,89 @@ 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)
+    = pure $ pretty0 header <+> line <+> !(ploc fc)
+       <+> line
+       <+> "Possible solutions:" <+> line
+       <+> indent 1 (vsep (map (\s => "-" <++> pretty0 s) solutions))
+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
+       <++> "operator."
+       <+> line <+> !(ploc fc)
+       <+> "Explanation: regular, typebind and autobind operators all use a slightly different"
+       <++> "syntax, typebind looks like this: '(name : type)" <++> pretty0 opName
+       <++> "expr', autobind looks like this: '(name := expr)" <++> pretty0 opName
+       <++> "expr'."
+       <+> line <+> line
+       <+> "Possible solutions:" <+> line
+       <+> indent 1 (vsep (map ("-" <++>)
+           (expressionDiagnositc ++ [fixityDiagnostic, moduleDiagnostic] ++ spellingCandidates)))
+    where
+      spellingCandidates : List (Doc IdrisAnn)
+      spellingCandidates = case candidates of
+                              [] => []
+                              [x] => ["Did you mean" <++> enclose "'" "'" (pretty0 x) <++> "?"]
+                              xs => ["Did you mean either of:" <++> hcat (punctuate ", "
+                                       (map (enclose "'" "'" . pretty0) xs)) <++> "?"]
+
+
+      moduleDiagnostic : Doc IdrisAnn
+      moduleDiagnostic = case expected of
+                              Backticked => "Import a module that exports a suitable fixity."
+                              (DeclaredFixity a) => "Hide or remove the fixity at" <++> byShow a.fc
+                                     <++> "and import a module that exports a compatible fixity."
+      infixOpName : Doc IdrisAnn
+      infixOpName = case expected of
+                         Backticked => enclose "`" "`" (byShow opName)
+                         _ => byShow opName
+
+      displayFixityInfo : FixityInfo -> BindingModifier -> Doc IdrisAnn
+      displayFixityInfo (MkFixityInfo fc1 vis _ fix precedence) NotBinding
+        = byShow vis <++> byShow fix <++> byShow precedence <++> pretty0 opName
+      displayFixityInfo (MkFixityInfo _ vis _ fix precedence) usedBinder
+        = byShow vis <++> byShow usedBinder <++> byShow fix <++> byShow precedence <++> pretty0 opName
+
+      printE : ? -> Doc IdrisAnn
+      printE x = reAnnotate (const Code) (p x)
+
+      expressionDiagnositc : List (Doc IdrisAnn)
+      expressionDiagnositc = case expected of
+          Backticked => []
+          (DeclaredFixity e) => let sentence = "Write the expression using" <++> byShow e.bindingInfo <++> "syntax:"
+                   in pure $ sentence <++> enclose "'" "'" (case e.bindingInfo of
+                           NotBinding =>
+                              printE actual.getLhs <++> infixOpName <++> printE rhs
+                           Autobind =>
+                              parens (maybe "_" printE actual.getBoundPat <++> ":="
+                                      <++> printE actual.getLhs)
+                              <++> infixOpName <++> printE rhs
+                           Typebind =>
+                              parens (maybe "_" printE actual.getBoundPat <++> ":"
+                                      <++> printE actual.getLhs)
+                              <++> infixOpName <++> printE rhs
+                           ) <+> dot
+
+
+      fixityDiagnostic : Doc IdrisAnn
+      fixityDiagnostic = case expected of
+          Backticked => "Define a new fixity:" <++> "infixr 0" <++> infixOpName
+          (DeclaredFixity fix) =>
+            "Change the fixity defined at" <++> pretty0 fix.fc <++> "to"
+            <++> enclose "'" "'" (displayFixityInfo fix actual.getBinder)
+            <+> dot
+
+      printBindingModifier : BindingModifier -> Doc IdrisAnn
+      printBindingModifier NotBinding = "a regular"
+      printBindingModifier Typebind = "a type-binding (typebind)"
+      printBindingModifier Autobind = "an automatically-binding (autobind)"
+
+      printBindingInfo : BacktickOrOperatorFixity -> Doc IdrisAnn
+      printBindingInfo Backticked = "a regular"
+      printBindingInfo (DeclaredFixity x) = printBindingModifier x.bindingInfo
+
+
 perrorRaw (TTCError msg)
     = pure $ errorDesc (reflow "Error in TTC file" <+> colon <++> byShow msg)
         <++> parens "the most likely case is that the ./build directory in your current project contains files from a previous build of idris2 or the idris2 executable is from a different build than the installed .ttc files"

src/Idris/Parser.idr

@@ -105,14 +105,14 @@ pnoeq = { eqOK := False }
 
 export
 pdef : ParseOpts
-pdef = MkParseOpts True True
+pdef = MkParseOpts {eqOK = True, withOK = True}
 
 pnowith : ParseOpts
-pnowith = MkParseOpts True False
+pnowith = MkParseOpts {eqOK = True, withOK = False}
 
 export
 plhs : ParseOpts
-plhs = MkParseOpts False False
+plhs = MkParseOpts {eqOK = False, withOK = False}
 
 %hide Prelude.(>>)
 %hide Prelude.(>>=)
@@ -325,15 +325,51 @@ mutual
         decoratedSymbol fname "]"
         pure (map (\ n => (boundToFC fname n, n.val)) $ forget ns)
 
-  opExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
+  -- The different kinds of operator bindings `x : ty` for typebind
-  opExpr q fname indents
+  -- x := e and x : ty := e for autobind
+  opBinderTypes : OriginDesc -> IndentInfo -> WithBounds PTerm -> Rule (OperatorLHSInfo PTerm)
+  opBinderTypes fname indents boundName =
+           do decoratedSymbol fname ":"
+              ty <- typeExpr pdef fname indents
+              decoratedSymbol fname ":="
+              exp <- expr pdef fname indents
+              pure (BindExplicitType boundName.val ty exp)
+       <|> do decoratedSymbol fname ":="
+              exp <- expr pdef fname indents
+              pure (BindExpr boundName.val exp)
+       <|> do decoratedSymbol fname ":"
+              ty <- typeExpr pdef fname indents
+              pure (BindType boundName.val ty)
+
+  opBinder : OriginDesc -> IndentInfo -> Rule (OperatorLHSInfo PTerm)
+  opBinder fname indents
+      = do boundName <- bounds (expr plhs fname indents)
+           opBinderTypes fname indents boundName
+
+  autobindOp : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
+  autobindOp q fname indents
+      = do binder <- bounds $ parens fname (opBinder fname indents)
+           continue indents
+           op <- bounds iOperator
+           commit
+           e <- bounds (expr q fname indents)
+           pure (POp (boundToFC fname $ mergeBounds binder e)
+                     (boundToFC fname op)
+                     binder.val
+                     op.val
+                     e.val)
+
+  opExprBase : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
+  opExprBase q fname indents
       = do l <- bounds (appExpr q fname indents)
            (if eqOK q
-               then do r <- bounds (continue indents *> decoratedSymbol fname "=" *> opExpr q fname indents)
+               then do r <- bounds (continue indents
+                                *> decoratedSymbol fname "="
+                                *> opExprBase q fname indents)
                        pure $
                          let fc = boundToFC fname (mergeBounds l r)
                              opFC = virtualiseFC fc -- already been highlighted: we don't care
-                         in POp fc opFC (UN $ Basic "=") l.val r.val
+                         in POp fc opFC (NoBinder l.val) (UN $ Basic "=") r.val
                else fail "= not allowed")
              <|>
              (do b <- bounds $ do
@@ -346,9 +382,13 @@ mutual
                  (op, r) <- pure b.val
                  let fc = boundToFC fname (mergeBounds l b)
                  let opFC = boundToFC fname op
-                 pure (POp fc opFC op.val l.val r))
+                 pure (POp fc opFC (NoBinder l.val) op.val r))
                <|> pure l.val
 
+  opExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
+  opExpr q fname indents = autobindOp q fname indents
+                       <|> opExprBase q fname indents
+
   dpairType : OriginDesc -> WithBounds t -> IndentInfo -> Rule PTerm
   dpairType fname start indents
       = do loc <- bounds (do x <- UN . Basic <$> decoratedSimpleBinderName fname
@@ -654,8 +694,11 @@ mutual
       binderName = Basic <$> unqualifiedName
                <|> symbol "_" $> Underscore
 
+  PiBindList : Type
+  PiBindList = List (RigCount, WithBounds (Maybe Name), PTerm)
+
   pibindList : OriginDesc -> IndentInfo ->
-               Rule (List (RigCount, WithBounds (Maybe Name), PTerm))
+               Rule PiBindList
   pibindList fname indents
     = do params <- pibindListName fname indents
          pure $ map (\(rig, n, ty) => (rig, map Just n, ty)) params
@@ -981,6 +1024,7 @@ mutual
     <|> defaultImplicitPi fname indents
     <|> forall_ fname indents
     <|> implicitPi fname indents
+    <|> autobindOp pdef fname indents
     <|> explicitPi fname indents
     <|> lam fname indents
 
@@ -1825,16 +1869,23 @@ definition fname indents
     = do nd <- bounds (clause 0 Nothing fname indents)
          pure (PDef (boundToFC fname nd) [nd.val])
 
+operatorBindingKeyword : OriginDesc -> EmptyRule BindingModifier
+operatorBindingKeyword fname
+  =   (decoratedKeyword fname "autobind" >> pure Autobind)
+  <|> (decoratedKeyword fname "typebind" >> pure Typebind)
+  <|> pure NotBinding
+
 fixDecl : OriginDesc -> IndentInfo -> Rule (List PDecl)
 fixDecl fname indents
     = do vis <- exportVisibility fname
+         binding <- operatorBindingKeyword fname
          b <- bounds (do fixity <- decorate fname Keyword $ fix
                          commit
                          prec <- decorate fname Keyword $ intLit
                          ops <- sepBy1 (decoratedSymbol fname ",") iOperator
                          pure (fixity, prec, ops))
          (fixity, prec, ops) <- pure b.val
-         pure (map (PFixity (boundToFC fname b) vis fixity (fromInteger prec)) (forget ops))
+         pure (map (PFixity (boundToFC fname b) vis binding fixity (fromInteger prec)) (forget ops))
 
 directiveDecl : OriginDesc -> IndentInfo -> Rule PDecl
 directiveDecl fname indents

src/Idris/Pretty.idr

@@ -332,7 +332,19 @@ mutual
     prettyPrec d (PDotted _ p) = dot <+> prettyPrec d p
     prettyPrec d (PImplicit _) = "_"
     prettyPrec d (PInfer _) = annotate Hole $ "?"
-    prettyPrec d (POp _ _ op x y) =
+    prettyPrec d (POp _ _ (BindType nm left) op right) =
+        group $ parens (prettyPrec d nm <++> ":" <++> pretty left)
+           <++> prettyOp op
+           <++> pretty right
+    prettyPrec d (POp _ _ (BindExpr nm left) op right) =
+        group $ parens (prettyPrec d nm <++> ":=" <++> pretty left)
+           <++> prettyOp op
+           <++> pretty right
+    prettyPrec d (POp _ _ (BindExplicitType nm ty left) op right) =
+        group $ parens (prettyPrec d nm <++> ":" <++> pretty ty <++> ":=" <++> pretty left)
+           <++> prettyOp op
+           <++> pretty right
+    prettyPrec d (POp _ _ (NoBinder x) op y) =
       parenthesise (d >= App) $
         group $ pretty x
            <++> prettyOp op

src/Idris/Resugar.idr

@@ -46,7 +46,7 @@ mkOp tm@(PApp fc (PApp _ (PRef opFC kn) x) y)
        -- to know if the name is an operator or not, it's enough to check
        -- that the fixity context contains the name `(++)`
        let rootName = UN (Basic (nameRoot raw))
-       let asOp = POp fc opFC kn (unbracketApp x) (unbracketApp y)
+       let asOp = POp fc opFC (NoBinder (unbracketApp x)) kn (unbracketApp y)
        if not (null (lookupName rootName (infixes syn)))
          then pure asOp
          else case dropNS raw of
@@ -590,8 +590,8 @@ cleanPTerm ptm
     cleanNode : IPTerm -> Core IPTerm
     cleanNode (PRef fc nm)    =
       PRef fc <$> cleanKindedName nm
-    cleanNode (POp fc opFC op x y) =
+    cleanNode (POp fc opFC abi op y) =
-      (\ op => POp fc opFC op x y) <$> cleanKindedName op
+      (\ op => POp fc opFC abi op y) <$> cleanKindedName op
     cleanNode (PPrefixOp fc opFC op x) =
       (\ op => PPrefixOp fc opFC op x) <$> cleanKindedName op
     cleanNode (PSectionL fc opFC op x) =

src/Idris/Syntax.idr

@@ -29,44 +29,6 @@ import Parser.Lexer.Source
 
 %default covering
 
-public export
-data Fixity = InfixL | InfixR | Infix | Prefix
-
-export
-Show Fixity where
-  show InfixL = "infixl"
-  show InfixR = "infixr"
-  show Infix  = "infix"
-  show Prefix = "prefix"
-
-export
-Eq Fixity where
-  InfixL == InfixL = True
-  InfixR == InfixR = True
-  Infix == Infix = True
-  Prefix == Prefix = True
-  _ == _ = False
-
--- A record to hold all the information about a fixity
-public export
-record FixityInfo where
-  constructor MkFixityInfo
-  fc : FC
-  vis : Visibility
-  fix : Fixity
-  precedence : Nat
-
-export
-Show FixityInfo where
-  show fx = "fc: \{show fx.fc}, visibility: \{show fx.vis}, fixity: \{show fx.fix}, precedence: \{show fx.precedence}"
-
-export
-Eq FixityInfo where
-  x == y = x.fc == y.fc
-        && x.vis == y.vis
-        && x.fix == y.fix
-        && x.precedence == y.precedence
-
 public export
 OpStr' : Type -> Type
 OpStr' nm = nm
@@ -136,7 +98,9 @@ mutual
 
        -- Operators
 
-       POp : (full, opFC : FC) -> OpStr' nm -> PTerm' nm -> PTerm' nm -> PTerm' nm
+       POp : (full, opFC : FC) ->
+             (lhsInfo : OperatorLHSInfo (PTerm' nm)) ->
+             OpStr' nm -> (rhs : PTerm' nm) -> PTerm' nm
        PPrefixOp : (full, opFC : FC) -> OpStr' nm -> PTerm' nm -> PTerm' nm
        PSectionL : (full, opFC : FC) -> OpStr' nm -> PTerm' nm -> PTerm' nm
        PSectionR : (full, opFC : FC) -> PTerm' nm -> OpStr' nm -> PTerm' nm
@@ -470,7 +434,7 @@ mutual
        PFail : FC -> Maybe String -> List (PDecl' nm) -> PDecl' nm
 
        PMutual : FC -> List (PDecl' nm) -> PDecl' nm
-       PFixity : FC -> Visibility -> Fixity -> Nat -> OpStr -> PDecl' nm
+       PFixity : FC -> Visibility -> BindingModifier -> Fixity -> Nat -> OpStr -> PDecl' nm
        PNamespace : FC -> Namespace -> List (PDecl' nm) -> PDecl' nm
        PTransform : FC -> String -> PTerm' nm -> PTerm' nm -> PDecl' nm
        PRunElabDecl : FC -> PTerm' nm -> PDecl' nm
@@ -489,7 +453,7 @@ mutual
   getPDeclLoc (PRecord fc _ _ _ _) = fc
   getPDeclLoc (PMutual fc _) = fc
   getPDeclLoc (PFail fc _ _) = fc
-  getPDeclLoc (PFixity fc _ _ _ _) = fc
+  getPDeclLoc (PFixity fc _ _ _ _ _) = fc
   getPDeclLoc (PNamespace fc _ _) = fc
   getPDeclLoc (PTransform fc _ _ _) = fc
   getPDeclLoc (PRunElabDecl fc _) = fc
@@ -806,7 +770,14 @@ parameters {0 nm : Type} (toName : nm -> Name)
   showPTermPrec d (PDotted _ p) = "." ++ showPTermPrec d p
   showPTermPrec _ (PImplicit _) = "_"
   showPTermPrec _ (PInfer _) = "?"
-  showPTermPrec d (POp _ _ op x y) = showPTermPrec d x ++ " " ++ showOpPrec d op ++ " " ++ showPTermPrec d y
+  showPTermPrec d (POp _ _ (NoBinder left) op right)
+        = showPTermPrec d left ++ " " ++ showOpPrec d op ++ " " ++ showPTermPrec d right
+  showPTermPrec d (POp _ _ (BindType nm left) op right)
+        = "(" ++ showPTermPrec d nm ++ " : " ++ showPTermPrec d left ++ " " ++ showOpPrec d op ++ " " ++ showPTermPrec d right ++ ")"
+  showPTermPrec d (POp _ _ (BindExpr nm left) op right)
+        = "(" ++ showPTermPrec d nm ++ " := " ++ showPTermPrec d left ++ " " ++ showOpPrec d op ++ " " ++ showPTermPrec d right ++ ")"
+  showPTermPrec d (POp _ _ (BindExplicitType nm ty left) op right)
+        = "(" ++ showPTermPrec d nm ++ " : " ++ showPTermPrec d ty ++ ":=" ++ showPTermPrec d left ++ " " ++ showOpPrec d op ++ " " ++ showPTermPrec d right ++ ")"
   showPTermPrec d (PPrefixOp _ _ op x) = showOpPrec d op ++ showPTermPrec d x
   showPTermPrec d (PSectionL _ _ op x) = "(" ++ showOpPrec d op ++ " " ++ showPTermPrec d x ++ ")"
   showPTermPrec d (PSectionR _ _ x op) = "(" ++ showPTermPrec d x ++ " " ++ showOpPrec d op ++ ")"
@@ -999,9 +970,9 @@ initSyntax
 
     initFixities : ANameMap FixityInfo
     initFixities = fromList
-      [ (UN $ Basic "-", MkFixityInfo EmptyFC Export Prefix 10)
+      [ (UN $ Basic "-", MkFixityInfo EmptyFC Export NotBinding Prefix 10)
-      , (UN $ Basic "negate", MkFixityInfo EmptyFC Export Prefix 10) -- for documentation purposes
+      , (UN $ Basic "negate", MkFixityInfo EmptyFC Export NotBinding Prefix 10) -- for documentation purposes
-      , (UN $ Basic "=", MkFixityInfo EmptyFC Export Infix 0)
+      , (UN $ Basic "=", MkFixityInfo EmptyFC Export NotBinding Infix 0)
       ]
 
     initDocStrings : ANameMap String
@@ -1034,6 +1005,13 @@ removeFixity :
     {auto s : Ref Syn SyntaxInfo} -> Fixity -> Name -> Core ()
 removeFixity _ key = update Syn ({fixities $= removeExact key })
 
+||| Return all fixity declarations for an operator name
+export
+getFixityInfo : {auto s : Ref Syn SyntaxInfo} -> String -> Core (List (Name, FixityInfo))
+getFixityInfo nm = do
+  syn <- get Syn
+  pure $ lookupName (UN $ Basic nm) (fixities syn)
+
 export
 covering
 Show PTypeDecl where

src/Idris/Syntax/TTC.idr

@@ -81,19 +81,33 @@ TTC Import where
          nameAs <- fromBuf b
          pure (MkImport loc reexport path nameAs)
 
+export
+TTC BindingModifier where
+  toBuf b NotBinding = tag 0
+  toBuf b Typebind = tag 1
+  toBuf b Autobind = tag 2
+  fromBuf b
+      = case !getTag of
+             0 => pure NotBinding
+             1 => pure Typebind
+             2 => pure Autobind
+             _ => corrupt "binding"
+
 export
 TTC FixityInfo where
   toBuf b fx
       = do toBuf b fx.fc
            toBuf b fx.vis
+           toBuf b fx.bindingInfo
            toBuf b fx.fix
            toBuf b fx.precedence
   fromBuf b
       = do fc <- fromBuf b
            vis <- fromBuf b
+           binding <- fromBuf b
            fix <- fromBuf b
            prec <- fromBuf b
-           pure $ MkFixityInfo fc vis fix prec
+           pure $ MkFixityInfo fc vis binding fix prec
 
 
 export

src/Idris/Syntax/Traversals.idr

@@ -99,9 +99,29 @@ mapPTermM f = goPTerm where
       >>= f
     goPTerm t@(PImplicit _) = f t
     goPTerm t@(PInfer _) = f t
-    goPTerm (POp fc opFC x y z) =
+    goPTerm (POp fc opFC (NoBinder left) op right) =
-      POp fc opFC x <$> goPTerm y
+      POp fc opFC
-                    <*> goPTerm z
+          <$> (NoBinder <$> goPTerm left)
+          <*> pure op
+          <*> goPTerm right
+      >>= f
+    goPTerm (POp fc opFC (BindType nm left) op right) =
+      POp fc opFC
+          <$> (BindType <$> goPTerm nm <*> goPTerm left)
+          <*> pure op
+          <*> goPTerm right
+      >>= f
+    goPTerm (POp fc opFC (BindExpr nm left) op right) =
+      POp fc opFC
+          <$> (BindExpr nm <$> goPTerm left)
+          <*> pure op
+          <*> goPTerm right
+      >>= f
+    goPTerm (POp fc opFC (BindExplicitType nm ty left) op right) =
+      POp fc opFC
+          <$> (BindExplicitType <$> goPTerm nm <*> goPTerm ty <*> goPTerm left)
+          <*> pure op
+          <*> goPTerm right
       >>= f
     goPTerm (PPrefixOp fc opFC x y) =
       PPrefixOp fc opFC x <$> goPTerm y
@@ -265,7 +285,7 @@ mapPTermM f = goPTerm where
       pure $ PRecord fc doc v tot (MkPRecordLater n !(go4TupledPTerms nts))
     goPDecl (PFail fc msg ps) = PFail fc msg <$> goPDecls ps
     goPDecl (PMutual fc ps) = PMutual fc <$> goPDecls ps
-    goPDecl p@(PFixity _ _ _ _ _) = pure p
+    goPDecl p@(PFixity _ _ _ _ _ _) = pure p
     goPDecl (PNamespace fc strs ps) = PNamespace fc strs <$> goPDecls ps
     goPDecl (PTransform fc n a b) = PTransform fc n <$> goPTerm a <*> goPTerm b
     goPDecl (PRunElabDecl fc a) = PRunElabDecl fc <$> goPTerm a
@@ -434,8 +454,8 @@ mapPTerm f = goPTerm where
       = f $ PDotted fc $ goPTerm x
     goPTerm t@(PImplicit _) = f t
     goPTerm t@(PInfer _) = f t
-    goPTerm (POp fc opFC x y z)
+    goPTerm (POp fc opFC autoBindInfo opName z)
-      = f $ POp fc opFC x (goPTerm y) (goPTerm z)
+      = f $ POp fc opFC (map f autoBindInfo) opName (goPTerm z)
     goPTerm (PPrefixOp fc opFC x y)
       = f $ PPrefixOp fc opFC x $ goPTerm y
     goPTerm (PSectionL fc opFC x y)
@@ -533,7 +553,7 @@ mapPTerm f = goPTerm where
       = PRecord fc doc v tot (MkPRecordLater n (go4TupledPTerms nts))
     goPDecl (PFail fc msg ps) = PFail fc msg $ goPDecl <$> ps
     goPDecl (PMutual fc ps) = PMutual fc $ goPDecl <$> ps
-    goPDecl p@(PFixity _ _ _ _ _) = p
+    goPDecl p@(PFixity _ _ _ _ _ _) = p
     goPDecl (PNamespace fc strs ps) = PNamespace fc strs $ goPDecl <$> ps
     goPDecl (PTransform fc n a b) = PTransform fc n (goPTerm a) (goPTerm b)
     goPDecl (PRunElabDecl fc a) = PRunElabDecl fc $ goPTerm a
@@ -618,7 +638,7 @@ substFC fc = mapPTerm $ \case
   PDotted _ x => PDotted fc x
   PImplicit _ => PImplicit fc
   PInfer _ => PInfer fc
-  POp _ _ x y z => POp fc fc x y z
+  POp _ _ ab nm r => POp fc fc ab nm r
   PPrefixOp _ _ x y => PPrefixOp fc fc x y
   PSectionL _ _ x y => PSectionL fc fc x y
   PSectionR _ _ x y => PSectionR fc fc x y

src/Idris/Syntax/Views.idr

@@ -26,7 +26,8 @@ getFnArgs embed fts = go fts [] where
   go (PAutoApp fc f t) = go f . (Auto fc t ::)
   go (PNamedApp fc f n t) = go f . (Named fc n t ::)
   go (PBracketed fc f) = go f
-  go (POp fc opFC op l r) = (PRef opFC op,) . (Explicit fc l ::) . (Explicit fc r ::)
+  -- we don't care about the binder info here
+  go (POp fc opFC leftSide op r) = (PRef opFC op,) . (Explicit fc leftSide.getLhs ::) . (Explicit fc r ::)
   go (PEq fc l r) = (PRef fc $ embed eqName,) . (Explicit fc l ::) . (Explicit fc r ::)
   -- ambiguous, picking the type constructor here
   go (PPair fc l r) = (PRef fc $ embed pairname,) . (Explicit fc l ::) . (Explicit fc r ::)

src/Libraries/Utils/Shunting.idr

@@ -22,10 +22,9 @@ data OpPrec
 -- Tokens are either operators or already parsed expressions in some
 -- higher level language
 public export
-data Tok op a
+data Tok : (op, a : Type) ->  Type where
-  = ||| The second FC is for the operator alone
+    Op : (expressionLoc : FC) -> (operatorLoc : FC) -> (operatorInfo : op) -> OpPrec -> Tok op a
-    Op FC FC op OpPrec
+    Expr : a -> Tok op a
-  | Expr a
 
 -- The result of shunting is a parse tree with the precedences made explicit
 -- in the tree.
@@ -41,6 +40,12 @@ data Tree op a = Infix FC FC op (Tree op a) (Tree op a)
                | Pre FC FC op (Tree op a)
                | Leaf a
 
+public export
+Bifunctor Tree where
+  bimap f g (Infix fc fc1 x y z) = Infix fc fc1 (f x) (bimap f g y) (bimap f g z)
+  bimap f g (Pre fc fc1 x y) = Pre fc fc1 (f x) (bimap f g y)
+  bimap f g (Leaf x) = Leaf (g x)
+
 export
 (Show op, Show a) => Show (Tree op a) where
   show (Infix _ _ op l r) = "(" ++ show op ++ " " ++ show l ++ " " ++ show r ++ ")"
@@ -85,25 +90,27 @@ isLAssoc : OpPrec -> Bool
 isLAssoc (AssocL _) = True
 isLAssoc _ = False
 
--- Return whether the first operator should be applied before the second,
+-- Return whether the first operator should be applied before the second.
--- assuming
+-- Interpolation to show the operator naked, show to print the operator with its location
-higher : Show op => FC -> op -> OpPrec -> op -> OpPrec -> Core Bool
+higher : Interpolation op => (showLoc : Show op) => FC -> op -> OpPrec -> op -> OpPrec -> Core Bool
 higher loc opx op opy (Prefix p) = pure False
 higher loc opx (NonAssoc x) opy oy
     = if x == getPrec oy
-         then throw (GenericMsg loc ("Operator '" ++ show opx ++
+         then throw (GenericMsgSol loc ( "Operator \{opx} is non-associative")
-                                     "' is non-associative"))
+                                       [ "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 (GenericMsg loc ("Operator '" ++ show opy ++
+         then throw (GenericMsgSol loc ( "Operator \{opy} is non-associative")
-                                     "' is non-associative"))
+                                       [ "Add brackets around every use of \{opy}"
+                                       , "Change the fixity of \{show opy} to `infixl` or `infixr`"])
          else pure (getPrec ox > y)
 higher loc opl l opr r
     = pure $ (getPrec l > getPrec r) ||
              ((getPrec l == getPrec r) && isLAssoc l)
 
-processStack : Show op => {auto o : Ref Out (List (Tree op a))} ->
+processStack : Interpolation op => (showLoc : Show op) => {auto o : Ref Out (List (Tree op a))} ->
                List (FC, FC, op, OpPrec) -> op -> OpPrec ->
                Core (List (FC, FC, op, OpPrec))
 processStack [] op prec = pure []
@@ -113,7 +120,7 @@ processStack (x@(loc, opFC, opx, sprec) :: xs) opy prec
                  processStack xs opy prec
          else pure (x :: xs)
 
-shunt : Show op => {auto o : Ref Out (List (Tree op a))} ->
+shunt : Interpolation op => (showLoc : Show op) => {auto o : Ref Out (List (Tree op a))} ->
         (opstk : List (FC, FC, op, OpPrec)) ->
         List (Tok op a) -> Core (Tree op a)
 shunt stk (Expr x :: rest)
@@ -132,7 +139,7 @@ shunt stk []
     mkOp (loc, opFC, op, prec) = Op loc opFC op prec
 
 export
-parseOps : Show op => List (Tok op a) -> Core (Tree op a)
+parseOps : Interpolation op => (showLoc : Show op) => List (Tok op a) -> Core (Tree op a)
 parseOps toks
     = do o <- newRef {t = List (Tree op a)} Out []
          shunt [] toks

src/Parser/Lexer/Source.idr

@@ -245,7 +245,7 @@ keywords : List String
 keywords = ["data", "module", "where", "let", "in", "do", "record",
             "auto", "default", "implicit", "failing", "mutual", "namespace",
             "parameters", "with", "proof", "impossible", "case", "of",
-            "if", "then", "else", "forall", "rewrite",
+            "if", "then", "else", "forall", "rewrite", "typebind", "autobind",
             "using", "interface", "implementation", "open", "import",
             "public", "export", "private"] ++
             fixityKeywords ++

tests/Main.idr

@@ -112,6 +112,9 @@ idrisTestsReflection = testsInDir "idris2/reflection" "Quotation and Reflection"
 idrisTestsWith : IO TestPool
 idrisTestsWith = testsInDir "idris2/with" "With abstraction"
 
+idrisTestsOperators : IO TestPool
+idrisTestsOperators = testsInDir "idris2/operators" "Operator and fixities"
+
 idrisTestsIPKG : IO TestPool
 idrisTestsIPKG = testsInDir "idris2/pkg" "Package and .ipkg files"
 
@@ -216,6 +219,7 @@ main = runner $
   , !idrisTestsSchemeEval
   , !idrisTestsReflection
   , !idrisTestsWith
+  , !idrisTestsOperators
   , !idrisTestsDebug
   , !idrisTestsIPKG
   , testPaths "idris2/misc" idrisTests

tests/idris2/interactive/interactive028/expected

@@ -4,7 +4,7 @@ Main> Couldn't parse any alternatives:
 (Interactive):1:4--1:5
  1 | :t (3 : Nat)
         ^
-... (54 others)
+... (56 others)
 Main> Expected string begin.
 
 (Interactive):1:5--1:7

tests/idris2/operators/operators001/Test.idr

@@ -0,0 +1,80 @@
+
+module Test
+
+import Data.Vect
+
+typebind infixr 0 =@
+infixr 0 -@
+
+-- typebind infixr 1 =@@
+
+0 (=@) : (a : Type) -> (a -> Type) -> Type
+(=@) a f = (1 x : a) -> f x
+
+0 (=@@) : (a : Type) -> (a -> Type) -> Type
+(=@@) a f = (1 x : a) -> f x
+
+(-@) : (a, b : Type) -> Type
+(-@) a b = (1 _ : a) -> b
+
+data S : {ty : Type} -> (x : ty) -> Type where
+  MkS : (x : ty) =@ S x
+  Mk2 : (x : ty) =@ (y : ty) =@ S (x, y)
+  Mk3 : (x : ty) =@ ty -@ S x
+  Mk4 : ty -@ (x : ty) =@ S x
+
+-- map : (x : a) =@@ b -@ (y : List a) =@ List b
+
+map2 : ((x : a) =@ b) -@ (y : List a) =@ List b
+
+map3 : (x : a) =@ b -@ (y : List a) =@ List b
+
+map4 : (x : a) =@ (b -@ (y : List a) =@ List b)
+
+-- this could be possible if we allowed binding operators
+-- with higher precedences
+-- test : Test.map === Test.map2
+-- failing
+--   test2 : Test.map === Test.map3
+
+test3 : Test.map3 === Test.map4
+
+typebind infixr 0 *>
+
+-- (*>) : (ty : Type) -> (ty -> Type) -> Type
+-- (*>) = DPair
+--
+-- testCompose : (x : Nat) *> (y : Nat) *> Vect (n + m) String
+-- testCompose = (1 ** 2 ** ["hello", "world", "!"])
+
+autobind infixr 0 `MyLet`
+
+MyLet : (val) -> (val -> rest) -> rest
+MyLet arg fn = fn arg
+
+program : Nat
+program = (n := 3) `MyLet` 2 + n
+
+program2 : Nat
+program2 = (n : Nat := 3) `MyLet` 2 + n
+
+typebind infixr 0 |>
+
+record Container where
+  constructor (|>)
+  shape : Type
+  position : shape -> Type
+
+typebind infixr 0 @@
+
+record (@@) (x : Type) (y : x -> Type) where
+  constructor PairUp
+  fst : x
+  snd : y fst
+
+compose : Container -> Container -> Container
+compose (a |> a') (b |> b') =
+  (x : (y : a) @@ (a' y -> b)) |>
+       (y : a' x.fst) @@
+            b' (x.snd y)
+

tests/idris2/operators/operators001/expected

@@ -0,0 +1 @@
+1/1: Building Test (Test.idr)

tests/idris2/operators/operators001/run

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

tests/idris2/operators/operators002/Error2.idr

@@ -0,0 +1,12 @@
+
+typebind infixr 0 =@
+
+0 (=@) : (a : Type) -> (a -> Type) -> Type
+(=@) a f = (1 x : a) -> f x
+
+
+data S : {ty : Type} -> (x : ty) -> Type where
+  MkS : (x : ty) =@ S x
+
+wrongId : {0 a : Type} -> a =@ a
+wrongId x = x

tests/idris2/operators/operators002/Errors.idr

@@ -0,0 +1,9 @@
+
+typebind infixr 0 =@
+
+0 (=@) : (a : Type) -> (a -> Type) -> Type
+(=@) a f = (1 x : a) -> f x
+
+data S : {ty : Type} -> (x : ty) -> Type where
+  MkS : (x := ty) =@ S x
+

tests/idris2/operators/operators002/Errors2.idr

@@ -0,0 +1,8 @@
+
+autobind infixr 0 =@
+
+0 (=@) : (a : Type) -> (a -> Type) -> Type
+(=@) a f = (1 x : a) -> f x
+
+wrongId : {0 a : Type} -> a =@ a
+wrongId x = x

tests/idris2/operators/operators002/Errors3.idr

@@ -0,0 +1,8 @@
+
+typebind infixr 0 =@
+
+0 (=@) : (a : Type) -> (a -> Type) -> Type
+(=@) a f = (1 x : a) -> f x
+
+wrongId : {0 a : Type} -> a =@ a
+wrongId x = x

tests/idris2/operators/operators002/Errors4.idr

@@ -0,0 +1,9 @@
+
+infixr 0 =@
+
+0 (=@) : (a : Type) -> (a -> Type) -> Type
+(=@) a f = (1 x : a) -> f x
+
+
+data S : {ty : Type} -> (x : ty) -> Type where
+  MkS : (x : ty) =@ S x

tests/idris2/operators/operators002/Errors5.idr

@@ -0,0 +1,10 @@
+
+
+infixr 0 =@
+
+0 (=@) : (a : Type) -> (a -> Type) -> Type
+(=@) a f = (1 x : a) -> f x
+
+
+data S : {ty : Type} -> (x : ty) -> Type where
+  MkS : (x := ty) =@ S x

tests/idris2/operators/operators002/Test.idr

@@ -0,0 +1,38 @@
+
+
+import Data.Vect
+
+typebind infixr 0 =@
+infixr 0 -@
+
+0 (=@) : (a : Type) -> (a -> Type) -> Type
+(=@) a f = (1 x : a) -> f x
+
+(-@) : (a, b : Type) -> Type
+(-@) a b = (1 _ : a) -> b
+
+data S : {ty : Type} -> (x : ty) -> Type where
+  MkS : (x : ty) =@ S x
+  Mk2 : (x : ty) =@ (y : ty) =@ S (x, y)
+  Mk3 : (x : ty) =@ ty -@ S x
+  Mk4 : ty -@ (x : ty) =@ S x
+  Chain : (x : ty =@ y : ty =@ S (x, y))
+
+typebind infixr 0 *>
+
+-- (*>) : (ty : Type) -> (ty -> Type) -> Type
+-- (*>) = DPair
+--
+-- testCompose : (x : Nat) *> (y : Nat) *> Vect (n + m) String
+-- testCompose = (1 ** 2 ** ["hello", "world", "!"])
+
+autobind infixr 7 `MyLet`
+
+MyLet : (val) -> (val -> rest) -> rest
+MyLet arg fn = fn arg
+
+program : Nat
+program = (n := 3) `MyLet` 2 + n
+
+program2 : Nat
+program2 = (n : Nat := 3) `MyLet` 2 + n

tests/idris2/operators/operators002/expected

@@ -0,0 +1,80 @@
+1/1: Building Errors (Errors.idr)
+Error: Operator =@ is a type-binding (typebind) operator, but is used as an automatically-binding (autobind) operator.
+
+Errors:8:19--8:21
+ 4 | 0 (=@) : (a : Type) -> (a -> Type) -> Type
+ 5 | (=@) a f = (1 x : a) -> f x
+ 6 | 
+ 7 | data S : {ty : Type} -> (x : ty) -> Type where
+ 8 |   MkS : (x := ty) =@ S x
+                       ^^
+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 typebind syntax: '(x : ty) =@ S x'.
+ - Change the fixity defined at Errors:2:10--2:21 to 'export autobind infixr 0 =@'.
+ - Hide or remove the fixity at Errors:2:10--2:21 and import a module that exports a compatible fixity.
+1/1: Building Errors2 (Errors2.idr)
+Error: Operator =@ is an automatically-binding (autobind) operator, but is used as a regular operator.
+
+Errors2:7:29--7:31
+ 3 | 
+ 4 | 0 (=@) : (a : Type) -> (a -> Type) -> Type
+ 5 | (=@) a f = (1 x : a) -> f x
+ 6 | 
+ 7 | wrongId : {0 a : Type} -> a =@ a
+                                 ^^
+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 autobind syntax: '(_ := a) =@ a'.
+ - Change the fixity defined at Errors2:2:10--2:21 to 'export infixr 0 =@'.
+ - Hide or remove the fixity at Errors2:2:10--2:21 and import a module that exports a compatible fixity.
+1/1: Building Errors3 (Errors3.idr)
+Error: Operator =@ is a type-binding (typebind) operator, but is used as a regular operator.
+
+Errors3:7:29--7:31
+ 3 | 
+ 4 | 0 (=@) : (a : Type) -> (a -> Type) -> Type
+ 5 | (=@) a f = (1 x : a) -> f x
+ 6 | 
+ 7 | wrongId : {0 a : Type} -> a =@ a
+                                 ^^
+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 typebind syntax: '(_ : a) =@ a'.
+ - Change the fixity defined at Errors3:2:10--2:21 to 'export infixr 0 =@'.
+ - Hide or remove the fixity at Errors3:2:10--2:21 and import a module that exports a compatible fixity.
+1/1: Building Errors4 (Errors4.idr)
+Error: Operator =@ is a regular operator, but is used as a type-binding (typebind) operator.
+
+Errors4:9:18--9:20
+ 5 | (=@) a f = (1 x : a) -> f x
+ 6 | 
+ 7 | 
+ 8 | data S : {ty : Type} -> (x : ty) -> Type where
+ 9 |   MkS : (x : ty) =@ S x
+                      ^^
+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: 'ty =@ S x'.
+ - Change the fixity defined at Errors4:2:1--2:12 to 'export typebind infixr 0 =@'.
+ - Hide or remove the fixity at Errors4:2:1--2:12 and import a module that exports a compatible fixity.
+1/1: Building Errors5 (Errors5.idr)
+Error: Operator =@ is a regular operator, but is used as an automatically-binding (autobind) operator.
+
+Errors5:10:19--10:21
+ 06 | (=@) a f = (1 x : a) -> f x
+ 07 | 
+ 08 | 
+ 09 | data S : {ty : Type} -> (x : ty) -> Type where
+ 10 |   MkS : (x := ty) =@ S x
+                        ^^
+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: 'ty =@ S x'.
+ - Change the fixity defined at Errors5:3:1--3:12 to 'export autobind infixr 0 =@'.
+ - Hide or remove the fixity at Errors5:3:1--3:12 and import a module that exports a compatible fixity.

tests/idris2/operators/operators002/run

@@ -0,0 +1,8 @@
+. ../../../testutils.sh
+
+check Errors.idr
+check Errors2.idr
+check Errors3.idr
+check Errors4.idr
+check Errors5.idr
+

tests/idris2/operators/operators003/Error1.idr

@@ -0,0 +1,3 @@
+module Error1
+
+typebind infixl 0 =@

tests/idris2/operators/operators003/Error2.idr

@@ -0,0 +1,3 @@
+module Error2
+
+typebind infixr 3 =@

tests/idris2/operators/operators003/Error3.idr

@@ -0,0 +1,3 @@
+module Error3
+
+typebind infixl 3 =@

tests/idris2/operators/operators003/expected

@@ -0,0 +1,36 @@
+1/1: Building Error1 (Error1.idr)
+Error: Invalid fixity, typebind operator must be infixr 0.
+
+Error1:3:10--3:21
+ 1 | module Error1
+ 2 | 
+ 3 | typebind infixl 0 =@
+              ^^^^^^^^^^^
+
+Possible solutions:
+ - Make it `infixr 0`: `typebind infixr 0 =@`
+ - Remove the binding keyword: `infixl 0 =@`
+1/1: Building Error2 (Error2.idr)
+Error: Invalid fixity, typebind operator must be infixr 0.
+
+Error2:3:10--3:21
+ 1 | module Error2
+ 2 | 
+ 3 | typebind infixr 3 =@
+              ^^^^^^^^^^^
+
+Possible solutions:
+ - Make it `infixr 0`: `typebind infixr 0 =@`
+ - Remove the binding keyword: `infixr 3 =@`
+1/1: Building Error3 (Error3.idr)
+Error: Invalid fixity, typebind operator must be infixr 0.
+
+Error3:3:10--3:21
+ 1 | module Error3
+ 2 | 
+ 3 | typebind infixl 3 =@
+              ^^^^^^^^^^^
+
+Possible solutions:
+ - Make it `infixr 0`: `typebind infixr 0 =@`
+ - Remove the binding keyword: `infixl 3 =@`

tests/idris2/operators/operators003/run

@@ -0,0 +1,5 @@
+. ../../../testutils.sh
+
+check Error1.idr
+check Error2.idr
+check Error3.idr

tests/idris2/operators/operators004/Test.idr

@@ -0,0 +1,16 @@
+
+infix 5 -:-
+
+infix 5 :-:
+
+(-:-) : a -> List a -> List a
+(-:-) = (::)
+
+(:-:) : a -> List a -> List a
+(:-:) = (::)
+
+test : List Nat
+test = 4 -:- 3 :-: []
+
+test2 : List Nat
+test2 = 4 :-: 3 -:- []

tests/idris2/operators/operators004/expected

@@ -0,0 +1,27 @@
+1/1: Building Test (Test.idr)
+Error: Operator -:- is non-associative
+
+Test:13:8--13:22
+ 09 | (:-:) : a -> List a -> List a
+ 10 | (:-:) = (::)
+ 11 | 
+ 12 | test : List Nat
+ 13 | test = 4 -:- 3 :-: []
+             ^^^^^^^^^^^^^^
+
+Possible solutions:
+ - Add brackets around every use of -:-
+ - Change the fixity of -:- at Test:2:1--2:12 to `infixl` or `infixr`
+Error: Operator :-: is non-associative
+
+Test:16:9--16:23
+ 12 | test : List Nat
+ 13 | test = 4 -:- 3 :-: []
+ 14 | 
+ 15 | test2 : List Nat
+ 16 | test2 = 4 :-: 3 -:- []
+              ^^^^^^^^^^^^^^
+
+Possible solutions:
+ - Add brackets around every use of :-:
+ - Change the fixity of :-: at Test:4:1--4:12 to `infixl` or `infixr`

tests/idris2/operators/operators004/run

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

tests/idris2/operators/operators005/Test.idr

@@ -0,0 +1,19 @@
+
+import Data.String
+
+typebind infixr 0 :-
+autobind infixr 0 `for`
+
+record Container where
+  constructor (:-)
+  a1 : Type
+  a2 : a1 -> Type
+
+const : Type -> Type -> Container
+const a b = (_ : a) :- b
+
+test : Maybe (List Double)
+test = (_ := ["1", "two", "3"]) `for` Just 3
+
+test2 : Maybe (List Double)
+test2 = (_ : String := ["1", "two", "3"]) `for` Just 3

tests/idris2/operators/operators005/expected

@@ -0,0 +1 @@
+1/1: Building Test (Test.idr)

tests/idris2/operators/operators005/run

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

tests/idris2/operators/operators006/Test.idr

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

tests/idris2/operators/operators006/expected

@@ -0,0 +1 @@
+1/1: Building Test (Test.idr)

tests/idris2/operators/operators006/run

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

tests/idris2/operators/operators007/Test.idr

@@ -0,0 +1,10 @@
+
+import Data.Fin
+
+autobind 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/Test2.idr

@@ -0,0 +1,14 @@
+
+import Data.Fin
+
+autobind infixr 0 >>
+autobind infixr 0 >=
+
+(>>) : Monad m => m a -> (a -> m b) -> m b
+(>>) = (>>=)
+
+(>=) : 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,34 @@
+1/1: Building Test (Test.idr)
+Error: Operator >>= is a regular operator, but is used as an automatically-binding (autobind) operator.
+
+Test:10:28--10:31
+ 06 | (>>) : Monad m => m a -> (a -> m b) -> m b
+ 07 | (>>) = (>>=)
+ 08 | 
+ 09 | both : Maybe (Nat, Nat) -> Maybe Nat
+ 10 | 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 Prelude.Ops:20:1--20:37 to 'export autobind infixl 1 >>='.
+ - Hide or remove the fixity at Prelude.Ops:20:1--20:37 and import a module that exports a compatible fixity.
+ - Did you mean '>>' ?
+1/1: Building Test2 (Test2.idr)
+Error: Operator >>= is a regular operator, but is used as an automatically-binding (autobind) operator.
+
+Test2:14:28--14:31
+ 10 | (>=) : Monad m => m a -> (a -> m b) -> m b
+ 11 | (>=) = (>>=)
+ 12 | 
+ 13 | both : Maybe (Nat, Nat) -> Maybe Nat
+ 14 | 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 Prelude.Ops:20:1--20:37 to 'export autobind infixl 1 >>='.
+ - Hide or remove the fixity at Prelude.Ops:20:1--20:37 and import a module that exports a compatible fixity.
+ - Did you mean either of: '>=', '>>' ?

tests/idris2/operators/operators007/run

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

tests/idris2/operators/operators008/Test.idr

@@ -0,0 +1,13 @@
+module Test
+
+import Test2
+
+%hide Test2.infixr.(@>)
+
+infixl 9 @>
+
+(@>) : a -> b -> (a, b)
+(@>) = MkPair
+
+test : 3 @> 2 @> 1 === (3 @> 2) @> 1
+test = Refl

tests/idris2/operators/operators008/Test2.idr

@@ -0,0 +1,4 @@
+module Test2
+
+export autobind infixr 0 @>
+

tests/idris2/operators/operators008/expected

@@ -0,0 +1,2 @@
+1/2: Building Test2 (Test2.idr)
+2/2: Building Test (Test.idr)

tests/idris2/operators/operators008/run

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