[Agda] Parameterized modules

[Bruno Bianchi]

Hi,

I'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'm
also able to pass the termination checker.

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.

Thanks in advance,

Bruno


Bound.agda
----------------

module Bound {A : Set}(_<=_ : A -> A -> Set) where

data Bound : Set where
  bot : Bound
  val : A -> Bound

data LeB : Bound -> Bound -> Set where
  lebx : {b : Bound} -> LeB bot b
  lexy : {a b : A} -> a <= b -> LeB (val a) (val b)


OList.agda
---------------

module OList {A : Set}(_<=_ : A -> A -> Set) where

open import Data.List
open import Bound _<=_

data OList : Bound -> Set where
  nil : {b : Bound} -> OList b
  cons : {b : Bound}{x : A} -> LeB b (val x) -> OList (val x) -> OList b

forget : {b : Bound} -> OList b -> List A
forget nil = []
forget (cons {x = x} _ xs) = x :: forget xs

data Sorted : List A -> Set where
  empty : Sorted []
  single : (x : A) -> Sorted (x :: [])
  step : {x y : A}{ys : List A} -> x <= y -> Sorted (y :: ys) -> Sorted (x
:: y :: ys)

olist-sorted : {b : Bound}(xs : OList b) -> Sorted (forget xs)
olist-sorted nil = empty
olist-sorted (cons {x = x} _ nil) = single x
olist-sorted (cons b<=x (cons (lexy x<=y) ys)) = step x<=y (olist-sorted
(cons (lexy x<=y) ys))
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150530/d7785995/attachment.html