Split out modules needing guardedness #1509
Description
We are now getting errors like
Importing module Data.Container.Indexed.FreeMonad using the
--guardedness flag from a module which does not.
when scope checking the declaration
open import Data.Container.Indexed.FreeMonad using (_⋆C_)
I suppose I should not need to turn on --guardedness unless I want to use the M type.
Thus, we need to split out modules using --guardedness like we do with module using --with-K.
Or maybe we shouldn't push such a backwards-incompatible restrictions into the release last minute, @jespercockx ...
On the long run, we want --guardedness to be infective, so we need to refactor, but we would have more time and quiet after the release.