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 annotationtemp:xis telling Unison thattemphas the typexwhich is bound in the type signature, sotempandahave the same type.

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

temp : xrefers to the typexin the outer scope.

To explicitly shadow a type variable in scope, the variable can be reintroduced in the inner scope by aforallbinder, 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 variablexin the type ofidgets instantiated to two different types. 42instantiates it toNat,thenid a,instantiates it to the outer scope's typex.