GHC.Tc.Utils.Concrete

Checking for representation-polymorphism using the Concrete mechanism.

This module contains the logic for enforcing the representation-polymorphism invariants by way of emitting constraints.

Ensuring that a type has a fixed runtime representation

hasFixedRuntimeRep

Arguments

:: HasDebugCallStack

=> FixedRuntimeRepContext

Context to be reported to the user if the type ends up not having a fixed RuntimeRep.

-> TcType

The type to check (we only look at its kind).

-> TcM (TcCoercionN, TcTypeFRR)

(co, ty') where ty' :: ki', ki is concrete, and co :: ty ~# ty'. That is, ty' has a syntactically fixed RuntimeRep in the sense of Note [Fixed RuntimeRep].

Given a type ty :: ki, this function ensures that ty has a fixed RuntimeRep, by emitting a new equality constraint ki ~ concrete_tv for a concrete metavariable concrete_tv.

Returns a coercion co :: ty ~# concrete_ty as evidence. If ty obviously has a fixed RuntimeRep, e.g ki = IntRep, then this function immediately returns MRefl, without emitting any constraints.

hasFixedRuntimeRep_syntactic

Arguments

:: HasDebugCallStack

=> FixedRuntimeRepContext

Context to be reported to the user if the type does not have a syntactically fixed RuntimeRep.

-> TcType

The type to check (we only look at its kind).

-> TcM ()

Like hasFixedRuntimeRep, but we perform an eager syntactic check.

Throws an error in the TcM monad if the check fails.

This is useful if we are not actually going to use the coercion returned from hasFixedRuntimeRep; it would generally be unsound to allow a non-reflexive coercion but not actually make use of it in a cast.

The goal is to eliminate all uses of this function and replace them with hasFixedRuntimeRep, making use of the returned coercion. This is what is meant by going from PHASE 1 to PHASE 2, in Note [The Concrete mechanism].

unifyConcrete :: HasDebugCallStack => FastString -> ConcreteTvOrigin -> TcType -> TcM TcMCoercionN

Ensure that the given type ty can unify with a concrete type, in the sense of Note [Concrete types].

Returns a coercion co :: ty ~# conc_ty, where conc_ty is concrete.

If the type is already syntactically concrete, this immediately returns a reflexive coercion. Otherwise, it creates a new concrete metavariable concrete_tv and emits an equality constraint ty ~# concrete_tv, to be handled by the constraint solver.

Invariant: the kind of the supplied type must be concrete.

We assume the provided type is already at the kind-level (this only matters for error messages).

idConcreteTvs :: TcId -> ConcreteTyVars

Which type variables of this Id must be concrete when instantiated?

See Note [Representation-polymorphism checking built-ins] in GHC.Tc.Gen.Head.