Failure of termination checking for reflection-generated code due to data projections

[j-towns]

In the following, the function F-to-N passes the termination checker:

open import Agda.Builtin.Reflection
open import Agda.Builtin.List
open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit

data Nat : Set where
  z : Nat
  s : Nat -> Nat

data Fin : Nat -> Set where
  fz : {b : Nat}          -> Fin (s b)
  fs : {b : Nat} -> Fin b -> Fin (s b)

apply : {A B C : Set} (input : A) (f : A -> B) (cont : B -> C) -> C
apply input f cont = cont (f input)

 -- Converts Fin to Nat, PASSES termination checking:
F-to-N : {b : Nat} -> Fin b -> Nat
F-to-N {b} = \ { fz     -> z
               ; (fs x) -> apply x F-to-N \ { x -> s x } }

If we define a trivial macro which quotes and then unquotes the function, it still passes:

macro
  id-macro : {b : Nat} -> (Fin b -> Nat) -> Term -> TC ⊤
  id-macro f hole = 
    bindTC (quoteTC f) \ f-term ->
    unify hole f-term
    

F-to-N-pass : {b : Nat} -> Fin b -> Nat
F-to-N-pass = id-macro (\ { fz     → z
                          ; (fs x) → apply x F-to-N-pass \ { x -> s x } } )

But if we explicitly pass the argument b to the macro, termination checking fails:

 -- FAILS termination checking.
F-to-N-fail : {b : Nat} -> Fin b -> Nat
F-to-N-fail {b} = id-macro {b} (\ { fz     -> z
                                  ; (fs x) -> apply x F-to-N-fail \ { x -> s x } } )

gives the warning

Termination checking failed for the following functions:
  F-to-N-fail
Problematic calls:
  λ { fz → z ; (fs x) → apply x F-to-N-fail (λ { x → s x }) }
  F-to-N-fail

Another way to cause (to me unexpected) termination checking failure is to check the type of f-term in the macro, i.e.

macro
  id-macro-fail : {b : Nat} -> (Fin b -> Nat) -> Term -> TC ⊤
  id-macro-fail f hole = 
    bindTC (quoteTC f) \ f-term ->
    bindTC (inferType hole) \ hole-ty ->
    bindTC (checkType f-term hole-ty) \ f-term ->
    unify hole f-term

 -- again FAILS termination checker
F-to-N-fail-2 : {b : Nat} -> Fin b -> Nat
F-to-N-fail-2 = id-macro-fail (\ { fz     -> z
                                 ; (fs x) -> apply x F-to-N-fail-2 \ { x -> s x } } )

I'm pretty new to Agda, so I don't 100% know what the intended behaviour is/should be here. Are we sure that the original F-to-N functon should pass termination checking?

In my use-case I need to define functions with this structure in a macro, so I very much hope that this is supposed to work and can be fixed.

Thanks in advance for any help.

This issue may be related to/have the same underlying cause as #5747.

I'm using Agda version 2.6.2.2.

[andreasabel]

@j-towns

Are we sure that the original F-to-N function should pass termination checking?

Yes, by virtue of the hidden argument to F-to-N, given explicitly here:

F-to-N : {b : Nat} -> Fin b -> Nat
F-to-N {b} = \ { fz         -> zero
               ; (fs {a} x) -> apply x (F-to-N {a}) \ { x -> suc x } }

[andreasabel]

There is definitely something broken with the macro stuff.
Putting a meta in, solves the meta with ?0 := b and succeeds:

open import Agda.Builtin.Nat
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

data Fin : Nat → Set where
  fz : (b : Nat)         → Fin (suc b)
  fs : (b : Nat) → Fin b → Fin (suc b)

apply : {A B C : Set} (input : A) (f : A → B) (cont : B → C) → C
apply input f cont = cont (f input)

macro
  id-macro : (b : Nat) → (Fin b → Nat) → Term → TC ⊤
  id-macro b f hole =
    bindTC (quoteTC f) λ f-term →
    unify hole f-term

test : (b : Nat) → Fin b → Nat
test b = id-macro ? λ where
  (fz _)   → zero
  (fs a x) → apply x (test a) suc

But if the solution is put in (C-c C-s) and we reload (C-c C-l), we get the termination error:

Termination checking failed for the following functions:
  test
Problematic calls:
  λ { (fz .(Agda.Builtin.Nat.suc-0 _)) → zero
    ; (fs .(Agda.Builtin.Nat.suc-0 _) x)
        → apply x
          (test (Agda.Builtin.Nat.suc-0 (suc (Agda.Builtin.Nat.suc-0 b))))
          suc
    }
  test (Agda.Builtin.Nat.suc-0 (suc b))

Note the garbage Agda.Builtin.Nat.suc-0 which I cannot make sense of, and how the recursive argument to test when from a to Agda.Builtin.Nat.suc-0 (suc (Agda.Builtin.Nat.suc-0 b)).

[andreasabel]

Bisection blames my commit 792a357
Date: Wed Aug 12 16:45:01 2020 +0200
[ fixed #4776 ] refactor: add conDataRecord to ConHead

Instead of relying on (null . conFields) to check for record
constructor, the new component conDataRecord gives this information.

[andreasabel]

Note the garbage Agda.Builtin.Nat.suc-0 which I cannot make sense of,

Ok, this seems to be the "projection" from suc which is used by Cubical Agda:

agda/src/full/Agda/TypeChecking/Rules/Data.hs

Lines 317 to 319 in ca5fb2a

	-- Name for projection of ith field of constructor c is just c-i
	names <- forM [0 .. size fields - 1] $ \ i ->
	freshAbstractQName'_ $ P.prettyShow (A.qnameName c) ++ "-" ++ show i

So, maybe Nat.suc is confused for a record constructor with eta-equality...

[andreasabel]

I stumbled over the following issue when looking for uses of conFields:

• Internal error due to new forcing translation #4528 (comment)

@Saizan wrote:

I'm a bit concerned that the partial datatype projections like Agda.Builtin.List._∷_-0 now seem to be promoted to full projection status (e.g. by inclusion in ConHead), was this a deliberate choice?

So this issue is new forcing translation redux (ping @UlfNorell), and my refactoring only brought the problem to the surface. Indeed, with option {-# OPTIONS --no-forcing #-}, the problem goes away!

I read through the discussion at:

• Internal error due to new forcing translation #4528

I understood the following:

• The forcing translation deliberately produces ill-formed clauses for extended lambdas using the (partial) projections from data constructors.
• These would be printed badly to the user, so there is a workaround keeping the original clauses.
• However, this workaround does not kick in with reflection (I think), where the clauses after the forcing translation are turned to reflected syntax and then back to internal syntax, now officially in their broken status.

Yeah, just don't lean too far out of the window...

[j-towns]

Thanks for looking into it @andreasabel! For now I'll use --no-forcing.

[andreasabel]

2022-06-10 Discussion with Ulf: We could extend the termination checker to count projections from data as decrease.

[andreasabel]

(test (Agda.Builtin.Nat.suc-0 (suc (Agda.Builtin.Nat.suc-0 b))))

Q: Why are the projections not normalized against the constructors? Shouldn't this be just test (Agda.Builtin.Nat.suc-0 b)?
A: Because they are intentionally not Projs but Defs, see ddb8379.

[andreasabel]

Submitted PR to the extent of reducing data projections. This already fixes the issue (at least the OP).

• Fix #5922: reduce data projection applied to data constructor #5950

[j-towns]

Yes, my use case is fixed! Fantastic, thank you.