[Agda] agda halting problem

[Andreas Abel]

Termination checking happens only after type-checking.  This is a design 
flaw, and a long standing issue to be fixed.

   http://code.google.com/p/agda/issues/detail?id=42

It is in the back of my mind and should be implemented during the next 
major overhaul of the termination checker.

Cheers,
Andreas

On 05.07.12 7:50 PM, Dan Doel wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/