[ new ] Allow fixities to be hidden with %hide

* Change the printing of namespaced operator to show
  parenthesis around operators
* Update warning when conflicting fixities are found
* Do not warn about redundant but compatible fixities

CHANGELOG.md

@@ -14,6 +14,7 @@
   similar to the builtins `believe_me`, `assert_total`, etc.
 * Rudimentary support for defining lazy functions (addressing issue
   [#1066](https://github.com/idris-lang/idris2/issues/1066)).
+* `%hide` directives can now hide conflicting fixities from other modules.
 
 ### REPL changes
 

docs/source/reference/pragmas.rst

@@ -99,3 +99,28 @@ definition.
 
    %name Foo foo,bar
 
+``%hide``
+====================
+
+Hide a definition from imports. This is particularly useful when you are re-definiing functions or types from
+a module but still need to import it.
+
+.. code-block:: idris
+
+   module MyNat
+
+   %hide Prelude.Nat
+   %hide Prelude.S
+   %hide Prelude.Nat
+
+   data Nat = Z | S Nat
+
+You can also hide fixity declarations if you need to redefine your own.
+
+.. code-block:: idris
+
+   module MyNat
+
+   %hide Prelude.Ops.infixl.(+)
+
+   infixr 5 +

src/Compiler/ES/Doc.idr

@@ -2,8 +2,6 @@ module Compiler.ES.Doc
 
 import Data.List
 
-infixr 6 <++>
-
 public export
 data Doc
   = Nil
@@ -48,7 +46,7 @@ isMultiline (Seq x y)  = isMultiline x || isMultiline y
 
 export
 (<++>) : Doc -> Doc -> Doc
-a <++> b = a <+> " " <+> b
+(<++>) a b = a <+> " " <+> b
 
 export
 vcat : List Doc -> Doc

src/Core/Name.idr

@@ -238,7 +238,10 @@ Show UserName where
 export
 Show Name where
   show (NS ns n@(UN (Field _))) = show ns ++ ".(" ++ show n ++ ")"
-  show (NS ns n) = show ns ++ "." ++ show n
+  show (NS ns (UN (Basic n))) = if any isOpChar (unpack n)
+                       then "\{show ns}.(\{n})"
+                       else "\{show ns}.\{n}"
+  show (NS ns n) = "\{show ns}.\{show n}"
   show (UN x) = show x
   show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
   show (PV n d) = "{P:" ++ show n ++ ":" ++ show d ++ "}"

src/Idris/Desugar.idr

@@ -82,31 +82,9 @@ extendSyn newsyn
            , "New (" ++ unwords (map show $ saveMod newsyn) ++ "): "
               ++ show (modDocstrings newsyn)
            ]
-         -- Check there are no conflicting definitions
-         let oldprefix = map (Prefix,) <$> (prefixes syn)
-         let newprefix = map (Prefix,) <$> (prefixes newsyn)
-         let oldinfix  = infixes syn
-         let newinfix  = infixes newsyn
 
-         let check = mapMaybe (\ entry@(k, ((_, v), (_, v'))) => entry <$ guard (k /= "-" && (v /= v')))
+         put Syn ({ infixes $= merge (infixes newsyn),
-                   . StringMap.toList
+                    prefixes $= merge (prefixes newsyn),
-         let inter = concatMap {t = List} {m = List _} check
-                   [ sharedSupport oldprefix newprefix
-                   , sharedSupport oldprefix newinfix
-                   , sharedSupport oldinfix  newprefix
-                   , sharedSupport oldinfix  newinfix
-                   ]
-         unless (null inter) $ recordWarning $ GenericWarn emptyFC $ unlines
-           $ ("Conflicting fixity declarations:" ::)
-           $ flip (concatMap {m = List _}) inter
-           $ \ (k, ((fc1, fix1, prec1), (fc2, fix2, prec2))) => pure $ unwords
-           [ "\{k}:"
-           , "\{show fix1} \{show prec1} (at \{show fc1})", "and"
-           , "\{show fix2} \{show prec2} (at \{show fc2})"
-           ]
-
-         put Syn ({ infixes $= mergeLeft (infixes newsyn),
-                    prefixes $= mergeLeft (prefixes newsyn),
                     ifaces $= merge (ifaces newsyn),
                     modDocstrings $= mergeLeft (modDocstrings newsyn),
                     modDocexports $= mergeLeft (modDocexports newsyn),
@@ -120,34 +98,69 @@ mkPrec InfixR p = AssocR p
 mkPrec Infix p = NonAssoc p
 mkPrec Prefix p = Prefix p
 
+-- 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) ->
+                           FC -> Name -> Core OpPrec
+checkConflictingFixities isPrefix exprFC opn
+  = do syn <- get Syn
+       let op = nameRoot opn
+       let foundFixities : List (Name, FC, Fixity, Nat) = lookupName (UN (Basic op)) (fixities syn)
+       let (pre, inf) = partition (\(_, _, fx, _) => fx == Prefix) 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
+
+            (True, ((fxName, _, fix, prec) :: _), _) => do
+                -- in the prefix case, remove conflicts with infix (-)
+                let extraFixities = pre ++ (filter (\(nm, _) => not $ nameRoot nm == "-") inf)
+                unless (isCompatible fxName fix prec extraFixities) $ warnConflict fxName extraFixities
+                pure (mkPrec fix prec)
+            -- Could not find any prefix operator fixities, there may be infix ones
+            (True, [] , _) => throw (GenericMsg exprFC $ "'\{op}' is not a prefix operator")
+
+            (False, _, ((fxName, _, fix, prec) :: _)) => do
+                -- in the infix case, remove conflicts with prefix (-)
+                let extraFixities = (filter (\(nm, _) => not $ nm == UN (Basic "-")) pre) ++ inf
+                unless (isCompatible fxName fix prec extraFixities) $ warnConflict fxName extraFixities
+                pure (mkPrec fix prec)
+            -- 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
+    isCompatible : Name -> Fixity -> Nat -> (fixities : List (Name, FC, Fixity, Nat)) -> Bool
+    isCompatible opName fx prec fix
+      = all (\(nm, _, fx', prec') => fx' == fx && prec' == prec) fix
+
+    -- Emits a warning using the fixity that we picked and the list of all conflicting fixities
+    warnConflict : (picked : Name) -> (conflicts : List (Name, FC, Fixity, Nat)) -> Core ()
+    warnConflict fxName all =
+      recordWarning $ GenericWarn exprFC $ """
+                   operator fixity is ambiguous, we are picking \{show fxName} out of :
+                   \{unlines $ map (\(nm, _, _, fx) => " - \{show nm}, precedence level \{show fx}") $ toList all}
+                   To remove this warning, use `%hide` with the fixity to remove
+                   For example: %hide \{show fxName}
+                   """
+
 toTokList : {auto s : Ref Syn SyntaxInfo} ->
+            {auto c : Ref Ctxt Defs} ->
             PTerm -> Core (List (Tok OpStr PTerm))
 toTokList (POp fc opFC opn l r)
-    = do syn <- get Syn
+    = do precInfo <- checkConflictingFixities False fc opn
-         let op = nameRoot opn
+         rtoks <- toTokList r
-         case lookup op (infixes syn) of
+         pure (Expr l :: Op fc opFC opn precInfo :: rtoks)
-              Nothing =>
-                  if any isOpChar (fastUnpack op)
-                     then throw (GenericMsg fc $ "Unknown operator '" ++ op ++ "'")
-                     else do rtoks <- toTokList r
-                             pure (Expr l :: Op fc opFC opn backtickPrec :: rtoks)
-              Just (_, Prefix, _) =>
-                      throw (GenericMsg fc $ "'" ++ op ++ "' is a prefix operator")
-              Just (fixityFc, fix, prec) =>
-                   do rtoks <- toTokList r
-                      pure (Expr l :: Op fc opFC opn (mkPrec fix prec) :: rtoks)
-  where
-    backtickPrec : OpPrec
-    backtickPrec = NonAssoc 1
 toTokList (PPrefixOp fc opFC opn arg)
-    = do syn <- get Syn
+    = do precInfo <- checkConflictingFixities True fc opn
-         let op = nameRoot opn
+         rtoks <- toTokList arg
-         case lookup op (prefixes syn) of
+         pure (Op fc opFC opn precInfo :: rtoks)
-              Nothing =>
-                   throw (GenericMsg fc $ "'" ++ op ++ "' is not a prefix operator")
-              Just (fixityFc, prec) =>
-                   do rtoks <- toTokList arg
-                      pure (Op fc opFC opn (Prefix prec) :: rtoks)
 toTokList t = pure [Expr t]
 
 record BangData where
@@ -197,27 +210,6 @@ idiomise fc dons mns fn
 
 data Bang : Type where
 
-checkFixity : {auto c : Ref Ctxt Defs} ->
-              {auto s : Ref Syn SyntaxInfo} ->
-              FC -> Fixity -> Nat -> String -> Core ()
--- special case for "-", the one thing that's allowed to be both prefix & infix
-checkFixity fc fix prec "-" = pure ()
-checkFixity fc fix prec n =
-  do log "desugar.fixity" 10 "Desugaring fixity (\{show fix} \{show prec}) for \{show n}"
-     syn <- get Syn
-     let test = do (fc', fix', prec') <-
-                     lookup n (infixes syn)
-                     <|> map (map {f = Pair FC} {b = (Fixity, Nat)} (Prefix,)) (lookup n (prefixes syn))
-
-                   guard (not (fix == fix' && prec == prec'))
-                   pure (fc', fix', prec')
-     whenJust test $ \ (fc', fix', prec') =>
-       recordWarning $ GenericWarn fc $ unlines
-         [ "Conflicting fixity declarations for \{n}:"
-         , "  old: \{show fix'} \{show prec'} (\{show fc'})"
-         , "  new: \{show fix} \{show prec} (\{show fc})"
-         ]
-
 mutual
   desugarB : {auto s : Ref Syn SyntaxInfo} ->
              {auto b : Ref Bang BangData} ->
@@ -317,14 +309,16 @@ mutual
       = do syn <- get Syn
            -- It might actually be a prefix argument rather than a section
            -- so check that first, otherwise desugar as a lambda
-           case lookup (nameRoot op) (prefixes syn) of
+           case lookupName op (prefixes syn) of
-                Nothing =>
+                [] =>
-                   desugarB side ps (PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc)
+                    desugarB side ps
-                               (POp fc opFC op (PRef fc (MN "arg" 0)) arg))
+                        (PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc)
-                Just prec => desugarB side ps (PPrefixOp fc opFC op arg)
+                            (POp fc opFC op (PRef fc (MN "arg" 0)) 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)
+      = desugarB side ps
-                 (POp fc opFC op arg (PRef fc (MN "arg" 0))))
+          (PLam fc top Explicit (PRef fc (MN "arg" 0)) (PImplicit fc)
+              (POp fc opFC op arg (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
@@ -1094,16 +1088,22 @@ mutual
       mapDesugarPiInfo : List Name -> PiInfo PTerm -> Core (PiInfo RawImp)
       mapDesugarPiInfo ps = traverse (desugar AnyExpr ps)
 
-  desugarDecl ps (PFixity fc Prefix prec (UN (Basic n)))
+  desugarDecl ps (PFixity fc fix prec opName)
-      = do checkFixity fc Prefix prec n
+      = do ctx <- get Ctxt
-           update Syn { prefixes $= insert n (fc, prec) }
+           -- 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
+           -- declaration site and detect and handle ambiguous fixities
+           let updatedNS = NS (mkNestedNamespace (Just ctx.currentNS) (show fix))
+                              (UN $ Basic $ nameRoot opName)
+
+           -- Depending on the fixity we update the correct fixity context
+           case fix of
+                Prefix =>
+                    update Syn { prefixes $= addName updatedNS (fc, prec) }
+                _ =>
+                    update Syn { infixes $= addName updatedNS (fc, fix, prec) }
            pure []
-  desugarDecl ps (PFixity fc fix prec (UN (Basic n)))
-      = do checkFixity fc fix prec n
-           update Syn { infixes $= insert n (fc, fix, prec) }
-           pure []
-  desugarDecl ps (PFixity fc _ _ _)
-      = throw (GenericMsg fc "Fixity declarations must be for unqualified names")
   desugarDecl ps d@(PFail fc mmsg ds)
       = do -- save the state: the content of a failing block should be discarded
            ust <- get UST
@@ -1163,7 +1163,8 @@ mutual
            pure [IRunElabDecl fc tm']
   desugarDecl ps (PDirective fc d)
       = case d of
-             Hide n => pure [IPragma fc [] (\nest, env => hide fc n)]
+             Hide (HideName n) => pure [IPragma fc [] (\nest, env => hide fc n)]
+             Hide (HideFixity fx n) => pure [IPragma fc [] (\_, _ => removeFixity fx n)]
              Unhide n => pure [IPragma fc [] (\nest, env => unhide fc n)]
              Logging i => pure [ILog ((\ i => (topics i, verbosity i)) <$> i)]
              LazyOn a => pure [IPragma fc [] (\nest, env => lazyActive a)]

src/Idris/Doc/String.idr

@@ -314,11 +314,13 @@ getDocsForName fc n config
 
     getInfixDoc : Name -> Core (List (Doc IdrisDocAnn))
     getInfixDoc n
-        = do let Just (Basic n) = userNameRoot n
+        = let names = lookupName (UN $ Basic $ nameRoot n) (infixes !(get Syn))
-                    | _ => pure []
+          in pure $ map printName names
-             let Just (_, fixity, assoc) = S.lookup n (infixes !(get Syn))
+        where
-                    | Nothing => pure []
+          printName : (Name, FC, Fixity, Nat) -> (Doc IdrisDocAnn)
-             pure $ pure $ hsep
+          printName (name,  loc, fixity, assoc) =
+            -- todo,  change display as "infix operator (++)
+             hsep
                   [ pretty0 (show fixity)
                   , "operator,"
                   , "level"
@@ -327,11 +329,11 @@ getDocsForName fc n config
 
     getPrefixDoc : Name -> Core (List (Doc IdrisDocAnn))
     getPrefixDoc n
-        = do let Just (Basic n) = userNameRoot n
+        = let names = lookupName (UN $ Basic $ nameRoot n) (prefixes !(get Syn))
-                    | _ => pure []
+          in pure $ map printPrefixName names
-             let Just (_, assoc) = S.lookup n (prefixes !(get Syn))
+          where
-                    | Nothing => pure []
+            printPrefixName : (Name, FC, Nat) -> Doc IdrisDocAnn
-             pure $ ["prefix operator, level" <++> pretty0 (show assoc)]
+            printPrefixName (_, _, assoc) = "prefix operator, level" <++> pretty0 (show assoc)
 
     getFixityDoc : Name -> Core (List (Doc IdrisDocAnn))
     getFixityDoc n =

src/Idris/Parser.idr

@@ -1306,7 +1306,7 @@ logLevel fname
 directive : OriginDesc -> IndentInfo -> Rule Directive
 directive fname indents
     = do decoratedPragma fname "hide"
-         n <- name
+         n <- (fixityNS <|> (HideName <$> name))
          atEnd indents
          pure (Hide n)
   <|> do decoratedPragma fname "unhide"

src/Idris/Resugar.idr

@@ -19,6 +19,7 @@ import Data.List
 import Data.Maybe
 import Data.String
 import Libraries.Data.StringMap
+import Libraries.Data.ANameMap
 
 %default covering
 
@@ -36,20 +37,28 @@ mkOp : {auto s : Ref Syn SyntaxInfo} ->
        IPTerm -> Core IPTerm
 mkOp tm@(PApp fc (PApp _ (PRef opFC kn) x) y)
   = do syn <- get Syn
-       let n = rawName kn
+       let raw = rawName kn
+       -- to check if the name is an operator we use the root name as a basic
+       -- user name. This is because if the name is qualified with the namespace
+       -- looking the fixity context will fail. A qualified operator would look
+       -- like this: `M1.M2.(++)` which would not match its fixity namesapce
+       -- that looks like this: `M1.M2.infixl.(++)`. However, since we only want
+       -- 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)
-       case StringMap.lookup (snd $ displayName n) (infixes syn) of
+       if not (null (lookupName rootName (infixes syn)))
-         Just _ => pure asOp
+         then pure asOp
-         Nothing => case dropNS n of
+         else case dropNS raw of
            DN str _ => pure $ ifThenElse (isOpUserName (Basic str)) asOp tm
            _ => pure tm
 mkOp tm@(PApp fc (PRef opFC kn) x)
   = do syn <- get Syn
        let n = rawName kn
        let asOp = PSectionR fc opFC (unbracketApp x) kn
-       case StringMap.lookup (snd $ displayName n) (infixes syn) of
+       if not (null $ lookupName (UN $ Basic (nameRoot n)) (infixes syn))
-         Just _ => pure asOp
+         then pure asOp
-         Nothing => case dropNS n of
+         else case dropNS n of
            DN str _ => pure $ ifThenElse (isOpUserName (Basic str)) asOp tm
            _ => pure tm
 mkOp tm = pure tm
@@ -65,9 +74,9 @@ mkSectionL tm@(PLam fc rig info (PRef _ bd) ty
        syn <- get Syn
        let n = rawName kn
        let asOp = PSectionL fc opFC kn (unbracketApp x)
-       case StringMap.lookup (snd $ displayName n) (infixes syn) of
+       if not (null $ lookupName (UN $ Basic (nameRoot n)) (infixes syn))
-         Just _ => pure asOp
+         then pure asOp
-         Nothing => case dropNS n of
+         else case dropNS n of
            DN str _ => pure $ ifThenElse (isOpUserName (Basic str)) asOp tm
            _ => pure tm
 mkSectionL tm = pure tm

src/Idris/Syntax.idr

@@ -54,6 +54,10 @@ public export
 OpStr : Type
 OpStr = OpStr' Name
 
+public export
+data HidingDirective = HideName Name
+                     | HideFixity Fixity Name
+
 mutual
 
   ||| Source language as produced by the parser
@@ -331,7 +335,7 @@ mutual
 
   public export
   data Directive : Type where
-       Hide : Name -> Directive
+       Hide : HidingDirective -> Directive
        Unhide : Name -> Directive
        Logging : Maybe LogLevel -> Directive
        LazyOn : Bool -> Directive
@@ -882,10 +886,10 @@ record SyntaxInfo where
   -- (most obviously, -)
   ||| Infix operators as a map from their names to their fixity,
   ||| precedence, and the file context where that fixity was defined.
-  infixes : StringMap (FC, Fixity, Nat)
+  infixes : ANameMap (FC, Fixity, Nat)
   ||| Prefix operators as a map from their names to their precedence
   ||| and the file context where their fixity was defined.
-  prefixes : StringMap (FC, Nat)
+  prefixes : ANameMap (FC, Nat)
   -- info about modules
   saveMod : List ModuleIdent -- current module name
   modDocstrings : SortedMap ModuleIdent String
@@ -903,6 +907,10 @@ record SyntaxInfo where
   startExpr : RawImp
   holeNames : List String -- hole names in the file
 
+export
+fixities : SyntaxInfo -> ANameMap (FC, Fixity, Nat)
+fixities syn = merge (infixes syn) (ANameMap.fromList $ map (\(nm, fc, lv) => (nm, fc, Prefix, lv)) $ toList $ prefixes syn)
+
 HasNames IFaceInfo where
   full gam iface
       = do -- coreLift $ printLn (iconstructor iface)
@@ -958,13 +966,13 @@ initSyntax
 
   where
 
-    initInfix : StringMap (FC, Fixity, Nat)
+    initInfix : ANameMap (FC, Fixity, Nat)
-    initInfix = insert "=" (EmptyFC, Infix, 0) empty
+    initInfix = addName (UN $ Basic "=") (EmptyFC, Infix, 0) empty
 
-    initPrefix : StringMap (FC, Nat)
+    initPrefix : ANameMap (FC, Nat)
     initPrefix = fromList
-      [ ("-", (EmptyFC, 10))
+      [ (UN $ Basic "-", (EmptyFC, 10))
-      , ("negate", (EmptyFC, 10)) -- for documentation purposes
+      , (UN $ Basic "negate", (EmptyFC, 10)) -- for documentation purposes
       ]
 
     initDocStrings : ANameMap String
@@ -991,6 +999,13 @@ addModDocInfo mi doc reexpts
                  , modDocexports $= insert mi reexpts
                  , modDocstrings $= insert mi doc }
 
+-- remove a fixity from the context
+export
+removeFixity :
+    {auto s : Ref Syn SyntaxInfo} -> Fixity -> Name -> Core ()
+removeFixity Prefix key = update Syn ({prefixes $= removeExact key })
+removeFixity _ key = update Syn ({infixes $= removeExact key })
+
 export
 covering
 Show PTypeDecl where

src/Idris/Syntax/TTC.idr

@@ -84,8 +84,8 @@ TTC Import where
 export
 TTC SyntaxInfo where
   toBuf b syn
-      = do toBuf b (StringMap.toList (infixes syn))
+      = do toBuf b (ANameMap.toList (infixes syn))
-           toBuf b (StringMap.toList (prefixes syn))
+           toBuf b (ANameMap.toList (prefixes syn))
            toBuf b (filter (\n => elemBy (==) (fst n) (saveMod syn))
                            (SortedMap.toList $ modDocstrings syn))
            toBuf b (filter (\n => elemBy (==) (fst n) (saveMod syn))

src/Libraries/Data/ANameMap.idr

@@ -64,10 +64,32 @@ addName n val (MkANameMap dict hier)
            hier' = addToHier n val hier in
            MkANameMap dict' hier'
 
+||| Remove a fully qualified name
+export
+removeExact : Show a => Name -> ANameMap a -> ANameMap a
+removeExact n (MkANameMap dict hier)
+    = let dict' = delete n dict
+          n' = userNameRoot n
+          hier' = maybe hier
+                     (\foundName => deleteFromList foundName hier) n'
+      in MkANameMap dict' hier'
+  where
+    -- When we find the list of namespace candidates, we need to remove the one that we are pointing
+    -- at and leave the others untouched. We do this by filtering the list of candidates and removing
+    -- the one that matches the namespace of the given name `n`. While we're using `filter`, there should
+    -- only be one of them.
+    deleteFromList : (un : UserName) -> (um : UserNameMap (List (Name, a))) -> UserNameMap (List (Name, a))
+    deleteFromList un = adjust un (filter (\(key, _) => not $ key `matches` n))
+
 export
 toList : ANameMap a -> List (Name, a)
 toList dict = toList (exactNames dict)
 
+||| Export the list of name which are ambiguous without their namespace
+export
+toAmbiguousList : ANameMap a -> List (UserName, List a)
+toAmbiguousList dict = map (mapSnd (map snd)) (toList dict.hierarchy)
+
 export
 fromList : List (Name, a) -> ANameMap a
 fromList = fromList' empty

src/Libraries/Data/StringMap.idr

@@ -278,7 +278,7 @@ sharedSupport l
   = foldl (\acc, (k, v) => case lookup k l of
              Just v' => insert k (v, v') acc
              Nothing => acc)
-    empty . StringMap.toList
+      empty . StringMap.toList
 
 ||| Merge two maps. When encountering duplicate keys, using a function to combine the values.
 ||| Uses the ordering of the first map given.

src/Parser/Lexer/Source.idr

@@ -232,6 +232,10 @@ cgDirective
 mkDirective : String -> Token
 mkDirective str = CGDirective (trim (substr 3 (length str) str))
 
+public export
+fixityKeywords : List String
+fixityKeywords = ["infixl", "infixr", "infix", "prefix"]
+
 -- Reserved words
 -- NB: if you add a new keyword, please add the corresponding documentation in
 --     Idris.Doc.String
@@ -242,9 +246,9 @@ keywords = ["data", "module", "where", "let", "in", "do", "record",
             "parameters", "with", "proof", "impossible", "case", "of",
             "if", "then", "else", "forall", "rewrite",
             "using", "interface", "implementation", "open", "import",
-            "public", "export", "private",
+            "public", "export", "private"] ++
-            "infixl", "infixr", "infix", "prefix",
+            fixityKeywords ++
-            "total", "partial", "covering"]
+            ["total", "partial", "covering"]
 
 public export
 debugInfo : List (String, DebugInfo)

src/Parser/Rule/Source.idr

@@ -10,6 +10,10 @@ import Data.List1
 import Data.SnocList
 import Data.String
 import Libraries.Data.List.Extra
+import Idris.Syntax
+
+%hide Core.Core.(>>)
+%hide Core.Core.(>>=)
 
 %default total
 
@@ -305,12 +309,11 @@ isCapitalisedIdent str =
   let val = str.val
       loc = str.bounds
       err : EmptyRule ()
-          = failLoc loc ("Expected a capitalised identifier, got: " ++ val)
+          = failLoc loc ("Expected a capitalised identifier, got: \{val}")
   in case strM val of
        StrNil => err
        StrCons c _ => if (isUpper c || c > chr 160) then pure () else err
 
-
 export
 namespaceId : Rule Namespace
 namespaceId = do
@@ -402,6 +405,24 @@ nameWithCapital b = opNonNS <|> do
     symbol ")"
     pure (NS ns n)
 
+export
+fixityNS : Rule HidingDirective
+fixityNS = do
+  namespacePrefix <- bounds namespacedIdent
+  let nsVal = namespacePrefix.val
+  fx <- checkFixity (snd nsVal) namespacePrefix.bounds
+  symbol ".("
+  n <- unqualifiedOperatorName
+  symbol ")"
+  pure (HideFixity fx (NS (uncurry mkNestedNamespace nsVal) $ UN $ Basic n))
+  where
+    checkFixity : String -> Bounds -> EmptyRule Fixity
+    checkFixity "infixl" _ = pure InfixL
+    checkFixity "infixr" _ = pure InfixR
+    checkFixity "infix"  _ = pure Infix
+    checkFixity "prefix" _ = pure Prefix
+    checkFixity _ loc =  failLoc loc ""
+
 export
 name : Rule Name
 name = nameWithCapital False

tests/Main.idr

@@ -74,7 +74,7 @@ idrisTestsCasetree = MkTestPool "Case tree building" [] Nothing
 
 idrisTestsWarning : TestPool
 idrisTestsWarning = MkTestPool "Warnings" [] Nothing
-     ["warning001", "warning002", "warning003", "warning004"]
+      ["warning001", "warning002", "warning003", "warning004"]
 
 idrisTestsFailing : TestPool
 idrisTestsFailing = MkTestPool "Failing blocks" [] Nothing
@@ -276,7 +276,7 @@ idrisTests = MkTestPool "Misc" [] Nothing
        -- Implicit laziness, lazy evaluation
        "lazy001", "lazy002", "lazy003",
        -- Namespace blocks
-       "namespace001", "namespace002", "namespace003", "namespace004",
+       "namespace001", "namespace002", "namespace003", "namespace004", "namespace005",
        -- Parameters blocks
        "params001", "params002", "params003",
        -- Larger programs arising from real usage. Typically things with

tests/codegen/con001/expected

@@ -1,8 +1,8 @@
 Dumping case trees to Main.cases
 Prelude.Basics.Nil = Constructor tag Just 0 arity 0
-Prelude.Basics.:: = Constructor tag Just 1 arity 2
+Prelude.Basics.(::) = Constructor tag Just 1 arity 2
 Builtin.MkPair = Constructor tag Just 0 arity 2
-Prelude.Types.Stream.:: = Constructor tag Just 0 arity 2
+Prelude.Types.Stream.(::) = Constructor tag Just 0 arity 2
 Prelude.Num.MkNum = Constructor tag Just 0 arity 3
 Prelude.Num.MkNeg = Constructor tag Just 0 arity 3
 Prelude.Num.MkIntegral = Constructor tag Just 0 arity 3

tests/idris2/basic044/expected

@@ -99,8 +99,8 @@ LOG declare.type:1: Processing Vec.Vec
 LOG declare.def:2: Case tree for Vec.Vec: [0] ({arg:N} : (Data.Fin.Fin {arg:N}[1])) -> {arg:N}[1]
 LOG declare.type:1: Processing Vec.Nil
 LOG declare.def:2: Case tree for Vec.Nil: [0] (Prelude.Uninhabited.absurd {arg:N}[0] (Data.Fin.Fin Prelude.Types.Z) Data.Fin.Uninhabited implementation at Data.Fin:L:C--L:C)
-LOG declare.type:1: Processing Vec.::
+LOG declare.type:1: Processing Vec.(::)
-LOG declare.def:2: Case tree for Vec.::: case {arg:N}[4] : (Data.Fin.Fin (Prelude.Types.S {arg:N}[0])) of
+LOG declare.def:2: Case tree for Vec.(::): case {arg:N}[4] : (Data.Fin.Fin (Prelude.Types.S {arg:N}[0])) of
  { Data.Fin.FZ {e:N} => [0] {arg:N}[3]
  | Data.Fin.FS {e:N} {e:N} => [1] ({arg:N}[5] {e:N}[1])
  }
@@ -154,5 +154,5 @@ With default. Target type : Prelude.Types.Nat
 LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 2 candidates) (delayed) at Vec:L:C--L:C:
 $resolvedN
 Target type : (Prelude.Basics.List Prelude.Types.Nat)
-LOG declare.def:2: Case tree for Vec.test: [0] (Vec.:: (Prelude.Types.S Prelude.Types.Z) (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.Nil Prelude.Types.Nat) (Vec.:: Prelude.Types.Z (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.:: Prelude.Types.Nat Prelude.Types.Z (Prelude.Basics.Nil Prelude.Types.Nat)) (Vec.Nil (Prelude.Basics.List Prelude.Types.Nat))))
+LOG declare.def:2: Case tree for Vec.test: [0] (Vec.(::) (Prelude.Types.S Prelude.Types.Z) (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.Nil Prelude.Types.Nat) (Vec.(::) Prelude.Types.Z (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.(::) Prelude.Types.Nat Prelude.Types.Z (Prelude.Basics.Nil Prelude.Types.Nat)) (Vec.Nil (Prelude.Basics.List Prelude.Types.Nat))))
 Vec> Bye for now!

tests/idris2/interactive030/expected

@@ -1,4 +1,4 @@
-Main> Prelude.== : Eq ty => ty -> ty -> Bool
+Main> Prelude.(==) : Eq ty => ty -> ty -> Bool
   Totality: total
   Visibility: public export
   Fixity Declaration: infix operator, level 6
@@ -7,13 +7,13 @@ Main> Prelude.negate : Neg ty => ty -> ty
   Totality: total
   Visibility: public export
   Fixity Declaration: prefix operator, level 10
-Prelude.- : Neg ty => ty -> ty -> ty
+Prelude.(-) : Neg ty => ty -> ty -> ty
   Totality: total
   Visibility: public export
   Fixity Declarations:
     infixl operator, level 8
     prefix operator, level 10
-Main> Prelude.<$> : Functor f => (a -> b) -> f a -> f b
+Main> Prelude.(<$>) : Functor f => (a -> b) -> f a -> f b
   An infix alias for `map`, applying a function across everything of type 'a'
   in a parameterised type.
   @ f the parameterised type
@@ -44,20 +44,20 @@ Main> Prelude.div : Integral ty => ty -> ty -> ty
   Totality: total
   Visibility: public export
   Fixity Declaration: infixl operator, level 9
-Main> Prelude.>>= : Monad m => m a -> (a -> m b) -> m b
+Main> Prelude.(>>=) : Monad m => m a -> (a -> m b) -> m b
   Also called `bind`.
   Totality: total
   Visibility: public export
   Fixity Declaration: infixl operator, level 1
-Main> Prelude.>> : Monad m => m () -> Lazy (m b) -> m b
+Main> Prelude.(>>) : Monad m => m () -> Lazy (m b) -> m b
   Sequencing of effectful composition
   Totality: total
   Visibility: public export
   Fixity Declaration: infixl operator, level 1
-Main> Main> Main> Main> Main.@@ : (t : a) -> (u : a ** t = u)
+Main> Main> Main> Main> Main.(@@) : (t : a) -> (u : a ** t = u)
   Visibility: private
   Fixity Declaration: prefix operator, level 10
-Main> Prelude.<$ : Functor f => b -> f a -> f b
+Main> Prelude.(<$) : Functor f => b -> f a -> f b
   Run something for effects, replacing the return value with a given parameter.
   Totality: total
   Visibility: public export

tests/idris2/namespace005/Lib1.idr

@@ -0,0 +1,7 @@
+module Lib1
+
+infixr 5 %%%
+
+export
+(%%%) : Nat -> Nat -> Nat
+m %%% n = minus m n

tests/idris2/namespace005/Lib2.idr

@@ -0,0 +1,3 @@
+module Lib2
+
+infixl 5 %%%

tests/idris2/namespace005/LibPre1.idr

@@ -0,0 +1,7 @@
+module LibPre1
+
+prefix 6 *!
+
+export
+(*!) : Nat -> Nat
+(*!) n = n * n

tests/idris2/namespace005/LibPre2.idr

@@ -0,0 +1,3 @@
+module LibPre2
+
+prefix 2 *!

tests/idris2/namespace005/Main0.idr

@@ -0,0 +1,9 @@
+module Main
+
+import Lib1
+import Lib2
+
+%hide Lib1.infixr.(%%%)
+
+main : IO ()
+main = printLn (10 %%% 10 %%% 1)

tests/idris2/namespace005/Main1.idr

@@ -0,0 +1,9 @@
+module Main
+
+import Lib2
+import Lib1
+
+%hide Lib2.infixl.(%%%)
+
+main : IO ()
+main = printLn (10 %%% 10 %%% 1)

tests/idris2/namespace005/Main3.idr

@@ -0,0 +1,14 @@
+module Main3
+
+import Lib1
+
+prefix 4 %%%
+infixr 8 -
+
+(%%%) : Nat -> Nat
+(%%%) = S
+
+main : IO ()
+main = do printLn (the Nat (%%% 4))
+          printLn (1 - 1 - 1)
+

tests/idris2/namespace005/MainConflict.idr

@@ -0,0 +1,7 @@
+module MainConflict
+
+import NonConflict1
+import NonConflict2
+
+exec : IO ()
+exec = printLn (10 &&& 10 &&& 1)

tests/idris2/namespace005/MainFail.idr

@@ -0,0 +1,7 @@
+module Main
+
+import Lib2
+import Lib1
+
+main : IO ()
+main = printLn (10 %%% 10 %%% 1)

tests/idris2/namespace005/MainPre0.idr

@@ -0,0 +1,10 @@
+module Main
+
+import Lib1
+import LibPre1
+import LibPre2
+
+%hide LibPre2.prefix.(*!)
+
+main : IO ()
+main = printLn (*! 10 %%% 10) -- should be 90

tests/idris2/namespace005/MainPre1.idr

@@ -0,0 +1,10 @@
+module Main
+
+import Lib1
+import LibPre1
+import LibPre2
+
+%hide LibPre1.prefix.(*!)
+
+main : IO ()
+main = printLn (*! 10 %%% 10) -- should be 0

tests/idris2/namespace005/NonConflict1.idr

@@ -0,0 +1,8 @@
+module NonConflict1
+
+infixr 5 &&&
+
+export
+(&&&) : Nat -> Nat -> Nat
+(&&&) = minus
+

tests/idris2/namespace005/NonConflict2.idr

@@ -0,0 +1,3 @@
+module NonConflict2
+
+infixr 5 &&&

tests/idris2/namespace005/expected

@@ -0,0 +1,93 @@
+1/3: Building Lib1 (Lib1.idr)
+2/3: Building Lib2 (Lib2.idr)
+3/3: Building Main0 (Main0.idr)
+3/3: Building Main1 (Main1.idr)
+3/3: Building MainFail (MainFail.idr)
+Warning: operator fixity is ambiguous, we are picking Lib2.infixl.(%%%) out of :
+ - Lib2.infixl.(%%%), precedence level 5
+ - Lib1.infixr.(%%%), precedence level 5
+
+To remove this warning, use `%hide` with the fixity to remove
+For example: %hide Lib2.infixl.(%%%)
+
+MainFail:7:17--7:32
+ 3 | import Lib2
+ 4 | import Lib1
+ 5 | 
+ 6 | main : IO ()
+ 7 | main = printLn (10 %%% 10 %%% 1)
+                     ^^^^^^^^^^^^^^^
+
+Warning: operator fixity is ambiguous, we are picking Lib2.infixl.(%%%) out of :
+ - Lib2.infixl.(%%%), precedence level 5
+ - Lib1.infixr.(%%%), precedence level 5
+
+To remove this warning, use `%hide` with the fixity to remove
+For example: %hide Lib2.infixl.(%%%)
+
+MainFail:7:24--7:32
+ 3 | import Lib2
+ 4 | import Lib1
+ 5 | 
+ 6 | main : IO ()
+ 7 | main = printLn (10 %%% 10 %%% 1)
+                            ^^^^^^^^
+
+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:28--12:35
+ 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
+
+To remove this warning, use `%hide` with the fixity to remove
+For example: %hide Prelude.Ops.infixl.(-)
+
+Main3:13:20--13:29
+ 09 | (%%%) = S
+ 10 | 
+ 11 | main : IO ()
+ 12 | main = do printLn (the Nat (%%% 4))
+ 13 |           printLn (1 - 1 - 1)
+                         ^^^^^^^^^
+
+Warning: operator fixity is ambiguous, we are picking Prelude.Ops.infixl.(-) out of :
+ - Prelude.Ops.infixl.(-), precedence level 8
+ - Main3.infixr.(-), precedence level 8
+
+To remove this warning, use `%hide` with the fixity to remove
+For example: %hide Prelude.Ops.infixl.(-)
+
+Main3:13:24--13:29
+ 09 | (%%%) = S
+ 10 | 
+ 11 | main : IO ()
+ 12 | main = do printLn (the Nat (%%% 4))
+ 13 |           printLn (1 - 1 - 1)
+                             ^^^^^
+
+0
+1
+2/4: Building LibPre1 (LibPre1.idr)
+3/4: Building LibPre2 (LibPre2.idr)
+4/4: Building MainPre0 (MainPre0.idr)
+4/4: Building MainPre1 (MainPre1.idr)
+90
+0
+1/3: Building NonConflict1 (NonConflict1.idr)
+2/3: Building NonConflict2 (NonConflict2.idr)
+3/3: Building MainConflict (MainConflict.idr)
+1

tests/idris2/namespace005/run

@@ -0,0 +1,20 @@
+rm -rf ./build
+
+
+$1 --no-color --console-width 0 --check Main0.idr
+$1 --no-color --console-width 0 --check Main1.idr
+$1 --no-color --console-width 0 --check MainFail.idr
+$1 --no-color --console-width 0 --check Main3.idr
+
+$1 --no-color --console-width 0 --exec main Main0.idr
+$1 --no-color --console-width 0 --exec main Main1.idr
+
+$1 --no-color --console-width 0 --check MainPre0.idr
+$1 --no-color --console-width 0 --check MainPre1.idr
+
+$1 --no-color --console-width 0 --exec main MainPre0.idr
+$1 --no-color --console-width 0 --exec main MainPre1.idr
+
+$1 --no-color --console-width 0 --check MainConflict.idr
+$1 --no-color --console-width 0 --exec exec MainConflict.idr
+

tests/idris2/record019/expected

@@ -3,7 +3,7 @@ LOG declare.record.parameters:30: Unelaborated type: (%pi Rig0 Implicit (Just a)
 LOG declare.record.parameters:50: Decided to bind the following extra parameters:
   {0 a : %type}
 
-LOG declare.record.parameters:30: Unelaborated type: (%pi Rig0 Implicit (Just n) Prelude.Nat (%pi Rig0 Implicit (Just a) %type (%pi Rig0 Implicit (Just xs) ((Main.Vect a) n) (%pi Rig0 Implicit (Just ys) ((Main.Vect a) n) (%pi RigW Explicit Nothing (((Builtin.=== [a = ((Main.Vect a) n)]) xs) ys) (%pi RigW Explicit (Just zs) ((Main.Vect a) n) (%pi RigW Explicit Nothing (((Builtin.=== [a = ((Main.Vect a) n)]) zs) xs) %type)))))))
+LOG declare.record.parameters:30: Unelaborated type: (%pi Rig0 Implicit (Just n) Prelude.Nat (%pi Rig0 Implicit (Just a) %type (%pi Rig0 Implicit (Just xs) ((Main.Vect a) n) (%pi Rig0 Implicit (Just ys) ((Main.Vect a) n) (%pi RigW Explicit Nothing (((Builtin.(===) [a = ((Main.Vect a) n)]) xs) ys) (%pi RigW Explicit (Just zs) ((Main.Vect a) n) (%pi RigW Explicit Nothing (((Builtin.(===) [a = ((Main.Vect a) n)]) zs) xs) %type)))))))
 LOG declare.record.parameters:50: Decided to bind the following extra parameters:
   {0 n : Prelude.Types.Nat}
   {0 a : %type}

tests/idris2/spec001/expected

@@ -4,7 +4,7 @@ LOG specialise:3: Specialised type _PE.PE_smult_4e8901402355876e: (n : Prelude.T
 LOG specialise:5: Attempting to specialise:
 ((Main.smult Prelude.Types.Z) n) = Prelude.Types.Z
 ((Main.smult (Prelude.Types.S Prelude.Types.Z)) n) = n
-((Main.smult (Prelude.Types.S m)) n) = ((((Prelude.Num.+ [ty = Prelude.Types.Nat]) [__con = Prelude.Types.Num implementation at Prelude.Types:66:1--71:33]) n) ((Main.smult m) n))
+((Main.smult (Prelude.Types.S m)) n) = ((((Prelude.Num.(+) [ty = Prelude.Types.Nat]) [__con = Prelude.Types.Num implementation at Prelude.Types:66:1--71:33]) n) ((Main.smult m) n))
 LOG specialise:5: New patterns for _PE.PE_smult_4e8901402355876e:
 (_PE.PE_smult_4e8901402355876e $_pe0) = (($resolved2645 (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))) _pe0)
 LOG specialise:5: New RHS: (Prelude.Types.plus _pe0[0] (Prelude.Types.plus _pe0[0] _pe0[0]))
@@ -30,15 +30,15 @@ LOG specialise:5: Already specialised _PE.PE_fold_3a845f1ca594c582
 LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_8abb50b713fe8e5e by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8738} : a[0]) -> b[2]) => \({arg:8743} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapImpl b[3] a[2] func[1] {arg:8743}[0]))), (3, Dynamic)
 LOG specialise:3: Specialised type _PE.PE_fold_8abb50b713fe8e5e: ({arg:840} : ({arg:842} : (Prelude.Basics.List Prelude.Types.Nat)) -> Prelude.Types.Nat) -> ({arg:847} : (Main.Mu Prelude.Basics.List)) -> Prelude.Types.Nat
 LOG specialise:5: Attempting to specialise:
-(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.<$> [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8792} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t))
+(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8792} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t))
 LOG specialise:5: New patterns for _PE.PE_fold_8abb50b713fe8e5e:
-((_PE.PE_fold_8abb50b713fe8e5e alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.<$> [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8792} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8743}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8743}))))))]) alg)) t))
+((_PE.PE_fold_8abb50b713fe8e5e alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8792} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8743}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8743}))))))]) alg)) t))
 LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_a727631bc09e3761 by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8738} : a[0]) -> b[2]) => \({arg:8743} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapAppend a[2] b[3] (Prelude.Basics.Lin b[3]) func[1] {arg:8743}[0]))), (3, Dynamic)
 LOG specialise:3: Specialised type _PE.PE_fold_a727631bc09e3761: ({arg:840} : ({arg:842} : (Prelude.Basics.List Prelude.Types.Nat)) -> Prelude.Types.Nat) -> ({arg:847} : (Main.Mu Prelude.Basics.List)) -> Prelude.Types.Nat
 LOG specialise:5: Attempting to specialise:
