-\begin{code}
-tcSimplifyInfer doc tau_tvs wanted
- = do { tau_tvs1 <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
- ; wanted' <- mappM zonkInst wanted -- Zonk before deciding quantified tyvars
- ; gbl_tvs <- tcGetGlobalTyVars
- ; let preds1 = fdPredsOfInsts wanted'
- gbl_tvs1 = oclose preds1 gbl_tvs
- qtvs = grow preds1 tau_tvs1 `minusVarSet` gbl_tvs1
- -- See Note [Choosing which variables to quantify]
-
- -- To maximise sharing, remove from consideration any
- -- constraints that don't mention qtvs at all
- ; let (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
- ; extendLIEs free
-
- -- To make types simple, reduce as much as possible
- ; traceTc (text "infer" <+> (ppr preds1 $$ ppr (grow preds1 tau_tvs1) $$ ppr gbl_tvs $$
- ppr gbl_tvs1 $$ ppr free $$ 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
-
- -- Now work out all over again which type variables to quantify,
- -- exactly in the same way as before, but starting from irreds2. Why?
- -- a) 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
- --
- -- b) 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
- --
- -- c) irreds may contain type variables not previously mentioned,
- -- e.g. instance D a x => Foo [a]
- -- wanteds = Foo [a]
- -- Then after simplifying we'll get (D a x), and x is fresh
- -- We must quantify over x else it'll be totally unbound
- ; tau_tvs2 <- zonkTcTyVarsAndFV (varSetElems tau_tvs1)
- ; gbl_tvs2 <- zonkTcTyVarsAndFV (varSetElems gbl_tvs1)
- -- Note that we start from gbl_tvs1
- -- We use tcGetGlobalTyVars, then oclose wrt preds2, because
- -- we've already put some of the original preds1 into frees
- -- E.g. wanteds = C a b (where a->b)
- -- gbl_tvs = {a}
- -- tau_tvs = {b}
- -- Then b is fixed by gbl_tvs, so (C a b) will be in free, and
- -- irreds2 will be empty. But we don't want to generalise over b!
- ; let preds2 = fdPredsOfInsts irreds2 -- irreds2 is zonked
- qtvs = grow preds2 tau_tvs2 `minusVarSet` oclose preds2 gbl_tvs2
- ; let (free, irreds3) = partition (isFreeWhenInferring qtvs) irreds2
- ; extendLIEs free
-
- -- Turn the quantified meta-type variables into real type variables
- ; qtvs2 <- zonkQuantifiedTyVars (varSetElems qtvs)
-
- -- We can't abstract over any remaining unsolved
- -- implications so instead just float them outwards. Ugh.
- ; let (q_dicts0, implics) = partition isAbstractableInst irreds3
- ; loc <- getInstLoc (ImplicOrigin doc)
- ; implic_bind <- bindIrreds loc qtvs2 q_dicts0 implics
-
- -- Prepare equality instances for quantification
- ; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0
- ; q_eqs <- mappM finalizeEqInst q_eqs0
-
- ; return (qtvs2, q_eqs ++ 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 i@(EqInst {}) | want_dict i = [i]
- | otherwise = []
- 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 get_dictsin approximateImplications.
-
-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 { traceTc (text "tcSimplifyInferCheck <-" <+> ppr wanteds)
- ; (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
-
- ; traceTc (text "tcSimplifyInferCheck ->" <+> ppr (implic_bind))
- ; 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 { traceTc (text "tcSimplifyCheck")
- ; (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 { traceTc (text "tcSimplifyCheckPat")
- ; (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 (TOMDO: true?)
- 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 (eq_givens,dict_givens) = partitionGivenEqInsts givens
- eq_tyvar_cos = map TyVarTy $ uniqSetToList $ tyVarsOfTypes $ map eqInstType eq_givens
- ; let name = mkInternalName uniq (mkVarOcc "ic") span
- implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
- tci_tyvars = all_tvs,
- tci_given = (eq_givens ++ dict_givens),
- tci_wanted = irreds, tci_loc = loc }
- ; let
- -- only create binder for dict_irreds
- -- we
- (eq_irreds,dict_irreds) = partitionWantedEqInsts irreds
- n_dict_irreds = length dict_irreds
- dict_irred_ids = map instToId dict_irreds
- tup_ty = mkTupleTy Boxed n_dict_irreds (map idType dict_irred_ids)
- 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 }
- ; -- pprTrace "Make implic inst" (ppr (implic_inst,irreds,dict_irreds,tup_ty)) $
- return ([implic_inst], unitBag (L span bind)) }
-
------------------------------------------------------------
-tryHardCheckLoop :: SDoc
- -> [Inst] -- Wanted
- -> TcM ([Inst], TcDictBinds)
-
-tryHardCheckLoop doc wanteds
- = do { (irreds,binds,_) <- checkLoop (mkRedEnv doc try_me []) wanteds
- ; return (irreds,binds)
- }
- 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
- = do { (irreds,binds,_) <- checkLoop env wanteds
- ; return (irreds,binds)
- }
- 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,
- [Inst]) -- needed givens
--- Precondition: givens are completely rigid
--- Postcondition: returned Insts are zonked
-
-checkLoop env wanteds
- = go env wanteds []
- where go env wanteds needed_givens
- = do { -- Givens are skolems, so no need to zonk them
- wanteds' <- zonkInsts wanteds
-
- ; (improved, binds, irreds, more_needed_givens) <- reduceContext env wanteds'
-
- ; let all_needed_givens = needed_givens ++ more_needed_givens
-
- ; if not improved then
- return (irreds, binds, all_needed_givens)
- 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, all_needed_givens1) <- go env irreds all_needed_givens
- ; return (irreds1, binds `unionBags` binds1, all_needed_givens1) } }
-\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
-
-Wanted: Max Z (S x) y
-
-Then we'll reduce using the Max instance to:
- (Lte Z (S x) l, If l (S x) Z y)
-and improve by binding l->T, after which we can do some reduction
-on both the Lte and If constraints. What we *can't* do is start again
-with (Max Z (S x) y)!
-
-
-
-%************************************************************************
-%* *
- tcSimplifySuperClasses
-%* *
-%************************************************************************
-
-Note [SUPERCLASS-LOOP 1]
-~~~~~~~~~~~~~~~~~~~~~~~~
-We have to be very, very careful when generating superclasses, lest we
-accidentally build a loop. Here's an example:
-
- class S a
-
- class S a => C a where { opc :: a -> a }
- class S b => D b where { opd :: b -> b }
-
- instance C Int where
- opc = opd
-
- instance D Int where
- opd = opc
-
-From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
-Simplifying, we may well get:
- $dfCInt = :C ds1 (opd dd)
- dd = $dfDInt
- ds1 = $p1 dd
-Notice that we spot that we can extract ds1 from dd.
-
-Alas! Alack! We can do the same for (instance D Int):
-
- $dfDInt = :D ds2 (opc dc)
- dc = $dfCInt
- 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
-
-\begin{code}
-tcSimplifySuperClasses
- :: InstLoc
- -> [Inst] -- Given
- -> [Inst] -- Wanted
- -> TcM TcDictBinds
-tcSimplifySuperClasses loc givens sc_wanteds
- = do { traceTc (text "tcSimplifySuperClasses")
- ; (irreds,binds1,_) <- checkLoop env sc_wanteds
- ; let (tidy_env, tidy_irreds) = tidyInsts 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
-\end{code}
-
-
-%************************************************************************
-%* *
-\subsection{tcSimplifyRestricted}
-%* *
-%************************************************************************
-
-tcSimplifyRestricted infers which type variables to quantify for a
-group of restricted bindings. This isn't trivial.
-
-Eg1: id = \x -> x
- We want to quantify over a to get id :: forall a. a->a
-
-Eg2: eq = (==)
- We do not want to quantify over a, because there's an Eq a
- constraint, so we get eq :: a->a->Bool (notice no forall)
-
-So, assume:
- RHS has type 'tau', whose free tyvars are tau_tvs
- RHS has constraints 'wanteds'
-
-Plan A (simple)
- Quantify over (tau_tvs \ ftvs(wanteds))
- This is bad. The constraints may contain (Monad (ST s))
- where we have instance Monad (ST s) where...
- so there's no need to be monomorphic in s!
-
- Also the constraint might be a method constraint,
- whose type mentions a perfectly innocent tyvar:
- op :: Num a => a -> b -> a
- Here, b is unconstrained. A good example would be
- foo = op (3::Int)
- We want to infer the polymorphic type
- foo :: forall b. b -> b
-
-
-Plan B (cunning, used for a long time up to and including GHC 6.2)
- Step 1: Simplify the constraints as much as possible (to deal
- with Plan A's problem). Then set
- qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
-
- Step 2: Now simplify again, treating the constraint as 'free' if
- it does not mention qtvs, and trying to reduce it otherwise.
- The reasons for this is to maximise sharing.
-
- This fails for a very subtle reason. Suppose that in the Step 2
- a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
- In the Step 1 this constraint might have been simplified, perhaps to
- (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
- This won't happen in Step 2... but that in turn might prevent some other
- constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..})
- and that in turn breaks the invariant that no constraints are quantified over.
-
- Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
- the problem.
-
-
-Plan C (brutal)
- Step 1: Simplify the constraints as much as possible (to deal
- with Plan A's problem). Then set
- qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
- Return the bindings from Step 1.
-
-
-A note about Plan C (arising from "bug" reported by George Russel March 2004)
-Consider this: