[Agda] nontermination and Sized types

[Nils Anders Danielsson]

On 2020-10-03 09:33, vlad wrote:
> IMO this bug and others (incompatibility of sized types with equality,
> ...) should be better documented.

It might be possible to fix the problems with sized types (see
https://github.com/agda/agda/issues/2820), but I'm not aware of anyone
that is working on that at the moment. I think we'll make --sized-types
incompatible with --safe:

   Add --safe-except-for-sized-types?
   https://github.com/agda/agda/issues/4908

-- 
/NAD