WIP: Redesign the type of magicDictwip/T16646-take-one

This doesn't work yet—see https://gitlab.haskell.org/ghc/ghc/-/issues/16646#note_346249.

[ci skip]

11 files changed, 175 insertions, 47 deletions

diff --git a/compiler/GHC/Core/Opt/ConstantFold.hs b/compiler/GHC/Core/Opt/ConstantFold.hs
index 2eb86f87f3..2029647dde 100644
--- a/compiler/GHC/Core/Opt/ConstantFold.hs
+++ b/compiler/GHC/Core/Opt/ConstantFold.hs
@@ -53,7 +53,7 @@ import GHC.Core.TyCon
    , tyConFamilySize )
 import GHC.Core.DataCon ( dataConTagZ, dataConTyCon, dataConWrapId, dataConWorkId )
 import GHC.Core.Utils  ( eqExpr, cheapEqExpr, exprIsHNF, exprType
-                       , stripTicksTop, stripTicksTopT, mkTicks, stripTicksE )
+                       , stripTicksTop, stripTicksTopT, mkTicks )
 import GHC.Core.Multiplicity
 import GHC.Core.FVs
 import GHC.Core.Type
@@ -1740,7 +1740,7 @@ builtinRules
      BuiltinRule { ru_name = fsLit "Inline", ru_fn = inlineIdName,
                    ru_nargs = 2, ru_try = \_ _ _ -> match_inline },
      BuiltinRule { ru_name = fsLit "MagicDict", ru_fn = magicDictName,
-                   ru_nargs = 4, ru_try = \_ _ _ -> match_magicDict },
+                   ru_nargs = 6, ru_try = \_ _ _ -> match_magicDict },
 
      mkBasicRule unsafeEqualityProofName 3 unsafeEqualityProofRule,
 
@@ -2243,14 +2243,11 @@ match_inline _ = Nothing
 -- See Note [magicDictId magic] in "GHC.Types.Id.Make"
 -- for a description of what is going on here.
 match_magicDict :: [Expr CoreBndr] -> Maybe (Expr CoreBndr)
-match_magicDict [Type _, (stripTicksE (const True) -> (Var wrap `App` Type a `App` Type _ `App` f)), x, y ]
-  | Just (_, fieldTy, _)  <- splitFunTy_maybe $ dropForAlls $ idType wrap
-  , Just (_, dictTy, _)   <- splitFunTy_maybe fieldTy
-  , Just dictTc           <- tyConAppTyCon_maybe dictTy
-  , Just (_,_,co)         <- unwrapNewTyCon_maybe dictTc
+match_magicDict [Type _rr, Type dt, Type _st, Type _r, k, sv]
+  | Just (dictTc, dictArgs) <- splitTyConApp_maybe dt
+  , Just (_,_,co)           <- unwrapNewTyCon_maybe dictTc
   = Just
-  $ f `App` Cast x (mkSymCo (mkUnbranchedAxInstCo Representational co [a] []))
-      `App` y
+  $ k `App` Cast sv (mkSymCo (mkUnbranchedAxInstCo Representational co dictArgs []))
 
 match_magicDict _ = Nothing
 
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
diff --git a/docs/users_guide/9.4.1-notes.rst b/docs/users_guide/9.4.1-notes.rst
new file mode 100644
index 0000000000..188593872e
--- /dev/null
+++ b/docs/users_guide/9.4.1-notes.rst
@@ -0,0 +1,22 @@
+.. _release-9-4-1:
+
+Version 9.4.1
+==============
+
+``base`` library
+~~~~~~~~~~~~~~~~
+
+- ``GHC.Exts.magicDict`` now has the type: ::
+
+        magicDict :: forall {rr :: RuntimeRep} dt st (r :: TYPE rr). (dt => r) -> st -> r
+
+  ``magicDict`` can now be used without defining an intermediate data type. For
+  example, the ``withTypeable`` function from the ``Data.Typeable`` module can
+  now be defined as: ::
+
+        withTypeable :: forall k (a :: k) rep (r :: TYPE rep). ()
+                     => TypeRep a -> (Typeable a => r) -> r
+        withTypeable rep k = magicDict @(Typeable a) k rep
+
+  Note that the explicit type application is required, as the call to
+  ``magicDict`` would be ambiguous otherwise.
diff --git a/docs/users_guide/release-notes.rst b/docs/users_guide/release-notes.rst
index 92d4277a67..8b1313d8fe 100644
--- a/docs/users_guide/release-notes.rst
+++ b/docs/users_guide/release-notes.rst
@@ -6,3 +6,4 @@ Release notes
 
    9.0.1-notes
    9.2.1-notes
