+---------------------------------------------
+reduceImplication :: RedEnv
+ -> Avails
+ -> Refinement -- May refine the givens; often empty
+ -> [TcTyVar] -- Quantified type variables; all skolems
+ -> [Inst] -- Extra givens; all rigid
+ -> [Inst] -- Wanted
+ -> InstLoc
+ -> TcM (Avails, LookupInstResult)
+\end{code}
+
+Suppose we are simplifying the constraint
+ forall bs. extras => wanted
+in the context of an overall simplification problem with givens 'givens',
+and refinment 'reft'.
+
+Note that
+ * The refinement is often empty
+
+ * The 'extra givens' need not mention any of the quantified type variables
+ e.g. forall {}. Eq a => Eq [a]
+ forall {}. C Int => D (Tree Int)
+
+ This happens when you have something like
+ data T a where
+ T1 :: Eq a => a -> T a
+
+ f :: T a -> Int
+ f x = ...(case x of { T1 v -> v==v })...
+
+\begin{code}
+ -- ToDo: should we instantiate tvs? I think it's not necessary
+ --
+ -- ToDo: what about improvement? There may be some improvement
+ -- exposed as a result of the simplifications done by reduceList
+ -- which are discarded if we back off.
+ -- This is almost certainly Wrong, but we'll fix it when dealing
+ -- better with equality constraints
+reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
+ = do { -- Add refined givens, and the extra givens
+ (refined_red_givens, avails)
+ <- if isEmptyRefinement reft then return (red_givens env, orig_avails)
+ else foldlM (addRefinedGiven reft) ([], orig_avails) (red_givens env)
+ ; avails <- foldlM addGiven avails extra_givens
+
+ -- Solve the sub-problem
+ ; let try_me inst = ReduceMe AddSCs -- Note [Freeness and implications]
+ env' = env { red_givens = refined_red_givens ++ extra_givens
+ , red_try_me = try_me }
+
+ ; traceTc (text "reduceImplication" <+> vcat
+ [ ppr (red_givens env), ppr extra_givens, ppr reft, ppr wanteds ])
+ ; avails <- reduceList env' wanteds avails
+
+ -- Extract the binding
+ ; (binds, irreds, _frees) <- extractResults avails wanteds
+ -- No frees, because try_me never says Free
+
+ ; let dict_ids = map instToId extra_givens
+ co = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet binds
+ rhs = mkHsWrap co payload
+ loc = instLocSpan inst_loc
+ payload | isSingleton wanteds = HsVar (instToId (head wanteds))
+ | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed
+
+ -- If there are any irreds, we back off and return NoInstance
+ -- Either way, we discard the extra avails we've generated;
+ -- but we remember if we have done any (global) improvement
+ ; let ret_avails = updateImprovement orig_avails avails
+ ; case irreds of
+ [] -> return (ret_avails, GenInst [] (L loc rhs))
+ other -> return (ret_avails, NoInstance)
+ }
+\end{code}
+
+Note [Freeness and implications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's hard to say when an implication constraint can be floated out. Consider
+ forall {} Eq a => Foo [a]
+The (Foo [a]) doesn't mention any of the quantified variables, but it
+still might be partially satisfied by the (Eq a).
+
+There is a useful special case when it *is* easy to partition the
+constraints, namely when there are no 'givens'. Consider
+ forall {a}. () => Bar b
+There are no 'givens', and so there is no reason to capture (Bar b).
+We can let it float out. But if there is even one constraint we
+must be much more careful:
+ forall {a}. C a b => Bar (m b)
+because (C a b) might have a superclass (D b), from which we might
+deduce (Bar [b]) when m later gets instantiated to []. Ha!
+
+Here is an even more exotic example
+ class C a => D a b
+Now consider the constraint
+ forall b. D Int b => C Int
+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!
+
+%************************************************************************
+%* *
+ Avails and AvailHow: the pool of evidence
+%* *
+%************************************************************************
+
+
+\begin{code}
+data Avails = Avails !ImprovementDone !AvailEnv
+
+type ImprovementDone = Bool -- True <=> some unification has happened
+ -- so some Irreds might now be reducible
+ -- keys that are now
+
+type AvailEnv = FiniteMap Inst AvailHow
+data AvailHow
+ = IsFree -- Used for free Insts
+ | IsIrred -- Used for irreducible dictionaries,
+ -- which are going to be lambda bound
+
+ | Given TcId -- Used for dictionaries for which we have a binding
+ -- e.g. those "given" in a signature
+
+ | Rhs -- Used when there is a RHS
+ (LHsExpr TcId) -- The RHS
+ [Inst] -- Insts free in the RHS; we need these too
+
+instance Outputable Avails where
+ ppr = pprAvails
+
+pprAvails (Avails imp avails)
+ = vcat [ ptext SLIT("Avails") <> (if imp then ptext SLIT("[improved]") else empty)
+ , nest 2 (vcat [sep [ppr inst, nest 2 (equals <+> ppr avail)]
+ | (inst,avail) <- fmToList avails ])]
+
+instance Outputable AvailHow where
+ ppr = pprAvail
+
projects / ghc-hetmet.git / commitdiff