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

15 files changed, 87 insertions, 41 deletions

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