Universes for val generalized independently of the corresponding let

[catalin-hritcu]

Some of the stlc-norm proofs that used to cause F* to blow up because of #577 now fail in subtler ways. I could minimize it to this:

module Bug604

(* Inductive equality on integers *)
noeq type ieq : int -> int -> Type =
| Refl : x:int -> ieq x x

(* Some predicate on integers *)
assume type pred : int -> Type

val steps_preserves_red : e:int -> e':int -> b:ieq e e' -> pred e -> Tot (pred e')
let steps_preserves_red e e' heq hp =
  match heq with
  | Refl e'' -> assert(e == e'' /\ e == e'); (* -- these work fine *)
                hp                           (* -- but this doesn't *)

which fails as follows:

[hritcu@detained bug-reports]$ fstar.exe bug604.fst
./bug604.fst(14,16-14,18) : Error
Expected expression of type "(Bug604.pred e')";
got expression "hp" of type "(Bug604.pred e)"

So in this case F* can apparently prove that e == e', but it still cannot turn a proof of pred e into a proof of pred e'. This seems like a regression.

[catalin-hritcu]

This seems to be caused by universe polymorphism. Replacing Type with Type0 in the type of pred

assume type pred : int -> Type0

makes this work. No longer sure whether this can be blamed on F* or on my bad understanding of universes.

[hritcu@detained bug-reports]$ fstar.exe bug604.fst --print_universes
./bug604.fst(14,16-14,18) : Error
Expected expression of type "(Bug604.pred<n472> e')";
got expression "hp" of type "(Bug604.pred<n471> e)"

[nikswamy]

Can you add --print_universes

I think I see the problem:

When you write a val it is universe generalized independently of its corresponding let, which may appear much later in the file. (this decision is questionable, but that's what it does now)

That means, steps_preserves_red is polymorphic in at 3 universes; 1 for b:ieq, one for the pred e, and one for the result type pred e'.

Of course, the definition is only polymorphic in 2 universes, since the result is in the same universe as hp. Hence the complaint.

There are several fixes:

1. don't use the val, but annotate the let itself. This is my preferred style these days, depite the lurking val declaration + let works differently from the new let (x:t) : M b notation #517, priority 1 bug.
2. we still need to add notation for explicit universe polymorphism, in which case you could write your val with just 2 universes instead of 3. That's a TODO in Work items for the universes release #505.

[catalin-hritcu]

@nikswamy Thanks for explaining. There are a couple of things F* could do better here:

• For a start, it could signal in the error that this is an universe mismatch. Without this the error messages will lead users in the wrong direction.
• It could do the generalization of the val and let together. While I assume that's not easy, universes only really work when they don't unnecessarily get in the way.

[kyoDralliam]

@nikswamy Thanks for the explanations on #689
I still have a problem when I'm trying to do a non-totally-trivial pattern matching afterwards, i.e.

//  Expected expression of type "(#a:Type(?59830) -> uu___:a@0 -> Tot Prims.unit)";
//                      vv
let test_wrong (f: #a:Type -> a -> Tot unit) : Tot unit =
  match Left () with
  | Left _ -> ()
  | Right _ -> ()

[nikswamy]

Hmm. This last bit seems to be an unrelated issue. It has more to do with instantiating implicit arguments in than universes. I'm looking into it ... will probably create a separate issue for it.

[nikswamy]

You should be able to work around it in the mean time by making f's first argument explicit. e.g,

let test_wrong (f: (a:Type -> a -> Tot unit)) : Tot unit =
  match Left #_ #nat () with
  | Left _ -> ()
  | Right _ -> ()

[s-zanella]

Here's a more concise example:

module M
#set-options "--print_universes --print_bound_var_types"

val foo: Type -> Type
let foo t = t

(*
(Error) Expected expression of type "Type('uu___17)"; got expression "t" of type "Type('uu___18)"
*)

As expected, let foo (t:Type) = t works fine.

[kyoDralliam]

A partial fix for this is to be explicit about universes i.e.

val foo: Type 'ua -> Type 'ua
let foo t = t

[mtzguido]

Here's another instance, which does not work even naming the universe in the val.

val poly2 : (#a:Type u#ua -> a -> list a) -> (list int & list bool)
let poly2 f = (f 1, f true)

[mtzguido]

Sorry, that was silly, the problem with the above is that there is no higher-order universe polymorphism. It doesn't work even if one just uses a let. Specializing to Type0 makes it work.

[nikswamy]

Since interfaces are checked and used separately from their definitions, there's no way in the current design to infer the universes annotation of vals while accounting for their corresponding definitions.

Addressing this will require redesigning how interfaces work.