The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

Example below demonstrates the problem I am having. I would like to define Module Type which is wrapper around a type and carries over an instance of a typeclass for this type.

Then I would like to use it when importing this module.
The direct approach does not work, as shown below. If there is
any way to make Et visible to typeclass resolution mechanism inside FooProperties? It is visible in general, not just to typeclass search:

(* Custom equality relation *)
Class Equiv (T: Type) := equiv: T -> T -> Prop.

(* A module to wrap a type which has `Equiv` instance *)
Module Type Foo.
  Parameter Inline t : Type.
  Context `{Et: Equiv t}.
  (* 'foo_ok' definition works here, as it finds "Et" as an instance of
  "Equiv t" *)
  Lemma foo_ok: forall (x y: t), equiv x y. Admitted.
End Foo.

Module FooProperties (F: Foo).
  Import F.

  (* The following prints:
     Et : Equiv t
   *)
  Check Et.

  (*
    The following fails with the error:

     Error: Unable to satisfy the following constraints:
     In environment: x, y : t
     ?Equiv : "Equiv t"
  *)
  Lemma foo_error: forall (x y: t), equiv x y.

Thanks!

—
Vadim Zaliva
CMU ECE Ph.D. candidate
Mobile/Signal/WhatsApp: +1(510)220-1060