[Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1

[Sergei Meshveliani]

On Sat, 2018-05-19 at 15:33 -0500, Andrés Sicard-Ramírez wrote:
> Dear all,
> 
> The Agda Team is very pleased to announce the first release candidate
> of Agda 2.5.4. We plan to release 2.5.4 in one week.
> 
> [..]
> 
> Enjoy the RC and please test as much as possible.


Please, consider a small code attached.
This is a lemma about mapping the _⊆_ relation for lists over setoids:

  map⊆ : (f : C → C') → (f Preserves _≈_ ⟶ _≈'_) →
                                         (map f) Preserves _⊆_ ⟶ _⊆'_
 
In DoCon-A-2.02  (see there List.L0.agda)  a similar code works under
Agda-2.5.3.

To port to Agda 2.5.3.20180519, I change the import for the experimental
Standard library: 

 import Data.List.Membership.Setoid as Membership
 import Data.List.Relation.Sublist.Setoid as Sublist-Setoid
 import Data.List.Relation.Sublist.Propositional as Sublist-≡

And change the local import in  module CongMap0  to

  open Membership A       using (_∈_)
  open Sublist-Setoid A   using (_⊆_)
  open Membership A'      using () renaming (_∈_ to _∈'_)
  open Sublist-≡ {A = C'} using () renaming (_⊆_ to _⊆'_)   -- * 


