[Git][ghc/ghc][wip/T23109] Allow SelCo for newtype classes

[Simon Peyton Jones (@simonpj)]

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


Commits:
5121fc57 by Simon Peyton Jones at 2023-06-10T15:56:50+02:00
Allow SelCo for newtype classes

Experimental change

- - - - -


2 changed files:

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


Changes:

=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -1307,7 +1307,7 @@ mkSubCo co = assertPpr (coercionRole co == Nominal) (ppr co <+> ppr (coercionRol
 
 isSubCo_maybe :: Coercion -> Maybe Coercion
 isSubCo_maybe (SubCo co) = Just co
-isSubCo_maybe co         = Nothing
+isSubCo_maybe _          = Nothing
 
 -- | Changes a role, but only a downgrade. See Note [Role twiddling functions]
 downgradeRole_maybe :: Role   -- ^ desired role


=====================================
compiler/GHC/Core/TyCon.hs
=====================================
@@ -67,7 +67,7 @@ module GHC.Core.TyCon(
         isOpenTypeFamilyTyCon, isClosedSynFamilyTyConWithAxiom_maybe,
         tyConInjectivityInfo,
         isBuiltInSynFamTyCon_maybe,
-        isGadtSyntaxTyCon, isInjectiveTyCon, isGenerativeTyCon, isGenInjAlgRhs,
+        isGadtSyntaxTyCon, isInjectiveTyCon, isGenerativeTyCon,
         isTyConAssoc, tyConAssoc_maybe, tyConFlavourAssoc_maybe,
         isImplicitTyCon,
         isTyConWithSrcDataCons,
@@ -1982,23 +1982,39 @@ isTypeDataTyCon (TyCon { tyConDetails = details })
 -- See also Note [Decomposing TyConApp equalities] in "GHC.Tc.Solver.Canonical"
 isInjectiveTyCon :: TyCon -> Role -> Bool
 isInjectiveTyCon (TyCon { tyConDetails = details }) role
-  = go details role
+  = go details
   where
-    go _                             Phantom          = True -- Vacuously; (t1 ~P t2) holds for all t1, t2!
-    go (AlgTyCon {})                 Nominal          = True
-    go (AlgTyCon {algTcRhs = rhs})   Representational = isGenInjAlgRhs rhs
-    go (SynonymTyCon {})             _                = False
-    go (FamilyTyCon { famTcFlav = DataFamilyTyCon _ })
-                                                  Nominal = True
-    go (FamilyTyCon { famTcInj = Injective inj }) Nominal = and inj
-    go (FamilyTyCon {})              _                = False
-    go (PrimTyCon {})                _                = True
-    go (PromotedDataCon {})          _                = True
-    go (TcTyCon {})                  _                = True
+    go _ | Phantom <- role = True -- Vacuously; (t1 ~P t2) holds for all t1, t2!
+
+    go (AlgTyCon {algTcRhs = rhs, algTcFlavour = flav})
+       | Nominal <- role                                = True
+       | Representational <- role                       = go_alg_rep rhs flav
 
-  -- Reply True for TcTyCon to minimise knock on type errors
-  -- See Note [How TcTyCons work] item (1) in GHC.Tc.TyCl
+    go (FamilyTyCon { famTcFlav = DataFamilyTyCon _ })
+       | Nominal <- role                                = True
+    go (FamilyTyCon { famTcInj = Injective inj })
+       | Nominal <- role                                = and inj
+    go (FamilyTyCon {})                                 = False
 
+    go (SynonymTyCon {})    = False
+    go (PrimTyCon {})       = True
+    go (PromotedDataCon {}) = True
+    go (TcTyCon {})         = True
+       -- Reply True for TcTyCon to minimise knock on type errors
+       -- See Note [How TcTyCons work] item (1) in GHC.Tc.TyCl
+
+    -- go_alg_rep used only at Representational role
+    go_alg_rep (TupleTyCon {})    _               = True
+    go_alg_rep (SumTyCon {})      _               = True
+    go_alg_rep (DataTyCon {})     _               = True
+    go_alg_rep (AbstractTyCon {}) _               = False
+    go_alg_rep (NewTyCon {})      (ClassTyCon {}) = True -- See Note [Newtype classes]
+    go_alg_rep (NewTyCon {})      _               = False
+
+{- Note [Newtype classes]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+ToDo: write this up
+-}
 
 -- | 'isGenerativeTyCon' is true of 'TyCon's for which this property holds
 -- (where r is the role passed in):
@@ -2018,14 +2034,6 @@ isGenerativeTyCon tc@(TyCon { tyConDetails = details }) role
     -- In all other cases, injectivity implies generativity
     go r _ = isInjectiveTyCon tc r
 
--- | Is this an 'AlgTyConRhs' of a 'TyCon' that is generative and injective
--- with respect to representational equality?
-isGenInjAlgRhs :: AlgTyConRhs -> Bool
-isGenInjAlgRhs (TupleTyCon {})          = True
-isGenInjAlgRhs (SumTyCon {})            = True
-isGenInjAlgRhs (DataTyCon {})           = True
-isGenInjAlgRhs (AbstractTyCon {})       = False
-isGenInjAlgRhs (NewTyCon {})            = False
 
 -- | Is this 'TyCon' that for a @newtype@
 isNewTyCon :: TyCon -> Bool



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5121fc57b1e074e37f6752b4fc8a2e2962cd9bce

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5121fc57b1e074e37f6752b4fc8a2e2962cd9bce
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/20230610/f384b5d9/attachment-0001.html>