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

[Simon Peyton Jones (@simonpj)]

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


Commits:
69767270 by Simon Peyton Jones at 2022-08-13T00:04:05+01:00
Wibble to optCoercion

- - - - -


2 changed files:

- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion/Opt.hs


Changes:

=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -34,7 +34,7 @@ module GHC.Core.Coercion (
         mkAxInstLHS, mkUnbranchedAxInstLHS,
         mkPiCo, mkPiCos, mkCoCast,
         mkSymCo, mkTransCo,
-        mkNthCo, getNthFun, nthCoRole, mkLRCo,
+        mkNthCo, getNthFun, getNthFromType, nthCoRole, mkLRCo,
         mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo, mkFunResCo,
         mkForAllCo, mkForAllCos, mkHomoForAllCos,
         mkPhantomCo,
@@ -1087,18 +1087,7 @@ mkNthCo_maybe r n co
 
     go n co
       | Just (ty, _) <- isReflCo_maybe co
-      = case splitForAllTyCoVar_maybe ty of {
-          Just (tv,_) | n == 0
-              -> -- Works for both tyvar and covar
-                 -- nth:0 pulls out a kind coercion from a hetero forall
-                 assert (r == Nominal) $
-                 Just (mkNomReflCo (varType tv)) ;
-          _ -> case splitTyConApp_maybe ty of {
-
-          Just (_, tys) | tys `lengthExceeds` n
-              -> Just (mkReflCo r (tys `getNth` n)) ;
-
-          _ -> Nothing } }
+      = Just (mkReflCo r (getNthFromType n ty))
 
     go 0 (ForAllCo _ kind_co _)
       = assert (r == Nominal)
@@ -2375,7 +2364,7 @@ coercionLKind co
     go (InstCo aco arg)         = go_app aco [go arg]
     go (KindCo co)              = typeKind (go co)
     go (SubCo co)               = go co
-    go (NthCo _ d co)           = go_nth d (go co)
+    go (NthCo _ d co)           = getNthFromType d (go co)
     go (AxiomInstCo ax ind cos) = go_ax_inst ax ind (map go cos)
     go (AxiomRuleCo ax cos)     = pFst $ expectJust "coercionKind" $
                                   coaxrProves ax $ map coercionKind cos
@@ -2398,14 +2387,10 @@ coercionLKind co
     go_app (InstCo co arg) args = go_app co (go arg:args)
     go_app co              args = piResultTys (go co) args
 
-go_nth :: HasDebugCallStack => Int -> Type -> Type
-go_nth d ty
+getNthFromType :: HasDebugCallStack => Int -> Type -> Type
+getNthFromType d ty
   | Just (_af, mult, arg, res) <- splitFunTy_maybe ty
-  = case d of
-       0 -> mult
-       1 -> arg
-       2 -> res
-       _ -> pprPanic "coercionKind1" bad_doc
+  = getNthFun d mult arg res
 
   | Just args <- tyConAppArgs_maybe ty
   = assertPpr (args `lengthExceeds` d) bad_doc $
@@ -2413,11 +2398,12 @@ go_nth d ty
 
   | d == 0
   , Just (tv,_) <- splitForAllTyCoVar_maybe ty
+     -- Works for both tyvar and covar
+     -- nth:0 pulls out a kind coercion from a hetero forall
   = tyVarKind tv
 
   | otherwise
-  = pprPanic "coercionKind2" bad_doc
-
+  = pprPanic "getNthFromType" bad_doc
   where
     bad_doc = ppr d $$ ppr ty
 
@@ -2440,7 +2426,7 @@ coercionRKind co
     go (InstCo aco arg)         = go_app aco [go arg]
     go (KindCo co)              = typeKind (go co)
     go (SubCo co)               = go co
-    go (NthCo _ d co)           = go_nth d (go co)
+    go (NthCo _ d co)           = getNthFromType d (go co)
     go (AxiomInstCo ax ind cos) = go_ax_inst ax ind (map go cos)
     go (AxiomRuleCo ax cos)     = pSnd $ expectJust "coercionKind" $
                                   coaxrProves ax $ map coercionKind cos


=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -23,6 +23,7 @@ import GHC.Core.Unify
 
 import GHC.Types.Var.Set
 import GHC.Types.Var.Env
+import GHC.Types.Unique.Set
 
 import GHC.Data.Pair
 import GHC.Data.List.SetOps ( getNth )
@@ -145,12 +146,14 @@ optCoercion' env co
                           , text "out_ty2:" <+> ppr out_ty2
                           , text "in_role:" <+> ppr in_role
                           , text "out_role:" <+> ppr out_role
+                          , vcat $ map ppr_one $ nonDetEltsUniqSet $ coVarsOfCo co
                           , text "subst:" <+> ppr env ]))
-              out_co
+               out_co
 
   | otherwise         = opt_co1 lc False co
   where
     lc = mkSubstLiftingContext env
+    ppr_one cv = ppr cv <+> dcolon <+> ppr (coVarKind cv)
 
 
 type NormalCo    = Coercion
@@ -338,20 +341,7 @@ opt_co4 env sym rep r (TransCo co1 co2)
 opt_co4 env _sym rep r (NthCo _r n co)
   | Just (ty, _) <- isReflCo_maybe co
   = assert (r == _r ) $
-    let arg_ty | n == 0
-               , Just (tv, _) <- splitForAllTyCoVar_maybe ty
-               = varType tv -- works for both tyvar and covar
-
-               | Just (_af, mult, arg, res) <- splitFunTy_maybe ty
-               = getNthFun n mult arg res
-
-               | Just (_tc, args) <- splitTyConApp_maybe ty
-               = args `getNth` n
-
-               | otherwise
-               = pprPanic "opt_co4" (ppr n $$ ppr ty)
-
-    in liftCoSubst (chooseRole rep r) env arg_ty
+    liftCoSubst (chooseRole rep r) env (getNthFromType n ty)
 
 opt_co4 env sym rep r (NthCo r1 n (TyConAppCo _ _ cos))
   = assert (r == r1 )



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/697672709d5be6ace8e1d44c689acbf5f9b059ae

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/697672709d5be6ace8e1d44c689acbf5f9b059ae
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/20220812/7b3dda4f/attachment-0001.html>