## Stream: Coq users

### Topic: ✔ Error in typeDenote function

#### Julin Shaji (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 Shaji (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: Jun 16 2024 at 01:42 UTC