diff --git a/papers/hatra21/hatra21.pdf b/papers/hatra21/hatra21.pdf
index 293e29eb..b170c533 100644
Binary files a/papers/hatra21/hatra21.pdf and b/papers/hatra21/hatra21.pdf differ
diff --git a/papers/hatra21/hatra21.tex b/papers/hatra21/hatra21.tex
index 26f78e71..4f083479 100644
--- a/papers/hatra21/hatra21.tex
+++ b/papers/hatra21/hatra21.tex
@@ -5,6 +5,9 @@
 \acmYear{2021}
 \acmConference[HATRA '21]{Human Aspects of Types and Reasoning Assistants}{October 2021}{Chicago, IL}
 
+\newcommand{\squnder}[1]{\underline{#1}}
+\newcommand{\infer}[2]{\frac{\textstyle#1}{\textstyle#2}}
+
 \begin{document}
 
 \title{Position Paper: Goals of the Luau Type System}
@@ -129,17 +132,50 @@ even to creators who are not explicitly providing types.
 \section{Types}
 \subsection{Infallible types}
 
-Goal: support type-directed tools in all programs
+Goal: \emph{support type-driven tools in all programs}.
 
-- All programs have a type (analogy with infallible parsers)
+Programs spend much of their time under development in an incomplete state, even if the final arifact
+is well-typed. Type-driven tools should support this, by providing type information for all programs.
 
-- Used by autocomplete + goto-declaration
+An analogy is infallible parsers, which perform error recovery and provide an AST for all input texts.
 
-- Still support red squigglies
+Program analysis can still flag type errors, for example with red
+squiggly underlining. Formalizing this, rather than a judgement
+$\Gamma\vdash M:T$, for an input terms $M$, there is a judgement
+$\Gamma \vdash M \Rightarrow M' : T$ where $M'$ is an output term
+where some subterms are flagged $\squnder{M}$. For example the usual type rules for field access becomes:
+\[
+  \infer{
+    \Gamma \vdash M \Rightarrow M' : T
+  }{
+    \Gamma \vdash M.\ell \Rightarrow M'.\ell : U
+  }
+  [
+    T = \{ \overline{\ell:U} \} \mbox{ and } (\ell:U) \in (\overline{\ell:U})
+  ]
+\]
+but there is also a rule for unsuccesful field access:  
+\[
+  \infer{
+    \Gamma \vdash M \Rightarrow M' : T
+  }{
+    \Gamma \vdash M.\ell \Rightarrow \squnder{M'.\ell} : U
+  }
+  [
+    T = \{ \overline{\ell:U} \} \mbox{ implies } \ell \not\in \overline{\ell}
+  ]
+\]
+In this type rule, $U$ is unconstrained.
 
-- Problem: stop the user being swamped by cascading errors
-
-- Problem: no ``right'' type, just heuristics
+Some issues raised by infallible types:
+\begin{itemize}
+\item Which heuristics should be used to provide types for flagged programs? For example, could one
+  use minimal edit distance to correct for spelling mistakes in field names?
+\item How can we avoid cascading type errors, where a developer is
+  faced with type errors that are artifacts of the heuristics rather
+  than genuine errors?
+\item How can the goals of an infallible type system be formalized?
+\end{itemize}
 
 \subsection{Strict types}