<div dir="ltr"><div>Hi,</div><div> </div><div>I&#39;m trying to compile the following two modules in 2.4.2.3, but for some reason the second one does not pass the termination checker due to the recursive call in olist-sorted. If I include the content of the first module instead of importing it, then it does pass the termination checker. If I remove the parameters from both modules and I postulate them in a third one (which would be imported by both modules), then I&#39;m also able to pass the termination checker.</div><div> </div><div>Is there any way to make such parameterized modules pass the termination checker in 2.4.2.3? It used to work in 2.3.2.2.</div><div> </div><div><div>Thanks in advance,</div><div> </div><div>Bruno</div><div> </div></div><div> </div><div>Bound.agda</div><div>----------------</div><div> </div><div>module Bound {A : Set}(_&lt;=_ : A -&gt; A -&gt; Set) where</div><div> </div><div>data Bound : Set where<br>  bot : Bound <br>  val : A -&gt; Bound</div><div> </div><div>data LeB : Bound -&gt; Bound -&gt; Set where<br>  lebx : {b : Bound} -&gt; LeB bot b<br>  lexy : {a b : A} -&gt; a &lt;= b -&gt; LeB (val a) (val b)</div><div> </div><div> </div><div>OList.agda</div><div>---------------</div><div> </div><div>module OList {A : Set}(_&lt;=_ : A -&gt; A -&gt; Set) where</div><div> </div><div>open import Data.List<br>open import Bound _&lt;=_</div><div> </div><div>data OList : Bound -&gt; Set where<br>  nil : {b : Bound} -&gt; OList b<br>  cons : {b : Bound}{x : A} -&gt; LeB b (val x) -&gt; OList (val x) -&gt; OList b</div><div> </div><div>forget : {b : Bound} -&gt; OList b -&gt; List A<br>forget nil = []<br>forget (cons {x = x} _ xs) = x :: forget xs</div><div> </div><div>data Sorted : List A -&gt; Set where<br>  empty : Sorted []<br>  single : (x : A) -&gt; Sorted (x :: [])<br>  step : {x y : A}{ys : List A} -&gt; x &lt;= y -&gt; Sorted (y :: ys) -&gt; Sorted (x :: y :: ys)</div><div> </div><div>olist-sorted : {b : Bound}(xs : OList b) -&gt; Sorted (forget xs)<br>olist-sorted nil = empty<br>olist-sorted (cons {x = x} _ nil) = single x<br>olist-sorted (cons b&lt;=x (cons (lexy x&lt;=y) ys)) = step x&lt;=y (olist-sorted (cons (lexy x&lt;=y) ys))</div></div>