[Agda] with - refl strangeness

[Sergei Meshveliani]

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