
%-------------------------------------------------------------------------------
% Non-checking                                                                  
%-------------------------------------------------------------------------------

\subsection{The ``doesn't typecheck'' judgment}

\newcommand{\NoCheck}[3][\Gamma]{#1\vdash #2 \nLeftarrow #3}
\newcommand{\NoFocus}[4][\Gamma]{#1\vdash #2 : #3 \ngtr #4}
\newcommand{\NoEquiv}[2]{#1 \not\equiv #2}

For terms that don't typecheck, we would like evidence to that
effect.  We thus define ``doesn't typecheck'' judgments mirroring
the typechecking and equivalence judgments.
We use the judgment $c\NoStep$ to mean that
$c$ does not have a definition (i.e. is a declared constant).

\bigskip 
\framebox{$\NoCheck{K}{\Kind}$}
\bigskip 

$$
\begin{array}{ccc}
\infer{\NoCheck{\PiTyp{A}{K}}{\Kind}}{\NoCheck{A}{\Type}} &
\infer{\NoCheck{\PiTyp{A}{K}}{\Kind}}{\CheckTy{A}{\Type} & \NoCheck[\Gamma,A]{K}{\Kind}} &
\mbox{no rule for $\Type$}
\end{array} 
$$

\bigskip 
\framebox{$\NoCheck{A}{\Type}$}
\bigskip 

$$
\begin{array}{cc}
\infer{\NoCheck{a\cdot S}{\Type}}{a\not\in\Sigma} &
\infer{\NoCheck{a\cdot S}{\Type}}{\Sigma(a) = K & \NoFocus{S}{K}{\Type}} \\\\
\infer{\NoCheck{\PiTyp{A_1}{A_2}}{\Type}}{\NoCheck{A_1}{\Type}} &
\infer{\NoCheck{\PiTyp{A_1}{A_2}}{\Type}}{\CheckTy{A_1}{\Type} & \NoCheck[\Gamma,A_1]{A_2}{\Type}} 
\end{array} 
$$

\bigskip 
\framebox{$\NoCheck{M}{A}$}
\bigskip 

$$
\begin{array}{ccc}
\infer{\NoCheck{M}{A}}{\NoCheck{A}{\Type}} &
\infer{\NoCheck{\Lam{M}}{a\cdot S}}{} &
\infer{\NoCheck{\Lam{M}}{\PiTyp{A_1}{A_2}}}{\NoCheck[\Gamma,A_1]{M}{A_2}} \\\\
\infer{\NoCheck{i\cdot S}{A}}{\card{\Gamma} < i} & 
\infer{\NoCheck{i\cdot S}{A}}{\Gamma(i)=A' & \NoFocus{S}{A'}{A}} \\\\
\infer{\NoCheck{c\cdot S}{A}}{c \not\in\Sigma} & 
\infer{\NoCheck{c\cdot S}{A}}{\Sigma(c)=A' & \NoFocus{S}{A'}{A}}
\end{array} 
$$

\bigskip 
\framebox{$\NoFocus{S}{K}{\Type}$}
\bigskip 

$$
\begin{array}{ccc}
\infer{\NoFocus{S}{K}{\Type}} {\NoCheck{K}{\Kind}} &
\infer{\NoFocus{\Nil}{\PiTyp{A}{K}}{\Type}}{} &
\infer{\NoFocus{M;S}{\PiTyp{A}{K}}{\Type}}{\NoCheck{M}{A}}\\\\
\multicolumn{3}{c}{\infer{\NoFocus{M;S}{\PiTyp{A}{K}}{\Type}}{\CheckTy{M}{A} & \NoFocus[\Gamma,A]{S}{K[M\cdot\IdSub]}{\Type}}}
\end{array} 
$$

\bigskip 
\framebox{$\NoFocus{S}{A_1}{A_2}$}
\bigskip 

$$
\begin{array}{cc}
\infer{\NoFocus{S}{A_1}{A_2}} {\NoCheck{A_1}{\Type}} &
\infer{\NoFocus{S}{A_1}{A_2}} {\NoCheck{A_2}{\Type}} \\\\
\infer{\NoFocus{\Nil}{\PiTyp{A_1}{A_2}}{A_3}}{} &
\infer{\NoFocus{M;S}{a\cdot S}{A}}{} \\\\
\infer{\NoFocus{M;S}{\PiTyp{A_1}{A_2}}{A_3}}{\NoCheck{M}{A_1}} &
\infer{\NoFocus{M;S}{\PiTyp{A_1}{A_2}}{A_3}}
                  {\CheckTy{M}{A} & \NoFocus[\Gamma,A_1]{S}{A_2[M\cdot\IdSub]}{A_3}} \\\\
\infer{\NoFocus{M;S}{\PiTyp{A_1}{A_2}}{A_3}}
                  {\CheckTy{M}{A} & \Focus[\Gamma,A_1]{S}{A_2[M\cdot\IdSub]}{A_3'} & \NoEquiv{A_3'}{A_3}} 
\end{array} 
$$

\bigskip 
\framebox{$\NoEquiv{A}{A'}$}
\bigskip 

$$
\begin{array}{ccc}
\infer{\NoEquiv{A}{A'}}{\NoEquiv{A'}{A}} &
\infer{\NoEquiv{a\cdot S}{a\cdot S'}}{\NoEquiv{S}{S'}} &
\infer{\NoEquiv{a\cdot S}{a'\cdot S'}}{} \\\\
\infer{\NoEquiv{\PiTyp{A_1}{A_2}}{\PiTyp{A_1'}{A_2'}}}{\NoEquiv{A_1}{A_1'}} &
\infer{\NoEquiv{\PiTyp{A_1}{A_2}}{\PiTyp{A_1'}{A_2'}}}{\NoEquiv{A_2}{A_2'}} 
\end{array} 
$$

\bigskip 
\framebox{$\NoEquiv{M}{M'}$}
\bigskip 

$$
\begin{array}{ccc}
\infer{\NoEquiv{M}{M'}}{\NoEquiv{M'}{M}} &
\infer{\NoEquiv{i\cdot S}{i\cdot S'}}{\NoEquiv{S}{S'}} &
\infer{\NoEquiv{i\cdot S}{i'\cdot S'}}{} \\\\
\infer{\NoEquiv{c\cdot S}{c\cdot S'}}{\NoEquiv{S}{S'}} &
\infer{\NoEquiv{c\cdot S}{c'\cdot S'}}{c\NoStep & c'\NoStep} &
\infer{\NoEquiv{c\cdot S}{M}}{c\StepsTo M' & \NoEquiv{M' @ S}{M}} 
\end{array} 
$$

\bigskip 
\framebox{$\NoEquiv{S}{S'}$}
\bigskip 

$$
\begin{array}{ccc}
\infer{\NoEquiv{\Nil}{M;S}}{} &
\infer{\NoEquiv{M;S}{M';S'}}{\NoEquiv{M}{M'}} &
\infer{\NoEquiv{M;S}{M';S'}}{\NoEquiv{S}{S'}} 
\end{array} 
$$
