From:

No type variable 'ex14#

to:

Type error:
[../and_let_bool.sail]:6:19-50
6 |  and_bool(let y : bool = x in not_bool(y), x)
  |           ^-----------------------------^
  | The type variable 'ex14# would leak into an outer scope.
  |
  | Try adding a type annotation to this expression.
  | This error was caused by:
  | [../and_let_bool.sail]:6:23-24
  | 6 |  and_bool(let y : bool = x in not_bool(y), x)
  |   |               ^
  |   | Type variable 'ex14# was introduced here
  |

When returning a type from a letbinding we need to be careful that the
type it returns does not refer to any type variable that only exists for
the lifetime of the letbinding (because it was bound by it). Normally
this fails because any type variable bound in the inner letbinding won't
exist in the outer scope, but if it is shadowed this can cause an issue.

The following is therefore always forbidden

```
scattered union U

enum E = A | B | C

union clause U = Ctor : E
```

We attempt to detect when this occurs and include a hint indicating the
likely reason why a 'Undefined type E' error might occur in this
circumstance

Ensure we give a nice error message that explains that recursive types are forbidden

```
Type error:
[struct_rec.sail]:3:10-11
3 |  field : S
  |          ^
  | Undefined type S
  | This error was caused by:
  | [struct_rec.sail]:2:0-4:1
  | 2 |struct S = {
  |   |^-----------
  | 4 |}
  |   |^
  |   | Recursive types are not allowed
```

The theorem prover backends create a special register_value union that
can be recursive, so we make sure to special case that.