+\begin{code}
+
+solveCTyFunEqs :: CanonicalCts -> Bag Implication -> TcS (Bag WantedEvVar, Bag Implication)
+-- 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 implics
+ = do { untch <- getUntouchables
+ ; let (unsolved_can_cts, funeq_bnds) = getSolvableCTyFunEqs untch cts
+ ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
+ , ppr funeq_bnds
+ ])
+ ; mapM_ solve_one funeq_bnds
+
+ -- Apply the substitution through to eliminate the flatten
+ -- unification variables we substituted both in the unsolved flats and implics
+ ; let final_unsolved
+ = Bag.mapBag (subst_wevar funeq_bnds . deCanonicaliseWanted) unsolved_can_cts
+ final_implics
+ = Bag.mapBag (subst_impl funeq_bnds) implics
+
+ ; return (final_unsolved, final_implics) }
+
+ where solve_one (tv,(ty,cv,fl))
+ | not (typeKind ty `isSubKind` tyVarKind tv)
+ = addErrorTcS KindError fl (mkTyVarTy tv) ty
+ -- Must do a small kind check since TcCanonical invariants
+ -- on family equations only impose compatibility, not subkinding
+ | otherwise = setWantedTyBind tv ty >> setWantedCoBind cv ty
+
+ subst_wanted :: FunEqBinds -> WantedConstraint -> WantedConstraint
+ subst_wanted funeq_bnds (WcEvVar wv) = WcEvVar (subst_wevar funeq_bnds wv)
+ subst_wanted funeq_bnds (WcImplic impl) = WcImplic (subst_impl funeq_bnds impl)
+
+ subst_wevar :: FunEqBinds -> WantedEvVar -> WantedEvVar
+ subst_wevar funeq_bnds (WantedEvVar v loc)
+ = let orig_ty = varType v
+ new_ty = substFunEqBnds funeq_bnds orig_ty
+ in WantedEvVar (setVarType v new_ty) loc
+
+ subst_impl :: FunEqBinds -> Implication -> Implication
+ subst_impl funeq_bnds impl@(Implic { ic_wanted = ws })
+ = impl { ic_wanted = Bag.mapBag (subst_wanted funeq_bnds) ws }
+
+
+type FunEqBinds = [(TcTyVar,(TcType,CoVar,CtFlavor))]
+-- Invariant: if it contains:
+-- [... a -> (ta,...) ... b -> (tb,...) ... ]
+-- then 'ta' cannot mention 'b'
+
+getSolvableCTyFunEqs :: Untouchables
+ -> CanonicalCts -- Precondition: all wanteds
+ -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables
+getSolvableCTyFunEqs untch cts
+ = Bag.foldlBag dflt_funeq (emptyCCan, []) cts
+ where dflt_funeq (cts_in, extra_binds) ct@(CFunEqCan { cc_id = cv
+ , cc_flavor = fl
+ , cc_fun = tc
+ , cc_tyargs = xis
+ , cc_rhs = xi })
+ | Just tv <- tcGetTyVar_maybe xi
+ , isTouchableMetaTyVar_InRange untch tv -- If RHS is a touchable unif. variable
+ , Nothing <- lookup tv extra_binds -- or in extra_binds
+ -- See Note [Solving Family Equations], Point 1
+ = ASSERT ( isWanted fl )
+ let ty_orig = mkTyConApp tc xis
+ ty_bind = substFunEqBnds extra_binds ty_orig
+ in if tv `elemVarSet` tyVarsOfType ty_bind
+ then (cts_in `extendCCans` ct, extra_binds)
+ -- See Note [Solving Family Equations], Point 2
+ else (cts_in, (tv,(ty_bind,cv,fl)):extra_binds)
+ -- Postcondition met because extra_binds is already applied to ty_bind
+
+ dflt_funeq (cts_in, extra_binds) ct = (cts_in `extendCCans` ct, extra_binds)
+
+substFunEqBnds :: FunEqBinds -> TcType -> TcType
+substFunEqBnds bnds ty
+ = foldr (\(x,(t,_cv,_fl)) xy -> substTyWith [x] [t] xy) ty bnds
+ -- foldr works because of the FunEqBinds invariant
+
+
+\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.
+
+
projects / ghc-hetmet.git / blobdiff