Ltac2 lacks proper abstract types (and related features)

[rlepigre]

I sometimes really miss the ability to hide the implementation details of an Ltac2 type.

Ideally, there would be an #[abstract] attribute that one could add to Ltac2 type to specify that the type is to be seen as abstract from any function not in the current module. For example:

Module Counter.
  #[abstract] Ltac2 Type t := int ref.
  Ltac2 create : unit -> t := fun () => Ref.ref 0.
  Ltac2 incr : t -> unit := Ref.incr.
  Ltac2 get : t -> int := Ref.get.
End Counter.

(* Fails with something like: [r] has type [Counter.t] but is expected to have type [int Ref.t]. *)
Fail Ltac2 incr_n : Counter.t -> int -> unit := fun r i =>
  Ref.set r (Int.add i (Ref.get r)).

A variation of that attribute could be #[private], forbidding one to construct values of the type outside of the module where it is defined, but still allowing matching.

How hard would these be to implement?