Commit 9a96ff6b authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Marge Bot

Update core spec to reflect changes to Core.

Key changes:
 * Adds a new rule for forall-coercions over coercion variables, which
was implemented but conspicuously missing from the spec.
 * Adds treatment for FunCo.
 * Adds treatment for ForAllTy over coercion variables.
 * Improves commentary (including restoring a Note lost in
03d48526) in the source.

No changes to running code.
parent faa36e5b
Pipeline #16961 passed with stages
in 340 minutes and 21 seconds
......@@ -29,6 +29,8 @@ for l in linters:
# Don't lint font files
l.add_path_filter(lambda path: not path.parent == Path('docs','users_guide',
'rtd-theme', 'static', 'fonts'))
# Don't lint core spec
l.add_path_filter(lambda path: not path.name == 'core-spec.pdf')
if __name__ == '__main__':
run_linters(linters)
......@@ -1371,7 +1371,7 @@ promoteCoercion co = case co of
ForAllCo _ _ _
-> ASSERT( False )
mkNomReflCo liftedTypeKind
-- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
-- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
FunCo _ _ _
-> ASSERT( False )
......@@ -1420,7 +1420,7 @@ promoteCoercion co = case co of
| otherwise
-> ASSERT( False)
mkNomReflCo liftedTypeKind
-- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
-- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
KindCo _
-> ASSERT( False )
......
......@@ -1467,7 +1467,6 @@ lintType t@(ForAllTy (Bndr cv _vis) ty)
; checkValueKind k (text "the body of forall:" <+> ppr t)
; return liftedTypeKind
-- We don't check variable escape here. Namely, k could refer to cv'
-- See Note [NthCo and newtypes] in GHC.Core.TyCo.Rep
}}
lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
......@@ -1826,7 +1825,7 @@ lintCoercion (ForAllCo cv1 kind_co co)
; (k3, k4, t1, t2, r) <- lintCoercion co
; checkValueKind k3 (text "the body of a ForAllCo over covar:" <+> ppr co)
; checkValueKind k4 (text "the body of a ForAllCo over covar:" <+> ppr co)
-- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
-- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
; in_scope <- getInScope
; let tyl = mkTyCoInvForAllTy cv1 t1
r2 = coVarRole cv1
......@@ -1845,7 +1844,7 @@ lintCoercion (ForAllCo cv1 kind_co co)
tyr = mkTyCoInvForAllTy cv2 $
substTy subst t2
; return (liftedTypeKind, liftedTypeKind, tyl, tyr, r) } }
-- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
-- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
lintCoercion co@(FunCo r co1 co2)
= do { (k1,k'1,s1,t1,r1) <- lintCoercion co1
......@@ -2019,7 +2018,7 @@ lintCoercion (InstCo co arg)
, CoercionTy s2' <- s2
-> do { return $
(liftedTypeKind, liftedTypeKind
-- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
-- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
, substTy (mkCvSubst in_scope $ unitVarEnv cv1 s1') t1
, substTy (mkCvSubst in_scope $ unitVarEnv cv2 s2') t2
, r) }
......
......@@ -206,6 +206,9 @@ data Type
| ForAllTy
{-# UNPACK #-} !TyCoVarBinder
Type -- ^ A Π type.
-- INVARIANT: If the binder is a coercion variable, it must
-- be mentioned in the Type. See
-- Note [Unused coercion variable in ForAllTy]
| FunTy -- ^ t1 -> t2 Very common, so an important special case
-- See Note [Function types]
......@@ -218,9 +221,10 @@ data Type
| CastTy
Type
KindCoercion -- ^ A kind cast. The coercion is always nominal.
-- INVARIANT: The cast is never refl.
-- INVARIANT: The cast is never reflexive
-- INVARIANT: The Type is not a CastTy (use TransCo instead)
-- See Note [Respecting definitional equality] (EQ2) and (EQ3)
-- INVARIANT: The Type is not a ForAllTy over a type variable
-- See Note [Respecting definitional equality] (EQ2), (EQ3), (EQ4)
| CoercionTy
Coercion -- ^ Injection of a Coercion into a type
......@@ -567,10 +571,19 @@ be pulled to the right. But we don't need to pull it: (T |> axFun) Int is not
`eqType` to any proper TyConApp -- thus, leaving it where it is doesn't violate
our (EQ) property.
Lastly, in order to detect reflexive casts reliably, we must make sure not
In order to detect reflexive casts reliably, we must make sure not
to have nested casts: we update (t |> co1 |> co2) to (t |> (co1 `TransCo` co2)).
In sum, in order to uphold (EQ), we need the following three invariants:
One other troublesome case is ForAllTy. See Note [Weird typing rule for ForAllTy].
The kind of the body is the same as the kind of the ForAllTy. Accordingly,
ForAllTy tv (ty |> co) and (ForAllTy tv ty) |> co
are `eqType`. But only the first can be split by splitForAllTy. So we forbid
the second form, instead pushing the coercion inside to get the first form.
This is done in mkCastTy.
In sum, in order to uphold (EQ), we need the following invariants:
(EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
cast is one that relates either a FunTy to a FunTy or a
......@@ -578,7 +591,7 @@ In sum, in order to uphold (EQ), we need the following three invariants:
(EQ2) No reflexive casts in CastTy.
(EQ3) No nested CastTys.
(EQ4) No CastTy over (ForAllTy (Bndr tyvar vis) body).
See Note [Weird typing rule for ForAllTy] in GHC.Core.Type.
See Note [Weird typing rule for ForAllTy]
These invariants are all documented above, in the declaration for Type.
......@@ -607,6 +620,45 @@ There are cases we want to skip the check. For example, the check is
unnecessary when it is known from the context that the input variable
is a type variable. In those cases, we use mkForAllTy.
Note [Weird typing rule for ForAllTy]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Here is the (truncated) typing rule for the dependent ForAllTy:
inner : TYPE r
tyvar is not free in r
----------------------------------------
ForAllTy (Bndr tyvar vis) inner : TYPE r
Note that the kind of `inner` is the kind of the overall ForAllTy. This is
necessary because every ForAllTy over a type variable is erased at runtime.
Thus the runtime representation of a ForAllTy (as encoded, via TYPE rep, in
the kind) must be the same as the representation of the body. We must check
for skolem-escape, though. The skolem-escape would prevent a definition like
undefined :: forall (r :: RuntimeRep) (a :: TYPE r). a
because the type's kind (TYPE r) mentions the out-of-scope r. Luckily, the real
type of undefined is
undefined :: forall (r :: RuntimeRep) (a :: TYPE r). HasCallStack => a
and that HasCallStack constraint neatly sidesteps the potential skolem-escape
problem.
If the bound variable is a coercion variable:
inner : TYPE r
covar is free in inner
------------------------------------
ForAllTy (Bndr covar vis) inner : Type
Here, the kind of the ForAllTy is just Type, because coercion abstractions
are *not* erased. The "covar is free in inner" premise is solely to maintain
the representation invariant documented in
Note [Unused coercion variable in ForAllTy]. Though there is surface similarity
between this free-var check and the one in the tyvar rule, these two restrictions
are truly unrelated.
-}
-- | A type labeled 'KnotTied' might have knot-tied tycons in it. See
......@@ -1003,6 +1055,7 @@ data Coercion
-- The TyCon is never a synonym;
-- we expand synonyms eagerly
-- But it can be a type function
-- TyCon is never a saturated (->); use FunCo instead
| AppCo Coercion CoercionN -- lift AppTy
-- AppCo :: e -> N -> e
......
......@@ -1382,6 +1382,7 @@ mkCastTy (CastTy ty co1) co2
mkCastTy (ForAllTy (Bndr tv vis) inner_ty) co
-- (EQ4) from the Note
-- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep.
| isTyVar tv
, let fvs = tyCoVarsOfCo co
= -- have to make sure that pushing the co in doesn't capture the bound var!
......
......@@ -1507,7 +1507,7 @@ ty_co_match menv subst (ForAllTy (Bndr tv1 _) ty1)
-- subst2 <- ty_co_match menv subst1 s2 eta2 kco3 kco4
-- Question: How do we get kcoi?
-- 2. Given:
-- lkco :: <*> -- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
-- lkco :: <*> -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
-- rkco :: <*>
-- Wanted:
-- ty_co_match menv' subst2 ty1 co2 lkco' rkco'
......
......@@ -4,3 +4,4 @@
CoreOtt.tex
core-spec.tex
*.fls
*.out
......@@ -232,8 +232,8 @@ G |-co g1 : s1 k1~R k'1 t1
G |-co g2 : s2 k2~R k'2 t2
G |-arrow k1 -> k2 : k
G |-arrow k'1 -> k'2 : k'
------------------------- :: TyConAppCoFunTy
G |-co (->)_R g1 g2 : (s1 -> s2) k~R k' (t1 -> t2)
------------------------- :: FunCo
G |-co g1 ->_R g2 : (s1 -> s2) k~R k' (t1 -> t2)
T /= (->)
</ Ri // i /> = take(length </ gi // i />, tyConRolesX R T)
......@@ -258,9 +258,19 @@ G |-app (t2 : k2') : k2 ~> k4
G |-co g1 g2 : (s1 t1) k3~Ph k4 (s2 t2)
G |-co h : k1 *~Nom * k2
G, z_k1 |-co g : t1 k3~R k4 t2
------------------------------------------------------------------ :: ForAllCo
G |-co forall z:h. g : (forall z_k1. t1) k3~R k4 (forall z_k2. (t2[z |-> z_k2 |> sym h]))
G, alpha_k1 |-co g : t1 k3~R k4 t2
------------------------------------------------------------------ :: ForAllCo_Tv
G |-co forall alpha:h. g : (forall alpha_k1. t1) k3~R k4 (forall alpha_k2. (t2[alpha |-> alpha_k2 |> sym h]))
G |-co h : k1 *~Nom * k2
G, x_k1 |-co g : t1 {TYPE s1}~R {TYPE s2} t2
R2 = coercionRole x_k1
h' = downgradeRole R2 h
h1 = nth R2 2 h'
h2 = nth R2 3 h'
almostDevoid x g
------------------------------------------- :: ForAllCo_Cv
G |-co forall x:h.g : (forall x_k1. t1) *~R * (forall x_k2. (t2[ x |-> h1 ; x_k2 ; sym h2 ]))
z_phi elt G
phi = t1 k1~#k2 t2
......@@ -495,10 +505,17 @@ G |-app </ (ti : ki) // i /> : tyConKind T ~> k
G |-ty T </ ti // i /> : k
G |-ki k1 ok
G, z_k1 |-ty t : TYPE s
not (z elt fv(s))
------------------------ :: ForAllTy
G |-ty forall z_k1. t : TYPE s
G, alpha_k1 |-ty t : TYPE s
not (alpha elt fv(s))
------------------------ :: ForAllTy_Tv
G |-ty forall alpha_k1. t : TYPE s
phi = s1 k1~#k2 s2
G |-ki phi ok
G, x_phi |-ty t : TYPE s
x elt fv(t)
--------------------- :: ForAllTy_Cv
G |-ty forall x_phi.t : *
G |-tylit lit : k
-------------- :: LitTy
......
......@@ -143,6 +143,7 @@ g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coder
| < t > R mg :: :: GRefl {{ com \ctor{GRefl}: Generalized Reflexivity }}
{{ tex {\langle [[t]] \rangle}^{[[mg]]}_{[[R]]} }}
| T RA </ gi // i /> :: :: TyConAppCo {{ com \ctor{TyConAppCo}: Type constructor application }}
| g1 -> RA g2 :: :: FunCo {{ com \ctor{FunCo}: Functions }}
| g1 g2 :: :: AppCo {{ com \ctor{AppCo}: Application }}
| forall z : h . g :: :: ForAllCo {{ com \ctor{ForAllCo}: Polymorphism }}
{{ tex [[forall]] [[z]]{:}[[h]].[[g]] }}
......@@ -162,6 +163,7 @@ g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coder
| sub g :: :: SubCo {{ com \ctor{SubCo}: Sub-role --- convert nominal to representational }}
| ( g ) :: M :: Parens {{ com Parentheses }}
| t $ liftingsubst :: M :: Lifted {{ com Type lifted to coercion }}
| downgradeRole R g :: M :: downgradeRole {{ com \textsf{downgradeRole} }}
prov :: 'UnivCoProvenance_' ::= {{ com \ctor{UnivCo} provenance, \coderef{types/TyCoRep.hs}{UnivCoProvenance} }}
| UnsafeCoerceProv :: :: UnsafeCoerceProv {{ com From \texttt{unsafeCoerce\#} }}
......@@ -396,8 +398,10 @@ terminals :: 'terminals_' ::=
| --> :: :: steps {{ tex \longrightarrow }}
| coercionKind :: :: coercionKind {{ tex \textsf{coercionKind} }}
| coercionRole :: :: coercionRole {{ tex \textsf{coercionRole} }}
| downgradeRole :: :: downgradeRole {{ tex \textsf{downgradeRole} }}
| take :: :: take {{ tex \textsf{take}\! }}
| coaxrProves :: :: coaxrProves {{ tex \textsf{coaxrProves} }}
| almostDevoid :: :: almostDevoid {{ tex \textsf{almostDevoid} }}
| Just :: :: Just {{ tex \textsf{Just} }}
| \\ :: :: newline {{ tex \\ }}
| classifiesTypeWithValues :: :: ctwv {{ tex \textsf{classifiesTypeWithValues} }}
......@@ -483,6 +487,7 @@ formula :: 'formula_' ::=
| z elt vars :: :: in_vars
| split _ I s = types :: :: split_type
{{ tex \mathop{\textsf{split} }_{[[I]]} [[s]] = [[types]] }}
| almostDevoid x g :: :: almostDevoid
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Subrules and Parsing %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......
......@@ -7,6 +7,7 @@
\usepackage{xcolor}
\usepackage{fullpage}
\usepackage{multirow}
\usepackage{hyperref}
\usepackage{url}
\newcommand{\ghcfile}[1]{\textsl{#1}}
......@@ -106,10 +107,10 @@ There are a few key invariants about expressions:
\item The right-hand sides of all top-level and recursive $[[let]]$s
must be of lifted type, with one exception: the right-hand side of a top-level
$[[let]]$ may be of type \texttt{Addr\#} if it's a primitive string literal.
See \verb|#top_level_invariant#| in \ghcfile{coreSyn/CoreSyn.hs}.
See \verb|#top_level_invariant#| in \ghcfile{GHC.Core}.
\item The right-hand side of a non-recursive $[[let]]$ and the argument
of an application may be of unlifted type, but only if the expression
is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{coreSyn/CoreSyn.hs}.
is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{GHC.Core}.
\item We allow a non-recursive $[[let]]$ for bind a type variable.
\item The $[[_]]$ case for a $[[case]]$ must come first.
\item The list of case alternatives must be exhaustive.
......@@ -119,7 +120,7 @@ In other words, the payload inside of a \texttt{Type} constructor must not turn
to be built with \texttt{CoercionTy}.
\item Join points (introduced by $[[join]]$ expressions) follow the invariants
laid out in \verb|Note [Invariants on join points]| in
\ghcfile{coreSyn/CoreSyn.hs}:
\ghcfile{GHC.Core}:
\begin{enumerate}
\item All occurrences must be tail calls. This is enforced in our typing
rules using the label environment $[[D]]$.
......@@ -166,13 +167,14 @@ A program is just a list of bindings:
\gram{\ottprogram}
\subsection{Types}
\label{sec:types}
\gram{\ottt}
\ctor{FunTy} is the special case for non-dependent function type. The
\ctor{TyBinder} in \ghcfile{types/TyCoRep.hs} distinguishes whether a binder is
\ctor{TyBinder} in \ghcfile{GHC.Core.TyCo.Rep} distinguishes whether a binder is
anonymous (\ctor{FunTy}) or named (\ctor{ForAllTy}). See
\verb|Note [TyBinders]| in \ghcfile{types/TyCoRep.hs}.
\verb|Note [TyBinders]| in \ghcfile{GHC.Core.TyCo.Rep}.
There are some invariants on types:
\begin{itemize}
......@@ -191,7 +193,7 @@ a term-level literal, but we are ignoring this distinction here.
\item If $[[forall n. t]]$ is a polymorphic type over a coercion variable (i.e.
$[[n]]$ is a coercion variable), then $[[n]]$ must appear in $[[t]]$;
otherwise it should be represented as a \texttt{FunTy}. See \texttt{Note
[Unused coercion variable in ForAllTy]} in \ghcfile{types/TyCoRep.hs}.
[Unused coercion variable in ForAllTy]} in \ghcfile{GHC.Core.TyCo.Rep}.
\end{itemize}
Note that the use of the $[[T </ ti // i />]]$ form and the $[[t1 -> t2]]$ form
......@@ -216,14 +218,15 @@ Invariants on coercions:
reflexive, use $[[T_R </ gi // i />]]$, never $[[<T> g1 g2]] \ldots$.
\item The $[[T]]$ in $[[T_R </gi//i/>]]$ is never a type synonym, though it could
be a type function.
\item Every non-reflexive coercion coerces between two distinct types.
\item The name in a coercion must be a term-level name (\ctor{Id}).
\item The contents of $[[<t>]]$ must not be a coercion. In other words,
the payload in a \texttt{Refl} must not be built with \texttt{CoercionTy}.
\item If $[[forall z: h .g]]$ is a polymorphic coercion over a coercion variable
(i.e. $[[z]]$ is a coercion variable), then $[[z]]$ can only appear in
\texttt{Refl} and \texttt{GRefl} in $[[g]]$. See \texttt{Note[Unused coercion
variable in ForAllCo] in \ghcfile{types/Coercion.hs}}.
\texttt{Refl} and \texttt{GRefl} in $[[g]]$. See \texttt{Note [Unused coercion
variable in ForAllCo] in \ghcfile{GHC.Core.Coercion}}.
\item Prefer $[[g1 ->_R g2]]$ over $[[(->)_R g1 g2]]$; that is, we use \ctor{FunCo},
never \ctor{TyConAppCo}, for coercions over saturated uses of $[[->]]$.
\end{itemize}
The \texttt{UnivCo} constructor takes several arguments: the two types coerced
......@@ -327,7 +330,7 @@ synonym for $[[TYPE 'Unlifted]]$.
\section{Contexts}
The functions in \ghcfile{coreSyn/CoreLint.hs} use the \texttt{LintM} monad.
The functions in \ghcfile{GHC.Core.Lint} use the \texttt{LintM} monad.
This monad contains a context with a set of bound variables $[[G]]$ and a set
of bound labels $[[D]]$. The formalism treats $[[G]]$ and $[[D]]$ as ordered
lists, but GHC uses sets as its
......@@ -432,6 +435,15 @@ a dead id and for one-tuples. These checks are omitted here.
\ottdefnlintType{}
Note the contrast between \ottdrulename{Ty\_ForAllTy\_Tv} and \ottdrulename{Ty\_ForAllTy\_Cv}.
The former checks type abstractions, which are erased at runtime. Thus, the kind of the
body must be the same as the kind of the $[[forall]]$-type (as these kinds indicate
the runtime representation). The latter checks coercion abstractions, which are \emph{not}
erased at runtime. Accordingly, the kind of a coercion abstraction is $[[*]]$. The
\ottdrulename{Ty\_ForAllTy\_Cv} rule also asserts that the bound variable $[[x]]$ is
actually used in $[[t]]$: this is to uphold a representation invariant, documented
with the grammar for types, Section~\ref{sec:types}.
\subsection{Kind validity}
\ottdefnlintKind{}
......@@ -451,6 +463,19 @@ and \ottdrulename{Co\_CoVarCoRepr}.
See Section~\ref{sec:tyconroles} for more information about $[[tyConRolesX]]$, and
see Section~\ref{sec:axiom_rules} for more information about $[[coaxrProves]]$.
The $[[downgradeRole R g]]$ function returns a new coercion that relates the same
types as $[[g]]$ but with role $[[R]]$. It assumes that the role of $[[g]]$ is a
sub-role ($\leq$) of $[[R]]$.
The $[[almostDevoid x g]]$ function makes sure that, if $[[x]]$ appears at all
in $[[g]]$, it appears only within a \ctor{Refl} or \ctor{GRefl} node. See
Section 5.8.5.2 of Richard Eisenberg's thesis for the details, or the ICFP'17
paper ``A Specification for Dependently-Typed Haskell''. (Richard's thesis
uses a technical treatment of this idea that's very close to GHC's implementation.
The ICFP'17 paper approaches the same restriction in a different way, by using
\emph{available sets} $\Delta$, as explained in Section 4.2 of that paper.
We believe both technical approaches are equivalent in what coercions they accept.)
\subsection{Name consistency}
\label{sec:name_consistency}
......@@ -463,7 +488,7 @@ There are three very similar checks for names, two performed as part of
The point of the extra checks on $[[t']]$ is that a join point's type cannot be
polymorphic in its return type; see \texttt{Note [The polymorphism rule of join
points]} in \ghcfile{coreSyn/CoreSyn.hs}.
points]} in \ghcfile{GHC.Core}.
\ottdefnlintBinder{}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment