Tracking universe unification variables?

[mtzguido]

This code:

val last : (#a:Type u#a) -> l:(list a){Cons? l} -> Tot a
let rec last #a l =
  match l with
  | [hd] -> hd
  | _::tl -> last #a tl

Is checked by F* into:

visible let rec last <uu___244> : 
    #a: Type u#uu__univ_bvar_0 ->
    l: Prims.list u#uu__univ_bvar_1 a {Prims.b2t (Cons? u#uu__univ_bvar_2 #a l)}
  -> Prims.Tot u#uu__univ_bvar_2 a = fun #a l ->
  (match l with
    | Prims.Cons #_ hd (Prims.Nil #_) -> hd
    | Prims.Cons #_ _ tl -> Last.last u#0 #a tl)
  <:
  a

Note how the function is universe polymorphic, but is instead applied to u#0 in the recursive call. The uvar actually remains unresolved, and a line in FStar.TypeChecker.Normalize.norm_universe sets it to 0:

https://github.com/FStarLang/FStar/blob/272994209aaef5afd439a684eca389b952364525/src/typechecker/FStar.TypeChecker.Normalize.fs#L187-L191

I noticed this while trying to remove that shady line.

[mtzguido]

Seems related to #604 since it works correctly without a val.

[mtzguido]

Tracked this down to lookup_qname which was calling inst_tscheme on recursive definitions, when it should have really been returning the exact same set of names on which the function is being defined. Then, typechecking last was returning something like last<?1> of type#a:Type u#some_univ_name -> l:list a{Cons? l} -> a, with ?1 totally unrelated. This happens since last is pushed into the environment as a Binding_lid which is already instantiated, so calling inst_tscheme on it does nothing on its type, but corrupts the concrete universes.

[mtzguido]

I fixed this on master already, but leaving it open since 1) I couldn't really add a regression test, since it was silently succeeding anyway; and 2) for better tracking of universe uvars 3) maybe removing the defaulting to zero (in any case, it shouldn't be done in the normalizer).