[Git][ghc/ghc][wip/update-core-spec] Update core spec to reflect changes to Core.
Richard Eisenberg
gitlab at gitlab.haskell.org
Thu Mar 19 12:04:55 UTC 2020
Richard Eisenberg pushed to branch wip/update-core-spec at Glasgow Haskell Compiler / GHC
Commits:
dd0ab863 by Richard Eisenberg at 2020-03-19T12:04:37Z
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.
* Improves commentary (including restoring a Note lost in
03d4852658e1b7407abb4da84b1b03bfa6f6db3b) in the source.
No changes to running code.
- - - - -
9 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Unify.hs
- docs/core-spec/CoreLint.ott
- docs/core-spec/CoreSyn.ott
- docs/core-spec/core-spec.mng
- docs/core-spec/core-spec.pdf
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -1367,7 +1367,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 )
@@ -1416,7 +1416,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 )
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -1825,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
@@ -1844,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
@@ -2018,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) }
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -578,7 +578,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 +607,23 @@ 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 : kind
+------------------------------------
+ForAllTy (Bndr tyvar vis) inner : kind
+
+inner : TYPE r
+------------------------------------
+ForAllTy (Bndr covar vis) inner : TYPE
+
+Note that when inside the binder is a tyvar, neither the inner type nor for
+ForAllTy itself have to have kind *! But, it means that we should push any kind
+casts through the ForAllTy. The only trouble is avoiding capture.
+See GHC.Core.Type.mkCastTy.
+
-}
-- | A type labeled 'KnotTied' might have knot-tied tycons in it. See
@@ -1003,6 +1020,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
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -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!
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -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'
=====================================
docs/core-spec/CoreLint.ott
=====================================
@@ -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
+------------------------------------------------------------------ :: ForAllCoTv
+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 *~R * t2
+R2 = coercionRole x_k1
+h' = downgradeRole R2 h
+h1 = nth R2 2 h'
+h2 = nth R2 3 h'
+almostDevoid x g
+------------------------------------------- :: ForAllCoCv
+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
=====================================
docs/core-spec/CoreSyn.ott
=====================================
@@ -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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
=====================================
docs/core-spec/core-spec.mng
=====================================
@@ -106,10 +106,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 +119,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]]$.
@@ -170,9 +170,9 @@ A program is just a list of bindings:
\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 +191,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 +216,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 +328,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
@@ -451,6 +452,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 +477,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{}
=====================================
docs/core-spec/core-spec.pdf
=====================================
Binary files a/docs/core-spec/core-spec.pdf and b/docs/core-spec/core-spec.pdf differ
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/dd0ab8635f191408aab4acdf140696606c895fa0
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/commit/dd0ab8635f191408aab4acdf140696606c895fa0
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200319/a5c44d7f/attachment-0001.html>
More information about the ghc-commits
mailing list