[Agda] two questions on type checker

[Jason -Zhong Sheng- Hu]

I guess a rule of thumb is to provide a clear indication of the decreasing structure syntactically in order to please termination checker. There aren't many reasons why such check fails, so I personally don't find it's too bad. Though, I do wish I can specify what is the decreasing structure in some occasions.

Sincerely Yours,

Jason Hu
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Sergei Meshveliani <mechvel at botik.ru>
Sent: September 24, 2018 8:50 AM
To: agda at lists.chalmers.se
Subject: [Agda] two questions on type checker

Dear Agda developers

I have two notes on a code of kind

----------------------------------------------------
lemma' y (x ∷ x' ∷ xs) _ i@(suc k , 1+k<|xx'xs|) =
  begin
    ...
    lookup' (x' ∷ xs) (k , k<|x'xs|)
                    ≡⟨ lemma' y x'xs 0<|x'xs| (k , k<|x'xs|)
    ...
  where
  x'xs = x' ∷ xs
  ...
----------------------------------------------------

Agda 2.6.0-05e8112  reports

-----------------
Termination checking failed for the following functions:
  lemma'
Problematic calls:
  lemma' y (x'xs y x x' xs x₁ k 1+k<|xx'xs|)
  (0<|x'xs| y x x' xs x₁ k 1+k<|xx'xs|)
  (k , k<|x'xs| y x x' xs x₁ k 1+k<|xx'xs|)
  ...
------------------

First, the print-out of the  lemma'  call in the message differs greatly
from the source code. Blanks inserted into identifiers, `∷' skipped etc.

Second, with expanding  x'xs  to (x' ∷ xs)  in the recursive call, Agda
sees termination.
Many users will not guess to do this expansion and will spend effort
trying to provide a wise termination proof.
If it is problematic to fix the feature, may be, Agda could issue some
hints after the message about termination - ?

Regards,

------
Sergei

_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180924/6e481022/attachment.html>