Use a class to check validity of withDictwip/withdict

This moves handling of the magic 'withDict' function from the desugarer
to the typechecker. Details in Note [withDict].

I've extracted a part of T16646Fail to a separate file T16646Fail2,
because the new error in 'reify' hides the errors from 'f' and 'g'.

WithDict now works with casts, this fixes #21328.

Part of #19915

6 files changed, 20 insertions, 21 deletions

diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index b1441fee84..2d2f735351 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -542,7 +542,7 @@ splitApp (TrTyCon{trTyCon = con, trKindVars = kinds})
 -- @
 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
+withTypeable rep k = withDict @(Typeable a) rep k
 
 -- | Pattern match on a type constructor
 pattern Con :: forall k (a :: k). ()
diff --git a/libraries/base/GHC/Exts.hs b/libraries/base/GHC/Exts.hs
index d4a59b440c..d9793d59d7 100755
--- a/libraries/base/GHC/Exts.hs
+++ b/libraries/base/GHC/Exts.hs
@@ -124,7 +124,7 @@ module GHC.Exts
         unsafeCoerce#,
 
         -- ** Casting class dictionaries with single methods
-        withDict,
+        WithDict(..),
 
         -- * The maximum tuple size
         maxTupleSize,
diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs
index 97b922c79e..a2310fd998 100644
--- a/libraries/base/GHC/TypeLits.hs
+++ b/libraries/base/GHC/TypeLits.hs
@@ -261,16 +261,16 @@ cmpChar x y = case compare (charVal x) (charVal y) of
 
 newtype SSymbol (s :: Symbol) = SSymbol String
 
--- See Note [withDict] in "GHC.HsToCore.Expr" in GHC
+-- See Note [withDict] in "GHC.Tc.Instance.Class" in GHC
 withSSymbol :: forall a b.
                (KnownSymbol a => Proxy a -> b)
             -> SSymbol a      -> Proxy a -> b
-withSSymbol f x y = withDict @(SSymbol a) @(KnownSymbol a) x f y
+withSSymbol f x y = withDict @(KnownSymbol a) x f y
 
 newtype SChar (s :: Char) = SChar Char
 
--- See Note [withDict] in "GHC.HsToCore.Expr" in GHC
+-- See Note [withDict] in "GHC.Tc.Instance.Class" in GHC
 withSChar :: forall a b.
              (KnownChar a => Proxy a -> b)
             -> SChar a      -> Proxy a -> b
-withSChar f x y = withDict @(SChar a) @(KnownChar a) x f y
+withSChar f x y = withDict @(KnownChar a) x f y
diff --git a/libraries/base/GHC/TypeNats.hs b/libraries/base/GHC/TypeNats.hs
index e764ed47db..6a71313404 100644
--- a/libraries/base/GHC/TypeNats.hs
+++ b/libraries/base/GHC/TypeNats.hs
@@ -39,7 +39,7 @@ module GHC.TypeNats
 
   ) where
 
-import GHC.Base(Eq(..), Ord(..), otherwise, withDict)
+import GHC.Base(Eq(..), Ord(..), otherwise, WithDict(..))
 import GHC.Types
 import GHC.Num.Natural(Natural)
 import GHC.Show(Show(..))
@@ -125,7 +125,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 [withDict] in "GHC.HsToCore.Expr" for details on how
+See Note [withDict] in "GHC.Tc.Instance.Class" for details on how
 we actually construct the dictionary.
 
 Note that using `Any Nat` is not really correct, as multiple calls to
@@ -245,8 +245,8 @@ cmpNat x y = case compare (natVal x) (natVal y) of
 
 newtype SNat    (n :: Nat)    = SNat    Natural
 
--- See Note [withDict] in "GHC.HsToCore.Expr" in GHC
+-- See Note [withDict] in "GHC.Tc.Instance.Class" in GHC
 withSNat :: forall a b.
             (KnownNat a => Proxy a -> b)
          -> SNat a      -> Proxy a -> b
-withSNat f x y = withDict @(SNat a) @(KnownNat a) x f y
+withSNat f x y = withDict @(KnownNat a) x f y
diff --git a/libraries/ghc-prim/GHC/Magic/Dict.hs b/libraries/ghc-prim/GHC/Magic/Dict.hs
index 12861db568..560ab3956f 100644
--- a/libraries/ghc-prim/GHC/Magic/Dict.hs
+++ b/libraries/ghc-prim/GHC/Magic/Dict.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE ImpredicativeTypes #-}
-{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
@@ -18,7 +18,7 @@
 -- Portability :  non-portable (GHC Extensions)
 --
 -- Defines the 'withDict' function. For more information, see
--- @Note [withDict]@ in "GHC.HsToCore.Expr" in GHC.
+-- @Note [withDict]@ in "GHC.Tc.Instance.Class" 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@.
@@ -28,9 +28,8 @@
 --
 -----------------------------------------------------------------------------
 
-module GHC.Magic.Dict (withDict) where
+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
@@ -38,7 +37,6 @@ import GHC.Types (RuntimeRep, TYPE)
 --
 -- '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"#
+-- @Note [withDict]@ in "GHC.Tc.Instance.Class" in GHC.
+class WithDict cls meth where
+  withDict :: forall {rr :: RuntimeRep} (r :: TYPE rr). meth -> (cls => r) -> r
diff --git a/libraries/ghc-prim/changelog.md b/libraries/ghc-prim/changelog.md
index 45701629a4..049b254743 100644
--- a/libraries/ghc-prim/changelog.md
+++ b/libraries/ghc-prim/changelog.md
@@ -4,7 +4,8 @@
   `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
+  class WithDict cls meth where
+    withDict :: forall {rr :: RuntimeRep} (r :: TYPE rr). meth -> (cls => r) -> r
   ```
 
   Unlike `magicDict`, `withDict` can be used without defining an
@@ -14,10 +15,10 @@
   ```
   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
+  withTypeable rep k = withDict @(Typeable a) rep k
   ```
 
-  Note that the explicit type applications are required, as the call to
+  Note that the explicit type application is required, as the call to
   `withDict` would be ambiguous otherwise.
 
 - Primitive types and functions which handle boxed values are now levity-polymorphic,