Improve handling of data type return kindswip/T18300

Following a long conversation with Richard, this patch tidies up the
handling of return kinds for data/newtype declarations (vanilla,
family, and instance).

I have substantially edited the Notes in TyCl, so they would
bear careful reading.

Fixes #18300, #18357

In GHC.Tc.Instance.Family.newFamInst we were checking some Lint-like
properties with ASSSERT.  Instead Richard and I have added
a proper linter for axioms, and called it from lintGblEnv, which in
turn is called in tcRnModuleTcRnM

New tests (T18300, T18357) cause an ASSERT failure in HEAD.

4 files changed, 83 insertions, 3 deletions

diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index 6aff07c499..092c894690 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -656,3 +656,43 @@ unify(</ tj // j />, </ t'j // j />) = subst
 subst(s) = subst(s')
 ----------------------------------------- :: CompatCoincident
 no_conflict(C, </ sj // j />, ind1, ind2)
+
+defn |- axiom C ok :: :: lint_axiom :: 'Ax_'
+  {{ com Coercion axiom linting, \coderef{GHC/Core/Lint.hs}{lint\_axiom} }}
+  {{ tex \labeledjudge{axiom} [[C]] [[ok]] }}
+by
+
+isNewTyCon T
+</ Ri // i /> = tyConRoles T
+</ alphai_ki // i /> |-ty T </ alphai$ // i /> : k0
+</ alphai_ki // i /> |-ty s : k0
+------------------------------ :: Newtype
+|-axiom T_Rep forall </ alphai_ki RAi // i />. (</ alphai$ // i /> ~> s) ok
+
+isOpenTypeFamilyTyCon T
+T |-branch b ok
+------------------------------ :: OpenTypeFamily
+|-axiom T_Nom b ok
+
+isClosedTypeFamilyTyCon T
+</ T |-branch bi ok // i />
+--------------------------- :: ClosedTypeFamily
+|-axiom T_Nom </ bi // i /> ok
+
+isDataFamilyTyCon T
+T |-branch b ok
+--------------------------- :: DataFamily
+|-axiom T_Rep b ok
+
+defn T |- branch b ok :: :: lint_family_branch :: 'Br_'
+  {{ com Type family branch linting, \coderef{GHC/Core/Lint.hs}{lint\_family\_branch} }}
+  {{ tex [[T]] \labeledjudge{branch} [[b]] [[ok]] }}
+by
+
+</ Ri = Nom // i />
+</ isTyFamFree tj // j />
+fv(</ tj // j />) = </ alphai$ // i />
+</ alphai_ki // i /> |-ty T </ tj // j /> : k0
+</ alphai_ki // i /> |-ty s : k0
+---------------------------------------------------------------- :: OK
+T |-branch forall </ alphai_ki RAi // i />. (</ tj // j /> ~> s) ok
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index 0b9893c3a9..aa1bec8ef9 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -52,10 +52,10 @@ l :: 'Label_' ::= {{ com Labels for join points, also \coderef{GHC/Types/Var.hs}
 
 vars :: 'Vars_' ::= {{ com List of variables }}
   | </ ni // , // i />       ::   :: List
-  | fv ( t )                 :: M :: fv_t
-    {{ tex \textit{fv}([[t]]) }}
   | fv ( e )                 :: M :: fv_e
     {{ tex \textit{fv}([[e]]) }}
+  | fv ( types )             :: M :: fv_types
+    {{ tex \textit{fv}([[types]]) }}
   | empty                    :: M :: empty
   | vars1 \inter vars2       :: M :: intersection
     {{ tex [[vars1]] \cap [[vars2]] }}
@@ -197,7 +197,7 @@ R {{ tex \rho }} :: 'Role_' ::= {{ com Roles, \coderef{GHC/Core/Coercion/Axiom.h
 
 axBranch, b :: 'CoAxBranch_' ::= {{ com Axiom branches, \coderef{GHC/Core/TyCon.hs}{CoAxBranch} }}
   | forall </ ni RAi // i /> . ( </ tj // j /> ~> s )  ::   :: CoAxBranch  {{ com \ctor{CoAxBranch}: Axiom branch }}
-  | ( </ axBranchi // i /> ) [ ind ]               :: M :: lookup      {{ com List lookup }}
+  | ( </ axBranchi // i /> ) [ ind ]                   :: M :: lookup      {{ com List lookup }}
 
 mu {{ tex \mu }} :: 'CoAxiomRule_' ::= {{ com CoAxiomRules, \coderef{GHC/Core/Coercion/Axiom.hs}{CoAxiomRule} }}
   | M ( I , role_list , R' )   ::  :: CoAxiomRule  {{ com Named rule, with parameter info }}
@@ -376,6 +376,10 @@ terminals :: 'terminals_' ::=
   | dataConTyCon ::   :: dataConTyCon     {{ tex \textsf{dataConTyCon} }}
   | dataConRepType :: :: dataConRepType   {{ tex \textsf{dataConRepType} }}
   | isNewTyCon   ::   :: isNewTyCon       {{ tex \textsf{isNewTyCon} }}
+  | isOpenTypeFamilyTyCon :: :: isOpenTypeFamilyTyCon {{ tex \textsf{isOpenTypeFamilyTyCon} }}
+  | isClosedTypeFamilyTyCon :: :: isClosedTypeFamilyTyCon {{ tex \textsf{isClosedTypeFamilyTyCon} }}
+  | isDataFamilyTyCon :: :: isDataFamilyTyCon {{ tex \textsf{isDataFamilyTyCon} }}
+  | isTyFamFree  ::   :: isTyFamFree      {{ tex \textsf{isTyFamFree} }}
   | Constraint   ::   :: Constraint       {{ tex \textsf{Constraint} }}
   | TYPE         ::   :: TYPE             {{ tex \textsf{TYPE} }}
   | RuntimeRep   ::   :: RuntimeRep       {{ tex \textsf{RuntimeRep} }}
@@ -449,6 +453,10 @@ formula :: 'formula_' ::=
   | G |- tylit lit : k                 ::   :: lintTyLit
     {{ tex [[G]] \labeledjudge{tylit} [[lit]] : [[k]] }}
   | isNewTyCon T                       ::   :: isNewTyCon
+  | isOpenTypeFamilyTyCon T            ::   :: isOpenTypeFamilyTyCon
+  | isClosedTypeFamilyTyCon T          ::   :: isClosedTypeFamilyTyCon
+  | isDataFamilyTyCon T                ::   :: isDataFamilyTyCon
+  | isTyFamFree t                      ::   :: isTyFamFree
   | k1 elt { </ ki // , // i /> }      ::   :: kind_elt
   | e is_a_type                        ::   :: is_a_type
     {{ tex \exists \tau \text{ s.t.~} [[e]] = \tau }}
@@ -526,3 +534,4 @@ Expr_Coercion <= Subst_TmMapping
 
 Type_CastTy <= Var_IdOrTyVar
 
+Expr_Type <= Vars_fv_e
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index 18a856f4e6..1e77f3b4de 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -573,6 +573,37 @@ taking care to map identical type family applications to the same fresh variable
 The algorithm $[[unify]]$ is implemented in \coderef{GHC/Core/Unify.hs}{tcUnifyTys}.
 It performs a standard unification, returning a substitution upon success.
 
+\subsection{Axioms}
+
+After type-checking the type and class declarations of a file, the axioms
+in the file are optionally linted. This is done from \coderef{GHC/Tc/Types.hs}{lintGblEnv},
+which calls \coderef{GHC/Core/Lint.hs}{lintAxioms}. That function ensures
+the following judgement on each axiom:
+
+\ottdefnlintXXaxiom{}
+
+\ottdefnlintXXfamilyXXbranch{}
+
+In addition to these checks, the linter will also check several other conditions:
+
+\begin{itemize}
+\item Every \texttt{CoAxBranch} has a \texttt{cab\_cvs} field. This is unused
+currently and should always be empty.
+\item Every \texttt{CoAxBranch} has a \texttt{cab\_eta\_tvs} field. This is used
+only for data family instances, but is not involved in type correctness. (It is
+used for pretty-printing.) The implemented linter checks to make sure this field
+is empty for axioms that are not associated with data family instances.
+\item Every \texttt{CoAxBranch} has a \texttt{cab\_incomps} field that stores
+a list of incompatible branches. The implemented linter checks that these
+branches are indeed incompatible with the current one.
+\item The linter checks that newtypes are associated with exactly one axiom,
+as are closed type families.
+\item The linter checks that all instances of the same open family are compatible.
+\end{itemize}
+
+A nice summary of the required checks is in Section F.1 of the \emph{Safe Coercions}
+paper (JFP'16).
+
 \section{Operational semantics}
 
 \subsection{Disclaimer}
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index 97da6c89f1..8d77a63f5f 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf