[TYPES] Do "phantom types" mean types like ('a, 'n)sized_list as a whole, or dummy parameters like 'n itself?

[Eijiro Sumii]

Dear Types people,

I am (again) asking a question about terminology: recently, a student
of mine and I have been developing a library extensively using
so-called phantom types.  As far as we understand, phantoms types are
concerned with polymorphic data types whose type parameter does not
appear in the r.h.s. of the definition, e.g. (in OCaml syntax),

  type ('a, 'n) sized_list = 'a list
    (* should be made abstract by module signature *)

where

  type zero (* no constructor *)
  type 'n succ (* no constructor *)
  let nil : ('a, zero) sized_list = []
  let cons ((a : 'a), (d : ('a, 'n) sized_list))
    : ('a, 'n succ) sized_list = a :: d
  let car (x : ('a, 'n succ) sized_list)
    : 'a = List.hd x
  let cdr (x : ('a, 'n succ) sized_list)
    : ('a, 'n) sized_list = List.tl x

(this example is for pedagogy only).

My question is: do phantom types mean types like ('a,'n)sized_list as
a whole, or dummy parameters like 'n itself?  The majority of the
literature (and Web pages) means the former, while some seem to mean
the latter.

For me, the latter (the minority) seems to be more "logical" since
there is no constructor for the types substituted with 'n (hence the
terminology "phantom"), while ('a,'n)sized_list itself *does* have
flesh and blood (i.e., values).  Does anybody know any historical
reason for the former (the major) terminology?

N.B.  Yes, the types zero and 'n succ are like type void (in the sense
of type theory, not C), but they are distinguished from each other by
the names.

Best regards,

        Eijiro