[Agda] with - refl strangeness

[Dominique Devriese]

The problem is related to with-matches.  Where you write IRefl in the
RHS of foRef, you are expected to produce a value of type s =fo s for
some s.  But this type does not reduce to "Foo.list s =l Foo.list s"
as you seem to expect.   It reduces to "s =fo s | Foo.list s", in
essence a call to an anonymous function with the scrutinee of =fo's
with-block as an extra argument (Agda actually generates this
anonymous function internally when you write a with-block).  Because
"Foo.list s" is not known to be equal to one of the cases of the
with-block, this doesn't reduce and that's your error.  You can try to
make it reduce further by using a with-block on "Foo.list s" in
foRefl, but then you get a different problem. You could use the
inspect-pattern to solve that other problem, but it seems much better
to just move to your cleaner alternative III.  Another alternative
(the most obvious one) is "s =fo s' = Foo.list s =l Foo.list s'".

Regards,
Dominique

2013/6/2 Sergei Meshveliani <mechvel at botik.ru>:
> Please, what is wrong in the below program?
>
> This is on equality on natural lists wrapped to the record Foo.
>
> The below variants (II) and (III) are type-checked (when un-commented),
>
> and for (I) it reports for the line of  foRefl
>
>
> Thanks,
>
> ------
> Sergei
>
>
> ----------
> ListPoint.Rel (Setoid._≈_ nSetoid) _x_34 _x_34 !=<
> .x =fo .x | Foo.list .x of type Set
> when checking that the expression lRefl has type
> .x =fo .x | Foo.list .x
> -----------
>
> ------------------------------------------------------------------
> open import Level    using ()  renaming (zero to 0L)
> open import Function using (_$_; _on_)
> open import Relation.Binary using
>      (Rel; IsEquivalence; module IsEquivalence; Setoid; module Setoid;
>       DecSetoid; module DecSetoid; module DecTotalOrder; IsDecTotalOrder
>      )
> open import Relation.Binary.Core using
>                                  (Reflexive; Symmetric; Transitive)
> open import Data.Nat as Nat using (ℕ; _<_) renaming
>                                            (decTotalOrder to natDTO)
> open import Data.List as Ls using (List; []; _∷_)
> open import Relation.Binary.List.Pointwise as ListPoint using()
>                                          renaming (setoid to listSetoid)
>
>
> nDecSetoid = DecTotalOrder.Eq.decSetoid natDTO
> nSetoid    = DecSetoid.setoid nDecSetoid
>
> lSetoid = listSetoid nSetoid            -- for  List ℕ
> lEquiv  = Setoid.isEquivalence lSetoid
> open Setoid lSetoid using () renaming (_≈_ to _=l_)
> open IsEquivalence lEquiv renaming
>                           (refl to lRefl; sym to lSym; trans to lTrans)
>
> record Foo : Set where
>                  field  list : List ℕ
>
> _=fo_ : Rel Foo 0L
> s =fo s'  with  Foo.list s
>
> ... | []     =  []       =l Foo.list s'  -- (I)
> ... | x ∷ xs =  (x ∷ xs) =l Foo.list s'
>
> -- ... | xs =  xs =l Foo.list s'         -- (II)
>
> -- _=fo_ =  _=l_ on Foo.list             -- (III)
>
> foRefl : Reflexive _=fo_
> foRefl = lRefl
> ------------------------------------------------------------------------
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda