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, 192 insertions, 210 deletions

diff --git a/compiler/GHC/Builtin/Names.hs b/compiler/GHC/Builtin/Names.hs
index e99cb5a1c6..8aad951de0 100644
--- a/compiler/GHC/Builtin/Names.hs
+++ b/compiler/GHC/Builtin/Names.hs
@@ -222,7 +222,6 @@ basicKnownKeyNames
         ioTyConName, ioDataConName,
         runMainIOName,
         runRWName,
-        withDictName,
 
         -- Type representation types
         trModuleTyConName, trModuleDataConName,
@@ -259,6 +258,9 @@ basicKnownKeyNames
         starArrStarKindRepName,
         starArrStarArrStarKindRepName,
 
+        -- WithDict
+        withDictClassName,
+
         -- Dynamic
         toDynName,
 
@@ -931,10 +933,9 @@ and it's convenient to write them all down in one place.
 wildCardName :: Name
 wildCardName = mkSystemVarName wildCardKey (fsLit "wild")
 
-runMainIOName, runRWName, withDictName :: Name
+runMainIOName, runRWName :: Name
 runMainIOName = varQual gHC_TOP_HANDLER (fsLit "runMainIO") runMainKey
 runRWName     = varQual gHC_MAGIC       (fsLit "runRW#")    runRWKey
-withDictName  = varQual gHC_MAGIC_DICT  (fsLit "withDict")  withDictKey
 
 orderingTyConName, ordLTDataConName, ordEQDataConName, ordGTDataConName :: Name
 orderingTyConName = tcQual  gHC_TYPES (fsLit "Ordering") orderingTyConKey
@@ -1403,6 +1404,10 @@ starKindRepName        = varQual gHC_TYPES         (fsLit "krep$*")         star
 starArrStarKindRepName = varQual gHC_TYPES         (fsLit "krep$*Arr*")     starArrStarKindRepKey
 starArrStarArrStarKindRepName = varQual gHC_TYPES  (fsLit "krep$*->*->*")   starArrStarArrStarKindRepKey
 
+-- WithDict
+withDictClassName :: Name
+withDictClassName     = clsQual gHC_MAGIC_DICT (fsLit "WithDict") withDictClassKey
+
 -- Custom type errors
 errorMessageTypeErrorFamName
   , typeErrorTextDataConName
@@ -1707,6 +1712,9 @@ ixClassKey              = mkPreludeClassUnique 18
 typeableClassKey :: Unique
 typeableClassKey        = mkPreludeClassUnique 20
 
+withDictClassKey :: Unique
+withDictClassKey        = mkPreludeClassUnique 21
+
 monadFixClassKey :: Unique
 monadFixClassKey        = mkPreludeClassUnique 28
 
@@ -2343,9 +2351,6 @@ rationalToFloatIdKey, rationalToDoubleIdKey :: Unique
 rationalToFloatIdKey   = mkPreludeMiscIdUnique 132
 rationalToDoubleIdKey  = mkPreludeMiscIdUnique 133
 
-withDictKey :: Unique
-withDictKey                   = mkPreludeMiscIdUnique 156
-
 coerceKey :: Unique
 coerceKey                     = mkPreludeMiscIdUnique 157
 
diff --git a/compiler/GHC/HsToCore/Errors/Ppr.hs b/compiler/GHC/HsToCore/Errors/Ppr.hs
index a1aa921b2e..9695eee60c 100644
--- a/compiler/GHC/HsToCore/Errors/Ppr.hs
+++ b/compiler/GHC/HsToCore/Errors/Ppr.hs
@@ -3,7 +3,6 @@
 
 module GHC.HsToCore.Errors.Ppr where
 
-import GHC.Builtin.Names (withDictName)
 import GHC.Core.Predicate (isEvVar)
 import GHC.Core.Type
 import GHC.Driver.Flags
@@ -181,11 +180,6 @@ instance Diagnostic DsMessage where
       -> mkSimpleDecorated $
            hang (text "You can't mix polymorphic and unlifted bindings:")
               2 (ppr bind)
-    DsInvalidInstantiationDictAtType wrapped_ty
-      -> mkSimpleDecorated $
-           hang (text "Invalid instantiation of" <+>
-                quotes (ppr withDictName) <+> text "at type:")
-             4 (ppr wrapped_ty)
     DsWrongDoBind _rhs elt_ty
       -> mkSimpleDecorated $ badMonadBind elt_ty
     DsUnusedDoBind _rhs elt_ty
@@ -235,7 +229,6 @@ instance Diagnostic DsMessage where
     DsAggregatedViewExpressions{}               -> WarningWithoutFlag
     DsUnbangedStrictPatterns{}                  -> WarningWithFlag Opt_WarnUnbangedStrictPatterns
     DsCannotMixPolyAndUnliftedBindings{}        -> ErrorWithoutFlag
-    DsInvalidInstantiationDictAtType{}          -> ErrorWithoutFlag
     DsWrongDoBind{}                             -> WarningWithFlag Opt_WarnWrongDoBind
     DsUnusedDoBind{}                            -> WarningWithFlag Opt_WarnUnusedDoBind
     DsRecBindsNotAllowedForUnliftedTys{}        -> ErrorWithoutFlag
@@ -276,7 +269,6 @@ instance Diagnostic DsMessage where
     DsWrongDoBind rhs _                         -> [SuggestBindToWildcard rhs]
     DsUnusedDoBind rhs _                        -> [SuggestBindToWildcard rhs]
     DsRecBindsNotAllowedForUnliftedTys{}        -> noHints
-    DsInvalidInstantiationDictAtType{}          -> noHints
     DsRuleMightInlineFirst _ lhs_id rule_act    -> [SuggestAddInlineOrNoInlinePragma lhs_id rule_act]
     DsAnotherRuleMightFireFirst _ bad_rule _    -> [SuggestAddPhaseToCompetingRule bad_rule]
 
diff --git a/compiler/GHC/HsToCore/Errors/Types.hs b/compiler/GHC/HsToCore/Errors/Types.hs
index 55164e741b..d178eecfed 100644
--- a/compiler/GHC/HsToCore/Errors/Types.hs
+++ b/compiler/GHC/HsToCore/Errors/Types.hs
@@ -134,8 +134,6 @@ data DsMessage
 
   | DsCannotMixPolyAndUnliftedBindings !(HsBindLR GhcTc GhcTc)
 
-  | DsInvalidInstantiationDictAtType !Type
-
   | DsWrongDoBind !(LHsExpr GhcTc) !Type
 
   | DsUnusedDoBind !(LHsExpr GhcTc) !Type
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index bc287f433c..84dd992037 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -43,7 +43,6 @@ import GHC.Tc.Types.Evidence
 import GHC.Tc.Utils.Monad
 import GHC.Core.Type
 import GHC.Core.TyCo.Rep
-import GHC.Core.Coercion( instNewTyCon_maybe, mkSymCo )
 import GHC.Core
 import GHC.Core.Utils
 import GHC.Core.Make
@@ -757,8 +756,6 @@ dsDo ctx stmts
 dsHsVar :: Id -> DsM CoreExpr
 -- We could just call dsHsUnwrapped; but this is a short-cut
 -- for the very common case of a variable with no wrapper.
--- NB: withDict is always instantiated by a wrapper, so we need
---     only check for it in dsHsUnwrapped
 dsHsVar var
   = return (varToCoreExpr var) -- See Note [Desugaring vars]
 
@@ -831,7 +828,7 @@ warnDiscardedDoBindings rhs rhs_ty
 {-
 ************************************************************************
 *                                                                      *
-            dsHsWrapped and ds_withDict
+            dsHsWrapped
 *                                                                      *
 ************************************************************************
 -}
@@ -849,11 +846,6 @@ dsHsWrapped orig_hs_expr
        = go (wrap <.> WpTyApp ty) hs_e
 
     go wrap (HsVar _ (L _ var))
