Can we get inlining with a skolem? #31
Description
Currently, reflection clogs up the inliner pretty badly. The following modification seems to fix this, but there could be some gotcha somewhere.
data Skolem = Skolem
newtype Magic a r = Magic (Reifies Skolem a => Proxy Skolem -> r)The function passed to reify, of type forall (s :: *). Reifies s a => Proxy s -> r, can certainly be passed to Magic (automatically instantiating s to Skolem).
For example, using this definition,
foo :: Int -> Int
foo x = reify (5 :: Int) $ \(p :: Proxy s) -> reflect p + xyields
foo :: Int -> Int
foo =
\ (x_a4WB :: Int) ->
case ((\ _ -> I# 5) `cast` ...) ((Proxy) `cast` ...)
of _ { I# x1_a9qY ->
case x_a4WB of _ { I# y_a9r2 -> I# (+# x1_a9qY y_a9r2) }
}The only remaining traces of reflection are the Proxy and the failure to unbox 5. Note that Tagged-based reflection manages to get rid of absolutely all traces even when Proxy-based reflection is built on top of it:
class Reifies s a | s -> a where
reflect' :: Tagged s a
data Skolem = Skolem
newtype Magic a r = Magic (Reifies Skolem a => Tagged Skolem r)
reify' :: forall a r . a -> (forall (s :: *) . Reifies s a => Tagged s r) -> r
reify' a k = unsafeCoerce (Magic k :: Magic a r) a
{-# INLINE reify' #-}
reflect :: Reifies s a => proxy s -> a
reflect = proxy reflect'
{-# INLINE reflect #-}
reify :: forall a r . a -> (forall (s :: *) . Reifies s a => Proxy s -> r) -> r
reify a k = reify' a (unproxy k)
{-# INLINE reify #-}With these definitions, foo compiles to
foo :: Int -> Int
foo =
\ (x_aDk :: Int) ->
case x_aDk of _ { I# y_a12D -> I# (+# 5 y_a12D) }