CODEWITHSUNDEEP
coq
lynn
lynn

Reputation: 10784

Coq type error when matching with type family

I’m trying to re-implement an example from CPDT from memory. I wrote:

Inductive myType : Set := MyNat | MyBool.

Definition typeDenote (t : myType) : Set :=
  match t with
    | MyNat => nat
    | MyBool => bool
  end.

Inductive unaryOp : myType -> myType -> Set :=
| Twice : unaryOp MyNat MyNat.

Definition twice (n:nat) : nat := n + n.

Definition tunaryDenote (a b : myType) (t : unaryOp a b)
    : typeDenote a -> typeDenote b :=
  match t with
  | Twice => twice
  end.

The resulting error is:

Toplevel input, characters 125-130
>   | Twice => twice
>              ^^^^^
Error: In environment
a : myType
b : myType
t : unaryOp a b
The term "twice" has type "nat -> nat" while it is expected to have type
 "forall H : typeDenote ?141, typeDenote ?142"

I don’t understand this error message. I would think that once the match on Twice : unaryOp MyNat MyNat succeeds, Coq infers that a and b are MyNats, and thus typeDenote a -> typeDenote b ≡ nat -> nat, making twice a perfectly fine candidate for the return value. Where’d I go wrong?

Upvotes: 2

Views: 131

Answers (3)

lynn
lynn

Reputation: 10784

I tried a newer version of Coq, and like others have said, it typechecks without issue on Coq 8.5. :)

Upvotes: 0

gallais
gallais

Reputation: 12103

Just like @AntonTrunov said, it is typechecked without any issue on my Coq 8.5pl1. However if you need to add some extra annotations for your version to accept the function, you want to have a look at this section of the manual to figure out what to do.

My guess is that you want to have a match ... in ... return ... with to say that the return type should be refined by the information obtained by matching t at the type unaryOp a b (indeed: a and b will take concrete values in the Twice branch).

This is the definition you get using that technique:

Definition tunaryDenote (a b : myType) (t : unaryOp a b)
    : typeDenote a -> typeDenote b :=
  match t in unaryOp a b return typeDenote a -> typeDenote b with
  | Twice => twice
  end.

Upvotes: 1

Elazar
Elazar

Reputation: 21595

I think that the answer is that Coq's type inference is limited, and does not do the reasoning you want it to do.

Coq's type inference does not do arbitrary calculation but simple unification. It looks at twice, understand that it is nat->nat and concludes that it is not (syntactically) of the form typeDenote a -> TypeDenote b.

If it was doing calculation, it was likely to be non-terminating, since its type system is very sophisticated so you can encode non-trivial computation there.

Upvotes: 0

Related Questions