vars a, b : Type

free type Pair a b ::= Pair (fst : a; snd : b)

op f(a : a; b : b) : Pair a b = Pair (a, b);

op g : Pair a b ->? a

program g (Pair (a, b)) = a;

type

Pair : Type -> Type -> Type

vars

a : Type %(var_1)%;

b : Type %(var_2)%

op Pair : forall a : Type; b : Type . a * b -> Pair a b

%(constructor)%

op f : forall a : Type; b : Type . a * b -> Pair a b

%[op=

\ ((var a : a), (var b : b))

.! (op Pair : forall a : Type; b : Type . a * b -> Pair a b)[a, b]

((var a : a), (var b : b))

as Pair a b]%

op fst : forall a : Type; b : Type . Pair a b -> a

%(selector of constructor(s)

Pair : forall a : Type; b : Type . a * b -> Pair a b)%

op g : forall a : Type; b : Type . Pair a b ->? a %(op)%

op snd : forall a : Type; b : Type . Pair a b -> b

%(selector of constructor(s)

Pair : forall a : Type; b : Type . a * b -> Pair a b)%

forall a : Type; b : Type; x_1_1 : a; x_1_2 : b

. fst (Pair (x_1_1, x_1_2)) = x_1_1 %(ga_select_fst)%

forall a : Type; b : Type; x_1_1 : a; x_1_2 : b

. snd (Pair (x_1_1, x_1_2)) = x_1_2 %(ga_select_snd)%

free type Pair(a : Type)(b : Type) ::= Pair (fst : a; snd : b)

%(ga_Pair)%

forall a : a; b : b . f (a, b) = (Pair (a, b) as Pair a b)

%(def_f)%

program (g : Pair _v22_a _v23_b ->? _v22_a)

((Pair : _v22_a * _v23_b -> Pair _v22_a _v23_b) (a, b) :

Pair _v22_a _v23_b)

: _v22_a

= a %(pe_g)%

*** Error 8.24, in term 'program (op g : forall a : Type; b : Type . Pair a b ->? a)[_v22_a,

_v23_b]

((op Pair : forall a : Type; b : Type . a * b -> Pair a b)[_v22_a,

_v23_b]

(a, b))

= a'

are uninstantiated type variables '[_v22_a, _v23_b]'

### Hint 6.8-6.17, repeated declaration of 'g' with type 'Pair a b ->? a'