[Git][ghc/ghc][wip/forall-vis-coercions] Wibbles... in progress...may not compile

[Simon Peyton Jones (@simonpj)]

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


Commits:
04e69d62 by Simon Peyton Jones at 2023-07-10T17:50:00+01:00
Wibbles... in progress...may not compile

- - - - -


4 changed files:

- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Utils.hs
- compiler/GHC/Types/Var.hs


Changes:

=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -964,39 +964,48 @@ once ~# is made to be homogeneous.
 
 -- | Make a Coercion from a tycovar, a kind coercion, and a body coercion.
 -- The kind of the tycovar should be the left-hand kind of the kind coercion.
--- See Note [Unused coercion variable in ForAllCo]
 mkForAllCo :: HasDebugCallStack => TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> CoercionN -> Coercion -> Coercion
+-- See Note [Unused coercion variable in ForAllCo]
 mkForAllCo v visL visR kind_co co
   = assertPpr (varType v `eqType` (coercionLKind kind_co))
       (vcat [ ppr v <+> dcolon <+> ppr (varType v)
             , text "kind_co:" <+>  ppr kind_co
             , text "lkind:" <+> ppr (coercionLKind kind_co) ]) $
-    assert (isTyVar v || almostDevoidCoVarOfCo v co) $
+    assertPpr (isTyVar v || (almostDevoidCoVarOfCo v co &&
+                             (v `elemVarSet` tyCoVarsOfCo co))) (ppr v $$ ppr co) $
     mkNakedForAllCo v visL visR kind_co co
 
-mkNakedForAllCo :: TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> CoercionN -> Coercion -> Coercion
+mkNakedForAllCo :: TyVar -> ForAllTyFlag -> ForAllTyFlag -> CoercionN -> Coercion -> Coercion
 -- This version lacks the assertion checks.
 -- Used during type checking when the arguments may (legitimately) not be zonked
 -- and so the assertions might (bogusly) fail
-mkNakedForAllCo v visL visR kind_co co
-  | Just (ty, r) <- isReflCo_maybe co
+-- NB: since the coercions are un-zonked, we can't really deal with
+--     Note [Unused coercion variable in ForAllCo].  Fortunately we don't have to:
+--     this function is needed only for /type/ variables.
+mkNakedForAllCo tv visL visR kind_co co
+  | assertPpr (isTyVar tv) (ppr tv) True
+  , Just (ty, r) <- isReflCo_maybe co
   , isGReflCo kind_co
   , visL `eqForAllVis` visR
-  = mkReflCo r (mkTyCoForAllTy v visL ty)
+  = mkReflCo r (mkForAllTy (Bndr tv visL) ty)
   | otherwise
-  = ForAllCo { fco_tcv = v, fco_visL = visL, fco_visR = visR
+  = ForAllCo { fco_tcv = tv, fco_visL = visL, fco_visR = visR
              , fco_kind = kind_co, fco_body = co }
 
--- | Like 'mkForAllCo', but the inner coercion shouldn't be an obvious
--- reflexive coercion. For example, it is guaranteed in 'mkForAllCos'.
+-- | Like 'mkForAllCo', but there is no need to check that the inner coercion isn't Refl;
+--   the caller has done that. (For example, it is guaranteed in 'mkHomoForAllCos'.)
 -- The kind of the tycovar should be the left-hand kind of the kind coercion.
 mkForAllCo_NoRefl :: TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> CoercionN -> Coercion -> Coercion
 mkForAllCo_NoRefl v visL visR kind_co co
   | assert (varType v `eqType` (coercionLKind kind_co)) True
   , assert (not (isReflCo co)) True
   , isCoVar v
+  , assertPpr (visL == coreTyLamForAllTyFlag && visR == coreTyLamForAllTyFlag)
+              (ppr v <+> ppr visL <+> ppr visR) True
   , assert (almostDevoidCoVarOfCo v co) True
   , not (v `elemVarSet` tyCoVarsOfCo co)
+    -- We must test this to decide whether to build a FunCo or a ForAllCo
+    -- See Note [Unused coercion variable in ForAllCo]
   = mkFunCoNoFTF (coercionRole co) (multToCo ManyTy) kind_co co
       -- Functions from coercions are always unrestricted
   | otherwise


=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -1769,9 +1769,10 @@ mkTyCoForAllTy :: TyCoVar -> ForAllTyFlag -> Type -> Type
 mkTyCoForAllTy tv vis ty
   | isCoVar tv
   , not (tv `elemVarSet` tyCoVarsOfType ty)
+    -- See Note [Unused coercion variable in ForAllCo] in GHC.Core.TyCo.Rep
   = mkVisFunTyMany (varType tv) ty
   | otherwise
-  = ForAllTy (Bndr tv vis) ty
+  = ForAllTy (mkForAllTyBinder tv vis) ty
 
 -- | Make a dependent forall over a TyCoVar
 mkTyCoForAllTys :: [ForAllTyBinder] -> Type -> Type


=====================================
compiler/GHC/Core/Utils.hs
=====================================
@@ -174,7 +174,8 @@ mkLamType v body_ty
 
    | isCoVar v
    , v `elemVarSet` tyCoVarsOfType body_ty
-   = mkForAllTy (Bndr v Required) body_ty
+     -- See Note [Unused coercion variable in ForAllTy] in GHC.Core.TyCo.Rep
+   = mkForAllTy (Bndr v coreTyLamForAllTyFlag) body_ty
 
    | otherwise
    = mkFunctionType (varMult v) (varType v) body_ty


=====================================
compiler/GHC/Types/Var.hs
=====================================
@@ -752,7 +752,8 @@ isTyVarBinder (Bndr tcv _) = isTyVar tcv
 
 -- | Make a named binder
 mkForAllTyBinder :: vis -> TyCoVar -> VarBndr TyCoVar vis
-mkForAllTyBinder vis var = Bndr var vis
+mkForAllTyBinder vis var = assertPpr (isTyVar var || vis == coreTyLamForAllTyFlag)
+                           Bndr var vis
 
 -- | Make a named binder
 -- 'var' should be a type variable



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/04e69d6255545ea93bb576957c0f80de3a8f68a9

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/04e69d6255545ea93bb576957c0f80de3a8f68a9
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/20230710/cc6ca61c/attachment-0001.html>