-(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.<$> [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8792} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t))
+(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8792} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t))
 LOG specialise:5: New patterns for _PE.PE_fold_a727631bc09e3761:
-((_PE.PE_fold_a727631bc09e3761 alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.<$> [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8792} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8743}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8743}))))))]) alg)) t))
+((_PE.PE_fold_a727631bc09e3761 alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8792} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8743}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8738}) a b) (%lam RigW Explicit (Just {arg:8743}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8743}))))))]) alg)) t))
 LOG specialise:5: Already specialised _PE.PE_fold_a727631bc09e3761
 LOG specialise:5: New RHS: (alg[0] (Prelude.Types.List.mapAppend (Main.Mu Prelude.Basics.List) Prelude.Types.Nat (Prelude.Basics.Lin Prelude.Types.Nat) (_PE.PE_fold_a727631bc09e3761 alg[0]) t[1]))
 LOG specialise:5: Already specialised _PE.PE_fold_a727631bc09e3761
@@ -51,19 +51,19 @@ LOG specialise.declare:5: Specialising Main.identity ($resolved2645) -> _PE.PE_i
 LOG specialise:3: Specialised type _PE.PE_identity_3c7f5598e5c9b732: ({arg:813} : (Prelude.Basics.List Prelude.Types.Nat)) -> (Prelude.Basics.List Prelude.Types.Nat)
 LOG specialise:5: Attempting to specialise:
 ((Main.identity [a = a]) (Prelude.Basics.Nil [a = a])) = (Prelude.Basics.Nil [a = a])
