Fix two pernicious bugs in DeriveAnyClass

The way GHC was handling `DeriveAnyClass` was subtly wrong
in two notable ways:

* In `inferConstraintsDAC`, we were //always// bumping the `TcLevel`
  of newly created unification variables, under the assumption that
  we would always place those unification variables inside an
  implication constraint. But #14932 showed precisely the scenario
  where we had `DeriveAnyClass` //without// any of the generated
  constraints being used inside an implication, which made GHC
  incorrectly believe the unification variables were untouchable.
* Even worse, we were using the generated unification variables from
  `inferConstraintsDAC` in every single iteration of `simplifyDeriv`.
  In #14933, however, we have a scenario where we fill in a
  unification variable with a skolem in one iteration, discard it,
  proceed on to another iteration, use the same unification variable
  (still filled in with the old skolem), and try to unify it with
  a //new// skolem! This results in an utter disaster.

The root of both these problems is `inferConstraintsDAC`. This patch
fixes the issue by no longer generating unification variables
directly in `inferConstraintsDAC`. Instead, we store the original
variables from a generic default type signature in `to_metas`, a new
field of `ThetaOrigin`, and in each iteration of `simplifyDeriv`, we
generate fresh meta tyvars (avoiding the second issue). Moreover,
this allows us to more carefully fine-tune the `TcLevel` under which
we create these meta tyvars, fixing the first issue.

Test Plan: make test TEST="T14932 T14933"

Reviewers: simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #14932, #14933

Differential Revision: https://phabricator.haskell.org/D4507

5 files changed, 171 insertions, 79 deletions

diff --git a/compiler/typecheck/TcDerivInfer.hs b/compiler/typecheck/TcDerivInfer.hs
index ebabc0f806..2ea8372a34 100644
--- a/compiler/typecheck/TcDerivInfer.hs
+++ b/compiler/typecheck/TcDerivInfer.hs
@@ -19,14 +19,12 @@ import Bag
 import BasicTypes
 import Class
 import DataCon
--- import DynFlags
 import ErrUtils
 import Inst
 import Outputable
 import PrelNames
 import TcDerivUtils
 import TcEnv
--- import TcErrors (reportAllUnsolved)
 import TcGenFunctor
 import TcGenGenerics
 import TcMType
@@ -36,11 +34,10 @@ import TyCon
 import Type
 import TcSimplify
 import TcValidity (validDerivPred)
-import TcUnify (buildImplicationFor)
+import TcUnify (buildImplicationFor, checkConstraints)
 import Unify (tcUnifyTy)
 import Util
 import Var
-import VarEnv
 import VarSet
 
 import Control.Monad
@@ -88,7 +85,7 @@ inferConstraints mechanism
              sc_constraints = ASSERT2( equalLength cls_tvs inst_tys
                                      , ppr main_cls <+> ppr inst_tys )
                               [ mkThetaOrigin (mkDerivOrigin wildcard)
-                                              TypeLevel [] [] $
+                                              TypeLevel [] [] [] $
                                 substTheta cls_subst (classSCTheta main_cls) ]
              cls_subst = ASSERT( equalLength cls_tvs inst_tys )
                          zipTvSubst cls_tvs inst_tys
@@ -216,7 +213,7 @@ inferConstraintsDataConArgs inst_ty inst_tys
 
                -- Stupid constraints
            stupid_constraints
-             = [ mkThetaOrigin deriv_origin TypeLevel [] [] $
+             = [ mkThetaOrigin deriv_origin TypeLevel [] [] [] $
                  substTheta tc_subst (tyConStupidTheta rep_tc) ]
            tc_subst = -- See the comment with all_rep_tc_args for an
                       -- explanation of this assertion
@@ -303,7 +300,6 @@ inferConstraintsDAC inst_tys
                        | (sel_id, Just (_, GenericDM dm_ty)) <- classOpItems cls ]
 
              cls_tvs = classTyVars cls
-             empty_subst = mkEmptyTCvSubst (mkInScopeSet (mkVarSet tvs))
 
              do_one_meth :: (Id, Type) -> TcM ThetaOrigin
                -- (Id,Type) are the selector Id and the generic default method type
