Unresolved uvar error on just using an unresolved identifier

[nikswamy]

fn test (x:ref bool)
    requires pts_to x true
    returns ctxt:some_random_identifier
    ensures pts_to x true
{
  admit()
}

Fails with

• Tactic logged issue:
• Internal error: unexpected unresolved (universe) uvar in deep_compress: 10

And

• Tactic logged issue:
• Could not infer implicit arguments in
  x: ref bool -> stt some_random_identifier (pts_to x true) (fun _ -> pts_to x true)

[nikswamy]

Addressed by PR #112

some_random_identifier is a free in the annotated type and is then abstracted as an implicit argument. However, this implicit argument has type Type u#a and the unresolved universe variable leads to the failure.

• Previously, since the elaborated type on which F* was called has no range, the entire Pulse function would be blamed. Now, only the type annotation is blamed.

• Also, previously, F* would call deep_compress without checking if there are any unresolved uvars/univ_vars, which would result in a hard failure. That is fixed in F* PR 3084