`Include` duplicates typeclass instances

[RalfJung]

Example due to @robbertkrebbers:

Class Foo (n : nat) := {}.

Module foo.
  Global Instance foo_S n : Foo n -> Foo (S n) := {}.

  (* fails immediately *)
  Goal Foo 100. Fail apply _. Abort.
End foo.

Module bar.
  Include foo.

  (* takes forever *)
  Goal Foo 100. Timeout 10 apply _. Abort.
End bar.

The expected behavior is that Include brings names and other things like notations into scope, but doesn't duplicate typeclass hints. But instead we get duplicate hints which leads to backtracking which makes that failing TC search take exponential time.

With its current behavior, Include is unfortunately entirely unusable for any typeclass-using development.

[ppedrot]

This is basically a duplicate (ahah) of #6731. Unfortunately it's not completely clear how to make this work in so far as the hints are not exactly the same, they have different constant names (for those that are part of the module). We could factorize hints with the same canonical name but it may result in weird behaviours due to that.

[ppedrot]

The good news is that the work mentioned in #6731 is over already so this is easy to implement and test for issues.

[RalfJung]

What does Include do with inductives? Does it also duplicate them so they become mutually inconvertible?

[RalfJung]

@Janno also points out a possible work-around -- make foo a Module Type rather than a Module.

Class Foo (n : nat) := {}.

Module Type foo.
  Global Instance foo_S n : Foo n -> Foo (S n) := {}.

  (* fails immediately *)
  Goal Foo 100. Fail apply _. Abort.
End foo.

Module bar.
  Include foo.

  (* this still fails immediately. *)
  Goal Foo 100. Fail apply _. Abort.
End bar.

[SkySkimmer]

It seems there is already some deduplication since we don't get the slowdown if the instance is export and we import the module twice. Maybe we can make that deduplication be up to canord?

EDIT the dedup is based on "uid" which gets substituted to a new uid with Include