X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=071d4c0334c3a0a661ba863e4c14033d11492621;hp=ee62c0e8b04e54ae38f08a18a3b69801ad12c603;hb=c04a5fe3e2867d59ce9757069fdd20c06c326724;hpb=fce61e356063836debcc579e336e99a65d61284e diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index ee62c0e..071d4c0 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -6,13 +6,6 @@ TcSimplify \begin{code} -{-# OPTIONS -w #-} --- The above warning supression flag is a temporary kludge. --- While working on this module you are encouraged to remove it and fix --- any warnings in the module. See --- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings --- for details - module TcSimplify ( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyCheck, tcSimplifyRestricted, @@ -23,6 +16,8 @@ module TcSimplify ( tcSimplifyDeriv, tcSimplifyDefault, bindInstsOfLocalFuns, + + tcSimplifyStagedExpr, misMatchMsg ) where @@ -33,6 +28,7 @@ import {-# SOURCE #-} TcUnify( unifyType ) import HsSyn import TcRnMonad +import TcHsSyn ( hsLPatType ) import Inst import TcEnv import InstEnv @@ -40,8 +36,9 @@ import TcType import TcMType import TcIface import TcTyFuns -import TypeRep +import DsUtils -- Big-tuple functions import Var +import Id import Name import NameSet import Class @@ -54,14 +51,12 @@ import ErrUtils import BasicTypes import VarSet import VarEnv -import Module import FiniteMap import Bag import Outputable import Maybes import ListSetOps import Util -import UniqSet import SrcLoc import DynFlags import FastString @@ -99,34 +94,36 @@ we reduce the (C a b1) constraint from the call of f to (D a b1). Here is a more complicated example: -| > class Foo a b | a->b -| > -| > class Bar a b | a->b -| > -| > data Obj = Obj -| > -| > instance Bar Obj Obj -| > -| > instance (Bar a b) => Foo a b -| > -| > foo:: (Foo a b) => a -> String -| > foo _ = "works" -| > -| > runFoo:: (forall a b. (Foo a b) => a -> w) -> w -| > runFoo f = f Obj -| -| *Test> runFoo foo -| -| :1: -| Could not deduce (Bar a b) from the context (Foo a b) -| arising from use of `foo' at :1 -| Probable fix: -| Add (Bar a b) to the expected type of an expression -| In the first argument of `runFoo', namely `foo' -| In the definition of `it': it = runFoo foo -| -| Why all of the sudden does GHC need the constraint Bar a b? The -| function foo didn't ask for that... +@ + > class Foo a b | a->b + > + > class Bar a b | a->b + > + > data Obj = Obj + > + > instance Bar Obj Obj + > + > instance (Bar a b) => Foo a b + > + > foo:: (Foo a b) => a -> String + > foo _ = "works" + > + > runFoo:: (forall a b. (Foo a b) => a -> w) -> w + > runFoo f = f Obj + + *Test> runFoo foo + + :1: + Could not deduce (Bar a b) from the context (Foo a b) + arising from use of `foo' at :1 + Probable fix: + Add (Bar a b) to the expected type of an expression + In the first argument of `runFoo', namely `foo' + In the definition of `it': it = runFoo foo + + Why all of the sudden does GHC need the constraint Bar a b? The + function foo didn't ask for that... +@ The trouble is that to type (runFoo foo), GHC has to solve the problem: @@ -867,7 +864,7 @@ Note [NO TYVARS] The excitement comes when simplifying the bindings for h. Initially try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}. -From this we get t1:=:t2, but also various bindings. We can't forget +From this we get t1~t2, but also various bindings. We can't forget the bindings (because of [LOOP]), but in fact t1 is what g is polymorphic in. @@ -889,7 +886,9 @@ isFreeWhenChecking qtvs ips inst && isFreeWrtIPs ips inst -} +isFreeWrtTyVars :: VarSet -> Inst -> Bool isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs +isFreeWrtIPs :: NameSet -> Inst -> Bool isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst)) \end{code} @@ -975,17 +974,17 @@ makeImplicationBind :: InstLoc -> [TcTyVar] -> [Inst] -> [Inst] -> TcM ([Inst], TcDictBinds) -- Make a binding that binds 'irreds', by generating an implication --- constraint for them, *and* throwing the constraint into the LIE +-- constraint for them. +-- -- The binding looks like -- (ir1, .., irn) = f qtvs givens -- where f is (evidence for) the new implication constraint --- f :: forall qtvs. {reft} givens => (ir1, .., irn) +-- f :: forall qtvs. givens => (ir1, .., irn) -- qtvs includes coercion variables -- -- This binding must line up the 'rhs' in reduceImplication makeImplicationBind loc all_tvs - givens -- Guaranteed all Dicts - -- or EqInsts + givens -- Guaranteed all Dicts or EqInsts irreds | null irreds -- If there are no irreds, we are done = return ([], emptyBag) @@ -993,30 +992,38 @@ makeImplicationBind loc all_tvs = do { uniq <- newUnique ; span <- getSrcSpanM ; let (eq_givens, dict_givens) = partition isEqInst givens - eq_tyvar_cos = mkTyVarTys (varSetElems $ tyVarsOfTypes $ map eqInstType eq_givens) - -- Urgh! See line 2187 or thereabouts. I believe that all these - -- 'givens' must be a simple CoVar. This MUST be cleaned up. - ; let name = mkInternalName uniq (mkVarOcc "ic") span + -- extract equality binders + eq_cotvs = map eqInstType eq_givens + + -- make the implication constraint instance + name = mkInternalName uniq (mkVarOcc "ic") span implic_inst = ImplicInst { tci_name = name, tci_tyvars = all_tvs, - tci_given = (eq_givens ++ dict_givens), - tci_wanted = irreds, tci_loc = loc } - ; let -- only create binder for dict_irreds - (eq_irreds, dict_irreds) = partition isEqInst irreds - n_dict_irreds = length dict_irreds + tci_given = eq_givens ++ dict_givens, + -- same order as binders + tci_wanted = irreds, + tci_loc = loc } + + -- create binders for the irreducible dictionaries + dict_irreds = filter (not . isEqInst) irreds dict_irred_ids = map instToId dict_irreds - tup_ty = mkTupleTy Boxed n_dict_irreds (map idType dict_irred_ids) - pat = TuplePat (map nlVarPat dict_irred_ids) Boxed tup_ty - rhs = L span (mkHsWrap co (HsVar (instToId implic_inst))) - co = mkWpApps (map instToId dict_givens) - <.> mkWpTyApps eq_tyvar_cos - <.> mkWpTyApps (mkTyVarTys all_tvs) - bind | [dict_irred_id] <- dict_irred_ids = VarBind dict_irred_id rhs - | otherwise = PatBind { pat_lhs = L span pat, - pat_rhs = unguardedGRHSs rhs, - pat_rhs_ty = tup_ty, - bind_fvs = placeHolderNames } + lpat = mkBigLHsPatTup (map (L span . VarPat) dict_irred_ids) + + -- create the binding + rhs = L span (mkHsWrap co (HsVar (instToId implic_inst))) + co = mkWpApps (map instToId dict_givens) + <.> mkWpTyApps eq_cotvs + <.> mkWpTyApps (mkTyVarTys all_tvs) + bind | [dict_irred_id] <- dict_irred_ids + = VarBind dict_irred_id rhs + | otherwise + = PatBind { pat_lhs = lpat + , pat_rhs = unguardedGRHSs rhs + , pat_rhs_ty = hsLPatType lpat + , bind_fvs = placeHolderNames + } + ; traceTc $ text "makeImplicationBind" <+> ppr implic_inst ; return ([implic_inst], unitBag (L span bind)) } @@ -1027,11 +1034,11 @@ tryHardCheckLoop :: SDoc -> TcM ([Inst], TcDictBinds) tryHardCheckLoop doc wanteds - = do { (irreds,binds) <- checkLoop (mkRedEnv doc try_me []) wanteds + = do { (irreds,binds) <- checkLoop (mkInferRedEnv doc try_me) wanteds ; return (irreds,binds) } where - try_me inst = ReduceMe AddSCs + try_me _ = ReduceMe -- Here's the try-hard bit ----------------------------------------------------------- @@ -1047,7 +1054,7 @@ gentleCheckLoop inst_loc givens wanteds where env = mkRedEnv (pprInstLoc inst_loc) try_me givens - try_me inst | isMethodOrLit inst = ReduceMe AddSCs + try_me inst | isMethodOrLit inst = ReduceMe | otherwise = Stop -- When checking against a given signature -- we MUST be very gentle: Note [Check gently] @@ -1058,8 +1065,8 @@ gentleInferLoop doc wanteds = do { (irreds, binds) <- checkLoop env wanteds ; return (irreds, binds) } where - env = mkRedEnv doc try_me [] - try_me inst | isMethodOrLit inst = ReduceMe AddSCs + env = mkInferRedEnv doc try_me + try_me inst | isMethodOrLit inst = ReduceMe | otherwise = Stop \end{code} @@ -1096,18 +1103,16 @@ checkLoop :: RedEnv -- Postcondition: returned Insts are zonked checkLoop env wanteds - = go env wanteds (return ()) - where go env wanteds elim_skolems + = go env wanteds + where go env wanteds = do { -- We do need to zonk the givens; cf Note [Zonking RedEnv] ; env' <- zonkRedEnv env ; wanteds' <- zonkInsts wanteds - ; (improved, binds, irreds, elim_more_skolems) - <- reduceContext env' wanteds' - ; let elim_skolems' = elim_skolems >> elim_more_skolems + ; (improved, binds, irreds) <- reduceContext env' wanteds' - ; if not improved then - elim_skolems' >> return (irreds, binds) + ; if null irreds || not improved then + return (irreds, binds) else do -- If improvement did some unification, we go round again. @@ -1116,7 +1121,7 @@ checkLoop env wanteds -- variable which might have been unified, so we'd get an -- infinite loop if we started again with wanteds! -- See Note [LOOP] - { (irreds1, binds1) <- go env' irreds elim_skolems' + { (irreds1, binds1) <- go env' irreds ; return (irreds1, binds `unionBags` binds1) } } \end{code} @@ -1209,30 +1214,104 @@ Alas! Alack! We can do the same for (instance D Int): ds2 = $p1 dc And now we've defined the superclass in terms of itself. - -Solution: never generate a superclass selectors at all when -satisfying the superclass context of an instance declaration. - Two more nasty cases are in tcrun021 tcrun033 +Solution: + - Satisfy the superclass context *all by itself* + (tcSimplifySuperClasses) + - And do so completely; i.e. no left-over constraints + to mix with the constraints arising from method declarations + + +Note [Recursive instances and superclases] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider this code, which arises in the context of "Scrap Your +Boilerplate with Class". + + class Sat a + class Data ctx a + instance Sat (ctx Char) => Data ctx Char + instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] + + class Data Maybe a => Foo a + + instance Foo t => Sat (Maybe t) + + instance Data Maybe a => Foo a + instance Foo a => Foo [a] + instance Foo [Char] + +In the instance for Foo [a], when generating evidence for the superclasses +(ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]). +Using the instance for Data, we therefore need + (Sat (Maybe [a], Data Maybe a) +But we are given (Foo a), and hence its superclass (Data Maybe a). +So that leaves (Sat (Maybe [a])). Using the instance for Sat means +we need (Foo [a]). And that is the very dictionary we are bulding +an instance for! So we must put that in the "givens". So in this +case we have + Given: Foo a, Foo [a] + Watend: Data Maybe [a] + +BUT we must *not not not* put the *superclasses* of (Foo [a]) in +the givens, which is what 'addGiven' would normally do. Why? Because +(Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted +by selecting a superclass from Foo [a], which simply makes a loop. + +On the other hand we *must* put the superclasses of (Foo a) in +the givens, as you can see from the derivation described above. + +Conclusion: in the very special case of tcSimplifySuperClasses +we have one 'given' (namely the "this" dictionary) whose superclasses +must not be added to 'givens' by addGiven. + +There is a complication though. Suppose there are equalities + instance (Eq a, a~b) => Num (a,b) +Then we normalise the 'givens' wrt the equalities, so the original +given "this" dictionary is cast to one of a different type. So it's a +bit trickier than before to identify the "special" dictionary whose +superclasses must not be added. See test + indexed-types/should_run/EqInInstance + +We need a persistent property of the dictionary to record this +special-ness. Current I'm using the InstLocOrigin (a bit of a hack, +but cool), which is maintained by dictionary normalisation. +Specifically, the InstLocOrigin is + NoScOrigin +then the no-superclass thing kicks in. WATCH OUT if you fiddle +with InstLocOrigin! + \begin{code} -tcSimplifySuperClasses +tcSimplifySuperClasses :: InstLoc + -> Inst -- The dict whose superclasses + -- are being figured out -> [Inst] -- Given -> [Inst] -- Wanted -> TcM TcDictBinds -tcSimplifySuperClasses loc givens sc_wanteds +tcSimplifySuperClasses loc this givens sc_wanteds = do { traceTc (text "tcSimplifySuperClasses") + + -- Note [Recursive instances and superclases] + ; no_sc_loc <- getInstLoc NoScOrigin + ; let no_sc_this = setInstLoc this no_sc_loc + + ; let env = RedEnv { red_doc = pprInstLoc loc, + red_try_me = try_me, + red_givens = no_sc_this : givens, + red_stack = (0,[]), + red_improve = False } -- No unification vars + + ; (irreds,binds1) <- checkLoop env sc_wanteds ; let (tidy_env, tidy_irreds) = tidyInsts irreds - ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds + ; reportNoInstances tidy_env (Just (loc, givens)) [] tidy_irreds ; return binds1 } where - env = mkRedEnv (pprInstLoc loc) try_me givens - try_me inst = ReduceMe NoSCs - -- Like tryHardCheckLoop, but with NoSCs + try_me _ = ReduceMe -- Try hard, so we completely solve the superclass + -- constraints right here. See Note [SUPERCLASS-LOOP 1] \end{code} @@ -1353,7 +1432,7 @@ tcSimplifyRestricted -- Used for restricted binding groups tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- Zonk everything in sight = do { traceTc (text "tcSimplifyRestricted") - ; wanteds' <- zonkInsts wanteds + ; wanteds_z <- zonkInsts wanteds -- 'ReduceMe': Reduce as far as we can. Don't stop at -- dicts; the idea is to get rid of as many type @@ -1364,10 +1443,8 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- BUT do no improvement! See Plan D above -- HOWEVER, some unification may take place, if we instantiate -- a method Inst with an equality constraint - ; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs) - ; (_imp, _binds, constrained_dicts, elim_skolems) - <- reduceContext env wanteds' - ; elim_skolems + ; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe) + ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds_z -- Next, figure out the tyvars we will quantify over ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs) @@ -1395,6 +1472,13 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds ppr _binds, ppr constrained_tvs', ppr tau_tvs', ppr qtvs ]) + -- Zonk wanteds again! The first call to reduceContext may have + -- instantiated some variables. + -- FIXME: If red_improve would work, we could propagate that into + -- the equality solver, too, to prevent instantating any + -- variables. + ; wanteds_zz <- zonkInsts wanteds_z + -- The first step may have squashed more methods than -- necessary, so try again, this time more gently, knowing the exact -- set of type variables to quantify over. @@ -1414,10 +1498,9 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds ; let is_nested_group = isNotTopLevel top_lvl try_me inst | isFreeWrtTyVars qtvs inst, (is_nested_group || isDict inst) = Stop - | otherwise = ReduceMe AddSCs + | otherwise = ReduceMe env = mkNoImproveRedEnv doc try_me - ; (_imp, binds, irreds, elim_skolems) <- reduceContext env wanteds' - ; elim_skolems + ; (_imp, binds, irreds) <- reduceContext env wanteds_zz -- See "Notes on implicit parameters, Question 4: top level" ; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured @@ -1490,27 +1573,55 @@ Instead we want to quantify over the dictionaries separately. In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving all dicts unchanged, with absolutely no sharing. It's simpler to do this -from scratch, rather than further parameterise simpleReduceLoop etc +from scratch, rather than further parameterise simpleReduceLoop etc. +Simpler, maybe, but alas not simple (see Trac #2494) + +* Type errors may give rise to an (unsatisfiable) equality constraint + +* Applications of a higher-rank function on the LHS may give + rise to an implication constraint, esp if there are unsatisfiable + equality constraints inside. \begin{code} tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds) tcSimplifyRuleLhs wanteds - = go [] emptyBag wanteds + = do { wanteds' <- zonkInsts wanteds + ; (irreds, binds) <- go [] emptyBag wanteds' + ; let (dicts, bad_irreds) = partition isDict irreds + ; traceTc (text "tcSimplifyrulelhs" <+> pprInsts bad_irreds) + ; addNoInstanceErrs (nub bad_irreds) + -- The nub removes duplicates, which has + -- not happened otherwise (see notes above) + ; return (dicts, binds) } where - go dicts binds [] - = return (dicts, binds) - go dicts binds (w:ws) + go :: [Inst] -> TcDictBinds -> [Inst] -> TcM ([Inst], TcDictBinds) + go irreds binds [] + = return (irreds, binds) + go irreds binds (w:ws) | isDict w - = go (w:dicts) binds ws + = go (w:irreds) binds ws + | isImplicInst w -- Have a go at reducing the implication + = do { (binds1, irreds1) <- reduceImplication red_env w + ; let (bad_irreds, ok_irreds) = partition isImplicInst irreds1 + ; go (bad_irreds ++ irreds) + (binds `unionBags` binds1) + (ok_irreds ++ ws)} | otherwise = do { w' <- zonkInst w -- So that (3::Int) does not generate a call -- to fromInteger; this looks fragile to me ; lookup_result <- lookupSimpleInst w' ; case lookup_result of - GenInst ws' rhs -> - go dicts (addInstToDictBind binds w rhs) (ws' ++ ws) - NoInstance -> pprPanic "tcSimplifyRuleLhs" (ppr w) + NoInstance -> go (w:irreds) binds ws + GenInst ws' rhs -> go irreds binds' (ws' ++ ws) + where + binds' = addInstToDictBind binds w rhs } + + -- Sigh: we need to reduce inside implications + red_env = mkInferRedEnv doc try_me + doc = ptext (sLit "Implication constraint in RULE lhs") + try_me inst | isMethodOrLit inst = ReduceMe + | otherwise = Stop -- Be gentle \end{code} tcSimplifyBracket is used when simplifying the constraints arising from @@ -1566,15 +1677,22 @@ tcSimplifyIPs given_ips wanteds -- Unusually for checking, we *must* zonk the given_ips ; let env = mkRedEnv doc try_me given_ips' - ; (improved, binds, irreds, elim_skolems) <- reduceContext env wanteds' - ; elim_skolems + ; (improved, binds, irreds) <- reduceContext env wanteds' - ; if not improved then + ; if null irreds || not improved then ASSERT( all is_free irreds ) do { extendLIEs irreds ; return binds } - else - tcSimplifyIPs given_ips wanteds } + else do + -- If improvement did some unification, we go round again. + -- We start again with irreds, not wanteds + -- 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] + { binds1 <- tcSimplifyIPs given_ips' irreds + ; return $ binds `unionBags` binds1 + } } where doc = text "tcSimplifyIPs" <+> ppr given_ips ip_set = mkNameSet (ipNamesOfInsts given_ips) @@ -1582,7 +1700,7 @@ tcSimplifyIPs given_ips wanteds -- Simplify any methods that mention the implicit parameter try_me inst | is_free inst = Stop - | otherwise = ReduceMe NoSCs + | otherwise = ReduceMe \end{code} @@ -1657,8 +1775,9 @@ data RedEnv , red_try_me :: Inst -> WhatToDo , red_improve :: Bool -- True <=> do improvement , red_givens :: [Inst] -- All guaranteed rigid - -- Always dicts + -- Always dicts & equalities -- but see Note [Rigidity] + , red_stack :: (Int, [Inst]) -- Recursion stack (for err msg) -- See Note [RedStack] } @@ -1684,6 +1803,14 @@ mkRedEnv doc try_me givens red_stack = (0,[]), red_improve = True } +mkInferRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv +-- No givens at all +mkInferRedEnv doc try_me + = RedEnv { red_doc = doc, red_try_me = try_me, + red_givens = [], + red_stack = (0,[]), + red_improve = True } + mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv -- Do not do improvement; no givens mkNoImproveRedEnv doc try_me @@ -1693,11 +1820,11 @@ mkNoImproveRedEnv doc try_me red_improve = True } data WhatToDo - = ReduceMe WantSCs -- Try to reduce this - -- If there's no instance, add the inst to the - -- irreductible ones, but don't produce an error - -- message of any kind. - -- It might be quite legitimate such as (Eq a)! + = ReduceMe -- Try to reduce this + -- If there's no instance, add the inst to the + -- irreductible ones, but don't produce an error + -- message of any kind. + -- It might be quite legitimate such as (Eq a)! | Stop -- Return as irreducible unless it can -- be reduced to a constant in one step @@ -1740,110 +1867,102 @@ reduceContext :: RedEnv -> [Inst] -- Wanted -> TcM (ImprovementDone, TcDictBinds, -- Dictionary bindings - [Inst], -- Irreducible - TcM ()) -- Undo skolems from SkolemOccurs + [Inst]) -- Irreducible -reduceContext env wanteds +reduceContext env wanteds0 = do { traceTc (text "reduceContext" <+> (vcat [ text "----------------------", red_doc env, text "given" <+> ppr (red_givens env), - text "wanted" <+> ppr wanteds, + text "wanted" <+> ppr wanteds0, text "----------------------" ])) - - ; let givens = red_givens env - (given_eqs0, given_dicts0) = partition isEqInst givens - (wanted_eqs0, wanted_non_eqs) = partition isEqInst wanteds - (wanted_implics0, wanted_dicts) = partition isImplicInst wanted_non_eqs - -- 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 + ; ancestor_eqs <- ancestorEqualities wanteds0 ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs - -- 1. Normalise the *given* *equality* constraints - ; (given_eqs, eliminate_skolems) <- normaliseGivenEqs given_eqs0 - - -- 2. Normalise the *given* *dictionary* constraints - -- wrt. the toplevel and given equations - ; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs - given_dicts0 - - -- 5. Build the Avail mapping from "given_dicts" - ; (init_state, extra_givens) <- getLIE $ do - { init_state <- foldlM addGiven emptyAvails given_dicts + -- Normalise and solve all equality constraints as far as possible + -- and normalise all dictionary constraints wrt to the reduced + -- equalities. The returned wanted constraints include the + -- irreducible wanted equalities. + ; let wanteds = wanteds0 ++ ancestor_eqs + givens = red_givens env + ; (givens', + wanteds', + normalise_binds, + eq_improved) <- tcReduceEqs givens wanteds + ; traceTc $ text "reduceContext: tcReduceEqs result" <+> vcat + [ppr givens', ppr wanteds', ppr normalise_binds] + + -- Build the Avail mapping from "given_dicts" + ; (init_state, _) <- getLIE $ do + { init_state <- foldlM addGiven emptyAvails givens' ; return init_state } - -- *** ToDo: what to do with the "extra_givens"? For the - -- moment I'm simply discarding them, which is probably wrong - - -- 6. Solve the *wanted* *dictionary* constraints (not implications) - -- This may expose some further equational constraints... + -- Solve the *wanted* *dictionary* constraints (not implications) + -- This may expose some further equational constraints in the course + -- of improvement due to functional dependencies if any of the + -- involved unifications gets deferred. + ; let (wanted_implics, wanted_dicts) = partition isImplicInst wanteds' ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state) - ; (dict_binds, bound_dicts, dict_irreds) - <- extractResults avails wanted_dicts - ; traceTc $ text "reduceContext extractresults" <+> vcat + -- The getLIE is reqd because reduceList does improvement + -- (via extendAvails) which may in turn do unification + ; (dict_binds, + bound_dicts, + dict_irreds) <- extractResults avails wanted_dicts + ; traceTc $ text "reduceContext: extractResults" <+> vcat [ppr avails, ppr wanted_dicts, ppr dict_binds] -- Solve the wanted *implications*. In doing so, we can provide -- as "given" all the dicts that were originally given, -- *or* for which we now have bindings, -- *or* which are now irreds - ; let implic_env = env { red_givens = givens ++ bound_dicts - ++ dict_irreds } + -- NB: Equality irreds need to be converted, as the recursive + -- invocation of the solver will still treat them as wanteds + -- otherwise. + ; let implic_env = env { red_givens + = givens ++ bound_dicts ++ + map wantedToLocalEqInst dict_irreds } ; (implic_binds_s, implic_irreds_s) - <- mapAndUnzipM (reduceImplication implic_env) wanted_implics0 + <- mapAndUnzipM (reduceImplication implic_env) wanted_implics ; let implic_binds = unionManyBags implic_binds_s implic_irreds = concat implic_irreds_s - -- Normalise the wanted equality constraints - ; eq_irreds <- normaliseWantedEqs given_eqs (wanted_eqs ++ extra_eqs) - - -- Normalise the wanted dictionaries - ; let irreds = dict_irreds ++ implic_irreds - eqs = eq_irreds ++ given_eqs - ; (norm_irreds, normalise_binds) <- normaliseWantedDicts eqs irreds - - -- Figure out whether we should go round again. We do so in either - -- two cases: - -- (1) If any of the mutable tyvars in givens or irreds has been - -- filled in by improvement, there is merit in going around - -- again, because we may make further progress. - -- (2) If we managed to normalise any dicts, there is merit in going - -- around gain, because reduceList may be able to get further. - -- - -- ToDo: We may have exposed new - -- equality constraints and should probably go round again - -- then as well. But currently we are dropping them on the - -- floor anyway. - - ; let all_irreds = norm_irreds ++ eq_irreds - ; improvedMetaTy <- anyM isFilledMetaTyVar $ varSetElems $ - tyVarsOfInsts (givens ++ all_irreds) - ; let improvedDicts = not $ isEmptyBag normalise_binds - improved = improvedMetaTy || improvedDicts - - -- The old plan (fragile) - -- improveed = availsImproved avails - -- || (not $ isEmptyBag normalise_binds1) - -- || (not $ isEmptyBag normalise_binds2) - -- || (any isEqInst irreds) + -- Collect all irreducible instances, and determine whether we should + -- go round again. We do so in either of two cases: + -- (1) If dictionary reduction or equality solving led to + -- improvement (i.e., instantiated type variables). + -- (2) If we reduced dictionaries (i.e., got dictionary bindings), + -- they may have exposed further opportunities to normalise + -- family applications. See Note [Dictionary Improvement] + -- + -- NB: We do *not* go around for new extra_eqs. Morally, we should, + -- but we can't without risking non-termination (see #2688). By + -- not going around, we miss some legal programs mixing FDs and + -- TFs, but we never claimed to support such programs in the + -- current implementation anyway. + + ; let all_irreds = dict_irreds ++ implic_irreds ++ extra_eqs + avails_improved = availsImproved avails + improvedFlexible = avails_improved || eq_improved + reduced_dicts = not (isEmptyBag dict_binds) + improved = improvedFlexible || reduced_dicts + -- + improvedHint = (if avails_improved then " [AVAILS]" else "") ++ + (if eq_improved then " [EQ]" else "") ; traceTc (text "reduceContext end" <+> (vcat [ text "----------------------", red_doc env, text "given" <+> ppr givens, - text "given_eqs" <+> ppr given_eqs, - text "wanted" <+> ppr wanteds, - text "wanted_dicts" <+> ppr wanted_dicts, + text "wanted" <+> ppr wanteds0, text "----", text "avails" <+> pprAvails avails, - text "improved =" <+> ppr improved, + text "improved =" <+> ppr improved <+> text improvedHint, text "(all) irreds = " <+> ppr all_irreds, text "dict-binds = " <+> ppr dict_binds, text "implic-binds = " <+> ppr implic_binds, @@ -1851,11 +1970,9 @@ reduceContext env wanteds ])) ; return (improved, - given_binds `unionBags` normalise_binds - `unionBags` dict_binds - `unionBags` implic_binds, - all_irreds, - eliminate_skolems) + normalise_binds `unionBags` dict_binds + `unionBags` implic_binds, + all_irreds) } tcImproveOne :: Avails -> Inst -> TcM ImprovementDone @@ -1870,36 +1987,88 @@ tcImproveOne avails inst -- Avails has all the superclasses etc (good) -- It also has all the intermediates of the deduction (good) -- It does not have duplicates (good) - -- NB that (?x::t1) and (?x::t2) will be held separately in avails - -- so that improve will see them separate + -- NB that (?x::t1) and (?x::t2) will be held separately in + -- avails so that improve will see them separate ; traceTc (text "improveOne" <+> ppr inst) ; unifyEqns eqns } -unifyEqns :: [(Equation,(PredType,SDoc),(PredType,SDoc))] +unifyEqns :: [(Equation, (PredType, SDoc), (PredType, SDoc))] -> TcM ImprovementDone unifyEqns [] = return False unifyEqns eqns = do { traceTc (ptext (sLit "Improve:") <+> vcat (map pprEquationDoc eqns)) - ; mapM_ unify eqns - ; return True } + ; improved <- mapM unify eqns + ; return $ or improved + } where unify ((qtvs, pairs), what1, what2) - = addErrCtxtM (mkEqnMsg what1 what2) $ do - (_, _, tenv) <- tcInstTyVars (varSetElems qtvs) - mapM_ (unif_pr tenv) pairs - unif_pr tenv (ty1,ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2) + = addErrCtxtM (mkEqnMsg what1 what2) $ + do { let freeTyVars = unionVarSets (map tvs_pr pairs) + `minusVarSet` qtvs + ; (_, _, tenv) <- tcInstTyVars (varSetElems qtvs) + ; mapM_ (unif_pr tenv) pairs + ; anyM isFilledMetaTyVar $ varSetElems freeTyVars + } + + unif_pr tenv (ty1, ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2) -pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)] + tvs_pr (ty1, ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2 +pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc +pprEquationDoc (eqn, (p1, _), (p2, _)) + = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)] + +mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv + -> TcM (TidyEnv, SDoc) mkEqnMsg (pred1,from1) (pred2,from2) tidy_env - = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2 - ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' } + = do { pred1' <- zonkTcPredType pred1 + ; pred2' <- zonkTcPredType pred2 + ; let { pred1'' = tidyPred tidy_env pred1' + ; pred2'' = tidyPred tidy_env pred2' } ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"), nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])] ; return (tidy_env, msg) } \end{code} +Note [Dictionary Improvement] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In reduceContext, we first reduce equalities and then class constraints. +However, the letter may expose further opportunities for the former. Hence, +we need to go around again if dictionary reduction produced any dictionary +bindings. The following example demonstrated the point: + + data EX _x _y (p :: * -> *) + data ANY + + class Base p + + class Base (Def p) => Prop p where + type Def p + + instance Base () + instance Prop () where + type Def () = () + + instance (Base (Def (p ANY))) => Base (EX _x _y p) + instance (Prop (p ANY)) => Prop (EX _x _y p) where + type Def (EX _x _y p) = EX _x _y p + + data FOO x + instance Prop (FOO x) where + type Def (FOO x) = () + + data BAR + instance Prop BAR where + type Def BAR = EX () () FOO + +During checking the last instance declaration, we need to check the superclass +cosntraint Base (Def BAR), which family normalisation reduced to +Base (EX () () FOO). Chasing the instance for Base (EX _x _y p), gives us +Base (Def (FOO ANY)), which again requires family normalisation of Def to +Base () before we can finish. + + The main context-reduction function is @reduce@. Here's its game plan. \begin{code} @@ -1920,9 +2089,16 @@ reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state ; go ws state' } -- Base case: we're done! +reduce :: RedEnv -> Inst -> Avails -> TcM Avails reduce env wanted avails + + -- We don't reduce equalities here (and they must not end up as irreds + -- in the Avails!) + | isEqInst wanted + = return avails + -- It's the same as an existing inst, or a superclass thereof - | Just avail <- findAvail avails wanted + | Just _ <- findAvail avails wanted = do { traceTc (text "reduce: found " <+> ppr wanted) ; return avails } @@ -1933,18 +2109,18 @@ reduce env wanted avails Stop -> try_simple (addIrred NoSCs); -- See Note [No superclasses for Stop] - ReduceMe want_scs -> do -- It should be reduced + ReduceMe -> do -- It should be reduced { (avails, lookup_result) <- reduceInst env avails wanted ; case lookup_result of - NoInstance -> addIrred want_scs avails wanted + NoInstance -> addIrred AddSCs avails wanted -- Add it and its superclasses - GenInst [] rhs -> addWanted want_scs avails wanted rhs [] + GenInst [] rhs -> addWanted AddSCs avails wanted rhs [] GenInst wanteds' rhs -> do { avails1 <- addIrred NoSCs avails wanted ; avails2 <- reduceList env wanteds' avails1 - ; addWanted want_scs avails2 wanted rhs wanteds' } } + ; addWanted AddSCs avails2 wanted rhs wanteds' } } -- Temporarily do addIrred *before* the reduceList, -- which has the effect of adding the thing we are trying -- to prove to the database before trying to prove the things it @@ -1962,14 +2138,50 @@ reduce env wanted avails = do { res <- lookupSimpleInst wanted ; case res of GenInst [] rhs -> addWanted AddSCs avails wanted rhs [] - other -> do_this_otherwise avails wanted } + _ -> do_this_otherwise avails wanted } \end{code} +Note [RECURSIVE DICTIONARIES] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + data D r = ZeroD | SuccD (r (D r)); + + instance (Eq (r (D r))) => Eq (D r) where + ZeroD == ZeroD = True + (SuccD a) == (SuccD b) = a == b + _ == _ = False; + + equalDC :: D [] -> D [] -> Bool; + equalDC = (==); + +We need to prove (Eq (D [])). Here's how we go: + + d1 : Eq (D []) + +by instance decl, holds if + d2 : Eq [D []] + where d1 = dfEqD d2 + +by instance decl of Eq, holds if + d3 : D [] + where d2 = dfEqList d3 + d1 = dfEqD d2 + +But now we can "tie the knot" to give + + d3 = d1 + d2 = dfEqList d3 + d1 = dfEqD d2 + +and it'll even run! The trick is to put the thing we are trying to prove +(in this case Eq (D []) into the database before trying to prove its +contributing clauses. + Note [SUPERCLASS-LOOP 2] ~~~~~~~~~~~~~~~~~~~~~~~~ -But the above isn't enough. Suppose we are *given* d1:Ord a, -and want to deduce (d2:C [a]) where +We need to be careful when adding "the constaint we are trying to prove". +Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where class Ord a => C a where instance Ord [a] => C [a] where ... @@ -2007,42 +2219,6 @@ Now we implement the Right Solution, which is to check for loops directly when adding superclasses. It's a bit like the occurs check in unification. -Note [RECURSIVE DICTIONARIES] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - data D r = ZeroD | SuccD (r (D r)); - - instance (Eq (r (D r))) => Eq (D r) where - ZeroD == ZeroD = True - (SuccD a) == (SuccD b) = a == b - _ == _ = False; - - equalDC :: D [] -> D [] -> Bool; - equalDC = (==); - -We need to prove (Eq (D [])). Here's how we go: - - d1 : Eq (D []) - -by instance decl, holds if - d2 : Eq [D []] - where d1 = dfEqD d2 - -by instance decl of Eq, holds if - d3 : D [] - where d2 = dfEqList d3 - d1 = dfEqD d2 - -But now we can "tie the knot" to give - - d3 = d1 - d2 = dfEqList d3 - d1 = dfEqD d2 - -and it'll even run! The trick is to put the thing we are trying to prove -(in this case Eq (D []) into the database before trying to prove its -contributing clauses. - %************************************************************************ %* * @@ -2053,7 +2229,7 @@ contributing clauses. \begin{code} --------------------------------------------- reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult) -reduceInst env avails other_inst +reduceInst _ avails other_inst = do { result <- lookupSimpleInst other_inst ; return (avails, result) } \end{code} @@ -2111,20 +2287,32 @@ Note that -- -- Note on coercion variables: -- - -- The extra given coercion variables are bound at two different sites: + -- The extra given coercion variables are bound at two different + -- sites: + -- -- -) in the creation context of the implication constraint -- the solved equational constraints use these binders -- -- -) at the solving site of the implication constraint - -- the solved dictionaries use these binders + -- the solved dictionaries use these binders; -- these binders are generated by reduceImplication -- + -- Note [Binders for equalities] + -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + -- To reuse the binders of local/given equalities in the binders of + -- implication constraints, it is crucial that these given equalities + -- always have the form + -- cotv :: t1 ~ t2 + -- where cotv is a simple coercion type variable (and not a more + -- complex coercion term). We require that the extra_givens always + -- have this form and exploit the special form when generating binders. reduceImplication env orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc, tci_tyvars = tvs, - tci_given = extra_givens, tci_wanted = wanteds }) + tci_given = extra_givens, tci_wanted = wanteds + }) = do { -- Solve the sub-problem - ; let try_me inst = ReduceMe AddSCs -- Note [Freeness and implications] + ; let try_me _ = ReduceMe -- Note [Freeness and implications] env' = env { red_givens = extra_givens ++ red_givens env , red_doc = sep [ptext (sLit "reduceImplication for") <+> ppr name, @@ -2136,13 +2324,6 @@ reduceImplication env [ ppr (red_givens env), ppr extra_givens, ppr wanteds]) ; (irreds, binds) <- checkLoop env' wanteds - ; let (extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens - -- SLPJ Sept 07: I think this is bogus; currently - -- there are no Eqinsts in extra_givens - dict_ids = map instToId extra_dict_givens - - -- Note [Reducing implication constraints] - -- Tom -- update note, put somewhere! ; traceTc (text "reduceImplication result" <+> vcat [ppr irreds, ppr binds]) @@ -2156,11 +2337,17 @@ reduceImplication env -- SLPJ Sept 07: what if improvement happened inside the checkLoop? -- Then we must iterate the outer loop too! - ; traceTc (text "reduceImplication condition" <+> ppr ((isEmptyLHsBinds binds) || (null irreds))) + ; didntSolveWantedEqs <- allM wantedEqInstIsUnsolved wanteds + -- we solve wanted eqs by side effect! --- Progress is no longer measered by the number of bindings - ; if (isEmptyLHsBinds binds) && (not $ null irreds) then -- No progress - -- If there are any irreds, we back off and do nothing + -- Progress is no longer measered by the number of bindings + -- If there are any irreds, but no bindings and no solved + -- equalities, we back off and do nothing + ; let backOff = isEmptyLHsBinds binds && -- no new bindings + (not $ null irreds) && -- but still some irreds + didntSolveWantedEqs -- no instantiated cotv + + ; if backOff then -- No progress return (emptyBag, [orig_implic]) else do { (simpler_implic_insts, bind) @@ -2170,36 +2357,39 @@ reduceImplication env -- case. After all, we only try hard to reduce at top level, or -- when inferring types. - ; let dict_wanteds = filter (not . isEqInst) wanteds - -- TOMDO: given equational constraints bug! - -- we need a different evidence for given - -- equations depending on whether we solve - -- dictionary constraints or equational constraints - - eq_tyvars = varSetElems $ tyVarsOfTypes $ map eqInstType extra_eq_givens - -- SLPJ Sept07: this looks Utterly Wrong to me, but I think - -- that current extra_givens has no EqInsts, so - -- it makes no difference - co = wrap_inline -- Note [Always inline implication constraints] - <.> mkWpTyLams tvs - <.> mkWpLams eq_tyvars - <.> mkWpLams dict_ids - <.> WpLet (binds `unionBags` bind) - wrap_inline | null dict_ids = idHsWrapper - | otherwise = WpInline - rhs = mkHsWrap co payload - loc = instLocSpan inst_loc - payload | [dict_wanted] <- dict_wanteds = HsVar (instToId dict_wanted) - | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) dict_wanteds) Boxed + ; let -- extract Id binders for dicts and CoTyVar binders for eqs; + -- see Note [Binders for equalities] + (extra_eq_givens, extra_dict_givens) = partition isEqInst + extra_givens + eq_cotvs = map instToVar extra_eq_givens + dict_ids = map instToId extra_dict_givens + + -- Note [Always inline implication constraints] + wrap_inline | null dict_ids = idHsWrapper + | otherwise = WpInline + co = wrap_inline + <.> mkWpTyLams tvs + <.> mkWpTyLams eq_cotvs + <.> mkWpLams dict_ids + <.> WpLet (binds `unionBags` bind) + rhs = mkLHsWrap co payload + loc = instLocSpan inst_loc + -- wanted equalities are solved by updating their + -- cotv; we don't generate bindings for them + dict_bndrs = map (L loc . HsVar . instToId) + . filter (not . isEqInst) + $ wanteds + payload = mkBigLHsTup dict_bndrs ; traceTc (vcat [text "reduceImplication" <+> ppr name, ppr simpler_implic_insts, text "->" <+> ppr rhs]) - ; return (unitBag (L loc (VarBind (instToId orig_implic) (L loc rhs))), + ; return (unitBag (L loc (VarBind (instToId orig_implic) rhs)), simpler_implic_insts) } } +reduceImplication _ i = pprPanic "reduceImplication" (ppr i) \end{code} Note [Always inline implication constraints] @@ -2237,12 +2427,29 @@ We can satisfy the (C Int) from the superclass of D, so we don't want to float the (C Int) out, even though it mentions no type variable in the constraints! +One more example: the constraint + class C a => D a b + instance (C a, E c) => E (a,c) + + constraint: forall b. D Int b => E (Int,c) + +You might think that the (D Int b) can't possibly contribute +to solving (E (Int,c)), since the latter mentions 'c'. But +in fact it can, because solving the (E (Int,c)) constraint needs +dictionaries + C Int, E c +and the (C Int) can be satisfied from the superclass of (D Int b). +So we must still not float (E (Int,c)) out. + +To think about: special cases for unary type classes? + 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. +But BE CAREFUL of the examples above in [Freeness and implications]. 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 @@ -2280,6 +2487,7 @@ data AvailHow instance Outputable Avails where ppr = pprAvails +pprAvails :: Avails -> SDoc pprAvails (Avails imp avails) = vcat [ ptext (sLit "Avails") <> (if imp then ptext (sLit "[improved]") else empty) , nest 2 $ braces $ @@ -2324,11 +2532,8 @@ extendAvails avails@(Avails imp env) inst avail availsInsts :: Avails -> [Inst] availsInsts (Avails _ avails) = keysFM avails +availsImproved :: Avails -> ImprovementDone availsImproved (Avails imp _) = imp - -updateImprovement :: Avails -> Avails -> Avails --- (updateImprovement a1 a2) sets a1's improvement flag from a2 -updateImprovement (Avails _ avails1) (Avails imp2 _) = Avails imp2 avails1 \end{code} Extracting the bindings from a bunch of Avails. @@ -2356,10 +2561,13 @@ extractResults (Avails _ avails) wanteds -> DoneEnv -- Has an entry for each inst in the above three sets -> [Inst] -- Wanted -> TcM (TcDictBinds, [Inst], [Inst]) - go binds bound_dicts irreds done [] + go binds bound_dicts irreds _ [] = return (binds, bound_dicts, irreds) go binds bound_dicts irreds done (w:ws) + | isEqInst w + = go binds bound_dicts (w:irreds) done' ws + | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w = if w_id `elem` done_ids then go binds bound_dicts irreds done ws @@ -2406,12 +2614,18 @@ addWanted want_scs avails wanted rhs_expr wanteds avail = Rhs rhs_expr wanteds addGiven :: Avails -> Inst -> TcM Avails -addGiven avails given = addAvailAndSCs AddSCs avails given (Given given) - -- Always add superclasses for 'givens' - -- - -- No ASSERT( not (given `elemAvails` avails) ) because in an instance - -- decl for Ord t we can add both Ord t and Eq t as 'givens', - -- so the assert isn't true +addGiven avails given + = addAvailAndSCs want_scs avails given (Given given) + where + want_scs = case instLocOrigin (instLoc given) of + NoScOrigin -> NoSCs + _other -> AddSCs + -- Conditionally add superclasses for 'given' + -- See Note [Recursive instances and superclases] + + -- No ASSERT( not (given `elemAvails` avails) ) because in an + -- instance decl for Ord t we can add both Ord t and Eq t as + -- 'givens', so the assert isn't true \end{code} \begin{code} @@ -2438,7 +2652,7 @@ addAvailAndSCs want_scs avails inst avail -- Watch out, though. Since the avails may contain loops -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids - findAllDeps so_far other = so_far + findAllDeps so_far _ = so_far find_all :: IdSet -> Inst -> IdSet find_all so_far kid @@ -2478,7 +2692,7 @@ addSCs is_loop avails dict 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 + _ -> False -- From the a set of insts obtain all equalities that (transitively) occur in -- superclass contexts of class constraints (aka the ancestor equalities). @@ -2542,6 +2756,7 @@ tcSimplifyInteractive wanteds -- The TcLclEnv should be valid here, solely to improve -- error message generation for the monomorphism restriction +tc_simplify_top :: SDoc -> Bool -> [Inst] -> TcM (Bag (LHsBind TcId)) tc_simplify_top doc interactive wanteds = do { dflags <- getDOpts ; wanteds <- zonkInsts wanteds @@ -2551,7 +2766,7 @@ tc_simplify_top doc interactive wanteds ; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds -- ; (irreds1, binds1) <- gentleInferLoop doc1 wanteds ; traceTc (text "tc_simplify_top 1: " <+> ppr irreds1) - ; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1 + ; (irreds2, binds2) <- approximateImplications doc2 (\_ -> True) irreds1 ; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2) -- Use the defaulting rules to do extra unification @@ -2658,7 +2873,7 @@ disambiguate doc interactive dflags insts | extended_defaulting = any isInteractiveClass clss | otherwise = all is_std_class clss && (any is_num_class clss) - -- In interactive mode, or with -fextended-default-rules, + -- In interactive mode, or with -XExtendedDefaultRules, -- we default Show a to Show () to avoid graututious errors on "show []" isInteractiveClass cls = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey]) @@ -2719,12 +2934,12 @@ getDefaultTys extended_deflts ovl_strings opt_deflt ovl_strings string_ty) } } } where opt_deflt True ty = [ty] - opt_deflt False ty = [] + opt_deflt False _ = [] \end{code} Note [Default unitTy] ~~~~~~~~~~~~~~~~~~~~~ -In interative mode (or with -fextended-default-rules) we add () as the first type we +In interative mode (or with -XExtendedDefaultRules) we add () as the first type we try when defaulting. This has very little real impact, except in the following case. Consider: Text.Printf.printf "hello" @@ -2781,7 +2996,8 @@ tcSimplifyDeriv orig tyvars theta ; (irreds, _) <- tryHardCheckLoop doc wanteds ; let (tv_dicts, others) = partition ok irreds - ; addNoInstanceErrs others + (tidy_env, tidy_insts) = tidyInsts others + ; reportNoInstances tidy_env Nothing [alt_fix] tidy_insts -- See Note [Exotic derived instance contexts] in TcMType ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars) @@ -2795,6 +3011,8 @@ tcSimplifyDeriv orig tyvars theta ok dict | isDict dict = validDerivPred (dictPred dict) | otherwise = False + alt_fix = vcat [ptext (sLit "use a standalone 'deriving instance' declaration instead,"), + ptext (sLit "so you can specify the instance context yourself")] \end{code} @@ -2809,7 +3027,7 @@ tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it tcSimplifyDefault theta = do wanteds <- newDictBndrsO DefaultOrigin theta (irreds, _) <- tryHardCheckLoop doc wanteds - addNoInstanceErrs irreds + addNoInstanceErrs irreds if null irreds then return () else @@ -2818,6 +3036,26 @@ tcSimplifyDefault theta = do doc = ptext (sLit "default declaration") \end{code} +@tcSimplifyStagedExpr@ performs a simplification but does so at a new +stage. This is used when typechecking annotations and splices. + +\begin{code} + +tcSimplifyStagedExpr :: ThStage -> TcM a -> TcM (a, TcDictBinds) +-- Type check an expression that runs at a top level stage as if +-- it were going to be spliced and then simplify it +tcSimplifyStagedExpr stage tc_action + = setStage stage $ do { + -- Typecheck the expression + (thing', lie) <- getLIE tc_action + + -- Solve the constraints + ; const_binds <- tcSimplifyTop lie + + ; return (thing', const_binds) } + +\end{code} + %************************************************************************ %* * @@ -2836,7 +3074,7 @@ groupErrs :: ([Inst] -> TcM ()) -- Deal with one group -- Group together insts with the same origin -- We want to report them together in error messages -groupErrs report_err [] +groupErrs _ [] = return () groupErrs report_err (inst:insts) = do { do_one (inst:friends) @@ -2856,7 +3094,7 @@ addInstLoc :: [Inst] -> Message -> Message addInstLoc insts msg = msg $$ nest 2 (pprInstArising (head insts)) addTopIPErrs :: [Name] -> [Inst] -> TcM () -addTopIPErrs bndrs [] +addTopIPErrs _ [] = return () addTopIPErrs bndrs ips = do { dflags <- getDOpts @@ -2885,7 +3123,7 @@ addNoInstanceErrs :: [Inst] -- Wanted (can include implications) -> TcM () addNoInstanceErrs insts = do { let (tidy_env, tidy_insts) = tidyInsts insts - ; reportNoInstances tidy_env Nothing tidy_insts } + ; reportNoInstances tidy_env Nothing [] tidy_insts } reportNoInstances :: TidyEnv @@ -2893,13 +3131,15 @@ reportNoInstances -- Nothing => top level -- Just (d,g) => d describes the construct -- with givens g + -> [SDoc] -- Alternative fix for no-such-instance -> [Inst] -- What is wanted (can include implications) -> TcM () -reportNoInstances tidy_env mb_what insts - = groupErrs (report_no_instances tidy_env mb_what) insts +reportNoInstances tidy_env mb_what alt_fix insts + = groupErrs (report_no_instances tidy_env mb_what alt_fix) insts -report_no_instances tidy_env mb_what insts +report_no_instances :: TidyEnv -> Maybe (InstLoc, [Inst]) -> [SDoc] -> [Inst] -> TcM () +report_no_instances tidy_env mb_what alt_fixes insts = do { inst_envs <- tcGetInstEnvs ; let (implics, insts1) = partition isImplicInst insts (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1 @@ -2917,7 +3157,7 @@ report_no_instances tidy_env mb_what insts complain_implic inst -- Recurse! = reportNoInstances tidy_env (Just (tci_loc inst, tci_given inst)) - (tci_wanted inst) + alt_fixes (tci_wanted inst) check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc -- Right msg => overlap message @@ -2930,7 +3170,7 @@ report_no_instances tidy_env mb_what insts -- The case of exactly one match and no unifiers means a -- successful lookup. That can't happen here, because dicts -- only end up here if they didn't match in Inst.lookupInst - ([m],[]) + ([_],[]) | debugIsOn -> pprPanic "reportNoInstance" (ppr wanted) res -> Right (mk_overlap_msg wanted res) where @@ -2949,7 +3189,7 @@ report_no_instances tidy_env mb_what insts ASSERT( not (null unifiers) ) parens (vcat [ptext (sLit "The choice depends on the instantiation of") <+> quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))), - ptext (sLit "To pick the first instance above, use -fallow-incoherent-instances"), + ptext (sLit "To pick the first instance above, use -XIncoherentInstances"), ptext (sLit "when compiling the other instance declarations")])] where ispecs = [ispec | (ispec, _) <- matches] @@ -2965,13 +3205,13 @@ report_no_instances tidy_env mb_what insts = vcat [ addInstLoc insts $ sep [ ptext (sLit "Could not deduce") <+> pprDictsTheta insts , nest 2 $ ptext (sLit "from the context") <+> pprDictsTheta givens] - , show_fixes (fix1 loc : fixes2) ] + , show_fixes (fix1 loc : fixes2 ++ alt_fixes) ] | otherwise -- Top level = vcat [ addInstLoc insts $ ptext (sLit "No instance") <> plural insts <+> ptext (sLit "for") <+> pprDictsTheta insts - , show_fixes fixes2 ] + , show_fixes (fixes2 ++ alt_fixes) ] where fix1 loc = sep [ ptext (sLit "add") <+> pprDictsTheta insts @@ -2992,6 +3232,7 @@ report_no_instances tidy_env mb_what insts show_fixes (f:fs) = sep [ptext (sLit "Possible fix:"), nest 2 (vcat (f : map (ptext (sLit "or") <+>) fs))] +addTopAmbigErrs :: [Inst] -> TcRn () addTopAmbigErrs dicts -- Divide into groups that share a common set of ambiguous tyvars = ifErrsM (return ()) $ -- Only report ambiguity if no other errors happened @@ -3047,10 +3288,11 @@ monomorphism_fix dflags = ptext (sLit "Probable fix:") <+> vcat [ptext (sLit "give these definition(s) an explicit type signature"), if dopt Opt_MonomorphismRestriction dflags - then ptext (sLit "or use -fno-monomorphism-restriction") - else empty] -- Only suggest adding "-fno-monomorphism-restriction" + then ptext (sLit "or use -XNoMonomorphismRestriction") + else empty] -- Only suggest adding "-XNoMonomorphismRestriction" -- if it is not already set! +warnDefault :: [(Inst, Class, Var)] -> Type -> TcM () warnDefault ups default_ty = do warn_flag <- doptM Opt_WarnTypeDefaults addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg) @@ -3063,10 +3305,12 @@ warnDefault ups default_ty = do quotes (ppr default_ty), pprDictsInFull tidy_dicts] +reduceDepthErr :: Int -> [Inst] -> SDoc 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"), nest 4 (pprStack stack)] +pprStack :: [Inst] -> SDoc pprStack stack = vcat (map pprInstInFull stack) \end{code}