FStarLang / pulse

The Pulse separation logic DSL for F*
Apache License 2.0
1 stars 4 forks source link

Incorrect error position for implicit instantiation #36

Open gebner opened 1 month ago

gebner commented 1 month ago

Errors from instantiate_implicits are shown at unrelated locations:

```pulse // error shown here too!
fn foo
  (n : nat) // error shown here: Expected expression of type Type got expression n of type nat
  requires emp
  returns m:nat
  ensures pure (m == n)
{
  id #n // <- but the issue is here
}