Deriving hasEq predicate for inductive types, and types of equalities in F*

Reference issue#510.

Basic scheme

Consider a type t as follows:

type t (a:Type) (b:Type) =
  | C: x_i:t_i -> t a b

One candidate for hasEq predicate for type t could be:

forall (a:Type) (b:Type). (forall (x_i:t_i). /\_i hasEq t_i) ==> hasEq t a b

This basically says that if we can prove hasEq for all the field types t_i, then hasEq also holds for t. While this seems fine, there is an issue with instantiating the forall quantifiers in Z3. Specifically, what should be triggers for the quantifiers above ?

For the outermost quantifier, the trigger t a b seems a good candidate.

forall (a:Type) (b:Type). {:pattern (hasEq t a b)}. (forall (x_i:t_i). /\_i hasEq t_i) ==> hasEq t a b

But there does not seem to be a good candidate for the inner quantifiers.

Aside: This scheme also does not handle recursive types (such as lists), although that could be fixed by assuming hasEq (t a b) before trying to prove a recursive (or mutually recursive) type.

Take 2, avoiding the inner quantifiers

One way to avoid the inner quantifiers, is to only check for hasEq of a and b in the left side of the implication above, i.e.

forall (a:Type) (b:Type).{:pattern (hasEq t a b)} (hasEq a /\ hasEq b) ==> hasEq (t a b)

While this gets rid of the inner quantifiers, it adds an additional obligation of proving soundness w.r.t the constructor arguments. In particular, we need to prove that if hasEq a and hasEq b hold, then hasEq also holds for all the t_i.

To do this, before we generate the hasEq predicate above, we check the following for each t_i. Say, G is the current type environment. Then, we check that:

G, a:Type, b:Type, hasEq a, hasEq b, x_(i - 1):t_(i - 1) |= hasEq t_i

where x_(i - 1):t_(i - 1) are all the constructor arguments before x_i:t_i.

To handle recursive types, we also throw in the axiom in the context.

G, a:Type, b:Type, hasEq a, hasEq b, forall (a:Type) (b:Type).{:pattern (hasEq t a b)} (hasEq a /\ hasEq b) ==> hasEq (t a b), x_(i - 1):t_(i - 1) |= hasEq t_i

Once this succeeds for each t_i, the typechecker will add the hasEq predicate for type t in the context.

Take 3: Generalizing the scheme to term parameters

In the scheme above, we may not always generate well-typed terms if type parameters are terms. For example:

type t (n:nat) =
  | C: x_i:t_i -> t n

Recall the type of hasEq:

assume type hasEq: Type -> GTot Type0

If we follow the scheme for type t, we would generate the predicate:

forall (n:nat). hasEq n ==> hasEq (t n)

which is ill-typed since hasEq n is ill-typed.

To solve this, we can check that if (a:t) is a type parameter, and t <: Type(u) for some universe u, only then we add hasEq a to the left side of the implication in the hasEq predicate. So, for the type t with parameter n above, we would generate the following predicate:

forall (n:nat). hasEq (t n)

But, also note that our soundness checks would be:

G, n:nat, x_(i - 1):t_(i - 1) |= t_i

As another example, consider the following type:

type t (a:Type) (x:a) =
  | C: x_i:t_i -> t a x

In this example, in type environment G, a:Type, for the type parameter x:a, it is not always the case that a <: Type(u). Therefore, we would not add hasEq x in the predicate and in the environment for soundness checks.

noeq qualifier

If programmer writes a type for which the soundness checks for hasEq fail, F* would raise an error. To fix it, the programmer should either fix the type definition, or use the noeq qualifier with the type definition.

noeq type t =
  |C: f:(nat -> nat) -> t

If the noeq qualifier is specified, the typechecker will not attempt to generate the hasEq predicate for the type. Of course, this also means that the programmer cannot check terms of the type for decidable equality (alternative is to use propositional equality ==).

Indexed types

Extending the above scheme to handle indexed types is straightforward. For example, for the type below:

type t (a:Type) : Type -> Type =
  |C: x:a -> t a nat

We simply ensure that the hasEq predicate that we generate is well-formed. In particular, in addition to adding the forall quantifiers for the type parameters, we also add forall quantifiers for the indexes. So, for type t above, we would generate hasEq axiom as:

forall (a:Type) (b:Type). {:pattern (hasEq (t a b))} hasEq a ==> hasEq (t a b)

While the soundness check would be:

G, a:Type, hasEq a, (forall (a:Type) (b:Type). {:pattern (hasEq (t a b))} hasEq a ==> hasEq (t a b)
)) |= hasEq a

Different types of equalities in F*

With this change, the = operator usage will be restricted to types for which hasEq is valid. Equality for other types will have to use the propositional equality of F*, whose current type is as follows:

val (==) : #a:Type -> a -> a -> Tot Type0

In summary, F* has the following equality types:

val (=)  : #a:Type{hasEq a} -> a -> a -> Tot bool
val (==) : #a:Type -> a -> a -> Tot Type0
val (===): #a:Type -> #b:Type -> a -> b -> Tot Type0

Note that == is homogeneous propositional equality, while === is heterogeneous propositional equality.