X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;ds=sidebyside;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=911e2ff12d8a7f6c4d7a86da0040bb0ce6d19dbd;hb=0560e796f1d813582e066a5f2bec2684c71df44d;hp=794e09d949411dde5ec4b228b15ffe9fcee18f38;hpb=a3a15a646977ab98f9150bb2b926d960796077e4;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 794e09d..911e2ff 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -15,7 +15,7 @@ module TcSimplify ( tcSimplifyBracket, tcSimplifyCheckPat, tcSimplifyDeriv, tcSimplifyDefault, - bindInstsOfLocalFuns + bindInstsOfLocalFuns, bindIrreds, ) where #include "HsVersions.h" @@ -28,11 +28,10 @@ import Inst import TcEnv import InstEnv import TcGadt -import TcMType import TcType +import TcMType import TcIface import Var -import TyCon import Name import NameSet import Class @@ -398,8 +397,8 @@ When m is later unified with [], we can solve both constraints. Notes on implicit parameters -------------------------------------- -Question 1: can we "inherit" implicit parameters -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [Inheriting implicit parameters] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this: f x = (x::Int) + ?y @@ -424,6 +423,21 @@ BOTTOM LINE: when *inferring types* you *must* quantify over implicit parameters. See the predicate isFreeWhenInferring. +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 +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'. + + Question 2: type signatures ~~~~~~~~~~~~~~~~~~~~~~~~~~~ BUT WATCH OUT: When you supply a type signature, we can't force you @@ -642,42 +656,81 @@ tcSimplifyInfer :: SDoc -> TcTyVarSet -- fv(T); type vars -> [Inst] -- Wanted - -> TcM ([TcTyVar], -- Tyvars to quantify (zonked) - TcDictBinds, -- Bindings - [TcId]) -- Dict Ids that must be bound here (zonked) + -> TcM ([TcTyVar], -- Tyvars to quantify (zonked and quantified) + [Inst], -- Dict Ids that must be bound here (zonked) + TcDictBinds) -- Bindings -- Any free (escaping) Insts are tossed into the environment \end{code} \begin{code} -tcSimplifyInfer doc tau_tvs wanted_lie - = do { let try_me inst | isDict inst = Stop -- Dicts - | otherwise = ReduceMe NoSCs -- Lits, Methods, - -- and impliciation constraints - -- In an effort to make the inferred types simple, we try - -- to squeeze out implication constraints if we can. - -- See Note [Squashing methods] - - ; (binds1, irreds) <- checkLoop (mkRedEnv doc try_me []) wanted_lie - - ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs) +tcSimplifyInfer doc tau_tvs wanted + = do { tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs) + ; wanted' <- mappM zonkInst wanted -- Zonk before deciding quantified tyvars ; gbl_tvs <- tcGetGlobalTyVars - ; let preds = fdPredsOfInsts irreds + ; let preds = fdPredsOfInsts wanted' qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs - (free, bound) = partition (isFreeWhenInferring qtvs) irreds + (free, bound) = partition (isFreeWhenInferring qtvs) wanted' + ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$ ppr (oclose preds gbl_tvs) $$ ppr free $$ ppr bound)) + ; extendLIEs free - -- Remove redundant superclasses from 'bound' - -- The 'Stop' try_me result does not do so, - -- see Note [No superclasses for Stop] + -- To make types simple, reduce as much as possible ; let try_me inst = ReduceMe AddSCs - ; (binds2, irreds) <- checkLoop (mkRedEnv doc try_me []) bound + ; (irreds, binds) <- checkLoop (mkRedEnv doc try_me []) bound - ; extendLIEs free - ; return (varSetElems qtvs, binds1 `unionBags` binds2, map instToId irreds) } + ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs) + + -- We can't abstract over implications + ; let (dicts, implics) = partition isDict irreds + ; loc <- getInstLoc (ImplicOrigin doc) + ; implic_bind <- bindIrreds loc qtvs' dicts implics + + ; return (qtvs', dicts, binds `unionBags` implic_bind) } -- NB: when we are done, we might have some bindings, but -- the final qtvs might be empty. See Note [NO TYVARS] below. \end{code} +\begin{code} +----------------------------------------------------------- +-- tcSimplifyInferCheck is used when we know the constraints we are to simplify +-- against, but we don't know the type variables over which we are going to quantify. +-- This happens when we have a type signature for a mutually recursive group +tcSimplifyInferCheck + :: InstLoc + -> TcTyVarSet -- fv(T) + -> [Inst] -- Given + -> [Inst] -- Wanted + -> TcM ([TyVar], -- Fully zonked, and quantified + TcDictBinds) -- Bindings + +tcSimplifyInferCheck loc tau_tvs givens wanteds + = do { (irreds, binds) <- innerCheckLoop loc givens wanteds + + -- Figure out which type variables to quantify over + -- You might think it should just be the signature tyvars, + -- but in bizarre cases you can get extra ones + -- f :: forall a. Num a => a -> a + -- f x = fst (g (x, head [])) + 1 + -- g a b = (b,a) + -- Here we infer g :: forall a b. a -> b -> (b,a) + -- We don't want g to be monomorphic in b just because + -- f isn't quantified over b. + ; let all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens) + ; all_tvs <- zonkTcTyVarsAndFV all_tvs + ; gbl_tvs <- tcGetGlobalTyVars + ; let qtvs = varSetElems (all_tvs `minusVarSet` gbl_tvs) + -- We could close gbl_tvs, but its not necessary for + -- soundness, and it'll only affect which tyvars, not which + -- dictionaries, we quantify over + + ; qtvs' <- zonkQuantifiedTyVars qtvs + + -- Now we are back to normal (c.f. tcSimplCheck) + ; implic_bind <- bindIrreds loc qtvs' givens irreds + + ; return (qtvs', binds `unionBags` implic_bind) } +\end{code} + Note [Squashing methods] ~~~~~~~~~~~~~~~~~~~~~~~~~ Be careful if you want to float methods more: @@ -719,9 +772,9 @@ The net effect of [NO TYVARS] \begin{code} isFreeWhenInferring :: TyVarSet -> Inst -> Bool isFreeWhenInferring qtvs inst - = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars - && isInheritableInst inst -- And no implicit parameter involved - -- (see "Notes on implicit parameters") + = isFreeWrtTyVars qtvs inst -- Constrains no quantified vars + && isInheritableInst inst -- and no implicit parameter involved + -- see Note [Inheriting implicit parameters] {- No longer used (with implication constraints) isFreeWhenChecking :: TyVarSet -- Quantified tyvars @@ -756,10 +809,9 @@ tcSimplifyCheck :: InstLoc -> [Inst] -- Wanted -> TcM TcDictBinds -- Bindings tcSimplifyCheck loc qtvs givens wanteds - = ASSERT( all isSkolemTyVar qtvs ) - do { (binds, irreds) <- innerCheckLoop loc givens wanteds - ; implic_bind <- bindIrreds loc [] emptyRefinement - qtvs givens irreds + = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs ) + do { (irreds, binds) <- innerCheckLoop loc givens wanteds + ; implic_bind <- bindIrreds loc qtvs givens irreds ; return (binds `unionBags` implic_bind) } ----------------------------------------------------------- @@ -771,26 +823,37 @@ tcSimplifyCheckPat :: InstLoc -> [Inst] -- Wanted -> TcM TcDictBinds -- Bindings tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds - = ASSERT( all isSkolemTyVar qtvs ) - do { (binds, irreds) <- innerCheckLoop loc givens wanteds - ; implic_bind <- bindIrreds loc co_vars reft - qtvs givens irreds + = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs ) + do { (irreds, binds) <- innerCheckLoop loc givens wanteds + ; implic_bind <- bindIrredsR loc qtvs co_vars reft + givens irreds ; return (binds `unionBags` implic_bind) } ----------------------------------------------------------- -bindIrreds :: InstLoc -> [CoVar] -> Refinement - -> [TcTyVar] -> [Inst] -> [Inst] - -> TcM TcDictBinds +bindIrreds :: InstLoc -> [TcTyVar] + -> [Inst] -> [Inst] + -> TcM TcDictBinds +bindIrreds loc qtvs givens irreds + = bindIrredsR loc qtvs [] emptyRefinement givens irreds + +bindIrredsR :: InstLoc -> [TcTyVar] -> [CoVar] + -> Refinement -> [Inst] -> [Inst] + -> TcM TcDictBinds -- Make a binding that binds 'irreds', by generating an implication -- constraint for them, *and* throwing the constraint into the LIE -bindIrreds loc co_vars reft qtvs givens irreds +bindIrredsR loc qtvs co_vars reft givens irreds + | null irreds + = return emptyBag + | otherwise = do { let givens' = filter isDict givens -- The givens can include methods + -- See Note [Pruning the givens in an implication constraint] - -- If there are no 'givens', then it's safe to + -- If there are no 'givens' *and* the refinement is empty + -- (the refinement is like more givens), then it's safe to -- partition the 'wanteds' by their qtvs, thereby trimming irreds -- See Note [Freeness and implications] - ; irreds' <- if null givens' + ; irreds' <- if null givens' && isEmptyRefinement reft then do { let qtv_set = mkVarSet qtvs (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds @@ -800,7 +863,8 @@ bindIrreds loc co_vars reft qtvs givens irreds ; let all_tvs = qtvs ++ co_vars -- Abstract over all these ; (implics, bind) <- makeImplicationBind loc all_tvs reft givens' irreds' - -- This call does the real work + -- This call does the real work + -- If irreds' is empty, it does something sensible ; extendLIEs implics ; return bind } @@ -813,6 +877,8 @@ makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement -- 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) +-- qtvs includes coercion variables -- -- This binding must line up the 'rhs' in reduceImplication makeImplicationBind loc all_tvs reft @@ -846,8 +912,7 @@ makeImplicationBind loc all_tvs reft ----------------------------------------------------------- topCheckLoop :: SDoc -> [Inst] -- Wanted - -> TcM (TcDictBinds, - [Inst]) -- Irreducible + -> TcM ([Inst], TcDictBinds) topCheckLoop doc wanteds = checkLoop (mkRedEnv doc try_me []) wanteds @@ -858,8 +923,7 @@ topCheckLoop doc wanteds innerCheckLoop :: InstLoc -> [Inst] -- Given -> [Inst] -- Wanted - -> TcM (TcDictBinds, - [Inst]) -- Irreducible + -> TcM ([Inst], TcDictBinds) innerCheckLoop inst_loc givens wanteds = checkLoop env wanteds @@ -900,10 +964,8 @@ with topCheckLooop. ----------------------------------------------------------- checkLoop :: RedEnv -> [Inst] -- Wanted - -> TcM (TcDictBinds, - [Inst]) -- Irreducible --- Precondition: the try_me never returns Free --- givens are completely rigid + -> TcM ([Inst], TcDictBinds) +-- Precondition: givens are completely rigid checkLoop env wanteds = do { -- Givens are skolems, so no need to zonk them @@ -912,7 +974,7 @@ checkLoop env wanteds ; (improved, binds, irreds) <- reduceContext env wanteds' ; if not improved then - return (binds, irreds) + return (irreds, binds) else do -- If improvement did some unification, we go round again. @@ -920,8 +982,8 @@ checkLoop env 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, irreds1) <- checkLoop env irreds - ; return (binds `unionBags` binds1, irreds1) } } + { (irreds1, binds1) <- checkLoop env irreds + ; return (irreds1, binds `unionBags` binds1) } } \end{code} Note [LOOP] @@ -942,45 +1004,6 @@ on both the Lte and If constraints. What we *can't* do is start again with (Max Z (S x) y)! -\begin{code} ------------------------------------------------------------ --- tcSimplifyInferCheck is used when we know the constraints we are to simplify --- against, but we don't know the type variables over which we are going to quantify. --- This happens when we have a type signature for a mutually recursive group -tcSimplifyInferCheck - :: InstLoc - -> TcTyVarSet -- fv(T) - -> [Inst] -- Given - -> [Inst] -- Wanted - -> TcM ([TcTyVar], -- Variables over which to quantify - TcDictBinds) -- Bindings - -tcSimplifyInferCheck loc tau_tvs givens wanteds - = do { (binds, irreds) <- innerCheckLoop loc givens wanteds - - -- Figure out which type variables to quantify over - -- You might think it should just be the signature tyvars, - -- but in bizarre cases you can get extra ones - -- f :: forall a. Num a => a -> a - -- f x = fst (g (x, head [])) + 1 - -- g a b = (b,a) - -- Here we infer g :: forall a b. a -> b -> (b,a) - -- We don't want g to be monomorphic in b just because - -- f isn't quantified over b. - ; let all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens) - ; all_tvs <- zonkTcTyVarsAndFV all_tvs - ; gbl_tvs <- tcGetGlobalTyVars - ; let qtvs = varSetElems (all_tvs `minusVarSet` gbl_tvs) - -- We could close gbl_tvs, but its not necessary for - -- soundness, and it'll only affect which tyvars, not which - -- dictionaries, we quantify over - - -- Now we are back to normal (c.f. tcSimplCheck) - ; implic_bind <- bindIrreds loc [] emptyRefinement - qtvs givens irreds - ; return (qtvs, binds `unionBags` implic_bind) } -\end{code} - %************************************************************************ %* * @@ -1033,7 +1056,7 @@ tcSimplifySuperClasses -> [Inst] -- Wanted -> TcM TcDictBinds tcSimplifySuperClasses loc givens sc_wanteds - = do { (binds1, irreds) <- checkLoop env sc_wanteds + = do { (irreds, binds1) <- checkLoop env sc_wanteds ; let (tidy_env, tidy_irreds) = tidyInsts irreds ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds ; return binds1 } @@ -1152,7 +1175,7 @@ tcSimplifyRestricted -- Used for restricted binding groups -> [Name] -- Things bound in this group -> TcTyVarSet -- Free in the type of the RHSs -> [Inst] -- Free in the RHSs - -> TcM ([TcTyVar], -- Tyvars to quantify (zonked) + -> TcM ([TyVar], -- Tyvars to quantify (zonked and quantified) TcDictBinds) -- Bindings -- tcSimpifyRestricted returns no constraints to -- quantify over; by definition there are none. @@ -1160,7 +1183,7 @@ tcSimplifyRestricted -- Used for restricted binding groups tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- Zonk everything in sight - = mappM zonkInst wanteds `thenM` \ wanteds' -> + = do { wanteds' <- mappM zonkInst wanteds -- 'ReduceMe': Reduce as far as we can. Don't stop at -- dicts; the idea is to get rid of as many type @@ -1171,23 +1194,34 @@ 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) - in - reduceContext env wanteds' `thenM` \ (_imp, _binds, constrained_dicts) -> + ; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs) + ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds' -- Next, figure out the tyvars we will quantify over - zonkTcTyVarsAndFV (varSetElems tau_tvs) `thenM` \ tau_tvs' -> - tcGetGlobalTyVars `thenM` \ gbl_tvs' -> - mappM zonkInst constrained_dicts `thenM` \ constrained_dicts' -> - let - constrained_tvs' = tyVarsOfInsts constrained_dicts' - qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs') - `minusVarSet` constrained_tvs' - in - traceTc (text "tcSimplifyRestricted" <+> vcat [ + ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs) + ; gbl_tvs' <- tcGetGlobalTyVars + ; constrained_dicts' <- mappM zonkInst constrained_dicts + + ; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs' + -- As in tcSimplifyInfer + + -- Do not quantify over constrained type variables: + -- this is the monomorphism restriction + constrained_tvs' = tyVarsOfInsts constrained_dicts' + qtvs = qtvs1 `minusVarSet` constrained_tvs' + pp_bndrs = pprWithCommas (quotes . ppr) bndrs + + -- Warn in the mono + ; warn_mono <- doptM Opt_WarnMonomorphism + ; warnTc (warn_mono && (constrained_tvs' `intersectsVarSet` qtvs1)) + (vcat[ ptext SLIT("the Monomorphism Restriction applies to the binding") + <> plural bndrs <+> ptext SLIT("for") <+> pp_bndrs, + ptext SLIT("Consider giving a type signature for") <+> pp_bndrs]) + + ; traceTc (text "tcSimplifyRestricted" <+> vcat [ pprInsts wanteds, pprInsts constrained_dicts', ppr _binds, - ppr constrained_tvs', ppr tau_tvs', ppr qtvs ]) `thenM_` + ppr constrained_tvs', ppr tau_tvs', ppr qtvs ]) -- The first step may have squashed more methods than -- necessary, so try again, this time more gently, knowing the exact @@ -1205,27 +1239,23 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds -- -- At top level, we *do* squash methods becuase we want to -- expose implicit parameters to the test that follows - let - is_nested_group = isNotTopLevel top_lvl - try_me inst | isFreeWrtTyVars qtvs inst, - (is_nested_group || isDict inst) = Stop - | otherwise = ReduceMe AddSCs - env = mkNoImproveRedEnv doc try_me - in - reduceContext env wanteds' `thenM` \ (_imp, binds, irreds) -> - ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured + ; let is_nested_group = isNotTopLevel top_lvl + try_me inst | isFreeWrtTyVars qtvs inst, + (is_nested_group || isDict inst) = Stop + | otherwise = ReduceMe AddSCs + env = mkNoImproveRedEnv doc try_me + ; (_imp, binds, irreds) <- reduceContext env wanteds' -- See "Notes on implicit parameters, Question 4: top level" - if is_nested_group then - extendLIEs irreds `thenM_` - returnM (varSetElems qtvs, binds) - else - let - (non_ips, bad_ips) = partition isClassDict irreds - in - addTopIPErrs bndrs bad_ips `thenM_` - extendLIEs non_ips `thenM_` - returnM (varSetElems qtvs, binds) + ; ASSERT( all (isFreeWrtTyVars qtvs) irreds ) -- None should be captured + if is_nested_group then + extendLIEs irreds + else do { let (bad_ips, non_ips) = partition isIPDict irreds + ; addTopIPErrs bndrs bad_ips + ; extendLIEs non_ips } + + ; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs) + ; return (qtvs', binds) } \end{code} @@ -1422,7 +1452,7 @@ bindInstsOfLocalFuns wanteds local_ids returnM emptyLHsBinds | otherwise - = do { (binds, irreds) <- checkLoop env for_me + = do { (irreds, binds) <- checkLoop env for_me ; extendLIEs not_for_me ; extendLIEs irreds ; return binds } @@ -1805,10 +1835,12 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc , red_try_me = try_me } ; traceTc (text "reduceImplication" <+> vcat - [ ppr (red_givens env), ppr extra_givens, ppr reft, ppr wanteds ]) + [ ppr orig_avails, + ppr (red_givens env), ppr extra_givens, + ppr reft, ppr wanteds, ppr avails ]) ; avails <- reduceList env' wanteds avails - -- Extract the binding (no frees, because try_me never says Free) + -- Extract the binding ; (binds, irreds) <- extractResults avails wanteds -- We always discard the extra avails we've generated; @@ -1861,6 +1893,20 @@ 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! +Note [Pruning the givens in an implication constraint] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we are about to form the implication constraint + forall tvs. Eq a => Ord b +The (Eq a) cannot contribute to the (Ord b), because it has no access to +the type variable 'b'. So we could filter out the (Eq a) from the givens. + +Doing so would be a bit tidier, but all the implication constraints get +simplified away by the optimiser, so it's no great win. So I don't take +advantage of that at the moment. + +If you do, BE CAREFUL of wobbly type variables. + + %************************************************************************ %* * Avails and AvailHow: the pool of evidence @@ -1971,18 +2017,12 @@ extractResults (Avails _ avails) wanteds -- 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! --- | getSrcLoc id `precedesSrcLoc` srcSpanStart span --- -> go avails (addBind binds w_span id (nlHsVar w_id)) irreds ws - | otherwise -> go avails (addBind binds w (nlHsVar id)) irreds ws Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws) where new_binds = addBind binds w rhs - where - w_span = instSpan w - w_id = instToId w add_given avails w = extendAvailEnv avails w (Given (instToId w)) @@ -2020,7 +2060,9 @@ addRefinedGiven :: Refinement -> ([Inst], Avails) -> Inst -> TcM ([Inst], Avails addRefinedGiven reft (refined_givens, avails) given | isDict given -- We sometimes have 'given' methods, but they -- are always optional, so we can drop them - , Just (co, pred) <- refinePred reft (dictPred given) + , let pred = dictPred given + , isRefineablePred pred -- See Note [ImplicInst rigidity] + , Just (co, pred) <- refinePred reft pred = do { new_given <- newDictBndr (instLoc given) pred ; let rhs = L (instSpan given) $ HsWrap (WpCo co) (HsVar (instToId given)) @@ -2031,7 +2073,30 @@ addRefinedGiven reft (refined_givens, avails) given -- and hopefully the optimiser will spot the duplicated work | otherwise = return (refined_givens, avails) +\end{code} + +Note [ImplicInst rigidity] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + C :: forall ab. (Eq a, Ord b) => b -> T a + + ...(case x of C v ->
)... + +From the case (where x::T ty) we'll get an implication constraint + forall b. (Eq ty, Ord b) =>