Sized types will no longer be safe in 2.6.2 (#1465)

* Sized types will no longer be safe in 2.6.2

* Add removal of --safe from modules using sized types to changelog

* Split out `stream` into `Data.Nat.PseudoRandom.LCG.Unsafe`

Co-authored-by: = <[email protected]>

Author: jespercockx

CHANGELOG.md

@@ -64,6 +64,17 @@ Non-backwards compatible changes
     and `Reflection.Argument.Quantity`. The constructors of the types
     `Modality` and `Quantity` are reexported from `Reflection`.
 
+#### Sized types
+
+* Sized types are no longer considered safe in Agda 2.6.2. As a
+  result, all modules that use `--sized-types` no longer have the
+  `--safe` flag.  For a full list of affected modules, refer to the
+  relevant [commit](https://github.com/agda/agda-stdlib/pull/1465/files#diff-e1c0e3196e4cea6ff808f5d2906031a7657130e10181516206647b83c7014584R91-R131.)
+
+* In order to keep `Data.Nat.Pseudorandom.LCG` safe, the function
+  `stream` that relies on the newly unsafe `Codata` modules has
+  been moved to the new module `Data.Nat.Pseudorandom.LCG.Unsafe`.
+
 #### Other
 
 * `Data.Maybe.Base` now re-exports the definition of `Maybe` given by

GenerateEverything.hs

@@ -59,7 +59,7 @@ unsafeModules = map modToFile
   , "System.Exit.Primitive"
   , "Text.Pretty.Core"
   , "Text.Pretty"
-  ]
+  ] ++ sizedTypesModules
 
 isUnsafeModule :: FilePath -> Bool
 isUnsafeModule fp =
@@ -98,6 +98,55 @@ isWithKModule =
   \ fp -> unqualifiedModuleName fp == "WithK"
        || fp `elem` withKModules
 
+sizedTypesModules :: [FilePath]
+sizedTypesModules = map modToFile
+  [ "Codata.Cofin"
+  , "Codata.Cofin.Literals"
+  , "Codata.Colist"
+  , "Codata.Colist.Bisimilarity"
+  , "Codata.Colist.Categorical"
+  , "Codata.Colist.Properties"
+  , "Codata.Conat"
+  , "Codata.Conat.Bisimilarity"
+  , "Codata.Conat.Literals"
+  , "Codata.Conat.Properties"
+  , "Codata.Covec"
+  , "Codata.Covec.Bisimilarity"
+  , "Codata.Covec.Categorical"
+  , "Codata.Covec.Instances"
+  , "Codata.Covec.Properties"
+  , "Codata.Cowriter"
+  , "Codata.Cowriter.Bisimilarity"
+  , "Codata.Delay"
+  , "Codata.Delay.Bisimilarity"
+  , "Codata.Delay.Categorical"
+  , "Codata.Delay.Properties"
+  , "Codata.M"
+  , "Codata.M.Bisimilarity"
+  , "Codata.M.Properties"
+  , "Codata.Stream"
+  , "Codata.Stream.Bisimilarity"
+  , "Codata.Stream.Categorical"
+  , "Codata.Stream.Instances"
+  , "Codata.Stream.Properties"
+  , "Codata.Thunk"
+  , "Data.Container"
+  , "Data.Container.Any"
+  , "Data.Container.FreeMonad"
+  , "Data.Nat.PseudoRandom.LCG.Unsafe"
+  , "Data.Tree.Rose"
+  , "Data.Tree.Rose.Properties"
+  , "Data.Trie"
+  , "Data.Trie.NonEmpty"
+  , "Relation.Unary.Sized"
+  , "Size"
+  , "Text.Tree.Linear"
+  ]
+
+isSizedTypesModule :: FilePath -> Bool
+isSizedTypesModule =
+  \ fp -> fp `elem` sizedTypesModules
+
 unqualifiedModuleName :: FilePath -> String
 unqualifiedModuleName = dropExtension . takeFileName
 
