Use `withDict` for `reify` & co.

[int-e]

I've found out today that ghc (since version 7.8) implements dictionary reification for type literals with the help of some compiler magic. For example (see GHC.TypeLits):

newtype SSymbol (s :: Symbol) = SSymbol String

data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b)

-- See Note [magicDictId magic] in "basicType/MkId.hs"
withSSymbol :: (KnownSymbol a => Proxy a -> b)
            -> SSymbol a      -> Proxy a -> b
withSSymbol f x y = magicDict (WrapS f) x y

In a nutshell, the compiler magic is that there's a builtin rewrite rule that turns magicDict (WrapS f) x y into the moral equivalent of f (coerce x) y on the Core level, where dictionaries are represented as values (see MkId:Note [magicDictId magic]). This is actually better than what we get with the unsafeCoerce trick: rather than coercing f, it merely coerces the dictionary itself, so f can potentially be optimized more.

In light of this advantage, would it make sense for Data.Reflection to use magicDict as well?

It should be possible to tackle this together with #26.

[RyanGlScott]

Can you provide an example of a program where using magicDict would enable more optimization that the existing unsafeCoerce approach would? If I understand how magicDict works correctly, then this program shows the two approaches side by side:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Foo where

import Data.Proxy
import GHC.Exts
import GHC.TypeLits
import Unsafe.Coerce

newtype MagicSymbol r = MagicSymbol (forall (n :: Symbol). KnownSymbol n => Proxy n -> r)

reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
reifySymbol n k = unsafeCoerce (MagicSymbol k :: MagicSymbol r) n Proxy

data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b)

reifySymbol' :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
reifySymbol' n k = magicDict (WrapS k) n Proxy

However, if I look at the resulting Core:

$ /opt/ghc/8.6.5/bin/ghc Foo.hs -fforce-recomp -O2 -ddump-simpl -dsuppress-idinfo -dsuppress-coercions
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o )

==================== Tidy Core ====================
Result size of Tidy Core
  = {terms: 121, types: 97, coercions: 22, joins: 0/0}

-- RHS size: {terms: 6, types: 17, coercions: 18, joins: 0/0}
reifySymbol
  :: forall r.
     String
     -> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
reifySymbol
  = \ (@ r_a1lo)
      (n_a17J :: String)
      (k_a17K
         :: forall (n1 :: Symbol). KnownSymbol n1 => Proxy n1 -> r_a1lo) ->
      (k_a17K `cast` <Co:18>) n_a17J (Data.Proxy.Proxy @ Any @ Any)

-- RHS size: {terms: 6, types: 19, coercions: 4, joins: 0/0}
reifySymbol'
  :: forall r.
     String
     -> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
reifySymbol'
  = \ (@ r_a1kX)
      (n_a17L :: String)
      (k_a17M
         :: forall (n1 :: Symbol). KnownSymbol n1 => Proxy n1 -> r_a1kX) ->
      k_a17M @ Any (n_a17L `cast` <Co:4>) (Data.Proxy.Proxy @ Any @ Any)

The only appreciable difference seems to be the particular location of the cast, which (IIUC) shouldn't make any difference at runtime.

I'm not saying that I don't believe there isn't some program out there that might benefit from this, but it's not clear to me at present what that would be.

[int-e]

Thanks for the skepticism! It turns out that ghc is more clever when dealing with unsafeCoerce-d functions than I imagined. Consider the following code.

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
module Bar (test1, test2) where

import Data.Proxy
import GHC.Exts
import GHC.TypeLits
import Unsafe.Coerce

-- from Data.Reflection
class Given a where
  given :: a

newtype Gift a r = Gift (Given a => r)

give :: forall a r. a -> (Given a => r) -> r
give a k = unsafeCoerce (Gift k :: Gift a r) a

-- reimplementation using `magicDict`
data WrapGift a b = WrapGift (Given a => Proxy a -> b)

withGift :: (Given a => Proxy a -> b) -> a -> Proxy a -> b
withGift f x y = magicDict (WrapGift f) x y

give' :: forall a r. a -> (Given a => r) -> r
give' a k = withGift (\_ -> k) a Proxy

-- test
foo :: Given Int => Bool -> Int
foo True  = 42
foo False = given

test1 = give  (23 :: Int) foo True
test2 = give' (23 :: Int) foo True

I expected to see a difference between test1 and test2. In fact with ghc -O0, the code for test2 is (surprisingly!) just

