Redesign the type of magicDictwip/T16646-take-two

This gives a more precise type signature to `magicDict` as proposed in #16646.
In addition to making it more type safe:

* This allows the `magicDict` constant-folding rule to apply to classes with
  multiple type arguments, such as `Typeable @k a`. This means that
  `withTypeable` can now be implemented in terms of `magicDict`.
* Moreover, since the constant-folding rule no longer needs to case on the
  structure of the expression passed as an argument to `magicDict`, 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 `magicDict` in
action, both in terms of `base` functions defined in terms of `magicDict`
as well as in terms of functions from the `reflection` and `singletons`
libraries.

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

16 files changed, 267 insertions, 59 deletions

diff --git a/compiler/GHC/Builtin/Types/Prim.hs b/compiler/GHC/Builtin/Types/Prim.hs
index 115c76516d..187820cd35 100644
--- a/compiler/GHC/Builtin/Types/Prim.hs
+++ b/compiler/GHC/Builtin/Types/Prim.hs
@@ -31,6 +31,8 @@ module GHC.Builtin.Types.Prim(
 
         multiplicityTyVar1, multiplicityTyVar2,
 
+        constraintKindedTyVar,
+
         -- Kind constructors...
         tYPETyCon, tYPETyConName,
 
@@ -114,7 +116,7 @@ import {-# SOURCE #-} GHC.Builtin.Types
   , int64ElemRepDataConTy, word8ElemRepDataConTy, word16ElemRepDataConTy
   , word32ElemRepDataConTy, word64ElemRepDataConTy, floatElemRepDataConTy
   , doubleElemRepDataConTy
-  , mkPromotedListTy, multiplicityTy )
+  , mkPromotedListTy, multiplicityTy, constraintKind )
 
 import GHC.Types.Var    ( TyVar, mkTyVar )
 import GHC.Types.Name
@@ -380,7 +382,7 @@ alphaTyUnliftedRep :: Type
 
 runtimeRep1TyVar, runtimeRep2TyVar, runtimeRep3TyVar :: TyVar
 (runtimeRep1TyVar : runtimeRep2TyVar : runtimeRep3TyVar : _)
-  = drop 16 (mkTemplateTyVars (repeat runtimeRepTy))  -- selects 'q','r'
+  = drop 16 (mkTemplateTyVars (repeat runtimeRepTy))  -- selects 'q','r','s'
 
 runtimeRep1Ty, runtimeRep2Ty, runtimeRep3Ty :: Type
 runtimeRep1Ty = mkTyVarTy runtimeRep1TyVar
@@ -403,6 +405,9 @@ multiplicityTyVar1, multiplicityTyVar2  :: TyVar
 (multiplicityTyVar1 : multiplicityTyVar2 : _)
    = drop 13 (mkTemplateTyVars (repeat multiplicityTy))  -- selects 'n', 'm'
 
+constraintKindedTyVar :: TyVar
+(constraintKindedTyVar : _)
+   = drop 19 (mkTemplateTyVars (repeat constraintKind))  -- selects 't'
 
 {-
 ************************************************************************
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index 3438f372fc..ced4bc4ce6 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -37,6 +37,7 @@ import GHC.Core
 import GHC.Core.FVs
 import GHC.Core.Utils
 import GHC.Core.Stats ( coreBindsStats )
+import GHC.Core.Opt.ConstantFold ( match_magicDict )
 import GHC.Core.Opt.Monad
 import GHC.Data.Bag
 import GHC.Types.Literal
@@ -936,12 +937,24 @@ lintCoreExpr e@(App _ _)
        ; app_ty <- lintValApp arg3 fun_ty2 arg3_ty ue2 ue3
        ; lintCoreArgs app_ty rest }
 
+    -- If we see an application of magicDict, make sure it upholds the criteria
+    -- specified in Note [magicDictId magic] in GHC.Types.Id.Make.
+  | Var fun <- fun
+  , fun `hasKey` magicDictKey
+  = -- magicDict might be oversaturated, so only look at its first six arguments
+    if isJust (match_magicDict (take 6 args))
+       then lint_core_app
+       else failWithL $ hang (text "Invalid application of magicDict to arguments:")
+                           4 (ppr args)
+
   | otherwise
-  = do { pair <- lintCoreFun fun (length args)
-       ; lintCoreArgs pair args }
+  = lint_core_app
   where
     (fun, args) = collectArgs e
 
+    lint_core_app = do { pair <- lintCoreFun fun (length args)
+                       ; lintCoreArgs pair args }
+
 lintCoreExpr (Lam var expr)
   = markAllJoinsBad $
     lintLambda var $ lintCoreExpr expr
