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:x
is telling Unison thattemp
has the typex
which is bound in the type signature, sotemp
anda
have the same type.
ex1 : x -> y -> x
ex1 a b =
temp : x
temp = a
a
temp : x
refers to the typex
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 variablex
in the type ofid
gets instantiated to two different types. FirstFunction.id 42
instantiates it toNat
,thenid
a
,instantiates it to the outer scope's typex
.