[Git][ghc/ghc][wip/T21623] Wibble

[Simon Peyton Jones (@simonpj)]

Simon Peyton Jones pushed to branch wip/T21623 at Glasgow Haskell Compiler / GHC


Commits:
081540f8 by Simon Peyton Jones at 2022-08-09T22:27:40+01:00
Wibble

- - - - -


1 changed file:

- compiler/GHC/Core/Coercion.hs


Changes:

=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -1450,20 +1450,18 @@ promoteCoercion :: Coercion -> CoercionN
 -- First cases handles anything that should yield refl.
 promoteCoercion co = case co of
 
-    _ | ki1 `eqType` ki2
-      -> mkNomReflCo (typeKind ty1)
-     -- no later branch should return refl
-     --    The assert (False )s throughout
-     -- are these cases explicitly, but they should never fire.
+    Refl _ -> mkNomReflCo ki1
 
-    Refl _ -> assert False $
-              mkNomReflCo ki1
-
-    GRefl _ _ MRefl -> assert False $
-                       mkNomReflCo ki1
+    GRefl _ _ MRefl -> mkNomReflCo ki1
 
     GRefl _ _ (MCo co) -> co
 
+    _ | ki1 `eqType` ki2
+      -> mkNomReflCo (typeKind ty1)
+     -- No later branch should return refl
+     -- The assert (False )s throughout
+     -- are these cases explicitly, but they should never fire.
+
     TyConAppCo _ tc args
       | Just co' <- instCoercions (mkNomReflCo (tyConKind tc)) args
       -> co'
@@ -1481,13 +1479,19 @@ promoteCoercion co = case co of
       | isTyVar tv
       -> promoteCoercion g
 
-    ForAllCo _ _ _
+    ForAllCo {}
       -> assert False $
+            -- (ForAllCo {} :: (forall cv.t1) ~ (forall cv.t2)
+            -- The tyvar case is handled above, so the bound var is a
+            -- a coercion variable. So both sides have kind Type
+            -- (Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep).
+            -- So the result is Refl, and that should have been caught by
+            -- the first equation above
          mkNomReflCo liftedTypeKind
-      -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
 
-    FunCo {} -> assert False $
-                mkNomReflCo liftedTypeKind
+    FunCo {} -> mkKindCo co
+       -- We can get Type~Constraint or Constraint~Type
+       -- from FunCo {} :: (a -> (b::Type)) ~ (a -=> (b'::Constraint))
 
     CoVarCo {}     -> mkKindCo co
     HoleCo {}      -> mkKindCo co
@@ -1531,7 +1535,7 @@ promoteCoercion co = case co of
            -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
 
     KindCo _
-      -> assert False $
+      -> assert False $ -- See the first equation above
          mkNomReflCo liftedTypeKind
 
     SubCo g
@@ -1541,6 +1545,9 @@ promoteCoercion co = case co of
     Pair ty1 ty2 = coercionKind co
     ki1 = typeKind ty1
     ki2 = typeKind ty2
+    doc = vcat[ ppr co
+              , text "ty1" <+> ppr ty1 <+> dcolon <+> ppr ki1
+              , text "ty2" <+> ppr ty2 <+> dcolon <+> ppr ki2 ]
 
 -- | say @g = promoteCoercion h at . Then, @instCoercion g w@ yields @Just g'@,
 -- where @g' = promoteCoercion (h w)@.



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/081540f8954ba95e61acda35227f5e7de89bbaf4

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/081540f8954ba95e61acda35227f5e7de89bbaf4
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/20220809/e5853f83/attachment-0001.html>