-\begin{code}
-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 wanted'
- qtvs = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
- -- See Note [Choosing which variables to quantify]
-
- -- To maximise sharing, remove from consideration any
- -- constraints that don't mention qtvs at all
- ; let (free1, bound) = partition (isFreeWhenInferring qtvs) wanted'
- ; extendLIEs free1
-
- -- To make types simple, reduce as much as possible
- ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$
- ppr (oclose preds gbl_tvs) $$ ppr free1 $$ ppr bound))
- ; (irreds1, binds1) <- tryHardCheckLoop doc bound
-
- -- Note [Inference and implication constraints]
- ; let want_dict d = tyVarsOfInst d `intersectsVarSet` qtvs
- ; (irreds2, binds2) <- approximateImplications doc want_dict irreds1
-
- -- By now improvment may have taken place, and we must *not*
- -- quantify over any variable free in the environment
- -- tc137 (function h inside g) is an example
- ; gbl_tvs <- tcGetGlobalTyVars
- ; qtvs1 <- zonkTcTyVarsAndFV (varSetElems qtvs)
- ; qtvs2 <- zonkQuantifiedTyVars (varSetElems (qtvs1 `minusVarSet` gbl_tvs))
-
- -- Do not quantify over constraints that *now* do not
- -- mention quantified type variables, because they are
- -- simply ambiguous (or might be bound further out). Example:
- -- f :: Eq b => a -> (a, b)
- -- g x = fst (f x)
- -- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
- -- We decide to quantify over 'alpha' alone, but free1 does not include f77
- -- because f77 mentions 'alpha'. Then reducing leaves only the (ambiguous)
- -- constraint (Eq beta), which we dump back into the free set
- -- See test tcfail181
- ; let (free3, irreds3) = partition (isFreeWhenInferring (mkVarSet qtvs2)) irreds2
- ; extendLIEs free3
-
- -- We can't abstract over any remaining unsolved
- -- implications so instead just float them outwards. Ugh.
- ; let (q_dicts, implics) = partition isDict irreds3
- ; loc <- getInstLoc (ImplicOrigin doc)
- ; implic_bind <- bindIrreds loc qtvs2 q_dicts implics
-
- ; return (qtvs2, q_dicts, binds1 `unionBags` binds2 `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.
-
-approximateImplications :: SDoc -> (Inst -> Bool) -> [Inst] -> TcM ([Inst], TcDictBinds)
--- Note [Inference and implication constraints]
--- Given a bunch of Dict and ImplicInsts, try to approximate the implications by
--- - fetching any dicts inside them that are free
--- - using those dicts as cruder constraints, to solve the implications
--- - returning the extra ones too
-
-approximateImplications doc want_dict irreds
- | null extra_dicts
- = return (irreds, emptyBag)
- | otherwise
- = do { extra_dicts' <- mapM cloneDict extra_dicts
- ; tryHardCheckLoop doc (extra_dicts' ++ irreds) }
- -- By adding extra_dicts', we make them
- -- available to solve the implication constraints
- where
- extra_dicts = get_dicts (filter isImplicInst irreds)
-
- get_dicts :: [Inst] -> [Inst] -- Returns only Dicts
- -- Find the wanted constraints in implication constraints that satisfy
- -- want_dict, and are not bound by forall's in the constraint itself
- get_dicts ds = concatMap get_dict ds
-
- get_dict d@(Dict {}) | want_dict d = [d]
- | otherwise = []
- get_dict (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
- = [ d | let tv_set = mkVarSet tvs
- , d <- get_dicts wanteds
- , not (tyVarsOfInst d `intersectsVarSet` tv_set)]
- get_dict other = pprPanic "approximateImplications" (ppr other)
-\end{code}
-
-Note [Inference and implication constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we have a wanted implication constraint (perhaps arising from
-a nested pattern match) like
- C a => D [a]
-and we are now trying to quantify over 'a' when inferring the type for
-a function. In principle it's possible that there might be an instance
- instance (C a, E a) => D [a]
-so the context (E a) would suffice. The Right Thing is to abstract over
-the implication constraint, but we don't do that (a) because it'll be
-surprising to programmers and (b) because we don't have the machinery to deal
-with 'given' implications.
-
-So our best approximation is to make (D [a]) part of the inferred
-context, so we can use that to discharge the implication. Hence
-the strange function getImplicWanteds.
-
-The common cases are more clear-cut, when we have things like
- forall a. C a => C b
-Here, abstracting over (C b) is not an approximation at all -- but see
-Note [Freeness and implications].
-
-See Trac #1430 and test tc228.
-
-
-\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) <- gentleCheckLoop 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:
- truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
-From an application (truncate f i) we get
- t1 = truncate at f
- t2 = t1 at i
-If we have also have a second occurrence of truncate, we get
- t3 = truncate at f
- t4 = t3 at i
-When simplifying with i,f free, we might still notice that
-t1=t3; but alas, the binding for t2 (which mentions t1)
-may continue to float out!
-
-
-Note [NO TYVARS]
-~~~~~~~~~~~~~~~~~
- class Y a b | a -> b where
- y :: a -> X b
-
- instance Y [[a]] a where
- y ((x:_):_) = X x
-
- k :: X a -> X a -> X a
-
- g :: Num a => [X a] -> [X a]
- g xs = h xs
- where
- h ys = ys ++ map (k (y [[0]])) xs
-
-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
-the bindings (because of [LOOP]), but in fact t1 is what g is
-polymorphic in.
-
-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 Note [Inheriting implicit parameters]
-
-{- No longer used (with implication constraints)
-isFreeWhenChecking :: TyVarSet -- Quantified tyvars
- -> NameSet -- Quantified implicit parameters
- -> Inst -> Bool
-isFreeWhenChecking qtvs ips inst
- = isFreeWrtTyVars qtvs inst
- && isFreeWrtIPs ips inst
--}
-
-isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs
-isFreeWrtIPs ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
-\end{code}
-
-
-%************************************************************************
-%* *
-\subsection{tcSimplifyCheck}
-%* *
-%************************************************************************
-
-@tcSimplifyCheck@ is used when we know exactly the set of variables
-we are going to quantify over. For example, a class or instance declaration.
-
-\begin{code}
------------------------------------------------------------
--- tcSimplifyCheck is used when checking expression type signatures,
--- class decls, instance decls etc.
-tcSimplifyCheck :: InstLoc
- -> [TcTyVar] -- Quantify over these
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM TcDictBinds -- Bindings
-tcSimplifyCheck loc qtvs givens wanteds
- = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
- do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
- ; implic_bind <- bindIrreds loc qtvs givens irreds
- ; return (binds `unionBags` implic_bind) }
-
------------------------------------------------------------
--- tcSimplifyCheckPat is used for existential pattern match
-tcSimplifyCheckPat :: InstLoc
- -> [CoVar] -> Refinement
- -> [TcTyVar] -- Quantify over these
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM TcDictBinds -- Bindings
-tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
- = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
- do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
- ; implic_bind <- bindIrredsR loc qtvs co_vars reft
- givens irreds
- ; return (binds `unionBags` implic_bind) }
-
------------------------------------------------------------
-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
-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' *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' && isEmptyRefinement reft
- then do
- { let qtv_set = mkVarSet qtvs
- (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds
- ; extendLIEs frees
- ; return real_irreds }
- else return 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
- -- If irreds' is empty, it does something sensible
- ; extendLIEs implics
- ; return bind }
-
-
-makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement
- -> [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
--- 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
- givens -- Guaranteed all Dicts
- irreds
- | null irreds -- If there are no irreds, we are done
- = return ([], emptyBag)
- | otherwise -- Otherwise we must generate a binding
- = do { uniq <- newUnique
- ; span <- getSrcSpanM
- ; let name = mkInternalName uniq (mkVarOcc "ic") span
- implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
- tci_tyvars = all_tvs,
- tci_given = givens,
- tci_wanted = irreds, tci_loc = loc }
-
- ; let n_irreds = length irreds
- irred_ids = map instToId irreds
- tup_ty = mkTupleTy Boxed n_irreds (map idType irred_ids)
- pat = TuplePat (map nlVarPat irred_ids) Boxed tup_ty
- rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
- co = mkWpApps (map instToId givens) <.> mkWpTyApps (mkTyVarTys all_tvs)
- bind | n_irreds==1 = VarBind (head irred_ids) rhs
- | otherwise = PatBind { pat_lhs = L span pat,
- pat_rhs = unguardedGRHSs rhs,
- pat_rhs_ty = tup_ty,
- bind_fvs = placeHolderNames }
- ; -- pprTrace "Make implic inst" (ppr implic_inst) $
- return ([implic_inst], unitBag (L span bind)) }
-
------------------------------------------------------------
-tryHardCheckLoop :: SDoc
- -> [Inst] -- Wanted
- -> TcM ([Inst], TcDictBinds)
-
-tryHardCheckLoop doc wanteds
- = checkLoop (mkRedEnv doc try_me []) wanteds
- where
- try_me inst = ReduceMe AddSCs
- -- Here's the try-hard bit
-
------------------------------------------------------------
-gentleCheckLoop :: InstLoc
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM ([Inst], TcDictBinds)
-
-gentleCheckLoop inst_loc givens wanteds
- = checkLoop env wanteds
- where
- env = mkRedEnv (pprInstLoc inst_loc) try_me givens
-
- try_me inst | isMethodOrLit inst = ReduceMe AddSCs
- | otherwise = Stop
- -- When checking against a given signature
- -- we MUST be very gentle: Note [Check gently]
-\end{code}
-
-Note [Check gently]
-~~~~~~~~~~~~~~~~~~~~
-We have to very careful about not simplifying too vigorously
-Example:
- data T a where
- MkT :: a -> T [a]
-
- f :: Show b => T b -> b
- f (MkT x) = show [x]
-
-Inside the pattern match, which binds (a:*, x:a), we know that
- b ~ [a]
-Hence we have a dictionary for Show [a] available; and indeed we
-need it. We are going to build an implication contraint
- forall a. (b~[a]) => Show [a]
-Later, we will solve this constraint using the knowledg e(Show b)
-
-But we MUST NOT reduce (Show [a]) to (Show a), else the whole
-thing becomes insoluble. So we simplify gently (get rid of literals
-and methods only, plus common up equal things), deferring the real
-work until top level, when we solve the implication constraint
-with tryHardCheckLooop.
-
-
-\begin{code}
------------------------------------------------------------
-checkLoop :: RedEnv
- -> [Inst] -- Wanted
- -> TcM ([Inst], TcDictBinds)
--- Precondition: givens are completely rigid
--- Postcondition: returned Insts are zonked
-
-checkLoop env wanteds
- = do { -- Givens are skolems, so no need to zonk them
- wanteds' <- mappM zonkInst wanteds
-
- ; (improved, binds, irreds) <- reduceContext env wanteds'
-
- ; if not improved then
- return (irreds, binds)
- 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]
- { (irreds1, binds1) <- checkLoop env irreds
- ; return (irreds1, binds `unionBags` binds1) } }
-\end{code}
-
-Note [LOOP]
-~~~~~~~~~~~
- class If b t e r | b t e -> r
- instance If T t e t
- instance If F t e e
- class Lte a b c | a b -> c where lte :: a -> b -> c
- instance Lte Z b T
- instance (Lte a b l,If l b a c) => Max a b c