| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
GHC.Tc.Utils.Concrete
Description
Checking for representation-polymorphism using the Concrete mechanism.
This module contains the logic for enforcing the representation-polymorphism invariants by way of emitting constraints.
Synopsis
- hasFixedRuntimeRep :: HasDebugCallStack => FixedRuntimeRepContext -> TcType -> TcM (TcCoercionN, TcTypeFRR)
- hasFixedRuntimeRep_syntactic :: HasDebugCallStack => FixedRuntimeRepContext -> TcType -> TcM ()
- unifyConcrete :: HasDebugCallStack => FastString -> ConcreteTvOrigin -> TcType -> TcM TcMCoercionN
- idConcreteTvs :: TcId -> ConcreteTyVars
Ensuring that a type has a fixed runtime representation
Arguments
| :: HasDebugCallStack | |
| => FixedRuntimeRepContext | Context to be reported to the user
if the type ends up not having a fixed
|
| -> TcType | The type to check (we only look at its kind). |
| -> TcM (TcCoercionN, TcTypeFRR) |
|
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 Source #
Arguments
| :: HasDebugCallStack | |
| => FixedRuntimeRepContext | Context to be reported to the user
if the type does not have a syntactically
fixed |
| -> 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 Source #
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 Source #
Which type variables of this Id must be concrete when instantiated?
See Note [Representation-polymorphism checking built-ins]