1 files changed, 37 insertions, 18 deletions

diff --git a/compiler/GHC/Types/Id/Make.hs b/compiler/GHC/Types/Id/Make.hs
index 4e42fd734d..7001fac73b 100644
--- a/compiler/GHC/Types/Id/Make.hs
+++ b/compiler/GHC/Types/Id/Make.hs
@@ -1797,7 +1797,7 @@ The identifier `magicDict` is just a place-holder, which is used to
 implement a primitive that we cannot define in Haskell but we can write
 in Core.  It is declared with a place-holder type:
 
-    magicDict :: forall a. a
+    magicDict :: forall {rr :: RuntimeRep} dt st (r :: TYPE rr). (dt => r) -> st -> r
 
 The intention is that the identifier will be used in a very specific way,
 to create dictionaries for classes with a single method.  Consider a class
@@ -1810,34 +1810,53 @@ We are going to use `magicDict`, in conjunction with a built-in Prelude
 rule, to cast values of type `T a` into dictionaries for `C a`.  To do
 this, we define a function like this in the library:
 
-  data WrapC a b = WrapC (C a => Proxy a -> b)
+  withT :: (C a => b) -> T a -> b
+  withT f x y = magicDict @(C a) x y
 
-  withT :: (C a => Proxy a -> b)
-        ->  T a -> Proxy a -> b
-  withT f x y = magicDict (WrapC f) x y
+Here:
 
-The purpose of `WrapC` is to avoid having `f` instantiated.
-Also, it avoids impredicativity, because `magicDict`'s type
-cannot be instantiated with a forall.  The field of `WrapC` contains
-a `Proxy` parameter which is used to link the type of the constraint,
-`C a`, with the type of the `Wrap` value being made.
+* The `dt` in `magicDict` (short for "dictionary type") is instantiated to
+  `C a`. Note that the explicit type application is required, as the call to
+  `magicDict` would be ambiguous otherwise.
+
+* The `st` in `magicDict` (short for "singleton type") is instantiated to
+  `T a`. The definition of `T` itself is irrelevant, only that `C a` is a class
+  with a single method of type `T a`.
+
+* The `r` in `magicDict` is instantiated to `b`.
 
 Next, we add a built-in Prelude rule (see GHC.Core.Opt.ConstantFold),
 which will replace the RHS of this definition with the appropriate
 definition in Core.  The rewrite rule works as follows:
 
-  magicDict @t (wrap @a @b f) x y
+  magicDict @{rr} @dt @st @r k sv
 ---->
-  f (x `cast` co a) y
+  k (sv |> sym (co t_1 ... t_n))
+
+Where `dt = DT t_1 ... t_n`. The `co` coercion is the newtype coercion
+extracted from the type class DT.
+
+Some further observations about `magicDict`:
+
+* The `r` is levity polymorphic to support things like `withTypeable` in
+  `Data.Typeable.Internal`.
+
+* As an alternative to `magicDict`, one could define functions like `withT`
+  above in terms of `unsafeCoerce`. This is more error-prone, however, and
+  moreover, the Core that `unsafeCoerce` generates is likely to `case` on
+  `unsafeEqualityProof` at runtime. On the other hand, GHC can completely
+  optimize away `magicDict`.
+
+* In order to define things like `reifySymbol` below:
+
+    reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => r) -> r
 
-The `co` coercion is the newtype-coercion extracted from the type-class.
-The type class is obtained by looking at the type of wrap.
+  `magicDict` needs to be instantiated with `Any`, like so:
 
-In the constant folding rule it's very import to make sure to strip all ticks
-from the expression as if there's an occurence of
-magicDict we *must* convert it for correctness. See #19667 for where this went
-wrong in GHCi.
+    reifySymbol n k = magicDict @(KnownSymbol Any) @String @r (k @Any) n
 
+  The use of `Any` is explained in Note [NOINLINE someNatVal] in
+  base:GHC.TypeNats.
 
 -------------------------------------------------------------
 @realWorld#@ used to be a magic literal, \tr{void#}.  If things get