diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/GHC/Core/Type.hs | 19 | ||||
| -rw-r--r-- | compiler/GHC/Core/Unify.hs | 42 |
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 |