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

Making a type concrete

makeTypeConcrete :: ConcreteTvOrigin -> TcType -> TcM (TcType, [NotConcreteReason])

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

Returns a zonked type which is "as concrete as possible", and a list of problems encountered when trying to make it concrete.

INVARIANT: the returned type is equal to the input type, up to zonking. INVARIANT: if this function returns an empty list of NotConcreteReasons, then the returned type is concrete, in the sense of Note [Concrete types].