[Agda] Self-containing inductive-recursive definitions

[Dan Doel]

Greetings,

I was reading the recent Forsberg and Setzer paper* on inductive-inductive 
definitions, and they made a note that you could write definitions of that 
form in Agda which contain codes for the type being defined. However, this is 
currently no different than Agda's implementation of induction-recursion:

  mutual
    data U : Set where
      u : U
      x : (s : U) -> T s -> U

    T : U -> Set
    T u       = U
    T (x s y) = Σ (T s) (\z -> z == y)

Conor McBride confirmed for me that this definition would not be expressible 
in the more formal treatments of induction-recursion (by Dybjer and Setzer*, 
say). The positivity checker rules out some obviously bad variations of the 
above, like if we try to add pi types to the universe:

  pi : (s : U) -> (T s -> U) -> U

we could obtain:

  pi u : (U -> U) -> U

which is correctly rejected. However, informally, even the first definition 
above is bad, because the mutual definition plays on T being able to be 
defined for 'the elements of U constructed thus far', while U as a whole is 
not defined within the definition. More formally (Conor again informs me), the 
problem is that the functor for the above definition refers to its own initial 
algebra.

I don't have an example where this sort of thing leads to a proof of false; at 
a guess, you probably can't do anything really terrible unless the positivity 
checker is off. But, is this cause for concern anyhow? Should it be 
disallowed? I'm not sure if this warrants filing an issue in the bug tracker, 
so I thought I'd ask for opinions here first.

Cheers,
-- Dan

[1] http://cs.swan.ac.uk/~csfnf/papers/indind_csl2010.pdf
[2] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.9.2863