@@ -104,9 +104,9 @@ by implementation details. These meta-operations include:
104104\item \demph{Queries} which retrieve values from the proof state, without modifying
105105the state. For example, we can:
106106\begin{itemize}
107−\item Get the type of the current sub goal
108−\item Retrieve the local context $\Gamma$ at the current sub goal
109−\item Type check or normalise a term relative to $\Gamma$
107+\item Get the type of the current sub goal ($\MO{Type}$)
108+\item Retrieve the local context $\Gamma$ at the current sub goal ($\MO{Context}$)
109+\item Type check ($\MO{Check}$) or normalise ($\MO{Normalise}$) a term relative to $\Gamma$
110110\end{itemize}
111111\item \demph{Unification}, which unifies two terms (potentially solving sub goals)
112112relative to $\Gamma$
@@ -333,6 +333,10 @@ handle failure using the $\MO{Try}$ tactic combinator:
333333}
334334}
335335
336+We have a primitive tactic $\MO{Fail}$, which may be invoked by
337+any tactic which encounters a failure condition (for example, an unsolvable unification
338+problem) and is handled by $\MO{Try}$.
339+
336340\subsubsection{Creating binders}
337341
338342We also define primitive tactics for constructing binders. We can create a $\lambda$
@@ -667,8 +671,7 @@ the hole.
667671
668672\subsubsection{Elaborating bindings}
669673
670−To elaborate a $\lambda$ binding, we $\MO{Attack}$ the hole, which must be a function type
671−or elaboration will fail,
674+To elaborate a $\lambda$ binding, we $\MO{Attack}$ the hole, which must be a function type,
672675apply the $\MO{Lambda}$ tactic, elaborate the scope, then $\MO{Solve}$, which discharges
673676the $\MO{Attack}$:
674677
@@ -1227,6 +1230,89 @@ programs in \TT{}.
12271230
12281231\label{sect:instance}
12291232
1233+When elaborating applications, recall that we fill in implicit arguments by
1234+unification, and type class constraints by an $\MO{Instance}$ tactic which searches
1235+the context for an instance of the required type class.
1236+
1237+The $\MO{Instance}$ tactic begins by trying to find a solution in the local context,
1238+using the $\MO{Trivial}$ tactic, which attempts
1239+to solve the current goal with each local variable in turn. It is used as a very
1240+basic primitive for proof search, and is defined as follows:
1241+
1242+\DM{
1243+\AR{
1244+\MO{Trivial}\:\mq\:
1245+\RW{do}\:\AR{
1246+ \tv\gets\MO{Context}\\
1247+ \MO{TryAll}\:\tv
1248+ }
1249+\medskip\\
1250+\MO{TryAll}\:(\vv_1,\vv_2\ldots)\:\mq\:\MO{Try}\:\vv_1\:(\MO{TryAll}\:\vv_2\ldots)
1251+\\
1252+\MO{TryAll}\:\langle\rangle\:\mq\:\MO{Fail}
1253+}
1254+}
1255+
1256+For example, in the following function, we resolve the type class constraint required
1257+for the $\texttt{>}$ operator by finding an instance for \texttt{Ord a} in the local
1258+context:
1259+
1260+\begin{SaveVerbatim}{ordlocal}
1261+
1262+max : Ord a => a -> a -> a
1263+max x y = if (x > y) then x else y
1264+
1265+\end{SaveVerbatim}
1266+\useverb{ordlocal}
1267+
1268+If $\MO{Trivial}$ does not find a solution, $\MO{Instance}$ begins a global search,
1269+applying every type class instance, and attempting to resolve the instance's parameters
1270+recursively. Given an instance $\vI$ with parameters $\ta$:
1271+
1272+\DM{
1273+\MO{TryInstance}\:(\vI\:\ta)\:\mq\:\RW{do}\;
1274+\AR{
1275+\vec{\MO{Claim}}\:(\tx\Hab\ta)\\
1276+\ttinterp{\vI\:\tx}\\
1277+\vec{\MO{Focus}}\:\tx;\;\vec{\MO{Instance}}
1278+}
1279+}
1280+
1281+We define $\MO{Instance}$ as follows, using $\MO{AllInstances}$ to retrieve
1282+all possible type class instances in the form required by $\MO{TryInstance}$:
1283+
1284+\DM{
1285+\MO{Instance}\:\mq\:
1286+\MO{Try}\:
1287+\AR{
1288+\MO{Trivial}\\
1289+(\RW{do}\:\AR{
1290+\ti\gets\MO{AllInstances}\\
1291+\vec{\MO{TryInstance}}\:\ti
1292+)
1293+}
1294+}
1295+}
1296+
1297+In practice, for efficiency and to ensure that type class resolution terminates,
1298+we constrain the search by recording which instances are defined for each type class,
1299+and by ensuring that a recursive call of $\MO{Instance}$ is either searching for
1300+a different class, or a structurally smaller instance of the current class.
1301+
1302+For example, in the following function, we resolve the constraints required by the
1303+\tFN{show} function by a global search which locates a \tTC{Show} instance for
1304+\tTC{List a}, which in turn requires a \tTC{Show} instance for \texttt{a}.
1305+In this case \texttt{a} is instantiated by \tTC{Int}, so we finish by locating
1306+a \tTC{Show} instance for \tTC{Int}:
1307+
1308+\begin{SaveVerbatim}{showinst}
1309+
1310+main : IO ()
1311+main = putStrLn (show [1,2,3,4])
1312+
1313+\end{SaveVerbatim}
1314+\useverb{showinst}
1315+
12301316\subsection{Syntax Extensions}
12311317
12321318\subsubsection{Metavariables}