fstar

Mutually Inductive Datatypes with Type Parameters


I am trying to write a declaration of two mutually inductive datatypes that both take a type parameter as arguments as follows:

noeq
type foo 'a =
    | FooA: x: 'a -> foo 'a
    | Foob: y: bar 'a -> foo 'a
and bar 'b =
    | BarA: x: int -> bar 'b
    | BarF: y: foo 'b -> bar 'b

I get an error message that is as follows:

LabeledStates.fst(59,0-64,31): (Error 67) Failed to solve universe inequalities for inductives 1 error was reported (see above)

(where line 59 is the line that includes "type foo 'a")

What does this error mean and what can I do to fix it?

If I remove the type parameters (and give foo.x the type of int, for example) I do not get errors anymore. Similarly, if I just give one of the types a type parameter but not the other, I also do not have errors.


Solution

  • F* isn't capable of inferring universes in cases like this. You can provide explicit universe instantiations, however. For example, here are three possible solutions:

    First, a doubly universe polymorphic one, most general but also possibly quite cumbersome to use

    noeq
    type foo (a:Type u#a) : Type u#(max a b) =
       | FooA: x: a -> foo a
       | Foob: y: bar u#b u#a a -> foo a
    and bar (b:Type u#b) : Type u#(max a b) =
       | BarA: x: int -> bar b
       | BarF: y: foo u#b u#a b -> bar b
    

    A singly universe polymorphic solution, perhaps a bit simpler, though less general:

    noeq
    type foo1 (a:Type u#a) : Type u#a =
       | Foo1A: x: a -> foo1 a
       | Foo1b: y: bar1 u#a a -> foo1 a
    and bar1 (b:Type u#a) : Type u#a =
       | Bar1A: x: int -> bar1 b
       | Bar1F: y: foo1 u#a b -> bar1 b
    

    And, finally, a version specialized to universe 0, probably the easiest to use if it fits your needs, but also least general:

    noeq
    type foo0 (a:Type u#0) : Type u#0 =
       | Foo0A: x: a -> foo0 a
       | Foo0b: y: bar0 a -> foo0 a
    and bar0 (b:Type u#0) : Type u#0 =
       | Bar0A: x: int -> bar0 b
       | Bar0F: y: foo0 b -> bar0 b