% -*- LaTeX -*-
\documentclass[10pt]{article}

\usepackage{supertabular}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{stmaryrd}  % for ?
\usepackage{prettyref}
\usepackage{xcolor}

\newrefformat{fig}{Figure~\ref{#1}}
\newrefformat{sec}{Section~\ref{#1}}
\newrefformat{eq}{equation~\eqref{#1}}
\newrefformat{prob}{Problem~\ref{#1}}
\newrefformat{tab}{Table~\ref{#1}}
\newrefformat{thm}{Theorem~\ref{#1}}
\newrefformat{lem}{Lemma~\ref{#1}}
\newrefformat{prop}{Proposition~\ref{#1}}
\newrefformat{defn}{Definition~\ref{#1}}
\newrefformat{cor}{Corollary~\ref{#1}}
\newcommand{\pref}[1]{\prettyref{#1}}

% \Pref is just like \pref but it uppercases the first letter; for use
% at the beginning of a sentence.
\newcommand{\Pref}[1]{%
  \expandafter\ifx\csname r@#1\endcsname\relax {\scriptsize[ref]}
    \else
    \edef\reftext{\prettyref{#1}}\expandafter\MakeUppercase\reftext
    \fi
}

\newtheorem{thm}{Theorem}[section]
\newtheorem{lem}[thm]{Lemma}

\newcommand{\rulen}[1]{\textsc{#1}}

\DeclareMathOperator{\res}{res}

\begin{document}
  
  \input{fc-she-rules}

\section{Introduction}

\emph{This section is a stub.  You can help the authors by expanding
  it.}

Examples of programming at the type level (see examples/AddTF.hs).
However, this is currently \emph{untyped}.  What we would \emph{like}
to do is something like this (example).

Essentially, what we would like to be able to do is ``lift'' types to
the kind level, and data constructors to the type level.  We propose
to accomplish this by simply collapsing the distinction between types
and kinds, and allowing data constructors to be used as type
constructors.  However, other than automatically lifting data
constructors, we still maintain a strict separation between terms and
types.

\section{Types and coercions}

\subsection{Syntax}

The syntax of types and coercions is shown in~\pref{fig:types}.

\begin{figure}[htp]
  \centering
  \ottgrammartabular{
    \otts \ottinterrule
    \ottv \ottinterrule
    \ottg \ottafterlastrule
  }
  \caption{Syntax of types and coercions}
  \label{fig:types}
\end{figure}

Types include familiar type variables, type constructors, type
functions, universal quantification, and type application.  Note that
$[[ all a:k.s ]]$ is the type of functions with an \emph{implicit},
\emph{eraseable} argument, and we use $[[ s1 => s2 ]]$ as an
abbreviation for $[[ all a:s1. s2 ]]$ when $a$ does not occur free in
$[[s2]]$.  For typing functions with non-erasable (runtime) arguments,
we assume the environment contains a special type constructor $[[ (->)
]]$ with kind $[[ * => * => * ]]$, and use $[[ s1 -> s2 ]]$ as an
abbreviation for $[[((->) s1) s2]]$.

We also allow \emph{data constructors} $[[ K ]]$ in types.  Star
($\star$) is also a type, since we are collapsing types and kinds into
one level.  Finally, we have ways to abstract over equality proofs
($[[ all c:s1 ~ s2. s3 ]]$), to instantiate such an
abstraction with a concrete coercion ($[[ s g ]]$), and to use a
coercion to explicitly convert the kind of a type to another,
equivalent kind ($[[ s |> g ]]$).

The syntactic forms of coercions are discussed in more detail when we
discuss the kinding rules for coercions in \pref{sec:kinding}.

\subsection{Kinding}
\label{sec:kinding}

We will use the metavariable $v$ to range over type variables $a$,
type constructors $T$, type families $F$, and data constructors $K$.
The syntax of bindings and contexts and the definition of context
well-formedness are shown in~\pref{fig:contexts}.

\begin{figure}[htp]
  \centering
  \ottgrammartabular{
  \ottbinding \ottinterrule
  \ottG \ottafterlastrule
  } \par \bigskip
  \ottdefnctx{}
  \caption{Contexts}
  \label{fig:contexts}
\end{figure}

% The \emph{bi-annotation} binding forms are worth noting.  Since we use
% heterogeneous (untyped) coercions, when typechecking them we must
% allow our context to bifurcate into two versions with different typing
% assumptions for the same variables, one for checking the left-hand
% side of the coercion and one for the right-hand side.  When
% typechecking the types that occur in coercions, we ``unzip'' the
% context and use the left-hand or right-hand assumptions as
% appropriate.  Concretely, left context projection is defined by
% induction on contexts as follows:
% \[
% \begin{array}{lcl}
% [[ empty<- ]] &=& [[ empty ]]  \\
% [[ (G,v:k)<- ]] &=& [[ G<-, v:k ]] \\
% [[ (G,v:<k1,k2>)<- ]] &=& [[ G<-, v:k1 ]] \\
% [[ (G,c:s1 ~ s2)<- ]] &=& [[ G<-, c:s1 ~ s2 ]] \\
% [[ (G,c:<s1,s1'> ~ <s2,s2'>)<- ]] &=& [[ G<-, c:s1 ~ s2 ]] 
% \end{array}
% \]
% Right context projection $[[G->]]$ is defined similarly.  
% We could
% achieve a similar effect by parameterising the coercion kinding
% judgement over two contexts, one for the left-hand side and one for
% the right-hand side, but 

The kinding judgement for types is shown in~\pref{fig:kinding}.  Note
that we give $[[*]]$ itself the kind $[[*]]$. It is well-known that
this results in an inconsistent logic; however, Haskell's type system
already corresponds to an inconsistent logic due to general recursion,
so this is no great loss.  Otherwise, the kinding judgement is
relatively straightforward, and is shown in \pref{fig:kinding}. Note
that we use $[[ G |- s ]]$ as an abbreviation for $\exists
\kappa.\, [[ G |- s : k ]]$.

\begin{figure}[htp]
  \centering
  \ottdefnknd{}
  \caption{Kinding judgement}
  \label{fig:kinding}
\end{figure}

% \begin{lem}[Preservation of kinds under context projection]
% \label{lem:proj-pres}
% If $[[G |- s : k]]$ then $[[G<- |- s : k]]$ and $[[G-> |- s : k]]$.  
% \end{lem}
% \begin{proof}
%   Straightforward induction.
% \end{proof}

\subsection{Coercion kinding}
\label{sec:coercion-kinding}

The kinding judgement for coercions is shown below.  The first few
rules simply make explicit that coercions are reflexive, symmetric,
and transitive.  Beyond that, there are sets of rules for constructing
and destructing coercions between each syntactic form of types.
\bigskip

%\begin{figure}[htp]
%  \centering
  \ottdefncoerce{}
%  \caption{Coercion kinding judgement}
%  \label{fig:coercion-kinding}
%\end{figure}

\begin{itemize}
\item \rulen{C\_Abs} is for constructing coercions between polymorphic
  types; \rulen{C\_Inst} and \rulen{C\_Arg} let us decompose such
  coercions by instantiating the type parameters and equating the
  kinds of the type parameters, respectively.
\item \rulen{C\_App} lets us build coercions between type
  applications.  Likewise, there are two rules for decomposing
  coercions between type applications, \rulen{C\_Left} and
  \rulen{C\_Right}, which bear a bit of explanation.

  First, given $[[ s1 s2 ~ s1' s2' ]]$, when can we
  conclude that $[[ s1 ~ s1' ]]$?  Let's look at a few
  examples; consider \pref{fig:example-tcons}.

  \begin{figure}[htp]
    \centering
\begin{verbatim}
  data Maybe a = Nothing | Just a

  type family F a :: *
  type instance F Int  = Int
  type instance F Char = Int
  type instance F Bool = Maybe Int

  type family G a :: *
  type instance G Bool = Int

  data family H a :: *
  data instance H Int = HCon1 | HCon2 Bool
\end{verbatim}    
    \caption{Example data types, type families, and data families}
    \label{fig:example-tcons}
  \end{figure}
  \begin{itemize}
  \item If we know that \verb|Maybe a ~ Maybe b|, we are clearly
    justified in concluding that \verb|Maybe ~ Maybe| (although this
    is rather uninteresting).
  \item Evidently we have \verb|F Int ~ G Bool|, but just as evidently
    this does not allow us to conclude that \verb|F ~ G|.
  \item What if we have \verb|Maybe a ~ f b|, where \verb|f| is a
    unification variable?  Can we conclude that \verb|Maybe ~ f|?  A
    moment's thought reveals that we cannot, since we may have
    \verb|f = F| and \verb|b = Bool|. 
  \end{itemize}
  The key question is this: given \verb|Maybe a ~ f b|, what would we
  need to know about \verb|f| so that we \emph{would} be able to
  conclude \verb|Maybe ~ f|?  The key property that we need is
  \emph{generativity}.  Informally, we say that a type constructor
  \verb|f| is \emph{generative} if its declaration creates a new type
  that did not exist before.  More formally, if the declaration of
  \verb|f| takes place in an environment $\Gamma$ containing other
  type constructors (none of which refer to \verb|f|), then \verb|f|
  is generative if \verb|f a| $\neq$ \verb|g b| for every \verb|g|
  $\in \Gamma$ and any \verb|a|, \verb|b|.  By definition, if \verb|f|
  and \verb|g| are both generative, then \verb|f a ~ g b| implies
  \verb|f ~ g|. \rulen{C\_Left} embodies this reasoning principle.

  Data type constructors and data family constructors are generative;
  type synonym constructors and type family constructors are not.

  (Note: a different choice would be to have a separate syntactic form
  for type family applications, and to enforce that they are always
  fully applied; then having a type of the form $[[ s1 s2 ]]$
  would automatically imply that $[[ s1 ]]$ is generative, since
  it would not be allowed to correspond to a type function
  application.)

  On the other hand, if we know $[[ s1 s2 ~ s1' s2'
  ]]$, when can we conclude that $[[ s2 ~ s2' ]]$?  First, it
  makes sense to only consider cases where we already know that $[[
  s1 ~ s1' ]]$ --- if we don't know this then there's not a
  lot we could possibly say about $[[ s2 ]]$ and $[[ s2' ]]$.
  \begin{itemize}
  \item If we know \verb|Maybe a ~ Maybe b|, then we can conclude
    \verb|a ~ b|.
  \item Likewise, if we know \verb|H a ~ H b|, we can conclude \verb|a ~ b|.
  \item If we know \verb|F a ~ F b|, on the other hand, we cannot
    conclude anything about \verb|a| and \verb|b| --- for example, we
    could have \verb|a ~ Int| and \verb|b ~ Char|.
  \end{itemize}

  The key difference here is whether the type being applied is
  \emph{injective}. \rulen{C\_Right} embodies this reasoning
  principle.  Data types and data families are injective; type
  families are not (nor are type synonyms, since they may be synonyms
  for type family applications).

  A natural question arises: what is the difference between
  \emph{generative} types and \emph{injective} ones?  Currently, there
  is none!  However, it would be possible, for example, to add the
  ability to declare \emph{injective} type families, for example
\begin{verbatim}
  injective type family F a :: *
  type instance F Int  = Bool
  type instance F Char = [Bool]
  type instance F Bool = Int
\end{verbatim}
  (Presumably the compiler would check that none of the right-hand
  sides for \verb|F| axioms are overlapping.)  Now when encountering
  an equality of the form \verb|F a ~ F b|, we may conclude
  \verb|a ~ b|.  However, \verb|F| is still not generative, so if we
  know \verb|F a ~ g b| we may not conclude \verb|F ~ g|, even if we
  know \verb|g| is generative.

  Although it is a bit more of a stretch, it is also possible to
  imagine types which are generative but not injective.  For example,
  suppose we could declare a data family using the following made-up
  syntax:
\begin{verbatim}
  data family H a :: *
  data instance H (Int|Char) = HCon1 | HCon2
  data instance H Bool       = HCon3
\end{verbatim}

  The idea here is that the same constructors are used for both
  \verb|H Int| and \verb|H Char|.  In this case knowing
  \verb|H a ~ h b| would allow us to conclude \verb|H ~ h| as long as
  we know \verb|h| is generative; but we could not conclude that
  \verb|a ~ b|.

  Of course, this example is not currently valid Haskell, and would
  require extending the language of constraints with disjunction in
  addition to conjunction.  For example, the type of \verb|HCon1|
  ought to be something like 
%
  \verb+(a ~ Int | a ~ Char) => H a+. However, it is useful as a
  thought experiment to illustrate why the notions of generativity and
  injectivity of type constructors are (in theory) not the same.

  Finally, note that we can encode 

  \[ [[ nth k 0 g ]] = [[ left ]]^k [[ g ]]\]

  XXX finish this!

  % Finally, note that if we have a coercion between type constructor
  % applications such as $\gamma : \verb|T a b c ~ T d e f|$ and want to
  % extract a coercion between \verb|b| and \verb|e|, we can do so by a
  % suitable combination of primitive coercion constructors.  In
  % particular, \[ [[ right (sym ((left (left g)) b) ; left g) ]]
  % : \verb|b ~ e|. \] Of course, this is horrible to read and possibly
  % inefficient to boot.  A real implementation might include shortcuts
  % for extracting the $n$th argument from both sides of an equality,
  % but presenting the core system of coercions this way simplifies both
  % the presentation and the metatheory.

\item The \rulen{C\_CAbs} rule allows us to construct coercions
  between coercion abstractions; \rulen{C\_CInst} allows instantiating
  such coercions to obtain a coercion between the bodies of the
  abstractions; and \rulen{C\_CArgL} and \rulen{C\_CArgR} allow
  extracting equalities between the left- and right-hand-sides of the
  abstracted coercions.  Note that unlike \rulen{C\_Inst},
  \rulen{C\_CInst} does not require any particular relationship
  between $[[ g1 ]]$ and $[[ g1' ]]$, since we can never observe
  equality or inequality between coercions; all coercions with the
  same kind are interchangeable.  In particular, there is no
  \rulen{C\_CRight} rule which would allow us to conclude that $[[ g
  ]]$ and $[[ g' ]]$ are equal from $[[G1;G2 |- g1 : s g ~ s'
  g']]$.  Indeed, coercions are between types, so syntactically
  speaking we would not even be able to express this.

\item \rulen{C\_CApp} is for constructing coercions between
  applications of the form $[[ s g ]]$, where a type abstracted over a
  coercion is applied to a coercion.  \rulen{C\_CLeft} decomposes such
  a coercion to obtain a coercion between the left-hand sides.  As
  already noted, there is no corresponding \rulen{C\_CRight} because
  there are no coercions between coercions.

\item Finally, \rulen{C\_Coerce} provides for constructing coercions
  between coerced types of the form $[[ s |> g ]]$.  If we have a
  coercion $[[ G1;G2 |- g : s1 ~ s2 ]]$, we can also coerce between
  $[[ s1 |> g1 ]]$ and $[[ s2 ]]$ (as long as $[[ s1 |> g1 ]]$ is
  well-kinded under $[[G1]]$), since applying a coercion to $[[ s1 ]]$
  changes only its type, not its structure.

  It is useful to have this one-sided form of the rule, since it gives
  us everything we need with respect to coercions between coerced
  types.  We can obviously apply a coercion to the right-hand type
  with appropriate uses of symmetry.  Somewhat less obvious is the
  fact that we can also use this rule to \emph{remove} a coercion
  application from one side of an equality, by appropriate use of
  reflexivity, symmetry, and transitivity.  In particular, if \[ [[ G1;G2
  |- g : s1 |> g1 ~ s2 ]], \] then \[ [[ G1;G2 |- sym (<s1>
  |> g1) ; g : s1 ~ s2 ]]. \]
\end{itemize}

\subsection{Invariants}

If we have $[[ G1;G2 |- g : s1 ~ s2 ]]$, what should we be able to
conclude about $[[ s1 ]]$ and $[[ s2 ]]$?  There are a few
options:
\begin{enumerate}
\item There is an $[[ k ]]$ for which $[[ G1 |- s1 : k ]]$ and
  $[[ G2 |- s2 : k ]]$.  That is, coercions are always between
  two types with the same kind.

  However, this invariant is incompatible with the rule we have chosen
  for constructing coercions between applications: \[ \ottdruleCXXApp{} \]
  For example, suppose we have something like the following:
\begin{verbatim}
  data T a = K
  type family F :: * -> *
  type instance F Int = Int
\end{verbatim}
  corresponding to the top-level environment \[ [[ G ]] = [[ T : * =>
  *, K : all a:*. T a, F : * => *, c : F Int ~ Int ]]. \] Then we see
  that \[ [[ G;G |- K c : K (F Int) ~ K Int ]], \] but \[ [[ G |-
  K (F Int) : T (F Int) ]] \] whereas \[ [[ G |- K Int : T Int ]]. \]

  Accommodating this invariant would result in a much less expressive
  system, where we are only able to conclude that equivalent things
  applied to \emph{identical} arguments are equivalent.

\item If $[[ G1;G2 |- g : s1 ~ s2 ]]$, then $[[ G1 |- s1 : k1
  ]]$, $[[ G2 |- s2 : k2 ]]$, and there exists a coercion $[[ g'
  ]]$ such that $[[ G1;G2 |- g' : k1 ~ k2 ]]$.  In other words,
  convertible types have convertible kinds.  This option is rather
  complicated, however, since to maintain it we would probably have to
  pass around extra evidence.

\item The last choice is the simplest, and the one we adopt here.  If
  $[[ G1;G2 |- g : s1 ~ s2 ]]$, then $[[ G1 |- s1 ]]$ and $[[ G2
  |- s2 ]]$.  That is, convertible types must simply be
  well-kinded.
\end{enumerate}

Proving that this last invariant holds is not too hard, since we have
explicitly designed the coercion kinding rules to ensure that it is
true.

Another invariant we would like is for $[[ G |- s : k ]]$ to
imply $[[ G |- k : * ]]$.  Proving this is a straightforward
induction, but crucially it requires adding a premise to the
``standard'' kind judgement for coercion applications: \[
\ottdruleKXXCoerce{} \] The inductive hypothesis here tells us that
$[[ G |- k1 : * ]]$, and we know that $[[ G;G |- g : k1 ~ k2 ]]$,
but those facts don't tell us anything about what we want to prove,
namely, that $[[ G |- k2 : * ]]$.  Hence, we simply add this as a
precondition.

\subsection{Metatheory}

\begin{lem} \label{lem:tv-bind-star}
  If $[[ |- G ]]$ and $[[ a:k in G ]]$, then $[[ G |- k : * ]]$.
\end{lem}

\begin{proof}
  Either $[[G]] = [[G',a:k]]$ in which case the conclusion follows
  immediately, or $[[G]]$ ends with some other binding which we may
  discard via an easy strengthening lemma.
\end{proof}

\begin{lem}[Substitution of types in types] \label{lem:subst-ty-ty}
  If $[[ G, a:k, G' |- k1 : k2 ]]$ and $[[ G |- s : k ]]$,
  then $[[ G, G'[a |-> s] |- k1[a |-> s] : k2[a |-> s] ]]$.
\end{lem}
\begin{lem}[Substitution of types in coercions] \label{lem:subst-ty-co} 
  If $[[ G1, a:k1, G1'; G2, a:k2, G2' |- g : k1 ~ k2 ]]$ and $[[ G1 |- s : k1 
  ]]$ and $[[ G2 |- s : k2]]$, then $[[ G1, G1'[a |-> s]; G2, G2'[a |-> s] |- g[a |-> s] : k1[a |->
  s] ~ k2[a |-> s] ]]$.
\end{lem}
\begin{proof}
  XXX need to re-check this!
  We must prove these two lemmas simultaneously by mutual induction,
  since type kinding judgements contain coercion kinding judgements,
  and vice versa.  

  The first lemma proceeds by induction on $[[ G, a:k, G' |- k1 :
  k2 ]]$.  The only interesting case is \rulen{KVar}:
  \begin{itemize}
  \item \rulen{KVar}. If $a = [[k1]]$, then we must show that $[[
    G,G'[a |-> s] |- s : k2[a |-> s] ]]$.  However, we
    know that $[[ a : k2 in G, a:k, G' ]]$ and hence we must have
    $[[k2]] = [[k]]$.  $a$ does not appear free in $[[k]]$, so
    we now must show that $[[ G, G'[a |-> s] |- s : k ]]$,
    but this follows from the premise by weakening.

    On the other hand, if $a \neq [[k1]] = b$, then we must show $[[ G,
    G'[a |-> s] |- b : k2[a |-> s] ]]$.  We know there is
    a binding $[[b : k2 in G, a:k, G']]$, so it must be in
    either $[[G]]$ or $[[G']]$.  If in $[[G]]$, then $[[k2]]$ does
    not contain $a$ free, so the substitution has no effect and the
    desired result follows immediately.  If in $[[G']]$, then $[[b
    : k2[a |-> s] in G'[a |-> s] ]]$, also giving the desired
    result.
  \end{itemize}

  We prove the second lemma by a straightforward induction on $[[ G1,
  a:k1, G1'; G2, a:k2, G2' |- g : k1 ~ k2 ]]$, noting in the
  \rulen{C\_Left} and \rulen{C\_Right} cases that generativity and
  injectivity are preserved under substitution.
\end{proof}

\begin{lem}[Substitution of coercions in types] \label{lem:subst-co-ty}
  If $[[ G, c:k1 ~ k2 |- k3 : k4 ]]$ and $[[ G;G |- g : k1 ~
  k2 ]]$, then $[[ G |- k3[c |-> g] : k4 ]]$.
\end{lem}
\begin{lem}[Substitution of coercions in coercions] 
  \label{lem:subst-co-co} 
  If $[[ G1, c:k1 ~ k2; G2, c:k1~k2 |- g1 : k3 ~ k4 ]]$ and $[[ G1 |- g2 :
  k1 ~ k2 ]]$ and $[[ G2 |- g2 : k1' ~ k2' ]]$, then $[[ G1;G2 |- g1[c |-> g2] : k3[c |-> g2] ~
  k4[c |-> g2] ]]$.
\end{lem}

\begin{proof}
  XXX work through details.  May need to generalize statements.
  These lemmas again must be proved by mutual induction.  I assume
  they are also straightforward but have not worked through the
  details.
\end{proof}

\begin{lem}[Coercion well-kindedness] \label{lam:coercion-wf} If $[[ G1;G2
  |- g : s1 ~ s2 ]]$, then $[[ G1 |- s1 ]]$ and $[[ G2 |-
  s2 ]]$.
\end{lem}
\begin{proof}
  Simple induction on the derivation of $[[ G1;G2 |- g : s1 ~ s2
  ]]$, appealing to some weakening and substitution lemmas in the
  \rulen{C\_Abs} and \rulen{C\_CAbs} cases, and a substitution lemma
  in the \rulen{C\_Inst} and \rulen{C\_CInst} cases.
\end{proof}

\begin{thm}[Regularity of kinding] \label{lem:reg-kinding}
  If $[[ |- G ]]$ and $[[ G |- s : k ]]$, then $[[ G |- k : * ]]$.
\end{thm}

\begin{proof}
  Straightforward induction, appealing to \pref{lem:tv-bind-star} and
  \pref{lem:subst-ty-ty}.
\end{proof}

\subsection{The Lifting Lemma}

\Pref{fig:c-for-tv} defines what it means to substitute coercions for
\emph{type variables} occurring in types.  Intuitively, we can think
of the type $[[ s ]]$ as the identity coercion $[[ < s > ]]$, and
substituting a coercion for a type variable gives us a coercion
between two (possibly different) types, with the type variable
replaced by the two sides of the substituted coercion.  For
example, \[ [[ a : * |- <T Char a> : T Char a ~ T Char a ]], \] and
if \[ [[ empty |- g : Int ~ Char ]] \] then we can substitute $[[ g
]]$ for $a$: \[ [[ empty |- (T Char a)[a |-> g] : T Char Int ~ T Char
Char ]]. \]

In particular, we define the operation of substituting a coercion for
a type variable in a type by induction on the type as follows.
%% ARGH, the last case requires the context as an input!  Hrm, how to
%% rework this?
\[
\begin{array}{lcll}
  [[ * [a |-> g] ]] &=& [[ *~ ]] \\
  [[ a [a |-> g] ]] &=& [[ g ]] \\
  [[ v [a |-> g] ]] &=& [[ v ]] & (v \neq a) \\
  [[ (all b:k.s)[a |-> g] ]] &=& [[ all b:k[a |-> g]. s[a |-> g] ]] \\
  [[ (s1 s2)[a |-> g] ]] &=& [[ (s1 [a |-> g]) (s2 [a |-> g]) ]] \\
  [[ (all c:k1 ~ k2. s)[a |-> g] ]] &=& [[ all c:k1[a |-> g] ~ k2[a |-> g]. s[a |-> g] ]] \\
  [[ (s g1)[a |-> g] ]] &=& [[ s[a |-> g](g1[a |-> g], g1[a |-> g]) ]] \\
  [[ (s |> g1)[a |-> g] ]] &=& [[ g' |> g1[a |-> s1] ; sym(g') ; sym(sym(g') |> g1[a |-> s2]) ]] \\
  && \text{where\quad} [[g']] = [[ s[a |-> g] ]], [[g1']] = [[ g1[a |-> g] ]] \\
\end{array}
\]
This operation is a fairly straightforward congruence except for the
final case, where we must do some minor fiddling to make the type of
the coercion come out right; this is the price we pay for choosing the
non-symmetric rule \rulen{C\_Coerce}.  For the final two cases we must
also define what it means to substitute a coercion for a type variable
in a coercion.  This mostly consists of a straightforward congruence
for each syntactic coercion form, making a mutually recursive call
back to substitution in types when encountering a reflexivity
coercion:
\[
\begin{array}{lcll}
  [[ *~ [a |-> g] ]] &=& [[ *~ ]] \\
  [[ a[a |-> g] ]] &=& [[ g ]] \\
  [[ v [a |-> g] ]] &=& [[ v ]] & (v \neq a) \\
  [[ <s>[a |-> g] ]] &=& [[ s[a |-> g] ]] \\
  \text{\emph{\dots other cases just congruence.}}
\end{array}
\]

Finally, we define what it means to perform a bisubstitution on a
context. % XXX make this prettier
\[
\begin{array}{lcll}
  [[ empty [a |-> <s1,s2>] ]] &=& [[ empty ]] \\
  [[ (G, b:k) [ a |-> <s1,s2> ] ]] &=& [[ G[a |-> <s1,s2>], b:<k[a |-> s1], k[a |-> s2]> ]] \\
  [[ (G, b:<k1,k2>) [ a |-> <s1,s2> ] ]] &=& [[ G[a |-> <s1,s2>], b:<k1[a |-> s1], k2[a |-> s2]> ]] \\
  [[ (G, c:k1 ~ k2)[ a |-> <s1,s2> ] ]] &=& [[ G[a |-> <s1,s2>], c:<k1[a |-> s1], k1[a |-> s2]> ~ <k2[a |-> s1], k2[a |-> s2]> ]] \\
  [[ (G, c:<k1,k1'> ~ <k2,k2'>)[ a |-> <s1,s2> ] ]] &=& [[ G[a |-> <s1,s2>], c:<k1[a |-> s1], k1'[a |-> s2]> ~ <k2[a |-> s1], k2'[a |-> s2]> ]]
\end{array}
\]

\begin{lem} \label{lem:proj-bisubst}
  For all contexts $[[G]]$, $[[ (G[a |-> <s1,s2>])<- ]] = [[ G[a |->
  s1] ]]$, and $[[ (G[a |-> <s1,s2>])-> ]] = [[ G[a |-> s2] ]]$.
\end{lem}
\begin{proof}
  Routine induction on the structure of contexts.
\end{proof}

Now we can state the main lifting result.

\begin{lem}[Lifting]
  Suppose
  \begin{align*}
    & [[ G |- g : s1 ~ s2 ]], \\
    & [[ G |- s1 : k ]], \text{and} \\
    & [[ G |- s2 : k ]].
  \end{align*}
  \begin{enumerate}
  \item If $[[ G, a:k, G' |- s ]]$, then \[ [[ G, G'[a |-> <s1,s2>] |- s[a |-> g] : s[a |-> s1] ~ s[a |-> s2] ]]. \]
  \item If $[[ G, a:k, G' |- g' : k1 ~ k2 ]]$, then \[ [[ G, G'[a |->
    <s1,s2>] |- g'[a |-> g] : k1[a |-> s1] ~ k2[a |-> s2] ]]. \]
  \end{enumerate}

\end{lem}
\begin{proof}
  We prove (1) and (2) simultaneously by induction on their derivations.
  We begin by proving (1).
  \begin{itemize}
  \item \rulen{K\_Var}. If $[[s]] = a$, the desired conclusion follows
    from the premise by weakening.  If $[[s]]$ is a variable other
    than $a$, or a type constructor, type function, or lifted
    data constructor, the substitutions have no effect and the conclusion is
    immediate.
  \item \rulen{K\_Star}. Immediate.
  \item \rulen{K\_Abs}.  $[[s]] = [[all b:k'. s']]$. We wish to show
    that \[ [[ G,G'[a |-> <s1,s2>] |- (all b:k'.s')[a |-> g] : (all
    b:k'.s')[a |-> s1] ~ (all b:k'.s')[a |-> s2] ]]. \] By inversion
    on the typing judgement for $[[s]]$, we have $[[G, a:k, G' |- k' :
    *]]$ and $[[G, a:k, G', b:k' |- s' : * ]]$.  Applying the
    inductive hypothesis to each of these yields
    \begin{equation*} 
      \label{eq:IH1}
      [[G,G'[a |-> <s1,s2>] |- k'[a |-> g] : k'[a |-> s1] ~ k'[a |-> s2] ]]
    \end{equation*}
    and
    \begin{equation*}
      \label{eq:IH2}
      \begin{split}
      [[G,G'[a |-> <s1,s2>],b:<k'[a |-> s1], k'[a |-> s2]> ]] [[ |- ]] \\
      [[ s'[a |-> g] ]] : [[ s'[a |-> s1] ~ s'[a |-> s2] ]].
      \end{split}
    \end{equation*}
    These are exactly two of the premises we need to show the desired
    conclusion by \rulen{C\_Abs}, leaving only to show that $[[(G,
    G'[a |-> <s1,s2>])<- |- k'[a |-> s1] : * ]]$ and $[[(G, G'[a |->
    <s1,s2>])<-, b:k'[a |-> s1] |- s'[a |-> s1] : * ]]$ (and similarly
    for the right projections and $[[s2]]$).  Given
    \pref{lem:proj-pres} and \pref{lem:proj-bisubst}, these follow
    from the premises of the typing judgement for $[[s]]$, the typing
    judgements for $[[s1]]$ and $[[s2]]$, and the appropriate
    substitution lemma.

  \item \rulen{K\_App}. Straightforward induction.
  \item \rulen{K\_CAbs}. Similar to \rulen{K\_Abs} case.
  \item \rulen{K\_CApp}. Similar to \rulen{K\_App} case, making use of
    the mutual inductive hypothesis from (2).
  \item \rulen{K\_Coerce}. Very fiddly, but it works.  %% XXX actually write this up
  \end{itemize}
  Next we prove (2).
  \begin{itemize}
  \item 
  \end{itemize}
\end{proof}

\section{Surface Syntax}

The foregoing is good and well as a core language, but of course the
average Haskell programmer will never see the core language and wants
higher-level constructs to program with.  In this section we discuss,
with examples, the modifications to Haskell's surface syntax allowing
programmers to make use of the new features.

\subsection{Automatic Lifting}
\label{sec:auto-lifting}

One of the most basic things a Haskell programmer will want to do is
have names of types automatically interpreted as kinds, and names of
data constructors automatically interpreted as types, when
appropriate.  However, we have to be careful since this introduces
opportunities for ambiguity.

For example, suppose we are parsing a Haskell program, and see
something like the following:

\begin{verbatim}
  f :: Int -> [Bar]
\end{verbatim}

What is \verb|Bar|?  (Of course, we might also very well ask about
\verb|Int| and \verb|[]|, but for now let's stick with \verb|Bar|!)
Currently, GHC simply notes that it is in a type context and looks for
a type constructor named \verb|Bar|.  If it finds one, great; if not,
it emits an error complaining that there is no type constructor
\verb|Bar| in scope.  The presence or absence of a \emph{data}
constructor named \verb|Bar|, of course, makes no difference.  For
example, there might be a declaration like
\begin{verbatim}
  data Bar = Bar Char
\end{verbatim}
Thus, \verb|Bar| is both a data and a type constructor, but since data
and type constructors inhabit different namespaces, there is no
ambiguity.

However, what if we now allow data constructors to be automatically
lifted to types?  Clearly, the occurrence of \verb|Bar| in the type
signature of \verb|f| is now ambiguous. How should GHC decide which
\verb|Bar| is meant?

One possible solution is to require the programmer to give explicit
annotations marking each place where she wishes to lift a data
constructor into a type constructor:

\begin{verbatim}
f :: Int -> [{Bar}]
\end{verbatim}

However, putting curly braces everywhere quickly gets rather annoying,
especially in cases where there is no actual ambiguity.  Therefore, we
also propose a ``relaxed'' version of the syntax where curly braces
can be omitted in most circumstances, which works as follows:
\begin{itemize}
\item When encountering a name in context $C$ (either a term or type
  context), GHC first checks whether the name is bound in the
  namespace corresponding to the current context.  If so, that name is
  chosen.
\item Otherwise, GHC checks whether the name is bound in the
  \emph{other} namespace.  If so, that name is chosen.
\item Otherwise, GHC emits a not-in-scope error.
\item Curly braces can be used by the programmer to explicitly
  \emph{toggle} the current context (from term to type or vice versa).
  Note that this implies curly braces can be nested in order to do
  ``antiquoting''.
\end{itemize}


This also has another nice side benefit. Consider the following code:
\begin{verbatim}
  instance Monad Maybe where
    return = Maybe
    Nothing >>= _ = Nothing
    Maybe x >>= f = f x
\end{verbatim}
Can you spot the error?  This sort of mistake is commonly made by new
Haskell programmers (or seasoned Haskell programmers!) who confuse the
name of the type (\verb|Maybe|) with the name of a data constructor
(\verb|Just|).  GHC currently rejects this code with an error
complaining that \verb|Maybe| is not in scope, which can be rather
confusing to a new programmer: of course \verb|Maybe| is in scope!
Under the new name resolution proposal, however, GHC would simply
resolve \verb|Maybe| to the name of the type, and then a much better
error message could be given later while type checking (for example,
``The type constructor \verb|Maybe| cannot be used as a value; perhaps
you meant to use one of its constructors \verb|Nothing| or \verb|Just|
instead?'').

\subsection{Examples}

A few examples are in order.  First, \pref{fig:vec} shows a standard
type of length-indexed vectors.  The code above the line shows one way
to encode length-indexed vectors in current GHC Haskell; the code below
the line shows how it could be done using our proposed extensions.

\begin{figure}[htp]
\begin{verbatim}
  -- Before

  data Zero
  data Succ n

  data Vec :: * -> * -> * where
    Nil  :: Vec a Zero
    Cons :: a -> Vec a n -> Vec a (Succ n)

  -- After

  data Nat = Zero | Succ Nat

  data Vec :: * -> Nat -> * where
    Nil  :: Vec a Zero
    Cons :: a -> Vec a n -> Vec a (Succ n)
\end{verbatim}  
  \caption{Length-indexed vectors, before and after}
  \label{fig:vec}
\end{figure}

There are a few things to note.  First of all, in the ``Before'' code
we are forced to declare two empty types \verb|Zero| and \verb|Succ|
to serve as ``type-level values''; if we wanted value-level natural
numbers as well, we would have to declare them separately.  The
``After'' code, on the other hand, lets us reuse the normal \verb|Nat|
data type as an index to the \verb|Vec| type.  The \verb|Nat| in the
kind of \verb|Vec| is the type \verb|Nat|, automatically lifted to a
kind; \verb|Zero| and \verb|Succ| are used as automatically-lifted
type indices to \verb|Vec| in the types of \verb|Vec|'s constructors.

Another thing to note is that in the ``Before'' code, there is nothing
preventing us from accidentally writing a type like
\begin{verbatim}
  sum :: Vec n Int -> Int
\end{verbatim}
where we intended to indicate that \verb|sum| takes a vector of any
length containing \verb|Int|s, and returns their sum.  Unfortunately,
we got the parameters to \verb|Vec| the wrong way around, and since
both parameters to \verb|Vec| have kind \verb|*|, there is nothing
inherently wrong with this type itself.  However, we will most
certainly have trouble implementing a function of this type, and will
likely get rather confusing error messages from the body of
\verb|sum|.  On the other hand, in the ``After'' code, the second type
parameter to \verb|Vec| has a much more descriptive kind, and the
above type signature (before we have even written any code for
\verb|sum|) will generate a helpful kind mismatch error, informing us
that the second parameter to \verb|Vec| was expected to have kind
\verb|Nat|, but \verb|Int| has kind \verb|*|.

\subsection{Lifting functions}
Lifting value-level functions to the type level?

\subsection{Explicit type application}

XXX

\section{The Whole Shebang}

  \ottall

\end{document}

%   The only nontrivial case is with reflexivity coercions
% $[[<s>]]$---what should $[[<s>[a |-> g] ]]$ be when $[[s]]$ contains
% free occurrences of $a$?  The key observation is that we can always
% normalize coercions to get rid of all reflexivity brackets, by pushing
% the occurrences of reflexivity out to the leaves.  Doing this whenever
% encountering a reflexivity proof ensures that we expose all
% opportunities for substitution.

% Define a reflexivity proof normalization procedure as follows:
% \[
% \begin{array}{lcll}
%   [[ <<v>> ]] &=& [[ v ]] \\
%   [[ <<*>> ]] &=& [[ *~ ]] \\
%   [[ <<all a:k.s>> ]] &=& [[ all a:<<k>>.<<s>> ]] \\
%   [[ <<s1 s2>> ]] &=& [[ <<s1>> <<s2>> ]] \\
%   [[ <<all c:k1 ~ k2. s>> ]] &=& [[ all c:<<k1>> ~ <<k2>>. <<s>> ]] \\
%   [[ <<s g>> ]] &=& [[ <<s>>(g,g) ]] \\
%   [[ <<s |> g>> ]] &=& [[ <<s>> |> g ; sym (<<s>> |> g) ]]
% \end{array}
% \]