Documentation

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

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

Try to turn the provided type into a concrete type, by ensuring unfilled metavariables are appropriately marked as concrete.

Returns a coercion whose RHS is a zonked type which is "as concrete as possible", and a collection of Wanted equality constraints that are necessary to make the type concrete.

For example, for an input TYPE a[sk] we will return a coercion with RHS TYPE gamma[conc] together with the Wanted equality constraint a ~# gamma.

INVARIANT: the RHS type of the returned coercion is equal to the input type, up to zonking and the returned Wanted equality constraints.

INVARIANT: if this function returns an empty list of constraints then the RHS type of the returned coercion is concrete, in the sense of Note [Concrete types].

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

The structure of the LHS and which checks to perform in checkTyEqRhs, for an equality lhs ~# rhs.

See Note [TEFTask].

Create a "not unifying" TEFTask from a CanEqLHS.

See use-case (1) in Note [TEFTask].

Create "unifying" TEFTask from a TyVarLHS.

Invariant: the argument TyVar is a MetaTv.

What level check to perform, in a call to the pure unifier?

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]

Adjust the TyEqFlags when going undter a type family:

1. Only the outer family application gets the loop-breaker treatment
2. Weaken level checks for tyvar promotion. For example, in [W] alpha[2] ~ Maybe (F beta[3]), do not promote beta[3], instead promote (F beta[3]).
3. Occurs checks become potentially soluble (after additional type family reductions).

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.