Agda-stdlib: Build for `experimental` fails

[anuyts]

I know that this is not the recommended version of agda to use the stdlib 1.5 with, but since the agda-stdlib developers will eventually want to support agda 2.6.2, it seemed worth reporting.

I get the following error:

/path/to/agda-stdlib-1.5/src/Data/List/Membership/Propositional/Properties.agda:17,1-52
Failed to solve the following constraints:
  Check definition of to∘from : {P.A.a : Level} {P.A : Set P.A.a}
                                {P.p : Level} {P = P₁ : Pred P.A P.p} {Q.A.a : Level}
                                {Q.A : Set Q.A.a} {Q.p : Level} {Q = Q₁ : Pred Q.A Q.p}
                                {xs = xs₁ : List P.A} {ys = ys₁ : List Q.A}
                                (pq
                                 : Any (λ x → Any (λ y → Prod.Σ (P₁ x) (λ x₁ → Q₁ y)) ys₁) xs₁) →
                                Any-×⁺ (Any-×⁻ pq) ≡ pq
    stuck because
      /path/to/agda-stdlib-1.5/src/Data/List/Relation/Unary/Any/Properties.agda:267,3-34
      I'm not sure if there should be a case for the constructor refl,
      because I get stuck when trying to solve the following unification
      problems (inferred index ≟ expected index):
        lhs ≟ Any.map
              (λ x →
                 Any.map (λ q → P.subst P x p , q)
                 (Any.map
                  (λ x₁ →
                     P.subst Q x₁
                     (_5428 (x = x₂) (pq′ = pq′) (y = y) (y∈ys = y∈ys) (p = p) (q = q)
                      (lem₂ = lem₂) (pq = pq) (x∈xs = x∈xs) (lem₁ = lem₁)
                      (p = (P.subst P x p))))
                  y∈ys))
              x∈xs
      when checking that the pattern refl has type
      lhs ≡
      Any.map
      (λ x →
         Any.map (λ q → P.subst P x p , q)
         (Any.map
          (λ x₁ →
             P.subst Q x₁
             (_5428 (x = x₂) (pq′ = pq′) (y = y) (y∈ys = y∈ys) (p = p) (q = q)
              (lem₂ = lem₂) (pq = pq) (x∈xs = x∈xs) (lem₁ = lem₁)
              (p = (P.subst P x p))))
          y∈ys))
      x∈xs
    (blocked on _P.p_475)
when scope checking the declaration
  open import Data.List.Relation.Unary.Any.Properties
/path/to/agda-stdlib-1.5/src/Data/List/Membership/Propositional/Properties.agda:17,1-52
Unsolved metas at the following locations:
  /path/to/agda-stdlib-1.5/src/Data/List/Relation/Unary/Any/Properties.agda:100,17-18
  /path/to/agda-stdlib-1.5/src/Data/List/Relation/Unary/Any/Properties.agda:105,16-17
  /path/to/agda-stdlib-1.5/src/Data/List/Relation/Unary/Any/Properties.agda:105,28-29
when scope checking the declaration
  open import Data.List.Relation.Unary.Any.Properties

[gallais]

The experimental branch is already targeting Agda-dev cf. README.

[anuyts]

Thanks!

[anuyts]

Yet the issue persists:

