diff --git a/compiler/typecheck/TcDerivInfer.hs b/compiler/typecheck/TcDerivInfer.hs
index efad80f647d1c4aa328e2905fa5e784a56a89561..6c95ec981984cbb87a7998193831e408a6d87413 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
@@ -86,7 +83,7 @@ inferConstraints mechanism
cls_tvs = classTyVars main_cls
sc_constraints = ASSERT2( equalLength cls_tvs inst_tys
, ppr main_cls <+> ppr inst_tys )
- [ mkThetaOrigin DerivOrigin TypeLevel [] [] $
+ [ mkThetaOrigin DerivOrigin TypeLevel [] [] [] $
substTheta cls_subst (classSCTheta main_cls) ]
cls_subst = ASSERT( equalLength cls_tvs inst_tys )
zipTvSubst cls_tvs inst_tys
@@ -213,7 +210,7 @@ inferConstraintsDataConArgs inst_ty inst_tys
-- Stupid constraints
stupid_constraints
- = [ mkThetaOrigin DerivOrigin TypeLevel [] [] $
+ = [ mkThetaOrigin DerivOrigin TypeLevel [] [] [] $
substTheta tc_subst (tyConStupidTheta rep_tc) ]
tc_subst = -- See the comment with all_rep_tc_args for an
-- explanation of this assertion
@@ -297,7 +294,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
@@ -313,23 +309,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'
-
- ; (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)
+ tau_eq = mkPrimEqPred meth_tau dm_tau
; return (mkThetaOrigin DerivOrigin 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.
+ meth_tvs dm_tvs meth_theta (tau_eq:dm_theta)) }
+ ; theta_origins <- lift $ mapM do_one_meth gen_dms
; return (theta_origins, tvs, inst_tys) }
{- Note [Inferring the instance context]
@@ -640,9 +624,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
@@ -650,24 +644,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 ]
@@ -716,8 +709,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
@@ -793,7 +788,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]
@@ -803,11 +798,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 d6b02dcf0038f56d1d79b8646ed9bf680ac99bf8..9fe6bd0871bdd072f66ec8ffab9713e894f7a0c6 100644
--- a/compiler/typecheck/TcDerivUtils.hs
+++ b/compiler/typecheck/TcDerivUtils.hs
@@ -227,67 +227,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 0000000000000000000000000000000000000000..ece83cc497e84d27f11c518e43ccd0d66bf1b913
--- /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 0000000000000000000000000000000000000000..2682d6242fa770c5ad289193328d8996d8135301
--- /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 3360c81850e5677796ed014b60a0cf6c45a77908..4d8b2b6b84039c14e03fdcc42b2ddb43f48a35ca 100644
--- a/testsuite/tests/deriving/should_compile/all.T
+++ b/testsuite/tests/deriving/should_compile/all.T
@@ -101,3 +101,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, [''])