-((Main.identity [a = a]) (((Prelude.Basics.:: [a = a]) x) xs)) = (((Prelude.Basics.:: [a = a]) x) ((Main.identity [a = a]) xs))
+((Main.identity [a = a]) (((Prelude.Basics.(::) [a = a]) x) xs)) = (((Prelude.Basics.(::) [a = a]) x) ((Main.identity [a = a]) xs))
 LOG specialise:5: New patterns for _PE.PE_identity_3c7f5598e5c9b732:
 (_PE.PE_identity_3c7f5598e5c9b732 (Prelude.Basics.Nil [a = Prelude.Types.Nat])) = (Prelude.Basics.Nil [a = Prelude.Types.Nat])
-(_PE.PE_identity_3c7f5598e5c9b732 (((Prelude.Basics.:: [a = Prelude.Types.Nat]) x) xs)) = (((Prelude.Basics.:: [a = Prelude.Types.Nat]) x) ((Main.identity [a = Prelude.Types.Nat]) xs))
+(_PE.PE_identity_3c7f5598e5c9b732 (((Prelude.Basics.(::) [a = Prelude.Types.Nat]) x) xs)) = (((Prelude.Basics.(::) [a = Prelude.Types.Nat]) x) ((Main.identity [a = Prelude.Types.Nat]) xs))
 LOG specialise:5: New RHS: (Prelude.Basics.Nil Prelude.Types.Nat)
 LOG specialise:5: Already specialised _PE.PE_identity_3c7f5598e5c9b732
