The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

Existing Instance did the trick. Thanks Clément!

Shall I file this as a bug?

Vadim

--

Vadim Zaliva  

CMU ECE Ph.D. candidate

Mobile/Signal/WhatsApp: +1(510)220-1060

On Tue, Nov 19, 2019 at 5:28 AM Clément Pit-Claudel <cpitclaudel AT gmail.com> wrote:

On 2019-11-18 21:07, Vadim Zaliva wrote:
> 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. |

Try "Existing Instance Et"?