Idris allows very dependent types

[Tasiro]

This is essentially the same issue as in Agda (see https://github.com/agda/agda/issues/1556).

Very dependent types allow an indexed type to use itself as an index. It can be quite useful, but may not be safe. I therefore expect Idris to reject the following:

mutual
    A: Type
    A = D AA

    data D: A -> Type where
        DD: D AA

    AA: A
    AA = DD

This may also be the reason that the following causes Idris to loop (and eat up my memory):

mutual
    B: Type
    B = C B
    data C: Type -> Type where
        CC: C B

[gallais]

B = C B

This is straight up an infinite loop.

[Tasiro]

And it is caught in

mutual
    B: Type
    data C: Type -> Type where
        CC: C B
    B = C B