[Agda] irrelevant arg example

[Sergei Meshveliani]

On Wed, 2014-08-20 at 17:56 +0200, Ulf Norell wrote:
> I'm not sure what the different behaviour you are getting is (can you
> elaborate?), but f can be implemented as follows:
> 
> 
> ⊥-elim-irr : .⊥ → ∀ {a} {A : Set a} → A
> ⊥-elim-irr ()
> 
> 
> f : (x : ℕ) → .(nz : x ≢ 0) → x ≢ 0
> 
> f x nz z = ⊥-elim-irr (nz z)
> 
> 
> Under normal circumstances irrelevant things cannot be used in
> relevant contexts, but one exception is that you are allowed absurd
> elimination of irrelevant empty types into relevant types.
> 

Consider the example:

  record Foo (b : ℕ) (nzb : b ≢ 0) : Set where
                                         field foo : ℕ
  g : (x : ℕ) → .(nz : x ≢ 0) → ℕ
  g x _ = x + x

  f : (x : ℕ) → .(nz : x ≢ 0) → Foo x nz
  f x nz =  record { foo = g x nz }

In what contexts  "Foo x nz"  and  "g x nz"  are using  nz, 
in relevant contexts?

Agda of  August 19 2014  reports of an irrelevant  nz  wrongly used in
Foo x nz.
(Foo x _)  is said an "unsolved metas".
Is this possible to fix the implementation for  f  without changing the
above signatures? 

Agda-2.4.0.2  treated such examples in a different way. It type-checked
them, may be, after changing some occurrences of  nz  to  _. 

I suspect that I am forced to add a dot to  Foo :

  record Foo (b : ℕ) .(nzb : b ≢ 0)  ...

Which Agda is more correct at this point?


General consideration
--------------------- 
(1) In classical algorithmic mathematics, the conditions like the above 
x ≢ 0  need in most cases to be irrelevant: the result of the client
function does not depend on the way in which the condition is verified.

(2) On the other hand, Agda has proofs as data, and claims that it is
often nice to process a proof data to evaluate the value of a function.
For example, this is natural to process proofs in a provable function
for sorting a list (can this be implemented in other way?).

These two lines contradict each other. So that  
a) I doubt about using irrelevant patterns, 
b) on the other hand, not using them is likely to cause many additional
lengthy proofs about independence of the result on the condition
witness.

Meanwhile, I try this approach: 
to use irrelevant arguments everywhere where the type checker rejects
the proof due to seeing two witnesses in the scope for the condition. 
I doubt where this will lead me.
Also there is a question about Standard library.

Regards,

------
Sergei