Documentation

The wrapper has type: spec_ty ~> expected_ty See Note [Skolemisation] for the differences between tcSkolemiseCompleteSig and tcTopSkolemise

This is the key test for untouchability: See Note [Unification preconditions] in GHC.Tc.Utils.Unify and Note [Solve by unification] in GHC.Tc.Solver.Equality

True = the variable is touchable

checkTopShape checks (TYVAR-TV) Note [Unification preconditions]; returns True if these conditions are satisfied. But see the Note for other preconditions, too.

Infer a type using a fresh ExpType See also Note [ExpType] in GHC.Tc.Utils.TcMType

Use tcInferFRR if you require the type to have a fixed runtime representation.

Use this function to split off arguments types when you have an "expected" type.

This function skolemises at each polytype.

Invariant: this function only applies the provided function to a list of argument types which all have a syntactically fixed RuntimeRep in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. See Note [Return arguments with a fixed RuntimeRep].

Breaks apart a function kind into its pieces.

matchActualFunTy looks for just one function arrow, returning an uninstantiated sigma-type.

Invariant: the returned argument type has a syntactically fixed RuntimeRep in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.

See Note [Return arguments with a fixed RuntimeRep].

Like matchExpectedFunTys, but used when you have an "actual" type, for example in function application.

INVARIANT: the returned argument types all have a syntactically fixed RuntimeRep in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. See Note [Return arguments with a fixed RuntimeRep].

Options describing how to deal with a type equality in the pure unifier. See checkTyEqRhs

What to do when encountering a type-family application while processing a type equality in the pure unifier.

See Note [Family applications in canonical constraints]

How to break a family-application cycle when checking a type equality. Given a family-application fam_app, return a Reduction :: fam_app ~ cbv where cbv is a fresh cycle-breaker tyvar (for Given), or a fresh TauTv (for Wanted).

A fast check for unification. May return "not sure", in which case unification might still be OK, but it'll take more work to do (use the full checkTypeEq).

• Rejects if lhs_tv occurs in rhs_ty (occurs check)
• Rejects foralls unless lhs_tv is RuntimeUnk (used by GHCi debugger) or is a QL instantiation variable
• Rejects a non-concrete type if lhs_tv is concrete
• Rejects type families unless fam_ok=True
• Does a level-check for type variables, to avoid skolem escape

This function is pretty heavily used, so it's optimised not to allocate

The result type of simpleUnifyCheck.

Fill an InferResult with the given type.

If co = fillInferResult t1 infer_res, then co :: t1 ~# t2, where t2 is the type stored in the ir_ref field of infer_res.

This function enforces the following invariants:

• Level invariant. The stored type t2 is at the same level as given by the ir_lvl field.
• FRR invariant. Whenever the ir_frr field is not Nothing, t2 is guaranteed to have a syntactically fixed RuntimeRep, in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.