From af6932d6c068361c6ae300d52e72fbe13f8e1f18 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simon.peytonjones@gmail.com>
Date: Mon, 8 Jan 2024 10:49:49 +0000
Subject: [PATCH] Make TYPE and CONSTRAINT not-apart

Issue #24279 showed up a bug in the logic in GHC.Core.Unify.unify_ty
which is supposed to make TYPE and CONSTRAINT be not-apart.

Easily fixed.
---
 compiler/GHC/Core/Unify.hs                    |  7 +++--
 .../tests/typecheck/should_fail/T24279.hs     | 31 +++++++++++++++++++
 .../tests/typecheck/should_fail/T24279.stderr | 19 ++++++++++++
 testsuite/tests/typecheck/should_fail/all.T   |  1 +
 4 files changed, 56 insertions(+), 2 deletions(-)
 create mode 100644 testsuite/tests/typecheck/should_fail/T24279.hs
 create mode 100644 testsuite/tests/typecheck/should_fail/T24279.stderr

diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs
index 8dcbc09953be..ed43e139889f 100644
--- a/compiler/GHC/Core/Unify.hs
+++ b/compiler/GHC/Core/Unify.hs
@@ -31,6 +31,7 @@ import GHC.Types.Var
 import GHC.Types.Var.Env
 import GHC.Types.Var.Set
 import GHC.Types.Name( Name, mkSysTvName, mkSystemVarName )
+import GHC.Builtin.Names( tYPETyConKey, cONSTRAINTTyConKey )
 import GHC.Core.Type     hiding ( getTvSubstEnv )
 import GHC.Core.Coercion hiding ( getCvSubstEnv )
 import GHC.Core.TyCon
@@ -1149,8 +1150,10 @@ unify_ty env ty1 ty2 _kco
   -- TYPE and CONSTRAINT are not Apart
   -- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim
   -- NB: at this point we know that the two TyCons do not match
-  | Just {} <- sORTKind_maybe ty1
-  , Just {} <- sORTKind_maybe ty2
+  | Just (tc1,_) <- mb_tc_app1, let u1 = tyConUnique tc1
+  , Just (tc2,_) <- mb_tc_app2, let u2 = tyConUnique tc2
+  , (u1 == tYPETyConKey && u2 == cONSTRAINTTyConKey) ||
+    (u2 == tYPETyConKey && u1 == cONSTRAINTTyConKey)
   = maybeApart MARTypeVsConstraint
     -- We don't bother to look inside; wrinkle (W3) in GHC.Builtin.Types.Prim
     -- Note [Type and Constraint are not apart]
diff --git a/testsuite/tests/typecheck/should_fail/T24279.hs b/testsuite/tests/typecheck/should_fail/T24279.hs
new file mode 100644
index 000000000000..e659c78e50d4
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T24279.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE TypeFamilies #-}
+module T24279 where
+
+import GHC.Exts
+import Data.Kind
+
+type F :: (RuntimeRep -> Type) -> Type
+type family F a where
+  F TYPE = Int
+  F CONSTRAINT = Bool
+
+type G :: Type -> RuntimeRep -> Type
+type family G a where
+  G (a b) = a
+
+-- Should be rejected
+foo :: (F (G Constraint)) -> Bool
+foo x = x
+
+
+type family H a b where
+  H a a = Int
+  H a b = Bool
+
+-- Should be rejected
+bar1 :: H TYPE CONSTRAINT -> Int
+bar1 x = x
+
+-- Should be rejected
+bar2 :: H Type Constraint -> Int
+bar2 x = x
diff --git a/testsuite/tests/typecheck/should_fail/T24279.stderr b/testsuite/tests/typecheck/should_fail/T24279.stderr
new file mode 100644
index 000000000000..6c4880ce94ad
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T24279.stderr
@@ -0,0 +1,19 @@
+
+T24279.hs:18:9: error: [GHC-83865]
+    • Couldn't match type ‘F CONSTRAINT’ with ‘Bool’
+      Expected: Bool
+        Actual: F (G Constraint)
+    • In the expression: x
+      In an equation for ‘foo’: foo x = x
+
+T24279.hs:27:10: error: [GHC-83865]
+    • Couldn't match expected type ‘Int’
+                  with actual type ‘H TYPE CONSTRAINT’
+    • In the expression: x
+      In an equation for ‘bar1’: bar1 x = x
+
+T24279.hs:31:10: error: [GHC-83865]
+    • Couldn't match expected type ‘Int’
+                  with actual type ‘H (*) Constraint’
+    • In the expression: x
+      In an equation for ‘bar2’: bar2 x = x
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 48f1f7d1b4a2..e4bb647ee06d 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -711,3 +711,4 @@ test('T17940', normal, compile_fail, [''])
 test('ErrorIndexLinks', normal, compile_fail, ['-fprint-error-index-links=always'])
 test('T24064', normal, compile_fail, [''])
 test('T24298', normal, compile_fail, [''])
+test('T24279', normal, compile_fail, [''])
-- 
GitLab