How to declare a hasEq constraint?

Question

I'm just starting out with F*, by which I mean I've written a few lines along with the tutorial. So far it's really interesting and I'd like to keep learning.

The first thing I tried to do on my own was to write a type that represents a non-empty list. This was my attempt:

type nonEmptyList 'a = l : (list 'a) { l <> [] }

But I get the error

Failed to verify implicit argument: Subtyping check failed; expected type (a#6468:Type{(hasEq a@0)}); got type Type

I know I'm on the right track though because, if I constrain my list type to containing strings, this does work:

type nonEmptyList = l : (list string) { l <> [] }

I'm assuming this means that l <> [] in the original example isn't valid because I haven't specified that 'a should support equality. The problem is that I cannot for the life of me figure out how to do that. I guess is has something to do with a higher kind called hasEq, but trying things such as:

type nonEmptyList 'a = l : (list 'a) { hasEq 'a /\ l <> [] }

hasn't gotten me anywhere. The tutorial doesn't cover hasEq and I can't find anything helpful in the examples in the GitHub repo so now I'm stuck.

Answer 1

You correctly identified the problem here. The type 'a that you used in the definition of nonEmptyList is left unspecified and therefore could not support equality. Your intuition is correct, you need to tell F* that 'a is a type that has equality, by adding a refinement on it:

To do that, you can write the following:

type nonEmptyList (a:Type{hasEq a}) = l : (list a) { l <> [] }

Note that the binder I used for the type is a and not 'a. It would cause a syntax error, it makes more sense because it isn't "any" type anymore. Also, note that you can be even more precise and specify the universe of the type a as Type0 if needbe.