[ re #2832 ] warn about conflicting fixity declarations (#2889)

CHANGELOG.md

@@ -64,6 +64,10 @@
 
 * Made sure that the positivity checker now respects `assert_total` annotations.
 
+* We now raise a warning for conflicting fixity declarations. They are
+  dangerous as Idris will pick an arbitrary one and so the meaning of an
+  expression can depend e.g. on the order in which modules are imported.
+
 ### Library changes
 
 #### Prelude

libs/contrib/Data/Telescope/Telescope.idr

@@ -158,7 +158,7 @@ namespace Right
 
 namespace Tree
 
-  infixl 4 ++
+  infixl 4 ><
 
   mutual
     ||| A tree of dependent types
@@ -166,7 +166,7 @@ namespace Tree
     data Telescope : (k : Nat) -> Type where
       Nil  : Telescope 0
       Elt  : Type -> Telescope 1
-      (++) : (gamma : Tree.Telescope m) ->
+      (><) : (gamma : Tree.Telescope m) ->
              (delta : Tree.Environment gamma -> Tree.Telescope n) ->
               Telescope (m + n)
 
@@ -175,13 +175,13 @@ namespace Tree
     Environment : Tree.Telescope k -> Type
     Environment [] = ()
     Environment (Elt t) = t
-    Environment (gamma ++ delta) = (env : Environment gamma ** Environment (delta env))
+    Environment (gamma >< delta) = (env : Environment gamma ** Environment (delta env))
 
   export
   concat : (gamma : Tree.Telescope k) -> (delta : Right.Telescope k ** Environment delta -> Environment gamma)
   concat Nil = ([] ** id)
   concat (Elt t) = ((t .- const []) ** fst)
-  concat (gamma ++ delta) =
+  concat (gamma >< delta) =
     let (thetaL ** transpL) = concat gamma in
     ((thetaL ++ \ envL => fst (concat (delta (transpL envL))))
     ** \ env =>

libs/papers/Search/Tychonoff/PartI.idr

@@ -318,7 +318,6 @@ IsSubSingleton (So b) where
 IsSubSingleton (v === w) where
   isSubSingleton Refl Refl = Refl
 
-infix 0 ~~~
 0 (~~~) : {0 b : a -> Type} -> (f, g : (x : a) ->  b x) -> Type
 f ~~~ g = (x : a) -> f x === g x
 

src/Compiler/CompileExpr.idr

@@ -799,7 +799,7 @@ compileDef n
            -- we do for whole program compilation, though, since that involves
            -- traversing everything from the main expression.
            -- For now, consider it an incentive not to have cycles :).
-            then recordWarning (GenericWarn ("Compiling hole " ++ show n))
+            then recordWarning (GenericWarn emptyFC ("Compiling hole " ++ show n))
             else do ce <- toCDef n (type gdef) (eraseArgs gdef)
                            !(toFullNames (definition gdef))
                     setCompiled n ce

src/Compiler/ES/Doc.idr

@@ -2,7 +2,8 @@ module Compiler.ES.Doc
 
 import Data.List
 
-infixl 8 <++>, <?>
+infixr 6 <++>
+infixl 8 <?>
 
 public export
 data Doc

src/Core/Context.idr

@@ -705,16 +705,16 @@ HasNames Warning where
   full gam (ShadowingGlobalDefs fc xs)
     = ShadowingGlobalDefs fc <$> traverseList1 (traversePair (traverseList1 (full gam))) xs
   full gam w@(ShadowingLocalBindings _ _) = pure w
-  full gam (Deprecated x y) = Deprecated x <$> traverseOpt (traversePair (full gam)) y
-  full gam (GenericWarn x) = pure (GenericWarn x)
+  full gam (Deprecated fc x y) = Deprecated fc x <$> traverseOpt (traversePair (full gam)) y
+  full gam (GenericWarn fc x) = pure (GenericWarn fc x)
 
   resolved gam (ParserWarning fc x) = pure (ParserWarning fc x)
   resolved gam (UnreachableClause fc rho s) = UnreachableClause fc <$> resolved gam rho <*> resolved gam s
   resolved gam (ShadowingGlobalDefs fc xs)
     = ShadowingGlobalDefs fc <$> traverseList1 (traversePair (traverseList1 (resolved gam))) xs
   resolved gam w@(ShadowingLocalBindings _ _) = pure w
-  resolved gam (Deprecated x y) = Deprecated x <$> traverseOpt (traversePair (resolved gam)) y
-  resolved gam (GenericWarn x) = pure (GenericWarn x)
+  resolved gam (Deprecated fc x y) = Deprecated fc x <$> traverseOpt (traversePair (resolved gam)) y
+  resolved gam (GenericWarn fc x) = pure (GenericWarn fc x)
 
 export
 HasNames Error where
@@ -2483,7 +2483,7 @@ addImportedInc modNS inc
                 Nothing =>
                   -- No incremental compile data for current CG, so we can't
                   -- compile incrementally
-                  do recordWarning (GenericWarn ("No incremental compile data for " ++ show modNS))
+                  do recordWarning (GenericWarn emptyFC ("No incremental compile data for " ++ show modNS))
                      defs <- get Ctxt
                      put Ctxt ({ allIncData $= drop cg } defs)
                      -- Tell session that the codegen is no longer incremental
@@ -2536,5 +2536,5 @@ unhide fc n
               | res => ambiguousName fc n (map fst res)
          put Ctxt ({ gamma $= unhideName nsn } defs)
          unless (isHidden nsn (gamma defs)) $ do
-           recordWarning $ GenericWarn $
+           recordWarning $ GenericWarn fc $
              "Trying to %unhide `" ++ show nsn ++ "`, which was not hidden in the first place"

src/Core/Core.idr

@@ -73,8 +73,8 @@ data Warning : Type where
      ShadowingLocalBindings : FC -> (shadowed : List1 (String, FC, FC)) -> Warning
      ||| A warning about a deprecated definition. Supply an FC and Name to
      ||| have the documentation for the definition printed with the warning.
-     Deprecated : String -> Maybe (FC, Name) -> Warning
-     GenericWarn : String -> Warning
+     Deprecated : FC -> String -> Maybe (FC, Name) -> Warning
+     GenericWarn : FC -> String -> Warning
 
 %name Warning wrn
 
@@ -199,12 +199,12 @@ Show TTCErrorMsg where
 
 export
 Show Warning where
-    show (ParserWarning _ msg) = msg
-    show (UnreachableClause _ _ _) = ":Unreachable clause"
-    show (ShadowingGlobalDefs _ _) = ":Shadowing names"
-    show (ShadowingLocalBindings _ _) = ":Shadowing names"
-    show (Deprecated name _) = ":Deprecated " ++ name
-    show (GenericWarn msg) = msg
+    show (ParserWarning fc msg) = show fc ++ msg
+    show (UnreachableClause fc _ _) = show fc ++ ":Unreachable clause"
+    show (ShadowingGlobalDefs fc _) = show fc ++ ":Shadowing names"
+    show (ShadowingLocalBindings fc _) = show fc ++ ":Shadowing names"
+    show (Deprecated fc name _) = show fc ++ ":Deprecated " ++ name
+    show (GenericWarn fc msg) = show fc ++ msg
 
 
 export
@@ -387,13 +387,13 @@ Show Error where
   show (WarningAsError w) = show w
 
 export
-getWarningLoc : Warning -> Maybe FC
-getWarningLoc (ParserWarning fc _) = Just fc
-getWarningLoc (UnreachableClause fc _ _) = Just fc
-getWarningLoc (ShadowingGlobalDefs fc _) = Just fc
-getWarningLoc (ShadowingLocalBindings fc _) = Just fc
-getWarningLoc (Deprecated _ fcAndName) = fst <$> fcAndName
-getWarningLoc (GenericWarn _) = Nothing
+getWarningLoc : Warning -> FC
+getWarningLoc (ParserWarning fc _) = fc
+getWarningLoc (UnreachableClause fc _ _) = fc
+getWarningLoc (ShadowingGlobalDefs fc _) = fc
+getWarningLoc (ShadowingLocalBindings fc _) = fc
+getWarningLoc (Deprecated fc _ fcAndName) = fromMaybe fc (fst <$> fcAndName)
+getWarningLoc (GenericWarn fc _) = fc
 
 export
 getErrorLoc : Error -> Maybe FC
@@ -470,7 +470,7 @@ getErrorLoc (FailingWrongError fc _ _) = pure fc
 getErrorLoc (InLHS _ _ err) = getErrorLoc err
 getErrorLoc (InRHS _ _ err) = getErrorLoc err
 getErrorLoc (MaybeMisspelling err _) = getErrorLoc err
-getErrorLoc (WarningAsError warn) = getWarningLoc warn
+getErrorLoc (WarningAsError warn) = Just (getWarningLoc warn)
 
 export
 killWarningLoc : Warning -> Warning
@@ -479,8 +479,8 @@ killWarningLoc (UnreachableClause fc x y) = UnreachableClause emptyFC x y
 killWarningLoc (ShadowingGlobalDefs fc xs) = ShadowingGlobalDefs emptyFC xs
 killWarningLoc (ShadowingLocalBindings fc xs) =
     ShadowingLocalBindings emptyFC $ (\(n, _, _) => (n, emptyFC, emptyFC)) <$> xs
-killWarningLoc (Deprecated x y) = Deprecated x (map ((emptyFC,) . snd) y)
-killWarningLoc (GenericWarn x) = GenericWarn x
+killWarningLoc (Deprecated fc x y) = Deprecated emptyFC x (map ((emptyFC,) . snd) y)
+killWarningLoc (GenericWarn fc x) = GenericWarn emptyFC x
 
 export
 killErrorLoc : Error -> Error
@@ -630,19 +630,16 @@ export %inline
 ma >> mb = ma >>= const mb
 
 -- Flipped bind
-infixr 1 =<<
 export %inline
 (=<<) : (a -> Core b) -> Core a -> Core b
 (=<<) = flip (>>=)
 
 -- Kleisli compose
-infixr 1 >=>
 export %inline
 (>=>) : (a -> Core b) -> (b -> Core c) -> (a -> Core c)
 f >=> g = (g =<<) . f
 
 -- Flipped kleisli compose
-infixr 1 <=<
 export %inline
 (<=<) : (b -> Core c) -> (a -> Core b) -> (a -> Core c)
 (<=<) = flip (>=>)

src/Core/Name/Namespace.idr

@@ -81,7 +81,6 @@ mkModuleIdent (Just (MkNS ns)) n = MkMI (n :: ns)
 -- MANIPULATING NAMESPACES
 -------------------------------------------------------------------------------------
 
-infixl 5 <.>
 ||| Extend an existing namespace with additional name parts to form a more local one.
 ||| e.g. `X.Y.Z <.> S.T.U` to get `X.Y.Z.S.T.U`.
 export

src/Core/Options/Log.idr

@@ -88,6 +88,7 @@ knownTopics = [
     ("declare.type", Nothing),
     ("desugar.idiom", Nothing),
     ("desugar.failing", Just "Log result of desugaring a `failing' block"),
+    ("desugar.fixity", Just "Log result of desugaring a fixity declaration"),
     ("desugar.lhs", Just "Log result of desugaring a left hand side"),
     ("doc.data", Nothing),
     ("doc.implementation", Nothing),

src/Idris/Desugar.idr

@@ -82,6 +82,29 @@ 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')))
+                   . StringMap.toList
+         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),
@@ -174,6 +197,27 @@ 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} ->
@@ -1051,10 +1095,12 @@ mutual
       mapDesugarPiInfo ps = traverse (desugar AnyExpr ps)
 
   desugarDecl ps (PFixity fc Prefix prec (UN (Basic n)))
