Coq中Type Class访问器失效：是设计决策还是用法错误？

Great question—you’re right that type classes in Coq are built on top of records, but there’s a key difference in how their projections (accessors) are intended to be used, which is causing your confusion. Let’s break this down step by step.

Why the Record Version Works #

Your record example works because getter_r is a standard function that leverages implicit arguments (thanks to Set Implicit Arguments):

1. It takes an implicit type parameter A_r, which Coq infers automatically from the record value.
2. It takes a concrete record value of type Foo_r A_r.

When you call getter_r foo_r, Coq sees foo_r is of type Foo_r nat, so it fills in A_r = nat for you, and the call resolves correctly.

Why the Type Class Version Fails #

At first glance, getter_t looks identical to getter_r in its signature, but there’s a critical design difference: type class projections are optimized for implicit instance resolution, not explicit instance passing.

When you wrote Compute (getter_t foo_t), Coq throws an error because:

• The first parameter of getter_t is A_t : Type (explicit by default for type classes, even with Set Implicit Arguments).
• You’re passing foo_t, which is a term of type Foo_t nat—not a Type—so Coq can’t unify these to infer A_t.

Fixing the Type Class Call #

You have a few options to make the type class version work:

1. Explicitly Pass Both Arguments #

Since getter_t expects a type first, then an instance, you can call it directly with both parameters:

Compute (getter_t nat foo_t). (* Returns 2::nil *)

2. Match Record Behavior with Implicit Arguments #

You can adjust the implicit arguments for getter_t to mirror the record’s behavior:

Arguments getter_t {A_t} _.
Compute (getter_t foo_t). (* Now works exactly like the record version *)

3. Use Idiomatic Type Class Resolution #

The intended way to use type class projections is to let Coq find the instance automatically based on type context. For example:

Compute (getter_t : list nat). (* Coq automatically resolves the foo_t instance for nat *)

In larger terms where A_t is already inferred, Coq will resolve the instance without any extra input from you.

Conceptual Design Decision #

This isn’t a bug—it’s a deliberate choice. Type classes are designed to enable ad-hoc polymorphism, where Coq selects the right instance based on the types in your term. By prioritizing implicit resolution over explicit instance passing, Coq encourages this idiomatic workflow rather than treating instances as regular values to pass around.

While type classes are technically records under the hood, their projections are optimized for this implicit resolution pattern. You can force them to behave like record accessors (as shown in option 2), but that’s not the primary use case the Coq team had in mind.

内容的提问来源于stack exchange，提问作者Zheng Cheng