Changes explicit argument y to implicit in Induction.WellFounded.WfRec (#2084)

Author: jamesmckinna

CHANGELOG.md

@@ -585,6 +585,21 @@ Non-backwards compatible changes
   Prime n = ∀ {d} → 2 ≤ d → d < n → d ∤ n
   ```
 
+### Change to the definition of `Induction.WellFounded.WfRec` (issue #2083)
+
+* Previously, the following definition was adopted
+  ```agda
+  WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _
+  WfRec _<_ P x = ∀ y → y < x → P y
+  ```
+  with the consequence that all arguments involving about accesibility and
+  wellfoundedness proofs were polluted by almost-always-inferrable explicit
+  arguments for the `y` position. The definition has now been changed to
+  make that argument *implicit*, as 
+  ```agda
+  WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _
+  WfRec _<_ P x = ∀ {y} → y < x → P y
+
 ### Change in the definition of `_≤″_` (issue #1919)
 
 * The definition of `_≤″_` in `Data.Nat.Base` was previously:

README/Data/Nat/Induction.agda

@@ -14,6 +14,14 @@ open import Function.Base using (_∘_)
 open import Induction.WellFounded
 open import Relation.Binary.PropositionalEquality
 
+private
+
+  n<′1+n : ∀ {n} → n <′ suc n
+  n<′1+n = ≤′-refl
+
+  n<′2+n : ∀ {n} → n <′ suc (suc n)
+  n<′2+n = ≤′-step ≤′-refl
+
 -- Doubles its input.
 
 twice : ℕ → ℕ
@@ -46,7 +54,7 @@ mutual
   half₂-step = λ
     { zero          _   → zero
     ; (suc zero)    _   → zero
-    ; (suc (suc n)) rec → suc (rec n (≤′-step ≤′-refl))
+    ; (suc (suc n)) rec → suc (rec n<′2+n)
     }
 
   half₂ : ℕ → ℕ
@@ -92,21 +100,21 @@ half₂-2+ n = begin
 
   half₂-step (2 + n) (<′-recBuilder _ half₂-step (2 + n))     ≡⟨⟩
 
-  1 + <′-recBuilder _ half₂-step (2 + n) n (≤′-step ≤′-refl)  ≡⟨⟩
+  1 + <′-recBuilder _ half₂-step (2 + n) n<′2+n  ≡⟨⟩
 
   1 + Some.wfRecBuilder _ half₂-step (2 + n)
-        (<′-wellFounded (2 + n)) n (≤′-step ≤′-refl)          ≡⟨⟩
+        (<′-wellFounded (2 + n)) n<′2+n          ≡⟨⟩
 
   1 + Some.wfRecBuilder _ half₂-step (2 + n)
-        (acc (<′-wellFounded′ (2 + n))) n (≤′-step ≤′-refl)   ≡⟨⟩
+        (acc (<′-wellFounded′ (2 + n))) n<′2+n   ≡⟨⟩
 
   1 + half₂-step n
         (Some.wfRecBuilder _ half₂-step n
-           (<′-wellFounded′ (2 + n) n (≤′-step ≤′-refl)))     ≡⟨⟩
+           (<′-wellFounded′ (2 + n) n<′2+n))     ≡⟨⟩
 
   1 + half₂-step n
         (Some.wfRecBuilder _ half₂-step n
-           (<′-wellFounded′ (1 + n) n ≤′-refl))               ≡⟨⟩
+           (<′-wellFounded′ (1 + n) n<′1+n))               ≡⟨⟩
 
   1 + half₂-step n
         (Some.wfRecBuilder _ half₂-step n (<′-wellFounded n)) ≡⟨⟩
