Redesign withDict (formerly magicDict)

This gives a more precise type signature to `magicDict` as proposed in #16646.
In addition, this replaces the constant-folding rule for `magicDict` in
`GHC.Core.Opt.ConstantFold` with a special case in the desugarer in
`GHC.HsToCore.Expr.dsHsWrapped`. I have also renamed `magicDict` to `withDict`
in light of the discussion in
https://mail.haskell.org/pipermail/ghc-devs/2021-April/019833.html.
All of this has the following benefits:

* `withDict` is now more type safe than before. Moreover, if a user applies
  `withDict` at an incorrect type, the special-casing in `dsHsWrapped` will
  now throw an error message indicating what the user did incorrectly.
* `withDict` can now work with classes that have multiple type arguments, such
  as `Typeable @k a`. This means that `Data.Typeable.Internal.withTypeable` can
  now be implemented in terms of `withDict`.
* Since the special-casing for `withDict` no longer needs to match on the
  structure of the expression passed as an argument to `withDict`, it no
  longer cares about the presence or absence of `Tick`s. In effect, this
  obsoletes the fix for #19667.

The new `T16646` test case demonstrates the new version of `withDict` in
action, both in terms of `base` functions defined in terms of `withDict`
as well as in terms of functions from the `reflection` and `singletons`
libraries. The `T16646Fail` test case demonstrates the error message that GHC
throws when `withDict` is applied incorrectly.

This fixes #16646. By adding more tests for `withDict`, this also
fixes #19673 as a side effect.

8 files changed, 94 insertions, 28 deletions

diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index 39974b4052..962f5b82c1 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 = withDict @(TypeRep a) @(Typeable a) rep k
 
 -- | Pattern match on a type constructor
 pattern Con :: forall k (a :: k). ()
diff --git a/libraries/base/GHC/Base.hs b/libraries/base/GHC/Base.hs
index c32bfbceca..5eb0da3ea1 100644
--- a/libraries/base/GHC/Base.hs
+++ b/libraries/base/GHC/Base.hs
@@ -100,6 +100,7 @@ module GHC.Base
         module GHC.Classes,
         module GHC.CString,
         module GHC.Magic,
+        module GHC.Magic.Dict,
         module GHC.Types,
         module GHC.Prim,        -- Re-export GHC.Prim and [boot] GHC.Err,
         module GHC.Prim.Ext,    -- to avoid lots of people having to
@@ -112,6 +113,7 @@ import GHC.Types
 import GHC.Classes
 import GHC.CString
 import GHC.Magic
+import GHC.Magic.Dict
 import GHC.Prim
 import GHC.Prim.Ext
 import GHC.Err
diff --git a/libraries/base/GHC/Exts.hs b/libraries/base/GHC/Exts.hs
index d0a32b03d1..2834ec73e9 100755
--- a/libraries/base/GHC/Exts.hs
+++ b/libraries/base/GHC/Exts.hs
@@ -76,6 +76,9 @@ module GHC.Exts
         -- * Running 'RealWorld' state thread
         runRW#,
 
+        -- * Casting class dictionaries with single methods
+        withDict,
+
         -- * Safe coercions
         --
         -- | These are available from the /Trustworthy/ module "Data.Coerce" as well
diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs
index 2dcc28b223..0eb5f1e2fc 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
@@ -58,13 +59,13 @@ module GHC.TypeLits
 
   ) where
 
-import GHC.Base(Eq(..), Ord(..), Ordering(..), String, otherwise)
+import GHC.Base(Eq(..), Ord(..), Ordering(..), String, otherwise, withDict)
 import GHC.Types(Symbol, Char)
 import GHC.Num(Integer, fromInteger)
 import GHC.Show(Show(..))
 import GHC.Read(Read(..))
 import GHC.Real(toInteger)
