From d7865c4e9fa139d5ba7a40211c1de3e30db0c2f5 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 8 Nov 2021 19:11:58 -0500 Subject: Flesh out Note [The stupid context] and reference it `Note [The stupid context]` in `GHC.Core.DataCon` talks about stupid contexts from `DatatypeContexts`, but prior to this commit, it was rather outdated. This commit spruces it up and references it from places where it is relevant. --- compiler/GHC/Core/ConLike.hs | 1 + compiler/GHC/Core/DataCon.hs | 77 ++++++++++++++++++++++++++------------- compiler/GHC/Core/TyCon.hs | 4 +- compiler/GHC/Rename/Module.hs | 4 +- compiler/GHC/Tc/Deriv/Generics.hs | 1 + compiler/GHC/Tc/Deriv/Infer.hs | 10 ++--- compiler/GHC/Tc/Deriv/Utils.hs | 3 ++ compiler/GHC/Tc/Gen/Expr.hs | 3 +- compiler/GHC/Tc/Gen/Head.hs | 4 +- compiler/GHC/Tc/Gen/Pat.hs | 3 +- compiler/GHC/Tc/TyCl.hs | 3 +- compiler/GHC/Tc/TyCl/Build.hs | 2 + compiler/GHC/Tc/TyCl/Utils.hs | 3 +- 13 files changed, 78 insertions(+), 40 deletions(-) diff --git a/compiler/GHC/Core/ConLike.hs b/compiler/GHC/Core/ConLike.hs index b375b742f0..60f76fb302 100644 --- a/compiler/GHC/Core/ConLike.hs +++ b/compiler/GHC/Core/ConLike.hs @@ -146,6 +146,7 @@ conLikeName (PatSynCon pat_syn) = patSynName pat_syn -- -- > data Eq a => T a = ... -- It is empty for `PatSynCon` as they do not allow such contexts. +-- See @Note [The stupid context]@ in "GHC.Core.DataCon". conLikeStupidTheta :: ConLike -> ThetaType conLikeStupidTheta (RealDataCon data_con) = dataConStupidTheta data_con conLikeStupidTheta (PatSynCon {}) = [] diff --git a/compiler/GHC/Core/DataCon.hs b/compiler/GHC/Core/DataCon.hs index c4c7f90a71..6c256cca10 100644 --- a/compiler/GHC/Core/DataCon.hs +++ b/compiler/GHC/Core/DataCon.hs @@ -251,12 +251,21 @@ Data types can have a context: data (Eq a, Ord b) => T a b = T1 a b | T2 a -and that makes the constructors have a context too -(notice that T2's context is "thinned"): +And that makes the constructors have a context too. A constructor's context +isn't necessarily the same as the data type's context, however. Per the +Haskell98 Report, the part of the datatype context that is used in a data +constructor is the largest subset of the datatype context that constrains +only the type variables free in the data constructor's field types. For +example, here are the types of T1 and T2: T1 :: (Eq a, Ord b) => a -> b -> T a b T2 :: (Eq a) => a -> T a b +Notice that T2's context is "thinned". Since its field is of type `a`, only +the part of the datatype context that mentions `a`—that is, `Eq a`—is +included in T2's context. On the other hand, T1's fields mention both `a` +and `b`, so T1's context includes all of the datatype context. + Furthermore, this context pops up when pattern matching (though GHC hasn't implemented this, but it is in H98, and I've fixed GHC so that it now does): @@ -267,36 +276,49 @@ gets inferred type I say the context is "stupid" because the dictionaries passed are immediately discarded -- they do nothing and have no benefit. +(See Note [Instantiating stupid theta] in GHC.Tc.Gen.Head.) It's a flaw in the language. - Up to now [March 2002] I have put this stupid context into the - type of the "wrapper" constructors functions, T1 and T2, but - that turned out to be jolly inconvenient for generics, and - record update, and other functions that build values of type T - (because they don't have suitable dictionaries available). +GHC has made some efforts to correct this flaw. In GHC, datatype contexts +are not available by default. Instead, one must explicitly opt in to them by +using the DatatypeContexts extension. To discourage their use, GHC has +deprecated DatatypeContexts. + +Some other notes about stupid contexts: + +* Stupid contexts can interact badly with `deriving`. For instance, it's + unclear how to make this derived Functor instance typecheck: - So now I've taken the stupid context out. I simply deal with - it separately in the type checker on occurrences of a - constructor, either in an expression or in a pattern. + data Eq a => T a = MkT a + deriving Functor - [May 2003: actually I think this decision could easily be - reversed now, and probably should be. Generics could be - disabled for types with a stupid context; record updates now - (H98) needs the context too; etc. It's an unforced change, so - I'm leaving it for now --- but it does seem odd that the - wrapper doesn't include the stupid context.] + This is because the derived instance would need to look something like + `instance Functor T where ...`, but there is nowhere to mention the + requisite `Eq a` constraint. For this reason, GHC will throw an error if a + user attempts to derive an instance for Functor (or a Functor-like class) + where the last type variable is used in a datatype context. For Generic(1), + the requirements are even harsher, as stupid contexts are not allowed at all + in derived Generic(1) instances. (We could consider relaxing this requirement + somewhat, although no one has asked for this yet.) -[July 04] With the advent of generalised data types, it's less obvious -what the "stupid context" is. Consider - C :: forall a. Ord a => a -> a -> T (Foo a) -Does the C constructor in Core contain the Ord dictionary? Yes, it must: + Stupid contexts are permitted when deriving instances of non-Functor-like + classes, or when deriving instances of Functor-like classes where the last + type variable isn't mentioned in the stupid context. For example, the + following is permitted: - f :: T b -> Ordering - f = /\b. \x:T b. - case x of - C a (d:Ord a) (p:a) (q:a) -> compare d p q + data Show a => T a = MkT deriving Eq -Note that (Foo a) might not be an instance of Ord. + Note that because of the "thinning" behavior mentioned above, the generated + Eq instance should not mention `Show a`, as the type of MkT doesn't require + it. That is, the following should be generated (#20501): + + instance Eq (T a) where + (MkT == MkT) = True + +* It's not obvious how stupid contexts should interact with GADTs. For this + reason, GHC disallows combining datatype contexts with GADT syntax. As a + result, dcStupidTheta is always empty for data types defined using GADT + syntax. ************************************************************************ * * @@ -414,7 +436,8 @@ data DataCon -- or, rather, a "thinned" version thereof -- "Thinned", because the Report says -- to eliminate any constraints that don't mention - -- tyvars free in the arg types for this constructor + -- tyvars free in the arg types for this constructor. + -- See Note [The stupid context]. -- -- INVARIANT: the free tyvars of dcStupidTheta are a subset of dcUnivTyVars -- Reason: dcStupidTeta is gotten by thinning the stupid theta from the tycon @@ -1346,6 +1369,8 @@ dataConOrigResTy dc = dcOrigResTy dc -- | The \"stupid theta\" of the 'DataCon', such as @data Eq a@ in: -- -- > data Eq a => T a = ... +-- +-- See @Note [The stupid context]@. dataConStupidTheta :: DataCon -> ThetaType dataConStupidTheta dc = dcStupidTheta dc diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs index b0467bed81..fd5b3df534 100644 --- a/compiler/GHC/Core/TyCon.hs +++ b/compiler/GHC/Core/TyCon.hs @@ -797,6 +797,8 @@ data TyCon -- the left of an algebraic type -- declaration, e.g. @Eq a@ in the -- declaration @data Eq a => T a ...@. + -- See @Note [The stupid context]@ in + -- "GHC.Core.DataCon". algTcRhs :: AlgTyConRhs, -- ^ Contains information about the -- data constructors of the algebraic type @@ -2718,7 +2720,7 @@ newTyConDataCon_maybe _ = Nothing -- | Find the \"stupid theta\" of the 'TyCon'. A \"stupid theta\" is the context -- to the left of an algebraic type declaration, e.g. @Eq a@ in the declaration --- @data Eq a => T a ...@ +-- @data Eq a => T a ...@. See @Note [The stupid context]@ in "GHC.Core.DataCon". tyConStupidTheta :: TyCon -> [PredType] tyConStupidTheta (AlgTyCon {algTcStupidTheta = stupid}) = stupid tyConStupidTheta (FunTyCon {}) = [] diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs index bdb5a29e55..2febede5c5 100644 --- a/compiler/GHC/Rename/Module.hs +++ b/compiler/GHC/Rename/Module.hs @@ -1924,7 +1924,9 @@ rnDataDefn :: HsDocContext -> HsDataDefn GhcPs rnDataDefn doc (HsDataDefn { dd_ND = new_or_data, dd_cType = cType , dd_ctxt = context, dd_cons = condecls , dd_kindSig = m_sig, dd_derivs = derivs }) - = do { checkTc (h98_style || null (fromMaybeContext context)) + = do { -- DatatypeContexts (i.e., stupid contexts) can't be combined with + -- GADT syntax. See Note [The stupid context] in GHC.Core.DataCon. + checkTc (h98_style || null (fromMaybeContext context)) (badGadtStupidTheta doc) ; (m_sig', sig_fvs) <- case m_sig of diff --git a/compiler/GHC/Tc/Deriv/Generics.hs b/compiler/GHC/Tc/Deriv/Generics.hs index 3d71c25b7d..eee7496b6f 100644 --- a/compiler/GHC/Tc/Deriv/Generics.hs +++ b/compiler/GHC/Tc/Deriv/Generics.hs @@ -119,6 +119,7 @@ following constraints are satisfied. alpha-renaming). (b) D cannot have a "stupid context". + See Note [The stupid context] in GHC.Core.DataCon. (c) The right-hand side of D cannot include existential types, universally quantified types, or "exotic" unlifted types. An exotic unlifted type diff --git a/compiler/GHC/Tc/Deriv/Infer.hs b/compiler/GHC/Tc/Deriv/Infer.hs index 7276bfde83..2466931219 100644 --- a/compiler/GHC/Tc/Deriv/Infer.hs +++ b/compiler/GHC/Tc/Deriv/Infer.hs @@ -194,13 +194,9 @@ inferConstraintsStock (DerivInstTys { dit_cls_tys = cls_tys ] -- Stupid constraints from DatatypeContexts. Note that we -- must gather these constraints from the data constructors, - -- not from the parent type constructor, as the latter can - -- lead to redundant constraints in some cases. For example, - -- the derived Eq instance for: - -- - -- data Show a => T a = MkT deriving Eq - -- - -- Should not have Show in the instance context (#20501). + -- not from the parent type constructor, as the latter could + -- lead to redundant constraints due to thinning. + -- See Note [The stupid context] in GHC.Core.DataCon. stupid_theta = [ substTyWith (dataConUnivTyVars data_con) all_rep_tc_args diff --git a/compiler/GHC/Tc/Deriv/Utils.hs b/compiler/GHC/Tc/Deriv/Utils.hs index d97db525eb..dfd1b557a7 100644 --- a/compiler/GHC/Tc/Deriv/Utils.hs +++ b/compiler/GHC/Tc/Deriv/Utils.hs @@ -930,6 +930,9 @@ cond_functorOK allowFunctions allowExQuantifiedLastTyVar _ _ rep_tc | null tc_tvs = NotValid $ DerivErrMustHaveSomeParameters rep_tc + -- We can't handle stupid contexts that mention the last type argument, + -- so error out if we encounter one. + -- See Note [The stupid context] in GHC.Core.DataCon. | not (null bad_stupid_theta) = NotValid $ DerivErrMustNotHaveClassContext rep_tc bad_stupid_theta diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs index c9e9129251..6739e9a375 100644 --- a/compiler/GHC/Tc/Gen/Expr.hs +++ b/compiler/GHC/Tc/Gen/Expr.hs @@ -790,7 +790,8 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = Left rbnds }) res_ -- Typecheck the bindings ; rbinds' <- tcRecordUpd con1 con1_arg_tys' rbinds - -- STEP 6: Deal with the stupid theta + -- STEP 6: Deal with the stupid theta. + -- See Note [The stupid context] in GHC.Core.DataCon. ; let theta' = substThetaUnchecked scrut_subst (conLikeStupidTheta con1) ; instStupidTheta RecordUpdOrigin theta' diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs index bfaba5efcc..821b118ded 100644 --- a/compiler/GHC/Tc/Gen/Head.hs +++ b/compiler/GHC/Tc/Gen/Head.hs @@ -905,7 +905,9 @@ being able to reconstruct the exact original program. Note [Instantiating stupid theta] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider a data type with a "stupid theta": +Consider a data type with a "stupid theta" (see +Note [The stupid context] in GHC.Core.DataCon): + data Ord a => T a = MkT (Maybe a) We want to generate an Ord constraint for every use of MkT; but diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs index a09d77b6f7..a235c43236 100644 --- a/compiler/GHC/Tc/Gen/Pat.hs +++ b/compiler/GHC/Tc/Gen/Pat.hs @@ -1311,7 +1311,8 @@ tcConArg penv (arg_pat, Scaled arg_mult arg_ty) addDataConStupidTheta :: DataCon -> [TcType] -> TcM () -- Instantiate the "stupid theta" of the data con, and throw --- the constraints into the constraint set +-- the constraints into the constraint set. +-- See Note [The stupid context] in GHC.Core.DataCon. addDataConStupidTheta data_con inst_tys | null stupid_theta = return () | otherwise = instStupidTheta origin inst_theta diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs index 5dfa4cec86..17b6e2fc43 100644 --- a/compiler/GHC/Tc/TyCl.hs +++ b/compiler/GHC/Tc/TyCl.hs @@ -3312,7 +3312,8 @@ dataDeclChecks tc_name new_or_data mctxt cons ; let gadt_syntax = consUseGadtSyntax cons ; checkTc (gadtSyntax_ok || not gadt_syntax) (badGadtDecl tc_name) - -- Check that the stupid theta is empty for a GADT-style declaration + -- Check that the stupid theta is empty for a GADT-style declaration. + -- See Note [The stupid context] in GHC.Core.DataCon. ; checkTc (null stupid_theta || not gadt_syntax) (badStupidTheta tc_name) -- Check that a newtype has exactly one constructor diff --git a/compiler/GHC/Tc/TyCl/Build.hs b/compiler/GHC/Tc/TyCl/Build.hs index 7206fe70bd..4b44069950 100644 --- a/compiler/GHC/Tc/TyCl/Build.hs +++ b/compiler/GHC/Tc/TyCl/Build.hs @@ -192,6 +192,8 @@ buildDataCon fam_envs src_name declared_infix prom_info src_bangs impl_bangs -- the type variables mentioned in the arg_tys -- ToDo: Or functionally dependent on? -- This whole stupid theta thing is, well, stupid. +-- +-- See Note [The stupid context] in GHC.Core.DataCon. mkDataConStupidTheta :: TyCon -> [Type] -> [TyVar] -> [PredType] mkDataConStupidTheta tycon arg_tys univ_tvs | null stupid_theta = [] -- The common case diff --git a/compiler/GHC/Tc/TyCl/Utils.hs b/compiler/GHC/Tc/TyCl/Utils.hs index 1ce9ef8f82..347a7e57ff 100644 --- a/compiler/GHC/Tc/TyCl/Utils.hs +++ b/compiler/GHC/Tc/TyCl/Utils.hs @@ -906,7 +906,8 @@ mkOneRecordSelector all_cons idDetails fl has_sel || has_sel == NoFieldSelectors sel_ty | is_naughty = unitTy -- See Note [Naughty record selectors] | otherwise = mkForAllTys (tyVarSpecToBinders data_tvbs) $ - mkPhiTy (conLikeStupidTheta con1) $ -- Urgh! + -- Urgh! See Note [The stupid context] in GHC.Core.DataCon + mkPhiTy (conLikeStupidTheta con1) $ -- req_theta is empty for normal DataCon mkPhiTy req_theta $ mkVisFunTyMany data_ty $ -- cgit v1.2.1