GHC.Tc.Utils.Unify

A version of tcWrapResult to use when the actual type is a rho-type, so nothing to instantiate; just go straight to unify. It means we don't need to pass in a CtOrigin.

Checks that the actual type is more polymorphic than the expected type.

Connect up the inferred type of an application with the expected type. This is usually just a unification, but with deep subsumption there is more to do.

Variant of getDeepSubsumptionFlag which enables a top-level subsumption in order to implement the plan of Note [Typechecking data constructors].

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.

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].

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].

Perform the checks specified by the TyEqFlags on the RHS, in order to enforce the unification preconditions of Note [Unification preconditions].

See Note [checkTyEqRhs].

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

Create a "not unifying" TyEqFlags from a CanEqLHS.

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

Create "unifying" TyEqFlags from a TyVarLHS.

Invariant: the argument TcTyVar is a MetaTv.

TyEqFlags for a pure call of checkTyEqRhs.

A call to checkTyEqRhs with these TyEqFlags will perform an optimistic check: it will return PuFail if there is definitely a problem, but it might return PuOK if it isn't entirely sure.

What level check to perform, in a call to the pure unifier? A defunctionalisation of the possible level-check functions Interpreter: tyVarLevelCheck

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]

A defunctionalisation of family application breaker functions. Interpreter: famAppBreaker

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 IFRR_Check, t2 is guaranteed to have a syntactically fixed RuntimeRep, in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.