-      | var `hasKey` withDictKey
-      = do { wrap' <- dsHsWrapper wrap
-           ; ds_withDict (exprType (wrap' (varToCoreExpr var))) }
-
-      | otherwise
       = do { wrap' <- dsHsWrapper wrap
            ; let expr = wrap' (varToCoreExpr var)
                  ty   = exprType expr
@@ -866,186 +858,3 @@ dsHsWrapped orig_hs_expr
             ; addTyCs FromSource (hsWrapDictBinders wrap) $
               do { e <- dsExpr hs_e
                  ; return (wrap' e) } }
-
--- See Note [withDict]
-ds_withDict :: Type -> DsM CoreExpr
-ds_withDict wrapped_ty
-    -- Check that withDict is of the type `st -> (dt => r) -> r`.
-  | Just (Anon VisArg   (Scaled mult1 st),      rest) <- splitPiTy_maybe wrapped_ty
-  , Just (Anon VisArg   (Scaled mult2 dt_to_r), _r1)  <- splitPiTy_maybe rest
-  , Just (Anon InvisArg (Scaled _     dt),      _r2)  <- splitPiTy_maybe dt_to_r
-    -- Check that dt is a class constraint `C t_1 ... t_n`, where
-    -- `dict_tc = C` and `dict_args = t_1 ... t_n`.
-  , Just (dict_tc, dict_args) <- splitTyConApp_maybe dt
-    -- Check that C is a class of the form
-    -- `class C a_1 ... a_n where op :: meth_ty`, where
-    -- `meth_tvs = a_1 ... a_n` and `co` is a newtype coercion between
-    -- `C` and `meth_ty`.
-  , Just (inst_meth_ty, co) <- instNewTyCon_maybe dict_tc dict_args
-    --    co :: C t1 ..tn ~R# st
-    -- Check that `st` is equal to `meth_ty[t_i/a_i]`.
-  , st `eqType` inst_meth_ty
- = do { sv <- newSysLocalDs mult1 st
-       ; k  <- newSysLocalDs mult2 dt_to_r
-       ; let wd_rhs = mkLams [sv, k] $ Var k `App` Cast (Var sv) (mkSymCo co)
-       ; wd_id <- newSysLocalDs Many (exprType wd_rhs)
-       ; let wd_id' = wd_id `setInlinePragma` inlineAfterSpecialiser
-       ; pure $ Let (NonRec wd_id' wd_rhs) (Var wd_id') }
-         -- Why a Let?  See (WD8) in Note [withDict]
-
-  | otherwise
-  = errDsCoreExpr (DsInvalidInstantiationDictAtType wrapped_ty)
-
-inlineAfterSpecialiser :: InlinePragma
--- Do not inline before the specialiser; but do so afterwards
--- See (WD8) in Note [withDict]
-inlineAfterSpecialiser = alwaysInlinePragma `setInlinePragmaActivation`
-                         ActiveAfter NoSourceText 2
-
-{- Note [withDict]
-~~~~~~~~~~~~~~~~~~
-The identifier `withDict` 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:
-
-    withDict :: forall {rr :: RuntimeRep} st dt (r :: TYPE rr). st -> (dt => r) -> 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
-like this:
-
-   class C a where
-     f :: T a
-
-We can use `withDict`, in conjunction with a special case in the desugarer, to
-cast values of type `T a` into dictionaries for `C a`. To do this, we can
-define a function like this in the library:
-
-  withT :: T a -> (C a => b) -> b
-  withT t k = withDict @(T a) @(C a) t k
-
-Here:
-
-* The `dt` in `withDict` (short for "dictionary type") is instantiated to
-  `C a`.
-
-* The `st` in `withDict` (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 `withDict` is instantiated to `b`.
-
-There is a special case in dsHsWrapped.go_head which will replace the RHS
-of this definition with an appropriate definition in Core. The special case
-rewrites applications of `withDict` as follows:
-
-  withDict @{rr} @mtype @(C t_1 ... t_n) @r
----->
-  \(sv :: mtype) (k :: C t_1 ... t_n => r) -> k (sv |> sym (co t_1 ... t_n))
-
-Where:
-
-* The `C t_1 ... t_n` argument to withDict is a class constraint.
-
-* C must be defined as:
-
-    class C a_1 ... a_n where
-      op :: meth_type
-
-  That is, C must be a class with exactly one method and no superclasses.
-
-* The `mtype` argument to withDict must be equal to `meth_type[t_i/a_i]`,
-  which is instantiated type of C's method.
-
-* `co` is a newtype coercion that, when applied to `t_1 ... t_n`, coerces from
-  `C t_1 ... t_n` to `mtype`. This coercion is guaranteed to exist by virtue of
-  the fact that C is a class with exactly one method and no superclasses, so it
-  is treated like a newtype when compiled to Core.
-
-These requirements are implemented in the guards in ds_withDict's definition.
-
-Some further observations about `withDict`:
-
-(WD1) Every use of `withDict` must be instantiated at a /particular/ class C.
-      It's a bit like representation polymorphism: we don't allow class-polymorphic
-      calls of `withDict`. We check this in the desugarer -- and then we
-      can immediately replace this invocation of `withDict` with appropriate
-      class-specific Core code.
-
-(WD2) The `dt` in the type of withDict must be explicitly instantiated with
-      visible type application, as invoking `withDict` would be ambiguous
-      otherwise.
-
-      For examples of how `withDict` is used in the `base` library, see `withSNat`
-      in GHC.TypeNats, as well as `withSChar` and `withSSymbol` in GHC.TypeLits.
-
-(WD3) The `r` is representation-polymorphic, to support things like
-      `withTypeable` in `Data.Typeable.Internal`.
-
-(WD4) As an alternative to `withDict`, one could define functions like `withT`
-      above in terms of `unsafeCoerce`. This is more error-prone, however.
-
-(WD5) In order to define things like `reifySymbol` below:
-
-        reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => r) -> r
-
-      `withDict` needs to be instantiated with `Any`, like so:
-
-        reifySymbol n k = withDict @String @(KnownSymbol Any) @r n (k @Any)
-
-      The use of `Any` is explained in Note [NOINLINE someNatVal] in
-      base:GHC.TypeNats.
-
-(WD6) The only valid way to apply `withDict` is as described above. Applying
-      `withDict` in any other way will result in a non-recoverable error during
-      desugaring. In other words, GHC will never execute the `withDict` function
-      in compiled code.
-
-      In theory, this means that we don't need to define a binding for `withDict`
-      in GHC.Magic.Dict. In practice, we define a binding anyway, for two reasons:
-
-        - To give it Haddocks, and
-        - To define the type of `withDict`, which GHC can find in
-          GHC.Magic.Dict.hi.
-
-      Because we define a binding for `withDict`, we have to provide a right-hand
-      side for its definition. We somewhat arbitrarily choose:
-
-        withDict = panicError "Non rewritten withDict"#
-
-      This should never be reachable anyway, but just in case ds_withDict fails
-      to rewrite away `withDict`, this ensures that the program won't get very far.
-
-(WD7) One could conceivably implement this special case for `withDict` as a
-      constant-folding rule instead of during desugaring. We choose not to do so
-      for the following reasons:
-
-      - Having a constant-folding rule would require that `withDict`'s definition
-        be wired in to the compiler so as to prevent `withDict` from inlining too
-        early. Implementing the special case in the desugarer, on the other hand,
-        only requires that `withDict` be known-key.
-
-      - If the constant-folding rule were to fail, we want to throw a compile-time
-        error, which is trickier to do with the way that GHC.Core.Opt.ConstantFold
-        is set up.
-
-(WD8) In fact we desugar `withDict @{rr} @mtype @(C t_1 ... t_n) @r` to
-         let wd = \sv k -> k (sv |> co)
-             {-# INLINE [2] #-}
-         in wd
-
-      The local `let` and INLINE pragma delays inlining `wd` until after the
-      type-class Specialiser has run.  This is super important. Suppose we
-      have calls
-          withDict A k
-          withDict B k
-      where k1, k2 :: C T -> blah.  If we inline those withDict calls we'll get
-          k (A |> co1)
-          k (B |> co2)
-      and the Specialiser will assume that those arguments (of type `C T`) are
-      the same, will specialise `k` for that type, and will call the same,
-      specialised function from both call sites.  #21575 is a concrete case in point.
-
-      Solution: delay inlining `withDict` until after the specialiser; that is,
-      until Phase 2.  This is not a Final Solution -- seee #21575 "Alas..".
--}
diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs
index 50a13ba901..f2ffeea8c6 100644
--- a/compiler/GHC/Tc/Instance/Class.hs
+++ b/compiler/GHC/Tc/Instance/Class.hs
@@ -38,14 +38,19 @@ import GHC.Types.Var
 import GHC.Core.Predicate
 import GHC.Core.InstEnv
 import GHC.Core.Type
-import GHC.Core.Make ( mkCharExpr, mkNaturalExpr, mkStringExprFS )
+import GHC.Core.Make ( mkCharExpr, mkNaturalExpr, mkStringExprFS, mkCoreLams )
 import GHC.Core.DataCon
 import GHC.Core.TyCon
 import GHC.Core.Class
 
+import GHC.Core ( Expr(Var, App, Cast, Let), Bind (NonRec) )
+import GHC.Types.Basic
+import GHC.Types.SourceText
+
 import GHC.Utils.Outputable
 import GHC.Utils.Panic
 import GHC.Utils.Misc( splitAtList, fstOf3 )
+import GHC.Data.FastString
 
 import Data.Maybe
 
@@ -155,6 +160,7 @@ matchGlobalInst dflags short_cut clas tys
   = matchKnownChar dflags short_cut clas tys
   | isCTupleClass clas                = matchCTuple          clas tys
   | cls_name == typeableClassName     = matchTypeable        clas tys
+  | cls_name == withDictClassName     = matchWithDict             tys
   | clas `hasKey` heqTyConKey         = matchHeteroEquality       tys
   | clas `hasKey` eqTyConKey          = matchHomoEquality         tys
   | clas `hasKey` coercibleTyConKey   = matchCoercible            tys
@@ -431,6 +437,178 @@ makeLitDict clas ty et
 
 {- ********************************************************************
 *                                                                     *
+                   Class lookup for WithDict
+*                                                                     *
+***********************************************************************-}
+
+-- See Note [withDict]
+matchWithDict :: [Type] -> TcM ClsInstResult
+matchWithDict [cls, mty]
+    -- Check that cls is a class constraint `C t_1 ... t_n`, where
+    -- `dict_tc = C` and `dict_args = t_1 ... t_n`.
+  | Just (dict_tc, dict_args) <- tcSplitTyConApp_maybe cls
+    -- Check that C is a class of the form
+    -- `class C a_1 ... a_n where op :: meth_ty`
+    -- and in that case let
+    -- co :: C t1 ..tn ~R# inst_meth_ty
+  , Just (inst_meth_ty, co) <- tcInstNewTyCon_maybe dict_tc dict_args
+  = do { sv <- mkSysLocalM (fsLit "withDict_s") Many mty
+       ; k  <- mkSysLocalM (fsLit "withDict_k") Many (mkInvisFunTyMany cls openAlphaTy)
+
+       ; let evWithDict_type = mkSpecForAllTys [runtimeRep1TyVar, openAlphaTyVar] $
+                               mkVisFunTysMany [mty, mkInvisFunTyMany cls openAlphaTy] openAlphaTy
+
+       ; wd_id <- mkSysLocalM (fsLit "withDict_wd") Many evWithDict_type
+       ; let wd_id' = wd_id `setInlinePragma` inlineAfterSpecialiser
+
+       -- Given co2 : mty ~N# inst_meth_ty, construct the method of
+       -- the WithDict dictionary:
+       -- \@(r : RuntimeRep) @(a :: TYPE r) (sv : mty) (k :: cls => a) -> k (sv |> (sub co; sym co2))
+       ; let evWithDict co2 =
+               let wd_rhs = mkCoreLams [ runtimeRep1TyVar, openAlphaTyVar, sv, k ] $
+                            Var k `App` Cast (Var sv) (mkTcTransCo (mkTcSubCo co2) (mkTcSymCo co))
+               in Let (NonRec wd_id' wd_rhs) (Var wd_id')
+         -- Why a Let?  See (WD6) in Note [withDict]
+
+       ; tc <- tcLookupTyCon withDictClassName
+       ; let Just withdict_data_con
+                 = tyConSingleDataCon_maybe tc    -- "Data constructor"
+                                                  -- for WithDict
+             mk_ev [c] = evDataConApp withdict_data_con
+                            [cls, mty] [evWithDict (evTermCoercion (EvExpr c))]
+             mk_ev e   = pprPanic "matchWithDict" (ppr e)
+
+       ; return $ OneInst { cir_new_theta = [mkPrimEqPred mty inst_meth_ty]
+                          , cir_mk_ev     = mk_ev
+                          , cir_what      = BuiltinInstance }
+       }
+
+matchWithDict _
+  = return NoInstance
+
+inlineAfterSpecialiser :: InlinePragma
+-- Do not inline before the specialiser; but do so afterwards
+-- See (WD6) in Note [withDict]
+inlineAfterSpecialiser = alwaysInlinePragma `setInlinePragmaActivation`
+                         ActiveAfter NoSourceText 2
+
+{-
+Note [withDict]
+~~~~~~~~~~~~~~~
+The class `WithDict` is defined as:
+
+    class WithDict cls meth where
+        withDict :: forall {rr :: RuntimeRep} (r :: TYPE rr). meth -> (cls => r) -> r
+
+This class is special, like `Typeable`: GHC automatically solves
+for instances of `WithDict`, users cannot write their own.
+
+It is used to implement a primitive that we cannot define in Haskell
+but we can write in Core.
+
+`WithDict` is used to create dictionaries for classes with a single method.
+Consider a class like this:
+
+   class C a where
+     f :: T a
+
+We can use `withDict` to cast values of type `T a` into dictionaries for `C a`.
+To do this, we can define a function like this in the library:
+
+  withT :: T a -> (C a => b) -> b
+  withT t k = withDict @(C a) @(T a) t k
+
+Here:
+
+* The `cls` in `withDict` is instantiated to `C a`.
+
+* The `meth` in `withDict` 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 `withDict` is instantiated to `b`.
+
+For any single-method class C:
+   class C a1 .. an where op :: meth_ty
+
+The solver will solve the constraint `WithDict (C t1 .. tn) mty`
+as if the following instance declaration existed:
+
+instance (mty ~# inst_meth_ty) => WithDict (C t1..tn) mty where
+  withDict = \@{rr} @(r :: TYPE rr) (sv :: mty) (k :: C t1..tn => r) ->
+    k (sv |> (sub co2; sym co))
+
+That is, it matches on the first (constraint) argument of C; if C is
+a single-method class, the instance "fires" and emits an equality
+constraint `mty ~ inst_meth_ty`, where `inst_meth_ty` is `meth_ty[ti/ai]`.
+The coercion `co2` witnesses the equality `mty ~ inst_meth_ty`.
+
+The coercion `co` is a newtype coercion that coerces from `C t1 ... tn`
+to `inst_meth_ty`.
+This coercion is guaranteed to exist by virtue of the fact that
+C is a class with exactly one method and no superclasses, so it
+is treated like a newtype when compiled to Core.
+
+The condition that `C` is a single-method class is implemented in the
+guards of matchWithDict's definition.
+If the conditions are not held, the rewriting will not fire,
+and we'll report an unsolved constraint.
+
+Some further observations about `withDict`:
+
+(WD1) The `cls` in the type of withDict must be explicitly instantiated with
+      visible type application, as invoking `withDict` would be ambiguous
+      otherwise.
+
+      For examples of how `withDict` is used in the `base` library, see `withSNat`
+      in GHC.TypeNats, as well as `withSChar` and `withSSymbol` in GHC.TypeLits.
+
+(WD2) The `r` is representation-polymorphic, to support things like
+      `withTypeable` in `Data.Typeable.Internal`.
+
+(WD3) As an alternative to `withDict`, one could define functions like `withT`
+      above in terms of `unsafeCoerce`. This is more error-prone, however.
+
+(WD4) In order to define things like `reifySymbol` below:
+
+        reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => r) -> r
+
+      `withDict` needs to be instantiated with `Any`, like so:
+
+        reifySymbol n k = withDict @(KnownSymbol Any) @String @r n (k @Any)
+
+      The use of `Any` is explained in Note [NOINLINE someNatVal] in
+      base:GHC.TypeNats.
+
+(WD5) In earlier implementations, `withDict` was implemented as an identifier
+      with special handling during either constant-folding or desugaring.
+      The current approach is more robust, previously the type of `withDict`
+      did not have a type-class constraint and was overly polymorphic.
+      See #19915.
+
+(WD6) In fact we desugar `withDict @(C t_1 ... t_n) @mty @{rr} @r` to
+         let wd = \sv k -> k (sv |> co)
+             {-# INLINE [2] #-}
+         in wd
+      The local `let` and INLINE pragma delays inlining `wd` until after the
+      type-class Specialiser has run.  This is super important. Suppose we
+      have calls
+          withDict A k
+          withDict B k
+      where k1, k2 :: C T -> blah.  If we inline those withDict calls we'll get
+          k (A |> co1)
+          k (B |> co2)
+      and the Specialiser will assume that those arguments (of type `C T`) are
+      the same, will specialise `k` for that type, and will call the same,
+      specialised function from both call sites.  #21575 is a concrete case in point.
+
+      Solution: delay inlining `withDict` until after the specialiser; that is,
+      until Phase 2.  This is not a Final Solution -- seee #21575 "Alas..".
+
+-}
+
+{- ********************************************************************
+*                                                                     *
                    Class lookup for Typeable
 *                                                                     *
 ***********************************************************************-}
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 9010c43d46..22b627a36f 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -1407,7 +1407,7 @@ check_special_inst_head dflags is_boot is_sig ctxt clas cls_args
   -- instances for (~), (~~), or Coercible;
   -- but we DO want to allow them in quantified constraints:
   --   f :: (forall a b. Coercible a b => Coercible (m a) (m b)) => ...m...
-  | clas_nm `elem` [ heqTyConName, eqTyConName, coercibleTyConName ]
+  | clas_nm `elem` [ heqTyConName, eqTyConName, coercibleTyConName, withDictClassName ]
   , not quantified_constraint
   = failWithTc $ TcRnSpecialClassInst clas False