## Stream: Coq users

### Topic: ✔ Error in typeDenote function

#### Julin S (Dec 23 2021 at 09:22):

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
| 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?

#### Gaëtan Gilbert (Dec 23 2021 at 09:29):

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`

#### Julin S (Dec 23 2021 at 09:35):

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}`?

#### Gaëtan Gilbert (Dec 23 2021 at 09:38):

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}`

#### Gaëtan Gilbert (Dec 23 2021 at 09:39):

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

Thanks.

#### Notification Bot (Dec 23 2021 at 10:03):

Ju-sh has marked this topic as resolved.

Last updated: Feb 06 2023 at 12:04 UTC