[Agda] plfa preservation + progresss => eval termination checking failure in Agda 2.6.1?

[Dan Krejsa]

Hi,

I'm (slowly) working through Philip Wadler's PLFA course.
I happen to be using Agda 2.6.1, from the git 'master' branch at commit
d8449caf816e0c5e13419ee2d3fe32a047ec3db8,
and I ran into a termination checking failure in the 'eval' function in the
Properties.lagda chapter.

This version (from the text)

eval : ∀ {L A}
  → Gas
  → ∅ ⊢ L ⦂ A
    ---------
  → Steps L
eval {L} (gas zero)    ⊢L                             =  steps (L ∎)
out-of-gas
eval {L} (gas (suc m)) ⊢L with progress ⊢L
... | done VL                                         =  steps (L ∎) (done
VL)
... | step L—→M with eval (gas m) (preserve ⊢L L—→M)
...    | steps M—↠N fin                               =  steps (L —→⟨ L—→M
⟩ M—↠N) fin

fails termination checking.  Note that 'Gas' is just a type that holds a
natural number:

data Gas : Set where
  gas : ℕ → Gas

However, if one just replaces Gas with ℕ in the function, the termination
checker is happy:

eval : ∀ {L A}
  → ℕ
  → ∅ ⊢ L ⦂ A
    ---------
  → Steps L
eval {L} zero    ⊢L                             =  steps (L ∎) out-of-gas
eval {L} (suc m) ⊢L with progress ⊢L
... | done VL                                   =  steps (L ∎) (done VL)
... | step L—→M with eval m (preserve ⊢L L—→M)
...    | steps M—↠N fin                         =  steps (L —→⟨ L—→M ⟩
M—↠N) fin

Is this an intentional change in the termination checking?

- Dan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190715/b329a188/attachment.html>