search

FStarLang / steel

The Steel separation logic library for F*
Apache License 2.0
31 stars 5 forks source link

Support universe polymorphism #72

Open mtzguido opened 1 year ago

mtzguido commented 1 year ago

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 commented 1 year ago

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 commented 11 months ago

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