Note [Implicit parameters and ambiguity]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-What type should we infer for this?
- f x = (show ?y, x::Int)
-Since we must quantify over the ?y, the most plausible type is
- f :: (Show a, ?y::a) => Int -> (String, Int)
-But notice that the type of the RHS is (String,Int), with no type
-varibables mentioned at all! The type of f looks ambiguous. But
-it isn't, because at a call site we might have
- let ?y = 5::Int in f 7
+Only a *class* predicate can give rise to ambiguity
+An *implicit parameter* cannot. For example:
+ foo :: (?x :: [a]) => Int
+ foo = length ?x
+is fine. The call site will suppply a particular 'x'
+
+Furthermore, the type variables fixed by an implicit parameter
+propagate to the others. E.g.
+ foo :: (Show a, ?x::[a]) => Int
+ foo = show (?x++?x)
+The type of foo looks ambiguous. But it isn't, because at a call site
+we might have
+ let ?x = 5::Int in foo
and all is well. In effect, implicit parameters are, well, parameters,
so we can take their type variables into account as part of the
"tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
| otherwise -- Otherwise we must generate a binding
= do { uniq <- newUnique
; span <- getSrcSpanM
- ; let (eq_givens,dict_givens) = partitionGivenEqInsts givens
+ ; let (eq_givens, dict_givens) = partition isEqInst givens
eq_tyvar_cos = map TyVarTy $ uniqSetToList $ tyVarsOfTypes $ map eqInstType eq_givens
; let name = mkInternalName uniq (mkVarOcc "ic") span
implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
tci_tyvars = all_tvs,
tci_given = (eq_givens ++ dict_givens),
tci_wanted = irreds, tci_loc = loc }
- ; let
- -- only create binder for dict_irreds
- -- we
- (eq_irreds,dict_irreds) = partitionWantedEqInsts irreds
+ ; let -- only create binder for dict_irreds
+ (eq_irreds, dict_irreds) = partition isEqInst irreds
n_dict_irreds = length dict_irreds
dict_irred_ids = map instToId dict_irreds
tup_ty = mkTupleTy Boxed n_dict_irreds (map idType dict_irred_ids)
checkLoop env wanteds
= go env wanteds []
where go env wanteds needed_givens
- = do { -- Givens are skolems, so no need to zonk them
- wanteds' <- zonkInsts wanteds
+ = do { -- We do need to zonk the givens; cf Note [Zonking RedEnv]
+ ; env' <- zonkRedEnv env
+ ; wanteds' <- zonkInsts wanteds
- ; (improved, binds, irreds, more_needed_givens) <- reduceContext env wanteds'
+ ; (improved, binds, irreds, more_needed_givens) <- reduceContext env' wanteds'
; let all_needed_givens = needed_givens ++ more_needed_givens
-- Using an instance decl might have introduced a fresh type variable
-- which might have been unified, so we'd get an infinite loop
-- if we started again with wanteds! See Note [LOOP]
- { (irreds1, binds1, all_needed_givens1) <- go env irreds all_needed_givens
+ { (irreds1, binds1, all_needed_givens1) <- go env' irreds all_needed_givens
; return (irreds1, binds `unionBags` binds1, all_needed_givens1) } }
\end{code}
+Note [Zonking RedEnv]
+~~~~~~~~~~~~~~~~~~~~~
+It might appear as if the givens in RedEnv are always rigid, but that is not
+necessarily the case for programs involving higher-rank types that have class
+contexts constraining the higher-rank variables. An example from tc237 in the
+testsuite is
+
+ class Modular s a | s -> a
+
+ wim :: forall a w. Integral a
+ => a -> (forall s. Modular s a => M s w) -> w
+ wim i k = error "urk"
+
+ test5 :: (Modular s a, Integral a) => M s a
+ test5 = error "urk"
+
+ test4 = wim 4 test4'
+
+Notice how the variable 'a' of (Modular s a) in the rank-2 type of wim is
+quantified further outside. When type checking test4, we have to check
+whether the signature of test5 is an instance of
+
+ (forall s. Modular s a => M s w)
+
+Consequently, we will get (Modular s t_a), where t_a is a TauTv into the
+givens.
+
+Given the FD of Modular in this example, class improvement will instantiate
+t_a to 'a', where 'a' is the skolem from test5's signatures (due to the
+Modular s a predicate in that signature). If we don't zonk (Modular s t_a) in
+the givens, we will get into a loop as improveOne uses the unification engine
+TcGadt.tcUnifyTys, which doesn't know about mutable type variables.
+
+
Note [LOOP]
~~~~~~~~~~~
class If b t e r | b t e -> r
-- to fromInteger; this looks fragile to me
; lookup_result <- lookupSimpleInst w'
; case lookup_result of
- GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws)
+ GenInst ws' rhs ->
+ go dicts (addInstToDictBind binds w rhs) (ws' ++ ws)
NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w)
}
\end{code}
-- of a predicate when adding it to the avails
-- The reason for this flag is entirely the super-class loop problem
-- Note [SUPER-CLASS LOOP 1]
+
+zonkRedEnv :: RedEnv -> TcM RedEnv
+zonkRedEnv env
+ = do { givens' <- mappM zonkInst (red_givens env)
+ ; return $ env {red_givens = givens'}
+ }
\end{code}
+
%************************************************************************
%* *
\subsection[reduce]{@reduce@}
%* *
%************************************************************************
+Note [Ancestor Equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+During context reduction, we add to the wanted equalities also those
+equalities that (transitively) occur in superclass contexts of wanted
+class constraints. Consider the following code
+
+ class a ~ Int => C a
+ instance C Int
+
+If (C a) is wanted, we want to add (a ~ Int), which will be discharged by
+substituting Int for a. Hence, we ultimately want (C Int), which we
+discharge with the explicit instance.
\begin{code}
reduceContext :: RedEnv
text "----------------------"
]))
+ ; let givens = red_givens env
+ (given_eqs0, given_dicts0) = partition isEqInst givens
+ (wanted_eqs0, wanted_dicts) = partition isEqInst wanteds
- ; let givens = red_givens env
- (given_eqs0,given_dicts0) = partitionGivenEqInsts givens
- (wanted_eqs0,wanted_dicts) = partitionWantedEqInsts wanteds
+ -- We want to add as wanted equalities those that (transitively)
+ -- occur in superclass contexts of wanted class constraints.
+ -- See Note [Ancestor Equalities]
+ ; ancestor_eqs <- ancestorEqualities wanted_dicts
+ ; let wanted_eqs = wanted_eqs0 ++ ancestor_eqs
+ ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
- ; wanted_ancestor_eqs <- (mapM wantedAncestorEqualities wanted_dicts >>= \ls -> return (concat ls))
- ; traceTc (text "test wanted SCs" <+> ppr wanted_ancestor_eqs)
- ; let wanted_eqs = wanted_ancestor_eqs ++ wanted_eqs0
+ -- 1. Normalise the *given* *equality* constraints
+ ; (given_eqs, eliminate_skolems) <- normaliseGivenEqs given_eqs0
- ; -- 1. Normalise the *given* *equality* constraints
- (given_eqs,eliminate_skolems) <- normaliseGivens given_eqs0
-
- ; -- 2. Normalise the *given* *dictionary* constraints
+ -- 2. Normalise the *given* *dictionary* constraints
-- wrt. the toplevel and given equations
- (given_dicts,given_binds) <- normaliseGivenDicts given_eqs given_dicts0
-
- ; -- 3. Solve the *wanted* *equation* constraints
- eq_irreds0 <- solveWanteds given_eqs wanted_eqs
+ ; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs
+ given_dicts0
- -- 4. Normalise the *wanted* equality constraints with respect to each other
- ; eq_irreds <- normaliseWanteds eq_irreds0
+ -- 3. Solve the *wanted* *equation* constraints
+ ; eq_irreds0 <- solveWantedEqs given_eqs wanted_eqs
--- -- Do the real work
--- -- Process non-implication constraints first, so that they are
--- -- available to help solving the implication constraints
--- -- ToDo: seems a bit inefficient and ad-hoc
--- ; let (implics, rest) = partition isImplicInst wanteds
--- ; avails <- reduceList env (rest ++ implics) init_state
+ -- 4. Normalise the *wanted* equality constraints with respect to
+ -- each other
+ ; eq_irreds <- normaliseWantedEqs eq_irreds0
-- 5. Build the Avail mapping from "given_dicts"
; init_state <- foldlM addGiven emptyAvails given_dicts
; wanted_dicts' <- zonkInsts wanted_dicts
; avails <- reduceList env wanted_dicts' init_state
; (binds, irreds0, needed_givens) <- extractResults avails wanted_dicts'
- ; traceTc (text "reduceContext extractresults" <+> vcat
- [ppr avails,ppr wanted_dicts',ppr binds,ppr needed_givens])
+ ; traceTc $ text "reduceContext extractresults" <+> vcat
+ [ppr avails,ppr wanted_dicts',ppr binds,ppr needed_givens]
- ; -- 7. Normalise the *wanted* *dictionary* constraints
+ -- 7. Normalise the *wanted* *dictionary* constraints
-- wrt. the toplevel and given equations
- (irreds1,normalise_binds1) <- normaliseWantedDicts given_eqs irreds0
+ ; (irreds1,normalise_binds1) <- normaliseWantedDicts given_eqs irreds0
- ; -- 8. Substitute the wanted *equations* in the wanted *dictionaries*
- (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1
+ -- 8. Substitute the wanted *equations* in the wanted *dictionaries*
+ ; (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1
- ; -- 9. eliminate the artificial skolem constants introduced in 1.
- eliminate_skolems
+ -- 9. eliminate the artificial skolem constants introduced in 1.
+ ; eliminate_skolems
-- If there was some FD improvement,
-- or new wanted equations have been exposed,
; let improved = availsImproved avails
|| (not $ isEmptyBag normalise_binds1)
|| (not $ isEmptyBag normalise_binds2)
- || (not $ null $ fst $ partitionGivenEqInsts irreds)
+ || (any isEqInst irreds)
; traceTc (text "reduceContext end" <+> (vcat [
text "----------------------",
text "----------------------"
]))
- ; return (improved, given_binds `unionBags` normalise_binds1 `unionBags` normalise_binds2 `unionBags` binds, irreds ++ eq_irreds, needed_givens) }
+ ; return (improved,
+ given_binds `unionBags` normalise_binds1
+ `unionBags` normalise_binds2
+ `unionBags` binds,
+ irreds ++ eq_irreds,
+ needed_givens)
+ }
tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
tcImproveOne avails inst
-- when inferring types.
; let dict_wanteds = filter (not . isEqInst) wanteds
- (extra_eq_givens,extra_dict_givens) = partitionGivenEqInsts extra_givens
+ (extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens
dict_ids = map instToId extra_dict_givens
-- TOMDO: given equational constraints bug!
-- we need a different evidence for given
Just (Given id)
| id == w_id -> go avails binds irreds (w:givens) ws
- | otherwise -> go avails (addBind binds w (nlHsVar id)) irreds (update_id w id:givens) ws
+ | otherwise ->
+ go avails (addInstToDictBind binds w (nlHsVar id)) irreds
+ (update_id w id:givens) ws
-- The sought Id can be one of the givens, via a superclass chain
-- and then we definitely don't want to generate an x=x binding!
Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds givens (ws' ++ ws)
where
- new_binds = addBind binds w rhs
+ new_binds = addInstToDictBind binds w rhs
where
w_id = instToId w
update_id m@(Method{}) id = m {tci_id = id}
Just (Rhs rhs ws') -> go (add_given avails w) new_binds givens (ws' ++ ws)
where
- new_binds = addBind binds w rhs
+ new_binds = addInstToDictBind binds w rhs
where
w_id = instToId w
-- and hopefully the optimiser will spot the duplicated work
| otherwise
= return (refined_givens, avails)
-
-addRefinedGiven' :: Refinement -> [Inst] -> Inst -> TcM [Inst]
-addRefinedGiven' reft refined_givens given
- | isDict given -- We sometimes have 'given' methods, but they
- -- are always optional, so we can drop them
- , let pred = dictPred given
- , isRefineablePred pred -- See Note [ImplicInst rigidity]
- , Just (co, pred) <- refinePred reft pred
- = do { new_given <- newDictBndr (instLoc given) pred
- ; return (new_given:refined_givens) }
- -- ToDo: the superclasses of the original given all exist in Avails
- -- so we could really just cast them, but it's more awkward to do,
- -- and hopefully the optimiser will spot the duplicated work
- | otherwise
- = return refined_givens
\end{code}
Note [ImplicInst rigidity]
where
is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
-- Note: this compares by *type*, not by Unique
- deps = findAllDeps (unitVarSet (instToId inst)) avail
+ deps = findAllDeps (unitVarSet (instToVar inst)) avail
dep_tys = map idType (varSetElems deps)
findAllDeps :: IdSet -> AvailHow -> IdSet
find_all :: IdSet -> Inst -> IdSet
find_all so_far kid
+ | isEqInst kid = so_far
| kid_id `elemVarSet` so_far = so_far
| Just avail <- findAvail avails kid = findAllDeps so_far' avail
| otherwise = so_far'
where
(clas, tys) = getDictClassTys dict
(tyvars, sc_theta, sc_sels, _) = classBigSig clas
- sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
+ sc_theta' = filter (not . isEqPred) $
+ substTheta (zipTopTvSubst tyvars tys) sc_theta
add_sc avails (sc_dict, sc_sel)
| is_loop (dictPred sc_dict) = return avails -- See Note [SUPERCLASS-LOOP 2]
; addSCs is_loop avails' sc_dict }
where
sc_sel_rhs = L (instSpan dict) (HsWrap co_fn (HsVar sc_sel))
- co_fn = WpApp (instToId dict) <.> mkWpTyApps tys
+ co_fn = WpApp (instToVar dict) <.> mkWpTyApps tys
is_given :: Inst -> Bool
is_given sc_dict = case findAvail avails sc_dict of
Just (Given _) -> True -- Given is cheaper than superclass selection
other -> False
-
-wantedAncestorEqualities :: Inst -> TcM [Inst]
-wantedAncestorEqualities dict
- | isClassDict dict
- = mapM mkWantedEqInst $ filter isEqPred $ bagToList $ wantedAncestorEqualities' (dictPred dict) emptyBag
- | otherwise
- = return []
-
-wantedAncestorEqualities' :: PredType -> Bag PredType -> Bag PredType
-wantedAncestorEqualities' pred bag
- = ASSERT( isClassPred pred )
- let (clas, tys) = getClassPredTys pred
+-- From the a set of insts obtain all equalities that (transitively) occur in
+-- superclass contexts of class constraints (aka the ancestor equalities).
+--
+ancestorEqualities :: [Inst] -> TcM [Inst]
+ancestorEqualities
+ = mapM mkWantedEqInst -- turn only equality predicates..
+ . filter isEqPred -- ..into wanted equality insts
+ . bagToList
+ . addAEsToBag emptyBag -- collect the superclass constraints..
+ . map dictPred -- ..of all predicates in a bag
+ . filter isClassDict
+ where
+ addAEsToBag :: Bag PredType -> [PredType] -> Bag PredType
+ addAEsToBag bag [] = bag
+ addAEsToBag bag (pred:preds)
+ | pred `elemBag` bag = addAEsToBag bag preds
+ | isEqPred pred = addAEsToBag bagWithPred preds
+ | isClassPred pred = addAEsToBag bagWithPred predsWithSCs
+ | otherwise = addAEsToBag bag preds
+ where
+ bagWithPred = bag `snocBag` pred
+ predsWithSCs = preds ++ substTheta (zipTopTvSubst tyvars tys) sc_theta
+ --
(tyvars, sc_theta, _, _) = classBigSig clas
- sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
- add_sc bag sc_pred
- | elemBag sc_pred bag = bag
- | not (isEqPred sc_pred)
- && not (isClassPred sc_pred)
- = bag
- | isEqPred sc_pred = consBag sc_pred bag
- | otherwise = let bag' = consBag sc_pred bag
- in wantedAncestorEqualities' sc_pred bag'
- in foldl add_sc bag sc_theta'
-
+ (clas, tys) = getClassPredTys pred
\end{code}
+
%************************************************************************
%* *
\section{tcSimplifyTop: defaulting}
-> 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 tyvars theta
= do { (tvs, _, tenv) <- tcInstTyVars tyvars
; wanteds <- newDictBndrsO orig (substTheta tenv theta)
; (irreds, _) <- tryHardCheckLoop doc wanteds
- ; let (tv_dicts, others) = partition isTyVarDict irreds
+ ; let (tv_dicts, others) = partition ok irreds
; addNoInstanceErrs others
+ -- See Note [Exotic derived instance contexts] in TcMType
; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
simpl_theta = substTheta rev_env (map dictPred tv_dicts)
; return simpl_theta }
where
doc = ptext SLIT("deriving classes for a data type")
-\end{code}
-
-Note [Exotic derived instance contexts]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
- data T a b c = MkT (Foo a b c) deriving( Eq )
- instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
-
-Notice that this instance (just) satisfies the Paterson termination
-conditions. Then we *could* derive an instance decl like this:
-
- instance (C Int a, Eq b, Eq c) => Eq (T a b c)
-even though there is no instance for (C Int a), because there just
-*might* be an instance for, say, (C Int Bool) at a site where we
-need the equality instance for T's.
-
-However, this seems pretty exotic, and it's quite tricky to allow
-this, and yet give sensible error messages in the (much more common)
-case where we really want that instance decl for C.
-
-So for now we simply require that the derived instance context
-should have only type-variable constraints.
-
-Here is another example:
- data Fix f = In (f (Fix f)) deriving( Eq )
-Here, if we are prepared to allow -fallow-undecidable-instances we
-could derive the instance
- instance Eq (f (Fix f)) => Eq (Fix f)
-but this is so delicate that I don't think it should happen inside
-'deriving'. If you want this, write it yourself!
-
-NB: if you want to lift this condition, make sure you still meet the
-termination conditions! If not, the deriving mechanism generates
-larger and larger constraints. Example:
- data Succ a = S a
- data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
-
-Note the lack of a Show instance for Succ. First we'll generate
- instance (Show (Succ a), Show a) => Show (Seq a)
-and then
- instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
-and so on. Instead we want to complain of no instance for (Show (Succ a)).
+ ok dict | isDict dict = validDerivPred (dictPred dict)
+ | otherwise = False
+\end{code}
@tcSimplifyDefault@ just checks class-type constraints, essentially;
; mapM_ complain_implic implics
; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
; groupErrs complain_no_inst insts3
- ; mapM_ complain_eq eqInsts
+ ; mapM_ eqInstMisMatch eqInsts
}
where
complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
(Just (tci_loc inst, tci_given inst))
(tci_wanted inst)
- complain_eq EqInst {tci_left = lty, tci_right = rty,
- tci_loc = InstLoc _ _ ctxt}
- = do { (env, msg) <- misMatchMsg lty rty
- ; setErrCtxt ctxt $
- failWithTcM (env, msg)
- }
-
check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
-- Right msg => overlap message
-- Left inst => no instance
nest 4 (pprStack stack)]
pprStack stack = vcat (map pprInstInFull stack)
-
------------------------
-misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
--- Generate the message when two types fail to match,
--- going to some trouble to make it helpful.
--- The argument order is: actual type, expected type
-misMatchMsg ty_act ty_exp
- = do { env0 <- tcInitTidyEnv
- ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp ty_act
- ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act ty_exp
- ; return (env2,
- sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp,
- nest 7 $
- ptext SLIT("against inferred type") <+> pp_act],
- nest 2 (extra_exp $$ extra_act)]) }
-
-ppr_ty :: TidyEnv -> TcType -> TcType -> TcM (TidyEnv, SDoc, SDoc)
-ppr_ty env ty other_ty
- = do { ty' <- zonkTcType ty
- ; let (env1, tidy_ty) = tidyOpenType env ty'
- ; (env2, extra) <- ppr_extra env1 tidy_ty other_ty
- ; return (env2, quotes (ppr tidy_ty), extra) }
-
--- (ppr_extra env ty other_ty) shows extra info about 'ty'
-ppr_extra env (TyVarTy tv) other_ty
- | isSkolemTyVar tv || isSigTyVar tv
- = return (env1, pprSkolTvBinding tv1)
- where
- (env1, tv1) = tidySkolemTyVar env tv
-
-ppr_extra env (TyConApp tc1 _) (TyConApp tc2 _)
- | getOccName tc1 == getOccName tc2
- = -- This case helps with messages that would otherwise say
- -- Could not match 'T' does not match 'M.T'
- -- which is not helpful
- do { this_mod <- getModule
- ; return (env, quotes (ppr tc1) <+> ptext SLIT("is defined") <+> mk_mod this_mod) }
- where
- tc_mod = nameModule (getName tc1)
- tc_pkg = modulePackageId tc_mod
- tc2_pkg = modulePackageId (nameModule (getName tc2))
- mk_mod this_mod
- | tc_mod == this_mod = ptext SLIT("in this module")
-
- | not home_pkg && tc2_pkg /= tc_pkg = pp_pkg
- -- Suppress the module name if (a) it's from another package
- -- (b) other_ty isn't from that same package
-
- | otherwise = ptext SLIT("in module") <+> quotes (ppr tc_mod) <+> pp_pkg
- where
- home_pkg = tc_pkg == modulePackageId this_mod
- pp_pkg | home_pkg = empty
- | otherwise = ptext SLIT("in package") <+> quotes (ppr tc_pkg)
-
-ppr_extra env ty other_ty = return (env, empty) -- Normal case
\end{code}