/path/to/agda-stdlib-experimental/src/Data/List/Membership/Propositional/Properties.agda:17,1-52
Failed to solve the following constraints:
  Check definition of to∘from : {P.A.a : Level} {P.A : Set P.A.a}
                                {P.p : Level} {P = P₁ : Pred P.A P.p} {Q.A.a : Level}
                                {Q.A : Set Q.A.a} {Q.p : Level} {Q = Q₁ : Pred Q.A Q.p}
                                {xs = xs₁ : List P.A} {ys = ys₁ : List Q.A}
                                (pq
                                 : Any (λ x → Any (λ y → Prod.Σ (P₁ x) (λ x₁ → Q₁ y)) ys₁) xs₁) →
                                Any-×⁺ (Any-×⁻ pq) ≡ pq
    stuck because
      /path/to/agda-stdlib-experimental/src/Data/List/Relation/Unary/Any/Properties.agda:266,3-34
      I'm not sure if there should be a case for the constructor refl,
      because I get stuck when trying to solve the following unification
      problems (inferred index ≟ expected index):
        lhs ≟ Any.map
              (λ x →
                 Any.map (λ q → P.subst P x p , q)
                 (Any.map
                  (λ x₁ →
                     P.subst Q x₁
                     (_5428 (x = x₂) (pq′ = pq′) (y = y) (y∈ys = y∈ys) (p = p) (q = q)
                      (lem₂ = lem₂) (pq = pq) (x∈xs = x∈xs) (lem₁ = lem₁)
                      (p = (P.subst P x p))))
                  y∈ys))
              x∈xs
      when checking that the pattern refl has type
      lhs ≡
      Any.map
      (λ x →
         Any.map (λ q → P.subst P x p , q)
         (Any.map
          (λ x₁ →
             P.subst Q x₁
             (_5428 (x = x₂) (pq′ = pq′) (y = y) (y∈ys = y∈ys) (p = p) (q = q)
              (lem₂ = lem₂) (pq = pq) (x∈xs = x∈xs) (lem₁ = lem₁)
              (p = (P.subst P x p))))
          y∈ys))
      x∈xs
    (blocked on _P.p_475)
when scope checking the declaration
  open import Data.List.Relation.Unary.Any.Properties
/path/to/agda-stdlib-experimental/src/Data/List/Membership/Propositional/Properties.agda:17,1-52
Unsolved metas at the following locations:
  /path/to/agda-stdlib-experimental/src/Data/List/Relation/Unary/Any/Properties.agda:100,17-18
  /path/to/agda-stdlib-experimental/src/Data/List/Relation/Unary/Any/Properties.agda:105,16-17
  /path/to/agda-stdlib-experimental/src/Data/List/Relation/Unary/Any/Properties.agda:105,28-29
when scope checking the declaration
  open import Data.List.Relation.Unary.Any.Properties

[MatthewDaggitt]

Yes, you're right @anuyts . The test suite for the experimental branch is falling over:

https://travis-ci.org/github/agda/agda-stdlib/jobs/756182490

This proof always seems to be very brittle with respect to changes in how meta-variables are solved in Agda. I can't decide whether that's a bad thing (code breaks easily), or a good thing (excellent detection mechanism for such changes).

I'll have a poke around and see if I can figure out what's happening. Out of interest what commit is your version of development of Agda on? Is it after the following commit?

https://github.com/agda/agda/commit/ea402084ba2d84a82429a68050eb461a6d935618

[MatthewDaggitt]

We should also add the experimental badge to the README, so we stand a slightly better chance of noticing that experimental is falling over.

[anuyts]

I'm at e12f391, which is slightly older.

[JorisCeulemans]

I'm having the same issue with 18b8c6d, which dates back to October 13 2020.

[MatthewDaggitt]

Okay, I've done the easy bit of updating the badges in d1f4571. I'll bump the version of Agda that experimental is using to the latest build and see how that goes.

[gallais]

The build succeeded for me with Agda's master (well... the modified version I
have in agda/agda#5166). An annoying part of agda/agda#5166 is that we cannot use
noMissingDefinitions in the README files anymore.

Once we bump past that version, we'll have to remember to use --allow-unsolved-metas
and placeholders of the form thm = ? instead.

To get back noMissingDefinitions will involve a big refactoring of Agda's handling
of options that I have had in the back of my mind for a long time but won't be able
to work on any time soon.

Edit:

I'll bump the version of Agda that experimental is using to the latest build and see how that goes.

It worked!

[MatthewDaggitt]

Yup, I've updated experimental to build with agda/agda@fec6097 and it seems to pass. I suspect agda/agda@ea40208 fixed the issue.

Thanks for the report @anuyts

[anuyts]

Confirmed.