Revise implementation of overlapping type family instances.

This commit changes the syntax and story around overlapping type
family instances. Before, we had "unbranched" instances and
"branched" instances. Now, we have closed type families and
open ones.

The behavior of open families is completely unchanged. In particular,
coincident overlap of open type family instances still works, despite
emails to the contrary.

A closed type family is declared like this:
> type family F a where
>   F Int = Bool
>   F a   = Char
The equations are tried in order, from top to bottom, subject to
certain constraints, as described in the user manual. It is not
allowed to declare an instance of a closed family.

5 files changed, 42 insertions, 10 deletions

diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index beaf52a7d9..c452877ad5 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -229,7 +229,7 @@ forall </ ni // i />. (</ s1j // j /> ~> t1) = (</ axBranchkk // kk />)[ind]
 </ substi @ // i /> = inits(</ [ ni |-> s'i ] // i />)
 </ ni = zi_ki // i />
 </ k'i <: substi(ki) // i />
-no_conflict(C, </ s2j // j />, ind-1)
+no_conflict(C, </ s2j // j />, ind, ind-1)
 </ s2j = s1j </ [ni |-> s'i] // i/> // j />
 t2 = t1 </ [ni |-> t'i] // i />
 G |-ty t2 : k
@@ -403,16 +403,32 @@ Constraint <: *
 ------------------ :: LiftedConstraint
 * <: Constraint
 
-defn no_conflict ( C , </ sj // j /> , ind ) ::  :: check_no_conflict :: 'NoConflict_'
-  {{ com Branched axiom conflict checking, \coderef{coreSyn/CoreLint.lhs}{lintCoercion\#check\_no\_conflict} }}
+defn no_conflict ( C , </ sj // j /> , ind1 , ind2 ) ::  :: check_no_conflict :: 'NoConflict_'
+  {{ com \parbox{5in}{Branched axiom conflict checking, \coderef{types/OptCoercion.lhs}{checkAxInstCo} \\ and \coderef{types/FamInstEnv.lhs}{compatibleBranches} } }}
 by
 
 ------------------------------------------------ :: NoBranch
-no_conflict(C, </ si // i/>, -1)
+no_conflict(C, </ si // i/>, ind, -1)
 
 C = T </ axBranchkk // kk />
-forall </ ni // i />. (</ tj // j /> ~> t') = (</ axBranchkk // kk />)[ind]
+forall </ ni // i />. (</ tj // j /> ~> t') = (</ axBranchkk // kk />)[ind2]
 apart(</ sj // j />, </ tj // j />)
-no_conflict(C, </ sj // j />, ind-1)
------------------------------------------------- :: Branch
-no_conflict(C, </ sj // j />, ind)
+no_conflict(C, </ sj // j />, ind1, ind2-1)
+------------------------------------------------ :: Incompat
+no_conflict(C, </ sj // j />, ind1, ind2)
+
+C = T </ axBranchkk // kk />
+forall </ ni // i />. (</ tj // j /> ~> s) = (</ axBranchkk // kk />)[ind1]
+forall </ n'i // i />. (</ t'j // j /> ~> s') = (</ axBranchkk // kk />)[ind2]
+apart(</ tj // j />, </ t'j // j />)
+no_conflict(C, </ sj // j />, ind1, ind2-1)
+------------------------------------------- :: CompatApart
+no_conflict(C, </ sj // j />, ind1, ind2)
+
+C = T </ axBranchkk // kk />
+forall </ ni // i />. (</ tj // j /> ~> s) = (</ axBranchkk // kk />)[ind1]
+forall </ n'i // i />. (</ t'j // j /> ~> s') = (</ axBranchkk // kk />)[ind2]
+unify(</ tj // j />, </ t'j // j />) = subst
+subst(s) = subst(s')
+----------------------------------------- :: CompatCoincident
+no_conflict(C, </ sj // j />, ind1, ind2)
\ No newline at end of file
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index 4c59849bb6..ca27b8b34c 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -117,7 +117,7 @@ LorR :: 'LeftOrRight_' ::= {{ com left or right deconstructor, \coderef{types/Co
 
 C :: 'CoAxiom_' ::= {{ com Axioms, \coderef{types/TyCon.lhs}{CoAxiom} }}
   | T </ axBranchi // ; // i />    ::   :: CoAxiom  {{ com Axiom }}
-  | ( C )                              :: M :: Parens   {{ com Parentheses }}
+  | ( C )                          :: M :: Parens   {{ com Parentheses }}
 
 axBranch, b :: 'CoAxBranch_' ::= {{ com Axiom branches, \coderef{types/TyCon.lhs}{CoAxBranch} }}
   | forall </ ni // i /> . ( </ tj // j /> ~> s )  ::   :: CoAxBranch  {{ com Axiom branch }}
@@ -229,6 +229,7 @@ terminals :: 'terminals_' ::=
   | Constraint   ::   :: Constraint       {{ tex \textsf{Constraint} }}
   | no_conflict  ::   :: no_conflict      {{ tex \textsf{no\_conflict} }}
   | apart        ::   :: apart            {{ tex \textsf{apart} }}
+  | unify        ::   :: unify            {{ tex \textsf{unify} }}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Formulae  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -270,6 +271,7 @@ formula :: 'formula_' ::=
   | axBranch1 = axBranch2              ::   :: branch_rewrite
   | C1 = C2                            ::   :: axiom_rewrite
   | apart ( </ ti // i /> , </ sj // j /> ) :: :: apart
+  | unify ( </ ti // i /> , </ sj // j /> ) = subst :: :: unify
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Subrules and Parsing  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/docs/core-spec/Makefile b/docs/core-spec/Makefile
index 9449a0e1af..3dfed54e15 100644
--- a/docs/core-spec/Makefile
+++ b/docs/core-spec/Makefile
@@ -5,6 +5,7 @@ TARGET    = core-spec
 
 $(TARGET).pdf: $(TARGET).tex $(OTT_TEX)
 	latex -output-format=pdf $<
+	latex -output-format=pdf $<
 
 $(TARGET).tex: $(TARGET).mng $(OTT_FILES)
 	ott $(OTT_OPTS) -tex_filter $< $@ $(OTT_FILES)
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index 4b1e986c6d..10ed4f7e9f 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -150,6 +150,12 @@ Axioms:
 \ottaxBranch
 }
 
+The definition for $[[axBranch]]$ above does not include the list of
+incompatible branches (field \texttt{cab\_incomps} of \texttt{CoAxBranch}),
+as that would unduly clutter this presentation. Instead, as the list
+of incompatible branches can be computed at any time, it is checked for
+in the judgment $[[no_conflict]]$. See Section~\ref{sec:no_conflict}.
+
 \subsection{Type constructors}
 
 Type constructors in GHC contain \emph{lots} of information. We leave most of it out
@@ -306,10 +312,14 @@ There are two very similar checks for names, one declared as a local function:
 \ottdefnisSubKind{}
 
 \subsection{Branched axiom conflict checking}
+\label{sec:no_conflict}
 
 The following judgment is used within \ottdrulename{Co\_AxiomInstCo} to make
 sure that a type family application cannot unify with any previous branch
-in the axiom.
+in the axiom. The actual code scans through only those branches that are
+flagged as incompatible. These branches are stored directly in the
+$[[axBranch]]$. However, it is cleaner in this presentation to simply
+check for compatibility here.
 
 \ottdefncheckXXnoXXconflict{}
 
@@ -318,4 +328,7 @@ It checks to see if \coderef{types/Unify.lhs}{tcApartTys} returns \texttt{Surely
 Two types are apart if neither type is a type family application and if they do not
 unify.
 
+The algorithm $[[unify]]$ is implemented in \coderef{types/Unify.lhs}{tcUnifyTys}.
+It performs a standard unification, returning a substitution upon success.
+
 \end{document}
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index be13ca22c5..21de3642a3 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf