What are Generic Arguments in Coq and how are they structured in their OCaml code?

Developing plugins
1

I was trying to figure out why it seems that in a Coq generic argument there seems to be 3 arguments to the constructor GenArg when according to me there should only be 2 (plus one of the argument seems to skip to other constructors I was expecting based on the OCaml algebraic data type code e.g. OptArg).

I see from coq-serapi:

((GenArg raw (OptArg (ExtraArg ltac_selector)) ())
          (GenArg raw (OptArg (ExtraArg ltac_info)) ())
          (GenArg raw (ExtraArg tactic)
           (TacArg
            ((v
              (TacCall
               ((v
                 (((v (Ser_Qualid (DirPath ()) (Id ___hole)))
                   (loc
                    (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                      (line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 8)))))
                  ( (ConstrMayEval
                    (ConstrTerm
                     ((v
                       (CPrim (Numeral SPlus ((int 0) (frac "") (exp "")))))
                      (loc
                       (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                         (line_nb_last 1) (bol_pos_last 0) (bp 9) (ep 10))))))) )))
                (loc
                 (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                   (line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 10)))))))
             (loc
              (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                (line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 10)))))))
          (GenArg raw (ExtraArg ltac_use_default) false)) ))))

focusing on the first one in the raw_generic_argument list:

(GenArg raw (OptArg (ExtraArg ltac_selector)) ()

we see we have this weird word raw that according to me should NOT be there because look at the type definition for raw_generic_argument:

type 'l generic_argument =
| GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument	
A inhabitant of 'level generic_argument is a inhabitant of some type at level 'level, together with the representation of this type.

type raw_generic_argument = rlevel generic_argument

the constructor GenArg should only take 2 things. But the argument I showed takes 3 things – the last one being unit, perhaps?

Can someone explain we what’s going on?

In addition, the second argument (OptArg (ExtraArg ltac_selector)) seems completely off too. We know 'l is rlevel. We should have ('a rlevel) abstract_argument_type as the first argument (which seems to be the second one according to the s-expression I pasted. The abstract_argument_type has constructors:

type (_, _) abstract_argument_type =
| Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
| Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type
| Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type

but none appear…which is super puzzling to me. There are 3 options and nothing else. So why does it randomly skip to the constructor OptArg corresponding to gen_arg_type?