Commit 98930426 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
parent 10566a81
......@@ -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
......
......@@ -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)
......
{-# 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
......@@ -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, [''])
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