-      = do update Syn { prefixes $= insert n (fc, prec) }
+      = do checkFixity fc Prefix prec n
+           update Syn { prefixes $= insert n (fc, prec) }
            pure []
   desugarDecl ps (PFixity fc fix prec (UN (Basic n)))
-      = do update Syn { infixes $= insert n (fc, fix, prec) }
+      = 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")

src/Idris/Error.idr

@@ -33,8 +33,8 @@ Eq Warning where
   ParserWarning fc1 x1 == ParserWarning fc2 x2 = fc1 == fc2 && x1 == x2
   UnreachableClause fc1 rho1 s1 == UnreachableClause fc2 rho2 s2 = fc1 == fc2
   ShadowingGlobalDefs fc1 xs1 == ShadowingGlobalDefs fc2 xs2 = fc1 == fc2 && xs1 == xs2
-  Deprecated x1 y1 == Deprecated x2 y2 = x1 == x2 && y1 == y2
-  GenericWarn x1 == GenericWarn x2 = x1 == x2
+  Deprecated fc1 x1 y1 == Deprecated fc2 x2 y2 = fc1 == fc2 && x1 == x2 && y1 == y2
+  GenericWarn fc1 x1 == GenericWarn fc2 x2 = fc1 == fc2 && x1 == x2
   _ == _ = False
 
 export
