+ = do { res <- lookupSimpleInst wanted
+ ; case res of
+ GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
+ other -> do_this_otherwise avails wanted }
+\end{code}
+
+
+Note [SUPERCLASS-LOOP 2]
+~~~~~~~~~~~~~~~~~~~~~~~~
+But the above isn't enough. Suppose we are *given* d1:Ord a,
+and want to deduce (d2:C [a]) where
+
+ class Ord a => C a where
+ instance Ord [a] => C [a] where ...
+
+Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
+superclasses of C [a] to avails. But we must not overwrite the binding
+for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
+build a loop!
+
+Here's another variant, immortalised in tcrun020
+ class Monad m => C1 m
+ class C1 m => C2 m x
+ instance C2 Maybe Bool
+For the instance decl we need to build (C1 Maybe), and it's no good if
+we run around and add (C2 Maybe Bool) and its superclasses to the avails
+before we search for C1 Maybe.
+
+Here's another example
+ class Eq b => Foo a b
+ instance Eq a => Foo [a] a
+If we are reducing
+ (Foo [t] t)
+
+we'll first deduce that it holds (via the instance decl). We must not
+then overwrite the Eq t constraint with a superclass selection!
+
+At first I had a gross hack, whereby I simply did not add superclass constraints
+in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
+becuase it lost legitimate superclass sharing, and it still didn't do the job:
+I found a very obscure program (now tcrun021) in which improvement meant the
+simplifier got two bites a the cherry... so something seemed to be an Irred
+first time, but reducible next time.
+
+Now we implement the Right Solution, which is to check for loops directly
+when adding superclasses. It's a bit like the occurs check in unification.
+
+
+Note [RECURSIVE DICTIONARIES]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ data D r = ZeroD | SuccD (r (D r));
+
+ instance (Eq (r (D r))) => Eq (D r) where
+ ZeroD == ZeroD = True
+ (SuccD a) == (SuccD b) = a == b
+ _ == _ = False;
+
+ equalDC :: D [] -> D [] -> Bool;
+ equalDC = (==);
+
+We need to prove (Eq (D [])). Here's how we go:
+
+ d1 : Eq (D [])
+
+by instance decl, holds if
+ d2 : Eq [D []]
+ where d1 = dfEqD d2
+
+by instance decl of Eq, holds if
+ d3 : D []
+ where d2 = dfEqList d3
+ d1 = dfEqD d2
+
+But now we can "tie the knot" to give
+
+ d3 = d1
+ d2 = dfEqList d3
+ d1 = dfEqD d2
+
+and it'll even run! The trick is to put the thing we are trying to prove
+(in this case Eq (D []) into the database before trying to prove its
+contributing clauses.
+
+
+%************************************************************************
+%* *
+ Reducing a single constraint
+%* *
+%************************************************************************
+
+\begin{code}
+---------------------------------------------
+reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
+reduceInst env avails (ImplicInst { tci_tyvars = tvs, tci_reft = reft, tci_loc = loc,
+ tci_given = extra_givens, tci_wanted = wanteds })
+ = reduceImplication env avails reft tvs extra_givens wanteds loc
+
+reduceInst env avails other_inst
+ = do { result <- lookupSimpleInst other_inst
+ ; return (avails, result) }
+\end{code}
+
+\begin{code}
+---------------------------------------------
+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 (no frees, because try_me never says Free)
+ ; (binds, irreds, _frees) <- extractResults avails wanteds
+
+ -- We always discard the extra avails we've generated;
+ -- but we remember if we have done any (global) improvement
+ ; let ret_avails = updateImprovement orig_avails avails
+
+ ; if isEmptyLHsBinds binds then -- No progress
+ return (ret_avails, NoInstance)
+ else do
+ { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
+ -- This binding is useless if the recursive simplification
+ -- made no progress; but currently we don't try to optimise that
+ -- case. After all, we only try hard to reduce at top level, or
+ -- when inferring types.
+
+ ; let dict_ids = map instToId extra_givens
+ co = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind)
+ 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
+ ; return (ret_avails, GenInst implic_insts (L loc rhs))
+ } }