+   9.4.1-notes
diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index 39974b4052..3b0f0da2ae 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -495,12 +495,7 @@ splitApp (TrTyCon{trTyCon = con, trKindVars = kinds})
 -- | Use a 'TypeRep' as 'Typeable' evidence.
 withTypeable :: forall k (a :: k) rep (r :: TYPE rep). ()
              => TypeRep a -> (Typeable a => r) -> r
-withTypeable rep k = unsafeCoerce k' rep
-  where k' :: Gift a r
-        k' = Gift k
-
--- | A helper to satisfy the type checker in 'withTypeable'.
-newtype Gift a (r :: TYPE rep) = Gift (Typeable a => r)
+withTypeable rep k = magicDict @(Typeable a) k rep
 
 -- | Pattern match on a type constructor
 pattern Con :: forall k (a :: k). ()
diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs
index 3adf826002..17ac5bb649 100644
--- a/libraries/base/GHC/TypeLits.hs
+++ b/libraries/base/GHC/TypeLits.hs
@@ -11,6 +11,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeApplications #-}
 
 {-|
 GHC's @DataKinds@ language extension lifts data constructors, natural
@@ -306,18 +307,16 @@ cmpChar x y = case compare (charVal x) (charVal y) of
 
 newtype SSymbol (s :: Symbol) = SSymbol String
 
-data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b)
-
 -- See Note [magicDictId magic] in "GHC.Types.Id.Make" in GHC
-withSSymbol :: (KnownSymbol a => Proxy a -> b)
+withSSymbol :: forall a b.
+               (KnownSymbol a => Proxy a -> b)
             -> SSymbol a      -> Proxy a -> b
-withSSymbol f x y = magicDict (WrapS f) x y
+withSSymbol f x y = magicDict @(KnownSymbol a) f x y
 
 newtype SChar (s :: Char) = SChar Char
 
-data WrapC a b = WrapC (KnownChar a => Proxy a -> b)
-
 -- See Note [magicDictId magic] in "GHC.Types.Id.Make" in GHC
-withSChar :: (KnownChar a => Proxy a -> b)
+withSChar :: forall a b.
+             (KnownChar a => Proxy a -> b)
             -> SChar a      -> Proxy a -> b