-import GHC.Prim(magicDict, Proxy#)
+import GHC.Prim(Proxy#)
 import Data.Maybe(Maybe(..))
 import Data.Proxy (Proxy(..))
 import Data.Type.Equality((:~:)(Refl))
@@ -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 "basicType/MkId.hs"
-withSSymbol :: (KnownSymbol a => Proxy a -> b)
+-- See Note [withDict] in "GHC.HsToCore.Expr" in GHC
+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 = withDict @(SSymbol a) @(KnownSymbol a) x f y
 
 newtype SChar (s :: Char) = SChar Char
 
-data WrapC a b = WrapC (KnownChar a => Proxy a -> b)
-
--- See Note [q] in "basicType/MkId.hs"
-withSChar :: (KnownChar a => Proxy a -> b)
+-- See Note [withDict] in "GHC.HsToCore.Expr" in GHC
+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 = withDict @(SChar a) @(KnownChar a) x f y
diff --git a/libraries/base/GHC/TypeNats.hs b/libraries/base/GHC/TypeNats.hs
index f9733d55a3..fd7c847112 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
@@ -38,12 +39,12 @@ module GHC.TypeNats
 
   ) where
 
-import GHC.Base(Eq(..), Ord(..), otherwise)
+import GHC.Base(Eq(..), Ord(..), otherwise, withDict)
 import GHC.Types
 import GHC.Num.Natural(Natural)
 import GHC.Show(Show(..))
 import GHC.Read(Read(..))
-import GHC.Prim(magicDict, Proxy#)
+import GHC.Prim(Proxy#)
 import Data.Maybe(Maybe(..))
 import Data.Proxy (Proxy(..))
 import Data.Type.Equality((:~:)(Refl))
@@ -121,7 +122,7 @@ After inlining and simplification, this ends up looking something like this:
     where type T = Any Nat
 
 `KnownNat` is the constructor for dictionaries for the class `KnownNat`.
-See Note [magicDictId magic] in "basicType/MkId.hs" for details on how
+See Note [withDict] in "GHC.HsToCore.Expr" for details on how
 we actually construct the dictionary.
 
 Note that using `Any Nat` is not really correct, as multilple calls to
@@ -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 "basicType/MkId.hs"
-withSNat :: (KnownNat a => Proxy a -> b)
+-- See Note [withDict] in "GHC.HsToCore.Expr" in GHC
+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 = withDict @(SNat a) @(KnownNat a) x f y
diff --git a/libraries/ghc-prim/GHC/Magic/Dict.hs b/libraries/ghc-prim/GHC/Magic/Dict.hs
new file mode 100644
index 0000000000..12861db568
--- /dev/null
+++ b/libraries/ghc-prim/GHC/Magic/Dict.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE Unsafe #-}
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  GHC.Magic.Dict
+-- Copyright   :  (c) The University of Glasgow 2009
+-- License     :  see libraries/ghc-prim/LICENSE
+--
+-- Maintainer  :  cvs-ghc@haskell.org
+-- Stability   :  internal
+-- Portability :  non-portable (GHC Extensions)
+--
+-- Defines the 'withDict' function. For more information, see
+-- @Note [withDict]@ in "GHC.HsToCore.Expr" in GHC.
+-- The definition of 'withDict' is located in a separate module from
+-- "GHC.Magic" because 'withDict' is @Unsafe@ (it threatens type class
+-- coherence) while "GHC.Magic" is @Trustworthy@.
+--
+-- Use "GHC.Exts" from the @base@ package instead of importing this
+-- module directly.
+--
+-----------------------------------------------------------------------------
+
+module GHC.Magic.Dict (withDict) where
+
+import GHC.Prim.Panic (panicError)
+import GHC.Types (RuntimeRep, TYPE)
+
+-- | @'withDict' d f@ provides a way to call a type-class–overloaded function
+-- @f@ by applying it to the supplied dictionary @d@.
+--
+-- 'withDict' can only be used if the type class has a single method with no
+-- superclasses. For more (important) details on how this works, see
+-- @Note [withDict]@ in "GHC.HsToCore.Expr" in GHC.
+withDict :: forall {rr :: RuntimeRep} st dt (r :: TYPE rr). st -> (dt => r) -> r
+{-# NOINLINE withDict #-}
+withDict = panicError "Non-rewritten withDict"#
diff --git a/libraries/ghc-prim/changelog.md b/libraries/ghc-prim/changelog.md
index 6c7723068f..1ce61e2e61 100644
--- a/libraries/ghc-prim/changelog.md
+++ b/libraries/ghc-prim/changelog.md
@@ -1,3 +1,25 @@
+## next (edit as necessary)
+
+- `magicDict` has been renamed to `withDict` and is now defined in
+  `GHC.Magic.Dict` instead of `GHC.Prim`. `withDict` now has the type:
+
+  ```
+  withDict :: forall {rr :: RuntimeRep} st dt (r :: TYPE rr). st -> (dt => r) -> r
+  ```
+
+  Unlike `magicDict`, `withDict` can 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 = withDict @(TypeRep a) @(Typeable a) rep k
+  ```
+
+  Note that the explicit type applications are required, as the call to
+  `withDict` would be ambiguous otherwise.
+
 ## 0.8.0 (edit as necessary)
 
 - Change array access primops to use type with size maxing the element size:
@@ -23,7 +45,7 @@
 - Add known-key `cstringLength#` to `GHC.CString`. This is just the
   C function `strlen`, but a built-in rewrite rule allows GHC to
   compute the result at compile time when the argument is known.
-  
+
 - In order to support unicode better the following functions in `GHC.CString`
   gained UTF8 counterparts:
 
@@ -47,7 +69,7 @@
         atomicCasAddrAddr# :: Addr# -> Addr# -> Addr# -> State# s -> (# State# s, Addr# #)
         atomicCasWordAddr# :: Addr# -> Word# -> Word# -> State# s -> (# State# s, Word# #)
 
-- Add an explicit fixity for `(~)` and `(~~)`: 
+- Add an explicit fixity for `(~)` and `(~~)`:
 
         infix 4 ~, ~~
 
diff --git a/libraries/ghc-prim/ghc-prim.cabal b/libraries/ghc-prim/ghc-prim.cabal
index 05fd60f09a..61840021c1 100644
--- a/libraries/ghc-prim/ghc-prim.cabal
+++ b/libraries/ghc-prim/ghc-prim.cabal
@@ -45,6 +45,7 @@ Library
         GHC.Debug
         GHC.IntWord64
         GHC.Magic
+        GHC.Magic.Dict
         GHC.Prim.Ext
         GHC.Prim.Panic
         GHC.Prim.Exception