[Git][ghc/ghc][wip/T21623] Add isCovertGadtDataCon, fixing build

[Simon Peyton Jones (@simonpj)]

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


Commits:
292f4f89 by Simon Peyton Jones at 2022-10-14T23:29:02+01:00
Add isCovertGadtDataCon, fixing build

- - - - -


2 changed files:

- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Tc/Errors/Ppr.hs


Changes:

=====================================
compiler/GHC/Core/DataCon.hs
=====================================
@@ -55,7 +55,7 @@ module GHC.Core.DataCon (
         -- ** Predicates on DataCons
         isNullarySrcDataCon, isNullaryRepDataCon,
         isTupleDataCon, isBoxedTupleDataCon, isUnboxedTupleDataCon,
-        isUnboxedSumDataCon,
+        isUnboxedSumDataCon, isCovertGadtDataCon,
         isVanillaDataCon, isNewDataCon, isTypeDataCon,
         classDataCon, dataConCannotMatch,
         dataConUserTyVarsNeedWrapper, checkDataConTyVars,
@@ -422,7 +422,7 @@ data DataCon
                 --       syntax, provided its type looks like the above.
                 --       The declaration format is held in the TyCon (algTcGadtSyntax)
 
-        -- Universally-quantified type vars [a,b,c]
+        -- dcUnivTyVars: Universally-quantified type vars [a,b,c]
         -- INVARIANT: length matches arity of the dcRepTyCon
         -- INVARIANT: result type of data con worker is exactly (T a b c)
         -- COROLLARY: The dcUnivTyVars are always in one-to-one correspondence with
@@ -875,8 +875,7 @@ data StrictnessMark = MarkedStrict | NotMarkedStrict
 
 -- | An 'EqSpec' is a tyvar/type pair representing an equality made in
 -- rejigging a GADT constructor
-data EqSpec = EqSpec TyVar
-                     Type
+data EqSpec = EqSpec TyVar Type
 
 -- | Make a non-dependent 'EqSpec'
 mkEqSpec :: TyVar -> Type -> EqSpec
@@ -1711,6 +1710,53 @@ isNewDataCon dc = isNewTyCon (dataConTyCon dc)
 isTypeDataCon :: DataCon -> Bool
 isTypeDataCon dc = isTcClsNameSpace (nameNameSpace (getName dc))
 
+isCovertGadtDataCon :: DataCon -> Bool
+-- See Note [isCovertGadtDataCon]
+isCovertGadtDataCon (MkData { dcUnivTyVars  = univ_tvs
+                             , dcEqSpec     = eq_spec
+                             , dcRepTyCon   = rep_tc })
+  =  not (null eq_spec)                -- There are some constraints
+  && not (any is_visible_spec eq_spec) -- But none of them are visible
+  where
+    visible_univ_tvs :: [TyVar]  -- Visible arguments in result type
+    visible_univ_tvs
+      = [ univ_tv | (univ_tv, tcb) <- univ_tvs `zip` tyConBinders rep_tc
+                  , isVisibleTyConBinder tcb ]
+
+    is_visible_spec :: EqSpec -> Bool
+    is_visible_spec (EqSpec univ_tv _) = univ_tv `elem` visible_univ_tvs
+
+{- Note [isCovertGadtDataCon]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(isCovertGadtDataCon K) returns True if K is a GADT data constructor, but
+does not /look/ like it. Consider (#21447)
+    type T :: TYPE r -> Type
+    data T a where { MkT :: b -> T b }
+Here MkT doesn't look GADT-like, but it is. If we make the kind applications
+explicit we'd see:
+    data T a where { MkT :: b -> T @LiftedRep b }
+
+The test for covert-ness is bit tricky, because we want to see if
+  - dcEqSpec is non-empty
+  - none of the universal type variables that it constrains is
+    a required argument of the TyCon
+
+In the example above, the DataCon for MkT will have
+    dcUnivTyVars: [(r::RuntimeRep), (b :: TYPE r)]
+    dcEqSpec:     [ (r, LiftedRep) ]
+So `r` is constrained by dcEqSpec, but `b` is not, so the user-visible
+declaration   MkT :: b -> T b
+looks entirely non-GADT-ish.
+
+But remember:
+* The visibility or otherwise is a property of the /TyCon/ binders
+* The dcUnivTyVars may or may not be the same as the TyCon binders
+* So we have to zip them together.
+* For a data family the TyCon in question is the /representation/ TyCon
+  hence dcRepTyCon
+-}
+
+
 -- | Should this DataCon be allowed in a type even without -XDataKinds?
 -- Currently, only Lifted & Unlifted
 specialPromotedDc :: DataCon -> Bool


=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -1018,7 +1018,8 @@ instance Diagnostic TcRnMessage where
                 ppr con <+> dcolon <+> ppr (dataConDisplayType True con))
               IsGADT ->
                 (text "A newtype must not be a GADT",
-                ppr con <+> dcolon <+> pprWithExplicitKindsWhen sneaky_eq_spec (ppr $ dataConDisplayType show_linear_types con))
+                ppr con <+> dcolon <+> pprWithExplicitKindsWhen sneaky_eq_spec
+                                       (ppr $ dataConDisplayType show_linear_types con))
               HasConstructorContext ->
                 (text "A newtype constructor must not have a context in its type",
                 ppr con <+> dcolon <+> ppr (dataConDisplayType show_linear_types con))
@@ -1028,12 +1029,9 @@ instance Diagnostic TcRnMessage where
               HasStrictnessAnnotation ->
                 (text "A newtype constructor must not have a strictness annotation", empty)
 
-          -- Is there an EqSpec involving an invisible binder? If so, print the
-          -- error message with explicit kinds.
-          invisible_binders = filter isInvisibleTyConBinder (tyConBinders $ dataConTyCon con)
-          sneaky_eq_spec
-            = any (\eq -> any (( == eqSpecTyVar eq) . binderVar) invisible_binders)
-                $ dataConEqSpec con
+          -- Is the data con a "covert" GADT?  See Note [isCovertGadtDataCon]
+          -- in GHC.Core.DataCon
+          sneaky_eq_spec = isCovertGadtDataCon con
 
   diagnosticReason = \case
     TcRnUnknownMessage m



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/292f4f89f310cb1ff6723e0b7952c7f069abee41

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/292f4f89f310cb1ff6723e0b7952c7f069abee41
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/20221014/3ccb3beb/attachment-0001.html>