@@ -139,10 +188,9 @@ extractHeader mod = extract
                               , "Please see other existing files or consult HACKING.md."
                               ]
 
--- | A crude classifier looking for lines containing options & trying to guess
---   whether the safe file is using either @--guardedness@ or @--sized-types@
+-- | A crude classifier looking for lines containing options
 
-data Status = Deprecated | Unsafe | Safe | SafeGuardedness | SafeSizedTypes
+data Status = Deprecated | Unsafe | Safe
   deriving (Eq)
 
 classify :: FilePath -> [String] -> [String] -> Status
@@ -156,8 +204,6 @@ classify fp hd ls
   -- And then perform the actual classification
   | deprecated                = Deprecated
   | isUnsafe                  = Unsafe
-  | guardedness               = SafeGuardedness
-  | sizedtypes                = SafeSizedTypes
   | safe                      = Safe
   -- We know that @not (isUnsafe || safe)@, all cases are covered
   | otherwise                 = error "IMPOSSIBLE"
@@ -169,8 +215,6 @@ classify fp hd ls
     isUnsafe = isUnsafeModule fp
 
     -- based on detected OPTIONS
-    guardedness = option "--guardedness"
-    sizedtypes  = option "--sized-types"
     safe        = option "--safe"
     withK       = option "--with-K"
     withoutK    = option "--without-K"
@@ -223,9 +267,7 @@ checkFilePaths cat fps = forM_ fps $ \ fp -> do
 -- Collecting all non-Core library files, analysing them and generating
 -- 4 files:
 -- Everything.agda                 all the modules
--- EverythingSafe.agda             all the safe modules (may be incompatible)
--- EverythingSafeGuardedness.agda  all the safe modules using --guardedness
--- EverythingSafeSizedTypes.agda   all the safe modules using --sized-types
+-- EverythingSafe.agda             all the safe modules
 
 main = do
   args <- getArgs
@@ -254,27 +296,11 @@ main = do
 
   writeFileUTF8 (safeOutputFile ++ ".agda") $
     unlines [ header
-            , "{-# OPTIONS --guardedness --sized-types #-}\n"
+            , "{-# OPTIONS --safe --guardedness #-}\n"
             , mkModule safeOutputFile
             , format $ filter ((Unsafe /=) . status) libraryfiles
             ]
 
-  let safeGuardednessOutputFile = safeOutputFile ++ "Guardedness"
-  writeFileUTF8 (safeGuardednessOutputFile ++ ".agda") $
-    unlines [ header
-            , "{-# OPTIONS --safe --guardedness #-}\n"
-            , mkModule safeGuardednessOutputFile
-            , format $ filter ((SafeGuardedness ==) . status) libraryfiles
-            ]
-
-  let safeSizedTypesOutputFile = safeOutputFile ++ "SizedTypes"
-  writeFileUTF8 (safeSizedTypesOutputFile ++ ".agda") $
-    unlines [ header
-            , "{-# OPTIONS --safe --sized-types #-}\n"
-            , mkModule safeSizedTypesOutputFile
-            , format $ filter ((SafeSizedTypes ==) . status) libraryfiles
-            ]
-
 -- | Usage info.
 
 usage :: String

README/Data/Container/FreeMonad.agda

@@ -5,7 +5,7 @@
 -- used
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module README.Data.Container.FreeMonad where
 

README/Data/Tree/Rose.agda

@@ -4,7 +4,7 @@
 -- Some examples showing how the Rose tree module can be used
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module README.Data.Tree.Rose where
 

README/Data/Trie/NonDependent.agda

@@ -4,7 +4,7 @@
 -- Example use case for a trie: a wee generic lexer
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module README.Data.Trie.NonDependent where
 

src/Codata/Cofin.agda

@@ -4,7 +4,7 @@
 -- "Finite" sets indexed on coinductive "natural" numbers
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Cofin where
 

src/Codata/Cofin/Literals.agda

@@ -4,7 +4,7 @@
 -- Conat Literals
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Cofin.Literals where
 
