The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

> On 12.10.2017 18:45, Pierre Courtieu wrote:
>
> There is another problem with this:  Include will duplicate typeclass
> instances.  We have had problems with exponential blowup of typeclass
> search due to this.

Good point.

> Though maybe the fact that Module Types and nod just Module is involved
> here makes a difference?

I don't know.

>>   Parameter g : nat -> TSS.A.
> [snip]
>>   Definition g : nat -> nat := g_helper.
>
> Also, the type of g is duplicated.  Ideally, it should be possible to
> seal g without duplicating its type.

If I understand well you would like to do:

Definition g.

and have the goal nat -> nat automatically.

That is not the way things work internally I guess but it deserves a
feature wish imho. It could be implemented as a way to tell a type as
the type of something else.

P.

> Kind regards,
> Ralf