General inductive parameters

[janmasrovira]

• Depends on Interleave arity and typechecking #2481

This pr allows inductive type parameters to be any type. Until now, they had to be exactly Type. This allows us to define more general traits such as the Monad and Functor, as shown in the new test.
This is only supported under the temporary --new-typechecker flag.

Pending work:

Update the positivity checker if necessary (@jonaprieto).
Update the necessary compilation steps in Core (@lukaszcz).
Add compilation tests.

[jonaprieto]

Shortly, we can merge this PR since it does not replace the default typechecker. However, we need to address the positivity checker separately. I added two examples below to make it clear that there is an issue, although it is not straightforward to me at the moment how to solve it.

module NegativeEvil;

type Evil (f : Type -> Type) :=
  | magic : f (Evil f) -> Evil f;

First, the Evil data type is not strictly positive but it passes our checker, so we have an issue. Second, ignoring the positivity condition over the Evil definition for a moment, consider the rest of this program.

type Empty := mkEmpty {}; 

toEmpty (A : Type) : Type := A -> Empty;

panic : toEmpty (Evil toEmpty) 
  | x@(magic h) := h x ;

god : Empty := panic (magic panic); 

The above produces the following error,

The expression panic has type:
  Evil λ! {A := A → Empty} → Empty
but is expected to have type:
  _ (Evil _)

The message is a bit difficult to understand, at least to me, so we must fix it too.
Also, this should typecheck ignoring the positivity condition.

Similarly as with Evil, one could derive a term of Empty using for example, other types like:

type Free (f : Type -> Type) (A : Type)
 : Type :=
| Leaf : A -> Free f A
| Branch : f (Free f A) -> Free f A;

We can include these examples in a future PR fixing the pos. checker.

@rokopt could get benefit of being able to typecheck this Free data type, isn't it?
your BT A could be expressed as Free (\ {T := Prod T T}) A, or similar I'd say.

[rokopt]

@rokopt could get benefit of being able to typecheck this Free data type, isn't it? your BT A could be expressed as Free (\ {T := Prod T T}) A, or similar I'd say.

Yes, that's right!