Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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 ()
- makeTypeConcrete :: ConcreteTvOrigin -> TcType -> TcM (TcType, [NotConcreteReason])
Ensuring that a type has a fixed runtime representation
:: 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 #
:: 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].
Making a type concrete
makeTypeConcrete :: ConcreteTvOrigin -> TcType -> TcM (TcType, [NotConcreteReason]) Source #
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].