-LOG specialise:5: New RHS: (Prelude.Basics.:: Prelude.Types.Nat x[1] (_PE.PE_identity_3c7f5598e5c9b732 xs[0]))
+LOG specialise:5: New RHS: (Prelude.Basics.(::) Prelude.Types.Nat x[1] (_PE.PE_identity_3c7f5598e5c9b732 xs[0]))
 LOG specialise:5: Already specialised _PE.PE_identity_3c7f5598e5c9b732
 LOG compiler.identity:5: found identity flag for: _PE.PE_identity_3c7f5598e5c9b732, 0
-	old def: Just [{arg:0}]: (%case !{arg:0} [(%concase [nil] Prelude.Basics.Nil Just 0 [] (%con [nil] Prelude.Basics.Nil Just 0 [])), (%concase [cons] Prelude.Basics.:: Just 1 [{e:2}, {e:3}] (%con [cons] Prelude.Basics.:: Just 1 [!{e:2}, (_PE.PE_identity_3c7f5598e5c9b732 [!{e:3}])]))] Nothing)
+	old def: Just [{arg:0}]: (%case !{arg:0} [(%concase [nil] Prelude.Basics.Nil Just 0 [] (%con [nil] Prelude.Basics.Nil Just 0 [])), (%concase [cons] Prelude.Basics.(::) Just 1 [{e:2}, {e:3}] (%con [cons] Prelude.Basics.(::) Just 1 [!{e:2}, (_PE.PE_identity_3c7f5598e5c9b732 [!{e:3}])]))] Nothing)
 LOG compiler.identity:5: 	new def: [{arg:0}]: !{arg:0}
 LOG compiler.identity:5: found identity flag for: Main.identity, 0
