I was trying a simple example from the beginning of Chlipala's CPDT book like

```
Inductive type : Set := Nat | Bool.
Inductive tbinop : type -> type -> type -> Set :=
| TPlus : tbinop Nat Nat Nat
| TMult : tbinop Nat Nat Nat
| TEq : forall (t : type), tbinop t t Bool
| TLe : tbinop Nat Nat Bool.
Definition eqb (a b : bool) : bool := negb (xorb a b).
Definition typeDenote (t : type) : Set :=
match t with
| Nat => nat
| Bool => bool
end.
Definition tbinopDenote {t1 t2 t : type} (op : tbinop t1 t2 t) : (typeDenote t1) -> (typeDenote t2)-> (typeDenote t) -> Set :=
match op with
| TPlus => Nat.add
| TMult => mult
| TEq Nat => Nat.eqb
| TEq Bool => eqb
| TLe => Nat.ltb
end.
```

But I got an error at the first pattern (any pattern actually. Had tried chaning the order patterns) of `tbinopDenote`

.

```
In environment
t1 : type
t2 : type
t : type
op : tbinop t1 t2 t
The term "Nat.add" has type "nat -> nat -> nat"
while it is expected to have type
"typeDenote ?t@{t5:=Nat} ->
typeDenote ?t0@{t6:=Nat} -> typeDenote ?t1@{t7:=Nat} -> Set".
```

I thought stuff like `?t@{t5:=Nat}`

meant that there is a value `t`

whose possible value is `Nat`

. But if that was so, it's the only possibility and coq would've inferred it so I guess I'm wrong about that.

How can this error be fixed?

I thought stuff like ?t@{t5:=Nat} meant that there is a value t whose possible value is Nat

no, it means there is a value `t`

which can use the variable `t5`

and is used with `t5`

set to `Nat`

so both `?t := t5`

and `?t := Nat`

would work

in this case coq is smart enough to pick the first one, but your type is wrong because you put `-> Set`

Ah.. I hadn't noticed the type was different.. :sweat_smile: :grimacing:

```
it means there is a value `t` which can use the variable `t5` and is used with `t5` set to `Nat`
```

So `t5`

is just a placeholder? `?t@{t5:=Nat}`

could also be just `?t@{Nat}`

?

we don't print the accessible variables when they're the same as the ones in the context so it's really `?t@{t1:=t1;t5:=Nat}`

you can see it with `Set Printing Existential Instances.`

Thanks.

Ju-sh has marked this topic as resolved.

Last updated: Jun 16 2024 at 01:42 UTC