Now, everything is type-checked there -- except this last function

  map⊆ : (f : C → C') → (f Preserves _≈_ ⟶ _≈'_) →
                                           (map f) Preserves _⊆_ ⟶ _⊆'_
  map⊆ f fCong {xs} {ys} xs⊆ys {z} z∈f-xs =
       let
         (x , x∈≡xs , fx≈z) = counter-map {A = C} {sd = A'} f z∈f-xs
         x∈xs    = ∈≡→∈ x∈≡xs
         x∈ys    = xs⊆ys x∈xs
         fx∈f-ys = map∈ f fCong x∈ys
       in
       cong₁∈' fx≈z fx∈f-ys

The report is
  β != β= of type Level
  when checking that the expression z∈f-xs has type
  _y_249 A A' f fCong xs⊆ys z∈f-xs ∈'
  map f (_xs_248 A A' f fCong xs⊆ys z∈f-xs)

I wonder whether
* this is a bug in the candidate Agda
* or an error in  List.L0.agda  (missed by Agda 2.5.3)
* or a wrong port.

Can you, please, help?

------
Sergei

-------------- next part --------------
module T where

open import Level    using (Level; _⊔_)
open import Function using (_∘_; _$_)  
open import Relation.Binary using (Rel; _Respects_; _Preserves_⟶_; Setoid) 
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≗_; refl;
                                                                         cong)
open import Data.Product  using (_×_; _,_; ∃)
open import Data.List     using (List; []; _∷_; map)
open import Data.List.Any using (Any)
open import Data.List.All using (All) renaming ([] to []a; _∷_ to _∷a_) 
import Data.List.All.Properties as AllProp using () 

import Data.List.Membership.Setoid as Membership 
import Data.List.Relation.Sublist.Setoid as Sublist-Setoid
import Data.List.Relation.Sublist.Propositional as Sublist-≡ 



--****************************************************************************
open Any 

module _ {α β β=} {A : Set α} {sd : Setoid β β=} 
  where 
  open Setoid sd using (_≈_) renaming (Carrier to B; sym to ≈sym)

  open Membership (PE.setoid A) using () renaming (_∈_ to _∈≡_) 
  open Membership sd using () renaming (_∈_ to _∈'_)

  counter-map : (f : A → B) → {xs : List A} → {y : B} →
                              y ∈' (map f xs) → ∃ \x → (x ∈≡ xs) × (f x ≈ y)
  counter-map _ {[]}     ()
  counter-map f {x ∷ xs} {y} (here y≈fx)      = (x , here refl , ≈sym y≈fx)
  counter-map f {x ∷ xs} {y} (there y∈map-xs) =
                        let
                           (x , x∈xs , fx≈y) = counter-map f {xs} {y} y∈map-xs
                        in (x , there x∈xs , fx≈y)


--============================================================================
module CongMap0 {α α= β β=} (A : Setoid α α=) (A' : Setoid β β=) 
  where 
  open Setoid A using (_≈_) 
                renaming (Carrier to C; reflexive to ≈reflexive; 
                          refl to ≈refl; sym to ≈sym; trans to ≈trans)
                         
  ≡setoid-C = PE.setoid C
  open Membership ≡setoid-C using () renaming (_∈_ to _∈≡_)

  open Setoid A' using () 
                 renaming (Carrier to C'; _≈_ to _≈'_; refl to ≈'refl; 
                                               sym to ≈'sym; trans to ≈'trans)
  open Membership A       using (_∈_) 
  open Sublist-Setoid A   using (_⊆_)
  open Membership A'      using () renaming (_∈_ to _∈'_)
  open Sublist-≡ {A = C'} using () renaming (_⊆_ to _⊆'_)

  ----------------------------------------------------------------------------
  CongruentOn2 :  ∀ {r} → (_~_ : Rel C r) → (C → C') → Set (r ⊔ β= ⊔ α= ⊔ α)
  CongruentOn2 _~_ f =
                     {x y : C} → x ~ y → x ≈ y → f x ≈' f y

  CongruentOn :  ∀ {p} → (C → Set p) → (C → C') → Set  (p ⊔ β= ⊔ α= ⊔ α)
  CongruentOn P =
                  CongruentOn2 (\x y → P x × P y)

  CongruentOnList :  List C → (C → C') → Set (β= ⊔ α= ⊔ α)
  CongruentOnList xs =
                       CongruentOn (_∈ xs)

  congruentOnTail :  ∀ {x xs} {f : C → C'} → CongruentOnList (x ∷ xs) f → 
                                             CongruentOnList xs f 
  congruentOnTail fCong-xxs (y∈xs , z∈xs) = 
                                           fCong-xxs (there y∈xs , there z∈xs)

  ----------------------------------------------------------------------------
  gen-map∈ :  {x : C} → {xs : List C} → (f : C → C') → 
                             (CongruentOnList xs f) → x ∈ xs → f x ∈' map f xs

  gen-map∈ {_} {_ ∷ _} _ fCong-yxs (here x≈y) =  here fx=fy
                                   where
                                   x∈yxs =  here x≈y
                                   y∈yxs =  here ≈refl
                                   fx=fy =  fCong-yxs (x∈yxs , y∈yxs) x≈y 

  gen-map∈ {x} {y ∷ xs} f fCong-yxs (there x∈xs) =  
                                    there $ gen-map∈ {x} {xs} f fCong-xs x∈xs
                                    where
                                    fCong-xs = congruentOnTail fCong-yxs 

  -- a specialization of gen-map 
  map∈ : (f : C → C')  → (f Preserves _≈_ ⟶ _≈'_) → {x : C} → 
         {xs : List C} → x ∈ xs                   → f x ∈' map f xs

  map∈ f fCong {x} {xs} =  gen-map∈ {x} {xs} f (\_ → fCong)

  ----------------------------------------------------------------------------
  private 
    ∈≡→∈ : ∀ {x xs} → x ∈≡ xs → x ∈ xs
    ∈≡→∈ {x} {y ∷ xs} (here x≡y)    =  here $ ≈reflexive x≡y 
    ∈≡→∈ {x} {y ∷ xs} (there x∈≡xs) =  there $ ∈≡→∈ {x} {xs} x∈≡xs

    cong₁∈' : {zs : List C'} → (\x → x ∈' zs) Respects _≈'_
    cong₁∈' {z ∷ zs} {_} {_} x=y (here x=z) =   here (≈'trans (≈'sym x=y) x=z)
    cong₁∈' {z ∷ zs} {_} {_} x=y (there x∈zs) =  there (cong₁∈' {zs} x=y x∈zs)

  ----------------------------------------------------------------------------
--  postulate 
  map⊆ : (f : C → C') → (f Preserves _≈_ ⟶ _≈'_) → 
                                                 (map f) Preserves _⊆_ ⟶ _⊆'_
  map⊆ f fCong {xs} {ys} xs⊆ys {z} z∈f-xs = 
       let 
         (x , x∈≡xs , fx≈z) = counter-map {A = C} {sd = A'} f z∈f-xs 
         x∈xs    = ∈≡→∈ x∈≡xs                             
         x∈ys    = xs⊆ys x∈xs
         fx∈f-ys = map∈ f fCong x∈ys
       in
       cong₁∈' fx≈z fx∈f-ys