@@ -281,13 +281,13 @@ pwarningRaw (ShadowingLocalBindings fc ns)
     , !(ploc fc)
     ]
 
-pwarningRaw (Deprecated s fcAndName)
+pwarningRaw (Deprecated fc s fcAndName)
     = do docs <- traverseOpt (\(fc, name) => getDocsForName fc name justUserDoc) fcAndName
          pure . vsep $ catMaybes [ Just $ "Deprecation warning:" <++> pretty0 s
                                  , reAnnotate (const Pretty.UserDocString) <$> docs
                                  ]
-pwarningRaw (GenericWarn s)
-    = pure $ pretty0 s
+pwarningRaw (GenericWarn fc s)
+    = pure $ vcat [pretty0 s, !(ploc fc)]
 
 export
 pwarning : {auto c : Ref Ctxt Defs} ->

src/Idris/Package.idr

@@ -215,7 +215,7 @@ addField : {auto c : Ref Ctxt Defs} ->
 addField (PVersion fc n)       pkg = pure $ { version := Just n } pkg
 addField (PLangVersions fc bs) pkg = pure $ { langversion := Just bs } pkg
 addField (PVersionDep fc n)   pkg
-    = do emitWarning (Deprecated "version numbers must now be of the form x.y.z" Nothing)
+    = do emitWarning (Deprecated fc "version numbers must now be of the form x.y.z" Nothing)
          pure pkg
 addField (PAuthors fc a)     pkg = pure $ { authors := Just a } pkg
 addField (PMaintainers fc a) pkg = pure $ { maintainers := Just a } pkg