@@ -319,24 +315,11 @@ inferConstraintsDAC inst_tys
                           gen_dm_ty' = substTyWith cls_tvs inst_tys gen_dm_ty
                           (dm_tvs, dm_theta, dm_tau)
                                      = tcSplitNestedSigmaTys gen_dm_ty'
+                          tau_eq     = mkPrimEqPred meth_tau dm_tau
+                    ; return (mkThetaOrigin (mkDerivOrigin wildcard) TypeLevel
+                                meth_tvs dm_tvs meth_theta (tau_eq:dm_theta)) }
 
-                    ; (subst, _meta_tvs) <- pushTcLevelM_ $
-                                            newMetaTyVarsX empty_subst dm_tvs
-                      -- Yuk: the pushTcLevel is to match the one in mk_wanteds
-                      --      simplifyDeriv.  If we don't, the unification
-                      --      variables will bogusly be untouchable.
-
-                    ; let dm_theta' = substTheta subst dm_theta
-                          tau_eq = mkPrimEqPred meth_tau (substTy subst dm_tau)
-                    ; return (mkThetaOrigin (mkDerivOrigin wildcard)
-                                TypeLevel meth_tvs meth_theta
-                                (tau_eq:dm_theta')) }
-
-       ; theta_origins <- lift $ pushTcLevelM_ (mapM do_one_meth gen_dms)
-            -- Yuk: the pushTcLevel is to match the one wrapping the call
-            --      to mk_wanteds in simplifyDeriv.  If we omit this, the
-            --      unification variables will wrongly be untouchable.
-
+       ; theta_origins <- lift $ mapM do_one_meth gen_dms
        ; return (theta_origins, tvs, inst_tys) }
 
 {- Note [Inferring the instance context]
@@ -655,9 +638,19 @@ simplifyDeriv pred tvs thetas
                let given_pred = substTy skol_subst given
                in newEvVar given_pred
 
-             mk_wanted_ct :: PredOrigin -> TcM CtEvidence
-             mk_wanted_ct (PredOrigin wanted o t_or_k)
-               = newWanted o (Just t_or_k) (substTyUnchecked skol_subst wanted)
+             mk_wanted_cts :: [TyVar] -> [PredOrigin] -> TcM [CtEvidence]
+             mk_wanted_cts metas_to_be wanteds
+               = do -- We instantiate metas_to_be with fresh meta type
+                    -- variables. Currently, these can only be type variables
+                    -- quantified in generic default type signatures.
+                    -- See Note [Gathering and simplifying constraints for
+                    -- DeriveAnyClass]
+                    (meta_subst, _meta_tvs) <- newMetaTyVars metas_to_be
+                    let wanted_subst = skol_subst `unionTCvSubst` meta_subst
+                        mk_wanted_ct (PredOrigin wanted o t_or_k)
+                          = newWanted o (Just t_or_k) $
+                            substTyUnchecked wanted_subst wanted
+                    mapM mk_wanted_ct wanteds
 
              -- Create the implications we need to solve. For stock and newtype
              -- deriving, these implication constraints will be simple class
@@ -665,24 +658,23 @@ simplifyDeriv pred tvs thetas
              -- But with DeriveAnyClass, we make an implication constraint.
              -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
              mk_wanteds :: ThetaOrigin -> TcM WantedConstraints
-             mk_wanteds (ThetaOrigin { to_tvs            = local_skols
-                                     , to_givens         = givens
-                                     , to_wanted_origins = wanteds })
-               | null local_skols, null givens
-               = do { wanted_cts <- mapM mk_wanted_ct wanteds
-                    ; return (mkSimpleWC wanted_cts) }
-               | otherwise
-               = do { given_evs <- mapM mk_given_ev givens
-                    ; (wanted_cts, tclvl) <- pushTcLevelM $
-                                             mapM mk_wanted_ct wanteds
-                    ; (implic, _) <- buildImplicationFor tclvl skol_info local_skols
-                                                   given_evs (mkSimpleWC wanted_cts)
-                    ; pure (mkImplicWC implic) }
+             mk_wanteds (ThetaOrigin { to_anyclass_skols  = ac_skols
+                                     , to_anyclass_metas  = ac_metas
+                                     , to_anyclass_givens = ac_givens
+                                     , to_wanted_origins  = wanteds })
+               = do { ac_given_evs <- mapM mk_given_ev ac_givens
+                    ; (_, wanteds)
+                        <- captureConstraints $
+                           checkConstraints skol_info ac_skols ac_given_evs $
+                           do { cts <- mk_wanted_cts ac_metas wanteds
+                              ; emitSimples $ listToCts
+                                            $ map mkNonCanonical cts }
+                    ; pure wanteds }
 
        -- See [STEP DAC BUILD]
        -- Generate the implication constraints constraints to solve with the
        -- skolemized variables
-       ; (wanteds, tclvl) <- pushTcLevelM $ mapM mk_wanteds thetas
+       ; wanteds <- mapM mk_wanteds thetas
 
        ; traceTc "simplifyDeriv inputs" $
          vcat [ pprTyVars tvs $$ ppr thetas $$ ppr wanteds, doc ]
@@ -731,8 +723,10 @@ simplifyDeriv pred tvs thetas
 
        -- See [STEP DAC RESIDUAL]
        ; min_theta_vars <- mapM newEvVar min_theta
-       ; (leftover_implic, _) <- buildImplicationFor tclvl skol_info tvs_skols
-                                   min_theta_vars solved_implics
+       ; tc_lvl <- getTcLevel
+       ; (leftover_implic, _)
+           <- buildImplicationFor (pushTcLevel tc_lvl) skol_info tvs_skols
+                                  min_theta_vars solved_implics
        -- This call to simplifyTop is purely for error reporting
        -- See Note [Error reporting for deriving clauses]
        -- See also Note [Exotic derived instance contexts], which are caught
@@ -808,7 +802,7 @@ GHC were typechecking the binding
    bar = $gdm bar
 it would
    * skolemise the expected type of bar
-   * instantiate the type of $dm_bar with meta-type variables
+   * instantiate the type of $gdm_bar with meta-type variables
    * build an implication constraint
 
 [STEP DAC BUILD]
@@ -818,11 +812,25 @@ So that's what we do.  We build the constraint (call it C1)
                       Maybe s -> b -> String
                           ~ Maybe s -> cc -> String)
 
-The 'cc' is a unification variable that comes from instantiating
-$dm_bar's type.  The equality constraint comes from marrying up
-the instantiated type of $dm_bar with the specified type of bar.
-Notice that the type variables from the instance, 's' in this case,
-are global to this constraint.
+Here, the 'b' comes from the quantified type variable in the expected type
+of bar (i.e., 'to_anyclass_skols' in 'ThetaOrigin'). The 'cc' is a unification
+variable that comes from instantiating the quantified type variable 'c' in
+$gdm_bar's type (i.e., 'to_anyclass_metas' in 'ThetaOrigin).
+
+The (Ix b) constraint comes from the context of bar's type
+(i.e., 'to_wanted_givens' in 'ThetaOrigin'). The (Show (Maybe s)) and (Ix cc)
+constraints come from the context of $gdm_bar's type
+(i.e., 'to_anyclass_givens' in 'ThetaOrigin').
+
+The equality constraint (Maybe s -> b -> String) ~ (Maybe s -> cc -> String)
+comes from marrying up the instantiated type of $gdm_bar with the specified
+type of bar. Notice that the type variables from the instance, 's' in this
+case, are global to this constraint.
+
+Note that it is vital that we instantiate the `c` in $gdm_bar's type with a new
+unification variable for each iteration of simplifyDeriv. If we re-use the same
+unification variable across multiple iterations, then bad things can happen,
+such as Trac #14933.
 
 Similarly for 'baz', givng the constraint C2
 
