Support universe polymorphism

[mtzguido]

This:

assume val ty : Type

```pulse
fn test (x : ty)
  requires emp
  returns x:int
  ensures emp
{
  1
}

Fails with

Could not infer implicit arguments in x: ty -> stt int emp (fun _ -> emp) (in file <dummy>)

[mtzguido]

Running in the CLI also shows this:

(Error 339) Internal error: unexpected unresolved (universe) uvar in deep_compress: 7
<dummy>(0,0-0,0): (Error) Could not infer implicit arguments in x: Bug.ty -> Pulse.Lib.Core.stt Prims.int Pulse.Lib.Core.emp (fun _ -> Pulse.Lib.Core.emp)

and specializing to Type0 makes it work.

[nikswamy]

The issue here is that Pulse does not support universe polymorphic definitions. We should at least provide a better error.