Overzealous positivity checker?
On the following example, Why3 complains about a non strictly positive occurrence of t
, but I don't understand why it is problematic.
use int.Int
type t = { x : int }
with u = { y : t -> int; }
Obviously, in this simplified example, the recursive type definition is not needed, so there is an easy workaround. But in my general usecase (translating C programs to WhyML, including forward struct declarations and structs containing pointers to other structs), I will need recursive type definitions and this workaround will not apply. I don't understand the positivity criterion well enough to understand if what I'm doing is actually problematic or if the checker is being overzealous. @paskevyc maybe you can enlighten me?