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

27 files changed, 299 insertions, 272 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
 
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,
diff --git a/testsuite/tests/ghci/scripts/T19667Ghci.hs b/testsuite/tests/ghci/scripts/T19667Ghci.hs
index c3ffa71be8..bc8f36de93 100644
--- a/testsuite/tests/ghci/scripts/T19667Ghci.hs
+++ b/testsuite/tests/ghci/scripts/T19667Ghci.hs
@@ -21,7 +21,7 @@ symbolVal _ = case symbolSing :: SSymbol n of SSymbol x -> x
 -- See Note [NOINLINE someNatVal] in GHC.TypeNats
 {-# NOINLINE reifySymbol #-}
 reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
-reifySymbol n k = withDict @(SSymbol Any) @(KnownSymbol Any) (SSymbol n) (k @Any) (Proxy @(Any @Symbol))
+reifySymbol n k = withDict @(KnownSymbol Any) @(SSymbol Any) (SSymbol n) (k @Any) (Proxy @(Any @Symbol))
 
 main :: IO ()
 main = print $ reifySymbol "Hello World" symbolVal
diff --git a/testsuite/tests/simplCore/should_run/T21575.hs b/testsuite/tests/simplCore/should_run/T21575.hs
index 976483f963..d1b383ec1a 100644
--- a/testsuite/tests/simplCore/should_run/T21575.hs
+++ b/testsuite/tests/simplCore/should_run/T21575.hs
@@ -31,7 +31,7 @@ main = do
 toJSONBar :: Given Style => Bar -> Value
 
   give Normal (\gd -> toJSONBar gd e)
-  --> withDict @Style @(Given Style) Normal (toJSON e)
+  --> withDict @(Given Style) @Style Normal (toJSON e)
   --> toJSONBar ((Normal |> co) :: Given Style) e
 
   give Normal (\gd -> toJSONBar gd e')
@@ -40,7 +40,7 @@ toJSONBar :: Given Style => Bar -> Value
 --------- With new cast ------------
 
   give Normal (\gd -> toJSONBar gd e)
-  --> withDict @Style @(Given Style) Normal (\gd -> toJSONBar gd e)
+  --> withDict @(Given Style) @Style Normal (\gd -> toJSONBar gd e)
   --> ((\gd -> toJSONBar gd e) |> co) Normal
   --> (\gd' -> toJSonBar (gd' |> sym (co[1])) e) Normal
   --> toJSONBar (Normal |> co') e   -- Boo!
@@ -61,7 +61,7 @@ class Given a where
 
 give :: forall a r. a -> (Given a => r) -> r
 #if WITH_DICT
-give = withDict @a @(Given a)
+give = withDict @(Given a) @a
 #else
 give a k = unsafeCoerce (Gift k :: Gift a r) a
 
diff --git a/testsuite/tests/typecheck/should_compile/T21328.hs b/testsuite/tests/typecheck/should_compile/T21328.hs
new file mode 100644
index 0000000000..9b72df193f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T21328.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies #-}
+module T21328 where
+
+import GHC.Exts
+import Type.Reflection
+
+type family F x
+type instance F x = x
+
+type family G x
+type instance G x = x
+
+class C a where
+  m :: G a
+
+cast :: forall a. F a -> (C a => Int) -> Int
+cast = withDict  @(C a) @(F a)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index f08828eeea..a258f6de03 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -829,6 +829,7 @@ test('T21023', normal, compile, ['-ddump-types'])
 test('T21205', normal, compile, ['-O0'])
 test('T21323', normal, compile, [''])
 test('T21315', normal, compile, ['-Wredundant-constraints'])
+test('T21328', normal, compile, [''])
 test('T21516', normal, compile, [''])
 test('T21519', normal, compile, [''])
 test('T21519a', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T16646Fail.hs b/testsuite/tests/typecheck/should_fail/T16646Fail.hs
index 73ded574b7..bf3cfcc6f3 100644
--- a/testsuite/tests/typecheck/should_fail/T16646Fail.hs
+++ b/testsuite/tests/typecheck/should_fail/T16646Fail.hs
@@ -12,17 +12,11 @@ import Data.Kind
 import Data.Proxy
 import GHC.Exts
 
-f :: forall {rr :: RuntimeRep} st dt (r :: TYPE rr). st -> (dt => r) -> r
-f = withDict @st @dt
+f :: forall {rr :: RuntimeRep} cls meth (r :: TYPE rr). meth -> (cls => r) -> r
+f = withDict @cls @meth
 
 class Show a => C a where
   m :: Maybe a
 
 g :: forall a r. Maybe a -> (C a => r) -> r
-g = withDict @(Maybe a) @(C a)
-
-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 = withDict @_ @(Reifies (Any @Type) a) (const a) (k @Any) Proxy
+g = withDict @(C a) @(Maybe a)
diff --git a/testsuite/tests/typecheck/should_fail/T16646Fail.stderr b/testsuite/tests/typecheck/should_fail/T16646Fail.stderr
index 3873a096d9..4c597bed33 100644
--- a/testsuite/tests/typecheck/should_fail/T16646Fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T16646Fail.stderr
@@ -1,11 +1,15 @@
 
 T16646Fail.hs:16:5: error:
-    Invalid instantiation of ‘withDict’ at type: st -> (dt => r) -> r
+    • No instance for (WithDict cls meth) arising from a use of ‘withDict’
+      Possible fix:
+        add (WithDict cls meth) to the context of
+          the type signature for:
+            f :: forall (cls :: Constraint) meth r. meth -> (cls => r) -> r
+    • In the expression: withDict @cls @meth
+      In an equation for ‘f’: f = withDict @cls @meth
 
 T16646Fail.hs:22:5: error:
-    Invalid instantiation of ‘withDict’ at type:
-        Maybe a -> (C a => r) -> r
-
-T16646Fail.hs:28:13: error:
-    Invalid instantiation of ‘withDict’ at type:
-        (Any -> a) -> (Reifies Any a => Proxy Any -> r) -> Proxy Any -> r
+    • No instance for (WithDict (C a) (Maybe a))
+        arising from a use of ‘withDict’
+    • In the expression: withDict @(C a) @(Maybe a)
+      In an equation for ‘g’: g = withDict @(C a) @(Maybe a)
diff --git a/testsuite/tests/typecheck/should_fail/T16646Fail2.hs b/testsuite/tests/typecheck/should_fail/T16646Fail2.hs
new file mode 100644
index 0000000000..55934f7474
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16646Fail2.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+module T16646Fail where
+
+import Data.Kind
+import Data.Proxy
+import GHC.Exts
+
+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 = withDict @(Reifies (Any @Type) a) @_ (const a) (k @Any) Proxy
diff --git a/testsuite/tests/typecheck/should_fail/T16646Fail2.stderr b/testsuite/tests/typecheck/should_fail/T16646Fail2.stderr
new file mode 100644
index 0000000000..7a8178136c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16646Fail2.stderr
@@ -0,0 +1,16 @@
+
+T16646Fail2.hs:19:13: error:
+    • Couldn't match type: b0 -> a
+                     with: forall (proxy :: * -> *). proxy Any -> a
+        arising from a use of ‘withDict’
+    • In the expression:
+        withDict @(Reifies (Any @Type) a) @_ (const a) (k @Any) Proxy
+      In an equation for ‘reify’:
+          reify a k
+            = withDict @(Reifies (Any @Type) a) @_ (const a) (k @Any) Proxy
+    • Relevant bindings include
+        k :: forall s. Reifies s a => Proxy s -> r
+          (bound at T16646Fail2.hs:19:9)
+        a :: a (bound at T16646Fail2.hs:19:7)
+        reify :: a -> (forall s. Reifies s a => Proxy s -> r) -> r
+          (bound at T16646Fail2.hs:19:1)
diff --git a/testsuite/tests/typecheck/should_fail/T19915.hs b/testsuite/tests/typecheck/should_fail/T19915.hs
new file mode 100644
index 0000000000..9f7ac26389
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19915.hs
@@ -0,0 +1,5 @@
+module T19915 where
+
+import GHC.Exts
+
+instance WithDict a b
diff --git a/testsuite/tests/typecheck/should_fail/T19915.stderr b/testsuite/tests/typecheck/should_fail/T19915.stderr
new file mode 100644
index 0000000000..7f75999605
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19915.stderr
@@ -0,0 +1,4 @@
+
+T19915.hs:5:10: error:
+    • Class ‘WithDict’ does not support user-specified instances.
+    • In the instance declaration for ‘WithDict a b’
diff --git a/testsuite/tests/typecheck/should_fail/T21328.hs b/testsuite/tests/typecheck/should_fail/T21328.hs
deleted file mode 100644
index f589c5d3a7..0000000000
--- a/testsuite/tests/typecheck/should_fail/T21328.hs
+++ /dev/null
@@ -1,11 +0,0 @@
-{-# LANGUAGE TypeFamilies #-}
-module T21328 where
-
-import GHC.Exts
-import Type.Reflection
-
-type family Id x
-type instance Id x = x
-
-cast :: forall a. Id (TypeRep a) -> (Typeable a => Int) -> Int
-cast = withDict @(TypeRep a) @(Typeable a)
diff --git a/testsuite/tests/typecheck/should_fail/T21328.stderr b/testsuite/tests/typecheck/should_fail/T21328.stderr
deleted file mode 100644
index a7d106a793..0000000000
--- a/testsuite/tests/typecheck/should_fail/T21328.stderr
+++ /dev/null
@@ -1,4 +0,0 @@
-
-T21328.hs:11:8: error:
-    Invalid instantiation of ‘withDict’ at type:
-        Id (TypeRep a) -> (Typeable a => Int) -> Int
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 83ba2c4414..46fecd51ce 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -530,6 +530,7 @@ test('T16627', normal, compile_fail, [''])
 test('T502', normal, compile_fail, [''])
 test('T16517', normal, compile_fail, [''])
 test('T16646Fail', normal, compile_fail, [''])
+test('T16646Fail2', normal, compile_fail, [''])
 test('T15883', normal, compile_fail, [''])
 test('T15883b', normal, compile_fail, [''])
 test('T15883c', normal, compile_fail, [''])
@@ -629,6 +630,7 @@ test('T19397E3', extra_files(['T19397S.hs']), multimod_compile_fail,
 test('T19397E4', extra_files(['T19397S.hs']), multimod_compile_fail,
     ['T19397E4.hs', '-v0 -main-is foo'])
 test('T19415', normal, compile_fail, [''])
+test('T19915', normal, compile_fail, [''])
 test('T19977a', normal, compile_fail, [''])
 test('T19977b', normal, compile_fail, [''])
 test('T19978', normal, compile_fail, [''])
@@ -653,6 +655,5 @@ test('T20064', normal, compile_fail, [''])
 test('T21130', normal, compile_fail, [''])
 test('T20768_fail', normal, compile_fail, [''])
 test('T21327', normal, compile_fail, [''])
-test('T21328', normal, compile_fail, [''])
 test('T21338', normal, compile_fail, [''])
 test('T21158', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_run/T16646.hs b/testsuite/tests/typecheck/should_run/T16646.hs
index 6af86e96a4..0976215ae9 100644
--- a/testsuite/tests/typecheck/should_run/T16646.hs
+++ b/testsuite/tests/typecheck/should_run/T16646.hs
@@ -22,8 +22,8 @@ instance KnownNat n => Reifies n Integer where
 
 reify :: forall a r. a -> (forall (s :: Type). Reifies s a => Proxy s -> r) -> r
 {-# NOINLINE reify #-} -- See Note [NOINLINE someNatVal] in GHC.TypeNats
-reify a k = withDict @(forall (proxy :: Type -> Type). proxy Any -> a)
-                     @(Reifies (Any @Type) a)
+reify a k = withDict @(Reifies (Any @Type) a)
+                     @(forall (proxy :: Type -> Type). proxy Any -> a)
                      (const a) (k @Any) Proxy
 
 class Given a where
@@ -32,7 +32,7 @@ class Given a where
 withGift :: forall a b.
             (Given a => Proxy a -> b)
          ->        a -> Proxy a -> b
-withGift f x y = withDict @a @(Given a) x f y
+withGift f x y = withDict @(Given a) @a x f y
 
 give :: forall a r. a -> (Given a => r) -> r
 give a k = withGift (\_ -> k) a Proxy
@@ -62,7 +62,7 @@ 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 = withDict @(Sing a) @(SingI a) s si
+    with_sing_i si = withDict @(SingI a) @(Sing a) s si
 
 withSingI :: Sing n -> (SingI n => r) -> r
 withSingI sn r =
diff --git a/testsuite/tests/typecheck/should_run/T19667.hs b/testsuite/tests/typecheck/should_run/T19667.hs
index c3ffa71be8..bc8f36de93 100644
--- a/testsuite/tests/typecheck/should_run/T19667.hs
+++ b/testsuite/tests/typecheck/should_run/T19667.hs
@@ -21,7 +21,7 @@ symbolVal _ = case symbolSing :: SSymbol n of SSymbol x -> x
 -- See Note [NOINLINE someNatVal] in GHC.TypeNats
 {-# NOINLINE reifySymbol #-}
 reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
-reifySymbol n k = withDict @(SSymbol Any) @(KnownSymbol Any) (SSymbol n) (k @Any) (Proxy @(Any @Symbol))
+reifySymbol n k = withDict @(KnownSymbol Any) @(SSymbol Any) (SSymbol n) (k @Any) (Proxy @(Any @Symbol))
 
 main :: IO ()
 main = print $ reifySymbol "Hello World" symbolVal