[Git][ghc/ghc][wip/T21623] Deal with rejigConRes

Simon Peyton Jones (@simonpj) gitlab at gitlab.haskell.org
Mon Sep 5 16:17:49 UTC 2022



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


Commits:
7183bcc0 by Simon Peyton Jones at 2022-09-05T17:18:53+01:00
Deal with rejigConRes

Needs a Note to be written by Richard

- - - - -


7 changed files:

- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/Opt/CallArity.hs
- compiler/GHC/Data/Graph/UnVar.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Types/Id/Make.hs
- compiler/GHC/Types/Var/Env.hs
- testsuite/tests/typecheck/should_fail/T12102.hs


Changes:

=====================================
compiler/GHC/Core/DataCon.hs
=====================================
@@ -20,7 +20,7 @@ module GHC.Core.DataCon (
         -- ** Equality specs
         EqSpec, mkEqSpec, eqSpecTyVar, eqSpecType,
         eqSpecPair, eqSpecPreds,
-        substEqSpec, filterEqSpec,
+        substEqSpec,
 
         -- ** Field labels
         FieldLabel(..), FieldLabelString,
@@ -58,7 +58,7 @@ module GHC.Core.DataCon (
         isTupleDataCon, isBoxedTupleDataCon, isUnboxedTupleDataCon,
         isUnboxedSumDataCon,
         isVanillaDataCon, isNewDataCon, classDataCon, dataConCannotMatch,
-        dataConUserTyVarsArePermuted,
+        dataConUserTyVarsArePermuted, checkDataConTyVars,
         isBanged, isMarkedStrict, cbvFromStrictMark, eqHsBang, isSrcStrict, isSrcUnpacked,
         specialPromotedDc,
 
@@ -94,7 +94,7 @@ import GHC.Utils.Binary
 import GHC.Types.Unique.FM ( UniqFM )
 import GHC.Types.Unique.Set
 import GHC.Builtin.Uniques( mkAlphaTyVarUnique )
-
+import GHC.Data.Graph.UnVar  -- UnVarSet and operations
 
 import GHC.Utils.Outputable
 import GHC.Utils.Misc
@@ -796,13 +796,6 @@ substEqSpec subst (EqSpec tv ty)
   where
     tv' = getTyVar (substTyVar subst tv)
 
--- | Filter out any 'TyVar's mentioned in an 'EqSpec'.
-filterEqSpec :: [EqSpec] -> [TyVar] -> [TyVar]
-filterEqSpec eq_spec
-  = filter not_in_eq_spec
-  where
-    not_in_eq_spec var = all (not . (== var) . eqSpecTyVar) eq_spec
-
 instance Outputable EqSpec where
   ppr (EqSpec tv ty) = ppr (tv, ty)
 
@@ -1681,14 +1674,35 @@ dataConCannotMatch tys con
 -- "MkId", and so 'dataConUserTyVarsArePermuted' is only called at most once
 -- during a data constructor's lifetime.
 
+checkDataConTyVars :: DataCon -> Bool
+-- Check that the worker and wrapper have the same set of type variables
+-- See Note [DataCon user type variable binders], as well as
+checkDataConTyVars dc
+  = mkUnVarSet (dataConUnconstrainedTyVars dc) == mkUnVarSet (dataConUserTyVars dc)
+    -- Worker tyvars ...should be the same set as...wrapper tyvars
+
+dataConUserTyVarsArePermuted :: DataCon -> Bool
+-- Check whether the worker and wapper have their tpye variables in
+-- the same order.  If not, we need a wrapper to swizzle them.
 -- See Note [DataCon user type variable binders], as well as
 -- Note [Data con wrappers and GADT syntax] for an explanation of what
 -- mkDataConRep is doing with this function.
-dataConUserTyVarsArePermuted :: DataCon -> Bool
-dataConUserTyVarsArePermuted (MkData { dcUnivTyVars = univ_tvs
-                                     , dcExTyCoVars = ex_tvs, dcEqSpec = eq_spec
-                                     , dcUserTyVarBinders = user_tvbs }) =
-  (filterEqSpec eq_spec univ_tvs ++ ex_tvs) /= binderVars user_tvbs
+dataConUserTyVarsArePermuted dc
+  = dataConUnconstrainedTyVars dc /= dataConUserTyVars dc
+    -- Worker tyvars                  Wrapper tyvars
+
+-- | Return the quantified variables (universal and existential)
+--   that are unconstrained by dcEqSpec, in the order that the /worker/ expects
+dataConUnconstrainedTyVars :: DataCon -> [TyVar]
+dataConUnconstrainedTyVars (MkData { dcUnivTyVars = univ_tvs
+                                   , dcExTyCoVars = ex_tvs
+                                   , dcEqSpec     = eq_spec })
+  = [ univ_tv | univ_tv <- univ_tvs
+              , not (isConstraintLikeKind (typeKind (tyVarKind univ_tv)))
+              , not (univ_tv `elemUnVarSet` eq_spec_tvs) ]
+    ++ ex_tvs
+  where
+    eq_spec_tvs = mkUnVarSet (map eqSpecTyVar eq_spec)
 
 {-
 %************************************************************************


=====================================
compiler/GHC/Core/Opt/CallArity.hs
=====================================
@@ -728,7 +728,7 @@ resDel :: Var -> CallArityRes -> CallArityRes
 resDel v (!g, !ae) = (g `delNode` v, ae `delVarEnv` v)
 
 domRes :: CallArityRes -> UnVarSet
-domRes (_, ae) = varEnvDom ae
+domRes (_, ae) = varEnvDomain ae
 
 -- In the result, find out the minimum arity and whether the variable is called
 -- at most once.


=====================================
compiler/GHC/Data/Graph/UnVar.hs
=====================================
@@ -16,7 +16,7 @@ equal to g, but twice as expensive and large.
 -}
 module GHC.Data.Graph.UnVar
     ( UnVarSet
-    , emptyUnVarSet, mkUnVarSet, varEnvDom, unionUnVarSet, unionUnVarSets
+    , emptyUnVarSet, mkUnVarSet, unionUnVarSet, unionUnVarSets
     , extendUnVarSet, extendUnVarSetList, delUnVarSet, delUnVarSetList
     , elemUnVarSet, isEmptyUnVarSet
     , UnVarGraph
@@ -26,13 +26,13 @@ module GHC.Data.Graph.UnVar
     , neighbors
     , hasLoopAt
     , delNode
+    , domUFMUnVarSet
     ) where
 
 import GHC.Prelude
 
-import GHC.Types.Id
-import GHC.Types.Var.Env
-import GHC.Types.Unique.FM
+import GHC.Types.Unique.FM( UniqFM, ufmToSet_Directly )
+import GHC.Types.Var
 import GHC.Utils.Outputable
 import GHC.Types.Unique
 
@@ -50,6 +50,9 @@ newtype UnVarSet = UnVarSet (S.IntSet)
 k :: Var -> Int
 k v = getKey (getUnique v)
 
+domUFMUnVarSet :: UniqFM key elt -> UnVarSet
+domUFMUnVarSet ae = UnVarSet $ ufmToSet_Directly ae
+
 emptyUnVarSet :: UnVarSet
 emptyUnVarSet = UnVarSet S.empty
 
@@ -75,9 +78,6 @@ sizeUnVarSet (UnVarSet s) = S.size s
 mkUnVarSet :: [Var] -> UnVarSet
 mkUnVarSet vs = UnVarSet $ S.fromList $ map k vs
 
-varEnvDom :: VarEnv a -> UnVarSet
-varEnvDom ae = UnVarSet $ ufmToSet_Directly ae
-
 extendUnVarSet :: Var -> UnVarSet -> UnVarSet
 extendUnVarSet v (UnVarSet s) = UnVarSet $ S.insert (k v) s
 


=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -4039,13 +4039,18 @@ mkGADTVars tmpl_tvs dc_tvs subst
               r_ty'  = mkTyVarTy r_tv1
 
                -- Not a simple substitution: make an equality predicate
-          _ -> choose (t_tv':univs) (mkEqSpec t_tv' r_ty : eqs)
+
+          _ -> choose (t_tv':univs) eqs'
                       (extendTvSubst t_sub t_tv (mkTyVarTy t_tv'))
                          -- We've updated the kind of t_tv,
                          -- so add it to t_sub (#14162)
                       r_sub t_tvs
             where
-              t_tv' = updateTyVarKind (substTy t_sub) t_tv
+              tv_kind  = tyVarKind t_tv
+              tv_kind' = substTy t_sub tv_kind
+              t_tv'    = setTyVarKind t_tv tv_kind'
+              eqs' | isConstraintLikeKind (typeKind tv_kind') = eqs
+                   | otherwise = mkEqSpec t_tv' r_ty : eqs
 
       | otherwise
       = pprPanic "mkGADTVars" (ppr tmpl_tvs $$ ppr subst)
@@ -4476,17 +4481,8 @@ checkValidDataCon dflags existential_ok tc con
           -- checked here because we sometimes build invalid DataCons before
           -- erroring above here
         ; when debugIsOn $
-          do { let (univs, exs, eq_spec, _, _, _) = dataConFullSig con
-                   user_tvs                       = dataConUserTyVars con
-                   user_tvbs_invariant
-                     =    Set.fromList (filterEqSpec eq_spec univs ++ exs)
-                       == Set.fromList user_tvs
-             ; massertPpr user_tvbs_invariant
-                          $ vcat ([ ppr con
-                               , ppr univs
-                               , ppr exs
-                               , ppr eq_spec
-                               , ppr user_tvs ]) }
+          massertPpr (checkDataConTyVars con) $
+          ppr con $$  ppr (dataConFullSig con)
 
         ; traceTc "Done validity of data con" $
           vcat [ ppr con


=====================================
compiler/GHC/Types/Id/Make.hs
=====================================
@@ -80,6 +80,7 @@ import GHC.Tc.Utils.TcType as TcType
 import GHC.Utils.Misc
 import GHC.Utils.Outputable
 import GHC.Utils.Panic
+import GHC.Utils.Trace
 import GHC.Utils.Panic.Plain
 
 import GHC.Data.FastString
@@ -741,11 +742,11 @@ mkDataConRep dc_bang_opts fam_envs wrap_name data_con
                      , dcr_bangs   = arg_ibangs }) }
 
   where
-    (univ_tvs, ex_tvs, eq_spec, theta, orig_arg_tys, _orig_res_ty)
+    (univ_tvs, ex_tvs, eq_spec, theta, orig_arg_tys, orig_res_ty)
       = dataConFullSig data_con
     stupid_theta = dataConStupidTheta data_con
     wrap_tvs     = dataConUserTyVars data_con
-    res_ty_args  = substTyVars (mkTvSubstPrs (map eqSpecPair eq_spec)) univ_tvs
+    res_ty_args  = tyConAppArgs orig_res_ty
 
     tycon        = dataConTyCon data_con       -- The representation TyCon (not family)
     wrap_ty      = dataConWrapperType data_con


=====================================
compiler/GHC/Types/Var/Env.hs
=====================================
@@ -23,7 +23,7 @@ module GHC.Types.Var.Env (
         isEmptyVarEnv,
         elemVarEnvByKey,
         filterVarEnv, restrictVarEnv,
-        partitionVarEnv,
+        partitionVarEnv, varEnvDomain,
 
         -- * Deterministic Var environments (maps)
         DVarEnv, DIdEnv, DTyVarEnv,
@@ -82,6 +82,7 @@ import GHC.Types.Name.Occurrence
 import GHC.Types.Name
 import GHC.Types.Var as Var
 import GHC.Types.Var.Set
+import GHC.Data.Graph.UnVar   -- UnVarSet
 import GHC.Types.Unique.Set
 import GHC.Types.Unique.FM
 import GHC.Types.Unique.DFM
@@ -504,6 +505,7 @@ extendVarEnv_Acc  :: (a->b->b) -> (a->b) -> VarEnv b -> Var -> a -> VarEnv b
 plusVarEnv        :: VarEnv a -> VarEnv a -> VarEnv a
 plusVarEnvList    :: [VarEnv a] -> VarEnv a
 extendVarEnvList  :: VarEnv a -> [(Var, a)] -> VarEnv a
+varEnvDomain      :: VarEnv elt -> UnVarSet
 
 partitionVarEnv   :: (a -> Bool) -> VarEnv a -> (VarEnv a, VarEnv a)
 -- | Only keep variables contained in the VarSet
@@ -560,7 +562,9 @@ mkVarEnv_Directly= listToUFM_Directly
 emptyVarEnv      = emptyUFM
 unitVarEnv       = unitUFM
 isEmptyVarEnv    = isNullUFM
-partitionVarEnv       = partitionUFM
+partitionVarEnv  = partitionUFM
+varEnvDomain     = domUFMUnVarSet
+
 
 restrictVarEnv env vs = filterUFM_Directly keep env
   where


=====================================
testsuite/tests/typecheck/should_fail/T12102.hs
=====================================
@@ -17,3 +17,26 @@ type family IsTypeLit a where
 data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type where
   MkNat    :: T 42
   MkSymbol :: T "Don't panic!"
+
+{-  Notes
+
+MkNat [InlPrag=CONLIKE]
+  :: forall {a1} {a2 :: IsTypeLit a1 ~ 'True} {b :: a1}.
+     (a1 ~# Natural, a2 ~# 'Eq#, b ~# 42) =>
+     T b
+
+MkNat :: forall a (c :: IsTypeLit a ~ 'True) (b :: a).
+         (a ~# Natural, b ~# 42) -> T @a @~c b
+
+We don't want to include `c` at all in the constraints.
+No point, and something goes wrong.
+  (~#) :: forall (k1 :: Type) (k2 :: Type). k1 -> k2 -> CONSTRAINT (TupleRep '[])
+
+So (a ~# Natural) is short for  (~#) Type Type a Natural
+And (b ~# 42)     is short for  (~#) a Natural b 42
+
+c ~# Eq# ... ==>  (~#) (IsTypeLit a ~ True) ... c (Eq# ...)
+and that application of (~#) is ill-kinded.
+
+Could generalise (~#), or have four versions of it.  But let's not.
+-}
\ No newline at end of file



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7183bcc0d725688254b508908b1003429d648fd3

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7183bcc0d725688254b508908b1003429d648fd3
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/20220905/3186a7d3/attachment-0001.html>


More information about the ghc-commits mailing list