import TcEnv
import InstEnv
import TcGadt
-import TcMType
import TcType
+import TcMType
import TcIface
import Var
-import TyCon
import Name
import NameSet
import Class
:: SDoc
-> TcTyVarSet -- fv(T); type vars
-> [Inst] -- Wanted
- -> TcM ([TcTyVar], -- Tyvars to quantify (zonked)
+ -> TcM ([TcTyVar], -- Tyvars to quantify (zonked and quantified)
[Inst], -- Dict Ids that must be bound here (zonked)
TcDictBinds) -- Bindings
-- Any free (escaping) Insts are tossed into the environment
| otherwise
= do { let givens' = filter isDict givens
-- The givens can include methods
+ -- See Note [Pruning the givens in an implication constraint]
-- If there are no 'givens', then it's safe to
-- partition the 'wanteds' by their qtvs, thereby trimming irreds
-> [Name] -- Things bound in this group
-> TcTyVarSet -- Free in the type of the RHSs
-> [Inst] -- Free in the RHSs
- -> TcM ([TyVar], -- Tyvars to quantify (zonked)
+ -> TcM ([TyVar], -- Tyvars to quantify (zonked and quantified)
TcDictBinds) -- Bindings
-- tcSimpifyRestricted returns no constraints to
-- quantify over; by definition there are none.
to float the (C Int) out, even though it mentions no type variable in
the constraints!
+Note [Pruning the givens in an implication constraint]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are about to form the implication constraint
+ forall tvs. Eq a => Ord b
+The (Eq a) cannot contribute to the (Ord b), because it has no access to
+the type variable 'b'. So we could filter out the (Eq a) from the givens.
+
+Doing so would be a bit tidier, but all the implication constraints get
+simplified away by the optimiser, so it's no great win. So I don't take
+advantage of that at the moment.
+
+If you do, BE CAREFUL of wobbly type variables.
+
+
%************************************************************************
%* *
Avails and AvailHow: the pool of evidence
\begin{code}
tcSimplifyDeriv :: InstOrigin
- -> TyCon
-> [TyVar]
-> ThetaType -- Wanted
-> TcM ThetaType -- Needed
+-- Given instance (wanted) => C inst_ty
+-- Simplify 'wanted' as much as possible
+-- The inst_ty is needed only for the termination check
-tcSimplifyDeriv orig tc tyvars theta
- = tcInstTyVars tyvars `thenM` \ (tvs, _, tenv) ->
+tcSimplifyDeriv orig tyvars theta
+ = do { (tvs, _, tenv) <- tcInstTyVars tyvars
-- The main loop may do unification, and that may crash if
-- it doesn't see a TcTyVar, so we have to instantiate. Sigh
-- ToDo: what if two of them do get unified?
- newDictBndrsO orig (substTheta tenv theta) `thenM` \ wanteds ->
- topCheckLoop doc wanteds `thenM` \ (irreds, _) ->
-
- doptM Opt_GlasgowExts `thenM` \ gla_exts ->
- doptM Opt_AllowUndecidableInstances `thenM` \ undecidable_ok ->
- let
- inst_ty = mkTyConApp tc (mkTyVarTys tvs)
- (ok_insts, bad_insts) = partition is_ok_inst irreds
- is_ok_inst inst
- = isDict inst -- Exclude implication consraints
- && (isTyVarClassPred pred || (gla_exts && ok_gla_pred pred))
- where
- pred = dictPred inst
-
- ok_gla_pred pred = null (checkInstTermination [inst_ty] [pred])
- -- See Note [Deriving context]
-
- tv_set = mkVarSet tvs
- simpl_theta = map dictPred ok_insts
- weird_preds = [pred | pred <- simpl_theta
- , not (tyVarsOfPred pred `subVarSet` tv_set)]
-
- -- Check for a bizarre corner case, when the derived instance decl should
- -- have form instance C a b => D (T a) where ...
- -- Note that 'b' isn't a parameter of T. This gives rise to all sorts
- -- of problems; in particular, it's hard to compare solutions for
- -- equality when finding the fixpoint. So I just rule it out for now.
-
- rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
- -- This reverse-mapping is a Royal Pain,
- -- but the result should mention TyVars not TcTyVars
- in
- -- In effect, the bad and wierd insts cover all of the cases that
- -- would make checkValidInstance fail; if it were called right after tcSimplifyDeriv
- -- * wierd_preds ensures unambiguous instances (checkAmbiguity in checkValidInstance)
- -- * ok_gla_pred ensures termination (checkInstTermination in checkValidInstance)
- addNoInstanceErrs bad_insts `thenM_`
- mapM_ (addErrTc . badDerivedPred) weird_preds `thenM_`
- returnM (substTheta rev_env simpl_theta)
+ ; wanteds <- newDictBndrsO orig (substTheta tenv theta)
+ ; (irreds, _) <- topCheckLoop doc wanteds
+
+ -- Insist that the context of a derived instance declaration
+ -- consists of constraints of form (C a b), where a,b are
+ -- type variables
+ -- NB: the caller will further check the tv_dicts for
+ -- legal instance-declaration form
+ ; let (tv_dicts, non_tv_dicts) = partition isTyVarDict irreds
+ ; addNoInstanceErrs non_tv_dicts
+
+ ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
+ simpl_theta = substTheta rev_env (map dictPred tv_dicts)
+ -- This reverse-mapping is a pain, but the result
+ -- should mention the original TyVars not TcTyVars
+
+ ; return simpl_theta }
where
doc = ptext SLIT("deriving classes for a data type")
\end{code}
quotes (ppr default_ty),
pprDictsInFull tidy_dicts]
--- Used for the ...Thetas variants; all top level
-badDerivedPred pred
- = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
- ptext SLIT("type variables that are not data type parameters"),
- nest 2 (ptext SLIT("Offending constraint:") <+> ppr pred)]
-
reduceDepthErr n stack
= vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
ptext SLIT("Use -fcontext-stack=N to increase stack size to N"),