Hello GHC friends,

The documentation for Any says:

> The type constructor Any is type to which you can unsafely coerce
> any lifted type, and back. More concretely, for a lifted type t and
> value x :: t, unsafeCoerce (unsafeCoerce x :: Any) :: t is
> equivalent to x.

https://www.stackage.org/haddock/lts-24.28/base-4.20.2.0/GHC-Base.html#t:Any

Is this also true of type constructors? For example, could I
unsafeCoerce `f x` to `Any x`? (assuming f maps lifted types to lifted
types)

In particular I'm interested in things like


{-# LANGUAGE QuantifiedConstraints #-}

import GHC.Exts (Any)
import Data.Kind (Type)
import Unsafe.Coerce (unsafeCoerce)

data C (f :: Type -> Type -> Type) where
  MkC :: (forall a. Monad (f a)) => C f

newtype CD (f :: Type -> Type -> Type) = MkCD (C Any)

putCD :: C f -> CD f
putCD c = MkCD (unsafeCoerce c)

getCD :: CD f -> C f
getCD (MkCD cd) = unsafeCoerce cd


Is that sound? Thanks (and additional thanks to Andreas Klebinger for
having a look at this on haskell-cafe),

Tom
_______________________________________________
ghc-devs mailing list -- ghc-devs@haskell.org
To unsubscribe send an email to ghc-devs-leave@haskell.org