X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=071d4c0334c3a0a661ba863e4c14033d11492621;hp=9b6fb9384ea6e94f6ca305f057c3182caa87fb43;hb=c04a5fe3e2867d59ce9757069fdd20c06c326724;hpb=cfda0421ca2c7c5f762814fd25988cf89871f1d8 diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 9b6fb93..071d4c0 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -16,6 +16,8 @@ module TcSimplify ( tcSimplifyDeriv, tcSimplifyDefault, bindInstsOfLocalFuns, + + tcSimplifyStagedExpr, misMatchMsg ) where @@ -58,6 +60,7 @@ import Util import SrcLoc import DynFlags import FastString + import Control.Monad import Data.List \end{code} @@ -861,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. @@ -977,7 +980,7 @@ makeImplicationBind :: InstLoc -> [TcTyVar] -- (ir1, .., irn) = f qtvs givens -- where f is (evidence for) the new implication constraint -- f :: forall qtvs. givens => (ir1, .., irn) --- qtvs includes coercion variables. +-- qtvs includes coercion variables -- -- This binding must line up the 'rhs' in reduceImplication makeImplicationBind loc all_tvs @@ -997,7 +1000,7 @@ makeImplicationBind loc all_tvs name = mkInternalName uniq (mkVarOcc "ic") span implic_inst = ImplicInst { tci_name = name, tci_tyvars = all_tvs, - tci_given = (eq_givens ++ dict_givens), + tci_given = eq_givens ++ dict_givens, -- same order as binders tci_wanted = irreds, tci_loc = loc } @@ -1262,9 +1265,23 @@ 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. That is the *whole* reason -for the red_given_scs field in RedEnv, and the function argument to -addGiven. +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 @@ -1276,20 +1293,23 @@ tcSimplifySuperClasses -> TcM TcDictBinds 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 = RedEnv { red_doc = pprInstLoc loc, - red_try_me = try_me, - red_givens = this:givens, - red_given_scs = add_scs, - red_stack = (0,[]), - red_improve = False } -- No unification vars - add_scs g | g==this = NoSCs - | otherwise = AddSCs - try_me _ = ReduceMe -- Try hard, so we completely solve the superclass -- constraints right here. See Note [SUPERCLASS-LOOP 1] \end{code} @@ -1412,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 @@ -1424,7 +1444,7 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- HOWEVER, some unification may take place, if we instantiate -- a method Inst with an equality constraint ; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe) - ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds' + ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds_z -- Next, figure out the tyvars we will quantify over ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs) @@ -1452,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. @@ -1473,7 +1500,7 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds (is_nested_group || isDict inst) = Stop | otherwise = ReduceMe env = mkNoImproveRedEnv doc try_me - ; (_imp, binds, irreds) <- reduceContext env wanteds' + ; (_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 @@ -1652,12 +1679,20 @@ tcSimplifyIPs given_ips wanteds ; let env = mkRedEnv doc try_me given_ips' ; (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) @@ -1743,8 +1778,6 @@ data RedEnv -- Always dicts & equalities -- but see Note [Rigidity] - , red_given_scs :: Inst -> WantSCs -- See Note [Recursive instances and superclases] - , red_stack :: (Int, [Inst]) -- Recursion stack (for err msg) -- See Note [RedStack] } @@ -1767,7 +1800,6 @@ mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv mkRedEnv doc try_me givens = RedEnv { red_doc = doc, red_try_me = try_me, red_givens = givens, - red_given_scs = const AddSCs, red_stack = (0,[]), red_improve = True } @@ -1776,7 +1808,6 @@ mkInferRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv mkInferRedEnv doc try_me = RedEnv { red_doc = doc, red_try_me = try_me, red_givens = [], - red_given_scs = const AddSCs, red_stack = (0,[]), red_improve = True } @@ -1785,7 +1816,6 @@ mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv mkNoImproveRedEnv doc try_me = RedEnv { red_doc = doc, red_try_me = try_me, red_givens = [], - red_given_scs = const AddSCs, red_stack = (0,[]), red_improve = True } @@ -1869,15 +1899,18 @@ reduceContext env wanteds0 -- Build the Avail mapping from "given_dicts" ; (init_state, _) <- getLIE $ do - { init_state <- foldlM (addGiven (red_given_scs env)) - emptyAvails givens' + { init_state <- foldlM addGiven emptyAvails givens' ; return init_state } -- Solve the *wanted* *dictionary* constraints (not implications) - -- This may expose some further equational constraints... + -- 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) + -- 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 @@ -1903,18 +1936,24 @@ reduceContext env wanteds0 -- 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 uncovered extra equalities. We will try to solve them - -- in the next iteration. + -- (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 - extraEqs = (not . null) extra_eqs - improved = improvedFlexible || extraEqs + reduced_dicts = not (isEmptyBag dict_binds) + improved = improvedFlexible || reduced_dicts -- improvedHint = (if avails_improved then " [AVAILS]" else "") ++ - (if eq_improved then " [EQ]" else "") ++ - (if extraEqs then " [EXTRA EQS]" else "") + (if eq_improved then " [EQ]" else "") ; traceTc (text "reduceContext end" <+> (vcat [ text "----------------------", @@ -1992,6 +2031,44 @@ mkEqnMsg (pred1,from1) (pred2,from2) tidy_env ; 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} @@ -2536,14 +2613,19 @@ addWanted want_scs avails wanted rhs_expr wanteds where avail = Rhs rhs_expr wanteds -addGiven :: (Inst -> WantSCs) -> Avails -> Inst -> TcM Avails -addGiven want_scs avails given = addAvailAndSCs (want_scs given) avails given (Given given) - -- Conditionally add superclasses for 'givens' +addGiven :: Avails -> Inst -> TcM Avails +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 + + -- 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} @@ -2914,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) @@ -2928,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} @@ -2942,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 @@ -2951,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} + %************************************************************************ %* * @@ -3018,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 @@ -3026,14 +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 :: TidyEnv -> Maybe (InstLoc, [Inst]) -> [Inst] -> TcM () -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 @@ -3051,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 @@ -3099,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