Possible Regression at fromℕ<

[dMaggot]

The following module works in v1.7.2 but does not work in master:

module bug where

open import Data.Maybe using (just)
open import Data.Fin using (fromℕ<)
open import Data.List using (List; lookup; length; head; _∷_; [])
open import Data.Nat using (_<_; ℕ)
open import Data.Nat.Properties using (n<1⇒n≡0; ≤-reflexive)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)

bug : ∀ {l : List ℕ} → (len≡1 : length l ≡ 1) → lookup l (fromℕ< (≤-reflexive (sym len≡1))) < (length l) → head l ≡ just 0
bug {x ∷ []} len≡1 headBounded rewrite n<1⇒n≡0 headBounded = refl

According to git bisect the culprit is 82c1b9d so I suppose the problem is fromℕ<.

[gallais]

Can you please provide a more detailed report than "does not work"?

[dMaggot]

The error message is

bug.agda:11,62-66
x != ℕ.zero of type ℕ
when checking that the expression refl has type just x ≡ just 0

but I do not think that is very revealing without familiarizing oneself with the example.

Here ≤-reflexive (sym len≡1) is simply 0 < length l so fromℕ< should give you 0 and headBounded should be lookup (x ∷ []) 0 < (length (x ∷ [])) and the rewriting should be on x ≡ 0. This all works as expected in v1.7.2 but the rewriting does not happen in master. If the culprit is indeed fromℕ< then there may be a simpler minimal example but I have not had time to look into that yet.

[gallais]

#1709 made fromℕ< more strict by turning a call to ≤-pred on the right hand side into a pattern on the left.

[jamesmckinna]

module unbug where

open import Data.Maybe using (just)
open import Data.Fin using (fromℕ<)
open import Data.List using (List; lookup; length; head; _∷_; [])
open import Data.Nat using (_<_; ℕ; z<s)
open import Data.Nat.Properties using (n<1⇒n≡0; ≤-reflexive)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)

unbug : ∀ {l : List ℕ} → (len≡1 : length l ≡ 1) → lookup l (fromℕ< (≤-reflexive (sym len≡1))) < (length l) → head l ≡ just 0
unbug {x ∷ []} refl z<s = refl

So... your regression test bug fails, while the above succeeds, so what exactly is at stake here?

The 'offending' PR/commit was, in part, concerned with simplifying the imports associated with Data.Nat.Properties, and in particular, the problem of artificial separation out of a Core submodule for the sake of narrowing the imports of Data.Fin.Base. The introduction of the additional pattern synonyms for _<_ provides an alternative solution to your problem, as shown. See also the discussion in #1698 and related/referenced issues there.

A further alternative (but going completely against #1726 / #1868) might be to reinstate the _≺_ view in Data.Fin.Base (and its equivalence with _<_ from Data.Nat.Base and use that view to define fromℕ< by projecting out i from the constructor pattern n ≻toℕ i, ie define fromℕ< as a view-derived inverse to toℕ...

[jamesmckinna]

And as for the regression test, the following modification

bug {x ∷ []} len≡1 headBounded rewrite len≡1 | n<1⇒n≡0 headBounded = refl

which disguises the match on refl in len≡1, does pass the typechecker...

[jamesmckinna]

Ah... perhaps more annoying than the above, the definitions at the end of Data.Nat.DivMod are now arguably too strict. All other uses of fromℕ< in the library seem only to concern properties of computations (we might debate the uses in Data.Vec.{Functional}.Properties). Hmmm.

[jamesmckinna]

Fixed by #2000 ?

[dMaggot]

Yes, the example above and my original problem both typecheck at jamesmckinna/agda-stdlib@e7d75d300.

[jamesmckinna]

I'd like to find a way to triage #2000 enough to be able to fix such things before v2.0