-	old def: Just [{arg:1}]: (%case !{arg:1} [(%concase [nil] Prelude.Basics.Nil Just 0 [] (%con [nil] Prelude.Basics.Nil Just 0 [])), (%concase [cons] Prelude.Basics.:: Just 1 [{e:2}, {e:3}] (%con [cons] Prelude.Basics.:: Just 1 [!{e:2}, (Main.identity [!{e:3}])]))] Nothing)
+	old def: Just [{arg:1}]: (%case !{arg:1} [(%concase [nil] Prelude.Basics.Nil Just 0 [] (%con [nil] Prelude.Basics.Nil Just 0 [])), (%concase [cons] Prelude.Basics.(::) Just 1 [{e:2}, {e:3}] (%con [cons] Prelude.Basics.(::) Just 1 [!{e:2}, (Main.identity [!{e:3}])]))] Nothing)
 LOG compiler.identity:5: 	new def: [{arg:1}]: !{arg:1}
 LOG compiler.identity:5: found identity flag for: _PE.PE_identity_3c7f5598e5c9b732, 0
 	old def: Just [{arg:0}]: !{arg:0}

tests/idris2/warning004/expected

@@ -1,12 +1,66 @@
 1/3: Building Lib1 (Lib1.idr)
 2/3: Building Lib2 (Lib2.idr)
 3/3: Building Main0 (Main0.idr)
