Improve error messages for unsolved function quantifiers

For example, for a function like

```
val aget_X : forall 'n, 0 <= 'n <= 31. int('n) -> bits(64)

function test(n : int) -> unit = {
  let y = aget_X(n);
  ()
}
```

we get the message

> Could not resolve quantifiers for aget_X (0 <= 'ex7# & 'ex7# <= 31)
>
> Try adding named type variables for n : atom('ex7#)
>
> The property (0 <= n & n <= 31) must hold

which suggests adding a name for the type variable 'ex7#, and gives
the property in terms of the variable n. If we give n a type variable name:

```
val test : int -> unit

function test(n as 'N) = {
  let y = aget_X(n);
  ()
}
```

It will suggest a constraint involving the type variable name

> Could not resolve quantifiers for aget_X (0 <= 'ex6# & 'ex6# <= 31)
>
> Try adding the constraint (0 <= 'N & 'N <= 31)

0 files changed, 0 insertions, 0 deletions