[Agda] agda halting problem

[Dan Doel]

On Thu, Jul 5, 2012 at 12:07 PM, Daniel Peebles <pumpkingod at gmail.com> wrote:
> I don't think there's an easy way to check. Not-obviously-terminating
> definitions will get marked in pink if typechecking completes, but if you go
> and use one directly in a type somewhere and the definition really doesn't
> terminate on the input in the type, then the typechecker won't terminate. So
> if you use possibly non-terminating functions in types, you might want to
> split up your file to make sure nothing that would normally be pink is
> hanging your typechecker.

Although I don't run into this often, it is kind of unfortunate. Have
any of the implementors considered a flag that would make type
checking fail if a type contains something rejected by the termination
checker? Is that even possible at present (i.e. are type and
termination checking interleaved)?

-- Dan