From 4f2c8810cab3b2a76bb5e85d6c4c956aa91c3ac8 Mon Sep 17 00:00:00 2001 From: Richard Eisenberg Date: Tue, 17 Mar 2020 15:13:38 +0000 Subject: 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 03d4852658e1b7407abb4da84b1b03bfa6f6db3b) in the source. No changes to running code. --- .gitlab/linters/check-cpp.py | 2 ++ compiler/GHC/Core/Coercion.hs | 4 +-- compiler/GHC/Core/Lint.hs | 7 ++--- compiler/GHC/Core/TyCo/Rep.hs | 63 ++++++++++++++++++++++++++++++++++++++---- compiler/GHC/Core/Type.hs | 1 + compiler/GHC/Core/Unify.hs | 2 +- docs/core-spec/.gitignore | 1 + docs/core-spec/CoreLint.ott | 35 +++++++++++++++++------ docs/core-spec/CoreSyn.ott | 5 ++++ docs/core-spec/core-spec.mng | 47 +++++++++++++++++++++++-------- docs/core-spec/core-spec.pdf | Bin 366905 -> 374165 bytes 11 files changed, 135 insertions(+), 32 deletions(-) diff --git a/.gitlab/linters/check-cpp.py b/.gitlab/linters/check-cpp.py index 5377fcb005..1b4b26a760 100755 --- a/.gitlab/linters/check-cpp.py +++ b/.gitlab/linters/check-cpp.py @@ -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) diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs index 3e59a6ef85..73178af87f 100644 --- a/compiler/GHC/Core/Coercion.hs +++ b/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 ) diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs index b22705eb6f..287dc54598 100644 --- a/compiler/GHC/Core/Lint.hs +++ b/compiler/GHC/Core/Lint.hs @@ -1466,7 +1466,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) @@ -1825,7 +1824,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 +1843,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 +2017,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) } diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs index 26c01ebcb8..376a62d360 100644 --- a/compiler/GHC/Core/TyCo/Rep.hs +++ b/compiler/GHC/Core/TyCo/Rep.hs @@ -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 diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs index 3af971c101..3e86e86cf4 100644 --- a/compiler/GHC/Core/Type.hs +++ b/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! diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs index fa188fc022..3b8fd46220 100644 --- a/compiler/GHC/Core/Unify.hs +++ b/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' diff --git a/docs/core-spec/.gitignore b/docs/core-spec/.gitignore index dac3bd2547..d5181cb718 100644 --- a/docs/core-spec/.gitignore +++ b/docs/core-spec/.gitignore @@ -4,3 +4,4 @@ CoreOtt.tex core-spec.tex *.fls +*.out diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott index 606e45c190..3004802ad4 100644 --- a/docs/core-spec/CoreLint.ott +++ b/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 /= (->) = take(length , 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 : tyConKind T ~> k G |-ty T : 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 diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott index cb9f1fc275..9ce8b5e16d 100644 --- a/docs/core-spec/CoreSyn.ott +++ b/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 :: :: 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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng index 167ca85644..ea488921be 100644 --- a/docs/core-spec/core-spec.mng +++ b/docs/core-spec/core-spec.mng @@ -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 ]]$ form and the $[[t1 -> t2]]$ form @@ -216,14 +218,15 @@ Invariants on coercions: reflexive, use $[[T_R ]]$, never $[[ g1 g2]] \ldots$. \item The $[[T]]$ in $[[T_R ]]$ 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 $[[]]$ 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{} diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf index ad2d57196c..75bb620edc 100644 Binary files a/docs/core-spec/core-spec.pdf and b/docs/core-spec/core-spec.pdf differ -- cgit v1.2.1