diff --git a/compiler/typecheck/TcDerivUtils.hs b/compiler/typecheck/TcDerivUtils.hs
index ef9e83239d..c10b0b87d6 100644
--- a/compiler/typecheck/TcDerivUtils.hs
+++ b/compiler/typecheck/TcDerivUtils.hs
@@ -283,67 +283,104 @@ data DerivStatus = CanDerive                 -- Stock class, can derive
 -- and whether or the constraint deals in types or kinds.
 data PredOrigin = PredOrigin PredType CtOrigin TypeOrKind
 
--- | A list of wanted 'PredOrigin' constraints ('to_wanted_origins') alongside
--- any corresponding given constraints ('to_givens') and locally quantified
--- type variables ('to_tvs').
+-- | A list of wanted 'PredOrigin' constraints ('to_wanted_origins') to
+-- simplify when inferring a derived instance's context. These are used in all
+-- deriving strategies, but in the particular case of @DeriveAnyClass@, we
+-- need extra information. In particular, we need:
 --
--- In most cases, 'to_givens' will be empty, as most deriving mechanisms (e.g.,
--- stock and newtype deriving) do not require given constraints. The exception
--- is @DeriveAnyClass@, which can involve given constraints. For example,
--- if you tried to derive an instance for the following class using
--- @DeriveAnyClass@:
+-- * 'to_anyclass_skols', the list of type variables bound by a class method's
+--   regular type signature, which should be rigid.
+--
+-- * 'to_anyclass_metas', the list of type variables bound by a class method's
+--   default type signature. These can be unified as necessary.
+--
+-- * 'to_anyclass_givens', the list of constraints from a class method's
+--   regular type signature, which can be used to help solve constraints
+--   in the 'to_wanted_origins'.
+--
+-- (Note that 'to_wanted_origins' will likely contain type variables from the
+-- derived type class or data type, neither of which will appear in
+-- 'to_anyclass_skols' or 'to_anyclass_metas'.)
+--
+-- For all other deriving strategies, it is always the case that
+-- 'to_anyclass_skols', 'to_anyclass_metas', and 'to_anyclass_givens' are
+-- empty.
+--
+-- Here is an example to illustrate this:
 --
 -- @
 -- class Foo a where
