[Agda] two questions on type checker

[Sergei Meshveliani]

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