-- but when there is nothing to quantify we don't wrap
-- in a degenerate implication, so we do that here instead
simplifyTop wanteds
- = simplifyCheck SimplCheck wanteds
+ = simplifyCheck (SimplCheck (ptext (sLit "top level"))) wanteds
------------------
simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
-> TcM () -- Succeeds iff the constraint is soluble
simplifyDefault theta
= do { wanted <- newFlatWanteds DefaultOrigin theta
- ; _ignored_ev_binds <- simplifyCheck SimplCheck (mkFlatWC wanted)
+ ; _ignored_ev_binds <- simplifyCheck (SimplCheck (ptext (sLit "defaults")))
+ (mkFlatWC wanted)
; return () }
\end{code}
\begin{code}
simplifyDeriv :: CtOrigin
- -> [TyVar]
- -> ThetaType -- Wanted
- -> TcM ThetaType -- Needed
+ -> PredType
+ -> [TyVar]
+ -> ThetaType -- Wanted
+ -> TcM ThetaType -- Needed
-- Given instance (wanted) => C inst_ty
-- Simplify 'wanted' as much as possibles
-- Fail if not possible
-simplifyDeriv orig tvs theta
- = do { tvs_skols <- tcInstSuperSkolTyVars tvs -- Skolemize
- -- One reason is that the constraint solving machinery
- -- expects *TcTyVars* not TyVars. Another is that
- -- when looking up instances we don't want overlap
- -- of type variables
+simplifyDeriv orig pred tvs theta
+ = do { tvs_skols <- tcInstSkolTyVars tvs -- Skolemize
+ -- The constraint solving machinery
+ -- expects *TcTyVars* not TyVars.
+ -- We use *non-overlappable* (vanilla) skolems
+ -- See Note [Overlap and deriving]
; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
+ doc = parens $ ptext (sLit "deriving") <+> parens (ppr pred)
; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
; traceTc "simplifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
; (residual_wanted, _binds)
- <- runTcS SimplInfer NoUntouchables $
+ <- runTcS (SimplInfer doc) NoUntouchables $
solveWanteds emptyInert (mkFlatWC wanted)
; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
; return (substTheta subst_skol min_theta) }
\end{code}
+Note [Overlap and deriving]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider some overlapping instances:
+ data Show a => Show [a] where ..
+ data Show [Char] where ...
+
+Now a data type with deriving:
+ data T a = MkT [a] deriving( Show )
+
+We want to get the derived instance
+ instance Show [a] => Show (T a) where...
+and NOT
+ instance Show a => Show (T a) where...
+so that the (Show (T Char)) instance does the Right Thing
+
+It's very like the situation when we're inferring the type
+of a function
+ f x = show [x]
+and we want to infer
+ f :: Show [a] => a -> String
+
+BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
+ the context for the derived instance.
+ Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
+
Note [Exotic derived instance contexts]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In a 'derived' instance declaration, we *infer* the context. It's a
-- Step 2
-- Now simplify the possibly-bound constraints
; (simpl_results, tc_binds0)
- <- runTcS SimplInfer NoUntouchables $
+ <- runTcS (SimplInfer (ppr (map fst name_taus))) NoUntouchables $
simplifyWithApprox (zonked_wanteds { wc_flat = perhaps_bound })
; when (insolubleWC simpl_results) -- Fail fast if there is an insoluble constraint
-- variables; hence *no untouchables*
; (lhs_results, lhs_binds)
- <- runTcS SimplRuleLhs untch $
+ <- runTcS (SimplRuleLhs name) untch $
solveWanteds emptyInert zonked_lhs
; traceTc "simplifyRule" $
-- Hence the rather painful ad-hoc treatement here
; rhs_binds_var@(EvBindsVar evb_ref _) <- newTcEvBinds
- ; rhs_binds1 <- simplifyCheck SimplCheck $
+ ; let doc = ptext (sLit "rhs of rule") <+> doubleQuotes (ftext name)
+ ; rhs_binds1 <- simplifyCheck (SimplCheck doc) $
WC { wc_flat = emptyBag
, wc_insol = emptyBag
, wc_impl = unitBag $
| otherwise
= do { -- See Note [Preparing inert set for implications]
-- Push the unsolved wanteds inwards, but as givens
- traceTcS "solveWanteds: preparing inerts for implications {" empty
-
- ; let pushed_givens = givensFromWanteds unsolved_cans
+ let pushed_givens = givensFromWanteds unsolved_cans
tcs_untouchables = filterVarSet isFlexiTcsTv $
tyVarsOfEvVarXs pushed_givens
-- See Note [Extra TcsTv untouchables]
+ ; traceTcS "solveWanteds: preparing inerts for implications {"
+ (vcat [ppr tcs_untouchables, ppr pushed_givens])
+
; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens
; traceTcS "solveWanteds: } now doing nested implications {" $
constraints. In effect, by floating an equality out of the
implication we are committing to have it solved in the outside.
-NB: A consequence is that every simplifier-generated TcsTv variable that gets floated out
- of an implication becomes now untouchable next time we go inside that implication to
- solve any residual constraints. In effect, by floating an equality out of the implication
- we are committing to have it solved in the outside.
+Note [Float Equalities out of Implications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We want to float equalities out of vanilla existentials, but *not* out
+of GADT pattern matches.
\begin{code}
; return (niFixTvSubst ni_subst, unsolved_can_cts) }
where
- solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setWantedCoBind cv ty
+ solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setCoBind cv ty
------------
type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])