Prevent (or support) induction recursion

[flupe]

I was hoping that funMutuals, dataMutuals and recMutuals would be enough to detect and prevent induction recursion.

But it looks like when doing induction-recursion, the function defined over the datatype doesn't appear in dataMutuals (even if used inside the datatype constructors' types). Likewise, the datatype doesn't appear in funMutuals. This means we currently accept code that produces weird-looking typed λ□.

So the big problem is figuring out when induction-recursion is happening, i.e being able to know the names in a mutual block consistently.

Two ways to investigate:

• Detect when we require a definition that has already been compiled. This situation means that it's impossible to reach a valid global environment. This can happen when Agda tries to compile the function before the datatype. But that's not very nice, because we don't have a lot of information on what went wrong.

• Figure out how to use MutualId to hopefully find some information about the whole mutual block (not just funMutuals and dataPars that are disjoint)