diff --git a/compiler/GHC/Core/Coercion/Opt.hs b/compiler/GHC/Core/Coercion/Opt.hs
index 55cff8999d67100760f389ca78bf2d6ccc9c1d7d..2f9cfb1133ff3c57167c36c219636ad46d8437b1 100644
--- a/compiler/GHC/Core/Coercion/Opt.hs
+++ b/compiler/GHC/Core/Coercion/Opt.hs
@@ -1113,7 +1113,7 @@ co3 = axEq[1] (axId[0] Int) (axId[0] Bool)
:: Equal (Id Int) (Id Bool) ~ False
which is bogus! This is because the type system isn't smart enough to know
-that (Id Int) and (Id Bool) are Surely Apart, as they're headed by type
+that (Id Int) and (Id Bool) are SurelyApart, as they're headed by type
families. At the time of writing, I (Richard Eisenberg) couldn't think of
a way of detecting this any more efficient than just building the optimised
coercion and checking.
diff --git a/compiler/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs
index a44169329e10ba885df109a6c8161be5483bf6e1..bedf309a40d192e946e02960fa56f911b7baad4f 100644
--- a/compiler/GHC/Core/FamInstEnv.hs
+++ b/compiler/GHC/Core/FamInstEnv.hs
@@ -488,8 +488,8 @@ Here is how we do it:
apart(target, pattern) = not (unify(flatten(target), pattern))
where flatten (implemented in flattenTys, below) converts all type-family
-applications into fresh variables. (See
-Note [Flattening type-family applications when matching instances] in GHC.Core.Unify.)
+applications into fresh variables. (See Note [Apartness and type families]
+in GHC.Core.Unify.)
Note [Compatibility]
~~~~~~~~~~~~~~~~~~~~
@@ -513,11 +513,11 @@ might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int
only when we can be sure that 'a' is not Int.
To achieve this, after finding a possible match within the equations, we have to
-go back to all previous equations and check that, under the
-substitution induced by the match, other branches are surely apart. (See
-Note [Apartness].) This is similar to what happens with class
-instance selection, when we need to guarantee that there is only a match and
-no unifiers. The exact algorithm is different here because the
+go back to all previous equations and check that, under the substitution induced
+by the match, other branches are surely apart, using `tcUnifyTysFG`. (See
+Note [Apartness and type families] in GHC.Core.Unify.) This is similar to what
+happens with class instance selection, when we need to guarantee that there is
+only a match and no unifiers. The exact algorithm is different here because the
potentially-overlapping group is closed.
As another example, consider this:
@@ -580,7 +580,7 @@ fails anyway.
compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
- = case tcUnifyTysFG alwaysBindFun commonlhs1 commonlhs2 of
+ = case tcUnifyTysFG alwaysBindFam alwaysBindTv commonlhs1 commonlhs2 of
-- Here we need the cab_tvs of the two branches to be disinct.
-- See Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom.
SurelyApart -> True
@@ -611,7 +611,8 @@ injectiveBranches injectivity
-- See Note [Verifying injectivity annotation], case 1.
= let getInjArgs = filterByList injectivity
in_scope = mkInScopeSetList (tvs1 ++ tvs2)
- in case tcUnifyTyWithTFs True in_scope rhs1 rhs2 of -- True = two-way pre-unification
+ in case tcUnifyTyForInjectivity True in_scope rhs1 rhs2 of
+ -- True = two-way pre-unification
Nothing -> InjectivityAccepted
-- RHS are different, so equations are injective.
-- This is case 1A from Note [Verifying injectivity annotation]
@@ -1229,22 +1230,16 @@ findBranch branches target_tys
-> Maybe (BranchIndex, [Type], [Coercion])
go (index, branch) other
= let (CoAxBranch { cab_tvs = tpl_tvs, cab_cvs = tpl_cvs
- , cab_lhs = tpl_lhs
- , cab_incomps = incomps }) = branch
- in_scope = mkInScopeSet (unionVarSets $
- map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
- -- See Note [Flattening type-family applications when matching instances]
- -- in GHC.Core.Unify
- flattened_target = flattenTys in_scope target_tys
+ , cab_lhs = tpl_lhs }) = branch
in case tcMatchTys tpl_lhs target_tys of
- Just subst -- matching worked. now, check for apartness.
- | apartnessCheck flattened_target branch
- -> -- matching worked & we're apart from all incompatible branches.
+ Just subst -- Matching worked. now, check for apartness.
+ | apartnessCheck target_tys branch
+ -> -- Matching worked & we're apart from all incompatible branches.
-- success
assert (all (isJust . lookupCoVar subst) tpl_cvs) $
Just (index, substTyVars subst tpl_tvs, substCoVars subst tpl_cvs)
- -- failure. keep looking
+ -- Failure. keep looking
_ -> other
-- | Do an apartness check, as described in the "Closed Type Families" paper
@@ -1252,15 +1247,12 @@ findBranch branches target_tys
-- ('CoAxBranch') of a closed type family can be used to reduce a certain target
-- type family application.
apartnessCheck :: [Type]
- -- ^ /flattened/ target arguments. Make sure they're flattened! See
- -- Note [Flattening type-family applications when matching instances]
- -- in GHC.Core.Unify.
- -> CoAxBranch -- ^ the candidate equation we wish to use
+ -> CoAxBranch -- ^ The candidate equation we wish to use
-- Precondition: this matches the target
-> Bool -- ^ True <=> equation can fire
-apartnessCheck flattened_target (CoAxBranch { cab_incomps = incomps })
+apartnessCheck target (CoAxBranch { cab_incomps = incomps })
= all (isSurelyApart
- . tcUnifyTysFG alwaysBindFun flattened_target
+ . tcUnifyTysFG alwaysBindFam alwaysBindTv target
. coAxBranchLHS) incomps
where
isSurelyApart SurelyApart = True
diff --git a/compiler/GHC/Core/InstEnv.hs b/compiler/GHC/Core/InstEnv.hs
index ee44c7e6afd867e2f9f3b22d5c3c19e74e2be85b..6ca5fd0de3dbab53a5e4f6df67f6fe2f8e828f0e 100644
--- a/compiler/GHC/Core/InstEnv.hs
+++ b/compiler/GHC/Core/InstEnv.hs
@@ -174,7 +174,7 @@ That is, they are
Reason for freshness: we use unification when checking for overlap
etc, and that requires the tyvars to be distinct.
-The invariant is checked by the ASSERT in lookupInstEnv'.
+The invariant is checked by the ASSERT in instEnvMatchesAndUnifiers.
Note [Proper-match fields]
~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1105,11 +1105,12 @@ nullUnifiers :: PotentialUnifiers -> Bool
nullUnifiers NoUnifiers{} = True
nullUnifiers _ = False
-lookupInstEnv' :: InstEnv -- InstEnv to look in
- -> VisibleOrphanModules -- But filter against this
- -> Class -> [Type] -- What we are looking for
- -> ([InstMatch], -- Successful matches
- PotentialUnifiers) -- These don't match but do unify
+instEnvMatchesAndUnifiers
+ :: InstEnv -- InstEnv to look in
+ -> VisibleOrphanModules -- But filter against this
+ -> Class -> [Type] -- What we are looking for
+ -> ([InstMatch], -- Successful matches
+ PotentialUnifiers) -- These don't match but do unify
-- (no incoherent ones in here)
-- The second component of the result pair happens when we look up
-- Foo [a]
@@ -1121,7 +1122,7 @@ lookupInstEnv' :: InstEnv -- InstEnv to look in
-- but Foo [Int] is a unifier. This gives the caller a better chance of
-- giving a suitable error message
-lookupInstEnv' (InstEnv rm) vis_mods cls tys
+instEnvMatchesAndUnifiers (InstEnv rm) vis_mods cls tys
= (foldr check_match [] rough_matches, check_unifiers rough_unifiers)
where
(rough_matches, rough_unifiers) = lookupRM' rough_tcs rm
@@ -1159,10 +1160,14 @@ lookupInstEnv' (InstEnv rm) vis_mods cls tys
-- Unification will break badly if the variables overlap
-- They shouldn't because we allocate separate uniques for them
-- See Note [Template tyvars are fresh]
- case tcUnifyTysFG instanceBindFun tpl_tys tys of
+ case tcUnifyTysFG alwaysBindFam instanceBindFun tpl_tys tys of
+ -- alwaysBindFam: the family-application can't be in the instance head,
+ -- but it certainly can be in the Wanted constraint we are matching!
+ --
-- We consider MaybeApart to be a case where the instance might
-- apply in the future. This covers an instance like C Int and
-- a target like [W] C (F a), where F is a type family.
+ -- See (ATF1) in Note [Apartness and type families] in GHC.Core.Unify
SurelyApart -> check_unifiers items
-- See Note [Infinitary substitution in lookup]
MaybeApart MARInfinite _ -> check_unifiers items
@@ -1204,8 +1209,8 @@ lookupInstEnv check_overlap_safe
tys
= (final_matches, final_unifs, unsafe_overlapped)
where
- (home_matches, home_unifs) = lookupInstEnv' home_ie vis_mods cls tys
- (pkg_matches, pkg_unifs) = lookupInstEnv' pkg_ie vis_mods cls tys
+ (home_matches, home_unifs) = instEnvMatchesAndUnifiers home_ie vis_mods cls tys
+ (pkg_matches, pkg_unifs) = instEnvMatchesAndUnifiers pkg_ie vis_mods cls tys
all_matches = home_matches <> pkg_matches
all_unifs = home_unifs <> pkg_unifs
final_matches = pruneOverlappedMatches all_matches
@@ -1576,14 +1581,14 @@ specialisation: overview] details how we achieve that.
************************************************************************
-}
-instanceBindFun :: BindFun
-instanceBindFun tv _rhs_ty | isOverlappableTyVar tv = Apart
+instanceBindFun :: BindTvFun
+instanceBindFun tv _rhs_ty | isOverlappableTyVar tv = DontBindMe
| otherwise = BindMe
- -- Note [Binding when looking up instances]
+ -- Note [Super skolems: binding when looking up instances]
{-
-Note [Binding when looking up instances]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Super skolems: binding when looking up instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When looking up in the instance environment, or family-instance environment,
we are careful about multiple matches, as described above in
Note [Overlapping instances]
@@ -1599,9 +1604,9 @@ them in the unification test. These are called "super skolems". Example:
f :: T -> Int
f (MkT x) = op [x,x]
The op [x,x] means we need (Foo [a]). This `a` will never be instantiated, and
-so it is a super skolem. (See the use of tcInstSuperSkolTyVarsX in
+so it is a "super skolem". (See the use of tcInstSuperSkolTyVarsX in
GHC.Tc.Gen.Pat.tcDataConPat.) Super skolems respond True to
-isOverlappableTyVar, and the use of Apart in instanceBindFun, above, means
+isOverlappableTyVar, and the use of DontBindMe in instanceBindFun, above, means
that these will be treated as fresh constants in the unification algorithm
during instance lookup. Without this treatment, GHC would complain, saying
that the choice of instance depended on the instantiation of 'a'; but of
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index 9452841173ca532eafa3a890c9df066fc71d2723..de8292f3af220f620770e33cded32a35b97bd7d7 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -2756,7 +2756,7 @@ lintBranch this_co fam_tc branch arg_kinds
; _ <- foldlM check_ki (empty_subst, empty_subst)
(zip (ktvs ++ cvs) arg_kinds)
- ; case check_no_conflict flattened_target incomps of
+ ; case check_no_conflict target incomps of
Nothing -> return ()
Just bad_branch -> failWithL $ bad_ax this_co $
text "inconsistent with" <+>
@@ -2782,15 +2782,12 @@ lintBranch this_co fam_tc branch arg_kinds
subst = zipTvSubst tvs tys `composeTCvSubst`
zipCvSubst cvs co_args
target = Type.substTys subst (coAxBranchLHS branch)
- in_scope = mkInScopeSet $
- unionVarSets (map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
- flattened_target = flattenTys in_scope target
check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
check_no_conflict _ [] = Nothing
check_no_conflict flat (b@CoAxBranch { cab_lhs = lhs_incomp } : rest)
-- See Note [Apartness] in GHC.Core.FamInstEnv
- | SurelyApart <- tcUnifyTysFG alwaysBindFun flat lhs_incomp
+ | SurelyApart <- tcUnifyTysFG alwaysBindFam alwaysBindTv flat lhs_incomp
= check_no_conflict flat rest
| otherwise
= Just b
diff --git a/compiler/GHC/Core/Predicate.hs b/compiler/GHC/Core/Predicate.hs
index b354260d23ffef2b015a2cdefb7fdb9e32311099..0eeaca71f51f602182428c193ca4ff666ad445ce 100644
--- a/compiler/GHC/Core/Predicate.hs
+++ b/compiler/GHC/Core/Predicate.hs
@@ -34,7 +34,11 @@ module GHC.Core.Predicate (
-- * Well-scoped free variables
scopedSort, tyCoVarsOfTypeWellScoped,
- tyCoVarsOfTypesWellScoped
+ tyCoVarsOfTypesWellScoped,
+
+ -- Equality left-hand sides
+ CanEqLHS(..), canEqLHS_maybe, canTyFamEqLHS_maybe,
+ canEqLHSKind, canEqLHSType, eqCanEqLHS
) where
@@ -42,7 +46,7 @@ import GHC.Prelude
import GHC.Core.Type
import GHC.Core.Class
-import GHC.Core.TyCo.Compare( eqType )
+import GHC.Core.TyCo.Compare( eqType, tcEqTyConApps )
import GHC.Core.TyCo.FVs( tyCoVarsOfTypeList, tyCoVarsOfTypesList )
import GHC.Core.TyCon
import GHC.Core.TyCon.RecWalk
@@ -58,6 +62,13 @@ import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Data.FastString
+
+{- *********************************************************************
+* *
+* Pred and PredType *
+* *
+********************************************************************* -}
+
-- | A predicate in the solver. The solver tries to prove Wanted predicates
-- from Given ones.
data Pred
@@ -235,9 +246,12 @@ predTypeEqRel ty
| isReprEqPred ty = ReprEq
| otherwise = NomEq
-{-------------------------------------------
-Predicates on PredType
---------------------------------------------}
+
+{- *********************************************************************
+* *
+* Predicates on PredType *
+* *
+********************************************************************* -}
{-
Note [Evidence for quantified constraints]
@@ -616,3 +630,60 @@ tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList
tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList
+
+{- *********************************************************************
+* *
+* Equality left-hand sides
+* *
+********************************************************************* -}
+
+-- | A 'CanEqLHS' is a type that can appear on the left of a canonical
+-- equality: a type variable or /exactly-saturated/ type family application.
+data CanEqLHS
+ = TyVarLHS TyVar
+ | TyFamLHS TyCon -- ^ TyCon of the family
+ [Type] -- ^ Arguments, /exactly saturating/ the family
+
+instance Outputable CanEqLHS where
+ ppr (TyVarLHS tv) = ppr tv
+ ppr (TyFamLHS fam_tc fam_args) = ppr (mkTyConApp fam_tc fam_args)
+
+-----------------------------------
+-- | Is a type a canonical LHS? That is, is it a tyvar or an exactly-saturated
+-- type family application?
+-- Does not look through type synonyms.
+canEqLHS_maybe :: Type -> Maybe CanEqLHS
+canEqLHS_maybe xi
+ | Just tv <- getTyVar_maybe xi
+ = Just $ TyVarLHS tv
+
+ | otherwise
+ = canTyFamEqLHS_maybe xi
+
+canTyFamEqLHS_maybe :: Type -> Maybe CanEqLHS
+canTyFamEqLHS_maybe xi
+ | Just (tc, args) <- tcSplitTyConApp_maybe xi
+ , isTypeFamilyTyCon tc
+ , args `lengthIs` tyConArity tc
+ = Just $ TyFamLHS tc args
+
+ | otherwise
+ = Nothing
+
+-- | Convert a 'CanEqLHS' back into a 'Type'
+canEqLHSType :: CanEqLHS -> Type
+canEqLHSType (TyVarLHS tv) = mkTyVarTy tv
+canEqLHSType (TyFamLHS fam_tc fam_args) = mkTyConApp fam_tc fam_args
+
+-- | Retrieve the kind of a 'CanEqLHS'
+canEqLHSKind :: CanEqLHS -> Kind
+canEqLHSKind (TyVarLHS tv) = tyVarKind tv
+canEqLHSKind (TyFamLHS fam_tc fam_args) = piResultTys (tyConKind fam_tc) fam_args
+
+-- | Are two 'CanEqLHS's equal?
+eqCanEqLHS :: CanEqLHS -> CanEqLHS -> Bool
+eqCanEqLHS (TyVarLHS tv1) (TyVarLHS tv2) = tv1 == tv2
+eqCanEqLHS (TyFamLHS fam_tc1 fam_args1) (TyFamLHS fam_tc2 fam_args2)
+ = tcEqTyConApps fam_tc1 fam_args1 fam_tc2 fam_args2
+eqCanEqLHS _ _ = False
+
diff --git a/compiler/GHC/Core/TyCo/Compare.hs b/compiler/GHC/Core/TyCo/Compare.hs
index 5d1440e1c764d879aae2291ce743b9b991f122cb..fbe3782d048e0e0c260a8f1b66df0ef356b7be25 100644
--- a/compiler/GHC/Core/TyCo/Compare.hs
+++ b/compiler/GHC/Core/TyCo/Compare.hs
@@ -12,7 +12,7 @@ module GHC.Core.TyCo.Compare (
eqVarBndrs,
pickyEqType, tcEqType, tcEqKind, tcEqTypeNoKindCheck,
- tcEqTyConApps,
+ tcEqTyConApps, tcEqTyConAppArgs,
mayLookIdentical,
-- * Type comparison
@@ -226,13 +226,15 @@ tcEqTypeNoKindCheck = eqTypeNoKindCheck
-- are different, just checks the common prefix of arguments.
tcEqTyConApps :: TyCon -> [Type] -> TyCon -> [Type] -> Bool
tcEqTyConApps tc1 args1 tc2 args2
- = tc1 == tc2 &&
- and (zipWith tcEqTypeNoKindCheck args1 args2)
+ = tc1 == tc2 && tcEqTyConAppArgs args1 args2
+
+tcEqTyConAppArgs :: [Type] -> [Type] -> Bool
+tcEqTyConAppArgs args1 args2
+ = and (zipWith tcEqTypeNoKindCheck args1 args2)
-- No kind check necessary: if both arguments are well typed, then
-- any difference in the kinds of later arguments would show up
-- as differences in earlier (dependent) arguments
-
-- | Type equality on lists of types, looking through type synonyms
eqTypes :: [Type] -> [Type] -> Bool
eqTypes [] [] = True
diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs
index 58664a5ebfdcb0a0b78045453bac708d5a2a6d0a..4f9865172639a1fdc1944be565d74d92d555316a 100644
--- a/compiler/GHC/Core/Unify.hs
+++ b/compiler/GHC/Core/Unify.hs
@@ -11,18 +11,15 @@ module GHC.Core.Unify (
tcMatchTyX_BM, ruleMatchTyKiX,
-- Side-effect free unification
- tcUnifyTy, tcUnifyTyKi, tcUnifyTys, tcUnifyTyKis,
- tcUnifyTysFG, tcUnifyTyWithTFs,
- BindFun, BindFlag(..), matchBindFun, alwaysBindFun,
+ tcUnifyTy, tcUnifyTys, tcUnifyFunDeps, tcUnifyDebugger,
+ tcUnifyTysFG, tcUnifyTyForInjectivity,
+ BindTvFun, BindFamFun, BindFlag(..),
+ matchBindTv, alwaysBindTv, alwaysBindFam, dontCareBindFam,
UnifyResult, UnifyResultM(..), MaybeApartReason(..),
typesCantMatch, typesAreApart,
-- Matching a type against a lifted type (coercion)
- liftCoMatch,
-
- -- The core flattening algorithm
- flattenTys, flattenTysX,
-
+ liftCoMatch
) where
import GHC.Prelude
@@ -30,56 +27,127 @@ import GHC.Prelude
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.Predicate( scopedSort )
import GHC.Core.TyCon
+import GHC.Core.Predicate( CanEqLHS(..), canEqLHS_maybe )
+import GHC.Core.TyCon.Env
import GHC.Core.TyCo.Rep
-import GHC.Core.TyCo.Compare ( eqType, tcEqType )
+import GHC.Core.TyCo.Compare ( eqType, tcEqType, tcEqTyConAppArgs )
import GHC.Core.TyCo.FVs ( tyCoVarsOfCoList, tyCoFVsOfTypes )
-import GHC.Core.TyCo.Subst ( mkTvSubst, emptyIdSubstEnv )
+import GHC.Core.TyCo.Subst ( mkTvSubst )
import GHC.Core.Map.Type
+import GHC.Core.Multiplicity
+
import GHC.Utils.FV( FV, fvVarList )
import GHC.Utils.Misc
-import GHC.Data.Pair
import GHC.Utils.Outputable
-import GHC.Types.Unique
+import GHC.Types.Basic( SwapFlag(..) )
import GHC.Types.Unique.FM
-import GHC.Types.Unique.Set
import GHC.Exts( oneShot )
import GHC.Utils.Panic
-import GHC.Data.FastString
-import Data.List ( mapAccumL )
+import GHC.Data.Pair
+import GHC.Data.TrieMap
+import GHC.Data.Maybe( orElse )
+
import Control.Monad
import qualified Data.Semigroup as S
import GHC.Builtin.Types.Prim (fUNTyCon)
-import GHC.Core.Multiplicity
-{-
-
-Unification is much tricker than you might think.
+{- Note [The Core unifier]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+This module contains the (pure) unifier two types. It is subtle in a number
+of ways. Here we summarise, but see Note [Specification of unification].
-1. The substitution we generate binds the *template type variables*
- which are given to us explicitly.
+(CU1) It creates a substition only for "bindable" or "template" type variables.
+ These are identified by a `um_bind_tv_fun` function passed down in the `UMEnv`
+ environment.
-2. We want to match in the presence of foralls;
+(CU2) We want to match in the presence of foralls;
e.g (forall a. t1) ~ (forall b. t2)
+ That is what the `um_rn_env :: RnEnv2` field of `UMEnv` is for; it does the
+ alpha-renaming that makes it as if `a` and `b` were the same variable.
+ Initialising the `RnEnv2`, so that it can generate a fresh binder when
+ necessary, entails knowing the free variables of both types.
- That is what the RnEnv2 is for; it does the alpha-renaming
- that makes it as if a and b were the same variable.
- Initialising the RnEnv2, so that it can generate a fresh
- binder when necessary, entails knowing the free variables of
- both types.
-
-3. We must be careful not to bind a template type variable to a
+ Of course, we must be careful not to bind a template type variable to a
locally bound variable. E.g.
(forall a. x) ~ (forall b. b)
- where x is the template type variable. Then we do not want to
- bind x to a/b! This is a kind of occurs check.
- The necessary locals accumulate in the RnEnv2.
+ where `x` is the template type variable. Then we do not want to
+ bind `x` to a/b! See `mentionsForAllBoundTyVarsL/R`.
+
+(CU3) We want to take special care for type families.
+ See the big Note [Apartness and type families]
+
+(CU4) Rather than returning just "unifiable" or "not-unifiable" we do "fine-grained"
+ unification (hence "fg" or "FG" in this module) returning three possiblities,
+ captured in `UnifyResult`:
+ - Unifiable subst : certainly unifiable with this type substitution
+ - SurelyApart : cannot be unifiable, regardless of how type familes reduce
+ - MaybeApart : neither of the above
+ See Note [Unification result].
+
+ Four reasons for MaybeApart (see `MaybeApartReason`). The first two are the
+ big ones!
+ * MARTypeFamily:
+ Family reduction might make the two types equal
+ Maybe (F Int) ~ Maybe Bool
+ See Note [Apartness and type families]
+ * MARInfinite (occurs check):
+ See Note [Infinitary substitutions]
+ * MARTypeVsConstraint:
+ See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim
+ * MARCast (obscure):
+ See (KCU2) in Note [Kind coercions in Unify]
+
+(CU5) We need to take care with kinds. See Note [tcMatchTy vs tcMatchTyKi]
+
+(CU6) The "unifier" can also do /matching/, governed by `um_unif :: AmIUnifying`.
+ When matching, the LHS and RHS namespaces are unrelated. In particular, the
+ bindable type variable can occur (unrelatedly) in the RHS. E.g.
+ match (a,Maybe a) ~ ([a], Maybe [a])
+ We get the substitution [a :-> [a]], without confusing the
+ LHS `a` with the RHS `a`. The substitition is "one-shot", and should not be
+ iterated.
+
+Note [Infinitary substitutions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Do the types (x, x) and ([y], y) unify? The answer is seemingly "no" --
+no substitution to finite types makes these match. This is the famous
+"occurs check".
+
+But, a substitution to *infinite* types can unify these two types:
+ [x |-> [[...]]], y |-> [[[...]]] ].
+
+Why do we care? Consider these two type family instances:
+
+ type instance F x x = Int
+ type instance F [y] y = Bool
+
+If we also have
+
+ type instance Looper = [Looper]
+
+then the instances potentially overlap -- they are not "apart". So we must
+distinguish failure-to-unify from definitely-apart. The solution is to use
+unification over infinite terms. This is possible (see [1] for lots of gory
+details), but a full algorithm is a little more powerful than we need. Instead,
+we make a conservative approximation and just omit the occurs check.
+
+ [1]: http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
+
+tcUnifyTys considers an occurs-check problem as the same as general unification
+failure.
+
+See also #8162.
+
+It's worth noting that unification in the presence of infinite types is not
+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 [tcMatchTy vs tcMatchTyKi]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -108,17 +176,324 @@ How do you choose between them?
3. Otherwise, if you're sure that the variable kinds do not mention
type families and you're not already sure that the kind of the template
equals the kind of the target, then use the TyKi version.
+
+Note [Unification result]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See `UnifyResult` and `UnifyResultM`. 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.
+* SurelyApart, if there is no substitution s such that s(t1) = s(t2),
+ where "=" includes type-family reductions.
+* MaybeApart mar s, when we aren't sure. `mar` is a MaybeApartReason.
+
+Examples
+* [a] ~ Maybe b: SurelyApart, because [] and Maybe can't unify
+
+* [(a,Int)] ~ [(Bool,b)]: Unifiable
+
+* [F Int] ~ [Bool]: MaybeApart MARTypeFamily, because F Int might reduce to Bool
+ (the unifier does not try this)
+
+* a ~ Maybe a: MaybeApart MARInfinite. Not Unifiable clearly, but not SurelyApart
+ either; consider
+ a := Loop
+ where type family Loop where Loop = Maybe Loop
+
+Wrinkle (UR1): see `combineMAR`
+ There is the possibility that two types are MaybeApart for *both* reasons:
+
+ * (a, F Int) ~ (Maybe a, Bool)
+
+ What reason should we use? The *only* consumer of the reason is described
+ in Note [Infinitary substitution in lookup] in GHC.Core.InstEnv. The goal
+ there is identify which instances might match a target later (but don't
+ match now) -- except that we want to ignore the possibility of infinitary
+ substitutions. So let's examine a concrete scenario:
+
+ class C a b c
+ instance C a (Maybe a) Bool
+ -- other instances, including one that will actually match
+ [W] C b b (F Int)
+
+ Do we want the instance as a future possibility? No. The only way that
+ instance can match is in the presence of an infinite type (infinitely nested
+ Maybes). We thus say that `MARInfinite` takes precedence, so that InstEnv treats
+ this case as an infinitary substitution case; the fact that a type family is
+ involved is only incidental. We thus define `combineMAR` to prefer
+ `MARInfinite`.
+
+Note [Apartness and type families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this:
+
+ type family F a b where
+ F Int Bool = Char
+ F a b = Double
+ type family G a -- open, no instances
+
+How do we reduce (F (G Float) (G Float))? The first equation clearly doesn't
+match immediately while the second equation does. But, before reducing, we must
+make sure that the target can never become (F Int Bool). Well, no matter what G
+Float becomes, it certainly won't become *both* Int and Bool, so indeed we're
+safe reducing (F (G Float) (G Float)) to Double.
+
+So we must say that the argument list
+ (G Float) (G Float) is SurelyApart from Int Bool
+
+This is necessary not only to get more reductions (which we might be willing to
+give up on), but for /substitutivity/. If we have (F x x), we can see that (F x x)
+can reduce to Double. So, it had better be the case that (F blah blah) can
+reduce to Double, no matter what (blah) is!
+
+To achieve this, `go_fam` in `uVarOrFam` does this;
+
+* When we attempt to unify (G Float) ~ Int, we return MaybeApart..
+ but we /also/ extend a "family substitution" [G Float :-> Int],
+ in `um_fam_env`, alongside the regular [tyvar :-> type] substitution in
+ `um_tv_env`. See the `BindMe` case of `go_fam` in `uVarOrFam`.
+
+* When we later encounter (G Float) ~ Bool, we apply the family substitution,
+ very much as we apply the conventional [tyvar :-> type] substitution
+ when we encounter a type variable. See the `lookupFamEnv` in `go_fam` in
+ `uVarOrFam`.
+
+ So (G Float ~ Bool) becomes (Int ~ Bool) which is SurelyApart. Bingo.
+
+
+Wrinkles
+
+(ATF0) Once we encounter a type-family application, we only ever return
+ MaybeApart or SurelyApart
+ but never `Unifiable`. Accordingly, we only return a TyCoVar substitution
+ from `tcUnifyTys` and friends; we don't return a type-family substitution as
+ well. (We could imagine doing so, though.)
+
+(ATF1) Exactly the same mechanism is used in class-instance checking.
+ If we have
+ instance C (Maybe b)
+ instance {-# OVERLAPPING #-} C (Maybe Bool)
+ [W] C (Maybe (F a))
+ we want to know that the second instance might match later, when we know more about `a`.
+ The function `GHC.Core.InstEnv.instEnvMatchesAndUnifiers` uses `tcUnifyTysFG` to
+ account for type families in the type being matched.
+
+(ATF2) A very similar check is made in `GHC.Tc.Utils.Unify.mightEqualLater`, which
+ again uses `tcUnifyTysFG` to account for the possibility of type families. See
+ Note [What might equal later?] in GHC.Tc.Utils.Unify, esp example (10).
+
+(ATF3) What about foralls? For example, supppose we are unifying
+ (forall a. F a) -> (forall a. F a)
+ Those two (F a) types are unrelated, bound by different foralls.
+
+ So to keep things simple, the entire family-substitution machinery is used
+ only if there are no enclosing foralls (see the (um_foralls env)) check in
+ `uSatFamApp`). That's fine, because the apartness business is used only for
+ reducing type-family applications, and class instances, and their arguments
+ can't have foralls anyway.
+
+ The bottom line is that we won't discover that
+ (forall a. (a, F Int, F Int))
+ is surely apart from
+ (forall a. (a, Int, Bool))
+ but that doesn't matter. Fixing this would be possible, but would require
+ quite a bit of head-scratching.
+
+(ATF4) The family substitution only has /saturated/ family applications in
+ its domain. Consider the following concrete example from #16995:
+
+ type family Param :: Type -> Type -- arity 0
+
+ type family LookupParam (a :: Type) :: Type where
+ LookupParam (f Char) = Bool
+ LookupParam x = Int
+
+ foo :: LookupParam (Param ())
+ foo = 42
+
+ In order for `foo` to typecheck, `LookupParam (Param ())` must reduce to
+ `Int`. So (f Char) ~ (Param ()) must be SurelyApart. Remember, since
+ `Param` is a nullary type family, it is over-saturated in (Param ()).
+ This unification will only be SurelyApart if we decompose the outer AppTy
+ separately, to then give (() ~ Char).
+
+ Not only does this allow more programs to be accepted, it's also important
+ for correctness. Not doing this was the root cause of the Core Lint error
+ in #16995.
+
+(ATF5) Consider
+ instance (Generic1 f, Ord (Rep1 f a))
+ => Ord (Generically1 f a) where ...
+ -- The "..." gives rise to [W] Ord (Generically1 f a)
+ We must use the instance decl (recursively) to simplify the [W] constraint;
+ we do /not/ want to worry that the `[G] Ord (Rep1 f a)` might be an
+ alternative path. So `noMatchableGivenDicts` must return False;
+ so `mightMatchLater` must return False; so when um_bind_fam_fun returns
+ `DontBindMe`, the unifier must return `SurelyApart`, not `MaybeApart`. See
+ `go_fam` in `uVarOrFam`
+
+(ATF6) You might think that when /matching/ the um_fam_env will always be empty,
+ because type-class-instance and type-family-instance heads can't include type
+ families. E.g. instance C (F a) where ... -- Illegal
+
+ But you'd be wrong: when "improving" type family constraint we may have a
+ type family on the LHS of a match. Consider
+ type family G6 a = r | r -> a
+ type instance G6 [a] = [G a]
+ type instance G6 Bool = Int
+ and the Wanted constraint [W] G6 alpha ~ [Int]. We /match/ each type instance
+ RHS against [Int]! So we try
+ [G a] ~ [Int]
+ and we want to succeed with MaybeApart, so that we can generate the improvement
+ constraint [W] alpha ~ [beta] where beta is fresh.
+ See Section 5.2 of "Injective type families for Haskell".
+
+ A second place that we match with type-fams on the LHS is in `checkValidClass`.
+ In `check_dm` we check that the default method has the right type, using matching,
+ both ways. And that type may have type-family applications in it. Example in
+ test CoOpt_Singletons.
+
+(ATF7) You might think that (ATF6) is a very special case, and in /other/ uses of
+ matching, where we enter via `tc_match_tys_x` we will never see a type-family
+ in the template. But actually we do see that case in the specialiser: see
+ the call to `tcMatchTy` in `GHC.Core.Opt.Specialise.beats_or_same`
+
+ Also: a user-written RULE could conceivably have a type-family application
+ in the template. It might not be a good rule, but I don't think we currently
+ check for this.
+
+(ATF8) The treatment of type families is governed by
+ um_bind_fam_fun :: BindFamFun
+ in UMEnv, where
+ type BindFamFun = TyCon -> [Type] -> Type -> BindFlag
+ There are some simple BindFamFun functions provided:
+ alwaysBindFam do the clever stuff above
+ neverBindFam treat type families as SurelyApart
+ dontCareBindFam type families shouldn't exist at all
+ This function only affects the difference between the results MaybeApart and
+ SurelyApart; it never does not affect whether or not we return Unifiable.
+
+(ATF9) Decomposition. Consider unifying
+ F a ~ F Int
+ There is a unifying substitition [a :-> Int], and we want to find it, returning
+ Unifiable. (Remember, this is the Core unifier -- we are not doing type inference.)
+ So we should decompose to get (a ~ Int)
+
+ But consider unifying
+ F Int ~ F Bool
+ Although Int and Bool are SurelyApart, we must return MaybeApart for the outer
+ unification. Hence the use of `don'tBeSoSure` in `go_fam_fam`; it leaves Unifiable
+ alone, but weakens `SurelyApart` to `MaybeApart`.
+
+(ATF10) Injectivity. Consider (AFT9) where F is known to be injective. Then if we
+ are unifying
+ F Int ~ F Bool
+ we /can/ say SurelyApart. See the inj/noninj stuff in `go_fam_fam`.
+
+(ATF11) Consider unifying
+ [F Int, F Int, F Bool] ~ [F Bool, Char, Double]
+ We find (F Int ~ F Bool), so we can decompose. But we /also/ want to remember
+ the substitution [F Int :-> F Bool]. Then from (F Int ~ Char) we get the
+ substitution [F Bool :-> Char]. And that flat-out contradicts (F Bool ~ Double)
+ so we should get SurelyApart.
+
+ Key point: when decomposing (F tys1 ~ F tys2), we should /also/ extend the
+ type-family substitution.
+
+(ATF12) There is a horrid exception for the injectivity check. See (UR1) in
+ in Note [Specification of unification].
+
+SIDE NOTE. The paper "Closed type families with overlapping equations"
+http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
+tries to achieve the same effect with a standard yes/no unifier, by "flattening"
+the types (replacing each type-family application with a fresh type variable)
+and then unifying. But that does not work well. Consider (#25657)
+
+ type MyEq :: k -> k -> Bool
+ type family MyEq a b where
+ MyEq a a = 'True
+ MyEq _ _ = 'False
+
+ type Var :: forall {k}. Tag -> k
+ type family Var tag = a | a -> tag
+
+Then, because Var is injective, we want
+ MyEq (Var A) (Var B) --> False
+ MyEq (Var A) (Var A) --> True
+
+But if we flattten the types (Var A) and (Var B) we'll just get fresh type variables,
+and all is lost. But with the current algorithm we have that
+ a a ~ (Var A) (Var B)
+is SurelyApart, so the first equation definitely doesn't match and we can try the
+second, which does. END OF SIDE NOTE.
-}
--- | Some unification functions are parameterised by a 'BindFun', which
+{- *********************************************************************
+* *
+ Binding decisions
+* *
+********************************************************************* -}
+
+data BindFlag
+ = BindMe -- ^ A bindable type variable
+
+ | DontBindMe -- ^ Do not bind this type variable is /apart/
+ -- See also Note [Super skolems: binding when looking up instances]
+ -- in GHC.Core.InstEnv.
+ deriving Eq
+
+-- | Some unification functions are parameterised by a 'BindTvFun', which
-- says whether or not to allow a certain unification to take place.
--- A 'BindFun' takes the 'TyVar' involved along with the 'Type' it will
+-- A 'BindTvFun' takes the 'TyVar' involved along with the 'Type' it will
-- potentially be bound to.
--
-- It is possible for the variable to actually be a coercion variable
-- (Note [Matching coercion variables]), but only when one-way matching.
-- In this case, the 'Type' will be a 'CoercionTy'.
-type BindFun = TyCoVar -> Type -> BindFlag
+type BindTvFun = TyCoVar -> Type -> BindFlag
+
+-- | BindFamFun is similiar to BindTvFun, but deals with a saturated
+-- type-family application. See Note [Apartness and type families].
+type BindFamFun = TyCon -> [Type] -> Type -> BindFlag
+
+-- | Allow binding only for any variable in the set. Variables may
+-- be bound to any type.
+-- Used when doing simple matching; e.g. can we find a substitution
+--
+-- @
+-- S = [a :-> t1, b :-> t2] such that
+-- S( Maybe (a, b->Int ) = Maybe (Bool, Char -> Int)
+-- @
+matchBindTv :: TyCoVarSet -> BindTvFun
+matchBindTv tvs tv _ty
+ | tv `elemVarSet` tvs = BindMe
+ | otherwise = DontBindMe
+
+-- | Allow the binding of any variable to any type
+alwaysBindTv :: BindTvFun
+alwaysBindTv _tv _ty = BindMe
+
+-- | Allow the binding of a type-family application to any type
+alwaysBindFam :: BindFamFun
+-- See (ATF8) in Note [Apartness and type families]
+alwaysBindFam _tc _args _rhs = BindMe
+
+dontCareBindFam :: HasCallStack => BindFamFun
+-- See (ATF8) in Note [Apartness and type families]
+dontCareBindFam tc args rhs
+ = pprPanic "dontCareBindFam" $
+ vcat [ ppr tc <+> ppr args, text "rhs" <+> ppr rhs ]
+
+-- | Don't allow the binding of a type-family application at all
+neverBindFam :: BindFamFun
+-- See (ATF8) in Note [Apartness and type families]
+neverBindFam _tc _args _rhs = DontBindMe
+
+
+{- *********************************************************************
+* *
+ Various wrappers for matching
+* *
+********************************************************************* -}
-- | @tcMatchTy t1 t2@ produces a substitution (over fvs(t1))
-- @s@ such that @s(t1)@ equals @t2@.
@@ -132,67 +507,76 @@ type BindFun = TyCoVar -> Type -> BindFlag
-- always used on top-level types, so we can bind any of the
-- free variables of the LHS.
-- See also Note [tcMatchTy vs tcMatchTyKi]
-tcMatchTy :: Type -> Type -> Maybe Subst
+tcMatchTy :: HasDebugCallStack => Type -> Type -> Maybe Subst
tcMatchTy ty1 ty2 = tcMatchTys [ty1] [ty2]
-tcMatchTyX_BM :: BindFun -> Subst
+tcMatchTyX_BM :: HasDebugCallStack
+ => BindTvFun -> Subst
-> Type -> Type -> Maybe Subst
-tcMatchTyX_BM bind_me subst ty1 ty2
- = tc_match_tys_x bind_me False subst [ty1] [ty2]
+tcMatchTyX_BM bind_tv subst ty1 ty2
+ = tc_match_tys_x bind_tv False subst [ty1] [ty2]
-- | Like 'tcMatchTy', but allows the kinds of the types to differ,
-- and thus matches them as well.
-- See also Note [tcMatchTy vs tcMatchTyKi]
-tcMatchTyKi :: Type -> Type -> Maybe Subst
+tcMatchTyKi :: HasDebugCallStack => Type -> Type -> Maybe Subst
tcMatchTyKi ty1 ty2
- = tc_match_tys alwaysBindFun True [ty1] [ty2]
+ = tc_match_tys alwaysBindTv True [ty1] [ty2]
-- | This is similar to 'tcMatchTy', but extends a substitution
-- See also Note [tcMatchTy vs tcMatchTyKi]
-tcMatchTyX :: Subst -- ^ Substitution to extend
+tcMatchTyX :: HasDebugCallStack
+ => Subst -- ^ Substitution to extend
-> Type -- ^ Template
-> Type -- ^ Target
-> Maybe Subst
tcMatchTyX subst ty1 ty2
- = tc_match_tys_x alwaysBindFun False subst [ty1] [ty2]
+ = tc_match_tys_x alwaysBindTv False subst [ty1] [ty2]
-- | Like 'tcMatchTy' but over a list of types.
-- See also Note [tcMatchTy vs tcMatchTyKi]
-tcMatchTys :: [Type] -- ^ Template
+tcMatchTys :: HasDebugCallStack
+ => [Type] -- ^ Template
-> [Type] -- ^ Target
-> Maybe Subst -- ^ One-shot; in principle the template
-- variables could be free in the target
+ -- See (CU6) in Note [The Core unifier]
tcMatchTys tys1 tys2
- = tc_match_tys alwaysBindFun False tys1 tys2
+ = tc_match_tys alwaysBindTv False tys1 tys2
-- | Like 'tcMatchTyKi' but over a list of types.
-- See also Note [tcMatchTy vs tcMatchTyKi]
-tcMatchTyKis :: [Type] -- ^ Template
+tcMatchTyKis :: HasDebugCallStack
+ => [Type] -- ^ Template
-> [Type] -- ^ Target
- -> Maybe Subst -- ^ One-shot substitution
+ -> Maybe Subst -- ^ One-shot substitution
+ -- See (CU6) in Note [The Core unifier]
tcMatchTyKis tys1 tys2
- = tc_match_tys alwaysBindFun True tys1 tys2
+ = tc_match_tys alwaysBindTv True tys1 tys2
-- | Like 'tcMatchTys', but extending a substitution
-- See also Note [tcMatchTy vs tcMatchTyKi]
-tcMatchTysX :: Subst -- ^ Substitution to extend
+tcMatchTysX :: HasDebugCallStack
+ => Subst -- ^ Substitution to extend
-> [Type] -- ^ Template
-> [Type] -- ^ Target
- -> Maybe Subst -- ^ One-shot substitution
+ -> Maybe Subst -- ^ One-shot substitution
tcMatchTysX subst tys1 tys2
- = tc_match_tys_x alwaysBindFun False subst tys1 tys2
+ = tc_match_tys_x alwaysBindTv False subst tys1 tys2
-- | Like 'tcMatchTyKis', but extending a substitution
-- See also Note [tcMatchTy vs tcMatchTyKi]
-tcMatchTyKisX :: Subst -- ^ Substitution to extend
- -> [Type] -- ^ Template
- -> [Type] -- ^ Target
+tcMatchTyKisX :: HasDebugCallStack
+ => Subst -- ^ Substitution to extend
+ -> [Type] -- ^ Template
+ -> [Type] -- ^ Target
-> Maybe Subst -- ^ One-shot substitution
tcMatchTyKisX subst tys1 tys2
- = tc_match_tys_x alwaysBindFun True subst tys1 tys2
+ = tc_match_tys_x alwaysBindTv True subst tys1 tys2
-- | Same as tc_match_tys_x, but starts with an empty substitution
-tc_match_tys :: BindFun
+tc_match_tys :: HasDebugCallStack
+ => BindTvFun
-> Bool -- ^ match kinds?
-> [Type]
-> [Type]
@@ -203,14 +587,16 @@ tc_match_tys bind_me match_kis tys1 tys2
in_scope = mkInScopeSet (tyCoVarsOfTypes tys1 `unionVarSet` tyCoVarsOfTypes tys2)
-- | Worker for 'tcMatchTysX' and 'tcMatchTyKisX'
-tc_match_tys_x :: BindFun
+tc_match_tys_x :: HasDebugCallStack
+ => BindTvFun
-> Bool -- ^ match kinds?
-> Subst
-> [Type]
-> [Type]
-> Maybe Subst
-tc_match_tys_x bind_me match_kis (Subst in_scope id_env tv_env cv_env) tys1 tys2
- = case tc_unify_tys bind_me
+tc_match_tys_x bind_tv match_kis (Subst in_scope id_env tv_env cv_env) tys1 tys2
+ = case tc_unify_tys alwaysBindFam -- (ATF7) in Note [Apartness and type families]
+ bind_tv
False -- Matching, not unifying
False -- Not an injectivity check
match_kis
@@ -231,31 +617,21 @@ ruleMatchTyKiX
-> Maybe TvSubstEnv
ruleMatchTyKiX tmpl_tvs rn_env tenv tmpl target
-- See Note [Kind coercions in Unify]
- = case tc_unify_tys (matchBindFun tmpl_tvs) False False
- True -- <-- this means to match the kinds
+ = case tc_unify_tys neverBindFam (matchBindTv tmpl_tvs)
+ -- neverBindFam: a type family probably shouldn't appear
+ -- on the LHS of a RULE, although we don't currently prevent it.
+ -- But even if it did, (ATF8) in Note [Apartness and type families]
+ -- says it doesn't matter becuase here we only care about Unifiable.
+ -- So neverBindFam is efficient, and sufficient.
+ False -- Matching, not unifying
+ False -- No doing an injectivity check
+ True -- Match the kinds
IgnoreMultiplicities
-- See Note [Rewrite rules ignore multiplicities in FunTy]
rn_env tenv emptyCvSubstEnv [tmpl] [target] of
Unifiable (tenv', _) -> Just tenv'
_ -> Nothing
--- | Allow binding only for any variable in the set. Variables may
--- be bound to any type.
--- Used when doing simple matching; e.g. can we find a substitution
---
--- @
--- S = [a :-> t1, b :-> t2] such that
--- S( Maybe (a, b->Int ) = Maybe (Bool, Char -> Int)
--- @
-matchBindFun :: TyCoVarSet -> BindFun
-matchBindFun tvs tv _ty
- | tv `elemVarSet` tvs = BindMe
- | otherwise = Apart
-
--- | Allow the binding of any variable to any type
-alwaysBindFun :: BindFun
-alwaysBindFun _tv _ty = BindMe
-
{-
************************************************************************
* *
@@ -300,108 +676,172 @@ typesCantMatch :: [(Type,Type)] -> Bool
typesCantMatch prs = any (uncurry typesAreApart) prs
typesAreApart :: Type -> Type -> Bool
-typesAreApart t1 t2 = case tcUnifyTysFG alwaysBindFun [t1] [t2] of
+typesAreApart t1 t2 = case tcUnifyTysFG alwaysBindFam alwaysBindTv [t1] [t2] of
SurelyApart -> True
_ -> False
{-
************************************************************************
* *
- Unification
+ Various wrappers for unification
* *
-************************************************************************
-
-Note [Fine-grained unification]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Do the types (x, x) and ([y], y) unify? The answer is seemingly "no" --
-no substitution to finite types makes these match. But, a substitution to
-*infinite* types can unify these two types: [x |-> [[[...]]], y |-> [[[...]]] ].
-Why do we care? Consider these two type family instances:
-
-type instance F x x = Int
-type instance F [y] y = Bool
-
-If we also have
-
-type instance Looper = [Looper]
-
-then the instances potentially overlap. The solution is to use unification
-over infinite terms. This is possible (see [1] for lots of gory details), but
-a full algorithm is a little more power than we need. Instead, we make a
-conservative approximation and just omit the occurs check.
+********************************************************************* -}
-[1]: http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
-
-tcUnifyTys considers an occurs-check problem as the same as general unification
-failure.
-
-tcUnifyTysFG ("fine-grained") returns one of three results: success, occurs-check
-failure ("MaybeApart"), or general failure ("SurelyApart").
-
-See also #8162.
-
-It's worth noting that unification in the presence of infinite types is not
-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.
+-- | Simple unification of two types; all type variables are bindable
+-- Precondition: the kinds are already equal
+tcUnifyTy :: Type -> Type -- All tyvars are bindable
+ -> Maybe Subst
+ -- A regular one-shot (idempotent) substitution
+tcUnifyTy t1 t2 = tcUnifyTys alwaysBindTv [t1] [t2]
+
+tcUnifyDebugger :: Type -> Type -> Maybe Subst
+tcUnifyDebugger t1 t2
+ = case tc_unify_tys_fg
+ True -- Unify kinds
+ neverBindFam -- Does not affect Unifiable, so pick max efficient
+ -- See (ATF8) in Note [Apartness and type families]
+ alwaysBindTv
+ [t1] [t2] of
+ Unifiable subst -> Just subst
+ _ -> Nothing
-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.
-* SurelyApart, if there is no substitution s such that s(t1) = s(t2),
- where "=" includes type-family reductions.
-* MaybeApart mar s, when we aren't sure. `mar` is a MaybeApartReason.
+-- | Like 'tcUnifyTys' but also unifies the kinds
+tcUnifyFunDeps :: TyCoVarSet
+ -> [Type] -> [Type]
+ -> Maybe Subst
+tcUnifyFunDeps qtvs tys1 tys2
+ = case tc_unify_tys_fg
+ True -- Unify kinds
+ dontCareBindFam -- Class-instance heads never mention type families
+ (matchBindTv qtvs)
+ tys1 tys2 of
+ Unifiable subst -> Just subst
+ _ -> Nothing
+
+-- | Unify or match a type-family RHS with a type (possibly another type-family RHS)
+-- Precondition: kinds are the same
+tcUnifyTyForInjectivity
+ :: AmIUnifying -- ^ True <=> do two-way unification;
+ -- False <=> do one-way matching.
+ -- See end of sec 5.2 from the paper
+ -> InScopeSet -- Should include the free tyvars of both Type args
+ -> Type -> Type -- Types to unify
+ -> Maybe Subst
+-- This algorithm is an implementation of the "Algorithm U" presented in
+-- the paper "Injective type families for Haskell", Figures 2 and 3.
+-- The code is incorporated with the standard unifier for convenience, but
+-- its operation should match the specification in the paper.
+tcUnifyTyForInjectivity unif in_scope t1 t2
+ = case tc_unify_tys alwaysBindFam alwaysBindTv
+ unif -- Am I unifying?
+ True -- Do injectivity checks
+ False -- Don't check outermost kinds
+ RespectMultiplicities
+ rn_env emptyTvSubstEnv emptyCvSubstEnv
+ [t1] [t2] of
+ Unifiable (tv_subst, _cv_subst) -> Just $ maybe_fix tv_subst
+ MaybeApart _reason (tv_subst, _cv_subst) -> Just $ maybe_fix tv_subst
+ -- We want to *succeed* in questionable cases.
+ -- This is a pre-unification algorithm.
+ SurelyApart -> Nothing
+ where
+ rn_env = mkRnEnv2 in_scope
-Examples
-* [a] ~ Maybe b: SurelyApart, because [] and Maybe can't unify
-* [(a,Int)] ~ [(Bool,b)]: Unifiable
-* [F Int] ~ [Bool]: MaybeApart MARTypeFamily, because F Int might reduce to Bool (the unifier
- does not try this)
-* a ~ Maybe a: MaybeApart MARInfinite. Not Unifiable clearly, but not SurelyApart either; consider
- a := Loop
- where type family Loop where Loop = Maybe Loop
+ maybe_fix | unif = niFixSubst in_scope
+ | otherwise = mkTvSubst in_scope -- when matching, don't confuse
+ -- domain with range
-There is the possibility that two types are MaybeApart for *both* reasons:
+-----------------
+tcUnifyTys :: BindTvFun
+ -> [Type] -> [Type]
+ -> Maybe Subst
+ -- ^ A regular one-shot (idempotent) substitution
+ -- that unifies the erased types. See comments
+ -- for 'tcUnifyTysFG'
-* (a, F Int) ~ (Maybe a, Bool)
+-- The two types may have common type variables, and indeed do so in the
+-- second call to tcUnifyTys in GHC.Tc.Instance.FunDeps.checkClsFD
+tcUnifyTys bind_fn tys1 tys2
+ = case tcUnifyTysFG neverBindFam bind_fn tys1 tys2 of
+ Unifiable result -> Just result
+ _ -> Nothing
-What reason should we use? The *only* consumer of the reason is described
-in Note [Infinitary substitution in lookup] in GHC.Core.InstEnv. The goal
-there is identify which instances might match a target later (but don't
-match now) -- except that we want to ignore the possibility of infinitary
-substitutions. So let's examine a concrete scenario:
+-- | (tcUnifyTysFG bind_fam bind_tv tys1 tys2) does "fine-grain" unification
+-- of tys1 and tys2, under the control of `bind_fam` and `bind_tv`.
+-- This version requires that the kinds of the types are the same,
+-- if you unify left-to-right.
+-- See Note [The Core unifier]
+tcUnifyTysFG :: BindFamFun -> BindTvFun
+ -> [Type] -> [Type]
+ -> UnifyResult
+tcUnifyTysFG bind_fam bind_tv tys1 tys2
+ = tc_unify_tys_fg False bind_fam bind_tv tys1 tys2
- class C a b c
- instance C a (Maybe a) Bool
- -- other instances, including one that will actually match
- [W] C b b (F Int)
+tc_unify_tys_fg :: Bool
+ -> BindFamFun -> BindTvFun
+ -> [Type] -> [Type]
+ -> UnifyResult
+tc_unify_tys_fg match_kis bind_fam bind_tv tys1 tys2
+ = do { (tv_env, _) <- tc_unify_tys bind_fam bind_tv
+ True -- Unifying
+ False -- Not doing an injectivity check
+ match_kis -- Match outer kinds
+ RespectMultiplicities rn_env
+ emptyTvSubstEnv emptyCvSubstEnv
+ tys1 tys2
+ ; return $ niFixSubst in_scope tv_env }
+ where
+ in_scope = mkInScopeSet $ tyCoVarsOfTypes tys1 `unionVarSet` tyCoVarsOfTypes tys2
+ rn_env = mkRnEnv2 in_scope
-Do we want the instance as a future possibility? No. The only way that
-instance can match is in the presence of an infinite type (infinitely
-nested Maybes). We thus say that MARInfinite takes precedence, so that
-InstEnv treats this case as an infinitary substitution case; the fact
-that a type family is involved is only incidental. We thus define
-the Semigroup instance for MaybeApartReason to prefer MARInfinite.
+-- | This function is actually the one to call the unifier -- a little
+-- too general for outside clients, though.
+tc_unify_tys :: BindFamFun -> BindTvFun
+ -> AmIUnifying -- ^ True <=> unify; False <=> match
+ -> Bool -- ^ True <=> doing an injectivity check
+ -> Bool -- ^ True <=> treat the kinds as well
+ -> MultiplicityFlag -- ^ see Note [Rewrite rules ignore multiplicities in FunTy] in GHC.Core.Unify
+ -> RnEnv2
+ -> TvSubstEnv -- ^ substitution to extend
+ -> CvSubstEnv
+ -> [Type] -> [Type]
+ -> UnifyResultM (TvSubstEnv, CvSubstEnv)
+-- NB: It's tempting to ASSERT here that, if we're not matching kinds, then
+-- the kinds of the types should be the same. However, this doesn't work,
+-- as the types may be a dependent telescope, where later types have kinds
+-- that mention variables occurring earlier in the list of types. Here's an
+-- example (from typecheck/should_fail/T12709):
+-- template: [rep :: RuntimeRep, a :: TYPE rep]
+-- target: [LiftedRep :: RuntimeRep, Int :: TYPE LiftedRep]
+-- We can see that matching the first pair will make the kinds of the second
+-- pair equal. Yet, we still don't need a separate pass to unify the kinds
+-- of these types, so it's appropriate to use the Ty variant of unification.
+-- See also Note [tcMatchTy vs tcMatchTyKi].
+tc_unify_tys bind_fam bind_tv unif inj_check match_kis match_mults rn_env tv_env cv_env tys1 tys2
+ = initUM tv_env cv_env $
+ do { when match_kis $
+ unify_tys env kis1 kis2
+ ; unify_tys env tys1 tys2 }
+ where
+ env = UMEnv { um_bind_tv_fun = bind_tv
+ , um_bind_fam_fun = bind_fam
+ , um_foralls = emptyVarSet
+ , um_unif = unif
+ , um_inj_tf = inj_check
+ , um_arr_mult = match_mults
+ , um_rn_env = rn_env }
-Note [The substitution in MaybeApart]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The constructor MaybeApart carries data with it, typically a TvSubstEnv. Why?
-Because consider unifying these:
+ kis1 = map typeKind tys1
+ kis2 = map typeKind tys2
-(a, a, Int) ~ (b, [b], Bool)
-If we go left-to-right, we start with [a |-> b]. Then, on the middle terms, we
-apply the subst we have so far and discover that we need [b |-> [b]]. Because
-this fails the occurs check, we say that the types are MaybeApart (see above
-Note [Fine-grained unification]). But, we can't stop there! Because if we
-continue, we discover that Int is SurelyApart from Bool, and therefore the
-types are apart. This has practical consequences for the ability for closed
-type family applications to reduce. See test case
-indexed-types/should_compile/Overlap14.
+{- *********************************************************************
+* *
+ UnifyResult, MaybeApart etc
+* *
+********************************************************************* -}
-Note [Rewrite rules ignore multiplicities in FunTy]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Rewrite rules ignore multiplicities in FunTy]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following (higher-order) rule:
m :: Bool -> Bool -> Bool
@@ -434,74 +874,26 @@ multiplicity.
We select this situation by comparing the type constructor with fUNTyCon. In
this case, and this case only, we can safely drop the first argument (using the
tail function) and unify the rest.
--}
--- | Simple unification of two types; all type variables are bindable
--- Precondition: the kinds are already equal
-tcUnifyTy :: Type -> Type -- All tyvars are bindable
- -> Maybe Subst
- -- A regular one-shot (idempotent) substitution
-tcUnifyTy t1 t2 = tcUnifyTys alwaysBindFun [t1] [t2]
-
--- | Like 'tcUnifyTy', but also unifies the kinds
-tcUnifyTyKi :: Type -> Type -> Maybe Subst
-tcUnifyTyKi t1 t2 = tcUnifyTyKis alwaysBindFun [t1] [t2]
-
--- | Unify two types, treating type family applications as possibly unifying
--- with anything and looking through injective type family applications.
--- Precondition: kinds are the same
-tcUnifyTyWithTFs :: Bool -- ^ True <=> do two-way unification;
- -- False <=> do one-way matching.
- -- See end of sec 5.2 from the paper
- -> InScopeSet -- Should include the free tyvars of both Type args
- -> Type -> Type -- Types to unify
- -> Maybe Subst
--- This algorithm is an implementation of the "Algorithm U" presented in
--- the paper "Injective type families for Haskell", Figures 2 and 3.
--- The code is incorporated with the standard unifier for convenience, but
--- its operation should match the specification in the paper.
-tcUnifyTyWithTFs twoWay in_scope t1 t2
- = case tc_unify_tys alwaysBindFun twoWay True False RespectMultiplicities
- rn_env emptyTvSubstEnv emptyCvSubstEnv
- [t1] [t2] of
- Unifiable (tv_subst, _cv_subst) -> Just $ maybe_fix tv_subst
- MaybeApart _reason (tv_subst, _cv_subst) -> Just $ maybe_fix tv_subst
- -- we want to *succeed* in questionable cases. This is a
- -- pre-unification algorithm.
- SurelyApart -> Nothing
- where
- rn_env = mkRnEnv2 in_scope
-
- maybe_fix | twoWay = niFixSubst in_scope
- | otherwise = mkTvSubst in_scope -- when matching, don't confuse
- -- domain with range
-
------------------
-tcUnifyTys :: BindFun
- -> [Type] -> [Type]
- -> Maybe Subst
- -- ^ A regular one-shot (idempotent) substitution
- -- that unifies the erased types. See comments
- -- for 'tcUnifyTysFG'
+Note [The substitution in MaybeApart]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The constructor MaybeApart carries data with it, typically a TvSubstEnv. Why?
+Because consider unifying these:
--- The two types may have common type variables, and indeed do so in the
--- second call to tcUnifyTys in GHC.Tc.Instance.FunDeps.checkClsFD
-tcUnifyTys bind_fn tys1 tys2
- = case tcUnifyTysFG bind_fn tys1 tys2 of
- Unifiable result -> Just result
- _ -> Nothing
+(a, a, Int) ~ (b, [b], Bool)
--- | Like 'tcUnifyTys' but also unifies the kinds
-tcUnifyTyKis :: BindFun
- -> [Type] -> [Type]
- -> Maybe Subst
-tcUnifyTyKis bind_fn tys1 tys2
- = case tcUnifyTyKisFG bind_fn tys1 tys2 of
- Unifiable result -> Just result
- _ -> Nothing
+If we go left-to-right, we start with [a |-> b]. Then, on the middle terms, we
+apply the subst we have so far and discover that we need [b |-> [b]]. Because
+this fails the occurs check, we say that the types are MaybeApart (see above
+Note [Infinitary substitutions]). But, we can't stop there! Because if we
+continue, we discover that Int is SurelyApart from Bool, and therefore the
+types are apart. This has practical consequences for the ability for closed
+type family applications to reduce. See test case
+indexed-types/should_compile/Overlap14.
+-}
-- This type does double-duty. It is used in the UM (unifier monad) and to
--- return the final result. See Note [Fine-grained unification]
+-- return the final result. See Note [Unification result]
type UnifyResult = UnifyResultM Subst
-- | See Note [Unification result]
@@ -525,16 +917,25 @@ data MaybeApartReason
| MARTypeVsConstraint -- ^ matching Type ~? Constraint or the arrow types
-- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim
+ | MARCast -- ^ Very obscure.
+ -- See (KCU2) in Note [Kind coercions in Unify]
+
+
+combineMAR :: MaybeApartReason -> MaybeApartReason -> MaybeApartReason
+-- See (UR1) in Note [Unification result] for why MARInfinite wins
+combineMAR MARInfinite _ = MARInfinite -- MARInfinite wins
+combineMAR MARTypeFamily r = r -- Otherwise it doesn't really matter
+combineMAR MARTypeVsConstraint r = r
+combineMAR MARCast r = r
+
instance Outputable MaybeApartReason where
ppr MARTypeFamily = text "MARTypeFamily"
ppr MARInfinite = text "MARInfinite"
ppr MARTypeVsConstraint = text "MARTypeVsConstraint"
+ ppr MARCast = text "MARCast"
instance Semigroup MaybeApartReason where
- -- see end of Note [Unification result] for why
- MARTypeFamily <> r = r
- MARInfinite <> _ = MARInfinite
- MARTypeVsConstraint <> r = r
+ (<>) = combineMAR
instance Applicative UnifyResultM where
pure = Unifiable
@@ -548,76 +949,6 @@ instance Monad UnifyResultM where
SurelyApart -> SurelyApart
Unifiable x >>= f = f x
--- | @tcUnifyTysFG bind_tv tys1 tys2@ attempts to find a substitution @s@ (whose
--- domain elements all respond 'BindMe' to @bind_tv@) such that
--- @s(tys1)@ and that of @s(tys2)@ are equal, as witnessed by the returned
--- Coercions. This version requires that the kinds of the types are the same,
--- if you unify left-to-right.
-tcUnifyTysFG :: BindFun
- -> [Type] -> [Type]
- -> UnifyResult
-tcUnifyTysFG bind_fn tys1 tys2
- = tc_unify_tys_fg False bind_fn tys1 tys2
-
-tcUnifyTyKisFG :: BindFun
- -> [Type] -> [Type]
- -> UnifyResult
-tcUnifyTyKisFG bind_fn tys1 tys2
- = tc_unify_tys_fg True bind_fn tys1 tys2
-
-tc_unify_tys_fg :: Bool
- -> BindFun
- -> [Type] -> [Type]
- -> UnifyResult
-tc_unify_tys_fg match_kis bind_fn tys1 tys2
- = do { (env, _) <- tc_unify_tys bind_fn True False match_kis RespectMultiplicities rn_env
- emptyTvSubstEnv emptyCvSubstEnv
- tys1 tys2
- ; return $ niFixSubst in_scope env }
- where
- in_scope = mkInScopeSet $ tyCoVarsOfTypes tys1 `unionVarSet` tyCoVarsOfTypes tys2
- rn_env = mkRnEnv2 in_scope
-
--- | This function is actually the one to call the unifier -- a little
--- too general for outside clients, though.
-tc_unify_tys :: BindFun
- -> AmIUnifying -- ^ True <=> unify; False <=> match
- -> Bool -- ^ True <=> doing an injectivity check
- -> Bool -- ^ True <=> treat the kinds as well
- -> MultiplicityFlag -- ^ see Note [Rewrite rules ignore multiplicities in FunTy] in GHC.Core.Unify
- -> RnEnv2
- -> TvSubstEnv -- ^ substitution to extend
- -> CvSubstEnv
- -> [Type] -> [Type]
- -> UnifyResultM (TvSubstEnv, CvSubstEnv)
--- NB: It's tempting to ASSERT here that, if we're not matching kinds, then
--- the kinds of the types should be the same. However, this doesn't work,
--- as the types may be a dependent telescope, where later types have kinds
--- that mention variables occurring earlier in the list of types. Here's an
--- example (from typecheck/should_fail/T12709):
--- template: [rep :: RuntimeRep, a :: TYPE rep]
--- target: [LiftedRep :: RuntimeRep, Int :: TYPE LiftedRep]
--- We can see that matching the first pair will make the kinds of the second
--- pair equal. Yet, we still don't need a separate pass to unify the kinds
--- of these types, so it's appropriate to use the Ty variant of unification.
--- See also Note [tcMatchTy vs tcMatchTyKi].
-tc_unify_tys bind_fn unif inj_check match_kis match_mults rn_env tv_env cv_env tys1 tys2
- = initUM tv_env cv_env $
- do { when match_kis $
- unify_tys env kis1 kis2
- ; unify_tys env tys1 tys2
- ; (,) <$> getTvSubstEnv <*> getCvSubstEnv }
- where
- env = UMEnv { um_bind_fun = bind_fn
- , um_skols = emptyVarSet
- , um_unif = unif
- , um_inj_tf = inj_check
- , um_arr_mult = match_mults
- , um_rn_env = rn_env }
-
- kis1 = map typeKind tys1
- kis2 = map typeKind tys2
-
instance Outputable a => Outputable (UnifyResultM a) where
ppr SurelyApart = text "SurelyApart"
ppr (Unifiable x) = text "Unifiable" <+> ppr x
@@ -744,22 +1075,6 @@ niFixSubst in_scope tenv
where
tv' = updateTyVarKind (substTy subst) tv
-niSubstTvSet :: TvSubstEnv -> TyCoVarSet -> TyCoVarSet
--- Apply the non-idempotent substitution to a set of type variables,
--- remembering that the substitution isn't necessarily idempotent
--- This is used in the occurs check, before extending the substitution
-niSubstTvSet tsubst tvs
- = nonDetStrictFoldUniqSet (unionVarSet . get) emptyVarSet tvs
- -- It's OK to use a non-deterministic fold here because we immediately forget
- -- the ordering by creating a set.
- where
- get tv
- | Just ty <- lookupVarEnv tsubst tv
- = niSubstTvSet tsubst (tyCoVarsOfType ty)
-
- | otherwise
- = unitVarSet tv
-
{-
************************************************************************
* *
@@ -821,8 +1136,7 @@ in the "Injective Type Families" paper (Haskell'15), called [ITF]. When run
in this mode, it has the following properties.
(I1) If (unify σ τ) = SurelyApart, then σ and τ are not unifiable, even
- after arbitrary type family reductions. Note that σ and τ are
- not flattened here.
+ after arbitrary type family reductions.
(I2) If (unify σ τ) = MaybeApart θ, and if some
φ exists such that φ(σ) ~ φ(τ), then φ extends θ.
@@ -836,59 +1150,78 @@ but only when using this algorithm for matching:
Property M1 means that we must extend the substitution with,
say (a ↦ a) when appropriate during matching.
- See also Note [Self-substitution when matching].
+ See also Note [Self-substitution when unifying or matching].
(M2) Completeness of matching.
If θ(σ) = τ, then (match σ τ) = Unifiable φ,
where θ is an extension of φ.
-Sadly, property M2 and I2 conflict. Consider
+Wrinkle (SI1): um_inj_tf:
+ Sadly, property M2 and I2 conflict. Consider
+
+ type family F1 a b where
+ F1 Int Bool = Char
+ F1 Double String = Char
+
+ Consider now two matching problems:
+
+ P1. match (F1 a Bool) (F1 Int Bool)
+ P2. match (F1 a Bool) (F1 Double String)
-type family F1 a b where
- F1 Int Bool = Char
- F1 Double String = Char
+ In case P1, we must find (a ↦ Int) to satisfy M2. In case P2, we must /not/
+ find (a ↦ Double), in order to satisfy I2. (Note that the correct mapping for
+ I2 is (a ↦ Int). There is no way to discover this, but we mustn't map a to
+ anything else!)
-Consider now two matching problems:
+ We thus must parameterize the algorithm over whether it's being used
+ for an injectivity check (refrain from looking at non-injective arguments
+ to type families) or not (do indeed look at those arguments). This is
+ implemented by the um_inj_tf field of UMEnv.
-P1. match (F1 a Bool) (F1 Int Bool)
-P2. match (F1 a Bool) (F1 Double String)
+ (It's all a question of whether or not to include equation (7) from Fig. 2
+ of [ITF].)
-In case P1, we must find (a ↦ Int) to satisfy M2.
-In case P2, we must /not/ find (a ↦ Double), in order to satisfy I2. (Note
-that the correct mapping for I2 is (a ↦ Int). There is no way to discover
-this, but we mustn't map a to anything else!)
+ This extra parameter is a bit fiddly, perhaps, but seemingly less so than
+ having two separate, almost-identical algorithms.
-We thus must parameterize the algorithm over whether it's being used
-for an injectivity check (refrain from looking at non-injective arguments
-to type families) or not (do indeed look at those arguments). This is
-implemented by the um_inj_tf field of UMEnv.
+Note [Self-substitution when unifying or matching]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+What happens when we are unifying or matching two identical type variables?
+ a ~ a
-(It's all a question of whether or not to include equation (7) from Fig. 2
-of [ITF].)
+* When /unifying/, just succeed, without binding [a :-> a] in the substitution,
+ else we'd get an infinite substitution. We need to make this check before
+ we do the occurs check, of course.
-This extra parameter is a bit fiddly, perhaps, but seemingly less so than
-having two separate, almost-identical algorithms.
+* When /matching/, and `a` is a bindable variable from the template, we /do/
+ want to extend the substitution. Remember, a successful match should map all
+ the template variables (except ones that disappear when expanding synonyms),
-Note [Self-substitution when matching]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-What should happen when we're *matching* (not unifying) a1 with a1? We
-should get a substitution [a1 |-> a1]. A successful match should map all
-the template variables (except ones that disappear when expanding synonyms).
-But when unifying, we don't want to do this, because we'll then fall into
-a loop.
+ But when `a` is /not/ a bindable variable (perhaps it is a globally-in-scope
+ skolem) we want to treat it like a constant `Int ~ Int` and succeed.
-This arrangement affects the code in three places:
- - If we're matching a refined template variable, don't recur. Instead, just
- check for equality. That is, if we know [a |-> Maybe a] and are matching
- (a ~? Maybe Int), we want to just fail.
+ Notice: no occurs check! It's fine to match (a ~ Maybe a), because the
+ template vars of the template come from a different name space to the free
+ vars of the target.
- - Skip the occurs check when matching. This comes up in two places, because
- matching against variables is handled separately from matching against
- full-on types.
+ Note that this arrangement was provoked by a real failure, where the same
+ unique ended up in the template as in the target. (It was a rule firing when
+ compiling Data.List.NonEmpty.)
+
+* What about matching a /non-bindable/ variable? For example:
+ template-vars : {a}
+ matching problem: (forall b. b -> a) ~ (forall c. c -> Int)
+ We want to emerge with the substitution [a :-> Int]
+ But on the way we will encounter (b ~ b), when we match the bits before the
+ arrow under the forall, having renamed `c` to `b`. This match should just
+ succeed, just like (Int ~ Int), without extending the substitution.
+
+ It's important to do this for /non-bindable/ variables, not just for
+ forall-bound ones. In an associated type
+ instance C (Maybe a) where { type F (Maybe a) = Int }
+ `checkConsistentFamInst` matches (Maybe a) from the header against (Maybe a)
+ from the type-family instance, with `a` marked as non-bindable.
-Note that this arrangement was provoked by a real failure, where the same
-unique ended up in the template as in the target. (It was a rule firing when
-compiling Data.List.NonEmpty.)
Note [Matching coercion variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -922,55 +1255,84 @@ just match/unify their kinds, either, because this might gratuitously
fail. After all, `co` is the witness that the kinds are the same -- they
may look nothing alike.
-So, we pass a kind coercion to the match/unify worker. This coercion witnesses
+So, we pass a kind coercion `kco` to the main `unify_ty`. This coercion witnesses
the equality between the substed kind of the left-hand type and the substed
kind of the right-hand type. Note that we do not unify kinds at the leaves
-(as we did previously). We thus have
+(as we did previously).
-Hence: (Unification Kind Invariant)
------------------------------------
-In the call
+Hence: (UKINV) Unification Kind Invariant
+* In the call
unify_ty ty1 ty2 kco
-it must be that
+ it must be that
subst(kco) :: subst(kind(ty1)) ~N subst(kind(ty2))
-where `subst` is the ambient substitution in the UM monad. And in the call
+ where `subst` is the ambient substitution in the UM monad
+* In the call
unify_tys tys1 tys2
-(which has no kco), after we unify any prefix of tys1,tys2, the kinds of the
-head of the remaining tys1,tys2 are identical after substitution. This
-implies, for example, that the kinds of the head of tys1,tys2 are identical
-after substitution.
-
-To get this coercion, we first have to match/unify
-the kinds before looking at the types. Happily, we need look only one level
-up, as all kinds are guaranteed to have kind *.
-
-When we're working with type applications (either TyConApp or AppTy) we
-need to worry about establishing INVARIANT, as the kinds of the function
-& arguments aren't (necessarily) included in the kind of the result.
-When unifying two TyConApps, this is easy, because the two TyCons are
-the same. Their kinds are thus the same. As long as we unify left-to-right,
-we'll be sure to unify types' kinds before the types themselves. (For example,
-think about Proxy :: forall k. k -> *. Unifying the first args matches up
-the kinds of the second args.)
-
-For AppTy, we must unify the kinds of the functions, but once these are
-unified, we can continue unifying arguments without worrying further about
-kinds.
-
-The interface to this module includes both "...Ty" functions and
-"...TyKi" functions. The former assume that INVARIANT is already
-established, either because the kinds are the same or because the
-list of types being passed in are the well-typed arguments to some
-type constructor (see two paragraphs above). The latter take a separate
-pre-pass over the kinds to establish INVARIANT. Sometimes, it's important
-not to take the second pass, as it caused #12442.
-
-We thought, at one point, that this was all unnecessary: why should
-casts be in types in the first place? But they are sometimes. In
-dependent/should_compile/KindEqualities2, we see, for example the
-constraint Num (Int |> (blah ; sym blah)). We naturally want to find
-a dictionary for that constraint, which requires dealing with
-coercions in this manner.
+ (which has no kco), after we unify any prefix of tys1,tys2, the kinds of the
+ head of the remaining tys1,tys2 are identical after substitution. This
+ implies, for example, that the kinds of the head of tys1,tys2 are identical
+ after substitution.
+
+Preserving (UKINV) takes a bit of work, governed by the `match_kis` flag in
+`tc_unify_tys`:
+
+* When we're working with type applications (either TyConApp or AppTy) we
+ need to worry about establishing (UKINV), as the kinds of the function
+ & arguments aren't (necessarily) included in the kind of the result.
+ When unifying two TyConApps, this is easy, because the two TyCons are
+ the same. Their kinds are thus the same. As long as we unify left-to-right,
+ we'll be sure to unify types' kinds before the types themselves. (For example,
+ think about Proxy :: forall k. k -> *. Unifying the first args matches up
+ the kinds of the second args.)
+
+* For AppTy, we must unify the kinds of the functions, but once these are
+ unified, we can continue unifying arguments without worrying further about
+ kinds.
+
+* The interface to this module includes both "...Ty" functions and
+ "...TyKi" functions. The former assume that (UKINV) is already
+ established, either because the kinds are the same or because the
+ list of types being passed in are the well-typed arguments to some
+ type constructor (see two paragraphs above). The latter take a separate
+ pre-pass over the kinds to establish (UKINV). Sometimes, it's important
+ not to take the second pass, as it caused #12442.
+
+Wrinkles
+
+(KCU1) We ensure that the `kco` argument never mentions variables in the
+ domain of either RnEnvL or RnEnvR. Why?
+
+ * `kco` is used only to build the final well-kinded substitution
+ a :-> ty |> kco
+ The range of the substitution never mentions forall-bound variables,
+ so `kco` cannot either.
+
+ * `kco` mixes up types from both left and right arguments of
+ `unify_ty`, which have different renamings in the RnEnv2.
+
+ The easiest thing is to insist that `kco` does not need renaming with
+ the RnEnv2; it mentions no forall-bound variables.
+
+ To achieve this we do a `mentionsForAllBoundTyVars` test in the
+ `CastTy` cases of `unify_ty`.
+
+(KCU2) Suppose we are unifying
+ (forall a. x |> (...F a b...) ~ (forall a. y)
+ We can't bind y :-> x |> (...F a b...), becuase of that free `a`.
+
+ But if we later learn that b=Int, and F a Int = Bool,
+ that free `a` might disappear, so we could unify with
+ y :-> x |> (...Bool...)
+
+ Conclusion: if there is a free forall-bound variable in a cast,
+ return MaybeApart, with a MaybeApartReason of MARCast.
+
+(KCU3) We thought, at one point, that this was all unnecessary: why should
+ casts be in types in the first place? But they are sometimes. In
+ dependent/should_compile/KindEqualities2, we see, for example the
+ constraint Num (Int |> (blah ; sym blah)). We naturally want to find
+ a dictionary for that constraint, which requires dealing with
+ coercions in this manner.
Note [Matching in the presence of casts (1)]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1138,10 +1500,17 @@ c.f. Note [Comparing type synonyms] in GHC.Core.TyCo.Compare
type AmIUnifying = Bool -- True <=> Unifying
-- False <=> Matching
+type InType = Type -- Before applying the RnEnv2
+type OutCoercion = Coercion -- After applying the RnEnv2
+
+
unify_ty :: UMEnv
- -> Type -> Type -- Types to be unified and a co
- -> CoercionN -- A coercion between their kinds
- -- See Note [Kind coercions in Unify]
+ -> InType -> InType -- Types to be unified
+ -> OutCoercion -- A nominal coercion between their kinds
+ -- OutCoercion: the RnEnv has already been applied
+ -- When matching, the coercion is in "target space",
+ -- not "template space"
+ -- See Note [Kind coercions in Unify]
-> UM ()
-- Precondition: see (Unification Kind Invariant)
--
@@ -1157,53 +1526,93 @@ unify_ty env ty1 ty2 kco
-- Now handle the cases we can "look through": synonyms and casts.
| Just ty1' <- coreView ty1 = unify_ty env ty1' ty2 kco
| Just ty2' <- coreView ty2 = unify_ty env ty1 ty2' kco
- | CastTy ty1' co <- ty1 = if um_unif env
- then unify_ty env ty1' ty2 (co `mkTransCo` kco)
- else -- See Note [Matching in the presence of casts (1)]
- do { subst <- getSubst env
- ; let co' = substCo subst co
- ; unify_ty env ty1' ty2 (co' `mkTransCo` kco) }
- | CastTy ty2' co <- ty2 = unify_ty env ty1 ty2' (kco `mkTransCo` mkSymCo co)
-unify_ty env (TyVarTy tv1) ty2 kco
- = uVar env tv1 ty2 kco
-unify_ty env ty1 (TyVarTy tv2) kco
- | um_unif env -- If unifying, can swap args
- = uVar (umSwapRn env) tv2 ty1 (mkSymCo kco)
+unify_ty env (CastTy ty1 co1) ty2 kco
+ | mentionsForAllBoundTyVarsL env (tyCoVarsOfCo co1)
+ -- See (KCU1) in Note [Kind coercions in Unify]
+ = maybeApart MARCast -- See (KCU2)
-unify_ty env ty1 ty2 _kco
+ | um_unif env
+ = unify_ty env ty1 ty2 (co1 `mkTransCo` kco)
+
+ | otherwise -- We are matching, not unifying
+ = do { subst <- getSubst env
+ ; let co' = substCo subst co1
+ -- We match left-to-right, so the free template vars of the
+ -- coercion should already have been matched.
+ -- See Note [Matching in the presence of casts (1)]
+ -- NB: co1 does not mention forall-bound vars, so no need to rename
+ ; unify_ty env ty1 ty2 (co' `mkTransCo` kco) }
+
+unify_ty env ty1 (CastTy ty2 co2) kco
+ | mentionsForAllBoundTyVarsR env (tyCoVarsOfCo co2)
+ -- See (KCU1) in Note [Kind coercions in Unify]
+ = maybeApart MARCast -- See (KCU2)
+ | otherwise
+ = unify_ty env ty1 ty2 (kco `mkTransCo` mkSymCo co2)
+ -- NB: co2 does not mention forall-bound variables
- -- Handle non-oversaturated type families first
- -- See Note [Unifying type applications]
- --
- -- (C1) If we have T x1 ... xn ~ T y1 ... yn, use injectivity information of T
- -- Note that both sides must not be oversaturated
- | Just (tc1, tys1) <- isSatTyFamApp mb_tc_app1
- , Just (tc2, tys2) <- isSatTyFamApp mb_tc_app2
- , tc1 == tc2
- = do { let inj = case tyConInjectivityInfo tc1 of
- NotInjective -> repeat False
- Injective bs -> bs
+-- Applications need a bit of care!
+-- They can match FunTy and TyConApp, so use splitAppTy_maybe
+unify_ty env (AppTy ty1a ty1b) ty2 _kco
+ | Just (ty2a, ty2b) <- tcSplitAppTyNoView_maybe ty2
+ = unify_ty_app env ty1a [ty1b] ty2a [ty2b]
- (inj_tys1, noninj_tys1) = partitionByList inj tys1
- (inj_tys2, noninj_tys2) = partitionByList inj tys2
+unify_ty env ty1 (AppTy ty2a ty2b) _kco
+ | Just (ty1a, ty1b) <- tcSplitAppTyNoView_maybe ty1
+ = unify_ty_app env ty1a [ty1b] ty2a [ty2b]
- ; unify_tys env inj_tys1 inj_tys2
- ; unless (um_inj_tf env) $ -- See (end of) Note [Specification of unification]
- don'tBeSoSure MARTypeFamily $ unify_tys env noninj_tys1 noninj_tys2 }
+unify_ty _ (LitTy x) (LitTy y) _kco | x == y = return ()
- | Just _ <- isSatTyFamApp mb_tc_app1 -- (C2) A (not-over-saturated) type-family application
- = maybeApart MARTypeFamily -- behaves like a type variable; might match
+unify_ty env (ForAllTy (Bndr tv1 _) ty1) (ForAllTy (Bndr tv2 _) ty2) kco
+ -- ToDo: See Note [Unifying coercion-foralls]
+ = do { unify_ty env (varType tv1) (varType tv2) (mkNomReflCo liftedTypeKind)
+ ; let env' = umRnBndr2 env tv1 tv2
+ ; unify_ty env' ty1 ty2 kco }
- | Just _ <- isSatTyFamApp mb_tc_app2 -- (C2) A (not-over-saturated) type-family application
- -- behaves like a type variable; might unify
- -- but doesn't match (as in the TyVarTy case)
- = if um_unif env then maybeApart MARTypeFamily else surelyApart
+-- See Note [Matching coercion variables]
+unify_ty env (CoercionTy co1) (CoercionTy co2) kco
+ = do { c_subst <- getCvSubstEnv
+ ; case co1 of
+ CoVarCo cv
+ | not (um_unif env)
+ , not (cv `elemVarEnv` c_subst) -- Not forall-bound
+ , let (_mult_co, co_l, co_r) = decomposeFunCo kco
+ -- Because the coercion is used in a type, it should be safe to
+ -- ignore the multiplicity coercion, _mult_co
+ -- cv :: t1 ~ t2
+ -- co2 :: s1 ~ s2
+ -- co_l :: t1 ~ s1
+ -- co_r :: t2 ~ s2
+ rhs_co = co_l `mkTransCo` co2 `mkTransCo` mkSymCo co_r
+ , BindMe <- um_bind_tv_fun env cv (CoercionTy rhs_co)
+ -> if mentionsForAllBoundTyVarsR env (tyCoVarsOfCo co2)
+ then surelyApart
+ else extendCvEnv cv rhs_co
- -- Handle oversaturated type families.
- --
- -- They can match an application (TyConApp/FunTy/AppTy), this is handled
- -- the same way as in the AppTy case below.
+ _ -> return () }
+
+unify_ty env (TyVarTy tv1) ty2 kco
+ = uVarOrFam env (TyVarLHS tv1) ty2 kco
+
+unify_ty env ty1 (TyVarTy tv2) kco
+ | um_unif env -- If unifying, can swap args; but not when matching
+ = uVarOrFam (umSwapRn env) (TyVarLHS tv2) ty1 (mkSymCo kco)
+
+-- Deal with TyConApps
+unify_ty env ty1 ty2 kco
+ -- Handle non-oversaturated type families first
+ -- See Note [Unifying type applications]
+ | Just (tc,tys) <- mb_sat_fam_app1
+ = uVarOrFam env (TyFamLHS tc tys) ty2 kco
+
+ | um_unif env
+ , Just (tc,tys) <- mb_sat_fam_app2
+ = uVarOrFam (umSwapRn env) (TyFamLHS tc tys) ty1 (mkSymCo kco)
+
+ -- Handle oversaturated type families. Suppose we have
+ -- (F a b) ~ (c d) where F has arity 1
+ -- We definitely want to decompose that type application! (#22647)
--
-- If there is no application, an oversaturated type family can only
-- match a type variable or a saturated type family,
@@ -1227,7 +1636,7 @@ unify_ty env ty1 ty2 _kco
, Just (tc2, tys2) <- mb_tc_app2
, tc1 == tc2
= do { massertPpr (isInjectiveTyCon tc1 Nominal) (ppr tc1)
- ; unify_tc_app tc1 tys1 tys2
+ ; unify_tc_app env tc1 tys1 tys2
}
-- TYPE and CONSTRAINT are not Apart
@@ -1257,64 +1666,34 @@ unify_ty env ty1 ty2 _kco
where
mb_tc_app1 = splitTyConApp_maybe ty1
mb_tc_app2 = splitTyConApp_maybe ty2
+ mb_sat_fam_app1 = isSatFamApp ty1
+ mb_sat_fam_app2 = isSatFamApp ty2
- unify_tc_app tc tys1 tys2
- | tc == fUNTyCon
- , IgnoreMultiplicities <- um_arr_mult env
- , (_mult1 : no_mult_tys1) <- tys1
- , (_mult2 : no_mult_tys2) <- tys2
- = -- We're comparing function arrow types here (not constraint arrow
- -- types!), and they have at least one argument, which is the arrow's
- -- multiplicity annotation. The flag `um_arr_mult` instructs us to
- -- ignore multiplicities in this very case. This is a little tricky: see
- -- point (3) in Note [Rewrite rules ignore multiplicities in FunTy].
- unify_tys env no_mult_tys1 no_mult_tys2
-
- | otherwise
- = unify_tys env tys1 tys2
-
- -- Applications need a bit of care!
- -- They can match FunTy and TyConApp, so use splitAppTy_maybe
- -- NB: we've already dealt with type variables,
- -- so if one type is an App the other one jolly well better be too
-unify_ty env (AppTy ty1a ty1b) ty2 _kco
- | Just (ty2a, ty2b) <- tcSplitAppTyNoView_maybe ty2
- = unify_ty_app env ty1a [ty1b] ty2a [ty2b]
-
-unify_ty env ty1 (AppTy ty2a ty2b) _kco
- | Just (ty1a, ty1b) <- tcSplitAppTyNoView_maybe ty1
- = unify_ty_app env ty1a [ty1b] ty2a [ty2b]
-
-unify_ty _ (LitTy x) (LitTy y) _kco | x == y = return ()
-
-unify_ty env (ForAllTy (Bndr tv1 _) ty1) (ForAllTy (Bndr tv2 _) ty2) kco
- = do { unify_ty env (varType tv1) (varType tv2) (mkNomReflCo liftedTypeKind)
- ; let env' = umRnBndr2 env tv1 tv2
- ; unify_ty env' ty1 ty2 kco }
+unify_ty _ _ _ _ = surelyApart
--- See Note [Matching coercion variables]
-unify_ty env (CoercionTy co1) (CoercionTy co2) kco
- = do { c_subst <- getCvSubstEnv
- ; case co1 of
- CoVarCo cv
- | not (um_unif env)
- , not (cv `elemVarEnv` c_subst)
- , let (_, co_l, co_r) = decomposeFunCo kco
- -- Because the coercion is used in a type, it should be safe to
- -- ignore the multiplicity coercion.
- -- cv :: t1 ~ t2
- -- co2 :: s1 ~ s2
- -- co_l :: t1 ~ s1
- -- co_r :: t2 ~ s2
- rhs_co = co_l `mkTransCo` co2 `mkTransCo` mkSymCo co_r
- , BindMe <- tvBindFlag env cv (CoercionTy rhs_co)
- -> do { checkRnEnv env (tyCoVarsOfCo co2)
- ; extendCvEnv cv rhs_co }
- _ -> return () }
+-----------------------------
+unify_tc_app :: UMEnv -> TyCon -> [Type] -> [Type] -> UM ()
+-- Mainly just unifies the argument types;
+-- but with a special case for fUNTyCon
+unify_tc_app env tc tys1 tys2
+ | tc == fUNTyCon
+ , IgnoreMultiplicities <- um_arr_mult env
+ , (_mult1 : no_mult_tys1) <- tys1
+ , (_mult2 : no_mult_tys2) <- tys2
+ = -- We're comparing function arrow types here (not constraint arrow
+ -- types!), and they have at least one argument, which is the arrow's
+ -- multiplicity annotation. The flag `um_arr_mult` instructs us to
+ -- ignore multiplicities in this very case. This is a little tricky: see
+ -- point (3) in Note [Rewrite rules ignore multiplicities in FunTy].
+ unify_tys env no_mult_tys1 no_mult_tys2
-unify_ty _ _ _ _ = surelyApart
+ | otherwise
+ = unify_tys env tys1 tys2
+-----------------------------
unify_ty_app :: UMEnv -> Type -> [Type] -> Type -> [Type] -> UM ()
+-- Deal with (t1 t1args) ~ (t2 t2args)
+-- where length t1args = length t2args
unify_ty_app env ty1 ty1args ty2 ty2args
| Just (ty1', ty1a) <- splitAppTyNoView_maybe ty1
, Just (ty2', ty2a) <- splitAppTyNoView_maybe ty2
@@ -1330,6 +1709,7 @@ unify_ty_app env ty1 ty1args ty2 ty2args
-- See Note [Matching in the presence of casts (2)]
; unify_tys env ty1args ty2args }
+-----------------------------
unify_tys :: UMEnv -> [Type] -> [Type] -> UM ()
-- Precondition: see (Unification Kind Invariant)
unify_tys env orig_xs orig_ys
@@ -1346,153 +1726,216 @@ unify_tys env orig_xs orig_ys
-- Possibly different saturations of a polykinded tycon
-- See Note [Polykinded tycon applications]
-isSatTyFamApp :: Maybe (TyCon, [Type]) -> Maybe (TyCon, [Type])
+---------------------------------
+isSatFamApp :: Type -> Maybe (TyCon, [Type])
-- Return the argument if we have a saturated type family application
--- If it is /over/ saturated then we return False. E.g.
--- unify_ty (F a b) (c d) where F has arity 1
--- we definitely want to decompose that type application! (#22647)
-isSatTyFamApp tapp@(Just (tc, tys))
+-- Why saturated? See (ATF4) in Note [Apartness and type families]
+isSatFamApp (TyConApp tc tys)
| isTypeFamilyTyCon tc
&& not (tys `lengthExceeds` tyConArity tc) -- Not over-saturated
- = tapp
-isSatTyFamApp _ = Nothing
+ = Just (tc, tys)
+isSatFamApp _ = Nothing
---------------------------------
-uVar :: UMEnv
- -> InTyVar -- Variable to be unified
- -> Type -- with this Type
- -> Coercion -- :: kind tv ~N kind ty
- -> UM ()
-
-uVar env tv1 ty kco
- = do { -- Apply the ambient renaming
- let tv1' = umRnOccL env tv1
-
- -- Check to see whether tv1 is refined by the substitution
- ; subst <- getTvSubstEnv
- ; case (lookupVarEnv subst tv1') of
- Just ty' | um_unif env -- Unifying, so call
- -> unify_ty env ty' ty kco -- back into unify
- | otherwise
- -> -- Matching, we don't want to just recur here.
- -- 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) `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
- -> OutTyVar -- variable to be unified
- -> Type -- with this Type
- -> Type -- (version w/ expanded synonyms)
- -> Coercion -- :: kind tv ~N kind ty
- -> UM ()
-
--- We know that tv1 isn't refined
-
-uUnrefined env tv1' ty2 ty2' kco
- | Just ty2'' <- coreView ty2'
- = uUnrefined env tv1' ty2 ty2'' kco -- Unwrap synonyms
- -- This is essential, in case we have
- -- type Foo a = a
- -- and then unify a ~ Foo a
-
- | TyVarTy tv2 <- ty2'
- = do { let tv2' = umRnOccR env tv2
- ; unless (tv1' == tv2' && um_unif env) $ do
- -- If we are unifying a ~ a, just return immediately
- -- Do not extend the substitution
- -- See Note [Self-substitution when matching]
-
- -- Check to see whether tv2 is refined
- { subst <- getTvSubstEnv
- ; case lookupVarEnv subst tv2 of
- { Just ty' | um_unif env -> uUnrefined env tv1' ty' ty' kco
- ; _ ->
-
- do { -- So both are unrefined
- -- Bind one or the other, depending on which is bindable
- ; let rhs1 = ty2 `mkCastTy` mkSymCo kco
- rhs2 = ty1 `mkCastTy` kco
- b1 = tvBindFlag env tv1' rhs1
- b2 = tvBindFlag env tv2' rhs2
- ty1 = mkTyVarTy tv1'
- ; case (b1, b2) of
- (BindMe, _) -> bindTv env tv1' rhs1
- (_, BindMe) | um_unif env
- -> bindTv (umSwapRn env) tv2 rhs2
-
- _ | tv1' == tv2' -> return ()
- -- How could this happen? If we're only matching and if
- -- we're comparing forall-bound variables.
-
- _ -> surelyApart
- }}}}
-
-uUnrefined env tv1' ty2 _ kco -- ty2 is not a type variable
- = case tvBindFlag env tv1' rhs of
- Apart -> surelyApart
- BindMe -> bindTv env tv1' rhs
+uVarOrFam :: UMEnv -> CanEqLHS -> InType -> OutCoercion -> UM ()
+-- Invariants: (a) If ty1 is a TyFamLHS, then ty2 is NOT a TyVarTy
+-- (b) both args have had coreView already applied
+-- Why saturated? See (ATF4) in Note [Apartness and type families]
+uVarOrFam env ty1 ty2 kco
+ = do { substs <- getSubstEnvs
+ ; go NotSwapped substs ty1 ty2 kco }
where
- rhs = ty2 `mkCastTy` mkSymCo kco
-
-bindTv :: UMEnv -> OutTyVar -> Type -> UM ()
--- OK, so we want to extend the substitution with tv := ty
--- But first, we must do a couple of checks
-bindTv env tv1 ty2
- = do { let free_tvs2 = tyCoVarsOfType ty2
-
- -- Make sure tys mentions no local variables
- -- E.g. (forall a. b) ~ (forall a. [a])
- -- We should not unify b := [a]!
- ; checkRnEnv env free_tvs2
+ -- `go` takes two bites at the cherry; if the first one fails
+ -- it swaps the arguments and tries again; and then it fails.
+ -- The SwapFlag argument tells `go` whether it is on the first
+ -- bite (NotSwapped) or the second (IsSwapped).
+ -- E.g. a ~ F p q
+ -- Starts with: go a (F p q)
+ -- if `a` not bindable, swap to: go (F p q) a
+ go swapped substs (TyVarLHS tv1) ty2 kco
+ = go_tv swapped substs tv1 ty2 kco
+
+ go swapped substs (TyFamLHS tc tys) ty2 kco
+ = go_fam swapped substs tc tys ty2 kco
+
+ -----------------------------
+ -- go_tv: LHS is a type variable
+ -- The sequence of tests is very similar to go_tv
+ go_tv swapped substs tv1 ty2 kco
+ | Just ty1' <- lookupVarEnv (um_tv_env substs) tv1'
+ = -- We already have a substitution for tv1
+ if | um_unif env -> unify_ty env ty1' ty2 kco
+ | (ty1' `mkCastTy` kco) `tcEqType` ty2 -> return ()
+ | otherwise -> surelyApart
+ -- Unifying: recurse into unify_ty
+ -- Matching: we /don't/ want to just recurse here, because the range of
+ -- the subst is the target type, not the template type. So, just check
+ -- for normal type equality.
+ -- 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.
+
+ -- If we are matching or unifying a ~ a, take care
+ -- See Note [Self-substitution when unifying or matching]
+ | TyVarTy tv2 <- ty2
+ , let tv2' = umRnOccR env tv2
+ , tv1' == tv2'
+ = if | um_unif env -> return ()
+ | tv1_is_bindable -> extendTvEnv tv1' ty2
+ | otherwise -> return ()
+
+ | tv1_is_bindable
+ , not (mentionsForAllBoundTyVarsR env ty2_fvs)
+ -- ty2_fvs: kco does not mention forall-bound vars
+ , not occurs_check
+ = -- No occurs check, nor skolem-escape; just bind the tv
+ -- We don't need to rename `rhs` because it mentions no forall-bound vars
+ extendTvEnv tv1' rhs -- Bind tv1:=rhs and continue
+
+ -- When unifying, try swapping:
+ -- e.g. a ~ F p q with `a` not bindable: we might succeed with go_fam
+ -- e.g. a ~ beta with `a` not bindable: we might be able to bind `beta`
+ -- e.g. beta ~ F beta Int occurs check; but MaybeApart after swapping
+ | um_unif env
+ , NotSwapped <- swapped -- If we have swapped already, don't do so again
+ , Just lhs2 <- canEqLHS_maybe ty2
+ = go IsSwapped substs lhs2 (mkTyVarTy tv1) (mkSymCo kco)
+
+ | occurs_check = maybeApart MARInfinite -- Occurs check
+ | otherwise = surelyApart
+
+ where
+ tv1' = umRnOccL env tv1
+ ty2_fvs = tyCoVarsOfType ty2
+ rhs_fvs = ty2_fvs `unionVarSet` tyCoVarsOfCo kco
+ rhs = ty2 `mkCastTy` mkSymCo kco
+ tv1_is_bindable | not (tv1' `elemVarSet` um_foralls env)
+ -- tv1' is not forall-bound, but tv1 can still differ
+ -- from tv1; see Note [Cloning the template binders]
+ -- in GHC.Core.Rules. So give tv1' to um_bind_tv_fun.
+ , BindMe <- um_bind_tv_fun env tv1' rhs
+ = True
+ | otherwise
+ = False
+
+ occurs_check = um_unif env &&
+ occursCheck (um_tv_env substs) tv1 rhs_fvs
+ -- Occurs check, only when unifying
+ -- see Note [Infinitary substitutions]
+ -- Make sure you include `kco` in rhs_tvs #14846
+
+ -----------------------------
+ -- go_fam: LHS is a saturated type-family application
+ -- Invariant: ty2 is not a TyVarTy
+ go_fam swapped substs tc1 tys1 ty2 kco
+ -- If we are under a forall, just give up and return MaybeApart
+ -- see (ATF3) in Note [Apartness and type families]
+ | not (isEmptyVarSet (um_foralls env))
+ = maybeApart MARTypeFamily
+
+ -- We are not under any foralls, so the RnEnv2 is empty
+ -- Check if we have an existing substitution for the LHS; if so, recurse
+ | Just ty1' <- lookupFamEnv (um_fam_env substs) tc1 tys1
+ = if | um_unif env -> unify_ty env ty1' ty2 kco
+ -- Below here we are matching
+ -- The return () case deals with:
+ -- Template: (F a)..(F a)
+ -- Target: (F b)..(F b)
+ -- This should match! With [a :-> b]
+ | (ty1' `mkCastTy` kco) `tcEqType` ty2 -> return ()
+ | otherwise -> maybeApart MARTypeFamily
+
+ -- Check for equality F tys1 ~ F tys2
+ | Just (tc2, tys2) <- isSatFamApp ty2
+ , tc1 == tc2
+ = go_fam_fam tc1 tys1 tys2 kco
+
+ -- Now check if we can bind the (F tys) to the RHS
+ | BindMe <- um_bind_fam_fun env tc1 tys1 rhs
+ = -- ToDo: do we need an occurs check here?
+ do { extendFamEnv tc1 tys1 rhs
+ ; maybeApart MARTypeFamily }
+
+ -- Swap in case of (F a b) ~ (G c d e)
+ -- Maybe um_bind_fam_fun is False of (F a b) but true of (G c d e)
+ -- NB: a type family can appear on the template when matching
+ -- see (ATF6) in Note [Apartness and type families]
+ | um_unif env
+ , NotSwapped <- swapped
+ , Just lhs2 <- canEqLHS_maybe ty2
+ = go IsSwapped substs lhs2 (mkTyConApp tc1 tys1) (mkSymCo kco)
+
+ | otherwise -- See (ATF5) in Note [Apartness and type families]
+ = surelyApart
+
+ where
+ rhs = ty2 `mkCastTy` mkSymCo kco
+
+ -----------------------------
+ -- go_fam_fam: LHS and RHS are both saturated type-family applications,
+ -- for the same type-family F
+ go_fam_fam tc tys1 tys2 kco
+ | tcEqTyConAppArgs tys1 tys2
+ -- Detect (F tys ~ F tys); otherwise we'd build an infinite substitution
+ = return ()
- -- Occurs check, see Note [Fine-grained unification]
- -- Make sure you include 'kco' (which ty2 does) #14846
- ; occurs <- occursCheck env tv1 free_tvs2
-
- ; if occurs then maybeApart MARInfinite
- else extendTvEnv tv1 ty2 }
+ | otherwise
+ -- Decompose (F tys1 ~ F tys2): (ATF9)
+ -- Use injectivity information of F: (ATF10)
+ -- But first bind the type-fam if poss: (ATF11)
+ = do { bind_fam_if_poss -- (ATF11)
+ ; unify_tys env inj_tys1 inj_tys2 -- (ATF10)
+ ; unless (um_inj_tf env) $ -- (ATF12)
+ don'tBeSoSure MARTypeFamily $ -- (ATF9)
+ unify_tys env noninj_tys1 noninj_tys2 }
+ where
+ inj = case tyConInjectivityInfo tc of
+ NotInjective -> repeat False
+ Injective bs -> bs
+
+ (inj_tys1, noninj_tys1) = partitionByList inj tys1
+ (inj_tys2, noninj_tys2) = partitionByList inj tys2
+
+ bind_fam_if_poss | BindMe <- um_bind_fam_fun env tc tys1 rhs1
+ = extendFamEnv tc tys1 rhs1
+ | um_unif env
+ , BindMe <- um_bind_fam_fun env tc tys2 rhs2
+ = extendFamEnv tc tys2 rhs2
+ | otherwise
+ = return ()
+ rhs1 = mkTyConApp tc tys2 `mkCastTy` mkSymCo kco
+ rhs2 = mkTyConApp tc tys1 `mkCastTy` kco
+
+
+occursCheck :: TvSubstEnv -> TyVar -> TyCoVarSet -> Bool
+occursCheck env tv1 tvs
+ = anyVarSet bad tvs
+ where
+ bad tv | Just ty <- lookupVarEnv env tv
+ = anyVarSet bad (tyCoVarsOfType ty)
+ | otherwise
+ = tv == tv1
-occursCheck :: UMEnv -> TyVar -> VarSet -> UM Bool
-occursCheck env tv free_tvs
- | um_unif env
- = do { tsubst <- getTvSubstEnv
- ; return (tv `elemVarSet` niSubstTvSet tsubst free_tvs) }
+{- Note [Unifying coercion-foralls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we try to unify (forall cv. t1) ~ (forall cv. t2).
+See Note [ForAllTy] in GHC.Core.TyCo.Rep.
- | otherwise -- Matching; no occurs check
- = return False -- See Note [Self-substitution when matching]
+The problem with coercion variables is that coercion abstraction is not erased:
+the `kco` shouldn't propagate from outside the ForAllTy to inside. Instead, I think
+the correct new `kco` for the recursive call is `mkNomReflCo liftedTypeKind` (but I'm
+a little worried it might be Constraint sometimes).
-{-
-%************************************************************************
-%* *
- Binding decisions
-* *
-************************************************************************
+This potential problem has been there a long time, and I'm going to let
+sleeping dogs lie for now.
-}
-data BindFlag
- = BindMe -- ^ A regular type variable
-
- | Apart -- ^ Declare that this type variable is /apart/ from the
- -- type provided. That is, the type variable will never
- -- be instantiated to that type.
- -- See also Note [Binding when looking up instances]
- -- in GHC.Core.InstEnv.
- deriving Eq
--- NB: It would be conceivable to have an analogue to MaybeApart here,
--- but there is not yet a need.
-
{-
************************************************************************
* *
@@ -1506,30 +1949,51 @@ data UMEnv
, um_inj_tf :: Bool
-- Checking for injectivity?
- -- See (end of) Note [Specification of unification]
+ -- See (SI1) in Note [Specification of unification]
, um_arr_mult :: MultiplicityFlag
-- Whether to unify multiplicity arguments when unifying arrows.
-- See Note [Rewrite rules ignore multiplicities in FunTy]
, um_rn_env :: RnEnv2
- -- Renaming InTyVars to OutTyVars; this eliminates
- -- shadowing, and lines up matching foralls on the left
- -- and right
+ -- Renaming InTyVars to OutTyVars; this eliminates shadowing, and
+ -- lines up matching foralls on the left and right
+ -- See (CU2) in Note [The Core unifier]
- , um_skols :: TyVarSet
+ , um_foralls :: TyVarSet
-- OutTyVars bound by a forall in this unification;
-- Do not bind these in the substitution!
-- See the function tvBindFlag
- , um_bind_fun :: BindFun
- -- User-supplied BindFlag function,
- -- for variables not in um_skols
+ , um_bind_tv_fun :: BindTvFun
+ -- User-supplied BindFlag function, for variables not in um_foralls
+ -- See (CU1) in Note [The Core unifier]
+
+ , um_bind_fam_fun :: BindFamFun
+ -- Similar to um_bind_tv_fun, but for type-family applications
+ -- See (ATF8) in Note [Apartness and type families]
}
+type FamSubstEnv = TyConEnv (ListMap TypeMap Type)
+ -- Map a TyCon and a list of types to a type
+ -- Domain of FamSubstEnv is exactly-saturated type-family
+ -- applications (F t1...tn)
+
+lookupFamEnv :: FamSubstEnv -> TyCon -> [Type] -> Maybe Type
+lookupFamEnv env tc tys
+ = do { tys_map <- lookupTyConEnv env tc
+ ; lookupTM tys tys_map }
+
data UMState = UMState
{ um_tv_env :: TvSubstEnv
- , um_cv_env :: CvSubstEnv }
+ , um_cv_env :: CvSubstEnv
+ , um_fam_env :: FamSubstEnv }
+ -- um_tv_env, um_cv_env, um_fam_env are all "global" substitutions;
+ -- that is, neither their domains nor their ranges mention any variables
+ -- in um_foralls; i.e. variables bound by foralls inside the types being unified
+
+ -- When /matching/ um_fam_env is usually empty; but not quite always.
+ -- See (ATF6) and (ATF7) of Note [Apartness and type families]
newtype UM a
= UM' { unUM :: UMState -> UnifyResultM (UMState, a) }
@@ -1561,20 +2025,18 @@ instance MonadFail UM where
initUM :: TvSubstEnv -- subst to extend
-> CvSubstEnv
- -> UM a -> UnifyResultM a
+ -> UM ()
+ -> UnifyResultM (TvSubstEnv, CvSubstEnv)
initUM subst_env cv_subst_env um
= case unUM um state of
- Unifiable (_, subst) -> Unifiable subst
- MaybeApart r (_, subst) -> MaybeApart r subst
+ Unifiable (state, _) -> Unifiable (get state)
+ MaybeApart r (state, _) -> MaybeApart r (get state)
SurelyApart -> SurelyApart
where
state = UMState { um_tv_env = subst_env
- , um_cv_env = cv_subst_env }
-
-tvBindFlag :: UMEnv -> OutTyVar -> Type -> BindFlag
-tvBindFlag env tv rhs
- | tv `elemVarSet` um_skols env = Apart
- | otherwise = um_bind_fun env tv rhs
+ , um_cv_env = cv_subst_env
+ , um_fam_env = emptyTyConEnv }
+ get (UMState { um_tv_env = tv_env, um_cv_env = cv_env }) = (tv_env, cv_env)
getTvSubstEnv :: UM TvSubstEnv
getTvSubstEnv = UM $ \state -> Unifiable (state, um_tv_env state)
@@ -1582,6 +2044,9 @@ getTvSubstEnv = UM $ \state -> Unifiable (state, um_tv_env state)
getCvSubstEnv :: UM CvSubstEnv
getCvSubstEnv = UM $ \state -> Unifiable (state, um_cv_env state)
+getSubstEnvs :: UM UMState
+getSubstEnvs = UM $ \state -> Unifiable (state, state)
+
getSubst :: UMEnv -> UM Subst
getSubst env = do { tv_env <- getTvSubstEnv
; cv_env <- getCvSubstEnv
@@ -1596,19 +2061,32 @@ extendCvEnv :: CoVar -> Coercion -> UM ()
extendCvEnv cv co = UM $ \state ->
Unifiable (state { um_cv_env = extendVarEnv (um_cv_env state) cv co }, ())
+extendFamEnv :: TyCon -> [Type] -> Type -> UM ()
+extendFamEnv tc tys ty = UM $ \state ->
+ Unifiable (state { um_fam_env = extend (um_fam_env state) tc }, ())
+ where
+ extend :: FamSubstEnv -> TyCon -> FamSubstEnv
+ extend = alterTyConEnv alter_tm
+
+ alter_tm :: Maybe (ListMap TypeMap Type) -> Maybe (ListMap TypeMap Type)
+ alter_tm m_elt = Just (alterTM tys (\_ -> Just ty) (m_elt `orElse` emptyTM))
+
umRnBndr2 :: UMEnv -> TyCoVar -> TyCoVar -> UMEnv
umRnBndr2 env v1 v2
- = env { um_rn_env = rn_env', um_skols = um_skols env `extendVarSet` v' }
+ = env { um_rn_env = rn_env', um_foralls = um_foralls env `extendVarSet` v' }
where
(rn_env', v') = rnBndr2_var (um_rn_env env) v1 v2
-checkRnEnv :: UMEnv -> VarSet -> UM ()
-checkRnEnv env varset
- | isEmptyVarSet skol_vars = return ()
- | varset `disjointVarSet` skol_vars = return ()
- | otherwise = surelyApart
- where
- skol_vars = um_skols env
+mentionsForAllBoundTyVarsL, mentionsForAllBoundTyVarsR :: UMEnv -> VarSet -> Bool
+-- See (CU2) in Note [The Core unifier]
+mentionsForAllBoundTyVarsL = mentions_forall_bound_tvs inRnEnvL
+mentionsForAllBoundTyVarsR = mentions_forall_bound_tvs inRnEnvR
+
+mentions_forall_bound_tvs :: (RnEnv2 -> TyVar -> Bool) -> UMEnv -> VarSet -> Bool
+mentions_forall_bound_tvs in_rn_env env varset
+ | isEmptyVarSet (um_foralls env) = False
+ | anyVarSet (in_rn_env (um_rn_env env)) varset = True
+ | otherwise = False
-- NB: That isEmptyVarSet guard is a critical optimization;
-- it means we don't have to calculate the free vars of
-- the type, often saving quite a bit of allocation.
@@ -1891,325 +2369,3 @@ pushRefl co =
, fco_kind = mkNomReflCo (varType tv)
, fco_body = mkReflCo r ty })
_ -> Nothing
-
-{-
-************************************************************************
-* *
- Flattening
-* *
-************************************************************************
-
-Note [Flattening type-family applications when matching instances]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-As described in "Closed type families with overlapping equations"
-http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf
-we need to flatten core types before unifying them, when checking for "surely-apart"
-against earlier equations of a closed type family.
-Flattening means replacing all top-level uses of type functions with
-fresh variables, *taking care to preserve sharing*. That is, the type
-(Either (F a b) (F a b)) should flatten to (Either c c), never (Either
-c d).
-
-Here is a nice example of why it's all necessary:
-
- type family F a b where
- F Int Bool = Char
- F a b = Double
- type family G a -- open, no instances
-
-How do we reduce (F (G Float) (G Float))? The first equation clearly doesn't match,
-while the second equation does. But, before reducing, we must make sure that the
-target can never become (F Int Bool). Well, no matter what G Float becomes, it
-certainly won't become *both* Int and Bool, so indeed we're safe reducing
-(F (G Float) (G Float)) to Double.
-
-This is necessary not only to get more reductions (which we might be
-willing to give up on), but for substitutivity. If we have (F x x), we
-can see that (F x x) can reduce to Double. So, it had better be the
-case that (F blah blah) can reduce to Double, no matter what (blah)
-is! Flattening as done below ensures this.
-
-We also use this flattening operation to check for class instances.
-If we have
- instance C (Maybe b)
- instance {-# OVERLAPPING #-} C (Maybe Bool)
- [W] C (Maybe (F a))
-we want to know that the second instance might match later. So we
-flatten the (F a) in the target before trying to unify with instances.
-(This is done in GHC.Core.InstEnv.lookupInstEnv'.)
-
-The algorithm works by building up a TypeMap TyVar, mapping
-type family applications to fresh variables. This mapping must
-be threaded through all the function calls, as any entry in
-the mapping must be propagated to all future nodes in the tree.
-
-The algorithm also must track the set of in-scope variables, in
-order to make fresh variables as it flattens. (We are far from a
-source of fresh Uniques.) See Wrinkle 2, below.
-
-There are wrinkles, of course:
-
-1. The flattening algorithm must account for the possibility
- of inner `forall`s. (A `forall` seen here can happen only
- because of impredicativity. However, the flattening operation
- is an algorithm in Core, which is impredicative.)
- Suppose we have (forall b. F b) -> (forall b. F b). Of course,
- those two bs are entirely unrelated, and so we should certainly
- not flatten the two calls F b to the same variable. Instead, they
- must be treated separately. We thus carry a substitution that
- freshens variables; we must apply this substitution (in
- `coreFlattenTyFamApp`) before looking up an application in the environment.
- Note that the range of the substitution contains only TyVars, never anything
- else.
-
- For the sake of efficiency, we only apply this substitution when absolutely
- necessary. Namely:
-
- * We do not perform the substitution at all if it is empty.
- * We only need to worry about the arguments of a type family that are within
- the arity of said type family, so we can get away with not applying the
- substitution to any oversaturated type family arguments.
- * Importantly, we do /not/ achieve this substitution by recursively
- flattening the arguments, as this would be wrong. Consider `F (G a)`,
- where F and G are type families. We might decide that `F (G a)` flattens
- to `beta`. Later, the substitution is non-empty (but does not map `a`) and
- so we flatten `G a` to `gamma` and try to flatten `F gamma`. Of course,
- `F gamma` is unknown, and so we flatten it to `delta`, but it really
- should have been `beta`! Argh!
-
- Moral of the story: instead of flattening the arguments, just substitute
- them directly.
-
-2. There are two different reasons we might add a variable
- to the in-scope set as we work:
-
- A. We have just invented a new flattening variable.
- B. We have entered a `forall`.
-
- Annoying here is that in-scope variable source (A) must be
- threaded through the calls. For example, consider (F b -> forall c. F c).
- Suppose that, when flattening F b, we invent a fresh variable c.
- Now, when we encounter (forall c. F c), we need to know c is already in
- scope so that we locally rename c to c'. However, if we don't thread through
- the in-scope set from one argument of (->) to the other, we won't know this
- and might get very confused.
-
- In contrast, source (B) increases only as we go deeper, as in-scope sets
- normally do. However, even here we must be careful. The TypeMap TyVar that
- contains mappings from type family applications to freshened variables will
- be threaded through both sides of (forall b. F b) -> (forall b. F b). We
- thus must make sure that the two `b`s don't get renamed to the same b1. (If
- they did, then looking up `F b1` would yield the same flatten var for
- each.) So, even though `forall`-bound variables should really be in the
- in-scope set only when they are in scope, we retain these variables even
- outside of their scope. This ensures that, if we encounter a fresh
- `forall`-bound b, we will rename it to b2, not b1. Note that keeping a
- larger in-scope set than strictly necessary is always OK, as in-scope sets
- are only ever used to avoid collisions.
-
- Sadly, the freshening substitution described in (1) really mustn't bind
- variables outside of their scope: note that its domain is the *unrenamed*
- variables. This means that the substitution gets "pushed down" (like a
- reader monad) while the in-scope set gets threaded (like a state monad).
- Because a Subst contains its own in-scope set, we don't carry a Subst;
- instead, we just carry a TvSubstEnv down, tying it to the InScopeSet
- traveling separately as necessary.
-
-3. Consider `F ty_1 ... ty_n`, where F is a type family with arity k:
-
- type family F ty_1 ... ty_k :: res_k
-
- It's tempting to just flatten `F ty_1 ... ty_n` to `alpha`, where alpha is a
- flattening skolem. But we must instead flatten it to
- `alpha ty_(k+1) ... ty_n`—that is, by only flattening up to the arity of the
- type family.
-
- Why is this better? Consider the following concrete example from #16995:
-
- type family Param :: Type -> Type
-
- type family LookupParam (a :: Type) :: Type where
- LookupParam (f Char) = Bool
- LookupParam x = Int
-
- foo :: LookupParam (Param ())
- foo = 42
-
- In order for `foo` to typecheck, `LookupParam (Param ())` must reduce to
- `Int`. But if we flatten `Param ()` to `alpha`, then GHC can't be sure if
- `alpha` is apart from `f Char`, so it won't fall through to the second
- equation. But since the `Param` type family has arity 0, we can instead
- flatten `Param ()` to `alpha ()`, about which GHC knows with confidence is
- apart from `f Char`, permitting the second equation to be reached.
-
- Not only does this allow more programs to be accepted, it's also important
- for correctness. Not doing this was the root cause of the Core Lint error
- in #16995.
-
-flattenTys is defined here because of module dependencies.
--}
-
-data FlattenEnv
- = FlattenEnv { fe_type_map :: TypeMap (TyVar, TyCon, [Type])
- -- domain: exactly-saturated type family applications
- -- range: (fresh variable, type family tycon, args)
- , fe_in_scope :: InScopeSet }
- -- See Note [Flattening type-family applications when matching instances]
-
-emptyFlattenEnv :: InScopeSet -> FlattenEnv
-emptyFlattenEnv in_scope
- = FlattenEnv { fe_type_map = emptyTypeMap
- , fe_in_scope = in_scope }
-
-updateInScopeSet :: FlattenEnv -> (InScopeSet -> InScopeSet) -> FlattenEnv
-updateInScopeSet env upd = env { fe_in_scope = upd (fe_in_scope env) }
-
-flattenTys :: Traversable f => InScopeSet -> f Type -> f Type
--- See Note [Flattening type-family applications when matching instances]
-flattenTys = \ in_scope tys -> fst (flattenTysX in_scope tys)
-{-# INLINE flattenTys #-}
-
-flattenTysX :: Traversable f => InScopeSet -> f Type -> (f Type, TyVarEnv (TyCon, [Type]))
--- See Note [Flattening type-family applications when matching instances]
--- NB: the returned types mention the fresh type variables
--- in the domain of the returned env, whose range includes
--- the original type family applications. Building a substitution
--- from this information and applying it would yield the original
--- types -- almost. The problem is that the original type might
--- have something like (forall b. F a b); the returned environment
--- can't really sensibly refer to that b. So it may include a locally-
--- bound tyvar in its range. Currently, the only usage of this env't
--- checks whether there are any meta-variables in it
--- (in GHC.Tc.Solver.Monad.mightEqualLater), so this is all OK.
-flattenTysX in_scope tys
- = let (env, result) = coreFlattenTys emptyTvSubstEnv (emptyFlattenEnv in_scope) tys in
- (result, build_env (fe_type_map env))
- where
- build_env :: TypeMap (TyVar, TyCon, f Type) -> TyVarEnv (TyCon, f Type)
- build_env env_in
- = foldTM (\(tv, tc, tys) env_out -> extendVarEnv env_out tv (tc, tys))
- env_in emptyVarEnv
-{-# SPECIALIZE flattenTysX :: InScopeSet -> [Type] -> ([Type], TyVarEnv (TyCon, [Type])) #-}
-
-coreFlattenTys :: Traversable f => TvSubstEnv -> FlattenEnv
- -> f Type -> (FlattenEnv, f Type)
-coreFlattenTys = mapAccumL . coreFlattenTy
-{-# INLINE coreFlattenTys #-}
-
-coreFlattenTy :: TvSubstEnv -> FlattenEnv
- -> Type -> (FlattenEnv, Type)
-coreFlattenTy subst = go
- where
- go env ty | Just ty' <- coreView ty = go env ty'
-
- go env (TyVarTy tv)
- | Just ty <- lookupVarEnv subst tv = (env, ty)
- | otherwise = let (env', ki) = go env (tyVarKind tv) in
- (env', mkTyVarTy $ setTyVarKind tv ki)
- go env (AppTy ty1 ty2) = let (env1, ty1') = go env ty1
- (env2, ty2') = go env1 ty2 in
- (env2, AppTy ty1' ty2')
- go env (TyConApp tc tys)
- -- NB: Don't just check if isFamilyTyCon: this catches *data* families,
- -- which are generative and thus can be preserved during flattening
- | not (isGenerativeTyCon tc Nominal)
- = coreFlattenTyFamApp subst env tc tys
-
- | otherwise
- = let (env', tys') = coreFlattenTys subst env tys in
- (env', mkTyConApp tc tys')
-
- go env ty@(FunTy { ft_mult = mult, ft_arg = ty1, ft_res = ty2 })
- = let (env1, ty1') = go env ty1
- (env2, ty2') = go env1 ty2
- (env3, mult') = go env2 mult in
- (env3, ty { ft_mult = mult', ft_arg = ty1', ft_res = ty2' })
-
- go env (ForAllTy (Bndr tv vis) ty)
- = let (env1, subst', tv') = coreFlattenVarBndr subst env tv
- (env2, ty') = coreFlattenTy subst' env1 ty in
- (env2, ForAllTy (Bndr tv' vis) ty')
-
- go env ty@(LitTy {}) = (env, ty)
-
- go env (CastTy ty co)
- = let (env1, ty') = go env ty
- (env2, co') = coreFlattenCo subst env1 co in
- (env2, CastTy ty' co')
-
- go env (CoercionTy co)
- = let (env', co') = coreFlattenCo subst env co in
- (env', CoercionTy co')
-
-
--- when flattening, we don't care about the contents of coercions.
--- so, just return a fresh variable of the right (flattened) type
-coreFlattenCo :: TvSubstEnv -> FlattenEnv
- -> Coercion -> (FlattenEnv, Coercion)
-coreFlattenCo subst env co
- = (env2, mkCoVarCo covar)
- where
- (env1, kind') = coreFlattenTy subst env (coercionType co)
- covar = mkFlattenFreshCoVar (fe_in_scope env1) kind'
- -- Add the covar to the FlattenEnv's in-scope set.
- -- See Note [Flattening type-family applications when matching instances], wrinkle 2A.
- env2 = updateInScopeSet env1 (flip extendInScopeSet covar)
-
-coreFlattenVarBndr :: TvSubstEnv -> FlattenEnv
- -> TyCoVar -> (FlattenEnv, TvSubstEnv, TyVar)
-coreFlattenVarBndr subst env tv
- = (env2, subst', tv')
- where
- -- See Note [Flattening type-family applications when matching instances], wrinkle 2B.
- kind = varType tv
- (env1, kind') = coreFlattenTy subst env kind
- tv' = uniqAway (fe_in_scope env1) (setVarType tv kind')
- subst' = extendVarEnv subst tv (mkTyVarTy tv')
- env2 = updateInScopeSet env1 (flip extendInScopeSet tv')
-
-coreFlattenTyFamApp :: TvSubstEnv -> FlattenEnv
- -> TyCon -- type family tycon
- -> [Type] -- args, already flattened
- -> (FlattenEnv, Type)
-coreFlattenTyFamApp tv_subst env fam_tc fam_args
- = case lookupTypeMap type_map fam_ty of
- Just (tv, _, _) -> (env', mkAppTys (mkTyVarTy tv) leftover_args')
- Nothing ->
- let tyvar_name = mkFlattenFreshTyName fam_tc
- tv = uniqAway in_scope $
- mkTyVar tyvar_name (typeKind fam_ty)
-
- ty' = mkAppTys (mkTyVarTy tv) leftover_args'
- env'' = env' { fe_type_map = extendTypeMap type_map fam_ty
- (tv, fam_tc, sat_fam_args)
- , fe_in_scope = extendInScopeSet in_scope tv }
- in (env'', ty')
- where
- arity = tyConArity fam_tc
- tcv_subst = Subst (fe_in_scope env) emptyIdSubstEnv tv_subst emptyVarEnv
- (sat_fam_args, leftover_args) = assert (arity <= length fam_args) $
- splitAt arity fam_args
- -- Apply the substitution before looking up an application in the
- -- environment. See Note [Flattening type-family applications when matching instances],
- -- wrinkle 1.
- -- NB: substTys short-cuts the common case when the substitution is empty.
- sat_fam_args' = substTys tcv_subst sat_fam_args
- (env', leftover_args') = coreFlattenTys tv_subst env leftover_args
- -- `fam_tc` may be over-applied to `fam_args` (see
- -- Note [Flattening type-family applications when matching instances]
- -- wrinkle 3), so we split it into the arguments needed to saturate it
- -- (sat_fam_args') and the rest (leftover_args')
- fam_ty = mkTyConApp fam_tc sat_fam_args'
- FlattenEnv { fe_type_map = type_map
- , fe_in_scope = in_scope } = env'
-
-mkFlattenFreshTyName :: Uniquable a => a -> Name
-mkFlattenFreshTyName unq
- = mkSysTvName (getUnique unq) (fsLit "flt")
-
-mkFlattenFreshCoVar :: InScopeSet -> Kind -> CoVar
-mkFlattenFreshCoVar in_scope kind
- = let uniq = unsafeGetFreshLocalUnique in_scope
- name = mkSystemVarName uniq (fsLit "flc")
- in mkCoVar name kind
-
diff --git a/compiler/GHC/Runtime/Heap/Inspect.hs b/compiler/GHC/Runtime/Heap/Inspect.hs
index 0bac82d34cd4e19235fbb09dfe1977124c4b0244..68a52079f794090d7628b4a68f3286b59ab9919b 100644
--- a/compiler/GHC/Runtime/Heap/Inspect.hs
+++ b/compiler/GHC/Runtime/Heap/Inspect.hs
@@ -1129,7 +1129,7 @@ findPtrTyss i tys = foldM step (i, []) tys
-- The types can contain skolem type variables, which need to be treated as normal vars.
-- In particular, we want them to unify with things.
improveRTTIType :: HscEnv -> RttiType -> RttiType -> Maybe Subst
-improveRTTIType _ base_ty new_ty = U.tcUnifyTyKi base_ty new_ty
+improveRTTIType _ base_ty new_ty = U.tcUnifyDebugger base_ty new_ty
getDataConArgTys :: DataCon -> Type -> TR [Type]
-- Given the result type ty of a constructor application (D a b c :: ty)
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index cdf14f1071958586f54f15a9dfd94206cc29cb5f..742d3f4e7050fb832a2d1a905a4dba0d5b6ab800 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -2240,7 +2240,8 @@ mkDictErr ctxt orig_items
-- and the result of evaluating ...".
mk_dict_err :: HasCallStack => SolverReportErrCtxt -> (ErrorItem, ClsInstLookupResult)
-> TcM ( TcSolverReportMsg, ([ImportError], [GhcHint]) )
-mk_dict_err ctxt (item, (matches, pot_unifiers, unsafe_overlapped)) = case (NE.nonEmpty matches, NE.nonEmpty unsafe_overlapped) of
+mk_dict_err ctxt (item, (matches, pot_unifiers, unsafe_overlapped))
+ = case (NE.nonEmpty matches, NE.nonEmpty unsafe_overlapped) of
(Nothing, _) -> do -- No matches but perhaps several unifiers
{ (_, rel_binds, item) <- relevantBindings True ctxt item
; candidate_insts <- get_candidate_instances
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index ed369077ce73eaf3c63f7356bbce56c767a8f6a5..20ed7dc620dbfdcbeab08d6560242d35957966f2 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -1177,7 +1177,7 @@ tcDataConPat (L con_span con_name) data_con pat_ty_scaled
; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX skol_info tenv1 ex_tvs
-- Get location from monad, not from ex_tvs
-- This freshens: See Note [Freshen existentials]
- -- Why "super"? See Note [Binding when looking up instances]
+ -- Why "super"? See Note [Super skolems: binding when looking up instances]
-- in GHC.Core.InstEnv.
; let arg_tys' = substScaledTys tenv arg_tys
diff --git a/compiler/GHC/Tc/Instance/FunDeps.hs b/compiler/GHC/Tc/Instance/FunDeps.hs
index 90022dca41d4559145471a7ebea6775ac748dc30..8241e54d1ebc41cf204b5682ecf9a768d8fe53ce 100644
--- a/compiler/GHC/Tc/Instance/FunDeps.hs
+++ b/compiler/GHC/Tc/Instance/FunDeps.hs
@@ -663,19 +663,19 @@ checkFunDeps inst_envs (ClsInst { is_tvs = qtvs1, is_cls = cls
| instanceCantMatch trimmed_tcs rough_tcs2
= False
| otherwise
- = case tcUnifyTyKis bind_fn ltys1 ltys2 of
+ = case tcUnifyFunDeps qtvs ltys1 ltys2 of
Nothing -> False
Just subst
-> isNothing $ -- Bogus legacy test (#10675)
-- See Note [Bogus consistency check]
- tcUnifyTyKis bind_fn (substTysUnchecked subst rtys1) (substTysUnchecked subst rtys2)
+ tcUnifyFunDeps qtvs (substTysUnchecked subst rtys1) (substTysUnchecked subst rtys2)
where
trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs1
(ltys1, rtys1) = instFD fd cls_tvs tys1
(ltys2, rtys2) = instFD fd cls_tvs tys2
qtv_set2 = mkVarSet qtvs2
- bind_fn = matchBindFun (qtv_set1 `unionVarSet` qtv_set2)
+ qtvs = qtv_set1 `unionVarSet` qtv_set2
eq_inst i1 i2 = instanceDFunId i1 == instanceDFunId i2
-- A single instance may appear twice in the un-nubbed conflict list
diff --git a/compiler/GHC/Tc/Solver/Dict.hs b/compiler/GHC/Tc/Solver/Dict.hs
index 36ad82c083756bd846833ebedb2f4561eb8a8c02..2bb750d880d207cd5995f98e7a15398d495b11ec 100644
--- a/compiler/GHC/Tc/Solver/Dict.hs
+++ b/compiler/GHC/Tc/Solver/Dict.hs
@@ -1068,7 +1068,7 @@ Other notes:
- natural numbers
- Typeable
-* See also Note [What might equal later?] in GHC.Tc.Solver.InertSet.
+* See also Note [What might equal later?] in GHC.Tc.Utils.Unify
* The given-overlap problem is arguably not easy to appear in practice
due to our aggressive prioritization of equality solving over other
diff --git a/compiler/GHC/Tc/Solver/Equality.hs b/compiler/GHC/Tc/Solver/Equality.hs
index 67f6a4c04b767ab02a2356f3f848134395401e30..af697da65831df1e4c49d98275dbcc6cd49fce8d 100644
--- a/compiler/GHC/Tc/Solver/Equality.hs
+++ b/compiler/GHC/Tc/Solver/Equality.hs
@@ -33,7 +33,7 @@ import GHC.Core.TyCo.Rep -- cleverly decomposes types, good for completeness c
import GHC.Core.Coercion
import GHC.Core.Coercion.Axiom
import GHC.Core.Reduction
-import GHC.Core.Unify( tcUnifyTyWithTFs )
+import GHC.Core.Unify( tcUnifyTyForInjectivity )
import GHC.Core.FamInstEnv ( FamInstEnvs, FamInst(..), apartnessCheck
, lookupFamInstEnvByTyCon )
import GHC.Core
@@ -2446,10 +2446,9 @@ More details:
However, we make no attempt to detect cases like a ~ (F a, F a) and use the
same tyvar to replace F a. The constraint solver will common them up later!
- (Cf. Note [Flattening type-family applications when matching instances] in
- GHC.Core.Unify, which goes to this extra effort.) However, this is really
- a very small corner case. The investment to craft a clever, performant
- solution seems unworthwhile.
+ (Cf. Note [Apartness and type families] in GHC.Core.Unify, which goes to
+ this extra effort.) However, this is really a very small corner case. The
+ investment to craft a clever, performant solution seems unworthwhile.
(6) We often get the predicate associated with a constraint from its evidence
with ctPred. We thus must not only make sure the generated CEqCan's fields
@@ -3035,7 +3034,7 @@ improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty
do_one :: CoAxBranch -> TcS [TypeEqn]
do_one branch@(CoAxBranch { cab_tvs = branch_tvs, cab_lhs = branch_lhs_tys, cab_rhs = branch_rhs })
| let in_scope1 = in_scope `extendInScopeSetList` branch_tvs
- , Just subst <- tcUnifyTyWithTFs False in_scope1 branch_rhs rhs_ty
+ , Just subst <- tcUnifyTyForInjectivity False in_scope1 branch_rhs rhs_ty
= do { let inSubst tv = tv `elemVarEnv` getTvSubstEnv subst
unsubstTvs = filterOut inSubst branch_tvs
-- The order of unsubstTvs is important; it must be
@@ -3047,13 +3046,20 @@ improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty
-- be sure to apply the current substitution to a's kind.
-- Hence instFlexiX. #13135 was an example.
+ ; traceTcS "improve_inj_top" $
+ vcat [ text "branch_rhs" <+> ppr branch_rhs
+ , text "rhs_ty" <+> ppr rhs_ty
+ , text "subst" <+> ppr subst
+ , text "subst1" <+> ppr subst1 ]
; if apartnessCheck (substTys subst1 branch_lhs_tys) branch
- then return (mkInjectivityEqns inj_args (map (substTy subst1) branch_lhs_tys) lhs_tys)
+ then do { traceTcS "improv_inj_top1" (ppr branch_lhs_tys)
+ ; return (mkInjectivityEqns inj_args (map (substTy subst1) branch_lhs_tys) lhs_tys) }
-- NB: The fresh unification variables (from unsubstTvs) are on the left
-- See Note [Improvement orientation]
- else return [] }
+ else do { traceTcS "improve_inj_top2" empty; return [] } }
| otherwise
- = return []
+ = do { traceTcS "improve_inj_top:fail" (ppr branch_rhs $$ ppr rhs_ty $$ ppr in_scope $$ ppr branch_tvs)
+ ; return [] }
in_scope = mkInScopeSet (tyCoVarsOfType rhs_ty)
diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs
index fda755da648d1a91583c2b2c4babbb26177a87e0..6612cf260df3eb9f2a3095625ebbf903607c3c1c 100644
--- a/compiler/GHC/Tc/Solver/InertSet.hs
+++ b/compiler/GHC/Tc/Solver/InertSet.hs
@@ -1882,134 +1882,6 @@ prohibitedSuperClassSolve given_loc wanted_loc
| otherwise
= False
-{- Note [What might equal later?]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We must determine whether a Given might later equal a Wanted. We
-definitely need to account for the possibility that any metavariable
-might be arbitrarily instantiated. Yet we do *not* want
-to allow skolems in to be instantiated, as we've already rewritten
-with respect to any Givens. (We're solving a Wanted here, and so
-all Givens have already been processed.)
-
-This is best understood by example.
-
-1. C alpha ~? C Int
-
- That given certainly might match later.
-
-2. C a ~? C Int
-
- No. No new givens are going to arise that will get the `a` to rewrite
- to Int.
-
-3. C alpha[tv] ~? C Int
-
- That alpha[tv] is a TyVarTv, unifiable only with other type variables.
- It cannot equal later.
-
-4. C (F alpha) ~? C Int
-
- Sure -- that can equal later, if we learn something useful about alpha.
-
-5. C (F alpha[tv]) ~? C Int
-
- This, too, might equal later. Perhaps we have [G] F b ~ Int elsewhere.
- Or maybe we have C (F alpha[tv] beta[tv]), these unify with each other,
- and F x x = Int. Remember: returning True doesn't commit ourselves to
- anything.
-
-6. C (F a) ~? C a
-
- No, this won't match later. If we could rewrite (F a) or a, we would
- have by now. But see also Red Herring below.
-
-7. C (Maybe alpha) ~? C alpha
-
- We say this cannot equal later, because it would require
- alpha := Maybe (Maybe (Maybe ...)). While such a type can be contrived,
- we choose not to worry about it. See Note [Infinitary substitution in lookup]
- in GHC.Core.InstEnv. Getting this wrong let to #19107, tested in
- typecheck/should_compile/T19107.
-
-8. C cbv ~? C Int
- where cbv = F a
-
- The cbv is a cycle-breaker var which stands for F a. See
- Note [Type equality cycles] in GHC.Tc.Solver.Equality
- This is just like case 6, and we say "no". Saying "no" here is
- essential in getting the parser to type-check, with its use of DisambECP.
-
-9. C cbv ~? C Int
- where cbv = F alpha
-
- Here, we might indeed equal later. Distinguishing between
- this case and Example 8 is why we need the InertSet in mightEqualLater.
-
-10. C (F alpha, Int) ~? C (Bool, F alpha)
-
- This cannot equal later, because F a would have to equal both Bool and
- Int.
-
-To deal with type family applications, we use the Core flattener. See
-Note [Flattening type-family applications when matching instances] in GHC.Core.Unify.
-The Core flattener replaces all type family applications with
-fresh variables. The next question: should we allow these fresh
-variables in the domain of a unifying substitution?
-
-A type family application that mentions only skolems (example 6) is settled:
-any skolems would have been rewritten w.r.t. Givens by now. These type family
-applications match only themselves. A type family application that mentions
-metavariables, on the other hand, can match anything. So, if the original type
-family application contains a metavariable, we use BindMe to tell the unifier
-to allow it in the substitution. On the other hand, a type family application
-with only skolems is considered rigid.
-
-This treatment fixes #18910 and is tested in
-typecheck/should_compile/InstanceGivenOverlap{,2}
-
-Red Herring
-~~~~~~~~~~~
-In #21208, we have this scenario:
-
-instance forall b. C b
-[G] C a[sk]
-[W] C (F a[sk])
-
-What should we do with that wanted? According to the logic above, the Given
-cannot match later (this is example 6), and so we use the global instance.
-But wait, you say: What if we learn later (say by a future type instance F a = a)
-that F a unifies with a? That looks like the Given might really match later!
-
-This mechanism described in this Note is *not* about this kind of situation, however.
-It is all asking whether a Given might match the Wanted *in this run of the solver*.
-It is *not* about whether a variable might be instantiated so that the Given matches,
-or whether a type instance introduced in a downstream module might make the Given match.
-The reason we care about what might match later is only about avoiding order-dependence.
-That is, we don't want to commit to a course of action that depends on seeing constraints
-in a certain order. But an instantiation of a variable and a later type instance
-don't introduce order dependency in this way, and so mightMatchLater is right to ignore
-these possibilities.
-
-Here is an example, with no type families, that is perhaps clearer:
-
-instance forall b. C (Maybe b)
-[G] C (Maybe Int)
-[W] C (Maybe a)
-
-What to do? We *might* say that the Given could match later and should thus block
-us from using the global instance. But we don't do this. Instead, we rely on class
-coherence to say that choosing the global instance is just fine, even if later we
-call a function with (a := Int). After all, in this run of the solver, [G] C (Maybe Int)
-will definitely never match [W] C (Maybe a). (Recall that we process Givens before
-Wanteds, so there is no [G] a ~ Int hanging about unseen.)
-
-Interestingly, in the first case (from #21208), the behavior changed between
-GHC 8.10.7 and GHC 9.2, with the latter behaving correctly and the former
-reporting overlapping instances.
-
-Test case: typecheck/should_compile/T21208.
-
--}
{- *********************************************************************
* *
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 7074bb37aba3ae1ea8cf14981200eddda00304ac..3dbdbcd4f9c60ce017044785923381c5947124ba 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -5087,9 +5087,10 @@ checkValidClass cls
--
-- foo2 :: a -> Int
-- default foo2 :: a -> b
- unless (isJust $ tcMatchTys [dm_phi_ty, vanilla_phi_ty]
- [vanilla_phi_ty, dm_phi_ty]) $ addErrTc $
- TcRnDefaultSigMismatch sel_id dm_ty
+ unless (isJust (tcMatchTy dm_phi_ty vanilla_phi_ty) &&
+ isJust (tcMatchTy vanilla_phi_ty dm_phi_ty)) $
+ addErrTc $
+ TcRnDefaultSigMismatch sel_id dm_ty
-- Now do an ambiguity check on the default type signature.
checkValidType ctxt (mkDefaultMethodType cls sel_id dm_spec)
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index 5f817313909b96b24a2743dc9ad1bd91e6e8a1bd..d7635cf3631827d43d36da27abd5f581d49d13c5 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -352,10 +352,9 @@ does the same thing; it shows up in module Fraction.hs.
Conclusion: when typechecking the methods in a C [a] instance, we want to
treat the 'a' as an *existential* type variable, in the sense described
-by Note [Binding when looking up instances]. That is why isOverlappableTyVar
-responds True to an InstSkol, which is the kind of skolem we use in
-tcInstDecl2.
-
+by Note [Super skolems: binding when looking up instances] in GHC.Core.InstEnv
+That is why isOverlappableTyVar responds True to an InstSkol, which is the kind
+of skolem we use in tcInstDecl2.
Note [Tricky type variable scoping]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index 5f5d1247fc552a747d39a582ee42c9adf158c570..695be54d85994c5883b72c749577dd0a342b7505 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -46,10 +46,11 @@ module GHC.Tc.Types.Constraint (
cterHasNoProblem, cterHasProblem, cterHasOnlyProblem, cterHasOnlyProblems,
cterRemoveProblem, cterHasOccursCheck, cterFromKind,
-
+ -- Equality left-hand sides, re-exported from GHC.Core.Predicate
CanEqLHS(..), canEqLHS_maybe, canTyFamEqLHS_maybe,
canEqLHSKind, canEqLHSType, eqCanEqLHS,
+ -- Holes
Hole(..), HoleSort(..), isOutOfScopeHole,
DelayedError(..), NotConcreteError(..),
@@ -286,17 +287,6 @@ data EqCt -- An equality constraint; see Note [Canonical equalities]
eq_eq_rel :: EqRel -- INVARIANT: cc_eq_rel = ctEvEqRel cc_ev
}
--- | A 'CanEqLHS' is a type that can appear on the left of a canonical
--- equality: a type variable or /exactly-saturated/ type family application.
-data CanEqLHS
- = TyVarLHS TcTyVar
- | TyFamLHS TyCon -- ^ TyCon of the family
- [Xi] -- ^ Arguments, /exactly saturating/ the family
-
-instance Outputable CanEqLHS where
- ppr (TyVarLHS tv) = ppr tv
- ppr (TyFamLHS fam_tc fam_args) = ppr (mkTyConApp fam_tc fam_args)
-
eqCtEvidence :: EqCt -> CtEvidence
eqCtEvidence = eq_ev
@@ -777,45 +767,6 @@ instance Outputable Ct where
instance Outputable EqCt where
ppr (EqCt { eq_ev = ev }) = ppr ev
------------------------------------
--- | Is a type a canonical LHS? That is, is it a tyvar or an exactly-saturated
--- type family application?
--- Does not look through type synonyms.
-canEqLHS_maybe :: Xi -> Maybe CanEqLHS
-canEqLHS_maybe xi
- | Just tv <- getTyVar_maybe xi
- = Just $ TyVarLHS tv
-
- | otherwise
- = canTyFamEqLHS_maybe xi
-
-canTyFamEqLHS_maybe :: Xi -> Maybe CanEqLHS
-canTyFamEqLHS_maybe xi
- | Just (tc, args) <- tcSplitTyConApp_maybe xi
- , isTypeFamilyTyCon tc
- , args `lengthIs` tyConArity tc
- = Just $ TyFamLHS tc args
-
- | otherwise
- = Nothing
-
--- | Convert a 'CanEqLHS' back into a 'Type'
-canEqLHSType :: CanEqLHS -> TcType
-canEqLHSType (TyVarLHS tv) = mkTyVarTy tv
-canEqLHSType (TyFamLHS fam_tc fam_args) = mkTyConApp fam_tc fam_args
-
--- | Retrieve the kind of a 'CanEqLHS'
-canEqLHSKind :: CanEqLHS -> TcKind
-canEqLHSKind (TyVarLHS tv) = tyVarKind tv
-canEqLHSKind (TyFamLHS fam_tc fam_args) = piResultTys (tyConKind fam_tc) fam_args
-
--- | Are two 'CanEqLHS's equal?
-eqCanEqLHS :: CanEqLHS -> CanEqLHS -> Bool
-eqCanEqLHS (TyVarLHS tv1) (TyVarLHS tv2) = tv1 == tv2
-eqCanEqLHS (TyFamLHS fam_tc1 fam_args1) (TyFamLHS fam_tc2 fam_args2)
- = tcEqTyConApps fam_tc1 fam_args1 fam_tc2 fam_args2
-eqCanEqLHS _ _ = False
-
{-
************************************************************************
* *
diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index 1e5da18eaa4731841c670b43b55652fdfae553f3..8dd25bbc2b56c8b54572e5442e603ae1c78e0818 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/compiler/GHC/Tc/Utils/Instantiate.hs
@@ -580,7 +580,7 @@ tcSkolDFunType dfun_ty
; (subst, inst_tvs) <- tcInstSuperSkolTyVars skol_info tvs
-- We instantiate the dfun_tyd with superSkolems.
-- See Note [Subtle interaction of recursion and overlap]
- -- and Note [Binding when looking up instances]
+ -- and Note [Super skolems: binding when looking up instances]
; let inst_tys = substTys subst tys
skol_info_anon = mkClsInstSkol cls inst_tys }
@@ -591,7 +591,7 @@ tcSuperSkolTyVars :: TcLevel -> SkolemInfo -> [TyVar] -> (Subst, [TcTyVar])
-- Make skolem constants, but do *not* give them new names, as above
-- As always, allocate them one level in
-- Moreover, make them "super skolems"; see GHC.Core.InstEnv
--- Note [Binding when looking up instances]
+-- Note [Super skolems: binding when looking up instances]
-- See Note [Kind substitution when instantiating]
-- Precondition: tyvars should be ordered by scoping
tcSuperSkolTyVars tc_lvl skol_info = mapAccumL do_one emptySubst
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 091701a7caf0c44684a9c43809d2475556ac0a04..2f0bae22c00b228be0961c40b5ab80c4027a15de 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -606,7 +606,8 @@ data TcTyVarDetails
-- how this level number is used
Bool -- True <=> this skolem type variable can be overlapped
-- when looking up instances
- -- See Note [Binding when looking up instances] in GHC.Core.InstEnv
+ -- See Note [Super skolems: binding when looking up instances]
+ -- in GHC.Core.InstEnv
| RuntimeUnk -- Stands for an as-yet-unknown type in the GHCi
-- interactive context
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index bfcc700b8395e8731ebd898fb26fd8dc81207126..839ad4f54f4620e795bf987fef0ebc316f34d431 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -112,7 +112,6 @@ import GHC.Driver.DynFlags
import GHC.Data.Bag
import GHC.Data.FastString
import GHC.Data.Maybe (firstJusts)
-import GHC.Data.Pair
import Control.Monad
import Data.Functor.Identity (Identity(..))
@@ -4139,6 +4138,154 @@ makeTypeConcrete occ_fs conc_orig ty =
orig = case conc_orig of
ConcreteFRR frr_orig -> FRROrigin frr_orig
+
+{- *********************************************************************
+* *
+ mightEqualLater
+* *
+********************************************************************* -}
+
+{- Note [What might equal later?]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We must determine whether a Given might later equal a Wanted:
+ see Note [Instance and Given overlap] in GHC.Tc.Solver.Dict
+
+We definitely need to account for the possibility that any metavariable might be
+arbitrarily instantiated. Yet we do *not* want to allow skolems to be
+instantiated, as we've already rewritten with respect to any Givens. (We're
+solving a Wanted here, and so all Givens have already been processed.)
+
+This is best understood by example.
+
+1. C alpha[tau] ~? C Int
+
+ That Given certainly might match later.
+
+2. C a[sk] ~? C Int
+
+ No. No new givens are going to arise that will get the `a` to rewrite
+ to Int. Example:
+ f :: forall a. C a => blah
+ f = rhs -- Gives rise to [W] C Int
+ It would be silly to fail to solve ([W] C Int), just because we have
+ ([G] C a) in the Givens!
+
+3. C alpha[tv] ~? C Int
+
+ In this variant of (1) that alpha[tv] is a TyVarTv, unifiable only with
+ other type /variables/. It cannot equal Int later.
+
+4. C (F alpha[tau]) ~? C Int
+
+ Sure -- that can equal later, if we learn something useful about alpha.
+
+5. C (F alpha[tv]) ~? C Int
+
+ This, too, might equal later. Perhaps we have [G] F b ~ Int elsewhere.
+ Or maybe we have C (F alpha[tv] beta[tv]), these unify with each other,
+ and F x x = Int. Remember: returning True doesn't commit ourselves to
+ anything.
+
+6. C (F a[sk]) ~? C Int. For example
+ f :: forall a. C (F a) => blah
+ f = rhs -- Gives rise to [W] C Int
+
+ No, this won't match later. If we could rewrite (F a), we would
+ have by now. But see also Red Herring below.
+
+ This arises in instance decls too. For example in GHC.Core.Ppr we see
+ instance Outputable (XTickishId pass)
+ => Outputable (GenTickish pass) where
+ If we have [W] Outputable Int in the body, we don't want to fail to solve
+ it because (XTickishId pass) might simplify to Int.
+
+7. C (Maybe alpha[tau]) ~? C alpha[tau]
+
+ We say this cannot equal later, because it would require
+ alpha := Maybe (Maybe (Maybe ...)). While such a type can be contrived,
+ we choose not to worry about it. See Note [Infinitary substitution in lookup]
+ in GHC.Core.InstEnv. Getting this wrong led to #19107, tested in
+ typecheck/should_compile/T19107.
+
+8. C alpha[cbv] ~? C Int
+ where alpha[cbv] = F a
+
+ The alpha[cbv] is a cycle-breaker var which stands for F a. See
+ Note [Type equality cycles] in GHC.Tc.Solver.Equality
+ This is just like case 6, and we say "no". Saying "no" here is
+ essential in getting the parser to type-check, with its use of DisambECP.
+
+9. C alpha[cbv] ~? C Int
+ where alpha[cbv] = F beta[tau]
+
+ Here, we might indeed equal later. Distinguishing between
+ this case and Example 8 is why we need the InertSet in mightEqualLater.
+
+10. C (F alpha[tau], Int) ~? C (Bool, F alpha[tau])
+
+ This cannot equal later, because F alpha would have to equal both Bool and
+ Int.
+
+To deal with type family applications, we use the "fine-grained" Core unifier.
+See Note [Apartness and type families] in GHC.Core.Unify, controlled
+by the `bind_fam :: BindFamFun` function defined in `mightEqualLater`.
+
+One tricky point: a type family application that mentions only skolems (example
+6) is settled: any skolems would have been rewritten w.r.t. Givens by now. These
+type family applications match only themselves. However: a type family
+application that mentions metavariables, on the other hand, can match
+anything. So, if the original type family application contains a metavariable,
+we use BindMe to tell the unifier to allow it in the substitution. On the other
+hand, a type family application with only skolems is considered rigid. See the
+use of `mentions_meta_ty_var` in `mightEqualLater`.
+
+This treatment fixes #18910 and is tested in
+typecheck/should_compile/InstanceGivenOverlap{,2}
+
+Red Herring
+~~~~~~~~~~~
+In #21208, we have this scenario:
+
+ instance forall b. C b
+ [G] C a[sk]
+ [W] C (F a[sk])
+
+What should we do with that wanted? According to the logic above, the Given
+cannot match later (this is example 6), and so we use the global instance.
+But wait, you say: What if we learn later (say by a future type instance F a = a)
+that F a unifies with a? That looks like the Given might really match later!
+
+This mechanism described in this Note is *not* about this kind of situation, however.
+It is all asking whether a Given might match the Wanted *in this run of the solver*.
+It is *not* about whether a variable might be instantiated so that the Given matches,
+or whether a type instance introduced in a downstream module might make the Given match.
+The reason we care about what might match later is only about avoiding order-dependence.
+That is, we don't want to commit to a course of action that depends on seeing constraints
+in a certain order. But an instantiation of a variable and a later type instance
+don't introduce order dependency in this way, and so mightMatchLater is right to ignore
+these possibilities.
+
+Here is an example, with no type families, that is perhaps clearer:
+
+ instance forall b. C (Maybe b)
+ [G] C (Maybe Int)
+ [W] C (Maybe a)
+
+What to do? We *might* say that the Given could match later and should thus block
+us from using the global instance. But we don't do this. Instead, we rely on class
+coherence to say that choosing the global instance is just fine, even if later we
+call a function with (a := Int). After all, in this run of the solver, [G] C (Maybe Int)
+will definitely never match [W] C (Maybe a). (Recall that we process Givens before
+Wanteds, so there is no [G] a ~ Int hanging about unseen.)
+
+Interestingly, in the first case (from #21208), the behavior changed between
+GHC 8.10.7 and GHC 9.2, with the latter behaving correctly and the former
+reporting overlapping instances.
+
+Test case: typecheck/should_compile/T21208.
+
+-}
+
--------------------------------------------------------------------------------
-- mightEqualLater
@@ -4150,7 +4297,7 @@ mightEqualLater inert_set given_pred given_loc wanted_pred wanted_loc
= Nothing
| otherwise
- = case tcUnifyTysFG bind_fun [flattened_given] [flattened_wanted] of
+ = case tcUnifyTysFG bind_fam bind_tv [given_pred] [wanted_pred] of
Unifiable subst
-> Just subst
MaybeApart reason subst
@@ -4161,31 +4308,21 @@ mightEqualLater inert_set given_pred given_loc wanted_pred wanted_loc
SurelyApart -> Nothing
where
- in_scope = mkInScopeSet $ tyCoVarsOfTypes [given_pred, wanted_pred]
-
- -- NB: flatten both at the same time, so that we can share mappings
- -- from type family applications to variables, and also to guarantee
- -- that the fresh variables are really fresh between the given and
- -- the wanted. Flattening both at the same time is needed to get
- -- Example 10 from the Note.
- (Pair flattened_given flattened_wanted, var_mapping)
- = flattenTysX in_scope (Pair given_pred wanted_pred)
-
- bind_fun :: BindFun
- bind_fun tv rhs_ty
+ bind_tv :: BindTvFun
+ bind_tv tv rhs_ty
| MetaTv { mtv_info = info } <- tcTyVarDetails tv
- = if ok_shape tv info rhs_ty && can_unify tv rhs_ty
- then BindMe
- else Apart
-
- -- See Examples 4, 5, and 6 from the Note
- | Just (_fam_tc, fam_args) <- lookupVarEnv var_mapping tv
- , anyFreeVarsOfTypes mentions_meta_ty_var fam_args
+ , ok_shape tv info rhs_ty
+ , can_unify tv rhs_ty
= BindMe
| otherwise
- = Apart
- where
+ = DontBindMe
+
+ bind_fam :: BindFamFun
+ -- See Examples (4), (5), and (6) from the Note, especially (6)
+ bind_fam _fam_tc fam_args _rhs
+ | anyFreeVarsOfTypes mentions_meta_ty_var fam_args = BindMe
+ | otherwise = DontBindMe
can_unify :: TcTyVar -> TcType -> Bool
can_unify tv rhs_ty
@@ -4203,9 +4340,8 @@ mightEqualLater inert_set given_pred given_loc wanted_pred wanted_loc
| isMetaTyVar tv
= case metaTyVarInfo tv of
-- See Examples 8 and 9 in the Note
- CycleBreakerTv
- -> anyFreeVarsOfType mentions_meta_ty_var
- (lookupCycleBreakerVar tv inert_set)
+ CycleBreakerTv -> anyFreeVarsOfType mentions_meta_ty_var
+ (lookupCycleBreakerVar tv inert_set)
_ -> True
| otherwise
= False
@@ -4235,7 +4371,7 @@ false positives:
3. Concreteness: ty1 = kappa[conc] /~ ty2 = k[sk].
In these examples, ty1 and ty2 cannot unify; to inform the pure unifier of this
-fact, we use 'checkTyEqRhs' to provide the 'BindFun'.
+fact, we use 'checkTyEqRhs' to provide the 'BindTvFun'.
Failing to account for this caused #25744:
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 174cb33f91e3d6c02fe5c0ff777bc56101a11a9e..1d1434609fd6305b0d573f563d9f36e20d8aaf48 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -2612,7 +2612,7 @@ checkConsistentFamInst (InClsInst { ai_class = clas
-- The /scoped/ type variables from the class-instance header
-- should not be alpha-renamed. Inferred ones can be.
no_bind_set = mkVarSet inst_tvs
- bind_me tv _ty | tv `elemVarSet` no_bind_set = Apart
+ bind_me tv _ty | tv `elemVarSet` no_bind_set = DontBindMe
| otherwise = BindMe
diff --git a/compiler/GHC/Utils/Panic.hs b/compiler/GHC/Utils/Panic.hs
index 514583bb28e5f6357fccac4460c187f74694ecf7..9bfdaf095ff96607d07cc3db3e5f48b261e4de81 100644
--- a/compiler/GHC/Utils/Panic.hs
+++ b/compiler/GHC/Utils/Panic.hs
@@ -191,7 +191,7 @@ pprPanic :: HasCallStack => String -> SDoc -> a
pprPanic s doc = withFrozenCallStack $ panicDoc s (doc $$ callStackDoc)
-- | Throw an exception saying "bug in GHC"
-panicDoc :: String -> SDoc -> a
+panicDoc :: HasCallStack => String -> SDoc -> a
panicDoc x doc = throwGhcException (PprPanic x doc)
-- | Throw an exception saying "this isn't finished yet"
diff --git a/testsuite/tests/indexed-types/should_compile/T25657.hs b/testsuite/tests/indexed-types/should_compile/T25657.hs
new file mode 100644
index 0000000000000000000000000000000000000000..c63db1f36ffa6383edce92101bc16a3105f2858e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T25657.hs
@@ -0,0 +1,42 @@
+{-# language AllowAmbiguousTypes #-}
+{-# language TypeData #-}
+{-# language DataKinds, TypeFamilyDependencies #-}
+
+{- This test checks that
+ MyEq (Var A) (Var B) --> False
+ MyEq (Var A) (Var A) --> True
+
+remembering that Var is injective.
+
+To achieve this we need
+ MyEq (Var A) (Var B)
+to be apart from
+ MyEq a a
+o
+-}
+module T25657 where
+
+import Data.Kind (Type)
+import Data.Type.Equality ((:~:) (Refl))
+
+
+type Tag :: Type
+type data Tag = A | B
+
+
+type Var :: forall {k}. Tag -> k
+type family Var tag = a | a -> tag
+
+
+type MyEq :: k -> k -> Bool
+type family MyEq a b where
+ MyEq a a = 'True
+ MyEq _ _ = 'False
+
+
+true :: MyEq (Var A) (Var A) :~: 'True
+true = Refl
+
+
+false :: MyEq (Var A) (Var B) :~: 'False
+false = Refl
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index af391bd0b05eb4f6ac975eff876694a091efb44c..3f85a0b1b046092d30c47936c4cc5c0f9615ca13 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -315,3 +315,4 @@ test('T25611a', normal, compile, [''])
test('T25611b', normal, compile, [''])
test('T25611c', normal, compile, [''])
test('T25611d', normal, compile, [''])
+test('T25657', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_compile/InstanceGivenOverlap.hs b/testsuite/tests/typecheck/should_compile/InstanceGivenOverlap.hs
index 14d8717351619648927fc94f957020f7fb64c42c..ac01a64b31328daedebef3a8134ba063720c1166 100644
--- a/testsuite/tests/typecheck/should_compile/InstanceGivenOverlap.hs
+++ b/testsuite/tests/typecheck/should_compile/InstanceGivenOverlap.hs
@@ -19,5 +19,26 @@ type family F a b where
wob :: forall a b. (Q [F a b], R b a) => a -> Int
wob = undefined
-g :: forall a. Q [a] => [a] -> Int
-g x = wob x
+g :: forall c. Q [c] => [c] -> Int
+g x = wob x -- Instantiate wob @[c] @beta
+
+{- Constraint solving for g
+
+[G] Q [c]
+[W] Q [F [c] beta] -- Do NOT fire Q [x] instance
+[W] R beta [c]
+--> instance for R
+[G] Q [c]
+[W] Q [F [c] beta]
+[W] beta ~ c
+-->
+[G] Q [c]
+[W] Q [F [c] c]
+--> Eqn for F
+[G] Q [c]
+[W] Q [c]
+--> done
+
+c ~ F [c] beta
+
+-}