Demonstrate how opaque ascription takes hints from the interface, while transparent ascription takes them from bodies

modules_instances.v

Require Import stdpp.base.
Require Import NArith.

(* We omit [Require Import stdpp.numbers.], which already has the [Inhabited]
instances we test here. *)

Module Type X.
  #[global] Instance a : Inhabited nat.
  Proof.
    Fail apply _.
    refine (populate 0).
  Defined.

  Definition c : Inhabited N.
  Proof.
    Fail apply _.
    refine (populate 0%N).
  Defined.
End X.

#[global] Instance b : Inhabited nat.
  Fail apply _.
  Fail apply X.a.
Abort.

Module functor (x : X).
  #[global] Instance b : Inhabited nat.
  Proof.
    apply x.a.
    Restart.
    apply _.
  Abort.

  #[global] Instance d : Inhabited N.
  Proof.
    apply x.c.
    Restart.
    Fail apply _.
  Abort.
End functor.

Module y <: X.
  (* Won't be an instance. *)
  Definition a : Inhabited nat := populate 0.
  (* Will be an instance. *)
  #[global] Instance c : Inhabited N := populate 0%N.
End y.


#[global] Instance b : Inhabited nat.
Proof.
  apply y.a.
  Restart.
  (* [y.a] is not declared an instance! *)
  Fail apply _.
Abort.

#[global] Instance d : Inhabited N.
  apply y.c.
  Restart.
  apply _.
Abort.

(* We remove [y.c] to enable more testing. *)
#[global] Remove Hints y.c : typeclass_instances.


Module x : X.
  (* Here not an instance, but hints come from [X] so it will be. *)
  Definition a : Inhabited nat := populate 0.
  (* #[global] Instance x : Inhabited nat := populate 0. *)
  #[global] Instance c : Inhabited N := populate 0%N.
End x.

(* Same behavior as inside [functor]! *)
#[global] Instance b : Inhabited nat.
Proof.
  apply x.a.
  Restart.
  apply _.
Abort.

#[global] Instance d : Inhabited N.
Proof.
  apply x.c.
  Restart.
  Fail apply _.
Abort.