Safe Haskell	None
Language	Haskell2010

GHC.Tc.Utils.Concrete

Contents

Ensuring that a type has a fixed runtime representation

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 ()

Ensuring that a type has a fixed runtime representation

hasFixedRuntimeRep Source #

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 Source #

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