[Agda] Normalisation before termination checking

[Nils Anders Danielsson]

Hi,

I suggest that right-hand sides should be normalised before the
termination checker is run (with the defined names treated as neutral,
of course). This is not very important in the inductive case, but for
coinductive definitions my impression is that it would really improve
modularity and abstraction.

One drawback might be that typechecking becomes considerably slower.
Currently there are two termination checking passes. The first one
does not include dotted arguments, whereas the second does, and the
second one is only run if the first one fails. I suggest that
normalisation is only performed in the second pass.

Are there any other drawbacks that I have missed? I suspect that it is
very easy to implement this change.

-- 
/NAD