diff --git a/compiler/GHC/Core/Opt/ConstantFold.hs b/compiler/GHC/Core/Opt/ConstantFold.hs
index 88439edcc6..9c76231aa2 100644
--- a/compiler/GHC/Core/Opt/ConstantFold.hs
+++ b/compiler/GHC/Core/Opt/ConstantFold.hs
@@ -28,6 +28,7 @@ module GHC.Core.Opt.ConstantFold
    ( primOpRules
    , builtinRules
    , caseRules
+   , match_magicDict
    )
 where
 
@@ -53,7 +54,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 +1741,7 @@ builtinRules
      BuiltinRule { ru_name = fsLit "Inline", ru_fn = inlineIdName,
                    ru_nargs = 2, ru_try = \_ _ _ -> match_inline },
      BuiltinRule { ru_name = fsLit "MagicDict", ru_fn = idName magicDictId,
-                   ru_nargs = 4, ru_try = \_ _ _ -> match_magicDict },
+                   ru_nargs = 6, ru_try = \_ _ _ -> match_magicDict },
 
      mkBasicRule unsafeEqualityProofName 3 unsafeEqualityProofRule,
 
@@ -2243,14 +2244,19 @@ 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]
+  | -- 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 (meth_tvs, meth_ty, co) <- unwrapNewTyCon_maybe dict_tc
+    -- Check that `st` is equal to `meth_ty[t_i/a_i]`.
+  , st `eqType` substTyWith meth_tvs dict_args meth_ty
   = Just
-  $ f `App` Cast x (mkSymCo (mkUnbranchedAxInstCo Representational co [a] []))
-      `App` y
+  $ k `App` Cast sv (mkSymCo (mkUnbranchedAxInstCo Representational co dict_args []))
 
 match_magicDict _ = Nothing
 
diff --git a/compiler/GHC/Types/Id/Make.hs b/compiler/GHC/Types/Id/Make.hs
index 37a052d9ab..3c06cb6bae 100644
--- a/compiler/GHC/Types/Id/Make.hs
+++ b/compiler/GHC/Types/Id/Make.hs
@@ -1602,8 +1602,11 @@ magicDictId :: Id  -- See Note [magicDictId magic]
 magicDictId = pcMiscPrelId magicDictName ty info
   where
   info = noCafIdInfo `setInlinePragInfo` neverInlinePragma
-                     `setNeverLevPoly`   ty
-  ty   = mkSpecForAllTys [alphaTyVar] alphaTy
+  ty   = mkInfForAllTy runtimeRep2TyVar $
+         mkSpecForAllTys [constraintKindedTyVar, alphaTyVar, openBetaTyVar] $
+         mkVisFunTysMany [ mkInvisFunTyMany (mkTyVarTy constraintKindedTyVar)
+                                            openBetaTy
+                         , alphaTy ] openBetaTy
 
 --------------------------------------------------------------------------------
 
@@ -1807,7 +1810,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
@@ -1820,34 +1823,82 @@ 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`.
+
+* 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} @(C t_1 ... t_n) @mtype @r k sv
 ---->
-  f (x `cast` co a) y
+  k (sv |> sym (co t_1 ... t_n))
+
+Where:
+
+* The `C t_1 ... t_n` argument to magicDict 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 magicDict must be equal to `meth_type[t_i/a_i]`,
+  which is instantied 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.
+
+Some further observations about `magicDict`:
+
+* The `dt` in the type of magicDict must be explicitly instantiated with
+  visible type application, as invoking `magicDict` would be ambiguous
+  otherwise.
+
+* 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.
+
+* In order to define things like `reifySymbol` below:
+
+    reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => r) -> r
+
+  `magicDict` needs to be instantiated with `Any`, like so:
+
+    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.
 
-The `co` coercion is the newtype-coercion extracted from the type-class.
-The type class is obtained by looking at the type of wrap.
+* The only valid way to apply `magicDict` is as described in the rewrite rule
+  above. If a user applies `magicDict` in an invalid way, we want to make this
+  obvious. To that end, GHC will signal about invalid uses of `magicDict` 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.
+  - If -dcore-lint is enabled, then any applications of `magicDict` that do not
+    satisfy the conditions described in the rewrite rule above will trigger a
+    Core Lint error.
 
+  - If -dcore-lint is not enabled, then as a last resort, we define `magicDict`
+    such that it panics at runtime. That way, any non-rewritten occurrences of
+    `magicDict` will crash the program.
 
 -------------------------------------------------------------
 @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/Dict.hs b/libraries/ghc-prim/GHC/Magic/Dict.hs
index d8bc70e9ff..9bff4d4e70 100644
--- a/libraries/ghc-prim/GHC/Magic/Dict.hs
+++ b/libraries/ghc-prim/GHC/Magic/Dict.hs
@@ -1,5 +1,9 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE Unsafe #-}
 
 -----------------------------------------------------------------------------
@@ -14,6 +18,9 @@
 --
 -- Defines the 'magicDict' function. For more information, see
 -- @Note [magicDictId magic]@ in "GHC.Types.Id.Make" in GHC.
+-- The definition of 'magicDict' is located in a separate module from
+-- "GHC.Magic" because 'magicDict' 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.
@@ -23,11 +30,12 @@
 module GHC.Magic.Dict (magicDict) where
 
 import GHC.Prim.Panic (panicError)
+import GHC.Types (RuntimeRep, TYPE)
 
 -- | 'magicDict' is a special-purpose placeholder value.
 -- 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 "Non-rewritten magicDict"#
diff --git a/libraries/ghc-prim/changelog.md b/libraries/ghc-prim/changelog.md
index 94ede15904..41a8f5f864 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.Dict` 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/ghci/scripts/T19667Ghci.hs b/testsuite/tests/ghci/scripts/T19667Ghci.hs
index 21e484bee9..4c47addd82 100644
--- a/testsuite/tests/ghci/scripts/T19667Ghci.hs
+++ b/testsuite/tests/ghci/scripts/T19667Ghci.hs
@@ -18,12 +18,10 @@ class KnownSymbol (n :: Symbol) where
 symbolVal :: forall n proxy . KnownSymbol n => proxy n -> String
 symbolVal _ = case symbolSing :: SSymbol n of SSymbol x -> x
 
