[Git][ghc/ghc][wip/forall-vis-coercions] Wibbles

[Simon Peyton Jones (@simonpj)]

Simon Peyton Jones pushed to branch wip/forall-vis-coercions at Glasgow Haskell Compiler / GHC


Commits:
275cafcb by Simon Peyton Jones at 2023-07-11T08:32:51+01:00
Wibbles

- - - - -


3 changed files:

- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/TyCo/Rep.hs
- docs/core-spec/core-spec.mng


Changes:

=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -2255,9 +2255,13 @@ lintCoercion co@(ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR
        ; lintForAllBody tcv' rty
 
        ; when (isCoVar tcv) $
-         lintL (almostDevoidCoVarOfCo tcv body_co) $
-         text "Covar can only appear in Refl and GRefl: " <+> ppr co
-         -- See (FC6) in Note [ForAllCo] in GHC.Core.TyCo.Rep
+         do { lintL (visL == coreTyLamForAllTyFlag && visR == coreTyLamForAllTyFlag) $
+              text "Invalid visibility flags in CoVar ForAllCo" <+> ppr co
+              -- See (FC7) in Note [ForAllCo] in GHC.Core.TyCo.Rep
+            ; lintL (almostDevoidCoVarOfCo tcv body_co) $
+              text "Covar can only appear in Refl and GRefl: " <+> ppr co
+              -- See (FC6) in Note [ForAllCo] in GHC.Core.TyCo.Rep
+         }
 
        ; when (body_role == Nominal) $
          lintL (visL `eqForAllVis` visR) $


=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -878,7 +878,7 @@ data Coercion
       { fco_tcv  :: TyCoVar
       , fco_visL :: !ForAllTyFlag -- Vvisibility of coercionLKind
       , fco_visR :: !ForAllTyFlag -- Visibility of coercionRKind
-                                  -- See (FC7) of Note [ForallCo]
+                                  -- See (FC7) of Note [ForAllCo]
       , fco_kind :: KindCoercion
       , fco_body :: Coercion }
          -- ForAllCo :: _ -> N -> e -> e
@@ -1260,10 +1260,10 @@ Several things to note here
     * Even if cv occurs in body_co, it is possible that cv does not occur in the kind
       of body_co. Therefore the check in coercionKind is inevitable.
 
-(FC6) Consider (ForAllCo cv kind_co body_co) where `cv` is a coercion variable.
-  We insist that `cv` appears only in positions that are erased. In fact we use
+(FC6) Invariant: in a ForAllCo where fco_tcv is a coercion variable, `cv`,
+  we insist that `cv` appears only in positions that are erased. In fact we use
   a conservative approximation of this: we require that
-       (almostDevoidCoVarOfCo cv body_co)
+       (almostDevoidCoVarOfCo cv fco_body)
   holds.  This function checks that `cv` appers only within the type in a Refl
   node and under a GRefl node (including in the Coercion stored in a GRefl).
   It's possible other places are OK, too, but this is a safe approximation.
@@ -1282,7 +1282,7 @@ Several things to note here
   proved that the problem does not occur with homogeneous equality, so this
   check can be dropped once ~# is made to be homogeneous.
 
-(FC7) In a ForAllCo, if fco_tcv is a CoVar, then
+(FC7) Invariant: in a ForAllCo, if fco_tcv is a CoVar, then
          fco_visL = fco_visR = coreTyLamForAllTyFlag
   c.f. (FT2) in Note [ForAllTy]
 


=====================================
docs/core-spec/core-spec.mng
=====================================
@@ -223,8 +223,8 @@ be a type function.
 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{GHC.Core.Coercion}}.
+  \texttt{Refl} and \texttt{GRefl} in $[[g]]$. See \texttt{(FC6) in Note [ForAllCo]
+  in \ghcfile{GHC.Core.TyCon.Rep}}.
 \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}



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/275cafcb4f0045dde91c5ca1d0d564baf426afc4

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/275cafcb4f0045dde91c5ca1d0d564baf426afc4
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/20230711/11171557/attachment-0001.html>