strict positivity check

[aa755msr]

type negativeFunctor : Type -> Type
//type negativeFunctor (a:Type) = a -> Tot nat

type bad =
|Bad : (negativeFunctor bad) -> bad

Abstract functors should not be presumed to be positive. One can provide a negative implementation and violate termination guarantees.

[nikswamy]

Known issue. See the discussion on polarities on other threads. (#65)

[s-zanella]

I think implementing the strict positivity check in universes should be given a higher priority now that it's the default.

This verifies without any warning:

module Bug319

type t =
  | T: f:(t -> Tot False) -> t

let delta = T (fun x -> x.f x)

let omega: False = delta.f delta

val bug: unit -> Lemma False
let bug _ = ()

[aseemr]

@s-zanella , @nikswamy and I have talked about this. The implementation would be very similar to that of the hasEq check. The week after next I will work with @nikswamy to iron out the issues with hasEq, and then hopefully get to positivity.

[s-zanella]

Thanks, nice to hear you're working on it!

[nikswamy]

I could probably implement a simplified, conservative version of the check very quickly, and then we'll get a better check from Aseem later.

There used to be a warning about the missing check ... but it was really noisy since it would complain on every data type definition (rightfully so).

Anyway, I agree with the priority 1.

[aseemr]

Positivity check is in the master branch now. @s-zanella's example above gives an error: (Error) Inductive type Test.t does not satisfy the positivity condition, closing the issue.