test2 = GHC.Types.I# 42#

while test1 is not simplified; the True remains outside the unsafeCoerce, and the dictionary passed to foo is treated as unknown and foo is not inlined. But the difference disappears once optimization is enabled; in fact, ghc de-duplicates the code and generates test2 = test1.

Other observations:

• the magicDict version doesn't play nicely with ghci which will complain about not finding ghczmprim_GHCziPrim_magicDict_closure
• less relevantly, ghc-8.0 actually breaks the magicDict version when optimizations are enabled

So overall there appears to be no reason to change the existing code. One remaining advantage of the magicDict version is that it never produces unsafe coercions at the Core level, but that is more than outweighed by it being harder to understand and brittle with ghci. Moreover, it's a GHC internal API that may change with a new release.

@RyanGlScott: Sorry for wasting your time! I should've checked my hypotheses before creating the ticket. (The reason was that I was tired but still wanted to record the idea somewhere so I wouldn't forget.)

[RyanGlScott]

The situation in now different in GHC 9.0.1, which produces different Core in the example from #44 (comment):

$ /opt/ghc/9.0.1/bin/ghc Foo.hs -fforce-recomp -O2 -ddump-simpl -dsuppress-idinfo -dsuppress-coercions -dno-typeable-binds
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o )

==================== Tidy Core ====================
Result size of Tidy Core
  = {terms: 17, types: 102, coercions: 11, joins: 0/0}

-- RHS size: {terms: 9, types: 61, coercions: 7, joins: 0/0}
reifySymbol
  :: forall r.
     String
     -> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
reifySymbol
  = \ (@r_aEG)
      (n_aAd :: String)
      (k_aAe
         :: forall (n1 :: Symbol). KnownSymbol n1 => Proxy n1 -> r_aEG) ->
      case unsafeEqualityProof
             @(*) @(MagicSymbol r_aEG) @(String -> Proxy Any -> r_aEG)
      of
      { UnsafeRefl co_aFp ->
      (k_aAe `cast` <Co:7>) n_aAd (Data.Proxy.Proxy @Any @Any)
      }

-- RHS size: {terms: 6, types: 19, coercions: 4, joins: 0/0}
reifySymbol'
  :: forall r.
     String
     -> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
reifySymbol'
  = \ (@r_aEd)
      (n_aAf :: String)
      (k_aAg
         :: forall (n1 :: Symbol). KnownSymbol n1 => Proxy n1 -> r_aEd) ->
      k_aAg @Any (n_aAf `cast` <Co:4>) (Data.Proxy.Proxy @Any @Any)

reifySymbol', which uses magicDict, continues to use produce the same Core as in GHC 8.6.5. reifySymbol, which uses unsafeCoerce, produces worse Core, however, as it now must explicitly case on unsafeEqualityProof. This suggests that implementing reify in terms of magicDict could offer a mild performance boost.

I'll reopen this issue to track implementing this idea. As @int-e notes, however, the magicDict version breaks in GHCi. I've opened GHC#19667 to track this. This issue gives me pause, as I'd hate to break things for GHCi users, so perhaps we should wait until that bug is fixed before pursuing this further.

[phadej]

Note, GHCi problem is when you try to interpret the module using magicDict. But if it's used in compiled dependency (e.g. base) it's fine. So it only would break GHCi for developers of reflection, which is few. (Still annoying).

[RyanGlScott]

A status update, since much has happened since the last comment:

• GHC has now implemented withDict, a replacement for magicDict that is much less error-prone to use. withDict will debut in GHC 9.4
• Moreover, using withDict no longer breaks GHCi after GHC#19667 was fixed.
• It's possible to implement some parts of reflection using withDict today. In particular, the reify and give functions prove straightforward to implement on top of withDict. I've pushed a proof-of-concept to the T44 branch. The parts that we cannot implement yet are reifyNat and reifySymbol, since GHC.TypeLits does not export everything that we need. See GHC#21568 (specifically, point (2)) for more details. (EDIT: This is out of date, as this was done in Use new, safer GHC.TypeLits API to define reify{Nat,Symbol} #53.)
• I haven't submitted a PR for the T44 branch because those changes break the reflection test suite. See GHC#21575. I'm going to wait for a resolution to that issue before proceeding.

[ekmett]

... and with GHC#21575 it looks like the groundhog sees its shadow once again. I wonder when we'll ever get this hooked up to the 'official' mechanism.