-Warning: Conflicting fixity declarations:
+Warning: operator fixity is ambiguous, we are picking Lib2.infixl.(%%%) out of :
-%%%: infixl 5 (at Lib2:3:1--3:13) and infixr 5 (at Lib1:3:1--3:13)
+ - Lib2.infixl.(%%%), precedence level 5
+ - Lib1.infixr.(%%%), precedence level 5
+
+To remove this warning, use `%hide` with the fixity to remove
+For example: %hide Lib2.infixl.(%%%)
+
+Main0:7:17--7:32
+ 3 | import Lib1
+ 4 | import Lib2
+ 5 | 
+ 6 | main : IO ()
+ 7 | main = printLn (10 %%% 10 %%% 1)
+                     ^^^^^^^^^^^^^^^
+
+Warning: operator fixity is ambiguous, we are picking Lib2.infixl.(%%%) out of :
+ - Lib2.infixl.(%%%), precedence level 5
+ - Lib1.infixr.(%%%), precedence level 5
+
+To remove this warning, use `%hide` with the fixity to remove
+For example: %hide Lib2.infixl.(%%%)
+
+Main0:7:24--7:32
+ 3 | import Lib1
+ 4 | import Lib2
+ 5 | 
+ 6 | main : IO ()
+ 7 | main = printLn (10 %%% 10 %%% 1)
+                            ^^^^^^^^
 
 3/3: Building Main1 (Main1.idr)
