Automatically generated val sigelt does not elaborate

[gebner]

From FStar.Buffer.fst:

val contains #a h (b: buffer a) : GTot Type0
let contains #a h (b:buffer a) : GTot Type0 = HS.contains h b.content

In the above, the type of the argument h is unconstrained in the val, so we get an error. (NB, this is a definition and not a lemma.)

[gebner]

Another related way in which this can fail is by missing universe level instantiations, i.e., that a Type might implicitly become a Type0 in a let-definition.

let big_or' #a (f: (a -> Type)) (l: list a) : Type = map_op' l_or f l False
// ^^ Type actually means Type0 here