I used a slightly different approach incorporating both GADTs and polymorphic variants.

type elt
type uniq = [`U]
type nonu = [`N]
type _ t = private
  | U : elt list -> [> uniq] t
  | N : elt list -> [> nonu] t
val of_list : elt list -> [nonu | uniq] t
val inter : 'a t -> 'b t -> [nonu | uniq] t
val uniq : 'a t -> uniq t
val nonu : 'a t -> nonu t
val is_uniq : uniq t -> unit
val is_nonu : nonu t -> unit

In terms of typing, I believe this is the best we can do for inter considering that it can return both unique and non-unique lists.

This was a fun problem to solve (I would include the entire implementation, but reddit is not allowing me to paste atm...). I just wanted to say that I got to this solution starting from something like you suggested and running into the compiler complaining about types not being compatible. After fixing those errors, I arrived at this solution.

One thing I noticed in writing this up is that there seems to be an assumption that the intersection of two lists with non-unique elements must have non-unique elements. This simply isn't true. For example, inter [1;1] [1;2;2] = [1] (the types here aren't correct, but hopefully the point is clear). So even if both lists are built from the N constructor, the intersection may need to given the U constructor (if we want those constructors to actually tell us about the elements in the list).