From d0b4ddcf964118101c2ab092943bf932085b68f4 Mon Sep 17 00:00:00 2001
From: Eric Zhao <21zhaoe@protonmail.com>
Date: Thu, 1 Jun 2023 19:14:42 -0400
Subject: [PATCH] formalism: Add synthetic unmarked polymorphic expression
 typing rules

---
 formalism/polymorphism.tex         | 29 +++++++++++++++++++++++++++++
 formalism/symbols/polymorphism.tex |  3 +++
 2 files changed, 32 insertions(+)

diff --git a/formalism/polymorphism.tex b/formalism/polymorphism.tex
index 1260698..a51e3e7 100644
--- a/formalism/polymorphism.tex
+++ b/formalism/polymorphism.tex
@@ -273,3 +273,32 @@ \subsubsection{Unmarked expressions}
     \subsumable{\ETypeAp{\EMV}{\TMV}}
   }
 \end{mathpar}
+
+\subsubsection{Marked expressions}
+\judgbox{\ensuremath{\bothCtxSynTypeM{\tvarCtx}{\ctx}{\EMV}{\TMV}}} $\EMV$ synthesizes type $\TMV$
+%
+\begin{mathpar}
+  \cdots
+
+  \inferrule[MSTypeLam]{
+    \bothCtxSynTypeM{\extendTvarCtx{\tvarCtx}{\MTVarMV}}{\ctx}{\ECMV}{\MTMV}
+  }{
+    \bothCtxSynTypeM{\tvarCtx}{\ctx}{\ECTypeLam{\MTVarMV}{\ECMV}}{\MTForall{\MTVarMV}{\MTMV}}
+  }
+
+  \inferrule[MSTypeAp1]{
+    \bothCtxSynTypeM{\tvarCtx}{\ctx}{\ECMV}{\MTMV} \\
+    \tvarCtxWFM{\tvarCtx}{\MTMV_2} \\
+    \matchedForall{\MTMV}{\MTVarMV}{\MTMV_1}
+  }{
+    \bothCtxSynTypeM{\tvarCtx}{\ctx}{\ECTypeAp{\ECMV}{\MTMV_2}}{\subst{\MTMV_1}{\MTMV_2}{\MTVarMV}}
+  }
+
+  \inferrule[MSTypeAp2]{
+    \bothCtxSynTypeM{\tvarCtx}{\ctx}{\ECMV}{\MTMV} \\
+    \tvarCtxWFM{\tvarCtx}{\MTMV'} \\
+    \notMatchedForall{\MTMV}
+  }{
+    \bothCtxSynTypeM{\tvarCtx}{\ctx}{\ECTypeAp{\ECMV}{\MTMV'}}{\MTUnknown}
+  }
+\end{mathpar}
diff --git a/formalism/symbols/polymorphism.tex b/formalism/symbols/polymorphism.tex
index cbcd123..fd2d1c6 100644
--- a/formalism/symbols/polymorphism.tex
+++ b/formalism/symbols/polymorphism.tex
@@ -47,8 +47,11 @@
 \newcommand{\inTvarCtx}[2]{\ensuremath{#2 \in #1}}
 \newcommand{\notInTvarCtx}[2]{\ensuremath{\goodcolor{\colorFailSideJudge}{#2 \not\in #1}}}
 \newcommand{\withTvarCtx}[2]{\ensuremath{#1 \vdash #2}}
+\newcommand{\withTvarCtxNot}[2]{\ensuremath{\goodcolor{\colorFailSideJudge}{#1 \centernot\vdash #2}}}
 \newcommand{\withTvarCtxU}[2]{\ensuremath{#1 \goodcolor{\colorUText}{\vdash_{\hspace{-4.25pt}\scaleto{U}{3.5pt}}} #2}}
+\newcommand{\withTvarCtxUNot}[2]{\ensuremath{\goodcolor{\colorFailSideJudge}{#1 \centernot\vdash_{\hspace{-4.25pt}\scaleto{U}{3.5pt}} #2}}}
 \newcommand{\withTvarCtxM}[2]{\ensuremath{#1 \goodcolor{\colorMText}{\vdash_{\hspace{-4.25pt}\scaleto{M}{3.5pt}}} #2}}
+\newcommand{\withTvarCtxMNot}[2]{\ensuremath{\goodcolor{\colorFailSideJudge}{#1 \centernot\vdash_{\hspace{-4.25pt}\scaleto{M}{3.5pt}} #2}}}
 \newcommand{\withTvarCtxMK}[2]{\ensuremath{#1 \goodcolor{\colorMKText}{\vdash} #2}}
 
 \newcommand{\withBothCtx}[3]{\ensuremath{#1; #2 \vdash #3}}