---   bar :: a -> b -> String
---   default bar :: (Show a, Ix b) => a -> b -> String
---   bar = show
+--   bar :: forall b. Ix b => a -> b -> String
+--   default bar :: forall y. (Show a, Ix y) => a -> y -> String
+--   bar x y = show x ++ show (range (y, y))
 --
 --   baz :: Eq a => a -> a -> Bool
 --   default baz :: Ord a => a -> a -> Bool
 --   baz x y = compare x y == EQ
+--
+-- data Quux q = Quux deriving anyclass Foo
 -- @
 --
 -- Then it would generate two 'ThetaOrigin's, one for each method:
 --
 -- @
--- [ ThetaOrigin { to_tvs            = [b]
---               , to_givens         = []
---               , to_wanted_origins = [Show a, Ix b] }
--- , ThetaOrigin { to_tvs            = []
---               , to_givens         = [Eq a]
---               , to_wanted_origins = [Ord a] }
+-- [ ThetaOrigin { to_anyclass_skols  = [b]
+--               , to_anyclass_metas  = [y]
+--               , to_anyclass_givens = [Ix b]
+--               , to_wanted_origins  = [ Show (Quux q), Ix y
+--                                      , (Quux q -> b -> String) ~
+--                                        (Quux q -> y -> String)
+--                                      ] }
+-- , ThetaOrigin { to_anyclass_skols  = []
+--               , to_anyclass_metas  = []
+--               , to_anyclass_givens = [Eq (Quux q)]
+--               , to_wanted_origins  = [ Ord (Quux q)
+--                                      , (Quux q -> Quux q -> Bool) ~
+--                                        (Quux q -> Quux q -> Bool)
+--                                      ] }
 -- ]
 -- @
+--
+-- (Note that the type variable @q@ is bound by the data type @Quux@, and thus
+-- it appears in neither 'to_anyclass_skols' nor 'to_anyclass_metas'.)
+--
+-- See @Note [Gathering and simplifying constraints for DeriveAnyClass]@
+-- in "TcDerivInfer" for an explanation of how 'to_wanted_origins' are
+-- determined in @DeriveAnyClass@, as well as how 'to_anyclass_skols',
+-- 'to_anyclass_metas', and 'to_anyclass_givens' are used.
 data ThetaOrigin
-  = ThetaOrigin { to_tvs            :: [TyVar]
-                , to_givens         :: ThetaType
-                , to_wanted_origins :: [PredOrigin] }
+  = ThetaOrigin { to_anyclass_skols  :: [TyVar]
+                , to_anyclass_metas  :: [TyVar]
+                , to_anyclass_givens :: ThetaType
+                , to_wanted_origins  :: [PredOrigin] }
 
 instance Outputable PredOrigin where
   ppr (PredOrigin ty _ _) = ppr ty -- The origin is not so interesting when debugging
 
 instance Outputable ThetaOrigin where
-  ppr (ThetaOrigin { to_tvs = tvs
-                   , to_givens = givens
-                   , to_wanted_origins = wanted_origins })
+  ppr (ThetaOrigin { to_anyclass_skols  = ac_skols
+                   , to_anyclass_metas  = ac_metas
+                   , to_anyclass_givens = ac_givens
+                   , to_wanted_origins  = wanted_origins })
     = hang (text "ThetaOrigin")
-         2 (vcat [ text "to_tvs            =" <+> ppr tvs
-                 , text "to_givens         =" <+> ppr givens
-                 , text "to_wanted_origins =" <+> ppr wanted_origins ])
+         2 (vcat [ text "to_anyclass_skols  =" <+> ppr ac_skols
+                 , text "to_anyclass_metas  =" <+> ppr ac_metas
+                 , text "to_anyclass_givens =" <+> ppr ac_givens
+                 , text "to_wanted_origins  =" <+> ppr wanted_origins ])
 
 mkPredOrigin :: CtOrigin -> TypeOrKind -> PredType -> PredOrigin
 mkPredOrigin origin t_or_k pred = PredOrigin pred origin t_or_k
 
-mkThetaOrigin :: CtOrigin -> TypeOrKind -> [TyVar] -> ThetaType -> ThetaType
+mkThetaOrigin :: CtOrigin -> TypeOrKind
+              -> [TyVar] -> [TyVar] -> ThetaType -> ThetaType
               -> ThetaOrigin
-mkThetaOrigin origin t_or_k tvs givens
-  = ThetaOrigin tvs givens . map (mkPredOrigin origin t_or_k)
+mkThetaOrigin origin t_or_k skols metas givens
+  = ThetaOrigin skols metas givens . map (mkPredOrigin origin t_or_k)
 
 -- A common case where the ThetaOrigin only contains wanted constraints, with
 -- no givens or locally scoped type variables.
 mkThetaOriginFromPreds :: [PredOrigin] -> ThetaOrigin
-mkThetaOriginFromPreds = ThetaOrigin [] []
+mkThetaOriginFromPreds = ThetaOrigin [] [] []
 
 substPredOrigin :: HasCallStack => TCvSubst -> PredOrigin -> PredOrigin
 substPredOrigin subst (PredOrigin pred origin t_or_k)
diff --git a/testsuite/tests/deriving/should_compile/T14932.hs b/testsuite/tests/deriving/should_compile/T14932.hs
new file mode 100644
index 0000000000..ece83cc497
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T14932.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+module T14932 where
+
+import GHC.Exts
+
+class Zero a where
+ zero :: a
+ default zero :: (Code a ~ '[xs], All Zero xs) => a
+ zero = undefined
+
+type family All c xs :: Constraint where
+ All c '[] = ()
+ All c (x : xs) = (c x, All c xs)
+
+type family Code (a :: *) :: [[*]]
+type instance Code B1 = '[ '[ ] ]
+
+data B1 = B1
+ deriving Zero
diff --git a/testsuite/tests/deriving/should_compile/T14933.hs b/testsuite/tests/deriving/should_compile/T14933.hs
new file mode 100644
index 0000000000..2682d6242f
--- /dev/null
+++ b/testsuite/tests/deriving/should_compile/T14933.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE DeriveAnyClass    #-}
+{-# LANGUAGE TypeFamilies      #-}
+module T14933 where
+
+class Wrapped s where
+  type Unwrapped s :: *
+
+class Fork m where
+    fork :: (x, m)
+
+    default fork :: ( Wrapped m
+                    , Unwrapped m ~ t
+                    , Fork t
+                    ) => (x, m)
+    fork = undefined
+
+newtype MyThing m = MyThing m
+    deriving Fork
+
+instance Wrapped (MyThing m) where
+    type Unwrapped (MyThing m) = m
diff --git a/testsuite/tests/deriving/should_compile/all.T b/testsuite/tests/deriving/should_compile/all.T
index a06cd27c84..b2dd670212 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -102,3 +102,5 @@ test('T14331', normal, compile, [''])
 test('T14578', normal, compile, ['-ddump-deriv -dsuppress-uniques'])
 test('T14579', normal, compile, [''])
 test('T14682', normal, compile, ['-ddump-deriv -dsuppress-uniques'])
+test('T14932', normal, compile, [''])
+test('T14933', normal, compile, [''])