Universe name leak between val and let

[mtzguido]

trafficstars

This snippet leaks a U_name in the checked file, apparently since the val is universe-polymorphic, but the let is not.

module U

#set-options "--lax"

assume val f : t:Type u#b -> Type0

val downgrade_val_raise_val (a : Type0) (x : a) : Lemma (f (a -> Type u#b))
let downgrade_val_raise_val (a : Type0) (x : a) =
  // let _ = Type u#b in
  ()

Looking at the output of --dump_module, with enough flags:

val U.downgrade_val_raise_val <b> : (a#47:Type u#(0) -> ...
visible let  U.downgrade_val_raise_val <> : (a#116:Type u#(0) -> ...

Somehow this only happens in lax mode. Uncomment the letbinding makes it work, since the desugarer will take care of finding the free universe name and quantifying over it.

Found this while trying to make the deep_compress checks more defensive. Reminiscent of #604 too.