[Agda] Identifying experimental Agda features for Cabal support

[Darin Morrison]

Hi All,

I'd like to revive the discussion started at AIM 10 about which
features should be enabled by default in Agda and which should be
marked as experimental or as language extensions.

I think it's important to reach a consensus about this soon so that I
can add support for enabling/disabling these features in the Agda
cabal support, which I'm hoping can make it into the next Cabal/GHC
release (coming up in the next few weeks as I understand).

To get the discussion started, a quick proposal of language extensions
might look like the following:

Coinduction
InductiveFamilies
InductionRecursion
SizedTypes
UniversePolymorphism

One might also want to include options to disable various checks:

NoPositivityCheck
NoTerminationCheck
TypeInType

although maybe the latter shouldn't receive special treatment and
should just be specified as extra command line options.  Conceptually,
I don't think they are really language extensions so much as compiler
options.

I'm of the opinion that it would be best to start off as conservative
as possible regarding which features are defaulted so that people
really know what they are getting when they use an Agda package from
someone else.  Also, it's a lot easier to start off conservative and
change things later than the other way around once a large number of
packages have already been written.

Thoughts?

--
Darin