Cannot prove termination of functions on mutually recursive types

[facundominguez]

I don't know how to convince LH that function f is terminating in the following program.

module Test where

data X = X Y
data Y = Y0 | Y X

f :: X -> Int
f (X y) = 1 + g y -- isn't y smaller than (X y)?

g :: Y -> Int
g Y0 = 0
g (Y x) = f x -- isn't x smaller than (Y x)?

The recursion does look structural, but LH does not agree.

This is likely related to #1685.

[ranjitjhala]

@nikivazou understands the mutual recursion thing better than me :-)

[nikivazou]

Well, I do not think you can....
LH does not check structural termination for mutually defined functions (maybe this can change in the implementation of the structural termination checker).

You could define metrics (the way I "understand" better, as Ranjit says) but for that, you need to define a measure that maps X and Y to natural numbers. These metrics (since they will also be mutually recursive) is no way to prove them terminating...