Non-terminating function over tuples passed with --termination-depth=2

[nad]

In the following code there is special treatment of the cases "empty, singleton" and "singleton, empty", but in other cases where the lists have different lengths the extra elements are simply discarded:

agda/src/full/Agda/Termination/TermCheck.hs

Lines 1418 to 1430 in efa6fe4

	compareConArgs :: Args -> [NamedArg DeBruijnPattern] -> TerM Order
	compareConArgs ts ps = do
	cutoff <- terGetCutOff
	let ?cutoff = cutoff
	-- we may assume |ps| >= |ts|, otherwise c ps would be of functional type
	-- which is impossible
	case (length ts, length ps) of
	(0,0) -> return Order.le -- c <= c
	(0,1) -> return Order.unknown -- c not<= c x
	(1,0) -> __IMPOSSIBLE__
	(1,1) -> compareTerm' (unArg (head ts)) (notMasked $ namedArg $ head ps)
	(_,_) -> foldl (Order..*.) Order.le <$>
	zipWithM compareTerm' (map unArg ts) (map (notMasked . namedArg) ps)

@andreasabel, can you take a look at this? Do the lists necessarily have the same length? Or should we return Order.unknown more often?

[andreasabel]

@nad wrote:

Do the lists necessarily have the same length?

No, ps can be longer as ts as the comment says.

Can you break it? I cannot:

open import Agda.Builtin.Nat

data D : Set where
  c : Nat → Nat → D

mutual
  f : D → Set
  f (c (suc n) 0) = g (c n)
  f (c n (suc m)) = f (c (suc n) m)

  g : (Nat → D) → Set
  g h = f (h 42)

Termination checking failed for the following functions:
  f
Problematic calls:
  f (c (suc n) m)

[andreasabel]

{-# OPTIONS --termination-depth=2 #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

data D : Set where
  c : Nat → Nat → D

mutual
  f : (x : D) → Nat
  f (c (suc n) 0) = g (c n)
  f (c n (suc (suc m))) = f (c (suc n) m)
  f _ = zero

  g : (h : Nat → D) → Nat
  g h = f (h 2)

loop : f (c 1 0) ≡ zero
loop = refl

Loops.

[andreasabel]

And leads to inconsistency:

{-# OPTIONS --termination-depth=2 #-}

data ⊥ : Set where
record ⊤ : Set where

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

{-# BUILTIN NATURAL Nat #-}

data _≡_ (A : Set) : Set → Set₁ where
  refl : A ≡ A

cast : ∀{A B : Set} → A ≡ B → A → B
cast refl x = x

cast⁻¹ : ∀{A B : Set} → A ≡ B → B → A
cast⁻¹ refl x = x

-- Exploit the termination checker bug to prove ⊥.

data D : Set where
  _,_ : Nat → Nat → D

P : D → Set
P (suc _ , _)           = ⊥
P (_     , suc (suc _)) = ⊥
P (0 , 0) = ⊤
P (0 , 1) = ⊤

-- This does not hold definitionally (no exact split), so prove it.
lem : ∀ n {m} → P (n , suc (suc m)) ≡ ⊥
lem 0       = refl
lem (suc n) = refl

mutual
  f : (x : D) → P x
  -- The loop:
  f (suc n , _)           = cast   (lem n) (g (n ,_))       -- this call to g is fishy!
  f (n     , suc (suc m)) = cast⁻¹ (lem n) (f (suc n , m))
  -- Base cases:
  f (0 , 0) = record{}
  f (0 , 1) = record{}

  g : (h : Nat → D) → P (h 2)
  g h = f (h 2)

loop : ⊥
loop = f (1 , 0)

I can trace this issue back to at least Agda 2.4.2.4 (my oldest Agda).

[nad]

The use of zipWithM dates to 2013 (aa2eb80).

[andreasabel]

Yeah, now one stumbled over this in 9 years, given the counterexample is contrived and requires --termination-depth=2.