src/Idris/REPL/Common.idr

@@ -144,7 +144,7 @@ emitWarning : {auto c : Ref Ctxt Defs} ->
               {auto o : Ref ROpts REPLOpts} ->
               {auto s : Ref Syn SyntaxInfo} ->
               Warning -> Core ()
-emitWarning w = emitProblem w displayWarning pwarning getWarningLoc MsgStatusInfo
+emitWarning w = emitProblem w displayWarning pwarning (Just . getWarningLoc) MsgStatusInfo
 
 export
 emitWarnings : {auto c : Ref Ctxt Defs} ->

src/Idris/Syntax.idr

@@ -38,6 +38,14 @@ Show Fixity where
   show Infix  = "infix"
   show Prefix = "prefix"
 
+export
+Eq Fixity where
+  InfixL == InfixL = True
+  InfixR == InfixR = True
+  Infix == Infix = True
+  Prefix == Prefix = True
+  _ == _ = False
+
 public export
 OpStr' : Type -> Type
 OpStr' nm = nm

src/Libraries/Data/StringMap.idr

@@ -271,6 +271,15 @@ implementation Functor StringMap where
   map _ Empty = Empty
   map f (M n t) = M _ (treeMap f t)
 
+||| Return a map of pairs of values that happen to share the same keys
+export
+sharedSupport : StringMap v -> StringMap v -> StringMap (v, v)
+sharedSupport l
+  = foldl (\acc, (k, v) => case lookup k l of
+             Just v' => insert k (v, v') acc
+             Nothing => acc)
+    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.
 export

src/TTImp/Elab/App.idr

@@ -98,7 +98,7 @@ getNameType elabMode rigc env fc x
     checkDeprecation fc gdef =
       do when (Deprecate `elem` gdef.flags) $
            recordWarning $
-             Deprecated
+             Deprecated fc
                "\{show gdef.fullname} is deprecated and will be removed in a future version."
                (Just (fc, gdef.fullname))
 

tests/Main.idr

@@ -74,7 +74,7 @@ idrisTestsCasetree = MkTestPool "Case tree building" [] Nothing
 
 idrisTestsWarning : TestPool
 idrisTestsWarning = MkTestPool "Warnings" [] Nothing
-     ["warning001", "warning002", "warning003"]
+     ["warning001", "warning002", "warning003", "warning004"]
 
 idrisTestsFailing : TestPool
 idrisTestsFailing = MkTestPool "Failing blocks" [] Nothing

tests/idris2/warning004/Lib1.idr

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

tests/idris2/warning004/Lib2.idr

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

tests/idris2/warning004/Main0.idr

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

tests/idris2/warning004/Main1.idr

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

tests/idris2/warning004/expected

@@ -0,0 +1,12 @@
+1/3: Building Lib1 (Lib1.idr)
+2/3: Building Lib2 (Lib2.idr)
+3/3: Building Main0 (Main0.idr)
+Warning: Conflicting fixity declarations:
+%%%: infixl 5 (at Lib2:3:1--3:13) and infixr 5 (at Lib1:3:1--3:13)
+
+3/3: Building Main1 (Main1.idr)
+Warning: Conflicting fixity declarations:
+%%%: infixr 5 (at Lib1:3:1--3:13) and infixl 5 (at Lib2:3:1--3:13)
+
+0
+1

tests/idris2/warning004/run

@@ -0,0 +1,8 @@
+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 --exec main Main0.idr
+$1 --no-color --console-width 0 --exec main Main1.idr