Only base types are allowed to appear in the type of a measure, but this is less accurate than it could be, e.g. when dealing with measures that denote the size of a value.

measure len :: [a] -> Int len [] = 0 len (x:xs) = 1 + len xs

Since the type only specifies that len returns an Int, we need to additionally define an invariant on Int.

invariant {v:[a] | (len v) >= 0}

This is a bit tedious when what we really want to write is just

measure len :: [a] -> Nat len [] = 0 len (x:xs) = 1 + len xs

Perhaps there's a good reason to disallow refinements in the return type of a measure, but it isn't apparent to me.