Cannot set OPTION pragmas --allow-unsolved-metas
--no-positivity-check --no-termination-check --no-coverage-check
--type-in-type --sized-types --injective-type-constructors
--guardedness-preserving-type-constructors
--experimental-irrelevance with safe flag.