Fix Constraint vs Type againwip/21530

This patch fixes two bugs exposed in #21530.  But it is
NOT the last word.   See the discussion in #15918.

The basic plan is this:

* Fix `unifyWanted` in Canonical, by making the FunTy/FunTy
  case check the AnonArgFlag.  This is an easy win.

* Make `mkCastTy` use a version of `isReflexiveCo` that distinguishes
  Constraint from Type.  This isn't really "right"; but it's more
  right than what we have.

9 files changed, 75 insertions, 12 deletions

diff --git a/compiler/GHC/Core/Coercion.hs-boot b/compiler/GHC/Core/Coercion.hs-boot
index cbc40e2a13..fe75381fa5 100644
--- a/compiler/GHC/Core/Coercion.hs-boot
+++ b/compiler/GHC/Core/Coercion.hs-boot
@@ -34,10 +34,13 @@ mkSubCo :: HasDebugCallStack => Coercion -> Coercion
 mkProofIrrelCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion
 mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
 
-isGReflCo :: Coercion -> Bool
-isReflCo :: Coercion -> Bool
-isReflexiveCo :: Coercion -> Bool
-decomposePiCos :: HasDebugCallStack => Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion)
+isGReflCo     :: Coercion  -> Bool
+isReflCo      :: Coercion  -> Bool
+isReflexiveCo :: Coercion  -> Bool
+isGReflMCo    :: MCoercion -> Bool
+
+decomposePiCos :: HasDebugCallStack
+               => Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion)
 coVarKindsTypesRole :: HasDebugCallStack => CoVar -> (Kind, Kind, Type, Type, Role)
 coVarRole :: CoVar -> Role
 
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 76dec32239..28c75fd6fd 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -276,12 +276,12 @@ import {-# SOURCE #-} GHC.Core.Coercion
    , mkForAllCo, mkFunCo, mkAxiomInstCo, mkUnivCo
    , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo
    , mkKindCo, mkSubCo
-   , decomposePiCos, coercionKind, coercionLKind
-   , coercionRKind, coercionType
-   , isReflexiveCo, seqCo
+   , decomposePiCos
+   , coercionKind, coercionLKind, coercionRKind, coercionType
+   , isGReflMCo, seqCo
    , topNormaliseNewType_maybe
    )
