Commit d8dbe293 authored by Ryan Scott's avatar Ryan Scott Committed by Ben Gamari

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

(cherry picked from commit 98930426)
parent 43f63a6b
...@@ -19,14 +19,12 @@ import Bag ...@@ -19,14 +19,12 @@ import Bag
import BasicTypes import BasicTypes
import Class import Class
import DataCon import DataCon
-- import DynFlags
import ErrUtils import ErrUtils
import Inst import Inst
import Outputable import Outputable
import PrelNames import PrelNames
import TcDerivUtils import TcDerivUtils
import TcEnv import TcEnv
-- import TcErrors (reportAllUnsolved)
import TcGenFunctor import TcGenFunctor
import TcGenGenerics import TcGenGenerics
import TcMType import TcMType
...@@ -36,11 +34,10 @@ import TyCon ...@@ -36,11 +34,10 @@ import TyCon
import Type import Type
import TcSimplify import TcSimplify
import TcValidity (validDerivPred) import TcValidity (validDerivPred)
import TcUnify (buildImplicationFor) import TcUnify (buildImplicationFor, checkConstraints)
import Unify (tcUnifyTy) import Unify (tcUnifyTy)
import Util import Util
import Var import Var
import VarEnv
import VarSet import VarSet
import Control.Monad import Control.Monad
...@@ -86,7 +83,7 @@ inferConstraints mechanism ...@@ -86,7 +83,7 @@ inferConstraints mechanism
cls_tvs = classTyVars main_cls cls_tvs = classTyVars main_cls
sc_constraints = ASSERT2( equalLength cls_tvs inst_tys sc_constraints = ASSERT2( equalLength cls_tvs inst_tys
, ppr main_cls <+> ppr inst_tys ) , ppr main_cls <+> ppr inst_tys )
[ mkThetaOrigin DerivOrigin TypeLevel [] [] $ [ mkThetaOrigin DerivOrigin TypeLevel [] [] [] $
substTheta cls_subst (classSCTheta main_cls) ] substTheta cls_subst (classSCTheta main_cls) ]
cls_subst = ASSERT( equalLength cls_tvs inst_tys ) cls_subst = ASSERT( equalLength cls_tvs inst_tys )
zipTvSubst cls_tvs inst_tys zipTvSubst cls_tvs inst_tys
...@@ -213,7 +210,7 @@ inferConstraintsDataConArgs inst_ty inst_tys ...@@ -213,7 +210,7 @@ inferConstraintsDataConArgs inst_ty inst_tys
-- Stupid constraints -- Stupid constraints
stupid_constraints stupid_constraints
= [ mkThetaOrigin DerivOrigin TypeLevel [] [] $ = [ mkThetaOrigin DerivOrigin TypeLevel [] [] [] $
substTheta tc_subst (tyConStupidTheta rep_tc) ] substTheta tc_subst (tyConStupidTheta rep_tc) ]
tc_subst = -- See the comment with all_rep_tc_args for an tc_subst = -- See the comment with all_rep_tc_args for an
-- explanation of this assertion -- explanation of this assertion
...@@ -297,7 +294,6 @@ inferConstraintsDAC inst_tys ...@@ -297,7 +294,6 @@ inferConstraintsDAC inst_tys
| (sel_id, Just (_, GenericDM dm_ty)) <- classOpItems cls ] | (sel_id, Just (_, GenericDM dm_ty)) <- classOpItems cls ]
cls_tvs = classTyVars cls cls_tvs = classTyVars cls
empty_subst = mkEmptyTCvSubst (mkInScopeSet (mkVarSet tvs))
do_one_meth :: (Id, Type) -> TcM ThetaOrigin do_one_meth :: (Id, Type) -> TcM ThetaOrigin
-- (Id,Type) are the selector Id and the generic default method type -- (Id,Type) are the selector Id and the generic default method type
...@@ -313,23 +309,11 @@ inferConstraintsDAC inst_tys ...@@ -313,23 +309,11 @@ inferConstraintsDAC inst_tys
gen_dm_ty' = substTyWith cls_tvs inst_tys gen_dm_ty gen_dm_ty' = substTyWith cls_tvs inst_tys gen_dm_ty
(dm_tvs, dm_theta, dm_tau) (dm_tvs, dm_theta, dm_tau)
= tcSplitNestedSigmaTys gen_dm_ty' = tcSplitNestedSigmaTys gen_dm_ty'
tau_eq = mkPrimEqPred meth_tau dm_tau
; (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 DerivOrigin TypeLevel ; return (mkThetaOrigin DerivOrigin TypeLevel
meth_tvs meth_theta (tau_eq:dm_theta')) } meth_tvs dm_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) } ; return (theta_origins, tvs, inst_tys) }
{- Note [Inferring the instance context] {- Note [Inferring the instance context]
...@@ -640,9 +624,19 @@ simplifyDeriv pred tvs thetas ...@@ -640,9 +624,19 @@ simplifyDeriv pred tvs thetas
let given_pred = substTy skol_subst given let given_pred = substTy skol_subst given
in newEvVar given_pred in newEvVar given_pred
mk_wanted_ct :: PredOrigin -> TcM CtEvidence mk_wanted_cts :: [TyVar] -> [PredOrigin] -> TcM [CtEvidence]
mk_wanted_ct (PredOrigin wanted o t_or_k) mk_wanted_cts metas_to_be wanteds
= newWanted o (Just t_or_k) (substTyUnchecked skol_subst wanted) = 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 -- Create the implications we need to solve. For stock and newtype
-- deriving, these implication constraints will be simple class -- deriving, these implication constraints will be simple class
...@@ -650,24 +644,23 @@ simplifyDeriv pred tvs thetas ...@@ -650,24 +644,23 @@ simplifyDeriv pred tvs thetas
-- But with DeriveAnyClass, we make an implication constraint. -- But with DeriveAnyClass, we make an implication constraint.
-- See Note [Gathering and simplifying constraints for DeriveAnyClass] -- See Note [Gathering and simplifying constraints for DeriveAnyClass]
mk_wanteds :: ThetaOrigin -> TcM WantedConstraints mk_wanteds :: ThetaOrigin -> TcM WantedConstraints
mk_wanteds (ThetaOrigin { to_tvs = local_skols mk_wanteds (ThetaOrigin { to_anyclass_skols = ac_skols
, to_givens = givens , to_anyclass_metas = ac_metas
, to_wanted_origins = wanteds }) , to_anyclass_givens = ac_givens
| null local_skols, null givens , to_wanted_origins = wanteds })
= do { wanted_cts <- mapM mk_wanted_ct wanteds = do { ac_given_evs <- mapM mk_given_ev ac_givens
; return (mkSimpleWC wanted_cts) } ; (_, wanteds)
| otherwise <- captureConstraints $
= do { given_evs <- mapM mk_given_ev givens checkConstraints skol_info ac_skols ac_given_evs $
; (wanted_cts, tclvl) <- pushTcLevelM $ do { cts <- mk_wanted_cts ac_metas wanteds
mapM mk_wanted_ct wanteds ; emitSimples $ listToCts
; (implic, _) <- buildImplicationFor tclvl skol_info local_skols $ map mkNonCanonical cts }
given_evs (mkSimpleWC wanted_cts) ; pure wanteds }
; pure (mkImplicWC implic) }
-- See [STEP DAC BUILD] -- See [STEP DAC BUILD]
-- Generate the implication constraints constraints to solve with the -- Generate the implication constraints constraints to solve with the
-- skolemized variables -- skolemized variables
; (wanteds, tclvl) <- pushTcLevelM $ mapM mk_wanteds thetas ; wanteds <- mapM mk_wanteds thetas
; traceTc "simplifyDeriv inputs" $ ; traceTc "simplifyDeriv inputs" $
vcat [ pprTyVars tvs $$ ppr thetas $$ ppr wanteds, doc ] vcat [ pprTyVars tvs $$ ppr thetas $$ ppr wanteds, doc ]
...@@ -716,8 +709,10 @@ simplifyDeriv pred tvs thetas ...@@ -716,8 +709,10 @@ simplifyDeriv pred tvs thetas
-- See [STEP DAC RESIDUAL] -- See [STEP DAC RESIDUAL]
; min_theta_vars <- mapM newEvVar min_theta ; min_theta_vars <- mapM newEvVar min_theta
; (leftover_implic, _) <- buildImplicationFor tclvl skol_info tvs_skols ; tc_lvl <- getTcLevel
min_theta_vars solved_implics ; (leftover_implic, _)
<- buildImplicationFor (pushTcLevel tc_lvl) skol_info tvs_skols
min_theta_vars solved_implics
-- This call to simplifyTop is purely for error reporting -- This call to simplifyTop is purely for error reporting
-- See Note [Error reporting for deriving clauses] -- See Note [Error reporting for deriving clauses]
-- See also Note [Exotic derived instance contexts], which are caught -- See also Note [Exotic derived instance contexts], which are caught
...@@ -793,7 +788,7 @@ GHC were typechecking the binding ...@@ -793,7 +788,7 @@ GHC were typechecking the binding
bar = $gdm bar bar = $gdm bar
it would it would
* skolemise the expected type of bar * 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 * build an implication constraint
[STEP DAC BUILD] [STEP DAC BUILD]
...@@ -803,11 +798,25 @@ So that's what we do. We build the constraint (call it C1) ...@@ -803,11 +798,25 @@ So that's what we do. We build the constraint (call it C1)
Maybe s -> b -> String Maybe s -> b -> String
~ Maybe s -> cc -> String) ~ Maybe s -> cc -> String)
The 'cc' is a unification variable that comes from instantiating Here, the 'b' comes from the quantified type variable in the expected type
$dm_bar's type. The equality constraint comes from marrying up of bar (i.e., 'to_anyclass_skols' in 'ThetaOrigin'). The 'cc' is a unification
the instantiated type of $dm_bar with the specified type of bar. variable that comes from instantiating the quantified type variable 'c' in
Notice that the type variables from the instance, 's' in this case, $gdm_bar's type (i.e., 'to_anyclass_metas' in 'ThetaOrigin).
are global to this constraint.
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 Similarly for 'baz', givng the constraint C2
......
...@@ -227,67 +227,104 @@ data DerivStatus = CanDerive -- Stock class, can derive ...@@ -227,67 +227,104 @@ data DerivStatus = CanDerive -- Stock class, can derive
-- and whether or the constraint deals in types or kinds. -- and whether or the constraint deals in types or kinds.
data PredOrigin = PredOrigin PredType CtOrigin TypeOrKind data PredOrigin = PredOrigin PredType CtOrigin TypeOrKind
-- | A list of wanted 'PredOrigin' constraints ('to_wanted_origins') alongside -- | A list of wanted 'PredOrigin' constraints ('to_wanted_origins') to
-- any corresponding given constraints ('to_givens') and locally quantified -- simplify when inferring a derived instance's context. These are used in all
-- type variables ('to_tvs'). -- 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., -- * 'to_anyclass_skols', the list of type variables bound by a class method's
-- stock and newtype deriving) do not require given constraints. The exception -- regular type signature, which should be rigid.
-- is @DeriveAnyClass@, which can involve given constraints. For example, --
-- if you tried to derive an instance for the following class using -- * 'to_anyclass_metas', the list of type variables bound by a class method's
-- @DeriveAnyClass@: -- 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 -- class Foo a where
-- bar :: a -> b -> String -- bar :: forall b. Ix b => a -> b -> String
-- default bar :: (Show a, Ix b) => a -> b -> String -- default bar :: forall y. (Show a, Ix y) => a -> y -> String
-- bar = show -- bar x y = show x ++ show (range (y, y))
-- --
-- baz :: Eq a => a -> a -> Bool -- baz :: Eq a => a -> a -> Bool
-- default baz :: Ord a => a -> a -> Bool -- default baz :: Ord a => a -> a -> Bool
-- baz x y = compare x y == EQ -- 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: -- Then it would generate two 'ThetaOrigin's, one for each method:
-- --
-- @ -- @
-- [ ThetaOrigin { to_tvs = [b] -- [ ThetaOrigin { to_anyclass_skols = [b]
-- , to_givens = [] -- , to_anyclass_metas = [y]
-- , to_wanted_origins = [Show a, Ix b] } -- , to_anyclass_givens = [Ix b]
-- , ThetaOrigin { to_tvs = [] -- , to_wanted_origins = [ Show (Quux q), Ix y
-- , to_givens = [Eq a] -- , (Quux q -> b -> String) ~
-- , to_wanted_origins = [Ord a] } -- (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 data ThetaOrigin
= ThetaOrigin { to_tvs :: [TyVar] = ThetaOrigin { to_anyclass_skols :: [TyVar]
, to_givens :: ThetaType , to_anyclass_metas :: [TyVar]
, to_wanted_origins :: [PredOrigin] } , to_anyclass_givens :: ThetaType
, to_wanted_origins :: [PredOrigin] }
instance Outputable PredOrigin where instance Outputable PredOrigin where
ppr (PredOrigin ty _ _) = ppr ty -- The origin is not so interesting when debugging ppr (PredOrigin ty _ _) = ppr ty -- The origin is not so interesting when debugging
instance Outputable ThetaOrigin where instance Outputable ThetaOrigin where
ppr (ThetaOrigin { to_tvs = tvs ppr (ThetaOrigin { to_anyclass_skols = ac_skols
, to_givens = givens , to_anyclass_metas = ac_metas
, to_wanted_origins = wanted_origins }) , to_anyclass_givens = ac_givens
, to_wanted_origins = wanted_origins })
= hang (text "ThetaOrigin") = hang (text "ThetaOrigin")
2 (vcat [ text "to_tvs =" <+> ppr tvs 2 (vcat [ text "to_anyclass_skols =" <+> ppr ac_skols
, text "to_givens =" <+> ppr givens , text "to_anyclass_metas =" <+> ppr ac_metas
, text "to_wanted_origins =" <+> ppr wanted_origins ]) , text "to_anyclass_givens =" <+> ppr ac_givens
, text "to_wanted_origins =" <+> ppr wanted_origins ])
mkPredOrigin :: CtOrigin -> TypeOrKind -> PredType -> PredOrigin mkPredOrigin :: CtOrigin -> TypeOrKind -> PredType -> PredOrigin
mkPredOrigin origin t_or_k pred = PredOrigin pred origin t_or_k 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 -> ThetaOrigin
mkThetaOrigin origin t_or_k tvs givens mkThetaOrigin origin t_or_k skols metas givens
= ThetaOrigin tvs givens . map (mkPredOrigin origin t_or_k) = ThetaOrigin skols metas givens . map (mkPredOrigin origin t_or_k)
-- A common case where the ThetaOrigin only contains wanted constraints, with -- A common case where the ThetaOrigin only contains wanted constraints, with
-- no givens or locally scoped type variables. -- no givens or locally scoped type variables.
mkThetaOriginFromPreds :: [PredOrigin] -> ThetaOrigin mkThetaOriginFromPreds :: [PredOrigin] -> ThetaOrigin
mkThetaOriginFromPreds = ThetaOrigin [] [] mkThetaOriginFromPreds = ThetaOrigin [] [] []
substPredOrigin :: HasCallStack => TCvSubst -> PredOrigin -> PredOrigin substPredOrigin :: HasCallStack => TCvSubst -> PredOrigin -> PredOrigin
substPredOrigin subst (PredOrigin pred origin t_or_k) substPredOrigin subst (PredOrigin pred origin t_or_k)
......
{-# 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
{-# 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
...@@ -101,3 +101,5 @@ test('T14331', normal, compile, ['']) ...@@ -101,3 +101,5 @@ test('T14331', normal, compile, [''])
test('T14578', normal, compile, ['-ddump-deriv -dsuppress-uniques']) test('T14578', normal, compile, ['-ddump-deriv -dsuppress-uniques'])
test('T14579', normal, compile, ['']) test('T14579', normal, compile, [''])
test('T14682', normal, compile, ['-ddump-deriv -dsuppress-uniques']) test('T14682', normal, compile, ['-ddump-deriv -dsuppress-uniques'])
test('T14932', normal, compile, [''])
test('T14933', normal, compile, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment