强制立即类型类实例解析

Question

有没有办法在使用类型类时强制立即找到特定实例？

是的，现在我在没有可用实例时得到一个存在变量，但我想得到一个错误。

一个简单的例子可以更好地解释我想要实现的目标。我正在尝试通过某些类型的隐式转换获得函数评估。在这种情况下，我只想有一个可能的隐式转换 X' -> X.

Class Evaluation (A B C : Type) : Type :=
  {
    cast_eval : (A -> B) -> C -> B
  }.

Instance DirectEvaluation (A B : Type) : Evaluation A B A :=
  {
    cast_eval := fun f x => f x
  }.

Parameter (X X' X'' Y : Type) (f : X -> Y) (x : X) (x' : X') (x'' : X'') (x_cast : X' -> X).

Instance XDashEvaluation : Evaluation X Y X' :=
  {
    cast_eval := fun ff xx => f (x_cast xx)
  }.

Compute (cast_eval f x).   (* f x *)
Compute (cast_eval f x').  (* f (x_cast x') *)
Compute (cast_eval f x''). (* (let (cast_eval) := ?Evaluation in cast_eval) f x'' *)

有没有办法在调用 (cast_eval f x'') 时出错？

Answer 1

出现错误的一种方法是先创建 Definition：

Definition e := cast_eval f x''.
Compute e.

强制立即类型类实例解析

Enforce immediate typeclass instance resolution

typeclass

coq