Universe constraints not properly checked against some annotations

```
module Test
type sigma (p:Type -> Type) =
| MkSigma : a:Type -> p a -> sigma p
let id (a:Type) = a
let heap = nat -> Tot (option (sigma id))
let h0 : heap = //this seems to infer universes correctly, but doesn't check that it is compatible with the annotation
fun n -> Some (MkSigma #id (heap -> Tot unit) (fun h -> ()))
let f (x:heap) = unit
let g = f h0 //this leaves an unresolved universe variable allowing it to check incorrectly
```

Note, the following variation with an explicit `Type0` is rejected correctly:

```
module Test
type sigma (p:Type -> Type) =
| MkSigma : a:Type -> p a -> sigma p
let id (a:Type0) = a //notice the Type0 explicit ascription
let heap = nat -> Tot (option (sigma id))
let h0 : heap = //this rightfully fails
fun n -> Some (MkSigma #id (heap -> Tot unit) (fun h -> ()))
```

Reproduce the two `Test` modules in the issue, comparing the inferred-universe version with the explicit `Type0` variation. Start at the compiler's universe-constraint checking path and trace why the `heap` annotation is accepted; done means the first example is rejected consistently with the explicit `Type0` case.

Written by the indexing model from the issue text.