Make Constraint not *apart* from Type.

More details in Note [coreView vs tcView]

Close #21092.

2 files changed, 33 insertions, 28 deletions

diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index e05acf1881..c71bbdfc9e 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -380,21 +380,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