GHC.Tc.Solver.Rewrite

Documentation

rewrite :: CtEvidence -> TcType -> TcS (Reduction, RewriterSet)

See Note [Rewriting]. If (xi, co, rewriters) <- rewrite mode ev ty, then co :: xi ~r ty where r is the role in ev. rewriters is the set of coercion holes that have been used to rewrite See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint

rewriteForErrors :: CtEvidence -> TcType -> TcS (Reduction, RewriterSet)

See Note [Rewriting] rewriteForErrors is a variant of rewrite that rewrites w.r.t. nominal equality only, as this is better than full rewriting for error messages. (This was important when we flirted with rewriting newtypes but perhaps less so now.)

rewriteArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS (Reductions, RewriterSet)

rewriteType :: CtLoc -> TcType -> TcS TcType

Rewrite a type w.r.t. nominal equality. This is useful to rewrite a type w.r.t. any givens. It does not do type-family reduction. This will never emit new constraints. Call this when the inert set contains only givens.