Make mkFunCo take AnonArgFlags into accountwip/T21328

Previously, whenever `mkFunCo` would produce reflexive coercions, it would
use `mkVisFunTy` to produce the kind of the coercion. However, `mkFunCo` is
also used to produce coercions between types of the form `ty1 => ty2` in
certain places. This has the unfortunate side effect of causing the type of
the coercion to appear as `ty1 -> ty2` in certain error messages, as spotted
in #21328.

This patch address this by changing replacing the use of `mkVisFunTy` with
`mkFunctionType` in `mkFunCo`. `mkFunctionType` checks the kind of `ty1` and
makes the function arrow `=>` instead of `->` if `ty1` has kind `Constraint`,
so this should always produce the correct `AnonArgFlag`. As a result, this
patch fixes part (2) of #21328.

This is not the only possible way to fix #21328, as the discussion on that
issue lists some possible alternatives. Ultimately, it was concluded that the
alternatives would be difficult to maintain, and since we already use
`mkFunctionType` in `coercionLKind` and `coercionRKind`, using `mkFunctionType`
in `mkFunCo` is consistent with this choice. Moreover, using `mkFunctionType`
does not regress the performance of any test case we have in GHC's test suite.

4 files changed, 19 insertions, 2 deletions

diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 4cfdc3ee82..235e8c65fb 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -792,14 +792,15 @@ mkTyConAppCo r tc cos
   | otherwise = TyConAppCo r tc cos
 
 -- | Build a function 'Coercion' from two other 'Coercion's. That is,
--- given @co1 :: a ~ b@ and @co2 :: x ~ y@ produce @co :: (a -> x) ~ (b -> y)@.
+-- given @co1 :: a ~ b@ and @co2 :: x ~ y@ produce @co :: (a -> x) ~ (b -> y)@
+-- or @(a => x) ~ (b => y)@, depending on the kind of @a@/@b@.
 mkFunCo :: Role -> CoercionN -> Coercion -> Coercion -> Coercion
 mkFunCo r w co1 co2
     -- See Note [Refl invariant]
   | Just (ty1, _) <- isReflCo_maybe co1
   , Just (ty2, _) <- isReflCo_maybe co2
   , Just (w, _) <- isReflCo_maybe w
-  = mkReflCo r (mkVisFunTy w ty1 ty2)
+  = mkReflCo r (mkFunctionType w ty1 ty2)
   | otherwise = FunCo r w co1 co2
 
 -- | Apply a 'Coercion' to another 'Coercion'.
diff --git a/testsuite/tests/typecheck/should_fail/T21328.hs b/testsuite/tests/typecheck/should_fail/T21328.hs
new file mode 100644
index 0000000000..f589c5d3a7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T21328.hs
@@ -0,0 +1,11 @@
+{-# 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
new file mode 100644
index 0000000000..a7d106a793
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T21328.stderr
@@ -0,0 +1,4 @@
+
+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 c856ca7e95..aceaf051c9 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -653,4 +653,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, [''])