Refl package:ghc

Maximum level of refinement for refinement hole fits in typed hole error messages

Reflect a computation in the Ghc monad into the IO monad. You can use this to call functions returning an action in the Ghc monad inside an IO action. This is needed for some (too restrictive) callback arguments of some library functions:

libFunc :: String -> (Int -> IO a) -> IO a
ghcFunc :: Int -> Ghc a

ghcFuncUsingLibFunc :: String -> Ghc a -> Ghc a
ghcFuncUsingLibFunc str =
reifyGhc $ \s ->
libFunc $ \i -> do
reflectGhc (ghcFunc i) s

Tests if this coercion is obviously a generalized reflexive coercion. Guaranteed to work very quickly.

Returns the type coerced if this coercion is a generalized reflexive coercion. Guaranteed to work very quickly.

Tests if this MCoercion is obviously generalized reflexive Guaranteed to work very quickly.

Tests if this coercion is obviously reflexive. Guaranteed to work very quickly. Sometimes a coercion can be reflexive, but not obviously so. c.f. isReflexiveCo

Returns the type coerced if this coercion is reflexive. Guaranteed to work very quickly. Sometimes a coercion can be reflexive, but not obviously so. c.f. isReflexiveCo_maybe

Slowly checks if the coercion is reflexive. Don't call this in a loop, as it walks over the entire coercion.

Extracts the coerced type from a reflexive coercion. This potentially walks over the entire coercion, so avoid doing this in a loop.

Make a generalized reflexive coercion

Given r, ty :: k1, and co :: k1 ~N k2, produces co' :: (ty |> co) ~r ty

Given ty :: k1, co :: k1 ~ k2, produces co' :: ty ~r (ty |> co)

Make a nominal reflexive coercion

Make a reflexive coercion

Make a representational reflexive coercion