After playing around with this for a little while, it looks to me like
type t = []
isn't defining t as a synonym for the empty polyvariant, but rather defining t to be an ADT with one constructor, []. In particular, note that
type t = []
type s = []
let f (x : s) : t = x (* does not typecheck *)
type r = t = [] (* parses fine, showing [] is a constructor *)
let f [] = () (* no exhaustivity warnings, inferred type is f : r -> unit *)
It's odd that [] is a valid constructor name, but I suppose we want it so for lists, and might as well let other people reuse it.