Emit warning for fixities with no export modifiers (#3234)

* Emit warning for fixities with no export modifiers This is to help update all the existing code to program with explicit fixity export directives in preparation for the behavioral change where they will become private by default.
idris-lang · Apr 3, 2024 · 75032a7 · 75032a7
1 parent aa3f67c
commit 75032a7
Show file tree

Hide file tree

Showing 128 changed files with 417 additions and 303 deletions.
diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md
@@ -30,6 +30,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
   customise the syntax of operator to look more like a binder.
   See [#3113](https://github.com/idris-lang/Idris2/issues/3113).
 
+* Fixity declarations without an export modifier now emit a warning in peparation
+  for a future version where they will become private by default.
+
 * Elaborator scripts were made to be able to access the visibility modifier of a
   definition, via `getVis`.
 

diff --git a/libs/base/Data/Bits.idr b/libs/base/Data/Bits.idr
@@ -5,10 +5,10 @@ import Data.Vect
 
 %default total
 
-infixl 8 `shiftL`, `shiftR`
-infixl 7 .&.
-infixl 6 `xor`
-infixl 5 .|.
+export infixl 8 `shiftL`, `shiftR`
+export infixl 7 .&.
+export infixl 6 `xor`
+export infixl 5 .|.
 
 --------------------------------------------------------------------------------
 --          Interface Bits

diff --git a/libs/base/Data/Contravariant.idr b/libs/base/Data/Contravariant.idr
@@ -2,7 +2,7 @@ module Data.Contravariant
 
 %default total
 
-infixl 4 >$, >$<, >&<, $<
+export infixl 4 >$, >$<, >&<, $<
 
 ||| Contravariant functors
 public export

diff --git a/libs/base/Data/Fin.idr b/libs/base/Data/Fin.idr
@@ -304,7 +304,7 @@ namespace Equality
     FZ : Pointwise FZ FZ
     FS : Pointwise k l -> Pointwise (FS k) (FS l)
 
-  infix 6 ~~~
+  export infix 6 ~~~
   ||| Convenient infix notation for the notion of pointwise equality of Fins
   public export
   (~~~) : Fin m -> Fin n -> Type

diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr
@@ -270,7 +270,7 @@ public export
 deleteFirstsBy : (p : a -> b -> Bool) -> (source : List b) -> (undesirables : List a) -> List b
 deleteFirstsBy p = foldl (flip (deleteBy p))
 
-infix 7 \\
+export infix 7 \\
 
 ||| The non-associative list-difference.
 ||| A specialized form of @deleteFirstsBy@ where the predicate is equality under the @Eq@

diff --git a/libs/base/Data/List1.idr b/libs/base/Data/List1.idr
@@ -5,7 +5,7 @@ import public Control.Function
 
 %default total
 
-infixr 7 :::
+export infixr 7 :::
 
 ||| Non-empty lists.
 public export

diff --git a/libs/base/Data/Morphisms.idr b/libs/base/Data/Morphisms.idr
@@ -9,7 +9,7 @@ record Morphism a b where
   constructor Mor
   applyMor : a -> b
 
-infixr 1 ~>
+export infixr 1 ~>
 
 public export
 (~>) : Type -> Type -> Type

diff --git a/libs/base/Data/Zippable.idr b/libs/base/Data/Zippable.idr
@@ -21,7 +21,7 @@ interface Zippable z where
   zip : z a -> z b -> z (a, b)
   zip = zipWith (,)
 
-  infixr 6 `zip`
+  export infixr 6 `zip`
 
   ||| Combine three parameterised types by applying a function.
   ||| @ z the parameterised type

diff --git a/libs/base/Syntax/PreorderReasoning.idr b/libs/base/Syntax/PreorderReasoning.idr
@@ -2,9 +2,7 @@
 ||| poor-man's equational reasoning
 module Syntax.PreorderReasoning
 
-infixl 0  ~~,~=
-prefix 1  |~
-infix  1  ...,..<,..>,.=.,.=<,.=>
+import public Syntax.PreorderReasoning.Ops
 
 |||Slightly nicer syntax for justifying equations:
 |||```

diff --git a/libs/base/Syntax/PreorderReasoning/Generic.idr b/libs/base/Syntax/PreorderReasoning/Generic.idr
@@ -2,10 +2,7 @@ module Syntax.PreorderReasoning.Generic
 
 import Control.Relation
 import Control.Order
-infixl 0  ~~, ~=
-infixl 0  <~
-prefix 1  |~
-infix  1  ...,..<,..>,.=.,.=<,.=>
+import public Syntax.PreorderReasoning.Ops
 
 public export
 data Step : (leq : a -> a -> Type) -> a -> a -> Type where

diff --git a/libs/base/Syntax/PreorderReasoning/Ops.idr b/libs/base/Syntax/PreorderReasoning/Ops.idr
@@ -0,0 +1,6 @@
+module Syntax.PreorderReasoning.Ops
+
+export infixl 0  ~~, ~=
+export infixl 0  <~
+export prefix 1  |~
+export infix  1  ...,..<,..>,.=.,.=<,.=>
diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg
@@ -108,6 +108,7 @@ modules = Control.App,
           Language.Reflection.TTImp,
 
           Syntax.PreorderReasoning,
+          Syntax.PreorderReasoning.Ops,
           Syntax.PreorderReasoning.Generic,
 
           System,

diff --git a/libs/contrib/Control/Algebra.idr b/libs/contrib/Control/Algebra.idr
@@ -1,7 +1,7 @@
 module Control.Algebra
 
-infixl 6 <->
-infixl 7 <.>
+export infixl 6 <->
+export infixl 7 <.>
 
 public export
 interface Semigroup ty => SemigroupV ty where

diff --git a/libs/contrib/Control/Arrow.idr b/libs/contrib/Control/Arrow.idr
@@ -5,11 +5,11 @@ import Data.Either
 import Data.Morphisms
 
 
-infixr 5 <++>
-infixr 3 ***
-infixr 3 &&&
-infixr 2 +++
-infixr 2 \|/
+export infixr 5 <++>
+export infixr 3 ***
+export infixr 3 &&&
+export infixr 2 +++
+export infixr 2 \|/
 
 public export
 interface Category arr => Arrow (0 arr : Type -> Type -> Type) where

diff --git a/libs/contrib/Control/Category.idr b/libs/contrib/Control/Category.idr
@@ -20,7 +20,7 @@ Monad m => Category (Kleislimorphism m) where
   id                        = Kleisli (pure . id)
   (Kleisli f) . (Kleisli g) = Kleisli $ \a => g a >>= f
 
-infixr 1 >>>
+export infixr 1 >>>
 
 public export
 (>>>) : Category cat => cat a b -> cat b c -> cat a c

diff --git a/libs/contrib/Control/Validation.idr b/libs/contrib/Control/Validation.idr
@@ -96,7 +96,7 @@ export
 fail : Applicative m => String -> ValidatorT m a b
 fail s = MkValidator $ \_ => left s
 
-infixl 2 >>>
+export infixl 2 >>>
 
 ||| Compose two validators so that the second validates the output of the first.
 export

diff --git a/libs/contrib/Data/List/Alternating.idr b/libs/contrib/Data/List/Alternating.idr
@@ -3,8 +3,8 @@ module Data.List.Alternating
 import Data.Bifoldable
 import Data.List
 
-infixl 5 +>
-infixr 5 <+
+export infixl 5 +>
+export infixr 5 <+
 
 %default total
 

diff --git a/libs/contrib/Data/Monoid/Exponentiation.idr b/libs/contrib/Data/Monoid/Exponentiation.idr
@@ -23,7 +23,7 @@ public export
 modular : Monoid a => a -> Nat -> a
 modular v n = modularRec v (halfRec n)
 
-infixr 10 ^
+export infixr 10 ^
 public export
 (^) : Num a => a -> Nat -> a
 (^) = modular @{Multiplicative}

diff --git a/libs/contrib/Data/Seq/Internal.idr b/libs/contrib/Data/Seq/Internal.idr
@@ -342,7 +342,7 @@ viewRTree (Deep s pr m (Four w x y z)) =
 
 
 -- Construction
-infixr 5 `consTree`
+export infixr 5 `consTree`
 export
 consTree : Sized e => (r : e) -> FingerTree e -> FingerTree e
 a `consTree` Empty                       = Single a
@@ -352,7 +352,7 @@ a `consTree` Deep s (Two b c) st d2      = Deep (size a + s) (Three a b c) st d2
 a `consTree` Deep s (Three b c d) st d2  = Deep (size a + s) (Four a b c d) st d2
 a `consTree` Deep s (Four b c d f) st d2 = Deep (size a + s) (Two a b) (node3 c d f `consTree` st) d2
 
-infixl 5 `snocTree`
+export infixl 5 `snocTree`
 export
 snocTree : Sized e => FingerTree e -> (r : e) -> FingerTree e
 Empty `snocTree` a                       = Single a

diff --git a/libs/contrib/Data/Seq/Sized.idr b/libs/contrib/Data/Seq/Sized.idr
@@ -48,13 +48,13 @@ export
 reverse : Seq n a -> Seq n a
 reverse (MkSeq tr) = MkSeq (reverseTree id tr)
 
-infixr 5 `cons`
+export infixr 5 `cons`
 ||| O(1). Add an element to the left end of a sequence.
 export
 cons : e -> Seq n e -> Seq (S n) e
 a `cons` MkSeq tr = MkSeq (MkElem a `consTree` tr)
 
-infixl 5 `snoc`
+export infixl 5 `snoc`
 ||| O(1). Add an element to the right end of a sequence.
 export
 snoc : Seq n e -> e -> Seq (S n) e

diff --git a/libs/contrib/Data/Seq/Unsized.idr b/libs/contrib/Data/Seq/Unsized.idr
@@ -40,13 +40,13 @@ export
 reverse : Seq a -> Seq a
 reverse (MkSeq tr) = MkSeq (reverseTree id tr)
 
-infixr 5 `cons`
+export infixr 5 `cons`
 ||| O(1). Add an element to the left end of a sequence.
 export
 cons : e -> Seq e -> Seq e
 a `cons` MkSeq tr = MkSeq (MkElem a `consTree` tr)
 
-infixl 5 `snoc`
+export infixl 5 `snoc`
 ||| O(1). Add an element to the right end of a sequence.
 export
 snoc : Seq e -> e -> Seq e

diff --git a/libs/contrib/Data/String/Extra.idr b/libs/contrib/Data/String/Extra.idr
@@ -5,8 +5,8 @@ import Data.String
 
 %default total
 
-infixl 5 +>
-infixr 5 <+
+export infixl 5 +>
+export infixr 5 <+
 
 ||| Adds a character to the end of the specified string.
 |||

diff --git a/libs/contrib/Data/String/Parser.idr b/libs/contrib/Data/String/Parser.idr
@@ -106,7 +106,7 @@ export
                                 Fail i _ => Fail i msg)
                             (p.runParser s)
 
-infixl 0 <?>
+export infixl 0 <?>
 
 ||| Discards the result of a parser
 export

diff --git a/libs/contrib/Data/Telescope/Segment.idr b/libs/contrib/Data/Telescope/Segment.idr
@@ -59,7 +59,7 @@ toTelescope seg = untabulate seg ()
 
 %name Segment delta,delta',delta1,delta2
 
-infixl 3 |++, :++
+export infixl 3 |++, :++
 
 ||| This lemma comes up all the time when mixing induction on Nat with
 ||| indexing modulo addition.  An alternative is to use something like
@@ -141,7 +141,7 @@ projection {n = S n} {delta = ty :: delta} env
                     $ rewrite succLemma n k in env
     in env'
 
-infixl 4 .=
+export infixl 4 .=
 
 public export
 data Environment : (env : Left.Environment gamma)

diff --git a/libs/contrib/Data/Telescope/Telescope.idr b/libs/contrib/Data/Telescope/Telescope.idr
@@ -30,8 +30,8 @@ plusAccZeroRightNeutral m =
   Refl
 
 
-infixl 4 -.
-infixr 4 .-
+export infixl 4 -.
+export infixr 4 .-
 
 namespace Left
 
@@ -158,7 +158,7 @@ namespace Right
 
 namespace Tree
 
-  infixl 4 ><
+  export infixl 4 ><
 
   mutual
     ||| A tree of dependent types
@@ -189,14 +189,14 @@ namespace Tree
          (transpL env1 ** snd (concat (delta (transpL env1))) env2)
     )
 
-infix 5 <++>
+export infix 5 <++>
 
 public export
 (<++>) : (gamma : Left.Telescope m) -> (Environment gamma -> Right.Telescope n) -> Right.Telescope (plusAcc m n)
 [] <++> delta = delta ()
 (gamma -. sigma ) <++> delta = gamma <++> (\ env => sigma env .- \ v => delta (env ** v))
 
-infix 5 >++<
+export infix 5 >++<
 
 (>++<) : {m, n : Nat} -> (gamma : Right.Telescope m) -> (Environment gamma -> Left.Telescope n) ->
          Left.Telescope (plusAcc m n)

diff --git a/libs/contrib/Syntax/WithProof.idr b/libs/contrib/Syntax/WithProof.idr
@@ -1,6 +1,6 @@
 module Syntax.WithProof
 
-prefix 10 @@
+export prefix 10 @@
 
 ||| Until Idris2 supports the 'with (...) proof p' construct, here's a
 ||| poor-man's replacement.

diff --git a/libs/contrib/System/Path.idr b/libs/contrib/System/Path.idr
@@ -13,8 +13,8 @@ import Text.Quantity
 
 import System.Info
 
-infixl 5 </>, />
-infixr 7 <.>
+export infixl 5 </>, />
+export infixr 7 <.>
 
 
 ||| The character that separates directories in the path.

diff --git a/libs/contrib/Text/Parser/Core.idr b/libs/contrib/Text/Parser/Core.idr
@@ -128,7 +128,7 @@ export %inline
         Grammar state tok (c1 && c2) ty
 (<|>) = Alt
 
-infixr 2 <||>
+export infixr 2 <||>
 ||| Take the tagged disjunction of two grammars. If both consume, the
 ||| combination is guaranteed to consume.
 export

diff --git a/libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr b/libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr
@@ -122,7 +122,7 @@ export
 fill : Int -> Doc ann -> Doc ann
 fill n doc = width doc (\w => spaces $ n - w)
 
-infixr 6 <++>
+export infixr 6 <++>
 ||| Concatenates two documents with a space in between.
 export
 (<++>) : Doc ann -> Doc ann -> Doc ann

diff --git a/libs/linear/Data/Linear/Copies.idr b/libs/linear/Data/Linear/Copies.idr
@@ -6,7 +6,7 @@ import Data.Nat
 
 %default total
 
-infix 1 `Copies`
+export infix 1 `Copies`
 
 ||| Carries multiple linear copies of the same value. Usage: m `Copies` x
 ||| reads as "m copies of value x". This data structure is necessary to implement

diff --git a/libs/linear/Data/Linear/Interface.idr b/libs/linear/Data/Linear/Interface.idr
@@ -35,7 +35,7 @@ Consumable Int where
 
 -- But crucially we don't have `Consumable World` or `Consumable Handle`.
 
-infixr 5 `seq`
+export infixr 5 `seq`
 ||| We can sequentially compose a computation returning a value that is
 ||| consumable with another computation. This is done by first consuming
 ||| the result of the first computation and then returning the second one.

diff --git a/libs/linear/Data/Linear/Notation.idr b/libs/linear/Data/Linear/Notation.idr
@@ -2,7 +2,7 @@ module Data.Linear.Notation
 
 %default total
 
-infixr 0 -@
+export infixr 0 -@
 ||| Infix notation for linear implication
 public export
 (-@) : Type -> Type -> Type
@@ -18,7 +18,7 @@ public export
 (.) : (b -@ c) -@ (a -@ b) -@ (a -@ c)
 (.) f g v = f (g v)
 
-prefix 5 !*
+export prefix 5 !*
 ||| Prefix notation for the linear unrestricted modality
 public export
 record (!*) (a : Type) where

diff --git a/libs/papers/Data/Description/Regular.idr b/libs/papers/Data/Description/Regular.idr
@@ -88,7 +88,7 @@ Memo (Const s prop) x b = (v : s) -> b v
 Memo (d1 * d2) x b = Memo d1 x $ \ v1 => Memo d2 x $ \ v2 => b (v1, v2)
 Memo (d1 + d2) x b = (Memo d1 x (b . Left), Memo d2 x (b . Right))
 
-infixr 0 ~>
+export infixr 0 ~>
 
 ||| A memo trie is a coinductive structure
 export