@@ -20,4 +20,3 @@ number n = record
   { Constraint = λ k → True (suc k ℕ≤? n)
   ; fromNat    = λ n {{p}} → fromℕ< (toWitness p)
   }
-

src/Codata/Colist.agda

@@ -4,7 +4,7 @@
 -- The Colist type and some operations
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Colist where
 

src/Codata/Colist/Bisimilarity.agda

@@ -4,7 +4,7 @@
 -- Bisimilarity for Colists
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Colist.Bisimilarity where
 

src/Codata/Colist/Categorical.agda

@@ -4,7 +4,7 @@
 -- A categorical view of Colist
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Colist.Categorical where
 

src/Codata/Colist/Properties.agda

@@ -4,7 +4,7 @@
 -- Properties of operations on the Colist type
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Colist.Properties where
 

src/Codata/Conat.agda

@@ -4,7 +4,7 @@
 -- The Conat type and some operations
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Conat where
 

src/Codata/Conat/Bisimilarity.agda

@@ -4,7 +4,7 @@
 -- Bisimilarity for Conats
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Conat.Bisimilarity where
 

src/Codata/Conat/Literals.agda

@@ -4,7 +4,7 @@
 -- Conat Literals
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Conat.Literals where
 

src/Codata/Conat/Properties.agda

@@ -4,7 +4,7 @@
 -- Properties for Conats
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Conat.Properties where
 

src/Codata/Covec.agda

@@ -4,7 +4,7 @@
 -- The Covec type and some operations
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Covec where
 

src/Codata/Covec/Bisimilarity.agda

@@ -4,7 +4,7 @@
 -- Bisimilarity for Covecs
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Covec.Bisimilarity where
 

src/Codata/Covec/Categorical.agda

@@ -4,7 +4,7 @@
 -- A categorical view of Covec
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Covec.Categorical where
 

src/Codata/Covec/Instances.agda

@@ -4,7 +4,7 @@
 -- Typeclass instances for Covec
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Covec.Instances where
 

src/Codata/Covec/Properties.agda

@@ -4,7 +4,7 @@
 -- Properties of operations on the Covec type
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Covec.Properties where
 
@@ -29,4 +29,3 @@ module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where
  map-map-fusion : ∀ (f : A → B) (g : B → C) {m} as {i} → i , m ⊢ map g (map f as) ≈ map (g ∘ f) as
  map-map-fusion f g []       = []
  map-map-fusion f g (a ∷ as) = Eq.refl ∷ λ where .force → map-map-fusion f g (as .force)
-

src/Codata/Cowriter.agda

@@ -4,7 +4,7 @@
 -- The Cowriter type and some operations
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 -- Disabled to prevent warnings from BoundedVec
 {-# OPTIONS --warn=noUserWarning #-}

src/Codata/Cowriter/Bisimilarity.agda

@@ -4,7 +4,7 @@
 -- Bisimilarity for Cowriter
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Cowriter.Bisimilarity where
 

src/Codata/Delay.agda

@@ -4,7 +4,7 @@
 -- The Delay type and some operations
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Delay where
 

src/Codata/Delay/Bisimilarity.agda

@@ -4,7 +4,7 @@
 -- Bisimilarity for the Delay type
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Delay.Bisimilarity where
 

src/Codata/Delay/Categorical.agda

@@ -4,7 +4,7 @@
 -- A categorical view of Delay
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Delay.Categorical where
 

src/Codata/Delay/Properties.agda

@@ -4,7 +4,7 @@
 -- Properties of operations on the Delay type
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.Delay.Properties where
 

src/Codata/M.agda

@@ -4,7 +4,7 @@
 -- M-types (the dual of W-types)
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.M where
 

src/Codata/M/Bisimilarity.agda

@@ -4,7 +4,7 @@
 -- Bisimilarity for M-types
 ------------------------------------------------------------------------
 
-{-# OPTIONS --without-K --safe --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module Codata.M.Bisimilarity where