# [Agda] with - refl strangeness

Sergei Meshveliani mechvel at botik.ru
Sun Jun 2 20:12:48 CEST 2013

```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
------------------------------------------------------------------------

```