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

[Guillaume Allais]

Just had the same experience. Note that turning `Gas` into a record
rather than a datatype definition solves this problem.

On 16/07/2019 00:05, Dan Krejsa wrote:
> 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
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190806/c97aef8c/attachment.sig>