Remove as many uses of Sized Types as possible

[JacquesCarette]

As we know this is unsound, we should not be using that feature. The uses that are most worthy of adapting (after #3025 's fix of Data.Tree.Rose) would be

• Data.Trie
• Data.Container

Data.Nat.PseudoRandom.LCG.Unsafe also uses these, but since it's unsafe, I am less concerned. I would want to remove all of Codata.Sized.*.

The reasoning is simple: we should not use known unsound features, especially some where there are no known plans to fix them.

[jamesmckinna]

Thankfully, #3025 was relatively 'easy' because the explicit mutual recursion needed to side-step the original use of sized types was fairly orthodox, and moreover could be encapsulated (largely) to avoid having to be mutual; subsidiary auxiliary recursions sufficed.

I'm not across what's needed for the two other candidates you identify, though.

But the general message is clear and correct!

Modulo: in the absence of any settled story about all the various approaches to Codata, I'd be happy/happier leaving a large fossil record of unsafe modules, because while the library should be

• safe
• usable in particular streamlined wrt avoiding too much accumulated cruft/legacy code

I think it should nevertheless also retain material which shows a range of 'ways you could tackle implementing something' for external projects/users. Otherwise, such 'failed'/'unsafe' experiments get lost in the history? Unless we take care to carefully document a summary CHANGELOG for the various releases describing the highlights (what else?) that would allow future developers to find such material?

[gallais]

I agree with James; the guardedness method forces us to use a deeply embedded DSL to build
even basic bisimulation proofs and that really does not feel like a good state of the art.
A large fossil record waving in the direction of a more compositional approach is very important IMO.

I believe they're also just more pleasant to use for programming in anger in which case the
unsoundness is less of a worry (I had an experiment with sized IO and it is so much more usable
than the guarded version we have in the stdlib...).

[JacquesCarette]

Great, we seem to have reached a conclusion: let's not do this!

[jamesmckinna]

But that said: it was good (never mind intellectually satisfying...) to pick off #3025 .
Full marks to @Taneb and @gallais for nerd-sniping me on that one!