Scoped type variables

Type variables introduced by a type signature for a term remain in scope throughout the definition of that term.

For example in the following snippet, the type annotation temp:x is telling Unison that temp has the type x which is bound in the type signature, so temp and a have the same type.

ex1 : x -> y -> x
ex1 a b =
  temp : x
  temp = a
  a

temp : x refers to the type x in the outer scope.

To explicitly shadow a type variable in scope, the variable can be reintroduced in the inner scope by a forall binder, as follows:

ex2 : x -> y -> x
ex2 a b =
-- doesn’t refer to x in outer scope
id : ∀ x . x -> x
id v = v
temp = id 42
id a

id : ∀ x . x -> x doesn’t refer to x in outer scope

Note that here the type variable x in the type of id gets instantiated to two different types. First Function.id 42 instantiates it to Nat, then id a, instantiates it to the outer scope's type x.