@@ -146,14 +154,14 @@ half₁-+₂ = <′-rec _ λ
   { zero          _   → refl
   ; (suc zero)    _   → refl
   ; (suc (suc n)) rec →
-      cong (suc ∘ suc) (rec n (≤′-step ≤′-refl))
+      cong (suc ∘ suc) (rec n<′2+n)
   }
 
 half₂-+₂ : ∀ n → half₂ (twice n) ≡ n
 half₂-+₂ = <′-rec _ λ
   { zero          _   → refl
   ; (suc zero)    _   → refl
   ; (suc (suc n)) rec →
-      cong (suc ∘ suc) (rec n (≤′-step ≤′-refl))
+      cong (suc ∘ suc) (rec n<′2+n)
   }
 

src/Codata/Musical/Colist/Infinite-merge.agda

@@ -195,7 +195,7 @@ Any-merge {P = P} xss = mk↔ₛ′ (proj₁ ∘ to xss) from to∘from (proj₂
     ... | inj₂ q | P.refl | q≤p =
       Prod.map there
                (P.cong (there ∘ (Inverse.from (Any-⋎P xs)) ∘ inj₂))
-               (rec (♭ xss , q) (s≤′s q≤p))
+               (rec (s≤′s q≤p))
 
   to∘from = λ p → from-injective _ _ (proj₂ (to xss (from p)))
 

src/Data/Bool/Properties.agda

@@ -195,8 +195,8 @@ true  <? _     = no  (λ())
 <-wellFounded : WellFounded _<_
 <-wellFounded _ = acc <-acc
   where
-    <-acc : ∀ {x} y → y < x → Acc _<_ y
-    <-acc false f<t = acc (λ _ → λ())
+    <-acc : ∀ {x y} → y < x → Acc _<_ y
+    <-acc f<t = acc λ ()
 
 -- Structures
 

src/Data/Digit.agda

@@ -56,7 +56,7 @@ toNatDigits base@(suc (suc _)) n = aux (<-wellFounded-fast n) []
   aux {zero}        _      xs =  (0 ∷ xs)
   aux {n@(suc _)} (acc wf) xs with does (0 <? n / base)
   ... | false = (n % base) ∷ xs
-  ... | true  = aux (wf (n / base) q<n) ((n % base) ∷ xs)
+  ... | true  = aux (wf q<n) ((n % base) ∷ xs)
     where
     q<n : n / base < n
     q<n = m/n<m n base (s<s z<s)
@@ -107,9 +107,8 @@ toDigits base@(suc (suc k)) n = <′-rec Pred helper n
 
   helper : ∀ n → <′-Rec Pred n → Pred n
   helper n                       rec with n divMod base
-  helper .(toℕ r + 0     * base) rec | result zero    r refl = ([ r ] , refl)
-  helper .(toℕ r + suc x * base) rec | result (suc x) r refl =
-    cons r (rec (suc x) (lem x k (toℕ r)))
+  ... | result zero    r eq = ([ r ] , P.sym eq)
+  ... | result (suc x) r refl = cons r (rec (lem x k (toℕ r)))
 
 ------------------------------------------------------------------------
 -- Showing digits

src/Data/Fin/Induction.agda

@@ -65,7 +65,7 @@ open WF public using (Acc; acc)
   induct {suc j} (acc rs) (tri< (s≤s i≤j) _ _) _ = Pᵢ⇒Pᵢ₊₁ j P[1+j]
     where
     toℕj≡toℕinjJ = sym $ toℕ-inject₁ j
-    P[1+j] = induct (rs _ (s≤s (subst (ℕ._≤ toℕ j) toℕj≡toℕinjJ ≤-refl)))
+    P[1+j] = induct (rs (s≤s (subst (ℕ._≤ toℕ j) toℕj≡toℕinjJ ≤-refl)))
       (<-cmp i $ inject₁ j) (subst (toℕ i ℕ.≤_) toℕj≡toℕinjJ i≤j)
 
 <-weakInduction : (P : Pred (Fin (suc n)) ℓ) →
@@ -80,8 +80,7 @@ open WF public using (Acc; acc)
 
 private
   acc-map : ∀ {x : Fin n} → Acc ℕ._<_ (n ∸ toℕ x) → Acc _>_ x
-  acc-map {n} (acc rs) = acc λ y y>x →
-    acc-map (rs (n ∸ toℕ y) (ℕ.∸-monoʳ-< y>x (toℕ≤n y)))
+  acc-map (acc rs) = acc λ y>x → acc-map (rs (ℕ.∸-monoʳ-< y>x (toℕ≤n _)))
 
 >-wellFounded : WellFounded {A = Fin n} _>_
 >-wellFounded {n} x = acc-map (ℕ.<-wellFounded (n ∸ toℕ x))
@@ -96,7 +95,7 @@ private
   induct {i} (acc rec) with n ℕ.≟ toℕ i
   ... | yes n≡i = subst P (toℕ-injective (trans (toℕ-fromℕ n) n≡i)) Pₙ
   ... | no  n≢i = subst P (inject₁-lower₁ i n≢i) (Pᵢ₊₁⇒Pᵢ _ Pᵢ₊₁)
-    where Pᵢ₊₁ = induct (rec _ (ℕ.≤-reflexive (cong suc (sym (toℕ-lower₁ i n≢i)))))
+    where Pᵢ₊₁ = induct (rec (ℕ.≤-reflexive (cong suc (sym (toℕ-lower₁ i n≢i)))))
 
 ------------------------------------------------------------------------
 -- Well-foundedness of other (strict) partial orders on Fin
@@ -112,20 +111,20 @@ module _ {_≈_ : Rel (Fin n) ℓ} where
 
   spo-wellFounded : ∀ {r} {_⊏_ : Rel (Fin n) r} →
                     IsStrictPartialOrder _≈_ _⊏_ → WellFounded _⊏_
-  spo-wellFounded {_} {_⊏_} isSPO i = go n i pigeon where
+  spo-wellFounded {_} {_⊏_} isSPO i = go n pigeon where
 
     module ⊏ = IsStrictPartialOrder isSPO
 
-    go : ∀ m i →
-         ((xs : Vec (Fin n) m) → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_) →
+    go : ∀ m {i} →
+         ({xs : Vec (Fin n) m} → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_) →
          Acc _⊏_ i
-    go zero    i k = k [] [-] i
-    go (suc m) i k = acc $ λ j j⊏i → go m j (λ xs i∷xs↑ → k (j ∷ xs) (j⊏i ∷ i∷xs↑))
+    go zero    k = k [-] _
+    go (suc m) k = acc λ j⊏i → go m λ i∷xs↑ → k (j⊏i ∷ i∷xs↑)
 
-    pigeon : (xs : Vec (Fin n) n) → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_
-    pigeon xs i∷xs↑ =
+    pigeon : {xs : Vec (Fin n) n} → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_
+    pigeon {xs} i∷xs↑ =
       let (i₁ , i₂ , i₁<i₂ , xs[i₁]≡xs[i₂]) = pigeonhole (n<1+n n) (Vec.lookup (i ∷ xs)) in
-      let xs[i₁]⊏xs[i₂] = Linkedₚ.lookup⁺ (Ord.transitive _⊏_ ⊏.trans) {xs = i ∷ xs} i∷xs↑ i₁<i₂ in
+      let xs[i₁]⊏xs[i₂] = Linkedₚ.lookup⁺ (Ord.transitive _⊏_ ⊏.trans) i∷xs↑ i₁<i₂ in
       let xs[i₁]⊏xs[i₁] = ⊏.<-respʳ-≈ (⊏.Eq.reflexive xs[i₁]≡xs[i₂]) xs[i₁]⊏xs[i₂] in
       contradiction xs[i₁]⊏xs[i₁] (⊏.irrefl ⊏.Eq.refl)
 

src/Data/Graph/Acyclic.agda

@@ -313,7 +313,7 @@ module _ {ℓ e} {N : Set ℓ} {E : Set e} where
     expand n rec (c & g) =
       node (label c)
            (List.map
-              (Prod.map id (λ i → rec (n - suc i) (lemma n i) (g [ i ])))
+              (Prod.map id (λ i → rec (lemma n i) (g [ i ])))
               (successors c))
 
 -- Performs the toTree expansion once for each node.

src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda

@@ -384,15 +384,15 @@ split v as bs p = helper as bs p (<-wellFounded (steps p))
   helper (a ∷ [])     bs (refl eq)    _ = [ a ]      , bs , eq
   helper (a ∷ b ∷ as) bs (refl eq)    _ = a ∷ b ∷ as , bs , eq
   helper []           bs (prep v≈x _) _ = [] , _ , v≈x ∷ ≋-refl
-  helper (a ∷ as)     bs (prep eq as↭xs) (acc rec) with helper as bs as↭xs (rec _ ≤-refl)
+  helper (a ∷ as)     bs (prep eq as↭xs) (acc rec) with helper as bs as↭xs (rec ≤-refl)
   ... | (ps , qs , eq₂) = a ∷ ps , qs , eq ∷ eq₂
   helper [] (b ∷ bs)     (swap x≈b y≈v _) _ = [ b ] , _     , x≈b ∷ y≈v ∷ ≋-refl
   helper (a ∷ [])     bs (swap x≈v y≈a ↭) _ = []    , a ∷ _ , x≈v ∷ y≈a ∷ ≋-refl
-  helper (a ∷ b ∷ as) bs (swap x≈b y≈a as↭xs) (acc rec) with helper as bs as↭xs (rec _ ≤-refl)
+  helper (a ∷ b ∷ as) bs (swap x≈b y≈a as↭xs) (acc rec) with helper as bs as↭xs (rec ≤-refl)
   ... | (ps , qs , eq) = b ∷ a ∷ ps , qs , x≈b ∷ y≈a ∷ eq
-  helper as           bs (trans ↭₁ ↭₂) (acc rec) with helper as bs ↭₂ (rec _ (m<n+m (steps ↭₂) (0<steps ↭₁)))
+  helper as           bs (trans ↭₁ ↭₂) (acc rec) with helper as bs ↭₂ (rec (m<n+m (steps ↭₂) (0<steps ↭₁)))
   ... | (ps , qs , eq) = helper ps qs (↭-respʳ-≋ eq ↭₁)
-    (rec _ (subst (_< _) (sym (steps-respʳ eq ↭₁)) (m<m+n (steps ↭₁) (0<steps ↭₂))))
+      (rec (subst (_< _) (sym (steps-respʳ eq ↭₁)) (m<m+n (steps ↭₁) (0<steps ↭₂))))
 
 ------------------------------------------------------------------------
 -- filter

src/Data/List/Sort/MergeSort.agda

@@ -44,20 +44,21 @@ open PermutationReasoning
 -- Definition
 
 mergePairs : List (List A) → List (List A)
-mergePairs (xs ∷ ys ∷ xss) = merge _≤?_ xs ys ∷ mergePairs xss
+mergePairs (xs ∷ ys ∷ yss) = merge _≤?_ xs ys ∷ mergePairs yss
 mergePairs xss             = xss
 
 private
-  length-mergePairs : ∀ xs ys xss → length (mergePairs (xs ∷ ys ∷ xss)) < length (xs ∷ ys ∷ xss)
+  length-mergePairs : ∀ xs ys yss → let zss = xs ∷ ys ∷ yss in
+                      length (mergePairs zss) < length zss
   length-mergePairs _ _ []              = s<s z<s
-  length-mergePairs _ _ (xss ∷ [])      = s<s (s<s z<s)
-  length-mergePairs _ _ (xs ∷ ys ∷ xss) = s<s (m<n⇒m<1+n (length-mergePairs xs ys xss))
+  length-mergePairs _ _ (xs ∷ [])       = s<s (s<s z<s)
+  length-mergePairs _ _ (xs ∷ ys ∷ yss) = s<s (m<n⇒m<1+n (length-mergePairs xs ys yss))
 
 mergeAll : (xss : List (List A)) → Acc _<_ (length xss) → List A
 mergeAll []        _               = []
 mergeAll (xs ∷ []) _               = xs
-mergeAll (xs ∷ ys ∷ xss) (acc rec) = mergeAll
-  (mergePairs (xs ∷ ys ∷ xss)) (rec _ (length-mergePairs xs ys xss))
+mergeAll xss@(xs ∷ ys ∷ yss) (acc rec) = mergeAll
+  (mergePairs xss) (rec (length-mergePairs xs ys yss))
 
 sort : List A → List A
 sort xs = mergeAll (map [_] xs) (<-wellFounded-fast _)

src/Data/Nat/DivMod.agda

@@ -294,7 +294,7 @@ m*n/m*o≡n/o m@(suc _) n o = helper (<-wellFounded n)
   ... | no  n≮o = begin-equality
     (m * n) / (m * o)             ≡⟨  m/n≡1+[m∸n]/n (*-monoʳ-≤ m (≮⇒≥ n≮o)) ⟩
     1 + (m * n ∸ m * o) / (m * o) ≡˘⟨ cong (λ v → 1 + v / (m * o)) (*-distribˡ-∸ m n o) ⟩
-    1 + (m * (n ∸ o)) / (m * o)   ≡⟨  cong suc (helper (rec (n ∸ o) n∸o<n)) ⟩
+    1 + (m * (n ∸ o)) / (m * o)   ≡⟨  cong suc (helper (rec n∸o<n)) ⟩
     1 + (n ∸ o) / o               ≡˘⟨ cong₂ _+_ (n/n≡1 o) refl ⟩
     o / o + (n ∸ o) / o           ≡˘⟨ +-distrib-/-∣ˡ (n ∸ o) (divides 1 ((sym (*-identityˡ o)))) ⟩
     (o + (n ∸ o)) / o             ≡⟨  cong (_/ o) (m+[n∸m]≡n (≮⇒≥ n≮o)) ⟩

src/Data/Nat/GCD.agda

@@ -43,7 +43,7 @@ open import Algebra.Definitions {A = ℕ} _≡_ as Algebra
 
 gcd′ : ∀ m n → Acc _<_ m → n < m → ℕ
 gcd′ m zero      _         _   = m
-gcd′ m n@(suc _) (acc rec) n<m = gcd′ n (m % n) (rec _ n<m) (m%n<n m n)
+gcd′ m n@(suc _) (acc rec) n<m = gcd′ n (m % n) (rec n<m) (m%n<n m n)
 
 gcd : ℕ → ℕ → ℕ
 gcd m n with <-cmp m n
@@ -55,15 +55,15 @@ gcd m n with <-cmp m n
 -- Core properties of gcd′
 
 gcd′[m,n]∣m,n : ∀ {m n} rec n<m → gcd′ m n rec n<m ∣ m × gcd′ m n rec n<m ∣ n
-gcd′[m,n]∣m,n {m} {zero}  rec       n<m = ∣-refl , m ∣0
-gcd′[m,n]∣m,n {m} {suc n} (acc rec) n<m
-  with gcd∣n , gcd∣m%n ← gcd′[m,n]∣m,n (rec _ n<m) (m%n<n m (suc n))
+gcd′[m,n]∣m,n {m} {zero}      rec       n<m = ∣-refl , m ∣0
+gcd′[m,n]∣m,n {m} {n@(suc _)} (acc rec) n<m
+  with gcd∣n , gcd∣m%n ← gcd′[m,n]∣m,n (rec n<m) (m%n<n m n)
   = ∣n∣m%n⇒∣m gcd∣n gcd∣m%n , gcd∣n
 
 gcd′-greatest : ∀ {m n c} rec n<m → c ∣ m → c ∣ n → c ∣ gcd′ m n rec n<m
-gcd′-greatest {m} {zero}  rec       n<m c∣m c∣n = c∣m
-gcd′-greatest {m} {suc n} (acc rec) n<m c∣m c∣n =
-  gcd′-greatest (rec _ n<m) (m%n<n m (suc n)) c∣n (%-presˡ-∣ c∣m c∣n)
+gcd′-greatest {m} {zero}      rec       n<m c∣m c∣n = c∣m
+gcd′-greatest {m} {n@(suc _)} (acc rec) n<m c∣m c∣n =
+  gcd′-greatest (rec n<m) (m%n<n m n) c∣n (%-presˡ-∣ c∣m c∣n)
 
 ------------------------------------------------------------------------
 -- Core properties of gcd
@@ -387,13 +387,13 @@ module Bézout where
     P (m , n) = Lemma m n
 
     gcd″ : ∀ p → (<′-Rec ⊗ <′-Rec) P p → P p
-    gcd″ (zero  , n)     rec = Lemma.base n
-    gcd″ (suc m , zero)  rec = Lemma.sym (Lemma.base (suc m))
-    gcd″ (suc m , suc n) rec with compare m n
-    ... | equal m     = Lemma.refl (suc m)
-    ... | less m k    = Lemma.stepˡ $ proj₁ rec (suc k) (lem₁ k m)
+    gcd″ (zero      , n)     rec = Lemma.base n
+    gcd″ (m@(suc _) , zero)  rec = Lemma.sym (Lemma.base m)
+    gcd″ (m′@(suc m) , n′@(suc n)) rec with compare m n
+    ... | equal m     = Lemma.refl m′
+    ... | less m k    = Lemma.stepˡ $ proj₁ rec (lem₁ k m)
                       -- "gcd (suc m) (suc k)"
-    ... | greater n k = Lemma.stepʳ $ proj₂ rec (suc k) (lem₁ k n) (suc n)
+    ... | greater n k = Lemma.stepʳ $ proj₂ rec (lem₁ k n) n′
                       -- "gcd (suc k) (suc n)"
 
   -- Bézout's identity can be recovered from the GCD.

src/Data/Nat/Induction.agda

@@ -67,8 +67,8 @@ cRec = build cRecBuilder
 
 <′-wellFounded n = acc (<′-wellFounded′ n)
 
-<′-wellFounded′ (suc n) n <′-base       = <′-wellFounded n
-<′-wellFounded′ (suc n) m (<′-step m<n) = <′-wellFounded′ n m m<n
+<′-wellFounded′ (suc n) <′-base       = <′-wellFounded n
+<′-wellFounded′ (suc n) (<′-step m<n) = <′-wellFounded′ n m<n
 
 module _ {ℓ : Level} where
   open WF.All <′-wellFounded ℓ public
@@ -100,7 +100,7 @@ module _ {ℓ : Level} where
   <-wellFounded-skip : ∀ (k : ℕ) → WellFounded _<_
   <-wellFounded-skip zero    n       = <-wellFounded n
   <-wellFounded-skip (suc k) zero    = <-wellFounded 0
-  <-wellFounded-skip (suc k) (suc n) = acc (λ m _ → <-wellFounded-skip k m)
+  <-wellFounded-skip (suc k) (suc n) = acc λ {m} _ → <-wellFounded-skip k m
 
 module _ {ℓ : Level} where
   open WF.All <-wellFounded ℓ public

src/Data/Nat/Logarithm/Core.agda

@@ -23,15 +23,15 @@ open import Data.Unit
 ⌊log2⌋ : ∀ n → Acc _<_ n → ℕ
 ⌊log2⌋ 0          _        = 0
 ⌊log2⌋ 1          _        = 0
-⌊log2⌋ (suc n′@(suc n)) (acc rs) = 1 + ⌊log2⌋ (suc ⌊ n /2⌋) (rs _ (⌊n/2⌋<n n′))
+⌊log2⌋ (suc n′@(suc n)) (acc rs) = 1 + ⌊log2⌋ (suc ⌊ n /2⌋) (rs (⌊n/2⌋<n n′))
 
 
 -- Ceil version
 
 ⌈log2⌉ : ∀ n → Acc _<_ n → ℕ
 ⌈log2⌉ 0                _        = 0
 ⌈log2⌉ 1                _        = 0
-⌈log2⌉ (suc (suc n)) (acc rs) = 1 + ⌈log2⌉ (suc ⌈ n /2⌉) (rs _ (⌈n/2⌉<n n))
+⌈log2⌉ (suc (suc n)) (acc rs) = 1 + ⌈log2⌉ (suc ⌈ n /2⌉) (rs (⌈n/2⌉<n n))
 
 ------------------------------------------------------------------------
 -- Properties of ⌊log2⌋

src/Data/Nat/Properties.agda

@@ -486,7 +486,7 @@ m<1+n⇒m≤n (s≤s m≤n) = m≤n
 ∀[m<n⇒m≢o]⇒n≤o (suc n) (suc o) m<n⇒m≢o = s≤s (∀[m<n⇒m≢o]⇒n≤o n o rec)
   where
   rec : ∀ {m} → m < n → m ≢ o
-  rec x<m refl = m<n⇒m≢o (s≤s x<m) refl
+  rec o<n refl = m<n⇒m≢o (s<s o<n) refl
 
 ------------------------------------------------------------------------
 -- A module for reasoning about the _≤_ and _<_ relations

src/Data/Product/Relation/Binary/Lex/Strict.agda

@@ -202,13 +202,13 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂} {_<₂_ : Rel B ℓ
     ×-acc : ∀ {x y} →
             Acc _<₁_ x → Acc _<₂_ y →
             WfRec _<ₗₑₓ_ (Acc _<ₗₑₓ_) (x , y)
-    ×-acc (acc rec₁) acc₂ (u , v) (inj₁ u<x)
-      = acc (×-acc (rec₁ u u<x) (wf₂ v))
-    ×-acc acc₁ (acc rec₂) (u , v) (inj₂ (u≈x , v<y))
+    ×-acc (acc rec₁) acc₂ (inj₁ u<x)
+      = acc (×-acc (rec₁ u<x) (wf₂ _))
+    ×-acc acc₁ (acc rec₂) (inj₂ (u≈x , v<y))
       = Acc-resp-flip-≈
         (×-respectsʳ {_<₁_ = _<₁_} {_<₂_ = _<₂_} trans resp (≡.respʳ _<₂_))
         (u≈x , ≡.refl)
-        (acc (×-acc acc₁ (rec₂ v v<y)))
+        (acc (×-acc acc₁ (rec₂ v<y)))
 
 
 module _ {_<₁_ : Rel A ℓ₁} {_<₂_ : Rel B ℓ₂} where

src/Data/Vec/Relation/Binary/Lex/Strict.agda

@@ -134,7 +134,8 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
     where
 
     <-wellFounded : ∀ {n} → WellFounded (_<_ {n})
-    <-wellFounded {0}     [] = acc λ ys ys<[] → ⊥-elim (xs≮[] ys<[])
+    <-wellFounded {0}     [] = acc λ ys<[] → ⊥-elim (xs≮[] ys<[])
+
     <-wellFounded {suc n} xs = Subrelation.wellFounded <⇒uncons-Lex uncons-Lex-wellFounded xs
       where
         <⇒uncons-Lex : {xs ys : Vec A (suc n)} → xs < ys → (×-Lex _≈_ _≺_ _<_ on uncons) xs ys