Use tcEqType in GHC.Core.Unify.uVar

  Because uVar used eqType instead of tcEqType, it was possible
  to accumulate a substitution that unified Type and Constraint.

  For example, a call to `tc_unify_tys` with arguments

    tys1 = [ k, k ]
    tys2 = [ Type, Constraint ]

  would first add `k = Type` to the substitution. That's fine, but then
  the second call to `uVar` would claim that the substitution also
  unifies `k` with `Constraint`. This could then be used to cause
  trouble, as per #20521.

  Fixes #20521

13 files changed, 73 insertions, 10 deletions

diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs
index 2e6b89f355..a4dbdcb75d 100644
--- a/compiler/GHC/Core/Unify.hs
+++ b/compiler/GHC/Core/Unify.hs
@@ -47,6 +47,7 @@ import GHC.Utils.Outputable
 import GHC.Types.Unique
 import GHC.Types.Unique.FM
 import GHC.Types.Unique.Set
+import {-# SOURCE #-} GHC.Tc.Utils.TcType ( tcEqType )
 import GHC.Exts( oneShot )
 import GHC.Utils.Panic
 import GHC.Utils.Panic.Plain
@@ -1236,8 +1237,17 @@ uVar env tv1 ty kco
                       -- this is because the range of the subst is the target
                       -- type, not the template type. So, just check for
                       -- normal type equality.
-                      unless ((ty' `mkCastTy` kco) `eqType` ty) $
-                      surelyApart
+                      unless ((ty' `mkCastTy` kco) `tcEqType` ty) $
+                        surelyApart
+                      -- NB: it's important to use `tcEqType` instead of `eqType` here,
+                      -- otherwise we might not reject a substitution
+                      -- which unifies `Type` with `Constraint`, e.g.
+                      -- a call to tc_unify_tys with arguments
+                      --
+                      --   tys1 = [k,k]
+                      --   tys2 = [Type, Constraint]
+                      --
+                      -- See test cases: T11715b, T20521.
           Nothing  -> uUnrefined env tv1' ty ty kco } -- No, continue
 
 uUnrefined :: UMEnv
@@ -1549,6 +1559,8 @@ ty_co_match menv subst ty co lkco rkco
   | tyCoVarsOfType ty `isNotInDomainOf` subst
   , Just (ty', _) <- isReflCo_maybe co
   , ty `eqType` ty'
+    -- Why `eqType` and not `tcEqType`? Because this function is only used
+    -- during coercion optimisation, after type-checking has finished.
   = Just subst
 
   where
diff --git a/compiler/GHC/Tc/Utils/TcType.hs-boot b/compiler/GHC/Tc/Utils/TcType.hs-boot
index 6b808dd7ab..2a7a34dc97 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs-boot
+++ b/compiler/GHC/Tc/Utils/TcType.hs-boot
@@ -2,6 +2,8 @@ module GHC.Tc.Utils.TcType where
 import GHC.Utils.Outputable( SDoc )
 import GHC.Prelude ( Bool )
 import {-# SOURCE #-} GHC.Types.Var ( TcTyVar )
+import {-# SOURCE #-} GHC.Core.TyCo.Rep
+import GHC.Utils.Misc ( HasDebugCallStack )
 
 data MetaDetails
 
@@ -10,3 +12,5 @@ pprTcTyVarDetails :: TcTyVarDetails -> SDoc
 vanillaSkolemTv :: TcTyVarDetails
 isMetaTyVar :: TcTyVar -> Bool
 isTyConableTyVar :: TcTyVar -> Bool
+
+tcEqType :: HasDebugCallStack => Type -> Type -> Bool
diff --git a/testsuite/tests/indexed-types/should_compile/T11715b.hs b/testsuite/tests/indexed-types/should_compile/T11715b.hs
new file mode 100644
index 0000000000..361653595d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T11715b.hs
@@ -0,0 +1,20 @@
+
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+
+module T11715b where
+
+import Data.Kind ( Constraint )
+
+type Id :: ( k -> Constraint ) -> l -> Constraint
+type family   Id a
+type instance Id f = f
+
+type T = Id Eq (Eq Bool)
+-- this should remain stuck, instead of
+-- reducing to the ill-kinded `Eq (Eq Bool)`
+-- The type family equation for Id should not apply,
+-- as this application is of the form `Id @Type @Constraint`
+-- whereas the type family axiom is of the form `Id @k @k`.
diff --git a/testsuite/tests/indexed-types/should_compile/T11715b.script b/testsuite/tests/indexed-types/should_compile/T11715b.script
new file mode 100644
index 0000000000..7af739a7f0
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T11715b.script
@@ -0,0 +1,2 @@
+:l T11715b
+:kind! T
diff --git a/testsuite/tests/indexed-types/should_compile/T11715b.stdout b/testsuite/tests/indexed-types/should_compile/T11715b.stdout
new file mode 100644
index 0000000000..e8bdfb98f0
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T11715b.stdout
@@ -0,0 +1,2 @@
+T :: Constraint
+= Id Eq (Eq Bool)
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 7d8aa9f3ae..c2f6b12aaf 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -303,3 +303,4 @@ test('T18875', normal, compile, [''])
 test('T8707', normal, compile, ['-O'])
 test('T14111', normal, compile, ['-O'])
 test('T19336', normal, compile, ['-O'])
+test('T11715b', normal, ghci_script, ['T11715b.script'])
diff --git a/testsuite/tests/indexed-types/should_fail/T20521.hs b/testsuite/tests/indexed-types/should_fail/T20521.hs
new file mode 100644
index 0000000000..397648fc5d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T20521.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T20521 where
+
+import Data.Kind
+
+type XFam :: forall k l -> k -> l
+type family XFam k l x where
+  forall k (x :: k). XFam k k x = x
+
+type C2T c = XFam Constraint Type c
+type T2C t = XFam Type Constraint t
+
+bad :: C2T (T2C Float) -> Float
+bad x = x
diff --git a/testsuite/tests/indexed-types/should_fail/T20521.stderr b/testsuite/tests/indexed-types/should_fail/T20521.stderr
new file mode 100644
index 0000000000..2909a9c892
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T20521.stderr
@@ -0,0 +1,9 @@
+
+T20521.hs:19:9: error:
+    • Couldn't match type ‘XFam
+                             Constraint (*) (XFam (*) Constraint Float)’
+                     with ‘Float’
+      Expected: Float
+        Actual: C2T (T2C Float)
+    • In the expression: x
+      In an equation for ‘bad’: bad x = x
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index c97c8c56e4..c3d98b43f0 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -165,3 +165,4 @@ test('T13571a', normal, compile_fail, [''])
 test('T18648', normal, compile_fail, [''])
 test('ExpandTFs', normal, compile_fail, [''])
 test('T20465', normal, compile_fail, [''])
+test('T20521', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T20356.hs b/testsuite/tests/typecheck/should_compile/T20356.hs
index 6a847cb22a..6a847cb22a 100644
--- a/testsuite/tests/typecheck/should_fail/T20356.hs
+++ b/testsuite/tests/typecheck/should_compile/T20356.hs
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 1a7c9567ce..a2bb10ba02 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -805,3 +805,4 @@ test('T20181', normal, compile, [''])
 test('T20241', normal, compile, [''])
 test('T20187a', normal, compile, ['-Wredundant-strictness-flags'])
 test('T20187b', normal, compile, ['-Wredundant-strictness-flags'])
+test('T20356', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T20356.stderr b/testsuite/tests/typecheck/should_fail/T20356.stderr
deleted file mode 100644
index 476b71a385..0000000000
--- a/testsuite/tests/typecheck/should_fail/T20356.stderr
+++ /dev/null
@@ -1,7 +0,0 @@
-
-T20356.hs:18:10: error:
-    • Couldn't match kind ‘*’ with ‘Constraint’
-      When matching the kind of ‘Eq’
-    • In the first argument of ‘id'’, namely ‘(MkProxy @T)’
-      In the expression: id' (MkProxy @T)
-      In an equation for ‘z’: z = id' (MkProxy @T)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index aea4b132cb..3aba1c9ac0 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -606,7 +606,6 @@ test('TyAppPat_ScopedTyVarConflict', normal, compile_fail, [''])
 test('TyAppPat_TooMany', normal, compile_fail, [''])
 test('T12178a', normal, compile_fail, [''])
 test('T18869', normal, compile_fail, [''])
-test('T20356', normal, compile_fail, [''])
 test('T19142', normal, compile_fail, [''])
 test('T19346', normal, compile_fail, ['-fprint-typechecker-elaboration'])
 test('T19364', normal, compile_fail, [''])