-data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b)
-
 -- 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 = magicDict (WrapS k) (SSymbol n) (Proxy @(Any @Symbol))
+reifySymbol n k = magicDict @(KnownSymbol Any) (k @Any) (SSymbol n) (Proxy @(Any @Symbol))
 
 main :: IO ()
 main = print $ reifySymbol "Hello World" symbolVal
diff --git a/testsuite/tests/typecheck/should_run/T16646.hs b/testsuite/tests/typecheck/should_run/T16646.hs
new file mode 100644
index 0000000000..43b396fecf
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T16646.hs
@@ -0,0 +1,91 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+module Main where
+
+import Data.Kind (Type)
+import Data.Proxy (Proxy(..))
+import GHC.Exts (Any, magicDict)
+import GHC.TypeLits
+import Type.Reflection (TypeRep, typeRep, withTypeable)
+
+-----
+-- reflection
+-----
+
+class Reifies s a | s -> a where
+  reflect :: proxy s -> a
+
+instance KnownNat n => Reifies n Integer where
+  reflect = natVal
+
+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 = magicDict @(Reifies (Any @Type) a)
+                      @(forall (proxy :: Type -> Type). proxy Any -> 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
+  -- Type.Reflection
+  let f :: forall a. TypeRep a -> IO ()
+      f tr = withTypeable tr $ print $ typeRep @a
+   in f $ typeRep @Int
+
+  -- GHC.TypeLits
+  print $ someCharVal 'a'
+  print $ someNatVal 42
+  print $ someSymbolVal "Hello World"
+
+  -- reflection
+  print $ reify 6 (\p -> reflect p + reflect p)
+  print $ give (23 :: Int) foo True
+
+  -- singletons
+  print $ withSingI SFalse (sing @False)
diff --git a/testsuite/tests/typecheck/should_run/T16646.stdout b/testsuite/tests/typecheck/should_run/T16646.stdout
new file mode 100644
index 0000000000..9d2fdaadf5
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T16646.stdout
@@ -0,0 +1,7 @@
+Int
+'a'
+Just 42
+"Hello World"
+12
+42
+SFalse
diff --git a/testsuite/tests/typecheck/should_run/T19667.hs b/testsuite/tests/typecheck/should_run/T19667.hs
index 21e484bee9..4c47addd82 100644
--- a/testsuite/tests/typecheck/should_run/T19667.hs
+++ b/testsuite/tests/typecheck/should_run/T19667.hs
@@ -18,12 +18,10 @@ class KnownSymbol (n :: Symbol) where
 symbolVal :: forall n proxy . KnownSymbol n => proxy n -> String
 symbolVal _ = case symbolSing :: SSymbol n of SSymbol x -> x
 
-data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b)
-
 -- 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 = magicDict (WrapS k) (SSymbol n) (Proxy @(Any @Symbol))
+reifySymbol n k = magicDict @(KnownSymbol Any) (k @Any) (SSymbol n) (Proxy @(Any @Symbol))
 
 main :: IO ()
 main = print $ reifySymbol "Hello World" symbolVal
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',''])