I've typechecked this by hand, and indeed it looks to me as if it should work. (Admittedly, your inAssocL function is making an unsubstantiated claim (since you define it as 'undefined'), but that is still sound since any attempt to run the program will diverge. But it should tpyecheck.) Here is my calculation, for the Cons case of | > revcat :: List a m -> List a n -> List a (Plus m n) | > revcat Nil y = y | > revcat (Cons a x) y = | > subst incAssocL (revcat x (Cons a y)) y :: List a n x :: List a k, where m ~ Suc k Cons a y : List a Suc n revcat x (Cons a y) :: List a (Plus k (Suc n)) subst inAssocL (revcat x (Cons a y)) :: List a (Plus (Suc k) n) So to make the result type match up with the type of the RHS we need m ~ Suc k => List a (Plus m n) ~ List a (Plus (Suc k) n) which is of course the case. Manuel has made some recent changes -- I have not seen if they fix this. Simon