[Agda] termination by contradiction

[Sergei Meshveliani]

On Wed, 2014-07-02 at 18:00 +0200, Ulf Norell wrote:
> 
> [..]


>         > For instance,
>         >
>         > False : ℕ → Set
>         > False _ = ⊥
>         >
>         > decFalse : Decidable False
>         > decFalse _ = no (λ x → x)
>         >
>         > loopy : ¬ (∀ n → ¬ False n) → Σ ℕ False
>         > loopy H = findNatByContra False decFalse H
>         >
>         >
>         > Here, loopy will happily evaluate forever with the
>         hypothetical
>         > (classical) proof that there is a number satisfying False.
>         There > is no need to evaluate under the case since decFalse
>         comes back > 'no' for any number.
>         
>         
>         Can you, please, explain further?
>         
>         To apply  (loopy H),  one needs to provide
>                                            H : (∀ n → ¬ False n) → ⊥.
>         
>         And this is not possible, because its type normalizes to
>         
>         ((n : ℕ) → (False n → ⊥)) → ⊥,  and to  ((n : ℕ) → (⊥ → ⊥)) →
>         ⊥,
>         
>         and the type  (n : ℕ) → (⊥ → ⊥)  has a value  (\n → id)  in
>         it.
>         
>         
>         As one cannot provide any argument value to `loopy',  how can
>         it
>         evaluate forever?
> 
> 
> The problem is that in Agda programs need to terminate not only at
> run-time when you apply them to actual arguments, but also at type
> checking-time when the type checker runs programs to check for
> equality. For instance, suppose you define loopy as above and then try
> to prove that loopy always returns 42
> 
> 
> thm : (H : ¬ (∀ n → ¬ False n)) → proj₁ (loopy H) ≡ 42
> thm _ = refl
> 
> 
> In this case the type checker needs to evaluate loopy in the context
> of the
> free variable H to check if it normalises to 42. This evaluation will
> not terminate
> with your definition of findNatByContra.
> 

But  thm  is useless, because the type for its first argument is empty.
I hope, I can provide examples of practically usable programs which
apply  findNatByContra.

1) But can `loopy' be introduced other than by a mistake?
   Is there an example of a practically usable program which also uses  
   `loopy' ?  

2) Suppose one introduces `loopy' by a mistake, and sets its various
invocations, also by a mistake. What can happen then, in the worst case?
Probably, the type checker will loop forever, and the user will
interrupt the process of checking (as I did 10 minutes ago!).
This will not make the whole usage worse, because there are many other
ways in Agda to make the checker loop forever.

Am I missing something?

Regards,

------
Sergei