+'solveInteract' step first.
+
+Note [Extra TcsTv untouchables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Furthemore, we record the inert set simplifier-generated unification
+variables of the TcsTv kind (such as variables from instance that have
+been applied, or unification flattens). These variables must be passed
+to the implications as extra untouchable variables. Otherwise we have
+the danger of double unifications. Example (from trac ticket #4494):
+
+ (F Int ~ uf) /\ (forall a. C a => F Int ~ beta)
+
+In this example, beta is touchable inside the implication. The first
+solveInteract step leaves 'uf' ununified. Then we move inside the
+implication where a new constraint
+ uf ~ beta
+emerges. We may spontaneously solve it to get uf := beta, so the whole
+implication disappears but when we pop out again we are left with (F
+Int ~ uf) which will be unified by our final solveCTyFunEqs stage and
+uf will get unified *once more* to (F Int).
+
+The solution is to record the TcsTvs (i.e. the simplifier-generated
+unification variables) that are generated when solving the flats, and
+make them untouchables for the nested implication. In the example
+above uf would become untouchable, so beta would be forced to be
+unified as beta := uf.
+
+NB: A consequence is that every simplifier-generated TcsTv variable
+ that gets floated out of an implication becomes now untouchable
+ next time we go inside that implication to solve any residual
+ constraints. In effect, by floating an equality out of the
+ implication we are committing to have it solved in the outside.
+
+Note [Float Equalities out of Implications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We want to float equalities out of vanilla existentials, but *not* out
+of GADT pattern matches.
+
+
+\begin{code}
+
+solveCTyFunEqs :: CanonicalCts -> TcS (TvSubst, CanonicalCts)
+-- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
+-- See Note [Solving Family Equations]
+-- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications
+-- where the newly generated equalities (alpha := F xi) have been substituted through.
+solveCTyFunEqs cts
+ = do { untch <- getUntouchables
+ ; let (unsolved_can_cts, (ni_subst, cv_binds))
+ = getSolvableCTyFunEqs untch cts
+ ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
+ , ppr ni_subst, ppr cv_binds
+ ])
+ ; mapM_ solve_one cv_binds
+
+ ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
+ where
+ solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setCoBind cv ty
+
+------------
+type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
+ -- The TvSubstEnv is not idempotent, but is loop-free
+ -- See Note [Non-idempotent substitution] in Unify
+emptyFunEqBinds :: FunEqBinds
+emptyFunEqBinds = (emptyVarEnv, [])
+
+extendFunEqBinds :: FunEqBinds -> CoVar -> TcTyVar -> TcType -> FunEqBinds
+extendFunEqBinds (tv_subst, cv_binds) cv tv ty
+ = (extendVarEnv tv_subst tv ty, (cv, tv, ty):cv_binds)
+
+------------
+getSolvableCTyFunEqs :: TcsUntouchables
+ -> CanonicalCts -- Precondition: all Wanteds or Derived!
+ -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables
+getSolvableCTyFunEqs untch cts
+ = Bag.foldlBag dflt_funeq (emptyCCan, emptyFunEqBinds) cts
+ where
+ dflt_funeq :: (CanonicalCts, FunEqBinds) -> CanonicalCt
+ -> (CanonicalCts, FunEqBinds)
+ dflt_funeq (cts_in, feb@(tv_subst, _))
+ (CFunEqCan { cc_id = cv
+ , cc_flavor = fl
+ , cc_fun = tc
+ , cc_tyargs = xis
+ , cc_rhs = xi })
+ | Just tv <- tcGetTyVar_maybe xi -- RHS is a type variable
+
+ , isTouchableMetaTyVar_InRange untch tv
+ -- And it's a *touchable* unification variable
+
+ , typeKind xi `isSubKind` tyVarKind tv
+ -- Must do a small kind check since TcCanonical invariants
+ -- on family equations only impose compatibility, not subkinding
+
+ , not (tv `elemVarEnv` tv_subst)
+ -- Check not in extra_binds
+ -- See Note [Solving Family Equations], Point 1
+
+ , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
+ -- Occurs check: see Note [Solving Family Equations], Point 2
+ = ASSERT ( not (isGiven fl) )
+ (cts_in, extendFunEqBinds feb cv tv (mkTyConApp tc xis))
+
+ dflt_funeq (cts_in, fun_eq_binds) ct
+ = (cts_in `extendCCans` ct, fun_eq_binds)
+\end{code}
+
+Note [Solving Family Equations]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+After we are done with simplification we may be left with constraints of the form:
+ [Wanted] F xis ~ beta
+If 'beta' is a touchable unification variable not already bound in the TyBinds
+then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
+
+When is it ok to do so?
+ 1) 'beta' must not already be defaulted to something. Example:
+
+ [Wanted] F Int ~ beta <~ Will default [beta := F Int]
+ [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We
+ have to report this as unsolved.
+
+ 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
+ set [beta := F xis] only if beta is not among the free variables of xis.
+
+ 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
+ of type family equations. See Inert Set invariants in TcInteract.
+