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

[Simon Peyton Jones (@simonpj)]

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


Commits:
0d88a768 by Simon Peyton Jones at 2023-06-15T11:44:51+01:00
Wibble

- - - - -


3 changed files:

- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion.hs-boot
- compiler/GHC/Tc/Solver/Equality.hs


Changes:

=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -41,7 +41,7 @@ module GHC.Core.Coercion (
         mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo,
         mkFunCo, mkFunCo2, mkFunCoNoFTF, mkFunResCo,
         mkNakedFunCo,
-        mkForAllCo, mkHomoForAllCos,
+        mkNakedForAllCo, mkForAllCo, mkHomoForAllCos,
         mkPhantomCo,
         mkHoleCo, mkUnivCo, mkSubCo,
         mkAxiomInstCo, mkProofIrrelCo,
@@ -969,11 +969,21 @@ 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 :: TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> CoercionN -> Coercion -> Coercion
+mkForAllCo :: HasDebugCallStack => TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> CoercionN -> Coercion -> Coercion
 mkForAllCo v visL visR kind_co co
-  | assert (varType v `eqType` (coercionLKind kind_co)) True
-  , assert (isTyVar v || almostDevoidCoVarOfCo v co) True
-  , Just (ty, r) <- isReflCo_maybe 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) $
+    mkNakedForAllCo v visL visR kind_co co
+
+mkNakedForAllCo :: TyCoVar -> 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
   , isGReflCo kind_co
   , visL `eqForAllVis` visR
   = mkReflCo r (mkTyCoForAllTy v visL ty)


=====================================
compiler/GHC/Core/Coercion.hs-boot
=====================================
@@ -16,7 +16,7 @@ import GHC.Utils.Misc
 mkReflCo :: Role -> Type -> Coercion
 mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
 mkAppCo :: Coercion -> Coercion -> Coercion
-mkForAllCo :: TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
+mkForAllCo :: HasDebugCallStack => TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
 mkFunCo      :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
 mkNakedFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
 mkFunCo2     :: Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion


=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -517,7 +517,7 @@ can_eq_nc_forall ev eq_rel s1 s2
                          -- skol_tv is already in the in-scope set, but the
                          -- free vars of kind_co are not; hence "...AndInScope"
                    ; co <- go uenv skol_tvs subst' bndrs1 bndrs2
-                   ; return (mkForAllCo skol_tv vis1 vis2 kind_co co)}
+                   ; return (mkNakedForAllCo skol_tv vis1 vis2 kind_co co)}
 
             -- Done: unify phi1 ~ phi2
             go uenv [] subst bndrs1 bndrs2



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0d88a768e89c6d89e2312ade3d348e8881325be2

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0d88a768e89c6d89e2312ade3d348e8881325be2
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/20230615/fe14a544/attachment-0001.html>