Comment author: @gasche

I don't think this is a bug; -short-paths tries to find one of the shortest paths within the set of equivalent paths, and this is the behavior you observe here.

You seem to have a different specification in mind, where equalities are directed from the new name to its definition, and only expansions in this direction are tried to find a short path. However, I believe that we rely on the other direction (from the definition to the name) to be able to robustly re-fold type definitions in the way the user expects.
(I would expect introducing a Notation in Coq to have the same effect: it may affect the printing of terms that have been written without the notation at all.)

Having the "right" type show up among type-aliases is an ill-defined problem and it is likely that you will never be completely satisfied by the result. If you really care about which types get printed, you have to use incompatible types, for example through aliases:

type foo = Foo of bar [@@unboxed]

I agree with @gasche: this is not a bug.

For the use case of type aliases that you describe in Coq, I personally would use inline records: Foo of { module_ident: Id.t }.

@trefis out of curiosity, why are you recommending an inline record rather than (just a record with one field) or (just a variant constructor)? Personally I like the fact that (just a variant constructor) gives more flexibility in naming, but maybe that is what you are against?

I guess it's just a personal preference for labels, for examples, if we were talking about functions, I assume you'd suggest:

val sub : string -> pos:int -> len:int -> string

over

type pos = Pos of int [@@unboxed]
type len = Len of int [@@unboxed]

val sub : string -> pos -> len -> string

I agree it's not exactly the same situation, in particular using inline records will allow you to be less robust to changes of the type (because while your constructor might have 5 args, your pattern might look like Foo { one_arg; _ } -> ...). Still, ...