Flesh out Note [The stupid context] and reference itwip/T20501

`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.

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            $