-Warning: Conflicting fixity declarations:
+Warning: operator fixity is ambiguous, we are picking Lib2.infixl.(%%%) out of :
-%%%: infixr 5 (at Lib1:3:1--3:13) and infixl 5 (at Lib2:3:1--3:13)
+ - Lib2.infixl.(%%%), precedence level 5
+ - Lib1.infixr.(%%%), precedence level 5
+
+To remove this warning, use `%hide` with the fixity to remove
+For example: %hide Lib2.infixl.(%%%)
+
+Main1:7:17--7:32
+ 3 | import Lib2
+ 4 | import Lib1
+ 5 | 
+ 6 | main : IO ()
+ 7 | main = printLn (10 %%% 10 %%% 1)
+                     ^^^^^^^^^^^^^^^
+
+Warning: operator fixity is ambiguous, we are picking Lib2.infixl.(%%%) out of :
+ - Lib2.infixl.(%%%), precedence level 5
+ - Lib1.infixr.(%%%), precedence level 5
+
+To remove this warning, use `%hide` with the fixity to remove
+For example: %hide Lib2.infixl.(%%%)
+
+Main1:7:24--7:32
+ 3 | import Lib2
+ 4 | import Lib1
+ 5 | 
+ 6 | main : IO ()
+ 7 | main = printLn (10 %%% 10 %%% 1)
+                            ^^^^^^^^
 
 0
-1
+0