%include lhs2TeX.fmt

%if anyMath

%format .     = ".~"
%format alpha = "\alpha"
%format beta  = "\beta"
%format gamma = "\gamma"
%format delta = "\delta"
%format phi   = "\phi"
%format psi   = "\psi"
%format Set   = "\SET"
%format Sigma = "\Sigma"
%format |-    = "\vdash"
%format omega = "\omega"
%format Omega = "\Omega"
%format C1    = "C_1"
%format C2    = "C_2"
%format zero  = "0"

%format when  = "\mathbf{when}"

%endif

In this section we look at a few examples that illustrates the workings of the
type checker.

\subsubsection{A simple example}

First let us look at a very simple example. Consider the signature |Sigma = Nat : Set,
zero : Nat, id : (A : Set) -> A -> A = \A x. x, alpha : Set| containing a set |Nat| with an
element |zero|, a polymorphic identity function |id|, and a meta-variable
|alpha| of type |Set|. Now we want to compute |M| such that $\CheckTypeCtx {} {|id ?
zero|} {|alpha|} M$. To do this one of the conversion rules have to be applied,
so the type checker first infers the type of |id ? zero|.

{\small\[
    \Rule{ \InferTypeCtx {} {|id ? zero|} {|beta|} {|id beta zero|}}
    {\begin{array}{ccc}
	\begin{array}[b]{lll}
	    \InferTypeCtx {} {|id|} {|(A : Set) -> A -> A|} {|id|}
	&~&  \CheckTypeCtx {} {|?|} {|Set|} {|beta|}
	\end{array}
    &~&	\infer{ \CheckTypeCtx {} {|zero|} {|beta|} {|zero|} }
	{\begin{array}{lll}
	    \InferTypeCtx {} {|zero|} {|Nat|} {|zero|}
	&&  \InstMeta {|beta|} {|Nat|}
	\end{array}}
    \end{array}}
\]}
The inferred type |beta| is then compared against the expected type |alpha|,
resulting in the instantiation $\InstMeta {|alpha|} {|Nat|}$.
The final signature is |Nat : Set|, $0:\mathit{Nat}$, |id : (A : Set) -> A -> A = \A
x. x, alpha : Set = Nat, beta : Set = Nat| and $M = |id beta zero|$. Note that
it is important to look up the values of instantiated meta-variables--it would
not be correct to instantiate |alpha| to |beta|, since |beta| is not in scope
at the point where |alpha| is declared.

\subsubsection{An example with guarded constants}

In the previous example all constraints could be solved immediately so no
guarded constants had to be introduced. Now let us look at an example with
guarded constants. Consider the signature of natural numbers with a case
principle:

\begin{code}
    Nat : Set, zero : Nat, suc : Nat -> Nat,
    caseNat :  (P : Nat -> Set) -> P zero ->
	       ((n : Nat) -> P (suc n)) ->
	       (n : Nat) -> P n
\end{code}

In this signature we want to check that |caseNat ? zero (\n. n)| has type |Nat
-> Nat|. The first thing that happens is that the arguments to |caseNat| are checked
against their expected types. Checking |?| against |Nat -> Set| introduces a
fresh meta-variable
%
\begin{code}
alpha : Nat -> Set
\end{code}
%
Next the inferred type of |zero| is checked against the expected type |alpha
zero|. This produces an unsolved constraint |alpha zero = Nat|, so a guarded
constant is introduced:
%
\begin{code}
p : alpha zero = zero when alpha zero = Nat
\end{code}
%
Similarly, the third argument introduces a guarded constant.
%
\begin{code}
q : (n : Nat) -> alpha (suc n) = \n. n when (n : Nat) |- alpha (suc n) = Nat
\end{code}
%
The resulting type correct approximation is |caseNat alpha p (\n. q n)| of type
|(n : Nat) -> alpha n|.  This type is compared against the expected type |Nat
-> Nat| giving rise to the constraint |alpha n = Nat| which is solvable with
|alpha = \n. Nat|. Once |alpha| is instantiated we can perform a $\Simplify$
step to solve the guards on |p| and |q| and subsequently reduce |caseNat alpha
p (\n. q n)| to |caseNat (\n. Nat) zero (\n. n) : Nat -> Nat|.

\subsubsection{What could go wrong?} \label{secCoerce}

So far we have only looked at type correct examples, where nothing bad would
have happened if we had not introduced guarded constants when we did.  The
following example shows how things can go wrong. Take the signature |Nat : Set,
zero : Nat|. Now add the perfectly well-typed identity function |coerce|:
%
\begin{code}
coerce : (F : Nat -> Set) -> F zero -> F zero = \F x. x
\end{code}
%
For any well-typed term |t : B| and type |A|, |coerce ? t| will successfully
check against |A|, resulting in the constraints |alpha zero = B| and |A = alpha
zero|, none of which can be solved. If we did not introduce guarded constants
|coerce ? t| would reduce to |t| and hence we could use |coerce| to give an
arbitrary type to a term. For instance we can type\footnote{This only type
checks if we allow meta-variables to be instantiated to function types, which
is not the case in {\Core}. However, the type checking algorithm can be
extended to handle this, something we have done in the implementation.}
\begin{code}
omega  : (N -> N) -> N  = \x. x (coerce ? x)
Omega  : N	        = omega (coerce ? omega)
\end{code}
where without guarded constants |Omega| would reduce to the non-normalising
$\lambda$-term |(\x. x x) (\x. x x)|. With our, algorithm new guarded
constants are introduced for for the argument to |coerce| and for the
application of coerce. So the type correct appoximation of |Omega| would be
|omega p| where |p = coerce alpha q when alpha zero = N -> N| and |q = omega
when (N -> N) -> N = alpha zero|.