The Coq mailing list

[Clément Pit-Claudel <cpitclaudel AT gmail.com>]

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"?