-withSChar f x y = magicDict (WrapC f) x y
+withSChar f x y = magicDict @(KnownChar a) f x y
diff --git a/libraries/base/GHC/TypeNats.hs b/libraries/base/GHC/TypeNats.hs
index 354e6005a2..0514d41366 100644
--- a/libraries/base/GHC/TypeNats.hs
+++ b/libraries/base/GHC/TypeNats.hs
@@ -12,6 +12,7 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeApplications #-}
 
 {-| This module is an internal GHC module.  It declares the constants used
 in the implementation of type-level natural numbers.  The programmer interface
@@ -240,9 +241,8 @@ cmpNat x y = case compare (natVal x) (natVal y) of
 
 newtype SNat    (n :: Nat)    = SNat    Natural
 
-data WrapN a b = WrapN (KnownNat    a => Proxy a -> b)
-
 -- See Note [magicDictId magic] in "GHC.Types.Id.Make" in GHC
-withSNat :: (KnownNat a => Proxy a -> b)
+withSNat :: forall a b.
+            (KnownNat a => Proxy a -> b)
          -> SNat a      -> Proxy a -> b
-withSNat f x y = magicDict (WrapN f) x y
+withSNat f x y = magicDict @(KnownNat a) f x y
diff --git a/libraries/ghc-prim/GHC/Magic.hs b/libraries/ghc-prim/GHC/Magic.hs
index 1bcaa0ec11..14fb7571cd 100644
--- a/libraries/ghc-prim/GHC/Magic.hs
+++ b/libraries/ghc-prim/GHC/Magic.hs
@@ -8,6 +8,10 @@
 {-# LANGUAGE UnliftedFFITypes #-}
 {-# LANGUAGE UnboxedTuples #-}
 {-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -130,9 +134,9 @@ runRW# m = m realWorld#
 -- It is used internally by modules such as "GHC.TypeNats" to cast a typeclass
 -- dictionary with a single method. It is eliminated by a rule during compilation.
 -- For the details, see @Note [magicDictId magic]@ in "GHC.Types.Id.Make" in GHC.
-magicDict :: a
+magicDict :: forall {rr :: RuntimeRep} dt st (r :: TYPE rr). (dt => r) -> st -> r
 {-# NOINLINE magicDict #-}
-magicDict = panicError "Non-rewritten magicDict"#
+magicDict = panicError @((dt => r) -> st -> r) "Non-rewritten magicDict"#
 
 {-
 Note [Compiler error functions]
diff --git a/libraries/ghc-prim/changelog.md b/libraries/ghc-prim/changelog.md
index a31674fc38..7c23090176 100644
--- a/libraries/ghc-prim/changelog.md
+++ b/libraries/ghc-prim/changelog.md
@@ -1,6 +1,19 @@
 ## next (edit as necessary)
 
 - `magicDict` is now defined in `GHC.Magic` instead of `GHC.Prim`.
+  It now has the type:
+
+        magicDict :: forall {rr :: RuntimeRep} dt st (r :: TYPE rr). (dt => r) -> st -> r
+
+  `magicDict` can now be used without defining an intermediate data type. For example,
+  the `withTypeable` function from `base`'s `Data.Typeable` module can now be defined as:
+
+        withTypeable :: forall k (a :: k) rep (r :: TYPE rep). ()
+                     => TypeRep a -> (Typeable a => r) -> r
+        withTypeable rep k = magicDict @(Typeable a) k rep
+
+  Note that the explicit type application is required, as the call to
+  `magicDict` would be ambiguous otherwise.
 
 ## 0.8.0 (edit as necessary)
 
diff --git a/testsuite/tests/typecheck/should_run/T16646.hs b/testsuite/tests/typecheck/should_run/T16646.hs
new file mode 100644
index 0000000000..978ae31b60
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T16646.hs
@@ -0,0 +1,77 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE TypeFamilies #-}
+module Main where
+
+import Data.Kind (Type)
+import Data.Proxy (Proxy(..))
+import GHC.Exts (Any, magicDict)
+import GHC.TypeLits
+
+-----
+-- reflection
+-----
+
+class Reifies s a | s -> a where
+  reflect :: proxy s -> a
+
+reify :: forall a r. a -> (forall (s :: Type). Reifies s a => Proxy s -> r) -> r
+reify a k = magicDict @(Reifies (Any @Type) a) (k @Any) (const a) Proxy
+
+class Given a where
+  given :: a
+
+withGift :: forall a b.
+            (Given a => Proxy a -> b)
+         ->        a -> Proxy a -> b
+withGift f x y = magicDict @(Given a) f x y
+
+give :: forall a r. a -> (Given a => r) -> r
+give a k = withGift (\_ -> k) a Proxy
+
+foo :: Given Int => Bool -> Int
+foo True  = 42
+foo False = given
+
+-----
+-- singletons
+-----
+
+type family Sing :: k -> Type
+data SBool :: Bool -> Type where
+  SFalse :: SBool False
+  STrue  :: SBool True
+deriving instance Show (SBool z)
+type instance Sing @Bool = SBool
+
+class SingI a where
+  sing :: Sing a
+
+data SingInstance (a :: k) where
+  SingInstance :: SingI a => SingInstance a
+
+singInstance :: forall k (a :: k). Sing a -> SingInstance a
+singInstance s = with_sing_i SingInstance
+  where
+    with_sing_i :: (SingI a => SingInstance a) -> SingInstance a
+    with_sing_i si = magicDict @(SingI a) si s
+
+withSingI :: Sing n -> (SingI n => r) -> r
+withSingI sn r =
+  case singInstance sn of
+    SingInstance -> r
+
+-----
+
+main :: IO ()
+main = do
+  -- GHC.TypeLits
+  -- print $ someCharVal 'a'
+  -- print $ someNatVal 42
+  -- print $ someSymbolVal "Hello World"
+
+  -- reflection
+  print $ give (23 :: Int) foo True
+
+  -- singletons
+  print $ withSingI SFalse (sing @False)
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index efc9fcb374..a34fb61747 100755
--- a/testsuite/tests/typecheck/should_run/all.T
+++ b/testsuite/tests/typecheck/should_run/all.T
@@ -76,6 +76,7 @@ test('IPRun', normal, compile_and_run, [''])
 test('IPLocation', normal, compile_and_run, [''])
 test('T10845', normal, compile_and_run, [''])
 test('T10846', normal, compile_and_run, [''])
+test('T16646', normal, compile_and_run, [''])
 
 # Support files for T1735 are in directory T1735_Help/
 test('T1735', normal, multimod_compile_and_run, ['T1735',''])