[TYPES] System FC: inference rule (EqCo) and grammar for $\kappa$

[Adam Megacz]

Hello, I have a question about System FC, as described in the paper
"System F with Type Equality Coercions" (Sulzmann, Chakravarty, Jones,
Donnelly).

Figure 3 describes the judgment $\vdash_k$, which is a ternary relation
between a context, a kind, and a sort.  Specifically, if we see a
judgment:

   $$ X \vdash_k Y : Z $$

we know that X is from the syntactic class of contexts (nonterminal
\Gamma of Figure 1), Y is from the syntactic class of kinds (nonterminal
\kappa of Figure 1), and Z is from the syntactic class of sorts
(nonterminal \delta of Figure 1).

The first hypothesis of rule (EqCo) is

   $$ \Gamma \vdash_k \gamma_1 : CO $$

so we know that in rule (EqCo) $\gamma_1$ comes from the syntactic class
of kinds.  However, the conclusion of rule (EqCo) is:

   $$ \Gamma \vdash_k \gamma_1 \sim \gamma_2 : CO $$

We know that $\gamma_1 \sim \gamma_2$ is a kind, but in the $\kappa$
nonterminal in the grammar (Figure 1) the alternative for the $\sim$
operator indicates that its arguments -- in particular $\gamma_1$ --
must come from the syntactic class of types.  This is in conflict with
the previous paragraph.

I suspect that the authors intended to have a fourth alternative for
nonterminal $\kappa$, meaning that Figure 1 should be amended to:

  $$ \kappa,\iota
        \rightarrow 
        \star                           |
        \kappa_1 \righatrrow \kappa_2   |
        \sigma_1 \sim        \sigma_2   |
        \kappa_1 \sim        \kappa_2
  $$

Is my suspicion correct?  If so, I believe the $\sim$ operator is
actually triply-overloaded.

I have a similar question about $\gamma$ in the conclusion of (CompC).

Thanks,

  - a