[Agda] question on irrelevant argument

[Sergei Meshveliani]

On Sun, 2014-01-19 at 15:26 +0100, Ulf Norell wrote:
> You can define an irrelevant version of ⊥-elim which you can use in
> foo2 and foo3:
> 
> 
> ⊥-elim-irr : .(x : ⊥) → ∀ {a}{A : Set a} → A
> ⊥-elim-irr ()
> 

Thank you.

I tried several attempts with this. Finally I discover that this one is
type-checked:

  foo2 : (m n : ℕ) → .(nz : n ≢ zero) → ℕ
  foo2 _ (suc n) _  =  n
  foo2 _ zero    nz =  ⊥-elim-irr (nz PE.refl)

Generally, there are many situations in which I can write a type-checked
Agda program only by a lucky occasion. 

Thus, I tried in this example

        foo2 _ zero _ =  ⊥-elim-irr ({!!} PE.refl)

under emacs, and   C-c C-a.  This does not help!
I tried 
        foo2 _ zero    _  =  ⊥-elim-irr {!!}

This occurs lucky. Here  C-c C-a  shows  "(.nz PE.refl)"  -- some hint.

It is not still type checked! Then I change here  ".nz"  to  "nz" :
"Not in scope:  nz".

Then I replace there  "_ ="  with  "nz _ =".

I expected that it will report that  nz  declared as irrelevant and
cannot be used this way.
But it is type-checked!
-- unlike with  ⊥-elim.

Regards,

--------
Sergei


> 
> 
> On Sun, Jan 19, 2014 at 2:50 PM, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>         Please,
>         how to fix  foo2, foo3  shown below?
>         
>         ----------------------------------------------------------------
>         open import Relation.Binary.PropositionalEquality as PE using
>         (_≡_; _≢_)
>         open import Data.Empty using (⊥-elim)
>         open import Data.Nat   using (ℕ; module ℕ)
>         
>         open ℕ
>         
>         foo : (m n : ℕ) → n ≢ zero → ℕ             -- this works
>         foo _ (suc n) _  =  n
>         foo _ zero    nz =  ⊥-elim (nz PE.refl)
>         
>         
>         foo2 : (m n : ℕ) → .(n ≢ zero) → ℕ
>         foo2 _ (suc n) _ =  n
>         foo2 _ zero    _ =  ⊥-elim (u PE.refl)     -- is not
>         type-checked
>                             where
>                             u : zero ≢ zero
>                             u = _
>         {-
>         foo3 : (m n : ℕ) → .{nz : n ≢ zero} → ℕ
>         foo3 _ (suc n) {_} =  n
>         foo3 _ zero    {_} =  ⊥-elim (u PE.refl)      -- is not
>         type-checked
>                               where
>                               u : zero ≢ zero
>                               u = {!!}
>         -}
>         ---------------------------------------------------------------------
>         
>         The checker   (of  development Agda of January 8, 2014)
>         
>         does not allow to skip the `zero' branch, nor to set () there,
>         nor to apply  ⊥-elim
>         (nz  is rejected for  u,  as well as '_').
>         
>         Thanks,
>         
>         ------
>         Sergei
>         
>         _______________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se
>         https://lists.chalmers.se/mailman/listinfo/agda
> 
>