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

:: FRROrigin

Context to be reported to the user if the type ends up not having a fixed RuntimeRep (unsolved Wanted constraint).

-> TcType

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

-> TcM (Maybe (TcType, TcCoercion, TcTyVar))

Just ( ki, co, concrete_tv ) where co :: ki ~# concrete_ty is evidence that the type ty :: ki has a fixed RuntimeRep, or Nothing if ki responds True to isConcrete, (i.e. we can take co = Refl).

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 :: ki ~# concrete_tv as evidence. If ty obviously has a fixed RuntimeRep, e.g ki = IntRep, then this function immediately returns Nothing instead of emitting a new constraint.

hasFixedRuntimeRep_MustBeRefl :: FRROrigin -> TcType -> TcM ()

Like hasFixedRuntimeRep, but we insist that the obtained coercion must be Refl.

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. See Note [IsRefl#].

The goal is to eliminate all uses of this function and replace them with hasFixedRuntimeRep, making use of the returned coercion.