Make Constraint not *apart* from Type.wip/T21092

More details in Note [coreView vs tcView]

Close #21092.

8 files changed, 50 insertions, 38 deletions

diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 1b5a21b733..7211b71742 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -379,21 +379,10 @@ while coreView is used during e.g. optimisation passes.
 
 See also #11715, which tracks removing this inconsistency.
 
-The inconsistency actually leads to a potential soundness bug, in that
-Constraint and Type are considered *apart* by the type family engine.
-To wit, we can write
-
-  type family F a
-  type instance F Type = Bool
-  type instance F Constraint = Int
-
-and (because Type ~# Constraint in Core), thus build a coercion between
-Int and Bool. I (Richard E) conjecture that this never happens in practice,
-but it's very uncomfortable. This, essentially, is the root problem
-underneath #11715, which is quite resistant to an easy fix. The best
-idea is to have roles in kind coercions, but that has yet to be implemented.
-See also "A Role for Dependent Types in Haskell", ICFP 2019, which describes
-how roles in kinds might work out.
+In order to prevent users from discerning between Type and Constraint
+(which could create inconsistent axioms -- see #21092), we say that
+Type and Constraint are not SurelyApart in the pure unifier. See
+GHC.Core.Unify.unify_ty, where this case produces MaybeApart.
 
 One annoying consequence of this inconsistency is that we can get ill-kinded
 updates to metavariables. #20356 is a case in point. Simplifying somewhat,
diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs
index 52e2a97ca2..9a6ffcb18d 100644
--- a/compiler/GHC/Core/Unify.hs
+++ b/compiler/GHC/Core/Unify.hs
@@ -56,6 +56,7 @@ import GHC.Data.FastString
 import Data.List ( mapAccumL )
 import Control.Monad
 import qualified Data.Semigroup as S
+import GHC.Builtin.Names (constraintKindTyConKey, liftedTypeKindTyConKey)
 
 {-
 
@@ -397,8 +398,8 @@ complete. This means that, sometimes, a closed type family does not reduce
 when it should. See test case indexed-types/should_fail/Overlap15 for an
 example.
 
-Note [Unificiation result]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Unification result]
+~~~~~~~~~~~~~~~~~~~~~~~~~
 When unifying t1 ~ t2, we return
 * Unifiable s, if s is a substitution such that s(t1) is syntactically the
   same as s(t2), modulo type-synonym expansion.
@@ -522,7 +523,7 @@ tcUnifyTyKis bind_fn tys1 tys2
 -- return the final result. See Note [Fine-grained unification]
 type UnifyResult = UnifyResultM TCvSubst
 
--- | See Note [Unificiation result]
+-- | See Note [Unification result]
 data UnifyResultM a = Unifiable a        -- the subst that unifies the types
                     | MaybeApart MaybeApartReason
                                  a       -- the subst has as much as we know
@@ -531,19 +532,25 @@ data UnifyResultM a = Unifiable a        -- the subst that unifies the types
                     | SurelyApart
                     deriving Functor
 
--- | Why are two types 'MaybeApart'? 'MARTypeFamily' takes precedence:
+-- | Why are two types 'MaybeApart'? 'MARInfinite' takes precedence:
 -- This is used (only) in Note [Infinitary substitution in lookup] in GHC.Core.InstEnv
+-- As of Feb 2022, we never differentiate between MARTypeFamily and MARTypeVsConstraint;
+-- it's really only MARInfinite that's interesting here.
 data MaybeApartReason = MARTypeFamily   -- ^ matching e.g. F Int ~? Bool
                       | MARInfinite     -- ^ matching e.g. a ~? Maybe a
+                      | MARTypeVsConstraint  -- ^ matching Type ~? Constraint
+                                             -- See Note [coreView vs tcView] in GHC.Core.Type
 
 instance Outputable MaybeApartReason where
-  ppr MARTypeFamily = text "MARTypeFamily"
-  ppr MARInfinite   = text "MARInfinite"
+  ppr MARTypeFamily       = text "MARTypeFamily"
+  ppr MARInfinite         = text "MARInfinite"
+  ppr MARTypeVsConstraint = text "MARTypeVsConstraint"
 
 instance Semigroup MaybeApartReason where
   -- see end of Note [Unification result] for why
-  MARTypeFamily <> r = r
-  MARInfinite   <> _ = MARInfinite
+  MARTypeFamily       <> r = r
+  MARInfinite         <> _ = MARInfinite
+  MARTypeVsConstraint <> r = r
 
 instance Applicative UnifyResultM where
   pure  = Unifiable
@@ -1052,13 +1059,22 @@ unify_ty :: UMEnv
 -- See Note [Specification of unification]
 -- Respects newtypes, PredTypes
 -- See Note [Computing equality on types] in GHC.Core.Type
-unify_ty env ty1 ty2 kco
+unify_ty _env (TyConApp tc1 []) (TyConApp tc2 []) _kco
   -- See Note [Comparing nullary type synonyms] in GHC.Core.Type.
-  | TyConApp tc1 [] <- ty1
-  , TyConApp tc2 [] <- ty2
-  , tc1 == tc2                = return ()
+  | tc1 == tc2
+  = return ()
+
+  -- See Note [coreView vs tcView] in GHC.Core.Type.
+  | tc1 `hasKey` constraintKindTyConKey
+  , tc2 `hasKey` liftedTypeKindTyConKey
+  = maybeApart MARTypeVsConstraint
 
-    -- TODO: More commentary needed here
+  | tc2 `hasKey` constraintKindTyConKey
+  , tc1 `hasKey` liftedTypeKindTyConKey
+  = maybeApart MARTypeVsConstraint
+
+unify_ty env ty1 ty2 kco
+    -- Now handle the cases we can "look through": synonyms and casts.
   | Just ty1' <- tcView ty1   = unify_ty env ty1' ty2 kco
   | Just ty2' <- tcView ty2   = unify_ty env ty1 ty2' kco
   | CastTy ty1' co <- ty1     = if um_unif env
diff --git a/testsuite/tests/indexed-types/should_fail/T21092.hs b/testsuite/tests/indexed-types/should_fail/T21092.hs
new file mode 100644
index 0000000000..7b92656d46
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T21092.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies #-}
+module T21092 where
+
+import Data.Kind
+
+type family F a
+
+type instance F Type = Int
+type instance F Constraint = Bool
diff --git a/testsuite/tests/indexed-types/should_fail/T21092.stderr b/testsuite/tests/indexed-types/should_fail/T21092.stderr
new file mode 100644
index 0000000000..b5b211cb38
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T21092.stderr
@@ -0,0 +1,5 @@
+
+T21092.hs:8:15: error:
+    Conflicting family instance declarations:
+      F (*) = Int -- Defined at T21092.hs:8:15
+      F Constraint = Bool -- Defined at T21092.hs:9:15
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index c5321fc455..5338a8780f 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -107,6 +107,7 @@ test('T8368', normal, compile_fail, [''])
 test('T8368a', normal, compile_fail, [''])
 test('T8518', normal, compile_fail, [''])
 test('T9036', normal, compile_fail, [''])
+test('T21092', normal, compile_fail, [''])
 test('T9167', normal, compile_fail, [''])
 test('T9171', normal, compile_fail, [''])
 test('T9097', normal, compile_fail, [''])
diff --git a/testsuite/tests/linters/notes.stdout b/testsuite/tests/linters/notes.stdout
index 57d2aa1367..a6cbf6efd2 100644
--- a/testsuite/tests/linters/notes.stdout
+++ b/testsuite/tests/linters/notes.stdout
@@ -20,7 +20,6 @@ ref    compiler/GHC/Core/TyCon.hs:2442:62:     Note [Sharing nullary TyCons]
 ref    compiler/GHC/Core/Unfold.hs:1171:23:     Note [INLINE for small functions (3)]
 ref    compiler/GHC/Core/Unfold.hs:1242:50:     Note [Unfold info lazy contexts]
 ref    compiler/GHC/Core/Unfold/Make.hs:157:34:     Note [DFunUnfoldings]
-ref    compiler/GHC/Core/Unify.hs:544:16:     Note [Unification result]
 ref    compiler/GHC/Core/Unify.hs:1390:9:     Note [INLINE pragmas and (>>)]
 ref    compiler/GHC/Core/Utils.hs:947:40:     Note [ _       -> [con1]
 ref    compiler/GHC/CoreToStg.hs:462:15:     Note [Nullary unboxed tuple]
diff --git a/testsuite/tests/typecheck/should_run/T11715.hs b/testsuite/tests/typecheck/should_run/T11715.hs
index 3baeb12de9..e8522fe9ee 100644
--- a/testsuite/tests/typecheck/should_run/T11715.hs
+++ b/testsuite/tests/typecheck/should_run/T11715.hs
@@ -3,17 +3,10 @@
 import Data.Kind
 import Data.Typeable
 
-type family F x a b
-type instance F Type       a b = a
-type instance F Constraint a b = b
-
-foo :: x :~: y -> F x a b -> F y a b
-foo Refl = id
-
 unsafeCoerce :: a -> b
 unsafeCoerce x = case eqT :: Maybe (Type :~: Constraint) of
                    Nothing -> error "No more bug!"
-                   Just r  -> foo r x
+                   Just r  -> error "Bug!"
 
 main :: IO ()
 main = let x :: Int
diff --git a/testsuite/tests/typecheck/should_run/T11715.stderr b/testsuite/tests/typecheck/should_run/T11715.stderr
index 6b7b2dd10b..ef267fa85f 100644
--- a/testsuite/tests/typecheck/should_run/T11715.stderr
+++ b/testsuite/tests/typecheck/should_run/T11715.stderr
@@ -1,3 +1,3 @@
 T11715: No more bug!
 CallStack (from HasCallStack):
-  error, called at T11715.hs:15:31 in main:Main
+  error, called at T11715.hs:8:31 in main:Main