Because you have to actually compute `Refl` for it to be valid. Consirer a lie :: a :~: b lie = lie When you match on `lie` to get a proof of `a ~ b`, it will loop, so you won't make unsafeCoerce out of a thin air. Your a :~:# b doesn't work. you cannot define unboxedRefl: Top-level bindings for unlifted types aren't allowed: unboxedRefl = Refl (##) Also a ~ b is *boxed* constraint, so you need to create it e.g. unUnboxedRefl :: forall a b r. a :~:# b -> (a ~ b => r) -> r unUnboxedRefl (URefl (# #)) r = case unsafeCoerce (Refl :: a :~: a) :: a :~: b of Refl -> r Then you could (try to) have a local lie: myUnsafeCoerce :: forall a b. a -> b myUnsafeCoerce a = let lie :: a :~:# b lie = lie in unUnboxedRefl lie a GHC won't accept it (Recursive bindings for unlifted types aren't allowed: lie = lie). In summary, GHC tries hard to not let you define unsafeCoerce. On 12.1.2023 17.12, Tom Ellis wrote:
Subsequent to Bertram's helpful answer about the unboxed unit tuple as an argument type, I have a follow-up question.
Data.Typeable allows me to write a nice API like refl/unRefl below:
{-# LANGUAGE GHC2021 #-} {-# LANGUAGE LambdaCase #-}
module Example where
import Data.Typeable
refl :: a :~: a refl = Refl
unRefl :: a :~: b -> (a ~ b => r) -> r unRefl = \case Refl -> \r -> r
But why I am paying the cost for a boxed argument to unRefl? Is there an alternative API using an unboxed, zero-width equality witness that means I pay minimal cost for its existence? That is, an API like the following where `a :~:# b` is zero-width unboxed?
unboxedRefl :: a :~:# a
unUnboxedRefl :: a :~:# b -> (a ~ b => r) -> r
I guess I can do it the following unpleasant way, if I keep the constructor hidden. But is there a better way?
newtype a :~:# a = Refl (# #)
unboxedRefl :: a :~:# a unboxedRefl = Refl (# #)
unUnboxedRefl :: a :~:# b -> (a ~ b => r) -> r unUnboxedRefl (Refl (# #)) = unsafeCoerce
Tom
On Thu, Jan 12, 2023 at 04:01:48PM +0100, Bertram Felgenhauer via Haskell-Cafe wrote:
Tom Ellis wrote:
If I define bar and baz as below then, as I understand it, calling baz requires pushing an argument onto the machine stack. Is the same true for baz, or is "calling" baz the same as "calling" foo, i.e. no argument needs to be pushed?
{-# LANGUAGE MagicHash #-} {-# LANGUAGE UnboxedTuples #-}
module Bar where
import GHC.Prim
foo :: Int foo = 1
bar :: (# #) -> Int bar (# #) = 1
baz :: () -> Int baz () = 0 There is more to the story than just arguments. Assuming that nothing gets inlined,
- "calling" foo simply uses the existing `foo` closure (at the top level it becomes a static indirection)
- calling baz pushes an update frame recording where the result goes onto the stack and the argument as well, and calls the entry point for `baz`. Well, conceptually. Actually, the argument is passed in a register on x86_64.
- calling bar pushes an update frame, but does not push or pass an argument to the entry point of `bar`.
This is specific to `(# #)` being the final argument of the function. For intermediate arguments, the argument is just skipped. So if you had
foo :: Int -> Int foo x = x + 42
bar :: (# #) -> Int -> Int bar (# #) x = x + 42
then `foo 1` and `bar (# #) 1` produce identical same code.
If the arity of the function is unknown, as in
xyzzy :: ((# #) -> a) -> a xyzzy f = f (# #)
xyzzy :: (() -> a) -> a xyzzy f = f ()
then the distinction is delegated to a helper function in the RTS (`stg_ap_v_fast` vs. `stg_ap_p_fast`; `v` stands for "void", while `p` stands for "pointer") that inspects the info table of the `f` closure to determine whether the argument is the final one that needs special treatment, or whether the argument can simply be skipped.
Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.