-import {-# SOURCE #-} GHC.Tc.Utils.TcType ( isConcreteTyVar )
+import {-# SOURCE #-} GHC.Tc.Utils.TcType ( isConcreteTyVar, tcEqType )
 
 -- others
 import GHC.Utils.Misc
@@ -1613,7 +1613,8 @@ splitCastTy_maybe ty
 -- Coercion for reflexivity, dropping it if it's reflexive.
 -- See @Note [Respecting definitional equality]@ in "GHC.Core.TyCo.Rep"
 mkCastTy :: Type -> Coercion -> Type
-mkCastTy orig_ty co | isReflexiveCo co = orig_ty  -- (EQ2) from the Note
+mkCastTy orig_ty co
+  | hackyIsReflexiveCo co = orig_ty  -- (EQ2) from the Note
 -- NB: Do the slow check here. This is important to keep the splitXXX
 -- functions working properly. Otherwise, we may end up with something
 -- like (((->) |> something_reflexive_but_not_obviously_so) biz baz)
@@ -1621,6 +1622,18 @@ mkCastTy orig_ty co | isReflexiveCo co = orig_ty  -- (EQ2) from the Note
 -- in test dependent/should_compile/dynamic-paper.
 mkCastTy orig_ty co = mk_cast_ty orig_ty co
 
+hackyIsReflexiveCo :: Coercion -> Bool
+-- This function distinguishes Constraint from Type, so that mkCastTy
+-- works ok in the typechecker as well as in Core.  See #21530 for the
+-- sad story.
+--
+-- I'm worried about invalidating (EQ2), but that is already squishy
+-- across the Tc-to-Core transition.
+hackyIsReflexiveCo (Refl {})       = True
+hackyIsReflexiveCo (GRefl _ _ mco) = isGReflMCo mco
+hackyIsReflexiveCo co              = ty1 `tcEqType` ty2
+  where Pair ty1 ty2 = coercionKind co
+
 -- | Like 'mkCastTy', but avoids checking the coercion for reflexivity,
 -- as that can be expensive.
 mk_cast_ty :: Type -> Coercion -> Type
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index f63cb5c030..7b6af2b740 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -3081,7 +3081,9 @@ unifyWanted rewriters loc role orig_ty1 orig_ty2
     go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2
     go ty1 ty2 | Just ty2' <- tcView ty2 = go ty1 ty2'
 
-    go (FunTy _ w1 s1 t1) (FunTy _ w2 s2 t2)
+    go (FunTy { ft_af = af1, ft_mult = w1, ft_arg = s1, ft_res = t1 })
+       (FunTy { ft_af = af2, ft_mult = w2, ft_arg = s2, ft_res = t2 })
+      | af1 == af2  -- Important!  See #21530
       = do { co_s <- unifyWanted rewriters loc role s1 s2
            ; co_t <- unifyWanted rewriters loc role t1 t2
            ; co_w <- unifyWanted rewriters loc Nominal w1 w2
diff --git a/compiler/GHC/Tc/Utils/TcType.hs-boot b/compiler/GHC/Tc/Utils/TcType.hs-boot
index 4d09c1e7e1..0787bb51ff 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs-boot
+++ b/compiler/GHC/Tc/Utils/TcType.hs-boot
@@ -11,9 +11,10 @@ data MetaDetails
 data TcTyVarDetails
 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
 vanillaSkolemTvUnk :: HasCallStack => TcTyVarDetails
-isMetaTyVar :: TcTyVar -> Bool
+
+isMetaTyVar      :: TcTyVar -> Bool
 isTyConableTyVar :: TcTyVar -> Bool
-isConcreteTyVar :: TcTyVar -> Bool
+isConcreteTyVar  :: TcTyVar -> Bool
 
 tcEqType :: HasDebugCallStack => Type -> Type -> Bool
 
diff --git a/testsuite/tests/polykinds/T21530a.hs b/testsuite/tests/polykinds/T21530a.hs
new file mode 100644
index 0000000000..e33381fbfd
--- /dev/null
+++ b/testsuite/tests/polykinds/T21530a.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE RankNTypes #-}
+
+module T21530 where
+
+f :: (forall a. (Show a, Eq a) => a -> String) -> String
+f h = h True
+
+g :: (forall a. Show a => a -> String) -> String
+g = f
diff --git a/testsuite/tests/polykinds/T21530a.stderr b/testsuite/tests/polykinds/T21530a.stderr
new file mode 100644
index 0000000000..4d504ef901
--- /dev/null
+++ b/testsuite/tests/polykinds/T21530a.stderr
@@ -0,0 +1,8 @@
+
+T21530a.hs:9:5: error:
+    • Couldn't match type: Eq a => a -> String
+                     with: a -> String
+      Expected: (forall a. Show a => a -> String) -> String
+        Actual: (forall a. (Show a, Eq a) => a -> String) -> String
+    • In the expression: f
+      In an equation for ‘g’: g = f
diff --git a/testsuite/tests/polykinds/T21530b.hs b/testsuite/tests/polykinds/T21530b.hs
new file mode 100644
index 0000000000..e0afe1b873
--- /dev/null
+++ b/testsuite/tests/polykinds/T21530b.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeApplications #-}
+
+module Foo where
+
+import Data.Kind
+import Data.Proxy
+
+f :: forall (a :: Type). Proxy a -> Int
+f = f
+
+g :: Proxy (Eq Int)
+g = g
+
+h = f g
diff --git a/testsuite/tests/polykinds/T21530b.stderr b/testsuite/tests/polykinds/T21530b.stderr
new file mode 100644
index 0000000000..552d9f915d
--- /dev/null
+++ b/testsuite/tests/polykinds/T21530b.stderr
@@ -0,0 +1,11 @@
+
+T21530b.hs:14:7: error:
+    • Couldn't match kind ‘Constraint’ with ‘*’
+      When matching types
+        a0 :: *
+        Eq Int :: Constraint
+      Expected: Proxy a0
+        Actual: Proxy (Eq Int)
+    • In the first argument of ‘f’, namely ‘g’
+      In the expression: f g
+      In an equation for ‘h’: h = f g
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 459ba1350d..0cba0b4c1f 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -239,3 +239,5 @@ test('T19739a', normal, compile, [''])
 test('T19739b', normal, compile, [''])
 test('T19739c', normal, compile, [''])
 test('T19739d', normal, compile, [''])
+test('T21530a', normal, compile_fail, [''])
+test('T21530b', normal, compile_fail, [''])