Hello Agda Users,<br><br>Recently (about a week ago) I upgraded to the latest development version, I have noticed<br>that a function that used to pass termination check now does not. To start with, I am <br>exploring model checking from Agda as a platform. To this end, I require to represent <br>

infinite paths as
codata. <br><br>Using these codata structures complicates matters (particularly with dependant <br>pattern matching) so inductive data type of a lasso is defined, then a translation <br>from the lasso to infinite paths. It is this translation that is causing problems.<br>
<br>Below is a simplified version of the problem, instead of a lasso, loops are used. I have<br>tested a simpler version that dont require the principle of transfer and these pass the<br>termination check. To the best of my understanding the function loop2path (below)<br>
uses guarded recursion so should pass the check.<br>
<br>Could any one please explain why it applying the proof transfer principle breaks<br>termination? Or is this some kind of bug?<br><br>Best,<br>Karim Kanso<br><br>module coterm where<br><br>open import Data.Nat using (ℕ;suc;zero)<br>
open import Data.Fin using (Fin;suc;zero)<br>open import Relation.Binary.Core using (_≡_;refl)<br><br>transfer : {A : Set} →<br>           (F : A → Set) → <br>           (a b : A) →<br>           (r : a ≡ b) → <br>           (p : F a) →<br>
           F b<br>transfer F .b b refl p = p<br><br>postulate state : ℕ<br>postulate action : Fin state → ℕ<br>postulate transition : (s : Fin state) → <br>                       (a : Fin (action s)) → <br>                       Fin state<br>
<br>data Path : Fin state → Fin state → Set where<br>  end : {s : Fin state} → Path s s<br>  next : {s&#39; : Fin state} → <br>         (s : Fin state) → <br>         (a : Fin (action s)) → <br>         Path (transition s a) s&#39; → Path s s&#39;<br>
<br>codata Path&#39; : Fin state → Set where<br>  next : (s : Fin state) → <br>         (a : Fin (action s)) → <br>         Path&#39; (transition s a) → <br>         Path&#39; s<br><br>data Loop (s : Fin state) : Set where<br>
  loop : {s&#39; : Fin state} → <br>         (l : Path s s&#39;) →<br>         (a : Fin (action s&#39;)) →<br>         (lp : s ≡ (transition s&#39; a)) →<br>         Loop s<br><br>loop2path : {s : Fin state} → Loop s → Path&#39; s<br>
loop2path {s} (loop {s&#39;} l a lp) = aux l a lp<br>  where <br>    aux : {t t&#39; : Fin state} → (l : Path t t&#39;) → (a : Fin (action t&#39;)) → (lp : s ≡ transition t&#39; a) → Path&#39; t<br>    aux {t} {.t} end a&#39; lp&#39; = next t a&#39; (transfer Path&#39; s (transition t a&#39;) lp&#39; (aux l a lp))<br>
    aux {t} (next .t a&#39; y) a lp = next t a&#39; (aux y a lp)<br><br>