07 Oct '26
Simon Peyton Jones pushed to branch wip/T27828 at Glasgow Haskell Compiler / GHC
Commits:
2af96935 by Simon Peyton Jones at 2026-10-07T17:46:31+01:00
Refactor fundeps again
This MR fixes #27828; there was a bad scoping error in `trim_qtvs`.
The main changes are
* Refactor `trim_qtvs` completely to eliminate the bug.
* Remove a redundant `apartnessCheck` from `mkTopOpenFamEqFDs`.
* Lots of improvements to the Notes in FunDeps.hs
I also did a couple of pure refactors:
* I realised that we were carefully caching `cab_incomps` in each
`CoAxBranch`, to make it more efficient to reduce a type family application,
but we were not doing the same thing when computing relevance for functional
dependencies; see Note [Relevance] in GHC.Tc.Solver.FunDeps. So I added
`cab_overlaps`, which is now used in `noEarlierMatch`.
* Use a proper data types, `AmIUnifying` and `OuterKindsFlag`, for two
previously-Boolean arguments to `tc_unify_tys`. This is a pure refactor.
- - - - -
15 changed files:
- + changelog.d/T27828
- compiler/GHC/Builtin/WiredIn/Types/Box.hs
- compiler/GHC/Core/Coercion/Axiom.hs
- compiler/GHC/Core/FamInstEnv.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/Iface/Decl.hs
- compiler/GHC/Iface/Syntax.hs
- compiler/GHC/IfaceToCore.hs
- compiler/GHC/Tc/Instance/FunDeps.hs
- compiler/GHC/Tc/Solver/FunDeps.hs
- compiler/GHC/Tc/TyCl.hs
- + testsuite/tests/indexed-types/should_compile/T27828.hs
- + testsuite/tests/indexed-types/should_compile/T27828a.hs
- + testsuite/tests/indexed-types/should_compile/T27828b.hs
- testsuite/tests/indexed-types/should_compile/all.T
Changes:
=====================================
changelog.d/T27828
=====================================
@@ -0,0 +1,8 @@
+section: compiler
+synopsis: Fix a "No skolem info" compiler crash
+issues: #27828
+mrs: !16714
+
+description: {
+ There was a bug in the implementation of functional dependencies for type families.
+}
=====================================
compiler/GHC/Builtin/WiredIn/Types/Box.hs
=====================================
@@ -329,7 +329,8 @@ mkWiredInNewTyCon tc_name dc_name nt_co_uniq bndrs roles nt_fld_ty =
, cab_roles = roles
, cab_lhs = mkTyVarTys tvs
, cab_rhs = nt_fld_ty
- , cab_incomps = [] }
+ , cab_overlaps = []
+ , cab_incomps = [] }
-- | The wired-in @Box@ newtype:
--
=====================================
compiler/GHC/Core/Coercion/Axiom.hs
=====================================
@@ -18,7 +18,7 @@ module GHC.Core.Coercion.Axiom (
coAxiomSingleBranch, coAxBranchTyVars, coAxBranchCoVars,
coAxBranchRoles,
coAxBranchLHS, coAxBranchRHS, coAxBranchSpan, coAxBranchIncomps,
- placeHolderIncomps,
+ placeHolderIncomps, placeHolderOverlaps,
Role(..),
@@ -195,23 +195,44 @@ mapAccumBranches f (MkBranches arr)
Note [Storing compatibility]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-During axiom application, we need to be aware of which branches are compatible
-with which others. The full explanation is in Note [Compatibility] in
-GHc.Core.FamInstEnv. (The code is placed there to avoid a dependency from
-GHC.Core.Coercion.Axiom on the unification algorithm.) Although we could
-theoretically compute compatibility on the fly, this is silly, so we store it
-in a CoAxiom.
+A `CoAxBranch` caches some useful information in `cab_incomps` and `cab_overlaps`:
-Specifically, each branch refers to all other branches with which it is
-incompatible. This list might well be empty, and it will always be for the
-first branch of any axiom.
+* `cab_overlaps`: when computing "relevance", in the function
+ `GHC.Tc.Solver.FunDeps.getRelevantBranches`, we need to know which ealier branches
+ can match this one -- see `noEarlierMatch`.
-CoAxBranches that do not (yet) belong to a CoAxiom should have a panic thunk
-stored in cab_incomps. The incompatibilities are properly a property of the
-axiom as a whole, and they are computed only when the final axiom is built.
+ Again we could look at all earlier branches, but instead we cache in `cab_overlaps`
+ a list of all earlier branches that could overlap with this one.
-During serialization, the list is converted into a list of the indices
-of the branches.
+* `cab_incomps`: during axiom application, we need to be aware of which branches are
+ /compatible/ with which others. The full explanation is in Note [Compatibility] in
+ GHC.Core.FamInstEnv. (The code is placed there to avoid a dependency from
+ GHC.Core.Coercion.Axiom on the unification algorithm.)
+
+ Although we could readily compute compatibility on the fly, this is silly, so we
+ cache in `cab_incomps` a list of earlier branches that are /incompatible/ with
+ this one. (See Note [Compatibility] for a definition.)
+
+ Always a sub-list of `cab_overlaps`.
+
+Both lists can be empty, and always are for the first branch of any axiom.
+
+Some extra points:
+
+(SC1) A `CoAxBranch` that does not (yet) belong to a CoAxiom is initialised with panic
+ thunks, `placeHolderOverlaps` or `placeHolderIncomps`, for the two fields; see `mkCoAxBranch`.
+
+ Then, when a bunch of branches is grouped together in an axiom, we analyse the
+ branches as a whole and initialise the fields properly, using `computeAxiomIncomps`.
+ (For open type families, whose axioms have only one branch, we null out both lists
+ with `noAxiomIncomps`.)
+
+(SC2) We don't need to serialise `cab_overlaps` and `cab_incomps` into an interface
+ file, because we recompute them in `computeAxiomIncomps`. However, annoyingly,
+ the pretty printer converts to IfaceSyn before printing, and we do want to show
+ `cab_incomps` (see Note [Displaying axiom incompatibilities]). So, tiresomely,
+ `IfaceAxBranch` has a `ifaxbIncomps` field, used only for printing. For historical
+ reasons this is actually serialised. Yuk.
Note [CoAxioms are homogeneous]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -230,7 +251,9 @@ This is checked in FamInstEnv.mkCoAxBranch.
-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism] in GHC.Core.Lint
data CoAxiom br
- = CoAxiom -- Type equality axiom.
+ = -- `br` is Unbranched for each of the many axioms of an open type family
+ -- Branched for the single multi-branch axiom of a closed type family
+ CoAxiom -- Type equality axiom.
{ co_ax_unique :: Unique -- Unique identifier
, co_ax_name :: Name -- Name for pretty-printing
, co_ax_role :: Role -- Role of the axiom's equality
@@ -268,8 +291,15 @@ data CoAxBranch
, cab_rhs :: Type
-- ^ Right-hand side of the equality
-- See Note [CoAxioms are homogeneous]
+
+ , cab_overlaps :: [CoAxBranch]
+ -- ^ The preceding branches whose LHSs are /unify with/ this one
+ -- Order is unimportant
+ -- See Note [Storing compatibility]
+
, cab_incomps :: [CoAxBranch]
- -- ^ The previous incompatible branches
+ -- ^ The preceding branches that are /incompatible/ with this one
+ -- Order is unimportant
-- See Note [Storing compatibility]
}
deriving Data.Data
@@ -342,8 +372,9 @@ coAxBranchIncomps :: CoAxBranch -> [CoAxBranch]
coAxBranchIncomps = cab_incomps
-- See Note [Compatibility] in GHC.Core.FamInstEnv
-placeHolderIncomps :: [CoAxBranch]
-placeHolderIncomps = panic "placeHolderIncomps"
+placeHolderIncomps, placeHolderOverlaps :: [CoAxBranch]
+placeHolderIncomps = panic "placeHolderIncomps"
+placeHolderOverlaps = panic "placeHolderOverlaps"
{-
Note [CoAxBranch type variables]
=====================================
compiler/GHC/Core/FamInstEnv.hs
=====================================
@@ -19,7 +19,7 @@ module GHC.Core.FamInstEnv (
FamInstMatch(..),
lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon,
- isDominatedBy, apartnessCheck, compatibleBranches,
+ isDominatedBy, apartnessCheck, noEarlierMatchCheck, compatibleBranches,
-- Injectivity
InjectivityCheckResult(..),
@@ -487,20 +487,45 @@ in GHC.Core.Unify.)
Note [Compatibility]
~~~~~~~~~~~~~~~~~~~~
-Two patterns are /compatible/ if either of the following conditions hold:
-1) The patterns are apart.
-2) The patterns unify with a substitution S, and their right hand sides
-equal under that substitution.
+Consider a closed type family with two equations (X1) and (X2)
+ type family F a where
+ F lhs1 = rhs1 -- (X1)
+ ...
+ F lhs2 = rhs2 -- (X2)
+ ...
+Then equations (X1) and (X2) are /compatible/ if any target (F ty) that
+matches both equations yields the very same right hand side. Example:
+ And True True = True
+ And a True = a
+The target (And True True) matches both equations but they then both
+produce the same reduct True.
+
+More precisely (X1) and (X2) are /compatible/ iff
+ If LHSs unify with a substitution S, then S(rhs1) = S(rhs2)
+
+Conversely, (X1) and (X2) are /incompatible/ if
+ Their LHSs unify with S, and S(rhs1) /= S(rhs2)
For open type families, only compatible instances are allowed. For closed
-type families, the story is slightly more complicated. Consider the following:
+families, we use the Closed Family Matching Rule (see function `findBranch`):
-type family F a where
- F Int = Bool
- F a = Int
+ When looking up a target (F ty) in a closed type family F,
+ find an equation (branch) such that:
+ * the LHS matches the target
+ * the target is apart from every previous /incompatible/ equation for F
-g :: Show a => a -> F a
-g x = length (show x)
+We don't need to check the earlier equations that are compatible with the
+matching equation, because they are either irrelevant (clause 1 of compatible)
+or benign (clause 2 of compatible).
+
+Some examples:
+
+ type family F a where
+ F Int = Bool
+ F a = Int
+
+ g :: Show a => a -> F a
+ g x = length (show x)
Should that type-check? No. We need to allow for the possibility that 'a'
might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int
@@ -516,12 +541,12 @@ potentially-overlapping group is closed.
As another example, consider this:
-type family G x where
- G Int = Bool
- G a = Double
+ type family G x where
+ G Int = Bool
+ G a = Double
-type family H y
--- no instances
+ type family H y
+ -- no instances
Now, we want to simplify (G (H Char)). We can't, because (H Char) might later
simplify to be Int. So, (G (H Char)) is stuck, for now.
@@ -529,18 +554,13 @@ simplify to be Int. So, (G (H Char)) is stuck, for now.
While everything above is quite sound, it isn't as expressive as we'd like.
Consider this:
-type family J a where
- J Int = Int
- J a = a
+ type family J a where
+ J Int = Int
+ J a = a
Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if
b is instantiated with Int, but the RHSs coincide there, so it's all OK.
-
-So, the rule is this: when looking up a branch in a closed type family, we
-find a branch that matches the target, but then we make sure that the target
-is apart from every previous *incompatible* branch. We don't check the
-branches that are compatible with the matching branch, because they are either
-irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).
+Hence the Closed Family Matching Rule.
Note [Compatibility of eta-reduced axioms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -572,15 +592,32 @@ fails anyway.
-- See Note [Compatibility]
compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
-compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
- (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
+compatibleBranches b1 b2
+ = case compareBranches b1 b2 of
+ BC_Apart -> True
+ BC_Compat -> True
+ BC_Incompat -> False
+
+data BranchCompatibility
+ = BC_Apart -- LHSs are apart
+ | BC_Compat -- LHSs unify with S, and S(rhs1)=S(rhs2)
+ | BC_Incompat -- LHSs unify with S, and S(rhs1)/=S(rhs2)
+
+compareBranches :: CoAxBranch -> CoAxBranch -> BranchCompatibility
+compareBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
+ (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
= 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
- MaybeApart {} -> False
- Unifiable subst -> Type.substTyAddInScope subst rhs1 `eqType`
+ SurelyApart -> BC_Apart
+ Unifiable subst | Type.substTyAddInScope subst rhs1 `eqType`
Type.substTyAddInScope subst rhs2
+ -> BC_Compat
+ | otherwise
+ -> BC_Incompat
+ MaybeApart {} -> BC_Incompat
+ -- An occurs check yields MaybeApart;
+ -- see Note [Infinitary substitutions] in GHC.Core.Unify
where
(commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2
-- See Note [Compatibility of eta-reduced axioms]
@@ -603,8 +640,7 @@ injectiveBranches injectivity
ax1@(CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
ax2@(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
-- See Note [Verifying injectivity annotation], case 1.
- = case tcUnifyTysForInjectivity True [rhs1] [rhs2] of
- -- True = two-way pre-unification
+ = case tcUnifyTysForInjectivity Unifying [rhs1] [rhs2] of
Nothing -> InjectivityAccepted
-- RHS are different, so equations are injective.
-- This is case 1A from Note [Verifying injectivity annotation]
@@ -629,10 +665,11 @@ injectiveBranches injectivity
lhs1Subst = Type.substTys subst (getInjArgs lhs1)
lhs2Subst = Type.substTys subst (getInjArgs lhs2)
--- takes a CoAxiom with unknown branch incompatibilities and computes
--- the compatibilities
--- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom
computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch]
+-- Takes a CoAxiom for a closed type family that has place-holder
+-- `cab_incomps` and `cab_overlaps` fields, and computes those fields
+-- properly from the list of branches.
+-- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom
computeAxiomIncomps branches
= snd (mapAccumL go [] branches)
where
@@ -640,11 +677,23 @@ computeAxiomIncomps branches
go prev_brs cur_br
= (new_br : prev_brs, new_br)
where
- new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br }
-
- mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch]
- mk_incomps prev_brs cur_br
- = filter (not . compatibleBranches cur_br) prev_brs
+ (overlaps,incomps) = get_cab [] [] prev_brs
+ new_br = cur_br { cab_overlaps = overlaps, cab_incomps = incomps }
+
+ get_cab :: [CoAxBranch] -> [CoAxBranch] -- Accumulators
+ -> [CoAxBranch]
+ -> ([CoAxBranch], [CoAxBranch])
+ get_cab overlaps incomps [] = (overlaps,incomps)
+ get_cab overlaps incomps (br:brs)
+ = case compareBranches cur_br br of
+ BC_Apart -> get_cab overlaps incomps brs
+ BC_Compat -> get_cab (br:overlaps) incomps brs
+ BC_Incompat -> get_cab (br:overlaps) (br:incomps) brs
+
+noAxiomIncomps :: CoAxBranch -> CoAxBranch
+-- Overwrite the placeholders for `cab_incomps` and `cab_overlaps`
+-- with [], because unbranched axioms have no "preceding" equations
+noAxiomIncomps branch = branch { cab_incomps = [], cab_overlaps = [] }
{-
************************************************************************
@@ -715,14 +764,17 @@ mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
-> SrcSpan
-> CoAxBranch
mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc
- = CoAxBranch { cab_tvs = tvs'
- , cab_eta_tvs = eta_tvs'
- , cab_cvs = cvs'
- , cab_lhs = tidyTypes env lhs
- , cab_roles = roles
- , cab_rhs = tidyType env rhs
- , cab_loc = loc
- , cab_incomps = placeHolderIncomps }
+ = CoAxBranch { cab_tvs = tvs'
+ , cab_eta_tvs = eta_tvs'
+ , cab_cvs = cvs'
+ , cab_lhs = tidyTypes env lhs
+ , cab_roles = roles
+ , cab_rhs = tidyType env rhs
+ , cab_loc = loc
+
+ -- See (SC1) in Note [Storing compatibility]
+ , cab_overlaps = placeHolderOverlaps
+ , cab_incomps = placeHolderIncomps }
where
(env1, tvs') = tidyVarBndrs init_tidy_env tvs
(env2, eta_tvs') = tidyVarBndrs env1 eta_tvs
@@ -736,14 +788,16 @@ mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc
-- all of the following code is here to avoid mutual dependencies with
-- Coercion
-mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
-mkBranchedCoAxiom ax_name fam_tc branches
+mkBranchedCoAxiom :: Role -> Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
+mkBranchedCoAxiom role ax_name fam_tc branches
= CoAxiom { co_ax_unique = nameUnique ax_name
, co_ax_name = ax_name
, co_ax_tc = fam_tc
- , co_ax_role = Nominal
+ , co_ax_role = role
, co_ax_implicit = False
, co_ax_branches = manyBranches (computeAxiomIncomps branches) }
+ -- computeAxiomIncomps: see (SC1) in
+ -- Note [Storing compatibility]
mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched
mkUnbranchedCoAxiom ax_name fam_tc branch
@@ -752,7 +806,9 @@ mkUnbranchedCoAxiom ax_name fam_tc branch
, co_ax_tc = fam_tc
, co_ax_role = Nominal
, co_ax_implicit = False
- , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
+ , co_ax_branches = unbranched (noAxiomIncomps branch) }
+ -- noAxiomIncomps: see (SC1) in
+ -- Note [Storing compatibility]
mkSingleCoAxiom :: Role -> Name
-> [TyVar] -> [TyVar] -> [CoVar]
@@ -767,7 +823,9 @@ mkSingleCoAxiom role ax_name tvs eta_tvs cvs fam_tc lhs_tys rhs_ty
, co_ax_tc = fam_tc
, co_ax_role = role
, co_ax_implicit = False
- , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
+ , co_ax_branches = unbranched (noAxiomIncomps branch) }
+ -- noAxiomIncomps: see (SC1) in
+ -- Note [Storing compatibility]
where
branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty
(map (const Nominal) tvs)
@@ -785,7 +843,9 @@ mkNewTypeCoAxiom name tycon tvs roles rhs_ty
, co_ax_implicit = True -- See Note [Implicit axioms] in GHC.Core.TyCon
, co_ax_role = Representational
, co_ax_tc = tycon
- , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
+ , co_ax_branches = unbranched (noAxiomIncomps branch) }
+ -- noAxiomIncomps: see (SC1) in
+ -- Note [Storing compatibility]
where
branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty
roles (getSrcSpan name)
@@ -1223,7 +1283,9 @@ findBranch :: Array BranchIndex CoAxBranch
-> Maybe (BranchIndex, [Type], [Coercion])
-- coercions relate requested types to returned axiom LHS at role N
findBranch branches target_tys
- = foldr go Nothing (assocs branches)
+ = -- Implements the Closed Family Matching Rule
+ -- in Note [Compatibility]
+ foldr go Nothing (assocs branches)
where
go :: (BranchIndex, CoAxBranch)
-> Maybe (BranchIndex, [Type], [Coercion])
@@ -1258,6 +1320,20 @@ apartnessCheck target (CoAxBranch { cab_incomps = incomps })
isSurelyApart SurelyApart = True
isSurelyApart _ = False
+-- | Check whether an earlier branch matches these target types
+noEarlierMatchCheck
+ :: [Type]
+ -> CoAxBranch -- ^ The candidate equation we wish to use
+ -> Bool -- ^ True <=> equation can fire
+noEarlierMatchCheck target (CoAxBranch { cab_overlaps = overlaps })
+ -- NB: this is the /only/ use of the `cab_overlaps` field
+ -- See Note [Storing compatibility] and
+ -- (RW4) in Note [Relevance]
+ = not (any matches overlaps)
+ where
+ matches earlier_branch
+ = isJust (tcMatchTys (coAxBranchLHS earlier_branch) target)
+
{-
************************************************************************
* *
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -9,6 +9,7 @@ module GHC.Core.Unify (
tcMatchTyX_BM, ruleMatchTyKiX,
-- Side-effect free unification
+ AmIUnifying(..),
tcUnifyTy, tcUnifyTys, tcUnifyFunDeps, tcUnifyDebugger,
tcUnifyTysFG, tcUnifyTysForInjectivity,
BindTvFun, BindFamFun, BindFlag(..),
@@ -597,14 +598,14 @@ tcMatchTyX_BM :: HasDebugCallStack
=> BindTvFun -> Subst
-> Type -> Type -> Maybe Subst
tcMatchTyX_BM bind_tv subst ty1 ty2
- = tc_match_tys_x bind_tv False subst [ty1] [ty2]
+ = tc_match_tys_x bind_tv IgnoreOuterKinds 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 :: HasDebugCallStack => Type -> Type -> Maybe Subst
tcMatchTyKi ty1 ty2
- = tc_match_tys alwaysBindTv True [ty1] [ty2]
+ = tc_match_tys alwaysBindTv CheckOuterKinds [ty1] [ty2]
-- | This is similar to 'tcMatchTy', but extends a substitution
-- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -614,7 +615,7 @@ tcMatchTyX :: HasDebugCallStack
-> Type -- ^ Target
-> Maybe Subst
tcMatchTyX subst ty1 ty2
- = tc_match_tys_x alwaysBindTv False subst [ty1] [ty2]
+ = tc_match_tys_x alwaysBindTv IgnoreOuterKinds subst [ty1] [ty2]
-- | Like 'tcMatchTy' but over a list of types.
-- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -625,7 +626,7 @@ tcMatchTys :: HasDebugCallStack
-- variables could be free in the target
-- See (CU6) in Note [The Core unifier]
tcMatchTys tys1 tys2
- = tc_match_tys alwaysBindTv False tys1 tys2
+ = tc_match_tys alwaysBindTv IgnoreOuterKinds tys1 tys2
-- | Like 'tcMatchTyKi' but over a list of types.
-- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -635,7 +636,7 @@ tcMatchTyKis :: HasDebugCallStack
-> Maybe Subst -- ^ One-shot substitution
-- See (CU6) in Note [The Core unifier]
tcMatchTyKis tys1 tys2
- = tc_match_tys alwaysBindTv True tys1 tys2
+ = tc_match_tys alwaysBindTv CheckOuterKinds tys1 tys2
-- | Like 'tcMatchTys', but extending a substitution
-- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -645,7 +646,7 @@ tcMatchTysX :: HasDebugCallStack
-> [Type] -- ^ Target
-> Maybe Subst -- ^ One-shot substitution
tcMatchTysX subst tys1 tys2
- = tc_match_tys_x alwaysBindTv False subst tys1 tys2
+ = tc_match_tys_x alwaysBindTv IgnoreOuterKinds subst tys1 tys2
-- | Like 'tcMatchTyKis', but extending a substitution
-- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -655,12 +656,12 @@ tcMatchTyKisX :: HasDebugCallStack
-> [Type] -- ^ Target
-> Maybe Subst -- ^ One-shot substitution
tcMatchTyKisX subst tys1 tys2
- = tc_match_tys_x alwaysBindTv True subst tys1 tys2
+ = tc_match_tys_x alwaysBindTv CheckOuterKinds subst tys1 tys2
-- | Same as tc_match_tys_x, but starts with an empty substitution
tc_match_tys :: HasDebugCallStack
=> BindTvFun
- -> Bool -- ^ match kinds?
+ -> OuterKindsFlag -- ^ Match kinds?
-> [Type]
-> [Type]
-> Maybe Subst
@@ -672,7 +673,7 @@ tc_match_tys bind_me match_kis tys1 tys2
-- | Worker for 'tcMatchTysX' and 'tcMatchTyKisX'
tc_match_tys_x :: HasDebugCallStack
=> BindTvFun
- -> Bool -- ^ match kinds?
+ -> OuterKindsFlag -- ^ Match kinds?
-> Subst
-> [Type]
-> [Type]
@@ -680,8 +681,8 @@ tc_match_tys_x :: HasDebugCallStack
tc_match_tys_x bind_tv match_kis (Subst in_scope id_env tv_env cv_env) tys1 tys2
= case tc_unify_tys neverBindFam -- (ATF7) in Note [Apartness and type families]
bind_tv
- False -- Matching, not unifying
- False -- Not an injectivity check
+ Matching -- Matching, not unifying
+ False -- Not an injectivity check
match_kis
RespectMultiplicities
(mkRnEnv2 in_scope) tv_env cv_env tys1 tys2 of
@@ -706,9 +707,9 @@ ruleMatchTyKiX tmpl_tvs rn_env tenv tmpl target
-- 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
+ Matching -- Matching, not unifying
False -- No doing an injectivity check
- True -- Match the kinds
+ CheckOuterKinds -- Match the kinds
IgnoreMultiplicities
-- See Note [Rewrite rules ignore multiplicities in FunTy]
rn_env tenv emptyCvSubstEnv [tmpl] [target] of
@@ -784,7 +785,7 @@ tcUnifyTy t1 t2 = tcUnifyTys alwaysBindTv [t1] [t2]
tcUnifyDebugger :: Type -> Type -> Maybe Subst
tcUnifyDebugger t1 t2
= case tc_unify_tys_fg
- True -- Unify kinds
+ CheckOuterKinds -- Unify kinds
neverBindFam -- Does not affect Unifiable, so pick max efficient
-- See (ATF8) in Note [Apartness and type families]
alwaysBindTv
@@ -798,7 +799,7 @@ tcUnifyFunDeps :: TyCoVarSet
-> Maybe Subst
tcUnifyFunDeps qtvs tys1 tys2
= case tc_unify_tys_fg
- True -- Unify kinds
+ CheckOuterKinds -- Unify kinds
dontCareBindFam -- Class-instance heads never mention type families
(matchBindTv qtvs)
tys1 tys2 of
@@ -821,7 +822,7 @@ tcUnifyTysForInjectivity unif tys1 tys2
= case tc_unify_tys alwaysBindFam alwaysBindTv
unif -- Am I unifying?
True -- Do injectivity checks
- False -- Don't check outermost kinds
+ IgnoreOuterKinds -- Don't check outermost kinds
RespectMultiplicities
rn_env emptyTvSubstEnv emptyCvSubstEnv
tys1 tys2 of
@@ -838,8 +839,9 @@ tcUnifyTysForInjectivity unif tys1 tys2
-- should never actually be done
maybe_fix tv_subst
- | unif = niFixSubst in_scope tv_subst
- | otherwise = mkTvSubst in_scope tv_subst
+ = case unif of
+ Unifying -> niFixSubst in_scope tv_subst
+ Matching -> mkTvSubst in_scope tv_subst
-- When matching, don't confuse domain with range; no fixpoint!
-----------------
@@ -866,15 +868,15 @@ tcUnifyTysFG :: BindFamFun -> BindTvFun
-> [Type] -> [Type]
-> UnifyResult
tcUnifyTysFG bind_fam bind_tv tys1 tys2
- = tc_unify_tys_fg False bind_fam bind_tv tys1 tys2
+ = tc_unify_tys_fg IgnoreOuterKinds bind_fam bind_tv tys1 tys2
-tc_unify_tys_fg :: Bool
+tc_unify_tys_fg :: OuterKindsFlag
-> 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
+ Unifying
False -- Not doing an injectivity check
match_kis -- Match outer kinds
RespectMultiplicities rn_env
@@ -888,10 +890,10 @@ tc_unify_tys_fg match_kis bind_fam bind_tv tys1 tys2
-- | 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
+ -> AmIUnifying -- ^ Unifying or matching
+ -> Bool -- ^ True <=> doing an injectivity check
+ -> OuterKindsFlag -- ^ Check outer kinds or not
+ -> MultiplicityFlag -- ^ see Note [Rewrite rules ignore multiplicities in FunTy] in GHC.Core.Unify
-> RnEnv2
-> TvSubstEnv -- ^ substitution to extend
-> CvSubstEnv
@@ -910,8 +912,9 @@ tc_unify_tys :: BindFamFun -> BindTvFun
-- 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
+ do { case match_kis of
+ CheckOuterKinds -> unify_tys env kis1 kis2
+ IgnoreOuterKinds -> return ()
; unify_tys env tys1 tys2 }
where
env = UMEnv { um_bind_tv_fun = bind_tv
@@ -926,6 +929,11 @@ tc_unify_tys bind_fam bind_tv unif inj_check match_kis match_mults rn_env tv_env
kis2 = map typeKind tys2
+data OuterKindsFlag
+ = CheckOuterKinds -- Unify or match the /kind/ of the two types
+ | IgnoreOuterKinds -- Just unify or match the types, ignoring kinds
+ -- (typically, we already know they are equal)
+
{- *********************************************************************
* *
UnifyResult, MaybeApart etc
@@ -1583,8 +1591,7 @@ c.f. Note [Comparing type synonyms] in GHC.Core.TyCo.Compare
-------------- unify_ty: the main workhorse -----------
-type AmIUnifying = Bool -- True <=> Unifying
- -- False <=> Matching
+data AmIUnifying = Matching | Unifying
type InType = Type -- Before applying the RnEnv2
type OutCoercion = Coercion -- After applying the RnEnv2
@@ -1618,7 +1625,7 @@ unify_ty env (CastTy ty1 co1) ty2 kco
-- See (KCU1) in Note [Kind coercions in Unify]
= maybeApart MARCast -- See (KCU2)
- | um_unif env
+ | Unifying <- um_unif env
= unify_ty env ty1 ty2 (co1 `mkTransCo` kco)
| otherwise -- We are matching, not unifying
@@ -1661,7 +1668,7 @@ unify_ty env (CoercionTy co1) (CoercionTy co2) kco
= do { c_subst <- getCvSubstEnv
; case co1 of
CoVarCo cv
- | not (um_unif env)
+ | Matching <- 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
@@ -1682,7 +1689,7 @@ 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
+ | Unifying <- um_unif env -- If unifying, can swap args; but not when matching
= uVarOrFam (umSwapRn env) (TyVarLHS tv2) ty1 (mkSymCo kco)
-- Deal with TyConApps
@@ -1692,7 +1699,7 @@ unify_ty env ty1 ty2 kco
| Just (tc,tys) <- mb_sat_fam_app1
= uVarOrFam env (TyFamLHS tc tys) ty2 kco
- | um_unif env
+ | Unifying <- um_unif env
, Just (tc,tys) <- mb_sat_fam_app2
= uVarOrFam (umSwapRn env) (TyFamLHS tc tys) ty1 (mkSymCo kco)
@@ -1820,7 +1827,7 @@ uVarOrFam env ty1 ty2 kco
go swapped substs lhs@(TyVarLHS 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
+ if | Unifying <- um_unif env -> unify_ty env ty1' ty2 kco
| (ty1' `mkCastTy` kco) `tcEqType` ty2 -> return ()
| otherwise -> surelyApart
-- Unifying: recurse into unify_ty
@@ -1842,9 +1849,9 @@ uVarOrFam env ty1 ty2 kco
| TyVarTy tv2 <- ty2
, let tv2' = umRnOccR env tv2
, tv1' == tv2'
- = if | um_unif env -> return ()
- | tv1_is_bindable -> extendTvEnv tv1' ty2
- | otherwise -> return ()
+ = if | Unifying <- um_unif env -> return ()
+ | tv1_is_bindable -> extendTvEnv tv1' ty2
+ | otherwise -> return ()
| tv1_is_bindable
, not (mentionsForAllBoundTyVarsR env ty2_fvs)
@@ -1858,9 +1865,9 @@ uVarOrFam env ty1 ty2 kco
-- 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
+ | Unifying <- um_unif env
, NotSwapped <- swapped -- If we have swapped already, don't do so again
- , Just lhs2 <- canEqLHS_maybe ty2
+ , Just lhs2 <- canEqLHS_maybe ty2
= go IsSwapped substs lhs2 (mkTyVarTy tv1) (mkSymCo kco)
| occurs_check = maybeApart MARInfinite -- Occurs check
@@ -1879,7 +1886,9 @@ uVarOrFam env ty1 ty2 kco
| otherwise
= False
- occurs_check = um_unif env && uOccursCheck substs foralld_tvs lhs rhs
+ occurs_check = case um_unif env of
+ Unifying -> uOccursCheck substs foralld_tvs lhs rhs
+ Matching -> False
-- Occurs check, only when unifying
-- see Note [Infinitary substitutions]
-- Make sure you include `kco` in rhs #14846
@@ -1893,7 +1902,7 @@ uVarOrFam env ty1 ty2 kco
-- Hence the RnEnv2 is empty
| not under_forall
, Just ty1' <- lookupFamEnv (um_fam_env substs) tc1 tys1
- = if | um_unif env -> unify_ty env ty1' ty2 kco
+ = if | Unifying <- um_unif env -> unify_ty env ty1' ty2 kco
-- Below here we are matching
-- The return () case deals with:
-- Template: (F a)..(F a)
@@ -1930,9 +1939,9 @@ uVarOrFam env ty1 ty2 kco
-- NB: a type family can appear on the template when matching
-- see (ATF6) in Note [Apartness and type families]
-- (Only worth doing this if we are not under a forall.)
- | um_unif env
+ | Unifying <- um_unif env
, NotSwapped <- swapped
- , Just lhs2 <- canEqLHS_maybe ty2
+ , Just lhs2 <- canEqLHS_maybe ty2
= go IsSwapped substs lhs2 (mkTyConApp tc1 tys1) (mkSymCo kco)
| otherwise -- See (ATF5) in Note [Apartness and type families]
@@ -1962,9 +1971,9 @@ uVarOrFam env ty1 ty2 kco
(inj_tys2, noninj_tys2) = partitionByList inj tys2
bind_fam_if_poss
- | not (um_unif env) -- Not when matching (ATF11-1)
+ | Matching <- um_unif env -- Not when matching (ATF11-1)
= return ()
- | under_forall -- Not under a forall (ATF3)
+ | under_forall -- Not under a forall (ATF3)
= return ()
| BindMe <- um_bind_fam_fun env tc tys1 rhs1
= unless (uOccursCheck substs emptyVarSet (TyFamLHS tc tys1) rhs1) $
=====================================
compiler/GHC/Iface/Decl.hs
=====================================
@@ -112,7 +112,7 @@ coAxBranchToIfaceBranch tc lhs_s
, ifaxbRoles = roles
, ifaxbRHS = toIfaceType rhs
, ifaxbIncomps = iface_incomps }
- where
+ where
iface_incomps = map (expectJust
. flip findIndex lhs_s
. eqTypes
=====================================
compiler/GHC/Iface/Syntax.hs
=====================================
@@ -338,7 +338,12 @@ data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars :: [IfaceTvBndr]
, ifaxbRoles :: [Role]
, ifaxbRHS :: IfaceType
, ifaxbIncomps :: [BranchIndex] }
- -- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom
+ -- We store the incompatibilities in IfaceAxBranch
+ -- just for (perhaps unnecessary) display purposes:
+ -- see Note [Displaying axiom incompatibilities]
+ -- When we construct a real CoAxBranch we compute cab_incomps directly
+ -- from the equations, ignoring the ifaxbIncomps.
+ -- We could consider getting rid of ifaxbIncomps altogether.
data IfaceConDecls
= IfAbstractTyCon -- c.f TyCon.AbstractTyCon
@@ -779,14 +784,13 @@ that is what is seen by importing module with --make
Note [Displaying axiom incompatibilities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-With -fprint-axiom-incomps we display which closed type family equations
-are incompatible with which. This information is sometimes necessary
-because GHC doesn't try equations in order: any equation can be used when
-all preceding equations that are incompatible with it do not apply.
-
-For example, the last "a && a = a" equation in Data.Type.Bool.&& is
-actually compatible with all previous equations, and can reduce at any
-time.
+With -fprint-axiom-incomps we display which closed type family equations are
+incompatible with which (see #15546). This information is sometimes necessary
+because GHC doesn't try equations in order: any equation can be used when all
+preceding equations that are incompatible with it do not apply.
+
+For example, the last "a && a = a" equation in Data.Type.Bool.&& is actually
+compatible with all previous equations, and can reduce at any time.
This is displayed as:
Prelude> :i Data.Type.Equality.==
=====================================
compiler/GHC/IfaceToCore.hs
=====================================
@@ -91,7 +91,6 @@ import GHC.Utils.Logger
import GHC.Data.Bag
import GHC.Data.Maybe
import GHC.Data.FastString
-import GHC.Data.List.SetOps
import GHC.Types.Annotations
import GHC.Types.SourceFile
@@ -903,12 +902,7 @@ tc_iface_decl _ _ (IfaceAxiom { ifName = tc_name, ifTyCon = tc
-- See #13803
; tc_branches <- forkM (text "Axiom branches" <+> ppr tc_name)
$ tc_ax_branches branches
- ; let axiom = CoAxiom { co_ax_unique = nameUnique tc_name
- , co_ax_name = tc_name
- , co_ax_tc = tc_tycon
- , co_ax_role = role
- , co_ax_branches = manyBranches tc_branches
- , co_ax_implicit = False }
+ ; let axiom = mkBranchedCoAxiom role tc_name tc_tycon tc_branches
; return (ACoAxiom axiom) }
tc_iface_decl _ _ (IfacePatSyn{ ifName = name
@@ -1116,15 +1110,14 @@ tc_fd (tvs1, tvs2) = do { tvs1' <- mapM tcIfaceTyVar tvs1
; return (tvs1', tvs2') }
tc_ax_branches :: [IfaceAxBranch] -> IfL [CoAxBranch]
-tc_ax_branches if_branches = foldlM tc_ax_branch [] if_branches
+tc_ax_branches if_branches = mapM tc_ax_branch if_branches
-tc_ax_branch :: [CoAxBranch] -> IfaceAxBranch -> IfL [CoAxBranch]
-tc_ax_branch prev_branches
- (IfaceAxBranch { ifaxbTyVars = tv_bndrs
+tc_ax_branch :: IfaceAxBranch -> IfL CoAxBranch
+tc_ax_branch (IfaceAxBranch { ifaxbTyVars = tv_bndrs
, ifaxbEtaTyVars = eta_tv_bndrs
, ifaxbCoVars = cv_bndrs
, ifaxbLHS = lhs, ifaxbRHS = rhs
- , ifaxbRoles = roles, ifaxbIncomps = incomps })
+ , ifaxbRoles = roles })
= bindIfaceTyConBinders_AT
(map (\b -> Bndr (IfaceTvBndr b) (NamedTCB Inferred)) tv_bndrs) $ \ tvs ->
-- The _AT variant is needed here; see Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom
@@ -1135,15 +1128,15 @@ tc_ax_branch prev_branches
; this_mod <- getIfModule
; let loc = mkGeneralSrcSpan (fsLit "module " `appendFS`
moduleNameFS (moduleName this_mod))
- br = CoAxBranch { cab_loc = loc
- , cab_tvs = binderVars tvs
- , cab_eta_tvs = eta_tvs
- , cab_cvs = cvs
- , cab_lhs = tc_lhs
- , cab_roles = roles
- , cab_rhs = tc_rhs
- , cab_incomps = map (prev_branches `getNth`) incomps }
- ; return (prev_branches ++ [br]) }
+ ; return (CoAxBranch { cab_loc = loc
+ , cab_tvs = binderVars tvs
+ , cab_eta_tvs = eta_tvs
+ , cab_cvs = cvs
+ , cab_lhs = tc_lhs
+ , cab_roles = roles
+ , cab_rhs = tc_rhs
+ , cab_overlaps = placeHolderOverlaps
+ , cab_incomps = placeHolderIncomps }) }
tcIfaceDataCons :: Name -> TyCon -> IfaceConDecls -> IfL AlgTyConRhs
tcIfaceDataCons tycon_name tycon if_cons
=====================================
compiler/GHC/Tc/Instance/FunDeps.hs
=====================================
@@ -136,10 +136,10 @@ data FunDepEqns -- Plural becuase fd_eqs has multiple equations
-- to fresh unification vars,
-- See (IMP2) in Note [Improving against instances]
- , fd_eqs :: [TypeEqn] -- Make these pairs of types equal
- -- Invariant: In each (Pair ty1 ty2), the fd_qtvs may be
- -- free in ty1 but not in ty2. See Wrinkle (1) of
- -- Note [Improving against instances]
+ , fd_eqs :: [TypeEqn] -- Make these pairs of types equal
+ -- Invariant: In each (Pair ty1 ty2), the fd_qtvs may be
+ -- free in ty1 but not in ty2. See Wrinkle (1) of
+ -- Note [Improving against instances]
}
instance Outputable FunDepEqns where
=====================================
compiler/GHC/Tc/Solver/FunDeps.hs
=====================================
@@ -26,20 +26,23 @@ import GHC.Core.Coercion
import GHC.Core.TyCo.Rep( Type(..) )
import GHC.Core.Predicate( EqRel(..) )
import GHC.Core.TyCon
-import GHC.Core.Unify( tcUnifyTysForInjectivity, typeListsAreApart )
+import GHC.Core.Unify( AmIUnifying(..)
+ , tcUnifyTysForInjectivity, typeListsAreApart )
import GHC.Core.Coercion.Axiom
-import GHC.Core.TyCo.Subst( elemSubst )
+import GHC.Core.TyCo.Subst( elemSubst, extendTvSubstWithClone )
import GHC.Builtin.WiredIn.TypeLits( tryInteractTopFam, tryInteractInertFam )
+import GHC.Types.Var( TyVar, tyVarKind, setTyVarKind )
import GHC.Types.Var.Set
+import GHC.Types.Var.Env( mkInScopeSet )
import GHC.Utils.Outputable
import GHC.Utils.Panic
import Control.Monad( unless )
import GHC.Data.Pair
-import Data.Maybe( isNothing, isJust, mapMaybe )
+import Data.Maybe( isJust, mapMaybe )
{- Note [Overview of functional dependencies in type inference]
@@ -109,7 +112,6 @@ Wrinkles
from fundeps, but that would require new evidence forms, and an extension to
FC, so we don't do that right now (Dec 14).
-
Note [FunDep and implicit parameter reactions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Currently, our story of interacting two dictionaries (or a dictionary
@@ -573,6 +575,7 @@ tryEqFunDeps work_item@(EqCt { eq_lhs = work_lhs
tryFamEqFunDeps :: TcSMode -> [EqCt] -> TyCon -> [TcType] -> EqCt -> SolverStage ()
+-- See Note [Type inference for type families with injectivity]
tryFamEqFunDeps mode eqs_for_me fam_tc work_args
work_item@(EqCt { eq_ev = ev, eq_rhs = work_rhs })
| Just ops <- builtInClosedTyFamTyCon_maybe fam_tc
@@ -583,6 +586,7 @@ tryFamEqFunDeps mode eqs_for_me fam_tc work_args
; tryFDEqns False fam_tc work_args work_item eqns
; unless (hasRelevantGiven eqs_for_me work_args work_item) $
+ -- hasRelevantGiven: See (CF1) in Note [Exploiting closed type families]
do { eqns <- mkTopBuiltinFamEqFDs fam_tc ops work_args work_rhs
; tryFDEqns True fam_tc work_args work_item eqns } }
@@ -599,8 +603,11 @@ tryFamEqFunDeps mode eqs_for_me fam_tc work_args
NotInjective -> nopStage ()
Injective inj -> do { eqns <- mkLocalFamEqFDs eqs_for_me fam_tc inj work_args work_rhs
; tryFDEqns False fam_tc work_args work_item eqns }
+ -- NB: tryFDEqns bales out on an insoluble fundep
+ -- See (CF4) in Note [Exploiting closed type families]
; unless (hasRelevantGiven eqs_for_me work_args work_item) $
+ -- hasRelevantGiven: See (CF1) in Note [Exploiting closed type families]
do { eqns <- mkTopFamEqFDs fam_tc work_args work_item
; tryFDEqns True fam_tc work_args work_item eqns } }
@@ -638,10 +645,11 @@ tryFDEqns is_top fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs= rhs }) f
-- User-defined type families
-----------------------------------------
mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> EqCt -> SolverStage [FunDepEqns]
+-- Implements (INJFAM:Wanted/top-closed)
+-- See Note [Exploiting closed type families]
-- Look at the top-level axioms; we effectively infer injectivity,
--- so we don't need tyConInjectivtyInfo. This works fine for closed
+-- so we don't need tyConInjectivityInfo. This works fine for closed
-- type families without injectivity info
--- See Note [Exploiting closed type families]
mkTopClosedFamEqFDs ax work_args (EqCt { eq_ev = ev, eq_rhs = work_rhs })
| isGenerativeType work_rhs -- See (CF5) in Note [Exploiting closed type families]
= Stage $
@@ -679,39 +687,46 @@ hasRelevantGiven eqs_for_me work_args (EqCt { eq_rhs = work_rhs })
relevant (EqCt { eq_ev = ev, eq_lhs = lhs, eq_rhs = rhs_ty })
| isGiven ev
, TyFamLHS _ lhs_tys <- lhs
- = isJust (tcUnifyTysForInjectivity True work_tys (rhs_ty:lhs_tys))
+ = isJust (tcUnifyTysForInjectivity Unifying work_tys (rhs_ty:lhs_tys))
| otherwise
= False
getRelevantBranches :: CoAxiom Branched -> [TcType] -> Xi -> [FunDepEqns]
-- Return the FunDepEqns that arise from each relevant branch
+-- Implements Note [Relevance]
getRelevantBranches ax work_args work_rhs
- = go [] (fromBranches (coAxiomBranches ax))
+ = go (fromBranches (coAxiomBranches ax))
where
work_tys = work_rhs : work_args
- go _ [] = []
- go preceding (branch:branches)
+ go [] = []
+ go (branch:branches)
= case is_relevant branch of
- Just eqn -> eqn : go (branch:preceding) branches
- Nothing -> go (branch:preceding) branches
+ Just eqn -> eqn : go branches
+ Nothing -> go branches
where
- is_relevant (CoAxBranch { cab_tvs = qtvs, cab_lhs = lhs_tys, cab_rhs = rhs_ty })
- | Just subst <- tcUnifyTysForInjectivity True (rhs_ty:lhs_tys) work_tys
- , let (subst', qtvs') = trim_qtvs subst qtvs
- lhs_tys' = substTys subst' lhs_tys
- rhs_ty' = substTy subst' rhs_ty
- , all (no_match lhs_tys') preceding
+ is_relevant branch@(CoAxBranch { cab_tvs = qtvs
+ , cab_lhs = lhs_tys
+ , cab_rhs = rhs_ty })
+ | Just subst <- tcUnifyTysForInjectivity Unifying (rhs_ty:lhs_tys) work_tys
+ -- See (RW1)-(RW3) in Note [Relevance]
+ -- This is a pre-/unification/ check (not matching)
+ -- so `subst` can bind both `qtvs` and fvs(work_tys)
+ , let (subst',qtvs') = trim_qtvs subst qtvs
+ lhs_tys' = substTys subst' lhs_tys
+ rhs_ty' = substTy subst' rhs_ty
+ branch_tys' = rhs_ty' : lhs_tys'
+ , noEarlierMatchCheck lhs_tys' branch -- See (RW4) in Note [Relevance]
= Just (FDEqns { fd_qtvs = qtvs'
- , fd_eqs = zipWith Pair (rhs_ty':lhs_tys') work_tys })
+ , fd_eqs = zipWith Pair branch_tys' work_tys })
+ -- Do not apply the substition to `work_tys`;
+ -- See (CF7) in Note [Exploiting closed type families]
| otherwise
= Nothing
- no_match lhs_tys (CoAxBranch { cab_lhs = lhs_tys1 })
- = isNothing (tcUnifyTysForInjectivity False lhs_tys1 lhs_tys)
-
mkTopOpenFamEqFDs :: TyCon -> [Bool] -> [TcType] -> EqCt -> TcS [FunDepEqns]
--- Implements (INJFAM:Wanted/top)
+-- Implements (INJFAM:Wanted/top-open)
+-- See Note [Exploiting open type families]
mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs })
= do { fam_envs <- getFamInstEnvs
; let branches :: [CoAxBranch]
@@ -720,15 +735,15 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs })
; return (mapMaybe do_one branches) }
where
do_one :: CoAxBranch -> Maybe FunDepEqns
- do_one branch@(CoAxBranch { cab_tvs = branch_tvs
- , cab_lhs = branch_lhs_tys
- , cab_rhs = branch_rhs })
- | Just subst <- tcUnifyTysForInjectivity False [branch_rhs] [work_rhs]
- -- False: matching, not unifying
- , let (subst', qtvs) = trim_qtvs subst branch_tvs
+ do_one (CoAxBranch { cab_tvs = branch_qtvs
+ , cab_lhs = branch_lhs_tys
+ , cab_rhs = branch_rhs })
+ | Just subst <- tcUnifyTysForInjectivity Matching [branch_rhs] [work_rhs]
+ , let (subst', qtvs') = trim_qtvs subst branch_qtvs
branch_lhs_tys' = substTys subst' branch_lhs_tys
- , apartnessCheck branch_lhs_tys' branch -- See (TIF3)
- = Just (mkInjectivityFDEqn inj_flags qtvs branch_lhs_tys' work_args)
+ -- No need for an apartness check here; for open type families
+ -- there are no "preceding" equations
+ = Just (mkInjectivityFDEqn inj_flags qtvs' branch_lhs_tys' work_args)
| otherwise
= Nothing
@@ -736,7 +751,7 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs })
mkLocalFamEqFDs :: [EqCt] -> TyCon -> [Bool] -> [TcType] -> Xi -> SolverStage [FunDepEqns]
-- Wanted constraints only
-- Both open and closed type families, but only ones with declared injectivity
--- See Note [Type inference for type families with injectivity] esp (TIF2)
+-- See Note [Exploiting local type-family injectivity]
mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs
= do { let -- eqns_from_inerts: see (INJFAM:Wanted/other)
eqns_from_inerts = mapMaybe do_one eqs_for_me
@@ -755,15 +770,27 @@ mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs
mk_eqn iargs = mkInjectivityFDEqn inj_flags [] work_args iargs
-trim_qtvs :: Subst -> [TcTyVar] -> (Subst,[TcTyVar])
--- Tricky stuff: see (TIF1) in
--- Note [Type inference for type families with injectivity]
-trim_qtvs subst [] = (subst, [])
-trim_qtvs subst (tv:tvs)
- | tv `elemSubst` subst = trim_qtvs subst tvs
- | otherwise = let !(subst1, tv') = substTyVarBndr subst tv
- !(subst', tvs') = trim_qtvs subst1 tvs
- in (subst', tv':tvs')
+trim_qtvs :: Subst -> [TyVar] -> (Subst, [TyVar])
+-- Tricky stuff: see (OF1) in Note [Exploiting open type families]
+trim_qtvs unif_subst qtvs
+ = go unif_subst qtvs
+ where
+ go :: Subst -> [TyVar] -> (Subst, [TyVar])
+ go subst [] = (subst, [])
+ go subst (tv:tvs)
+ | tv `elemSubst` unif_subst = go subst tvs
+ | otherwise = go_fresh subst tv tvs
+
+ -- Using an auxiliary function here to avoid prematurely forcing
+ -- the (banged) recursive call to `go` in the non-fresh case
+ go_fresh subst tv tvs = (subst'', tv':tvs')
+ where
+ !(subst'', tvs') = go subst' tvs
+ tv' = tv `setTyVarKind` substTy subst (tyVarKind tv)
+ subst' = extendTvSubstWithClone subst tv tv'
+ -- extendTvSubstWithClone: see (OF1b) in
+ -- Note [Exploiting open type families]
+
-----------------------------------------
-- Built-in type families
@@ -924,15 +951,20 @@ we attempt to exploit injectivity, via `mkLocalFamEqFDs`:
* (INJFAM:Wanted/other) see `mkLocalFamEqFDs`
work item: [W] F s1 s2 ~ rhs -- Wanted
inert: [G/W] F t2 t2 ~ rhs -- Same `rhs`, Given or Wanted
- We can generate FunDepEqns: (s2 ~ t2)
+ See Note [Exploiting local type-family injectivity]
+
+* (INJFAM:Wanted/top-open) for open type families: `mkTopOpenFamEqFDs`
+ type family F a b = r | r -> b
+ type instance F Int (Maybe a) = [G Int] -- G is a type family
+ [W] F alpha beta = [ty]
+ We can generate (Maybe gamma ~ beta)
+ See Note [Exploiting open type families]
-* (INJFAM:Wanted/top) see `mkTopUserFamEqFDs`
- work item: [W] F s1 s2 ~ rhs
- type instance forall a b c. F t1 t2 ~ top_rhs
- and we can /match/ the LHS, so that
- S(top_rhs) = rhs
- then we can generate the FunDepEqns: forall a c. s2 ~ S(t2)
- But see wrinkle (TIF1), (TIF3)
+* (INJFAM:Wanted/top-closed) for closed type families: `mkTopClosedFamEqFDs`
+ type family F a b where { ...eqns... }
+ [W] F alpha ~ Int
+ We may be able to generate some extra equalities to constraint `alpha`
+ See very clever Note [Exploiting closed type families]
For /built-in/ type families, it's pretty similar, except that
@@ -945,45 +977,36 @@ For /built-in/ type families, it's pretty similar, except that
* mkLocalBuiltinFamEqFDs
* mkTopBuiltinFamEqFDs
-(TIF1) Generating fundeps from a top-level type instance is covered in
- Section 5.2 in the Injective Type Families paper. It's a bit tricky.
- Consider
- type family F @k (a::k) (b::k) = r | r -> k b
- type instance forall k (a::k) (b::k). F @k (Proxy @k a) (Proxy @k b) = Proxy @k a
- [W] F @kappa alpha beta ~ Maybe (Proxy @kappa (delta::kappa))
-
- we match (Proxy @kappa delta) against the template (Proxy k a), succeeding
- with substitution [k:->kappa, a:->delta]. We want to generate this FunDepEqns
- FDEqn { fd_qtvs = [b:kappa], fd_eqs = [ beta ~ Proxy @kappa b ] }
- Notice that
- * we must quantify the FunDepEqns over `b`, which is not matched; for this
- we will generate a fresh unification variable in `instantiateFunDepEqn`.
- * we must substitute `k:->kappa` in the kind of `b`.
- This fancy footwork for `fd_qtvs` is done by `trim_qtvs` in
- `mkInjWantedFamEqTopEqns`.
-
-(TIF2) All this applies equally to /closed/ type families; it is /not/
- subsumed by Note [Exploiting closed type families]. Consider:
+Note [Exploiting local type-family injectivity] see `mkLocalFamEqFDs`
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have a type family with declared injectivity:
+ type family F a b = r | r -> b
+and we have
+ work item: [W] F s1 s2 ~ F t1 t2
+or
+ work item: [W] F s1 s2 ~ rhs -- Wanted
+ inert: [G/W] F t2 t2 ~ rhs -- Same `rhs`, Given or Wanted
+
+Then we can generate FunDepEqns: (s2 ~ t2)
+
+This applies equally to /closed/ type families; it is /not/ subsumed
+by Note [Exploiting closed type families]. Consider:
+
type family F a | r -> a where { .... }
[W] F t1 ~ a
[W] F t2 ~ a
- Then since F is declared injective, we can generate t1~t2.
+Then since F is declared injective, we can generate t1~t2.
- As for open type families, we insist on /user-declared/ injectivity only; we
- don't try to /infer/ injectivity even for a closed family. See Section 3.4
- of the "Injective type families" paper. (Arguably, we could /infer/
- injectivity for closed type families, and that would be more in the spirit of
- Note [Exploiting closed type families].)
+As for open type families, we insist on /user-declared/ injectivity only; we
+don't try to /infer/ injectivity even for a closed family. See Section 3.4
+of the "Injective type families" paper. (Arguably, we could /infer/
+injectivity for closed type families, and that would be more in the spirit of
+Note [Exploiting closed type families].)
-(TIF3) Further to (TIF1), if we are considering a /closed/ type family, we
- must ensure (see Section 5.2 of the paper) that after matching that
- equation would indeed be the one to fire. So we call `apartnessCheck`
- on the branch to ensure this, in `mkTopUserFamEqFDs`.
-
-Definition [Relevance]
-~~~~~~~~~~~~~~~~~~~~~~
+Note [Relevance]
+~~~~~~~~~~~~~~~~
We say that a closed-type-family equation `F lhs = rhs` is
/relevant/ for a Wanted [W] F wlhs ~ wrhs
iff
@@ -992,6 +1015,10 @@ iff
(R2) There is no earlier equation that matches S(lhs). See (RW4) below.
+The relevance check is implemented by `getRelevantBranches`, which actually
+returns the [FunDepEqns] described in the Closed Family Fundep Algorithm in
+Note [Exploiting closed type families].
+
(RW1) Pre-unification treats type-family applications as binding to anything,
rather like type variables. If two types don't even pre-unify, we say that they
are /apart/. It is done by `tcUnifyTysForInjectivity`.
@@ -1014,24 +1041,130 @@ iff
Clearly the RHS is apart from the first equation and we want to fire injectivity
on the second equation.
-(RW4) Why "no earlier equation matches" in conditoin (R2)? Consider the family
+(RW4) Why "no earlier equation matches" in condition (R2)? Consider the family
type family Bak a = r where
Bak Int = Char -- B1
Bak Char = Int -- B2
Bak a = a -- B3
- and [W] Bak alpha ~ Char. In fact, only (B2) is relevant for this Wanted.
+ and [W] Bak alpha ~ Char. In fact, only (B1) is relevant for this Wanted.
You might think that (B3) could be instantiated to Bak Char ~ Char; but
actually that instantiation will never fire because (B2) Bak Char ~ Int would
- fire first. So the only way to return a Char is if the argment is Int; so we
- can emit [W] alpha ~ Int. Hence (B3) is not relevant; only (B2) is relevant.
+ fire first. So the only way to return a Char is via (B1); so we
+ can emit [W] alpha ~ Int. Hence (B3) is not relevant; only (B1) is relevant.
That is the reason for condition (R2) in the definition of Relevance above.
A watertight proof that this is the Right Thing is not very easy. See more
- discussion in #23162.
-
-Note [Exploiting closed type families]
+ discussion in #23162, and Section 5.2 of the paper.
+
+ How, precisely, do we implement (R2)? We check that there is no earlier equation
+ that fires on S(lhs), in this case (on Bak Char). Notice that this is different
+ from the `apartnessCheck`, which checks that all preceding equations are apart
+ from S(lhs). Apartness checking uses /unification/; here we want /matching/.
+ Hence using `noEarlierMatchCheck`, not `apartnessCheck`.
+
+ Here's a good example from T27171_aux. T
+ type family TMessage m where
+ {- T1 -} TMessage @f @t (CustomMethod s :: Method f t) = ()
+ {- T2 -} TMessage @f @Req (m :: Method f Req) = TRequestMessage m
+ {- T3 -} TMessage @f @Not (m :: Method f Not) = TNotificationMessage m
+
+ [W] TMessage @SC @Req alpha ~# TRequestMessage alpha
+
+ There is only one relevant equation, namely (T2). If we apply its
+ pre-unification substitution [f :-> SC, m :-> alpha] to its LHS we get
+ TMessage @SC @Req alpha
+ and equation (T1) does not match that. (It does unify, but we don't care.)
+
+(RW5) `noEarlierMatchCheck`: in (RW4) We really do need to check that /no/
+ earlier equation matches, not just no earlier /incompatible/ equation
+ matches. Consider T27828a:
+ type family F a where
+ F Int = Int -- B1
+ F Char = Bool -- B2
+ F a = a -- B3
+
+ [W] F alpha ~ Int
+
+ (B1) is relevant, and (B2) is not. What about (B3)? It pre-unifies with
+ the Wanted via [alpha :-> Int, a :-> Int]. But under that substitution
+ (B1) would fire, so (B3) is not relevant.
+
+ And yet, (B1) is /compatible/ with (B3), so it's no good just looking at
+ the `cab_incomps` of (B3). Instead we look at `cab_overlaps`.
+
+Note [Exploiting open type families] see `mkTopOpenFamEqFDs`
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Generating fundeps from a top-level type instance is covered in Section 5.2 in
+the Injective Type Families paper. For open type families, suppose we have
+
+ type family F a = r | r -> a
+ type instance F [a] = a->a
+
+ [W] F alpha ~ Int->Int
+
+Then, since F has been checked as injective, and the RHS `a->a` (pre-)unifies
+with the `Int->Int` in the Wanted with substitution [a :-> Int], we can
+add a derived FunDepEqns
+ FDEqns{ fd_qtvs = [], fd_eqs = [ [Int] ~ alpha ] }
+and thereby emit (via `instantiateFunDepEqns`)
+ [W] [Int] ~ alpha
+
+Things are a bit trickier when not all the quantified variables of the
+instance are bound by the pre-unification step. Suppose we have
+
+ type family F a = r | r -> a
+ type instance F (Maybe a) = [G a] -- G is a type family
+
+ [W] F alpha ~ [ty]
+
+Then, the RHS [G a] pre-unifies with the RHS of the Wanted, but with an
+empty substitution, which does not fix `a`. So we get this FunDepEqns:
+ FDEqns{ fd_qtvs = a, fd_eqs = [ Maybe a ~ alpha ] }
+(note the fd_qtvs=a) and thereby emit (via `instantiateFunDepEqns`)
+ [W] Maybe gamma ~ alpha -- Fresh gamma
+We have learned that `alpha` must be a list, but that is all; we don't
+know what is inside it, hence the fresh `gamma`.
+
+In general we have:
+
+ type family F x1 ... xn = r | r -> x1 x3 (say)
+ type instance forall qs. F t1 ... tn = rhs
+ [W] F a1 ... an ~ b
+
+Suppose `b` pre-unifies with `rhs`, with substitution `S` that binds
+some (but perhaps not all) of the `qs`. Lets say
+ unbound_qs = qs \ dom(S)
+
+Then we generate the FunDepEqs
+ FDEqns{ fd_qtvs = unbound_qs
+ , fd_eqs = [ S(t1) ~ S(a1), S(t3) ~ S(a3) ]
+
+These 'fd_qtvs' are subsequently instantiated to fresh metavariables by
+'instantiateFunDepEqns'.
+
+(OF1) The computation of `unbound_qs` is done by `trim_qtvs`, but we
+ have to be careful. Suppose (OF1a)
+ qs = [ k::*, a::k ]
+ S = [ k :-> UnliftedType ]
+ Then we want
+ unbound_qs = [ a::UnliftedType ] -- Must apply S to q's kind!!
+
+ And (OF1b), although I'm not sure if this can acutally happen:
+ qs = [ k::*, a::(k::*), b::(a::k) ]
+ S = [ k :-> UnliftedType ]
+ We want
+ unbound_qs = [ a::UnliftedType, b::(a::UnliftedType) ]
+ Note that the occurrence of `a` in b's kind should be replaced by the
+ newly-kinded `a` not the original `a::k`.
+
+ This fancy footwork for `fd_qtvs` is done by `trim_qtvs`. It
+ * Drops a quantified tyvar that /is/ matched
+ * Substitutes in the kind of a quantified tyvar `a` that is /not/ matched
+ * Adds the substitution [a::k :-> a::S(k)] to the substitution
+
+Note [Exploiting closed type families] see `mkTopClosedFamEqFDs`
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
type family F a b where
@@ -1042,17 +1175,18 @@ Suppose we have
[W] F Int alpha ~ Char
The /only/ way to solve this Wanted is using (F2), so we can safely unify
-alpha:=Char without risking losing any solutions. That is what
-`mkTopClosedFamEqFDs` does. Ticket #23162 has lots of background detail
+alpha:=Char without risking losing any solutions. We don't even need any
+injectivity annotations. Ticket #23162 has lots of background detail.
-More precisely, here is the Closed Family Fundep Algorithm (CFFA)
+More precisely, here is the very clever Closed Family Fundep Algorithm (CFFA)
IF * F a is a closed type family.
* We are trying to solve [W] F wlhs ~ wrhs.
- * There are no "relevant" Givens [G] F lhs ~ rhs. See (CF1) below.
- * F has exactly one equation, F lhs = rhs that is "relevant" for that Wanted
+ * There are no "relevant Givens" [G] F lhs ~ rhs. See (CF1) below.
+ * F has exactly one equation, F lhs = rhs that is "relevant" for
+ that Wanted (see Note [Relevance])
THEN
- we can emit and solve the fundep equalities:
+ we can emit and solve the fundeps :: [FunDepEqns]:
[W] wlhs1 ~ lhs1
...
[W] wlhsn ~ lhsn
@@ -1060,7 +1194,10 @@ More precisely, here is the Closed Family Fundep Algorithm (CFFA)
with fresh unification vars in lhs and rhs for the quantified variables of the
equation.
-See Definition [Relevance] for what "relevant" means.
+ Actually we take advantage of the substitution generated by the relevance
+ check, see (CF7) below.
+
+See Note [Relevance] for what "relevant" means.
We need to take care about non-termination; see (CF3).
Key point: equations that are not relevant do not need to be considered for fundeps at all.
@@ -1166,6 +1303,8 @@ Key point: equations that are not relevant do not need to be considered for fund
I was looking at non-termination for closed type families, but it's a small
improvement in general.
+ This bale-out is implementedn in `tryFDEqns`.
+
(CF5) Consider (see "Yikes5" in #23162):
type family F a where
F (Just x) = Int
@@ -1196,7 +1335,7 @@ Key point: equations that are not relevant do not need to be considered for fund
type family I t = res | res -> t where
I TInt = Int |> g -- where g :: Type ~# IK k
and [W] I alpha ~ Int |> g2
- Here we definiteily want to take advantage of injectivity.
+ Here we definitely want to take advantage of injectivity.
(CF6) This machinery can also have a significant positive effect on the size of
proof terms. For example (simplification of T26426):
@@ -1204,7 +1343,8 @@ Key point: equations that are not relevant do not need to be considered for fund
type family (++) a b where { '[] ++ ys = ys; (x:xs) ++ ys = x : (xs ++ ys) }
type family MapId a where { MapId '[] = '[]; MapId (x:xs) = x : MapId xs }
- app :: (MapId xs ++ MapId ys ~ MapId (xs ++ ys)) => Proxy xs -> Proxy ys -> Proxy (xs ++ ys)
+ app :: (MapId xs ++ MapId ys ~ MapId (xs ++ ys))
+ => Proxy xs -> Proxy ys -> Proxy (xs ++ ys)
test :: Proxy [ty_1, ..., ty_n]
test = Proxy @'[ty_1]
@@ -1248,6 +1388,30 @@ Key point: equations that are not relevant do not need to be considered for fund
instead of relying on recursively built sub-proof terms, which brings down
coercion sizes (in certain situations) from O(n^3) to O(n^2).
+(CF7) Relevance. When computing relevance in the Closed Family Fundep Algorithm,
+ for [W] F wlhs1 wlhs2 ~ wrhs, against an equation F lhs1 lhs2 ~ rhs
+ we get back a pre-unifying substitution S that makes the two as equal as poss.
+ Then we use `trim_qtvs` in exactly the same way as in
+ (OF1) of Note [Exploiting open type families], to generate qtvs' and S'
+ Then we generate
+ FDEqns { fd_qtvs = qtvs', fd_eqs [ S'(lhs1) ~ wlhs1
+ , S'(lhs2) ~ wlhs2
+ , S'(rhs) ~ wrhs ] }
+ Notice that we do /not/ apply S' to wlhs/wrhs. These type contain unification
+ variables that we must actually unify! Example
+ type family F a b where
+ F [a] (Maybe b) = (a, G b)
+ [W] F alpha beta ~ (Int, [gamma])
+ Pre-unification gives [alpha :-> [a], beta :-> Maybe b, a :-> Int]
+ This substitution eliminates the quantified variable `a` but not `b`, so we
+ want this:
+ FDEqns { fd_qtvs = [b], fd_eqs [ [Int] ~ alpha
+ , Maybe b ~ beta
+ , (Int,G b) ~ (Int, [gamma]) ] }
+
+ Notice also that by applying the substitution to the template but not to the
+ Wanted, we uphold the `fd_eqs` invariant in `FDEqns` (see its data type decl)
+
Note [Cache-caused loops]
~~~~~~~~~~~~~~~~~~~~~~~~~
It is very dangerous to cache a rewritten wanted family equation as 'solved' in
@@ -1340,28 +1504,34 @@ solveFunDeps work_ev fd_eqns
; uPairsTcM uenv eqs }
instantiateFunDepEqns :: FunDepEqns -> TcM [TypeEqn]
-instantiateFunDepEqns (FDEqns { fd_qtvs = tvs, fd_eqs = eqs })
- | null tvs
+-- See GHC.Tc.Instance.Fundeps Note [Improving against instances]
+-- Wrinkle (IMP1)
+instantiateFunDepEqns (FDEqns { fd_qtvs = qtvs, fd_eqs = eqs })
+ | null qtvs
= return rev_eqs
| otherwise
- = do { TcM.traceTc "instantiateFunDepEqns" (ppr tvs $$ ppr eqs)
- ; (_, subst) <- instFlexiXTcM emptySubst tvs -- Takes account of kind substitution
+ = do { TcM.traceTc "instantiateFunDepEqns" (ppr qtvs $$ ppr eqs)
+ ; (_, subst) <- instFlexiXTcM empty_subst qtvs -- Takes account of kind substitution
; return (map (subst_pair subst) rev_eqs) }
where
rev_eqs = reverse eqs
-- (reverse eqs): See Note [Reverse order of fundep equations]
+ -- The kinds of `qtvs` can have free variables, because of `trim_qtvs`
+ -- Example: T27828b
+ empty_subst = mkEmptySubst $ mkInScopeSet $
+ tyCoVarsOfTypes (map tyVarKind qtvs)
+
subst_pair subst (Pair ty1 ty2)
- = Pair (substTyUnchecked subst' ty1) ty2
- -- ty2 does not mention fd_qtvs, so no need to subst it.
- -- See GHC.Tc.Instance.Fundeps Note [Improving against instances]
- -- Wrinkle (1)
+ = Pair (substTy subst' ty1) ty2
+ -- NB: ty2 does not mention fd_qtvs, so no need to subst it.
+ -- See invariant on `fv_eqs` in `data FunDepEqns`.
where
subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1)
-- The free vars of ty1 aren't just fd_qtvs: ty1 is the result
-- of matching with the [W] constraint. So we add its free
-- vars to InScopeSet, to satisfy substTy's invariants, even
- -- though ty1 will never (currently) be a poytype, so this
+ -- though ty1 will never (currently) be a polytype, so this
-- InScopeSet will never be looked at.
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -3462,7 +3462,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
; let mb_co_ax
| null eqns = Nothing -- mkBranchedCoAxiom fails on empty list
- | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches)
+ | otherwise = Just (mkBranchedCoAxiom Nominal co_ax_name fam_tc branches)
fam_tc = mkFamilyTyCon tc_name kind tc_bndrs 0 res_kind (resultVariableName sig)
(ClosedTypeFamilyTyCon $ CTF mb_co_ax) parent inj'
=====================================
testsuite/tests/indexed-types/should_compile/T27828.hs
=====================================
@@ -0,0 +1,50 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeAbstractions #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Bug where
+
+import Data.Functor.Identity (Identity(..))
+import Data.Kind (Type)
+import Data.Proxy (Proxy(..))
+import Data.Type.Equality ((:~:)(..))
+
+type TyFun :: Type -> Type -> Type
+data TyFun a b
+
+type (~>) :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+
+type Apply :: (k1 ~> k2) -> k1 -> k2
+type family Apply f x
+
+type Rep1 :: (k -> Type) -> k -> Type
+type family Rep1 f
+
+type To1 :: Rep1 f a -> f a
+type family To1 z
+
+type Par1 :: Type -> Type
+newtype Par1 p = Par1 p
+
+type To1Sym0 :: forall k (f :: k -> Type) (a :: k). Rep1 f a ~> f a
+data To1Sym0 z
+
+applyTo1Sym0 :: forall k (f :: k -> Type) (a :: k) (x :: Rep1 f a). Proxy x -> Apply @(Rep1 f a) @(f a) To1Sym0 x :~: To1 x
+applyTo1Sym0 _ = undefined
+
+type IdentitySym0 :: a ~> Identity a
+data IdentitySym0 z
+type instance Apply IdentitySym0 x = 'Identity x
+
+type Aux :: Rep1 Identity a -> Rep1 Identity a -> Identity a
+type family Aux x y where
+ Aux x ('Par1 wombat) = Apply IdentitySym0 wombat
+
+type instance Rep1 Identity = Par1
+type instance To1 @Identity y = Aux y y
+
+lemma :: forall a (z :: a). Apply @(Rep1 Identity a) @(Identity a) To1Sym0 ('Par1 z) :~: 'Identity z
+lemma = applyTo1Sym0 @Type @Identity @a (Proxy @('Par1 z))
+-- lemma = applyTo1Sym0 @Type @Identity @a @('Par1 z) (Proxy @('Par1 z))
=====================================
testsuite/tests/indexed-types/should_compile/T27828a.hs
=====================================
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T27828a where
+
+import Data.Proxy
+
+type family F a where
+ F Int = Int -- B1
+ F Char = Bool -- B2
+ F a = a -- B3
+
+h :: (F a ~ Int) => Proxy a -> ()
+h = error "urk"
+
+k :: ()
+k = h Proxy -- [W] F alpha ~ Int
=====================================
testsuite/tests/indexed-types/should_compile/T27828b.hs
=====================================
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies, KindSignatures, AllowAmbiguousTypes #-}
+
+module T27828b where
+
+type family IsJust (m :: Maybe k) :: Bool where
+ IsJust ('Just x) = 'True
+ IsJust 'Nothing = 'False
+
+f :: forall k (m :: Maybe k). (IsJust m ~ 'True) => Int -> Int
+f = error "urk"
+
+g _ = f 3 -- Triggered checkValidSubst error in `instantiateFunDepEqns`o
=====================================
testsuite/tests/indexed-types/should_compile/all.T
=====================================
@@ -316,3 +316,6 @@ test('T25611b', normal, compile, [''])
test('T25611c', normal, compile, [''])
test('T25611d', normal, compile, [''])
test('T25657', normal, compile, [''])
+test('T27828', normal, compile, [''])
+test('T27828a', normal, compile, [''])
+test('T27828b', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2af969356bdfd6bf677d19eddcab9a1ā¦
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2af969356bdfd6bf677d19eddcab9a1ā¦
You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help
1
0
[Git][ghc/ghc][wip/rafl/hpc-instances] 27 commits: Add regression test for #7803
by Florian Ragwitz (ļ¼ rafl) 07 Oct '26
by Florian Ragwitz (ļ¼ rafl) 07 Oct '26
07 Oct '26
Florian Ragwitz pushed to branch wip/rafl/hpc-instances at Glasgow Haskell Compiler / GHC
Commits:
234bab08 by Vladislav Zavialov at 2026-09-29T17:22:54-04:00
Add regression test for #7803
Commit 2effe18ab5, first shipped with GHC 8.2.1, fixed #7803 "Superclass
methods are left unspecialized".
This change turns the example from the ticket description into a regression
test, checking that foo1 is fully specialised at Double, with no calls to the
overloaded exp5Tail.
Closes #7803
Assisted-by: Claude Opus 5
- - - - -
c406135c by Andreas Klebinger at 2026-10-01T06:57:28-04:00
RTS: Update flag parsing/handling:
Using 0 as argument to any of these flags now resets the flags setting to default:
- ``-n0`` disables nursery chunking.
- ``-K0`` (or a bare ``-K``) removes the stack size limit.
- ``-M0`` removes the heap size limit.
- ``-H0`` resets the suggested heap size, including the nursery scaling set by ``-H``.
- ``-AL0`` makes the large object allocation limit follow ``-A`` again.
GC Generations are now limited to 64.
-n larger than -A now emits a warning and disables chunking.
Fixes #27830 #27829
- - - - -
984ee82b by Andreas Klebinger at 2026-10-01T06:58:10-04:00
Fix MultiLayerModules timeout multiplier.
We accidentally used the compile multiplier for ghci commands which
use the run timeout setting to set the timeout.
Fixes #26263 and #27796.
- - - - -
50a9cf26 by Andreas Klebinger at 2026-10-01T06:58:10-04:00
testsuite: Include runtime in JUnit report.
- - - - -
e358619f by Alan Zimmerman at 2026-10-01T06:59:01-04:00
EPA: Use EpaLocation in EpVirtualBraces
Haddock processing uses EpLayout.EpVirtualBraces to record the current
layout column, for allocating haddock comments correctly.
For exact printing, we need the line as well as the col, so we know
how many lines to skip when the indented code block starts.
This commit updates EpLayout.EpVirtualBraces so that it carries an
EpaLocation instead of just the Int column, to allow it to be used for
both purposes.
It is a simple mechanical change, with no other impact, but it allows
us to use EpLayout instead of AnnListLayout in AnnList, in the next
commit in this series.
- - - - -
1d2a26ee by Andrew Lelechenko at 2026-10-01T20:22:04-04:00
Remove bitSize from MINIMAL pragma of class Bits
Cf. https://github.com/haskell/core-libraries-committee/issues/441
The function is deprecated for 12 years and has a default implementation,
yet it was never removed from the MINIMAL pragma, putting library authors
in a very awkward position. Let's finally remove bitSize from MINIMAL.
- - - - -
3cc21e4c by Hannes Siebenhandl at 2026-10-01T20:22:59-04:00
Add regression test for #27641
- - - - -
c35096f5 by Hannes Siebenhandl at 2026-10-01T20:23:00-04:00
Don't `:add` modules the loader will reject
Only home modules can be actually added to the loader context, thus we
only accept the module if it belongs to a home unit.
- - - - -
a563cb27 by Simon Jakobi at 2026-10-02T17:37:36-04:00
ci: accept modified changelog.d entries in lint-changelog
The changelog guide says to extend an existing entry rather than add a
new one when the feature is already documented. lint_changelog only
counted added files, so such MRs failed before the validator ran.
Fixes #27779.
Assisted-by: Claude Fable 5.1
- - - - -
03082cd4 by Simon Jakobi at 2026-10-02T17:38:17-04:00
changelog.d: Fix warning flag name in the semaphore-v2 entry
The entry refers to -Wsemaphore-version-mismatch, which does not exist.
The warning GHC emits when it cannot use a -jsem semaphore, including
on a protocol version mismatch, is -Wsemaphore-open-failure.
Context: !15729, #25087
Assisted-by: Claude Fable 5.1
- - - - -
a93705ee by Simon Jakobi at 2026-10-02T17:38:17-04:00
changelog.d: Fix the CLC proposal link in the T27455 entry
The entry used the Sphinx :ref: role with a URL as its target. :ref:
resolves only internal labels, so the generated release notes would
show the proposal name without a link. Use the plain hyperlink form
like the other entries.
Context: !16274, #27455
Assisted-by: Claude Fable 5.1
- - - - -
54381079 by Hannes Siebenhandl at 2026-10-02T17:39:01-04:00
Extend the `TrustOverlay` for wired-in units
The TrustOverlay only contained the `UnitId` of all on-disk units.
However, wired-in units are referred to by their wired-in unit id, which
is not the same as the on-disk unit id.
Thus, trust checks for wired-in units failed because the lookup was
using the wired-in unit, which wasn't present in the `TrustOverlay`.
We fix #27834, by copying the trust info for wired-in unit ids.
- - - - -
f8cfb1a5 by HĆ©cate Kleidukos at 2026-10-04T19:36:39+02:00
[CLC 341] Strict variants of mutable types
This commit is the implementation of CLC Proposal 341
https://github.com/haskell/core-libraries-committee/issues/341
- - - - -
575c4bc6 by Rodrigo Mesquita at 2026-10-05T12:32:02-04:00
ttg: HsModuleName in the AST, ModuleName in GHC
This commit makes the AST fully independent from GHC by parsing a
"module name" as an `HsModuleName (= HText)` rather than constructing an
`ModuleName (= FastString)` straight away.
In the GHC side, everything remains as a `ModuleName`. We turn AST
`HsModuleName`s into fast strings with the cheap `mkFastStringShortText`
when we process the AST for manipulation within the compiler.
There are no performance regressions introduced by this approach.
This is the final piece of #21592
Alternative plans were discussed in
gitlab.haskell.org/ghc/ghc/-/merge_requests/16546#note_694647,
but the Simon suggested one won in simplicity and performance when
compared against my attempt at implementing my original plan of having
a family `ModuleNameP`.
- - - - -
b3b89d32 by mangoiv at 2026-10-05T22:03:32-04:00
hadrian: Persist the used flavour name in the build root (#20650)
This executes the idea proposed in #20650, teaching Hadrian to persist
the flavour used to build a build root. This both makes use of multiple
build roots more ergonomic (as the user no longer needs to repeat
themselves) and avoids a tiresome foot-gun (forgetting to specify a
flavour, often wholly invalidating a build root).
Closes #20650.
Co-authored-by: Sylvain Henry <sylvain(a)haskus.fr>
- - - - -
f977837b by mangoiv at 2026-10-05T22:04:21-04:00
configure: fix sed script and subst tooldir script
Fixes #27672
Adds sanity checking for SUBST_TOOLDIR
Metric Decrease:
LinkableUsage01
MultiLayerModulesTH_OneShot
T10547
T12234
T12425
T13035
T13820
T18140
T18730
T18923
T9198
TcPlugin_RewritePerf
mhu-perf
- - - - -
f1cb08be by Hannes Siebenhandl at 2026-10-05T22:05:03-04:00
Prepend in-memory unit database for backpack
The packageDbFlags are stored in reverse order. Thus, prepending will
ensure that the in-memory unit database is the last item on the unit
database stack.
Further, the in-memory unit database needs to be able to shadow units
from earlier unit databases in the unit database stack.
Moreover, a `-clear-package-db` would remove the in-memory database if
it weren't the last item on the stack.
Closes #27835
- - - - -
8d49ed42 by Kazu Yamamoto at 2026-10-06T19:37:25-04:00
Do not leave standard file descriptors free at startup (#24450)
A process may be started with stdout closed -- `prog >&-` from a shell does
exactly that. Nothing then reserves descriptor 1, and open(), pipe() and
socket() hand out the lowest free descriptor, so the next descriptor the
runtime creates for itself takes it: the ticker's pipe, or a capability's IO
manager control pipe.
'GHC.Internal.IO.StdHandles.stdout' is a CAF, built the first time the program
writes to stdout, which is long after that has happened. It builds a 'Handle'
over descriptor 1, which now belongs to the runtime, and nothing reports an
error because the descriptor is perfectly good. The program then writes its
output into the runtime's own plumbing.
What that looks like from the outside is a hang. The descriptor the Handle has
taken over is the read end of a pipe, so poll() for POLLOUT on it never says
yes and epoll_ctl() accepts a registration for it; the thread waiting to write
blocks for ever. Closing the Handle at exit closes the runtime's descriptor,
which is worse: the ticker then fails on every tick.
'hs_init_ghc' now opens /dev/null onto whichever of descriptors 0, 1 and 2 are
closed, before the runtime creates any descriptor of its own. Each is opened
for the access that descriptor would normally have, read-only for 0 and
write-only for 1 and 2, so that writing to 'stdin' or reading from 'stdout'
still fails rather than quietly succeeding against /dev/null. See
Note [Standard file descriptors must be open].
Moving only the descriptors the runtime opens would not do: the first file the
program itself opened would land on the free number instead. The fix has to
leave no free number. A program run this way therefore finds stdout connected
to /dev/null rather than failing with EBADF on the first write, which is what
such a program would get from most other language runtimes.
Co-Authored-By: Claude Opus 5 (1M context) <noreply(a)anthropic.com>
- - - - -
65bcf9e9 by Simon Jakobi at 2026-10-06T19:38:09-04:00
changelog: Repair the sentence describing #27477
The description read "programs using could crash", the object of
"using" having been lost. The synopsis already says which programs are
affected, so drop the dangling word.
Assisted-by: Claude Fable 5.1
- - - - -
cd39cfb0 by Florian Ragwitz at 2026-10-07T06:51:51-07:00
hpc: Test desired HPC behaviour for class instances
- - - - -
4f89a68d by Florian Ragwitz at 2026-10-07T06:51:51-07:00
Extend TcGblEnv with a mapping from instance method Ids to DFunIds
We want to use this in HPC to provide better support for instance methods.
This is working towards #17155.
- - - - -
392d18f2 by Florian Ragwitz at 2026-10-07T06:51:52-07:00
hpc: Do not create top-level boxes for generated instance methods
Users care about which of their written methods are or aren't covered, not
whether all of the inherited methods are covered as well. Those should be
covered where they are implemented.
We achieve that by stopping to generate top-level boxes which will often appear
as uncovered with no clear indication as to why, and no way to fix other than
excercising code the user has not written.
Fixes #17155, #15932.
- - - - -
7698c840 by Florian Ragwitz at 2026-10-07T06:51:52-07:00
hpc: Provide coverage information for class instances
After fixing #17155, we no longer create top-level boxes for the source spans
of instance heads (previously that was the source span used for
inherited/generated instance methods).
With those boxes gone, we can introduce a new top-level box for each class
instance with that instance head source span, and provide more meaningful
coverage semantics for it.
We make the use of any of the instance's methods (user-written or generated)
tick this box, providing the programmer with useful information about whether
or not the instance was exercised at run-time, and whether the instance might
be unnecessary.
- - - - -
c08665f2 by Florian Ragwitz at 2026-10-07T06:51:52-07:00
hpc: Don't allocate boxes for methodless classes
With the plumbing we currently have, these could never be covered, which is not
helpful to hpc users. This could be improved upon further.
- - - - -
a233cc3a by Florian Ragwitz at 2026-10-07T06:51:52-07:00
Add a changelog entry for new HPC features
- - - - -
55f79d0f by Florian Ragwitz at 2026-10-07T09:31:16-07:00
Remove tcg_inst_meths in favour of a new IdDetails constructor
Thanks for this great suggestion, Sam! <3
- - - - -
dd907dc6 by Florian Ragwitz at 2026-10-07T09:31:16-07:00
Revert back to just using getOccString for DFunIds
- - - - -
160 changed files:
- .gitlab/ci.sh
- + changelog.d/24450
- + changelog.d/27641
- changelog.d/T27455
- + changelog.d/T27830-rts-flag-bounds
- + changelog.d/clc-341-strict-mutable-data-types
- changelog.d/fix-parallel-gc-selector-race-27477
- + changelog.d/hadrian-persist-flavour
- + changelog.d/hpc-classinsts
- changelog.d/semaphore-v2
- changelog.d/unit-index
- compiler/GHC.hs
- compiler/GHC/Builtin/Modules.hs
- compiler/GHC/ByteCode/Asm.hs
- compiler/GHC/ByteCode/Show.hs
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/Opt/CallerCC/Types.hs
- compiler/GHC/Core/Opt/Specialise.hs
- compiler/GHC/Driver/Backpack.hs
- compiler/GHC/Driver/Main/Compile.hs
- compiler/GHC/Driver/Pipeline.hs-boot
- compiler/GHC/Driver/Pipeline/Execute.hs
- compiler/GHC/Driver/Pipeline/Phases.hs
- compiler/GHC/Hs/Doc.hs
- compiler/GHC/Hs/Dump.hs
- compiler/GHC/Hs/Expr.hs
- compiler/GHC/Hs/ImpExp.hs
- compiler/GHC/Hs/Lit.hs
- compiler/GHC/HsToCore.hs
- compiler/GHC/HsToCore/Docs.hs
- compiler/GHC/HsToCore/Quote.hs
- compiler/GHC/HsToCore/Ticks.hs
- compiler/GHC/Iface/Errors/Types.hs
- compiler/GHC/Iface/Ext/Ast.hs
- compiler/GHC/Iface/Ext/Debug.hs
- compiler/GHC/Iface/Ext/Types.hs
- compiler/GHC/Parser.y
- compiler/GHC/Parser/Annotation.hs
- compiler/GHC/Parser/Errors/Types.hs
- compiler/GHC/Parser/Header.hs
- compiler/GHC/Parser/Lexer.x
- compiler/GHC/Parser/PostProcess.hs
- compiler/GHC/Parser/PostProcess/Haddock.hs
- compiler/GHC/Parser/String.hs
- compiler/GHC/Rename/Env.hs
- compiler/GHC/Rename/Names.hs
- compiler/GHC/Rename/Unbound.hs
- compiler/GHC/StgToJS/Linker/Linker.hs
- compiler/GHC/Tc/Deriv/Generics.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Gen/Export.hs
- compiler/GHC/Tc/Module.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/Types.hs
- compiler/GHC/Tc/Types/ErrCtxt.hs
- compiler/GHC/ThToHs.hs
- compiler/GHC/Types/Id/Info.hs
- compiler/GHC/Types/Unique.hs
- compiler/GHC/Types/UnresolvedImport.hs
- compiler/GHC/Unit/External/Wired.hs
- compiler/GHC/Unit/Home.hs
- compiler/GHC/Unit/Module.hs
- compiler/GHC/Unit/Module/Env.hs
- + compiler/GHC/Unit/Module/Name.hs
- compiler/GHC/Unit/Parser.hs
- compiler/GHC/Unit/State.hs
- compiler/GHC/Unit/Types.hs
- compiler/GHC/Unit/Types.hs-boot
- compiler/GHC/Utils/Binary.hs
- compiler/GHC/Utils/Outputable.hs
- compiler/Language/Haskell/Syntax.hs
- compiler/Language/Haskell/Syntax/Expr.hs
- compiler/Language/Haskell/Syntax/ImpExp.hs
- compiler/Language/Haskell/Syntax/Lit.hs
- compiler/Language/Haskell/Syntax/Module/Name.hs
- compiler/Language/Haskell/Syntax/Text.hs
- compiler/ghc.cabal.in
- distrib/configure.ac.in
- docs/users_guide/runtime_control.rst
- ghc/GHCi/UI.hs
- ghc/GHCi/UI/Info.hs
- hadrian/doc/flavours.md
- hadrian/src/Rules.hs
- hadrian/src/Settings.hs
- libraries/base/base.cabal.in
- libraries/base/changelog.md
- libraries/base/src/Control/Concurrent/Chan.hs
- + libraries/base/src/Control/Concurrent/Chan/Strict.hs
- libraries/base/src/Control/Concurrent/MVar.hs
- + libraries/base/src/Control/Concurrent/MVar/Strict.hs
- libraries/base/src/Data/IORef.hs
- + libraries/base/src/Data/IORef/Strict.hs
- libraries/ghc-internal/src/GHC/Internal/Bits.hs
- linters/lint-codes/LintCodes/Static.hs
- m4/subst_tooldir.m4
- rts/RtsFlags.c
- rts/RtsStartup.c
- rts/include/rts/Flags.h
- rts/include/rts/storage/GC.h
- rts/sm/GC.c
- rts/sm/Storage.c
- testsuite/driver/junit.py
- testsuite/driver/testglobals.py
- testsuite/driver/testlib.py
- + testsuite/tests/backpack/should_compile/T27835.bkp
- + testsuite/tests/backpack/should_compile/T27835.stderr
- testsuite/tests/backpack/should_compile/all.T
- testsuite/tests/count-deps/CountDepsAst.stdout
- testsuite/tests/count-deps/CountDepsParser.stdout
- testsuite/tests/ghc-api/downsweep/IncrementalDownsweep.hs
- testsuite/tests/ghc-api/exactprint/T22919.stderr
- testsuite/tests/ghc-api/exactprint/Test20239.stderr
- testsuite/tests/ghc-api/exactprint/ZeroWidthSemi.stderr
- + testsuite/tests/ghci/scripts/T27641.script
- + testsuite/tests/ghci/scripts/T27641.stderr
- + testsuite/tests/ghci/scripts/T27641.stdout
- + testsuite/tests/ghci/scripts/T27834.hs
- + testsuite/tests/ghci/scripts/T27834.script
- + testsuite/tests/ghci/scripts/T27834.stdout
- testsuite/tests/ghci/scripts/all.T
- testsuite/tests/haddock/should_compile_flag_haddock/T17544.stderr
- testsuite/tests/haddock/should_compile_flag_haddock/T17544_kw.stderr
- testsuite/tests/haddock/should_compile_flag_haddock/T24221.stderr
- testsuite/tests/hiefile/should_run/T24544.hs
- + testsuite/tests/hpc/instmeths/instmeths.hs
- + testsuite/tests/hpc/instmeths/instmeths.stdout
- + testsuite/tests/hpc/instmeths/test.T
- testsuite/tests/interface-stability/base-exports.stdout
- testsuite/tests/interface-stability/base-exports.stdout-javascript-unknown-ghcjs
- testsuite/tests/interface-stability/base-exports.stdout-mingw32
- testsuite/tests/module/mod185.stderr
- testsuite/tests/parser/should_compile/DumpParsedAst.stderr
- testsuite/tests/parser/should_compile/DumpParsedAstComments.stderr
- testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
- testsuite/tests/parser/should_compile/DumpSemis.stderr
- testsuite/tests/parser/should_compile/KindSigs.stderr
- testsuite/tests/parser/should_compile/T14189.stderr
- testsuite/tests/parser/should_compile/T15323.stderr
- testsuite/tests/parser/should_compile/T20452.stderr
- testsuite/tests/parser/should_compile/T20718.stderr
- testsuite/tests/parser/should_compile/T20718b.stderr
- testsuite/tests/parser/should_compile/T20846.stderr
- testsuite/tests/parser/should_compile/T23315/T23315.stderr
- testsuite/tests/perf/compiler/all.T
- testsuite/tests/printer/AnnotationNoListTuplePuns.stdout
- testsuite/tests/printer/T18791.stderr
- testsuite/tests/printer/Test20297.stdout
- testsuite/tests/printer/Test24533.stdout
- testsuite/tests/profiling/should_run/caller-cc/CallerCcParser.hs
- + testsuite/tests/rts/T24450.hs
- + testsuite/tests/rts/T24450.stderr
- testsuite/tests/rts/all.T
- testsuite/tests/rts/rtsflags001.stderr-ws-32
- testsuite/tests/rts/rtsflags001.stderr-ws-64
- + testsuite/tests/simplCore/should_compile/T7803.hs
- + testsuite/tests/simplCore/should_compile/T7803.stderr
- + testsuite/tests/simplCore/should_compile/T7803a.hs
- testsuite/tests/simplCore/should_compile/all.T
- utils/check-exact/ExactPrint.hs
- utils/haddock/haddock-api/src/Haddock/Backends/Hyperlinker/Renderer.hs
The diff was not included because it is too large.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/638439a1ed142304e625341d9d6936ā¦
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/638439a1ed142304e625341d9d6936ā¦
You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help
1
0
[Git][ghc/ghc][wip/andrea/with-signal-handlers] removed redundant import
by Andrea Vezzosi (ļ¼ trac-Saizan) 07 Oct '26
by Andrea Vezzosi (ļ¼ trac-Saizan) 07 Oct '26
07 Oct '26
Andrea Vezzosi pushed to branch wip/andrea/with-signal-handlers at Glasgow Haskell Compiler / GHC
Commits:
7b99dff6 by Andrea Vezzosi at 2026-10-07T14:52:34+02:00
removed redundant import
- - - - -
1 changed file:
- compiler/GHC/Utils/Panic.hs
Changes:
=====================================
compiler/GHC/Utils/Panic.hs
=====================================
@@ -79,8 +79,6 @@ import System.Posix.Signals as S
import GHC.ConsoleHandler as S
#endif
-import System.Mem.Weak ( deRefWeak )
-
-- | GHC's own exception type
-- error messages all take the form:
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7b99dff66f15981282978abb97cfa57ā¦
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7b99dff66f15981282978abb97cfa57ā¦
You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help
1
0
[Git][ghc/ghc] Pushed new branch wip/apk/no-tntc-master
by Andreas Klebinger (ļ¼ AndreasK) 07 Oct '26
by Andreas Klebinger (ļ¼ AndreasK) 07 Oct '26
07 Oct '26
Andreas Klebinger pushed new branch wip/apk/no-tntc-master at Glasgow Haskell Compiler / GHC
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/apk/no-tntc-master
You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help
1
0
[Git][ghc/ghc][wip/27845] 19 commits: RTS: Update flag parsing/handling:
by Zubin (ļ¼ wz1000) 07 Oct '26
by Zubin (ļ¼ wz1000) 07 Oct '26
07 Oct '26
Zubin pushed to branch wip/27845 at Glasgow Haskell Compiler / GHC
Commits:
c406135c by Andreas Klebinger at 2026-10-01T06:57:28-04:00
RTS: Update flag parsing/handling:
Using 0 as argument to any of these flags now resets the flags setting to default:
- ``-n0`` disables nursery chunking.
- ``-K0`` (or a bare ``-K``) removes the stack size limit.
- ``-M0`` removes the heap size limit.
- ``-H0`` resets the suggested heap size, including the nursery scaling set by ``-H``.
- ``-AL0`` makes the large object allocation limit follow ``-A`` again.
GC Generations are now limited to 64.
-n larger than -A now emits a warning and disables chunking.
Fixes #27830 #27829
- - - - -
984ee82b by Andreas Klebinger at 2026-10-01T06:58:10-04:00
Fix MultiLayerModules timeout multiplier.
We accidentally used the compile multiplier for ghci commands which
use the run timeout setting to set the timeout.
Fixes #26263 and #27796.
- - - - -
50a9cf26 by Andreas Klebinger at 2026-10-01T06:58:10-04:00
testsuite: Include runtime in JUnit report.
- - - - -
e358619f by Alan Zimmerman at 2026-10-01T06:59:01-04:00
EPA: Use EpaLocation in EpVirtualBraces
Haddock processing uses EpLayout.EpVirtualBraces to record the current
layout column, for allocating haddock comments correctly.
For exact printing, we need the line as well as the col, so we know
how many lines to skip when the indented code block starts.
This commit updates EpLayout.EpVirtualBraces so that it carries an
EpaLocation instead of just the Int column, to allow it to be used for
both purposes.
It is a simple mechanical change, with no other impact, but it allows
us to use EpLayout instead of AnnListLayout in AnnList, in the next
commit in this series.
- - - - -
1d2a26ee by Andrew Lelechenko at 2026-10-01T20:22:04-04:00
Remove bitSize from MINIMAL pragma of class Bits
Cf. https://github.com/haskell/core-libraries-committee/issues/441
The function is deprecated for 12 years and has a default implementation,
yet it was never removed from the MINIMAL pragma, putting library authors
in a very awkward position. Let's finally remove bitSize from MINIMAL.
- - - - -
3cc21e4c by Hannes Siebenhandl at 2026-10-01T20:22:59-04:00
Add regression test for #27641
- - - - -
c35096f5 by Hannes Siebenhandl at 2026-10-01T20:23:00-04:00
Don't `:add` modules the loader will reject
Only home modules can be actually added to the loader context, thus we
only accept the module if it belongs to a home unit.
- - - - -
a563cb27 by Simon Jakobi at 2026-10-02T17:37:36-04:00
ci: accept modified changelog.d entries in lint-changelog
The changelog guide says to extend an existing entry rather than add a
new one when the feature is already documented. lint_changelog only
counted added files, so such MRs failed before the validator ran.
Fixes #27779.
Assisted-by: Claude Fable 5.1
- - - - -
03082cd4 by Simon Jakobi at 2026-10-02T17:38:17-04:00
changelog.d: Fix warning flag name in the semaphore-v2 entry
The entry refers to -Wsemaphore-version-mismatch, which does not exist.
The warning GHC emits when it cannot use a -jsem semaphore, including
on a protocol version mismatch, is -Wsemaphore-open-failure.
Context: !15729, #25087
Assisted-by: Claude Fable 5.1
- - - - -
a93705ee by Simon Jakobi at 2026-10-02T17:38:17-04:00
changelog.d: Fix the CLC proposal link in the T27455 entry
The entry used the Sphinx :ref: role with a URL as its target. :ref:
resolves only internal labels, so the generated release notes would
show the proposal name without a link. Use the plain hyperlink form
like the other entries.
Context: !16274, #27455
Assisted-by: Claude Fable 5.1
- - - - -
54381079 by Hannes Siebenhandl at 2026-10-02T17:39:01-04:00
Extend the `TrustOverlay` for wired-in units
The TrustOverlay only contained the `UnitId` of all on-disk units.
However, wired-in units are referred to by their wired-in unit id, which
is not the same as the on-disk unit id.
Thus, trust checks for wired-in units failed because the lookup was
using the wired-in unit, which wasn't present in the `TrustOverlay`.
We fix #27834, by copying the trust info for wired-in unit ids.
- - - - -
f8cfb1a5 by HĆ©cate Kleidukos at 2026-10-04T19:36:39+02:00
[CLC 341] Strict variants of mutable types
This commit is the implementation of CLC Proposal 341
https://github.com/haskell/core-libraries-committee/issues/341
- - - - -
575c4bc6 by Rodrigo Mesquita at 2026-10-05T12:32:02-04:00
ttg: HsModuleName in the AST, ModuleName in GHC
This commit makes the AST fully independent from GHC by parsing a
"module name" as an `HsModuleName (= HText)` rather than constructing an
`ModuleName (= FastString)` straight away.
In the GHC side, everything remains as a `ModuleName`. We turn AST
`HsModuleName`s into fast strings with the cheap `mkFastStringShortText`
when we process the AST for manipulation within the compiler.
There are no performance regressions introduced by this approach.
This is the final piece of #21592
Alternative plans were discussed in
gitlab.haskell.org/ghc/ghc/-/merge_requests/16546#note_694647,
but the Simon suggested one won in simplicity and performance when
compared against my attempt at implementing my original plan of having
a family `ModuleNameP`.
- - - - -
b3b89d32 by mangoiv at 2026-10-05T22:03:32-04:00
hadrian: Persist the used flavour name in the build root (#20650)
This executes the idea proposed in #20650, teaching Hadrian to persist
the flavour used to build a build root. This both makes use of multiple
build roots more ergonomic (as the user no longer needs to repeat
themselves) and avoids a tiresome foot-gun (forgetting to specify a
flavour, often wholly invalidating a build root).
Closes #20650.
Co-authored-by: Sylvain Henry <sylvain(a)haskus.fr>
- - - - -
f977837b by mangoiv at 2026-10-05T22:04:21-04:00
configure: fix sed script and subst tooldir script
Fixes #27672
Adds sanity checking for SUBST_TOOLDIR
Metric Decrease:
LinkableUsage01
MultiLayerModulesTH_OneShot
T10547
T12234
T12425
T13035
T13820
T18140
T18730
T18923
T9198
TcPlugin_RewritePerf
mhu-perf
- - - - -
f1cb08be by Hannes Siebenhandl at 2026-10-05T22:05:03-04:00
Prepend in-memory unit database for backpack
The packageDbFlags are stored in reverse order. Thus, prepending will
ensure that the in-memory unit database is the last item on the unit
database stack.
Further, the in-memory unit database needs to be able to shadow units
from earlier unit databases in the unit database stack.
Moreover, a `-clear-package-db` would remove the in-memory database if
it weren't the last item on the stack.
Closes #27835
- - - - -
8d49ed42 by Kazu Yamamoto at 2026-10-06T19:37:25-04:00
Do not leave standard file descriptors free at startup (#24450)
A process may be started with stdout closed -- `prog >&-` from a shell does
exactly that. Nothing then reserves descriptor 1, and open(), pipe() and
socket() hand out the lowest free descriptor, so the next descriptor the
runtime creates for itself takes it: the ticker's pipe, or a capability's IO
manager control pipe.
'GHC.Internal.IO.StdHandles.stdout' is a CAF, built the first time the program
writes to stdout, which is long after that has happened. It builds a 'Handle'
over descriptor 1, which now belongs to the runtime, and nothing reports an
error because the descriptor is perfectly good. The program then writes its
output into the runtime's own plumbing.
What that looks like from the outside is a hang. The descriptor the Handle has
taken over is the read end of a pipe, so poll() for POLLOUT on it never says
yes and epoll_ctl() accepts a registration for it; the thread waiting to write
blocks for ever. Closing the Handle at exit closes the runtime's descriptor,
which is worse: the ticker then fails on every tick.
'hs_init_ghc' now opens /dev/null onto whichever of descriptors 0, 1 and 2 are
closed, before the runtime creates any descriptor of its own. Each is opened
for the access that descriptor would normally have, read-only for 0 and
write-only for 1 and 2, so that writing to 'stdin' or reading from 'stdout'
still fails rather than quietly succeeding against /dev/null. See
Note [Standard file descriptors must be open].
Moving only the descriptors the runtime opens would not do: the first file the
program itself opened would land on the free number instead. The fix has to
leave no free number. A program run this way therefore finds stdout connected
to /dev/null rather than failing with EBADF on the first write, which is what
such a program would get from most other language runtimes.
Co-Authored-By: Claude Opus 5 (1M context) <noreply(a)anthropic.com>
- - - - -
65bcf9e9 by Simon Jakobi at 2026-10-06T19:38:09-04:00
changelog: Repair the sentence describing #27477
The description read "programs using could crash", the object of
"using" having been lost. The synopsis already says which programs are
affected, so drop the dangling word.
Assisted-by: Claude Fable 5.1
- - - - -
6d20706d by Zubin Duggal at 2026-10-07T18:18:53+05:30
DmdAnal: Make AbsDmd neutral in maxDmd
fixes #27845
- - - - -
156 changed files:
- .gitlab/ci.sh
- + changelog.d/24450
- + changelog.d/27641
- + changelog.d/27845
- changelog.d/T27455
- + changelog.d/T27830-rts-flag-bounds
- + changelog.d/clc-341-strict-mutable-data-types
- changelog.d/fix-parallel-gc-selector-race-27477
- + changelog.d/hadrian-persist-flavour
- changelog.d/semaphore-v2
- changelog.d/unit-index
- compiler/GHC.hs
- compiler/GHC/Builtin/Modules.hs
- compiler/GHC/ByteCode/Asm.hs
- compiler/GHC/ByteCode/Show.hs
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/Opt/CallerCC/Types.hs
- compiler/GHC/Driver/Backpack.hs
- compiler/GHC/Driver/Main/Compile.hs
- compiler/GHC/Driver/Pipeline.hs-boot
- compiler/GHC/Driver/Pipeline/Execute.hs
- compiler/GHC/Driver/Pipeline/Phases.hs
- compiler/GHC/Hs/Doc.hs
- compiler/GHC/Hs/Dump.hs
- compiler/GHC/Hs/Expr.hs
- compiler/GHC/Hs/ImpExp.hs
- compiler/GHC/Hs/Lit.hs
- compiler/GHC/HsToCore/Docs.hs
- compiler/GHC/HsToCore/Quote.hs
- compiler/GHC/Iface/Errors/Types.hs
- compiler/GHC/Iface/Ext/Ast.hs
- compiler/GHC/Iface/Ext/Debug.hs
- compiler/GHC/Iface/Ext/Types.hs
- compiler/GHC/Parser.y
- compiler/GHC/Parser/Annotation.hs
- compiler/GHC/Parser/Errors/Types.hs
- compiler/GHC/Parser/Header.hs
- compiler/GHC/Parser/Lexer.x
- compiler/GHC/Parser/PostProcess.hs
- compiler/GHC/Parser/PostProcess/Haddock.hs
- compiler/GHC/Parser/String.hs
- compiler/GHC/Rename/Env.hs
- compiler/GHC/Rename/Names.hs
- compiler/GHC/Rename/Unbound.hs
- compiler/GHC/StgToJS/Linker/Linker.hs
- compiler/GHC/Tc/Deriv/Generics.hs
- compiler/GHC/Tc/Errors/Types.hs
- compiler/GHC/Tc/Gen/Export.hs
- compiler/GHC/Tc/Module.hs
- compiler/GHC/Tc/Types.hs
- compiler/GHC/Tc/Types/ErrCtxt.hs
- compiler/GHC/ThToHs.hs
- compiler/GHC/Types/Demand.hs
- compiler/GHC/Types/Unique.hs
- compiler/GHC/Types/UnresolvedImport.hs
- compiler/GHC/Unit/External/Wired.hs
- compiler/GHC/Unit/Home.hs
- compiler/GHC/Unit/Module.hs
- compiler/GHC/Unit/Module/Env.hs
- + compiler/GHC/Unit/Module/Name.hs
- compiler/GHC/Unit/Parser.hs
- compiler/GHC/Unit/State.hs
- compiler/GHC/Unit/Types.hs
- compiler/GHC/Unit/Types.hs-boot
- compiler/GHC/Utils/Binary.hs
- compiler/GHC/Utils/Outputable.hs
- compiler/Language/Haskell/Syntax.hs
- compiler/Language/Haskell/Syntax/Expr.hs
- compiler/Language/Haskell/Syntax/ImpExp.hs
- compiler/Language/Haskell/Syntax/Lit.hs
- compiler/Language/Haskell/Syntax/Module/Name.hs
- compiler/Language/Haskell/Syntax/Text.hs
- compiler/ghc.cabal.in
- distrib/configure.ac.in
- docs/users_guide/runtime_control.rst
- ghc/GHCi/UI.hs
- ghc/GHCi/UI/Info.hs
- hadrian/doc/flavours.md
- hadrian/src/Rules.hs
- hadrian/src/Settings.hs
- libraries/base/base.cabal.in
- libraries/base/changelog.md
- libraries/base/src/Control/Concurrent/Chan.hs
- + libraries/base/src/Control/Concurrent/Chan/Strict.hs
- libraries/base/src/Control/Concurrent/MVar.hs
- + libraries/base/src/Control/Concurrent/MVar/Strict.hs
- libraries/base/src/Data/IORef.hs
- + libraries/base/src/Data/IORef/Strict.hs
- libraries/ghc-internal/src/GHC/Internal/Bits.hs
- linters/lint-codes/LintCodes/Static.hs
- m4/subst_tooldir.m4
- rts/RtsFlags.c
- rts/RtsStartup.c
- rts/include/rts/Flags.h
- rts/include/rts/storage/GC.h
- rts/sm/GC.c
- rts/sm/Storage.c
- testsuite/driver/junit.py
- testsuite/driver/testglobals.py
- testsuite/driver/testlib.py
- + testsuite/tests/backpack/should_compile/T27835.bkp
- + testsuite/tests/backpack/should_compile/T27835.stderr
- testsuite/tests/backpack/should_compile/all.T
- testsuite/tests/count-deps/CountDepsAst.stdout
- testsuite/tests/count-deps/CountDepsParser.stdout
- + testsuite/tests/dmdanal/should_run/T27845.hs
- + testsuite/tests/dmdanal/should_run/T27845.stdout
- + testsuite/tests/dmdanal/should_run/T27845_Lib.hs
- + testsuite/tests/dmdanal/should_run/T27845b.hs
- + testsuite/tests/dmdanal/should_run/T27845b.stdout
- + testsuite/tests/dmdanal/should_run/T27845b_Lib.hs
- testsuite/tests/dmdanal/should_run/all.T
- testsuite/tests/ghc-api/downsweep/IncrementalDownsweep.hs
- testsuite/tests/ghc-api/exactprint/T22919.stderr
- testsuite/tests/ghc-api/exactprint/Test20239.stderr
- testsuite/tests/ghc-api/exactprint/ZeroWidthSemi.stderr
- + testsuite/tests/ghci/scripts/T27641.script
- + testsuite/tests/ghci/scripts/T27641.stderr
- + testsuite/tests/ghci/scripts/T27641.stdout
- + testsuite/tests/ghci/scripts/T27834.hs
- + testsuite/tests/ghci/scripts/T27834.script
- + testsuite/tests/ghci/scripts/T27834.stdout
- testsuite/tests/ghci/scripts/all.T
- testsuite/tests/haddock/should_compile_flag_haddock/T17544.stderr
- testsuite/tests/haddock/should_compile_flag_haddock/T17544_kw.stderr
- testsuite/tests/haddock/should_compile_flag_haddock/T24221.stderr
- testsuite/tests/hiefile/should_run/T24544.hs
- testsuite/tests/interface-stability/base-exports.stdout
- testsuite/tests/interface-stability/base-exports.stdout-javascript-unknown-ghcjs
- testsuite/tests/interface-stability/base-exports.stdout-mingw32
- testsuite/tests/module/mod185.stderr
- testsuite/tests/parser/should_compile/DumpParsedAst.stderr
- testsuite/tests/parser/should_compile/DumpParsedAstComments.stderr
- testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
- testsuite/tests/parser/should_compile/DumpSemis.stderr
- testsuite/tests/parser/should_compile/KindSigs.stderr
- testsuite/tests/parser/should_compile/T14189.stderr
- testsuite/tests/parser/should_compile/T15323.stderr
- testsuite/tests/parser/should_compile/T20452.stderr
- testsuite/tests/parser/should_compile/T20718.stderr
- testsuite/tests/parser/should_compile/T20718b.stderr
- testsuite/tests/parser/should_compile/T20846.stderr
- testsuite/tests/parser/should_compile/T23315/T23315.stderr
- testsuite/tests/perf/compiler/all.T
- testsuite/tests/printer/AnnotationNoListTuplePuns.stdout
- testsuite/tests/printer/T18791.stderr
- testsuite/tests/printer/Test20297.stdout
- testsuite/tests/printer/Test24533.stdout
- testsuite/tests/profiling/should_run/caller-cc/CallerCcParser.hs
- + testsuite/tests/rts/T24450.hs
- + testsuite/tests/rts/T24450.stderr
- testsuite/tests/rts/all.T
- testsuite/tests/rts/rtsflags001.stderr-ws-32
- testsuite/tests/rts/rtsflags001.stderr-ws-64
- utils/check-exact/ExactPrint.hs
- utils/haddock/haddock-api/src/Haddock/Backends/Hyperlinker/Renderer.hs
The diff was not included because it is too large.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/0689685b1903dc6bd4fbf10efae94aā¦
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/0689685b1903dc6bd4fbf10efae94aā¦
You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help
1
0
[Git][ghc/ghc][wip/T27844] Refactor and simplify solver's unification code
by Simon Peyton Jones (ļ¼ simonpj) 07 Oct '26
by Simon Peyton Jones (ļ¼ simonpj) 07 Oct '26
07 Oct '26
Simon Peyton Jones pushed to branch wip/T27844 at Glasgow Haskell Compiler / GHC
Commits:
96911a12 by Simon Peyton Jones at 2026-10-07T13:25:14+01:00
Refactor and simplify solver's unification code
Ticket #27844 showed that GHC's constraint solver could miss an
occurs check, and thereby build an infinite type.
This patch significantly simplifes the code in
GHC.Tc.Solver.Equality.canEqCanLHSFinish_try_unification
GHC.Tc.Solver.Equality.canEqCanLHSFinish_no_unification
It is now significantly simpler, and requires much less subtle
reasoning to understand.
Main changes
* If `canEqCanLHSFinish_try_unification` fails to unify, it now /always/ calls
`canEqCanLHSFinish_no_unification` rather than trying to finish the job itself.
* `GHC.Tc.Solver.Monad.checkTypeEq` is moved from Monad into Equality, and renamed
to `GHC.Tc.Solver.Equality.checkTypeEqNoUnification`.
* `canEqCanLHSFinish_no_unification` calls `checkTypeEqNoUnification` to test
the invariants for an inert equality. Before this MR there was a special case for
`do_not_prevent_rewriting`, but that has gone; instead it's just a consequence of
the flags passed to `checkTyEqRhs`, documented in the `PuOK` case of
`canEqCanLHSFinish_no_unification`.
* There is only one bit of "swap back" code, in `finish_no_unify` in
`canEqCanLHSFinish_try_unification. Previously this code was duplicated.
* `kickOutAfterFillingCoercionHole` should account for equalities with a
TyFamLHS. See (KOC5) in Note [Kick out after filling a coercion hole]
* No need to gather coercion holes in the `PuOK` case of `canEqCanLHSFinish_no_unification`.
See documentation with that code.
- - - - -
12 changed files:
- + changelog.d/T27844
- compiler/GHC/Runtime/Heap/Inspect.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/indexed-types/should_fail/T9662.stderr
- + testsuite/tests/typecheck/should_fail/T27844.hs
- + testsuite/tests/typecheck/should_fail/T27844.stderr
- testsuite/tests/typecheck/should_fail/all.T
Changes:
=====================================
changelog.d/T27844
=====================================
@@ -0,0 +1,9 @@
+section: compiler
+issues: #27844
+mrs: !16723
+synopsis:
+ Reinstate a missing occurs check in the constraint solver
+description:
+ Simplifies code in GHC's type-constraint solver, thereby fixing an outright
+ compiler loop (via a missing occurs check).
+
=====================================
compiler/GHC/Runtime/Heap/Inspect.hs
=====================================
@@ -630,7 +630,7 @@ be sigmas and not taus.
~~~~~~~~~~~~~~~~~~~~~~
In the GHCi debugger we use unification variables whose MetaInfo is
RuntimeUnkTv. The special property of a RuntimeUnkTv is that it can
-unify with a polytype (see GHC.Tc.Utils.Unify.checkTypeEq).
+unify with a polytype (see GHC.Tc.Solver.Equality.checkTypeEqNoUnification).
If we don't do this `:print <term>` will fail if the type of <term>
has nested `forall`s or `=>`s.
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -478,6 +478,7 @@ mkErrorItem ct
-- For this `suppress` stuff see
-- Note [Wanteds rewrite Wanteds: rewriter-sets] in GHC.Tc.Types.Constraint
+ -- especially (WRW8)
(suppress, m_evdest) = case ctEvidence ct of
CtGiven {} -> (False, Nothing)
CtWanted (WantedCt { ctev_rewriters = rws, ctev_dest = dest })
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -21,6 +21,7 @@ import GHC.Tc.Types.Evidence
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.CtLoc
import GHC.Tc.Types.Origin
+import GHC.Tc.Types( TcM )
import GHC.Tc.Utils.Unify
import GHC.Tc.Utils.TcType
import GHC.Tc.Instance.Family ( tcUnwrapNewtype_maybe )
@@ -36,8 +37,8 @@ import GHC.Core.Coercion
import GHC.Core.Reduction
import GHC.Core.FamInstEnv ( FamInstEnvs )
import GHC.Core
-import GHC.Types.Var
+import GHC.Types.Var
import GHC.Types.Basic
import GHC.Types.Name.Reader
import GHC.Types.Var.Env
@@ -49,6 +50,8 @@ import GHC.Utils.Misc
import GHC.Utils.Monad
import GHC.Data.Pair
+import GHC.Data.Bag
+
import Control.Monad
import Data.Maybe ( isJust, isNothing )
import Data.List ( zip4 )
@@ -406,11 +409,13 @@ canonicaliseEquality
-- hold.
canonicaliseEquality ev eq_rel ty1 ty2
- = Stage $ do { traceTcS "canonicaliseEquality" $
+ = Stage $ do { traceTcS "canonicaliseEquality {" $
vcat [ ppr ev, ppr eq_rel, ppr ty1, ppr ty2 ]
; rdr_env <- getGlobalRdrEnvTcS
; fam_insts <- getFamInstEnvs
- ; can_eq_nc initCanEqState rdr_env fam_insts ev eq_rel ty1 ty1 ty2 ty2 }
+ ; res <- can_eq_nc initCanEqState rdr_env fam_insts ev eq_rel ty1 ty1 ty2 ty2
+ ; traceTcS "canonicaliseEquality }" (ppr res)
+ ; return res }
-- | Main worker function for 'canonicaliseEquality'.
--
@@ -1822,7 +1827,7 @@ Ticket #10009, a very nasty example:
g :: forall a. (UnF (F a) ~ a) => a -> ()
g _ = f (undefined :: F a)
-For g we get [G] g1 : UnF (F a) ~ a
+For g we get [G] g1 : UnF (F a) ~ a
[W] w1 : UnF (F beta) ~ beta
[W] w2 : F a ~ F beta
@@ -2040,15 +2045,15 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
then finish_with_swapping
else finish_without_swapping }
- | TyVarLHS {} <- lhs1
+ | TyVarLHS tv <- lhs1
, TyFamLHS {} <- lhs2
- = if put_tyvar_on_lhs
+ = if mightPossiblyUnify ev eq_rel tv
then finish_without_swapping
else finish_with_swapping
| TyFamLHS {} <- lhs1
- , TyVarLHS {} <- lhs2
- = if put_tyvar_on_lhs
+ , TyVarLHS tv <- lhs2
+ = if mightPossiblyUnify ev eq_rel tv
then finish_with_swapping
else finish_without_swapping
@@ -2096,10 +2101,6 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
; new_ev <-rewriteEqEvidence ev swapped lhs1_redn lhs2_redn emptyCoHoleSet
; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) }
- put_tyvar_on_lhs = isWanted ev && eq_rel == NomEq
- -- See Note [Orienting TyVarLHS/TyFamLHS]
- -- Same conditions as for canEqCanLHSFinish_try_unification
- -- which we are setting ourselves up for here
{- Note [Orienting TyVarLHS/TyFamLHS]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2108,16 +2109,16 @@ Which to put on the left? Answer:
* If there is no chance of unifying, put the type family on the left,
(F tys ~ a), because it's generally better to rewrite away function
- calls. See `put_tyvar_on_lhs` in canEqCanLHS2; and
- Note [Orienting TyVarLHS/TyFamLHS]
+ calls. For the "no chance of unifying" test, see calls to
+ `mightPossiblyUnify` in `canEqCanLHS2; and Note [Orienting TyVarLHS/TyFamLHS]
* But if there /is/ a chance of unifying, put the tyvar on the left,
(a ~ F tys), as this may be our only shot to unify. Again see
- `put_tyvar_on_lhs`.
+ `mightPossiblyUnify`.
* But if we /fail/ to unify then flip back to (F tys ~ a) because it's
- generally better to rewrite away function calls. See the call to
- `swapAndFinish` in `canEqCanLHSFinish_try_unification`
+ generally better to rewrite away function calls. See the swapping-back
+ code in `finish_on_unify` in `canEqCanLHSFinish_try_unification`
It's important to flip back. Consider
[W] F alpha ~ alpha
@@ -2197,71 +2198,61 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
= return True
-----------------------
-canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
- -- Try unification; for Wanted, Nominal equalities with a meta-tyvar on the LHS
- | CtWanted wev <- ev -- See Note [Do not unify Givens]
+mightPossiblyUnify :: CtEvidence -> EqRel -> TcTyVar -> Bool
+mightPossiblyUnify ev eq_rel tv
+ | isMetaTyVar tv
+ , CtWanted wev <- ev -- See Note [Do not unify Givens]
, NomEq <- eq_rel -- See Note [Do not unify representational equalities]
, wantedCtHasNoRewriters wev -- See Note [Unify only if the rewriter set is empty]
- , TyVarLHS lhs_tv <- lhs
+ = True
+ | otherwise
+ = False
+
+canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
+ -- Try unification; for Wanted, Nominal equalities with a meta-tyvar on the LHS
+ | TyVarLHS lhs_tv <- lhs
+ , mightPossiblyUnify ev eq_rel lhs_tv
= do { given_eq_lvl <- getInnermostGivenEqLevel
; case simpleUnifyCheck UC_Solver given_eq_lvl lhs_tv rhs of
- SUC_CanUnify ->
- unify lhs_tv (mkReflRedn Nominal rhs)
- SUC_CannotUnify
- | Just can_rhs <- canTyFamEqLHS_maybe rhs
- -> swap_and_finish lhs_tv can_rhs -- See Note [Orienting TyVarLHS/TyFamLHS]
- | otherwise
- -> finish_no_unify
- SUC_NotSure ->
- -- We have a touchable unification variable on the left,
+ SUC_CannotUnify -> finish_no_unify
+ SUC_CanUnify -> do_unification lhs_tv (mkReflRedn Nominal rhs)
+ SUC_NotSure ->
+ -- We have a touchable, unfilled unification variable on the left,
-- and the top-shape check succeeded. These are both guaranteed
-- by the fact that simpleUnifyCheck did not return SUC_CannotUnify.
+ --
+ -- Next, do a full `checkTyEqRhs` check to see if we can unify
+ -- See Note [checkTyEqRhs] in GHC.Tc.Utils.Unify
do { let flags = unifyingLHSMetaTyVar_TEFTask ev lhs_tv
; check_result <- wrapTcS (checkTyEqRhs flags rhs)
+ ; traceTcS "canEqCanLHSFinish_try_unification" $
+ vcat [ text "lhs" <+> ppr lhs
+ , text "rhs" <+> ppr rhs
+ , text "check_result" <+> ppr check_result ]
; case check_result of
- PuOK cts rhs_redn ->
- do { emitWork cts
- ; unify lhs_tv rhs_redn }
- PuFail reason
- | Just can_rhs <- canTyFamEqLHS_maybe rhs
- -> swap_and_finish lhs_tv can_rhs -- See Note [Orienting TyVarLHS/TyFamLHS]
- | reason `cterHasOnlyProblems` do_not_prevent_rewriting
- ->
- -- ContinueWith, to allow using this constraint for
- -- rewriting (e.g. alpha[2] ~ beta[3]).
- do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs
- ; continueWith $ Right $
- EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
- , eq_lhs = lhs , eq_rhs = rhs }
- }
- | otherwise
- -> try_irred reason
- }
+ PuFail {} -> finish_no_unify
+ PuOK cts rhs_redn -> do { emitWork cts
+ ; do_unification lhs_tv rhs_redn } }
}
-- Otherwise unification is off the table
| otherwise
= finish_no_unify
where
- -- We can't unify, but this equality can go in the inert set
- -- and be used to rewrite other constraints.
- finish_no_unify =
- canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
-
- -- We can't unify, and this equality should not be used to rewrite
- -- other constraints (e.g. because it has an occurs check).
- -- So add it to the inert Irreds.
- try_irred reason =
- tryIrredInstead reason ev eq_rel swapped lhs rhs
-
- -- We can't unify as-is, and want to flip the equality around.
- -- Example: alpha ~ F tys, flip it around to become the canonical
- -- equality f tys ~ alpha.
- swap_and_finish tv can_rhs =
- swapAndFinish ev eq_rel swapped (mkTyVarTy tv) can_rhs
-
- -- Phew! Finally! We can unify; go ahead and do so.
- unify tv rhs_redn =
+ -- finish_no_unify: abandon the attempt to unify, and instead hand off to
+ -- canEqCanLHSFinish_no_unification
+ -- First, though, if we have (tv ~ F tys)
+ -- swap it over so we get (F tys ~ tv), with `F tys` on the LHS
+ -- See Note [Orienting TyVarLHS/TyFamLHS]
+ finish_no_unify
+ | TyVarLHS lhs_tv <- lhs
+ , Just can_rhs <- canTyFamEqLHS_maybe rhs
+ = canEqCanLHSFinish_no_unification ev eq_rel (flipSwap swapped) can_rhs (mkTyVarTy lhs_tv)
+ | otherwise
+ = canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
+
+ -- do_unification: Phew! Finally! We can unify; go ahead and do so.
+ do_unification tv rhs_redn =
do { -- In the common case where rhs_redn is Refl, we don't need to rewrite
-- the evidence, even if swapped=IsSwapped. Suppose the original was
-- [W] co : Int ~ alpha
@@ -2273,7 +2264,8 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
else rewriteEqEvidence ev swapped
(mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn
emptyCoHoleSet
- -- emptyCoHoleSet: rhs_redn has no CoercionHoles
+ -- emptyCoHoleSet: we are about to /solve/ this
+ -- constraint, so its CoHoleSet doesn't matter
; let tv_ty = mkTyVarTy tv
final_rhs = reductionReducedType rhs_redn
@@ -2297,45 +2289,48 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
; return (Stop new_ev (text "Solved by unification")) }
---------------------------
--- Unification is off the table
canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
- = do { -- Do checkTypeEq to guarantee (TyEq:OC), (TyEq:F)
+ -- We can't unify, but we can see if this equality can go in the inert set
+ -- and be used to rewrite other constraints.
+ -- See Note [Equalities where unification fails]
+ = do { -- Do checkTypeEqNoUnification to guarantee (TyEq:OC), (TyEq:F)
-- Must do the occurs check even on tyvar/tyvar equalities,
-- in case have x ~ (y :: ..x...); this is #12593.
- ; check_result <- checkTypeEq ev eq_rel lhs rhs
-
- ; let lhs_ty = canEqLHSType lhs
+ ; check_result <- checkTypeEqNoUnification ev eq_rel lhs rhs
; case check_result of
PuFail reason
-
- -- If we had F a ~ G (F a), which gives an occurs check,
- -- then swap it to G (F a) ~ F a, which does not
- -- However `swap_for_size` above will orient it with (G (F a)) on
- -- the left anwyway. `swap_for_rewriting` "wins", but that doesn't
- -- matter: in the occurs check case swap_for_rewriting will be moot.
- -- TL;DR: the next four lines of code are redundant
- -- I'm leaving them here in case they become relevant again
--- | TyFamLHS {} <- lhs
--- , Just can_rhs <- canTyFamEqLHS_maybe rhs
--- , reason `cterHasOnlyProblem` cteSolubleOccurs
--- -> swapAndFinish ev eq_rel swapped lhs_ty can_rhs
--- | otherwise
-
- | reason `cterHasOnlyProblems` do_not_prevent_rewriting
- -> do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs
- ; continueWith $ Right $
- EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
- , eq_lhs = lhs , eq_rhs = rhs }
- }
-
- | otherwise
- -> tryIrredInstead reason ev eq_rel swapped lhs rhs
+ -> -- We can't unify, and this equality should not be used to rewrite
+ -- other constraints (e.g. because it has an occurs check).
+ -- So add it to the inert Irreds.
+ -- NB: The `reason` will never include `cteConcrete` or `cteSkolemEscape`
+ -- because checkTypeEqNoUnification doesn't check for those things;
+ -- they do not prevent the equality being canonical. So you can't
+ -- rely on `reason` reporting those points, nor do we need to.
+ do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs
+ ; finishCanWithIrred (NonCanonicalReason reason) new_ev }
PuOK new_eqs rhs_redn
- -> do { emitWork new_eqs
- ; let new_holes = rewriterSetFromCts new_eqs
+ -> -- Put this constraint into the inert set, so that it will be used
+ -- to solve or rewrite other constraints.
+ --
+ -- NB: checkTypeEqNoUnification does not check for
+ -- (a) skolem-escape (tefTyVar_levelCheck = LC_None)
+ -- (b) concreteness (tefTyVar_concreteCheck = CC_None)
+ -- So an equality whose only problem is e.g. skolem-escape will
+ -- return PuOK, will be put in the inert set, will be used for
+ -- rewriting. That is fine.
+ --
+ -- assertPpr (isEmptyCts new_eqs):
+ -- checkTypeEqNoUnification does neither promotion nor type-family
+ -- flattening for Wanteds, and hence creates no equalities to solve
+ assertPpr (isEmptyCts new_eqs)
+ (vcat [ text "new_eqs" <+> ppr new_eqs
+ , text "rhs_redn" <+> ppr rhs_redn
+ , text "lhs" <+> ppr lhs
+ , text "rhs" <+> ppr rhs ]) $
+ do { let lhs_ty = canEqLHSType lhs
lhs_redn = mkReflRedn (eqRelRole eq_rel) lhs_ty
- ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn new_holes
+ ; new_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn emptyCoHoleSet
-- Important: even if the coercion is Refl,
-- * new_ev has reductionReducedType on the RHS
@@ -2346,45 +2341,56 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
, eq_lhs = lhs
, eq_rhs = reductionReducedType rhs_redn } } }
--- | Some problems prevent /unification/ but not /rewriting/:
---
--- Skolem-escape: if we have [W] alpha[2] ~ Maybe b[3]
--- we can't unify (skolem-escape); but it /is/ canonical,
--- and hence we /can/ use it for rewriting
---
--- Concrete-ness: alpha[conc] ~ b[sk]
--- We can use it to rewrite; we still have to solve the original
-do_not_prevent_rewriting :: CheckTyEqResult
-do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<>
- cteProblem cteConcrete
+checkTypeEqNoUnification :: CtEvidence -> EqRel -> CanEqLHS -> TcType
+ -> TcS (PuResult Ct Reduction)
+-- Used for general CanEqLHSs, when we have decided that we cannot unify
+checkTypeEqNoUnification ev eq_rel lhs rhs =
+ case ev of
+ CtGiven {} ->
+ do { traceTcS "checkTypeEqNoUnification (given) {" (vcat [ text "lhs:" <+> ppr lhs
+ , text "rhs:" <+> ppr rhs ])
+ ; check_result <- wrapTcS (checkTyEqRhs given_flags rhs)
+ ; traceTcS "checkTypeEqNoUnification }" (ppr check_result)
+ ; case check_result of
+ PuFail reason -> return (PuFail reason)
+ PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs
+ ; emitWork new_givens
+ ; updInertSet (addCycleBreakerBindings prs)
+ ; return (pure redn) } }
+ CtWanted {} -> do { traceTcS "checkTypeEqNoUnification (wanted) {" $
+ vcat [ text "lhs:" <+> ppr lhs
+ , text "rhs:" <+> ppr rhs ]
+ ; check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs)
+ ; traceTcS "checkTypeEqNoUnification }" (ppr check_result)
+ ; return check_result }
+ where
+ wanted_flags :: TyEqFlags TcM Ct
+ wanted_flags = notUnifying_TEFTask occ_prob lhs
+ -- See Note [Don't cycle-break Wanteds when not unifying]
+
+ given_flags :: TyEqFlags TcM (TcTyVar, TcType)
+ given_flags = wanted_flags { tef_fam_app = mkTEFA_Break ev eq_rel BreakGiven }
+ -- TEFA_Break used for: [G] a ~ Maybe (F a)
+ -- or [G] F a ~ Maybe (F a)
+
+ -- occ_prob: see Note [Occurs check and representational equality]
+ occ_prob = case eq_rel of
+ NomEq -> cteInsolubleOccurs
+ ReprEq -> cteSolubleOccurs
+
+ ---------------------------
+ mk_new_given :: (TcTyVar, TcType) -> TcS Ct
+ mk_new_given (new_tv, fam_app)
+ = mkNonCanonical . CtGiven <$> newGivenEv cb_loc (given_pred, given_term)
+ where
+ new_ty = mkTyVarTy new_tv
+ given_pred = mkNomEqPred fam_app new_ty
+ given_term = evCoercion $ mkNomReflCo new_ty -- See Detail (4) of Note
-----------------------
-swapAndFinish :: CtEvidence -> EqRel -> SwapFlag
- -> TcType -> CanEqLHS -- ty ~ F tys
- -> TcS (StopOrContinue (Either unused EqCt))
--- We have an equality alpha ~ F tys, that we can't unify e.g because 'tys'
--- mentions alpha, it would not be a canonical constraint as-is.
--- We want to flip it to (F tys ~ a), whereupon it is canonical
-swapAndFinish ev eq_rel swapped lhs_ty can_rhs
- = do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel (flipSwap swapped) can_rhs lhs_ty
- ; continueWith $ Right $
- EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
- , eq_lhs = can_rhs, eq_rhs = lhs_ty } }
+ -- See Detail (7) of the Note
+ cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
----------------------
-tryIrredInstead :: CheckTyEqResult -> CtEvidence
- -> EqRel -> SwapFlag -> CanEqLHS -> TcType
- -> TcS (StopOrContinue (Either IrredCt unused))
--- We have a non-canonical equality
--- We still swap it if 'swapped' says so, so that it is oriented
--- in the direction that the error-reporting machinery
--- expects it; e.g. (m ~ t m) rather than (t m ~ m)
--- This is not very important, and only affects error reporting.
-tryIrredInstead reason ev eq_rel swapped lhs rhs
- = do { traceTcS "cantMakeCanonical" (ppr reason $$ ppr lhs $$ ppr rhs)
- ; new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs
- ; finishCanWithIrred (NonCanonicalReason reason) new_ev }
-
finishCanWithIrred :: CtIrredReason -> CtEvidence
-> TcS (StopOrContinue (Either IrredCt a))
finishCanWithIrred reason ev
@@ -2404,8 +2410,63 @@ canEqReflexive ev eq_rel ty
= do { setEqIfWanted ev (mkReflCPH eq_rel ty)
; stopWith ev "Solved by reflexivity" }
-{- Note [Equalities with heterogeneous kinds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Equalities where unification fails]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we can't unify, but the equality is canonical, we still want to add it to the
+inert set so that it can be used to rewrite other Wanteds. (There are many
+reasons that unification might not happen: the LHS is not a touchable unification
+variable, it has rewriters, it's a Given etc.)
+
+* In this case we call `checkTypeEqNoUnification` to see whether it is canonical
+ (which in turn calls `checkTypeEqRhs` with suitable flags).
+
+* NB: we do /not/ try to take advantage of the case where
+ `canEqCanLHSFinish_try_unification` has already called `checkTyEqRhs`; doing so
+ caused #27844. (The first call did fam-app breaking, which concealed a genuine
+ occurs check.) It's just too clever; better to do the simple thing.
+
+Note [Don't cycle-break Wanteds when not unifying]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ [W] a[2] ~ Maybe (F a[2])
+
+Should we cycle-break this Wanted, thus?
+
+ [W] a[2] ~ Maybe delta[2]
+ [W] delta[2] ~ F a[2]
+
+For a start, this is dodgy because we might just unify delta, thus undoing
+what we have done, and getting an infinite loop in the solver. Even if we
+somehow prevented ourselves from doing so, is there any merit in the split?
+Maybe: perhaps we can use that equality on `a` to unlock other constraints?
+Consider
+ type instance F (Maybe _) = Bool
+
+ [G] g1: a ~ Maybe Bool
+ [W] w1: a ~ Maybe (F a)
+
+If we loop-break w1 to get
+ [W] w1': a ~ Maybe gamma
+ [W] w3: gamma ~ F a
+Now rewrite w3 with w1'
+ [W] w3': gamma ~ F (Maybe gamma)
+Now use the type instance to get
+ gamma := Bool
+Now we are left with
+ [W] w1': a ~ Maybe Bool
+which we can solve from the Given.
+
+BUT in this situation we could have rewritten the
+/original/ Wanted from the Given, like this:
+ [W] w1': Maybe Bool ~ Maybe (F (Maybe Bool))
+and that is readily soluble.
+
+In short: loop-breaking Wanteds, when we aren't unifying,
+seems of no merit. Hence TEFA_Recurse, rather than TEFA_Break,
+in `wanted_flags` in `checkTypeEqNoUnification`.
+
+Note [Equalities with heterogeneous kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
What do we do when we have an equality
(tv :: k1) ~ (rhs :: k2)
@@ -2587,8 +2648,8 @@ The details depend on whether we're working with a Given or a Wanted.
Given
-----
We emit a new Given, [G] F a ~ cbv, equating the type family application
-to our new cbv. This is actually done by `break_given` in
-`GHC.Tc.Solver.Monad.checkTypeEq`.
+to our new cbv. This is actually done by `BreakGiven` in the `given_flags`
+in `checkTypeEqNoUnification`.
Note its orientation: The type family ends up on the left; see
Note [Orienting TyFamLHS/TyFamLHS]. No special treatment for
@@ -2629,7 +2690,7 @@ Note that
Wanted
------
First, we do not cycle-break unless the LHS is a unifiable type variable
-See Note [Don't cycle-break Wanteds when not unifying] in GHC.Tc.Solver.Monad.
+See Note [Don't cycle-break Wanteds when not unifying].
OK, so suppose the LHS is a unifiable type variable. The fresh cycle-breaker
variables here must actually be normal, touchable metavariables. That is, they
@@ -3073,11 +3134,10 @@ inertsEqsCanDischarge inerts (EqCt { eq_lhs = lhs_w, eq_rhs = rhs_w
|| (empty_rw_w && not (isEmptyCoHoleSet (ctEvRewriters ev_i)))
-- Prefer the one that has no rewriters
-- See (CE4) in Note [Combining equalities]
+ -- and (WRW10) in Note [Wanteds rewrite Wanteds: rewriter-sets]
inertsEqsCanDischarge _ _ = Nothing
-
-
{- Note [Do not unify Givens]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this GADT match
@@ -3143,34 +3203,6 @@ Wrinkles:
we should kick out `co` so that we can now unify it, which might
unlock other stuff. See `kickOutAfterFillingCoercionHole` in
GHC.Tc.Solver.Monad.
-
-Note [Solve by unification]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If we solve
- alpha[n] ~ ty
-by unification, there are two cases to consider
-
-* TouchableSameLevel: if the ambient level is 'n', then
- we can simply update alpha := ty, and do nothing else
-
-* TouchableOuterLevel free_metas n: if the ambient level is greater than
- 'n' (the level of alpha), in addition to setting alpha := ty we must
- do two other things:
-
- 1. Promote all the free meta-vars of 'ty' to level n. After all,
- alpha[n] is at level n, and so if we set, say,
- alpha[n] := Maybe beta[m],
- we must ensure that when unifying beta we do skolem-escape checks
- etc relevant to level n. Simple way to do that: promote beta to
- level n.
-
- 2. Set the Unification Level Flag to record that a level-n unification has
- taken place. See Note [WhatUnifications] in GHC.Tc.Utils.Unify
-
-NB: TouchableSameLevel is just an optimisation for TouchableOuterLevel. Promotion
-would be a no-op, and setting the unification flag unnecessarily would just
-make the solver iterate more often. (We don't need to iterate when unifying
-at the ambient level because of the kick-out mechanism.)
-}
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -22,7 +22,7 @@ module GHC.Tc.Solver.InertSet (
InertEqs,
foldTyEqs, delEq, findEq,
partitionInertEqs, partitionFunEqs, transformAndPartitionTyVarEqs,
- filterInertEqs, filterFunEqs,
+ filterInertEqs, filterFunEqs, transformAndPartitionFunEqs,
foldFunEqs, addEqToCans,
-- * Inert Dicts
@@ -128,7 +128,7 @@ Further refinements:
* Among the equalities we prioritise ones with an empty rewriter set;
see Note [Wanteds rewrite Wanteds: rewriter-sets] in GHC.Tc.Types.Constraint,
- wrinkle (WRW8).
+ wrinkle (WRW7).
* Among equalities with an empty rewriter set, we prioritise nominal equalities.
* They have more rewriting power, so doing them first is better.
@@ -983,7 +983,7 @@ How do we establish these conditions?
with S(fw,_).
* (T3) is guaranteed by an occurs-check on the work item.
- This is done during canonicalisation, in checkTypeEq; invariant
+ This is done during canonicalisation, in checkTyEqRhs; invariant
(TyEq:OC) of CEqCan. See also Note [EqCt occurs check] in GHC.Tc.Types.Constraint.
* (T4) is established by GHC.Tc.Solver.Monad.kickOutRewritable. If the inert
@@ -1422,6 +1422,19 @@ addCanFunEq old_eqs fun_tc fun_args ct
foldFunEqs :: (EqCt -> b -> b) -> FunEqMap EqualCtList -> b -> b
foldFunEqs k fun_eqs z = foldTcAppMap (\eqs z -> foldr k z eqs) fun_eqs z
+transformAndPartitionFunEqs
+ :: (EqCt -> Either EqCt EqCt) -- Left => chuck out, Right => keep
+ -> InertFunEqs
+ -> ([EqCt], InertFunEqs) -- (chuck-out, keep)
+transformAndPartitionFunEqs pred orig_inerts
+ = foldFunEqs folder orig_inerts ([], emptyFunEqs)
+ where
+ folder :: EqCt -> ([EqCt], InertFunEqs) -> ([EqCt], InertFunEqs)
+ folder eq_ct (acc_true, acc_false)
+ = case pred eq_ct of
+ Left eq_ct' -> (eq_ct' : acc_true, acc_false)
+ Right eq_ct' -> (acc_true, addFunEqs eq_ct' acc_false)
+
partitionFunEqs :: (EqCt -> Bool) -- EqCt will have a TyFamLHS
-> InertFunEqs
-> ([EqCt], InertFunEqs)
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -117,10 +117,7 @@ module GHC.Tc.Solver.Monad (
getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS,
matchFam, matchFamTcM,
checkWellLevelledDFun,
- pprEq,
-
- -- Enforcing invariants for type equalities
- checkTypeEq
+ pprEq
) where
import GHC.Prelude
@@ -438,10 +435,12 @@ why solving `kco` might unlock `co`, especially (URW2).
Hence `kickOutAfterFillingCoercionHole`. It looks at inert constraints that are
* Wanted
- * Of the form alpha ~ rhs, where alpha is a unification variable
-and kicks out any that will have an empty rewriter set after filling the hole.
+ * Of the form (alpha ~ rhs), or (F tys ~ alpha)
+ where alpha is a unification variable
+and kicks out any that have an empty rewriter set after filling the hole.
Wrinkles:
+
(KOC1) If co's rewriter-set is {kco, xco}, there is no point in kicking it out,
because it still can't be unified. So we only kick out if the co's
rewriter-set becomes empty.
@@ -455,13 +454,17 @@ Wrinkles:
on `kco2` instead of `kco`. Hence the `new_holes` passed to
`kickOutAfterFillingCoercionHole`
-(KOC3) It's possible that this could just go ahead and unify, but could there
- be occurs-check problems? Seems simpler just to kick out.
+(KOC3) It's possible that this could just go ahead and unify on the spot, but could
+ there be occurs-check problems? Seems simpler just to kick out.
(KOC4) Kick-out is undesirable, so it'd be better to solve `kco` before `co`. So
the solver prioritises equalities with an empty rewriter set, to try to
avoid unnecessary kick-out. See GHC.Tc.Types.Constraint
Note [Prioritise Wanteds with empty CoHoleSet] esp (PER1)
+
+(KOC5) We kick out from both `inert_eqs` and `inert_funeqs`. The latter is needed
+ in case we have (F tys ~ alpha), which might (if it now has an empty rewriter
+ set) allow unifying alpha.
-}
kickOutRewritable :: KickOutSpec -> CtFlavourRole -> TcS ()
@@ -526,23 +529,32 @@ kickOutAfterFillingCoercionHole hole (CPH { cph_holes = new_holes })
; setInertCans ics' }
where
kick_out :: InertCans -> ([EqCt], InertCans)
- kick_out ics@(IC { inert_eqs = eqs })
- = (eqs_to_kick, ics { inert_eqs = eqs_to_keep })
+ kick_out ics@(IC { inert_eqs = eqs, inert_funeqs = funeqs })
+ = ( kick_funeqs ++ kick_eqs
+ , ics { inert_eqs = keep_eqs, inert_funeqs = keep_funeqs })
where
- (eqs_to_kick, eqs_to_keep) = transformAndPartitionTyVarEqs kick_out_eq eqs
+ (kick_eqs, keep_eqs) = transformAndPartitionTyVarEqs kick_out_eq eqs
+ (kick_funeqs, keep_funeqs) = transformAndPartitionFunEqs kick_out_eq funeqs
+ -- Kick out from funeqs as well as eqs.
+ -- See (KOC5) in Note [Kick out after filling a coercion hole]
+
+ is_meta_tv_equality (EqCt { eq_lhs = lhs, eq_rhs = rhs })
+ | TyVarLHS tv <- lhs = isMetaTyVar tv
+ | Just tv <- getTyVar_maybe rhs = isMetaTyVar tv
+ | otherwise = False
kick_out_eq :: EqCt -> Either EqCt EqCt
- kick_out_eq eq_ct@(EqCt { eq_ev = ev, eq_lhs = lhs })
+ kick_out_eq eq_ct@(EqCt { eq_ev = ev })
| CtWanted (wev@(WantedCt { ctev_rewriters = rewriters })) <- ev
- , TyVarLHS tv <- lhs
- , isMetaTyVar tv
, hole `elemCoHoleSet` rewriters
- , let holes' = (rewriters `delCoHoleSet` hole) `mappend` new_holes
- -- Adding new_holes and deleting hole: see (KOC2)
- eq_ct' = eq_ct { eq_ev = CtWanted (wev { ctev_rewriters = holes' }) }
- = if isEmptyCoHoleSet holes'
+ , is_meta_tv_equality eq_ct
+ , let rewriters' = (rewriters `delCoHoleSet` hole) `mappend` new_holes
+ -- Adding new_holes and deleting hole: see (KOC2)
+ eq_ct' = eq_ct { eq_ev = CtWanted (wev { ctev_rewriters = rewriters' }) }
+ = if isEmptyCoHoleSet rewriters'
then Left eq_ct' -- Kick out, if new rewriter set is empty (KOC1)
else Right eq_ct' -- Keep, but with trimmed holes see (KOC2)
+
| otherwise
= Right eq_ct
@@ -2302,52 +2314,6 @@ wrapUnifier rws loc role do_unifications
************************************************************************
-}
-checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType
- -> TcS (PuResult Ct Reduction)
--- Used for general CanEqLHSs, ones that do
--- not have a touchable type variable on the LHS (i.e. not unifying)
-checkTypeEq ev eq_rel lhs rhs =
- case ev of
- CtGiven {} ->
- do { traceTcS "checkTypeEq {" (vcat [ text "lhs:" <+> ppr lhs
- , text "rhs:" <+> ppr rhs ])
- ; check_result <- wrapTcS (checkTyEqRhs given_flags rhs)
- ; traceTcS "checkTypeEq }" (ppr check_result)
- ; case check_result of
- PuFail reason -> return (PuFail reason)
- PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs
- ; emitWork new_givens
- ; updInertSet (addCycleBreakerBindings prs)
- ; return (pure redn) } }
- CtWanted {} -> wrapTcS (checkTyEqRhs wanted_flags rhs)
- where
- wanted_flags :: TyEqFlags TcM Ct
- wanted_flags = notUnifying_TEFTask occ_prob lhs
- -- checkTypeEq deals only with the non-unifying case
-
- given_flags :: TyEqFlags TcM (TcTyVar, TcType)
- given_flags = wanted_flags { tef_fam_app = mkTEFA_Break ev eq_rel BreakGiven }
- -- TEFA_Break used for: [G] a ~ Maybe (F a)
- -- or [W] F a ~ Maybe (F a)
-
- -- occ_prob: see Note [Occurs check and representational equality]
- occ_prob = case eq_rel of
- NomEq -> cteInsolubleOccurs
- ReprEq -> cteSolubleOccurs
-
- ---------------------------
- mk_new_given :: (TcTyVar, TcType) -> TcS Ct
- mk_new_given (new_tv, fam_app)
- = mkNonCanonical . CtGiven <$> newGivenEv cb_loc (given_pred, given_term)
- where
- new_ty = mkTyVarTy new_tv
- given_pred = mkNomEqPred fam_app new_ty
- given_term = evCoercion $ mkNomReflCo new_ty -- See Detail (4) of Note
-
- -- See Detail (7) of the Note
- cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
-
--------------------------
-- | Fill in CycleBreakerTvs with the variables they stand for.
-- See Note [Type equality cycles] in GHC.Tc.Solver.Equality
restoreTyVarCycles :: InertSet -> TcM ()
@@ -2363,43 +2329,4 @@ restoreTyVarCycles is
(a ~R# b a) is soluble if b later turns out to be Identity
So we treat this as a "soluble occurs check".
-Note [Don't cycle-break Wanteds when not unifying]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consdier
- [W] a[2] ~ Maybe (F a[2])
-
-Should we cycle-break this Wanted, thus?
-
- [W] a[2] ~ Maybe delta[2]
- [W] delta[2] ~ F a[2]
-
-For a start, this is dodgy because we might just unify delta, thus undoing
-what we have done, and getting an infinite loop in the solver. Even if we
-somehow prevented ourselves from doing so, is there any merit in the split?
-Maybe: perhaps we can use that equality on `a` to unlock other constraints?
-Consider
- type instance F (Maybe _) = Bool
-
- [G] g1: a ~ Maybe Bool
- [W] w1: a ~ Maybe (F a)
-
-If we loop-break w1 to get
- [W] w1': a ~ Maybe gamma
- [W] w3: gamma ~ F a
-Now rewrite w3 with w1'
- [W] w3': gamma ~ F (Maybe gamma)
-Now use the type instance to get
- gamma := Bool
-Now we are left with
- [W] w1': a ~ Maybe Bool
-which we can solve from the Given.
-
-BUT in this situation we could have rewritten the
-/original/ Wanted from the Given, like this:
- [W] w1': Maybe Bool ~ Maybe (F (Maybe Bool))
-and that is readily soluble.
-
-In short: loop-breaking Wanteds, when we aren't unifying,
-seems of no merit. Hence TEFA_Recurse, rather than TEFA_Break,
-in `wanted_flags` in `checkTypeEq`.
-}
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -524,7 +524,7 @@ isInsolubleReason (InsolubleFunDepReason {}) = True
------------------------------------------------------------------------------
-- | A /set/ of problems in checking the validity of a type equality.
--- See 'checkTypeEq'.
+-- See 'GHC.Tc.Utils.Unify.checkTyEqRhs'.
newtype CheckTyEqResult = CTER Word8
-- | No problems in checking the validity of a type equality.
@@ -2623,19 +2623,24 @@ The rewriter-set plan
thereby dropping the reference to `co`. I'm not certain whether this actually
happens or not.
-(WRW7) In error reporting, we simply suppress any errors that have been rewritten
- by /unsolved/ wanteds. This suppression happens in GHC.Tc.Errors.mkErrorItem,
+(WRW7) When we fill a coercion hole `h` we kick out any inert Wanted that has `h`
+ in its rewriter set. See `kickOutAfterFilling CoercionHole`.
+ See Note [Kick out after filling a coercion hole] in GHC.Tc.Solver.Monad.
+
+ Furthermore, when we select a work item, in `selectNextWorkItem` we zonk the
+ rewriter set so that it accurately reflects the unsolved coercion holes. That
+ sets it up ready for the no-rewriter check in (WR5), when we process the equality.
+
+ In `selectNextWorkItem`, we also prioritise equalities with no rewiters.
+ See Note [Prioritise Wanteds with empty CoHoleSet] in GHC.Tc.Types.Constraint
+ wrinkle (PER1).
+
+(WRW8) In error reporting, we suppress any errors that have been rewritten
+ by /unsolved/ wanteds. This suppression happens in `GHC.Tc.Errors.mkErrorItem`,
which uses `GHC.Tc.Zonk.Type.zonkCoHoleSet` to look through any filled
coercion holes. The idea is that we wish to report the "root cause" -- the
error that rewrote all the others.
-(WRW8) In `selectNextWorkItem`, priorities equalities with no rewiters. See
- Note [Prioritise Wanteds with empty CoHoleSet] in GHC.Tc.Types.Constraint
- wrinkle (PER1).
-
-(WRW9) In error reporting, we prioritise Wanteds that have an empty CoHoleSet:
- see Note [Prioritise Wanteds with empty CoHoleSet].
-
Let's continue our first example above:
inert: [W] w1 :: a ~ Char
@@ -2661,8 +2666,10 @@ Wrinkles:
(WRW11) When zonking a constraint (with `zonkCt` and `zonkCtEvidence`) we take
the opportunity to zonk its `CoHoleSet`, which eliminates solved ones.
- This doesn't guarantee that rewriter sets are always up to date -- c.f.
- (WRW10) -- but it helps, and it de-clutters debug output.
+ This doesn't guarantee that rewriter sets are always up to date (c.f. (WRW10))
+ but it helps, and it de-clutters debug output.
+
+ See also (WRW7) which does the crucial just-in-time zonking of the rewriters.
Note [Prioritise Wanteds with empty CoHoleSet]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2705,9 +2712,8 @@ in our simplify_loop iteration, we happened to start with co_aym. All would have
been well if we'd started with the (not-rewritten) co_ayb and gotten it into the
inert set.
-With that in mind, we /prioritise/ the work-list to put
-constraints with no rewriters first. This prioritisation
-is done in `GHC.Tc.Solver.Monad.selectNextWorkItem`.
+With that in mind, we /prioritise/ the work-list to put constraints with no rewriters
+first. This prioritisation is done in `GHC.Tc.Solver.Monad.selectNextWorkItem`.
Wrinkles
@@ -2720,8 +2726,8 @@ Wrinkles
order to report /some/ error in this case, we simply report all the
Wanteds. The user will get a perhaps-confusing error message, but they've
written a confusing program! (T22707 and T22793 were close, but they do
- not exhibit this behaviour.) So belt and braces: see the `suppress`
- stuff in GHC.Tc.Errors.mkErrorItem.
+ not exhibit this behaviour.) So belt and braces:
+ see `GHC.Tc.Errors.reportWanteds`.
Note [Avoiding rewriting cycles]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -3617,15 +3617,20 @@ instance Outputable SimpleUnifyResult where
simpleUnifyCheck :: UnifyCheckCaller -> TcLevel -> TcTyVar -> TcType -> SimpleUnifyResult
-- ^ A fast check for unification. May return "not sure", in which case
-- unification might still be OK, but it'll take more work to do
--- (use the full 'checkTypeEq').
+-- (use the full 'checkTyEqRhs').
--
--- * Rejects if lhs_tv occurs in rhs_ty (occurs check)
--- * Rejects foralls unless
--- lhs_tv is RuntimeUnk (used by GHCi debugger)
--- or is a QL instantiation variable
--- * Rejects a non-concrete type if lhs_tv is concrete
--- * Rejects type families unless fam_ok=True
--- * Does a level-check for type variables, to avoid skolem escape
+-- It returns SUC_CannotUnify for
+-- * Touchability failure
+-- * Top level-shape failure
+--
+-- It returns SUC_NotSure for
+-- * Occurs check: lhs_tv occurs in rhs_ty
+-- * Type families unless fam_ok=True
+-- * Foralls unless
+-- lhs_tv is RuntimeUnk (used by GHCi debugger)
+-- or is a QL instantiation variable
+-- * Concreteness: lhs_tv is concrete and rhs is a non-concrete type
+-- * Skolem-escape: a level-check for type variables, to avoid skolem escape
--
-- This function is pretty heavily used, so it's optimised not to allocate
simpleUnifyCheck caller given_eq_lvl lhs_tv rhs
@@ -3753,8 +3758,8 @@ Consider
[W] alpha[2] ~ Maybe (S beta[4] gamma[2])
We don't want to promote beta to level 2; rather, we should
-expand the synonym. (Currently, in checkTypeEqRhs promotion
-is irrevocable, by side effect.)
+expand the synonym. (Currently, in `checkTyEqRhs` promotion
+is irrevocable, by side effect in `promote` in `checkTyVar`.)
To avoid this risk we eagerly expand forgetful synonyms.
This also means we won't get an occurs check in
@@ -4198,7 +4203,7 @@ famAppArgFlags flags = case flags of
The key function `checkTyEqRhs ty_eq_flags rhs` is called on the
RHS of a type equality
lhs ~ rhs
-and checks to see if `rhs` satisfies, or can be made to satisfy,
+and checks to see if `rhs` satisfies, /or can be made to satisfy/,
invariants described by `ty_eq_flags`. It can succeded or fail; in
the latter case it returns a `CheckTyEqResult` that describes why it
failed.
@@ -4219,6 +4224,15 @@ Notably, it can check for things like:
* Concreteness error
e.g. alpha[conc] ~ r[sk]
+Note "or can be made to satisfy the preconditions"! `checkTyEqRhs` may transform
+the RHS by
+
+ * Turning a type-family application into a type variable, perhaps to avoid
+ an occurs check. See Note Note [Family applications in canonical constraints]
+
+ * Promoting any nested unification variables, in order to satisfy the
+ level invariant. See Note [Promotion and level-checking]
+
Its specific behaviour is governed by the `TyEqFlags` that are passed
to it; see Note [TyEqFlags].
@@ -4275,7 +4289,7 @@ NB: We never see a TyVarLHS here, such as
[G] a ~ F tys here
because we'd have swapped it to
[G] F tys ~ a
-in canEqCanLHS2, before getting to checkTypeEq.
+in canEqCanLHS2, before getting to checkTyEqRhs.
-}
check_ty_eq_rhs :: forall m a
@@ -4799,7 +4813,6 @@ promote_meta_tyvar info dest_lvl occ_tv
touchabilityTest :: TcLevel -> TcTyVar -> Bool
-- ^ This is the key test for untouchability:
-- See Note [Unification preconditions] in GHC.Tc.Utils.Unify
--- and Note [Solve by unification] in GHC.Tc.Solver.Equality
--
-- @True@ <=> the variable is touchable
touchabilityTest given_eq_lvl tv
=====================================
testsuite/tests/indexed-types/should_fail/T9662.stderr
=====================================
@@ -1,12 +1,12 @@
T9662.hs:49:8: error: [GHC-25897]
- ā¢ Couldn't match type ānā with āIntā
+ ā¢ Couldn't match type āmā with āIntā
Expected: Exp (((sh :. k) :. m) :. n)
-> Exp (((sh :. m) :. n) :. k)
Actual: Exp
(Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
-> Exp
(Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int))
- ānā is a rigid type variable bound by
+ āmā is a rigid type variable bound by
the type signature for:
test :: forall sh k m n.
Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
=====================================
testsuite/tests/typecheck/should_fail/T27844.hs
=====================================
@@ -0,0 +1,14 @@
+-- Repro.hs
+-- The call to f forces c ~ (b, F c) inside the scope of the skolem b.
+-- Correct behaviour: a type error at the first argument of const
+-- (as GHC 9.12.4 reports).
+
+{-# LANGUAGE RankNTypes, TypeFamilies #-}
+module T27844 where
+
+type family F a
+
+f :: (forall b. b -> (b, F c)) -> c -> ()
+f _ _ = ()
+
+g x = f (\_ -> const x (show x)) x
=====================================
testsuite/tests/typecheck/should_fail/T27844.stderr
=====================================
@@ -0,0 +1,12 @@
+T27844.hs:14:22: error: [GHC-25897]
+ ā¢ Couldn't match expected type ā(b, F c)ā with actual type ācā
+ ācā is a rigid type variable bound by
+ the inferred type of g :: Show c => c -> ()
+ at T27844.hs:14:1-34
+ ā¢ In the first argument of āconstā, namely āxā
+ In the expression: const x (show x)
+ In the first argument of āfā, namely ā(\ _ -> const x (show x))ā
+ ā¢ Relevant bindings include
+ x :: c (bound at T27844.hs:14:3)
+ g :: c -> () (bound at T27844.hs:14:1)
+
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -763,3 +763,4 @@ test('T26861', normal, compile_fail, [''])
test('T26862', normal, compile_fail, [''])
test('T27210', normal, compile_fail, [''])
test('T26532', normal, compile_fail, [''])
+test('T27844', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/96911a123bfa84f5e3b079b1ea27ef1ā¦
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/96911a123bfa84f5e3b079b1ea27ef1ā¦
You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help
1
0
[Git][ghc/ghc][ghc-9.12] 12 commits: Never make an absent filler for a constraint type
by Magnus (ļ¼ MangoIV) 07 Oct '26
by Magnus (ļ¼ MangoIV) 07 Oct '26
07 Oct '26
Magnus pushed to branch ghc-9.12 at Glasgow Haskell Compiler / GHC
Commits:
c6e59f2b by Simon Peyton Jones at 2026-09-09T11:54:37+02:00
Never make an absent filler for a constraint type
mkAbsentFiller used isTerminatingType to decide, but that is not enough.
Consider
class Eq a => UC a where {}
let u :: UC Int -- UC Int is a "non-terminating type"
u = error "Absent"
let e :: Eq Int -- Eq Int is a "terminating type"
e = $p1UC u
We clearly must not make a filler for `e`, because we speculatively
evaluate it. But speculatively evaluating `e` forces `u`, so we must not
make one for `u` either.
Asking isDictTy instead is not enough either, because it does not catch a
constraint hidden behind an unreduced type family application:
type family F a :: Constraint
type instance F W = TC W
a :: F W => Int -> Int -- (F W) argument is absent
Oops! Entered absent arg Arg: irred
Type: F W
So play safe and use isPredTy: never make an absent filler for any
constraint-kinded type.
Fixes #27627
(cherry picked from commit 7bf546fc423e23cb649580016ee494efbfe144ab)
- - - - -
adb4ddfc by Zubin Duggal at 2026-09-09T11:54:37+02:00
Add tests for absent fillers at dictionary types
T27627 a unary class whose superclass is a non-unary class
T27627a ...whose superclass is a Constraint-kinded type family
T27627b ...whose superclass is a quantified constraint
T27627c a unary class applied to itself, (UC (UC (TC a)))
T27627e a (forall b. P b) dictionary that loops
(cherry picked from commit 5f474953d1880232b5e6c5741f08746e28cd25ab)
- - - - -
6b758dcb by Zubin Duggal at 2026-09-09T11:54:37+02:00
An abstract TyCon may hide a unary class
A class declared in an hs-boot file is an AbstractTyCon inside the
module loop, and compiling the real declaration may reveal it to be a
UnaryClassTyCon.
- isTerminatingType returned True for such AbstractTyCons
- IfaceToCore set the unary flag to False in the DFunId
So we could end up speculating bottom dictionaries because inside a module
loop we see an UnaryClassTyCon as an AbstractTyCon
Use isTerminatingTyCon, which returns False for an abstract TyCon.
The Bool in DFunId is now a cache for isTerminatingTyCon, set in
mkDFunIdDetails.
Fixes #27704
Note by the backporter (mangoiv): we're backporting by the fact that
a tycon is a unary type class con IFF it is a type class con and a
newtype prior to 9bd7fcc518111a1549c98720c222cdbabd32ed46.
(cherry picked from commit db1e0bda5c3209d75133fa9e2560d684f35f950b)
- - - - -
e1dc869f by Zubin Duggal at 2026-09-09T11:54:37+02:00
Specialise: don't replace dead args with absent fillers
specHeader decides an argument is dead by calling isDeadBinder on a binder of
the /optimised RHS/, then applies the filler to the /stable unfolding/
template instead. The two may differ, so the argument can be dead in
the RHS and not in the template.
The specialised function's unfolding then has an absent filler, and any call
site that inlines it evaluates the error thunk.
Dropping dead args in the specialiser is rarely worth it, to quote Simon,
"The later worker/wrapper pass will pick up the dead arg later if it is really dead. Keeps the specialiser simpler."
So instead of trying to check if the arg really is dead in the stable unfolding,
just drop the logic for dropping dead args in the specialiser altogeher.
Fixes #27703
(cherry picked from commit 2b3cdef64bbc535bd72e3dfb512b4cfd10a72ca2)
- - - - -
d7ad1bc4 by Zubin Duggal at 2026-09-09T11:54:38+02:00
CorePrep: don't speculate a call across an hs-boot edge
We take care not to evaluate things that might be bottom, like a
looping dictionary group, but our analysis is defeated by boot files.
We only track recursion within a module, so two dictionaries that
depend on each other across a module loop each look non-recursive, and
we might speculate them.
Any recursion we cannot see must cross an hs-boot edge, so refuse to
speculate calls that cross one.
Fixes #27717
(cherry picked from commit 664efc76286c475e0fcd1c1624e847831e7fc07a)
- - - - -
1e956205 by Ben Gamari at 2026-09-09T15:01:09+02:00
base: Don't drop exception context in SomeException(toException)
For reasons that are lost to time, the implementation of [CLC #200]
that was merged inappropriately dropped `ExceptionContext` in the
`toException` implementation given to `SomeException`.
Fix this infelicity.
[CLC #200]: https://github.com/haskell/core-libraries-committee/issues/200
(cherry picked from commit 2ab02c579a9625438f5281a258051cb32ba40004)
- - - - -
1ad61a58 by Zubin Duggal at 2026-09-09T15:01:09+02:00
DmdAnal: Fix maxDmdType
We need to eta expand the smaller DmdType using defaultArgDmd, like in lubDmdType.
Introduce zipDmdType as a common combinator to implement both maxDmdType and lubDmdType
uniformly.
fixes #27626
(cherry picked from commit e31885816b7c597ad89b05da64b21c5a241bf674)
- - - - -
1ee1b27b by Zubin Duggal at 2026-09-09T15:01:09+02:00
hadrian: Fix links to remaining doc sites to not use the package hash for haddock links
In 07267f79d91169f474cacc8bcd38d76a6e97887d we changed hadrian to not include the package hash in the haddock
directory. This patch takes care of a few remaining links that were missed in that patch
Fixes #27671
(cherry picked from commit 1446bb039a635f2b836be19f062cbffa568fe4c5)
- - - - -
4dcd9f77 by Luite Stegeman at 2026-09-09T15:01:09+02:00
rts: Fix missing memory barrier in eval_thunk_selector (#27477)
unchain_thunk_selectors() was missing an ACQUIRE_LOAD for the
indirectee, leading to segfaults and corruption during GC on
weakly-ordered architectures.
Fixes #27477
(cherry picked from commit 06eee015be4e361fe9cb33e8a608ab2ea1386b52)
- - - - -
1bb7dce4 by mangoiv at 2026-09-10T11:09:05+02:00
testsuite: allow metric decrease in WWRec
Metric Decrease:
T15164
WWRec
- - - - -
00e79136 by mangoiv at 2026-09-17T16:50:56+02:00
Fix a scoping error in Specialise
This small patch fixes #26329, which triggered a scoping error.
Test is in T21391, with -fpolymorphic-specialisation enabled
mangoiv(backported): Another test added for #27766 (T27766)
Fixes #27766
(cherry picked from commit b62491405ae851ae514afe18d51f0fe7fbefebf3)
- - - - -
087fbaa9 by mangoiv at 2026-10-06T12:27:47+02:00
ci: update signatories for root key for cabal-install 3.8
- - - - -
95 changed files:
- .gitlab/ci.sh
- + Repro019_minimal.hs
- + changelog.d/27626
- + changelog.d/27627
- + changelog.d/27703
- + changelog.d/27704
- + changelog.d/27717
- + changelog.d/T27455
- + changelog.d/fix-parallel-gc-selector-race-27477
- compiler/GHC/Core.hs
- compiler/GHC/Core/Opt/Specialise.hs
- compiler/GHC/Core/Opt/WorkWrap/Utils.hs
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Utils.hs
- compiler/GHC/CoreToStg/Prep.hs
- compiler/GHC/IfaceToCore.hs
- compiler/GHC/Types/Demand.hs
- compiler/GHC/Types/Id/Info.hs
- compiler/GHC/Types/Id/Make.hs
- compiler/GHC/Types/Literal.hs
- docs/index.html.in
- docs/users_guide/ghc_config.py.in
- hadrian/src/Rules/Generate.hs
- libraries/base/changelog.md
- libraries/ghc-internal/src/GHC/Internal/Exception/Type.hs
- rts/sm/Evac.c
- + testsuite/tests/core-to-stg/T27627/Callee.hs
- + testsuite/tests/core-to-stg/T27627/Caller.hs
- + testsuite/tests/core-to-stg/T27627/Main.hs
- + testsuite/tests/core-to-stg/T27627/T27627.stdout
- + testsuite/tests/core-to-stg/T27627/all.T
- + testsuite/tests/core-to-stg/T27627a/Callee.hs
- + testsuite/tests/core-to-stg/T27627a/Caller.hs
- + testsuite/tests/core-to-stg/T27627a/Main.hs
- + testsuite/tests/core-to-stg/T27627a/T27627a.stdout
- + testsuite/tests/core-to-stg/T27627a/all.T
- + testsuite/tests/core-to-stg/T27627b/Callee.hs
- + testsuite/tests/core-to-stg/T27627b/Caller.hs
- + testsuite/tests/core-to-stg/T27627b/Main.hs
- + testsuite/tests/core-to-stg/T27627b/T27627b.stdout
- + testsuite/tests/core-to-stg/T27627b/all.T
- + testsuite/tests/core-to-stg/T27627c/Callee.hs
- + testsuite/tests/core-to-stg/T27627c/Caller.hs
- + testsuite/tests/core-to-stg/T27627c/Main.hs
- + testsuite/tests/core-to-stg/T27627c/T27627c.stdout
- + testsuite/tests/core-to-stg/T27627c/all.T
- + testsuite/tests/core-to-stg/T27627e.hs
- + testsuite/tests/core-to-stg/T27627e.stdout
- + testsuite/tests/core-to-stg/T27627f/Callee.hs
- + testsuite/tests/core-to-stg/T27627f/Caller.hs
- + testsuite/tests/core-to-stg/T27627f/Inst.hs
- + testsuite/tests/core-to-stg/T27627f/Main.hs
- + testsuite/tests/core-to-stg/T27627f/T27627f.stdout
- + testsuite/tests/core-to-stg/T27627f/all.T
- + testsuite/tests/core-to-stg/T27704/Callee.hs
- + testsuite/tests/core-to-stg/T27704/Callee.hs-boot
- + testsuite/tests/core-to-stg/T27704/Main.hs
- + testsuite/tests/core-to-stg/T27704/Mid.hs
- + testsuite/tests/core-to-stg/T27704/T27704.stdout
- + testsuite/tests/core-to-stg/T27704/all.T
- + testsuite/tests/core-to-stg/T27704a/Callee.hs
- + testsuite/tests/core-to-stg/T27704a/Callee.hs-boot
- + testsuite/tests/core-to-stg/T27704a/Main.hs
- + testsuite/tests/core-to-stg/T27704a/Mid.hs
- + testsuite/tests/core-to-stg/T27704a/T27704a.stdout
- + testsuite/tests/core-to-stg/T27704a/all.T
- + testsuite/tests/core-to-stg/T27717/Callee.hs
- + testsuite/tests/core-to-stg/T27717/Callee.hs-boot
- + testsuite/tests/core-to-stg/T27717/Main.hs
- + testsuite/tests/core-to-stg/T27717/Mid.hs
- + testsuite/tests/core-to-stg/T27717/T27717.stdout
- + testsuite/tests/core-to-stg/T27717/Ty.hs
- + testsuite/tests/core-to-stg/T27717/all.T
- testsuite/tests/core-to-stg/all.T
- + testsuite/tests/dmdanal/should_run/M2.hs
- + testsuite/tests/dmdanal/should_run/T27626.hs
- + testsuite/tests/dmdanal/should_run/T27626.stdout
- testsuite/tests/dmdanal/should_run/all.T
- testsuite/tests/ghc-e/should_fail/T18441fail7.stderr
- testsuite/tests/ghc-e/should_fail/T9930fail.stderr
- testsuite/tests/ghc-e/should_run/ghc-e005.stderr
- + testsuite/tests/rts/T27477.hs
- + testsuite/tests/rts/T27477.stdout
- testsuite/tests/rts/all.T
- testsuite/tests/simplCore/should_compile/T17966.stderr
- + testsuite/tests/simplCore/should_compile/T27766.hs
- testsuite/tests/simplCore/should_compile/T7785.stderr
- testsuite/tests/simplCore/should_compile/all.T
- testsuite/tests/simplCore/should_compile/spec004.hs
- testsuite/tests/simplCore/should_compile/spec004.stderr
- + testsuite/tests/simplCore/should_run/T27703/Lib.hs
- + testsuite/tests/simplCore/should_run/T27703/Main.hs
- + testsuite/tests/simplCore/should_run/T27703/T27703.stdout
- + testsuite/tests/simplCore/should_run/T27703/all.T
The diff was not included because it is too large.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/abf7c3be17628108e5d70108a7089cā¦
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/abf7c3be17628108e5d70108a7089cā¦
You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help
1
0
[Git][ghc/ghc][wip/andrea/with-signal-handlers] added changelog
by Andrea Vezzosi (ļ¼ trac-Saizan) 07 Oct '26
by Andrea Vezzosi (ļ¼ trac-Saizan) 07 Oct '26
07 Oct '26
Andrea Vezzosi pushed to branch wip/andrea/with-signal-handlers at Glasgow Haskell Compiler / GHC
Commits:
f78b3075 by Andrea Vezzosi at 2026-10-07T13:38:16+02:00
added changelog
- - - - -
1 changed file:
- + changelog.d/T4162
Changes:
=====================================
changelog.d/T4162
=====================================
@@ -0,0 +1,18 @@
+section: compiler
+issues: #4162
+mrs: !16774
+synopsis:
+ runGhc/runGhcT no longer hijack process signals, withSignalHandlers still does
+ but fixed to handle multiple threads.
+description:
+ Functions runGhc/runGhcT no longer go out of their way to redirect process
+ signals as exceptions to them.
+
+ The installed handlers make it so other threads are unaware of any signals,
+ which can cause the process to become unresponsive whenever a crash of the GHC
+ session(s) does not cascade into a shutdown of the process itself.
+
+ The old behaviour is available through `runGhcWithSignalHandlers` or using
+ `withSignalHandlers` directly. The latter is also fixed so the installed
+ signal handlers throw exceptions to all the threads that are inside
+ `withSignalHandlers`, not only the first thread that entered.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f78b3075601d322fe10e8971189ff4eā¦
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f78b3075601d322fe10e8971189ff4eā¦
You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help
1
0
07 Oct '26
Simon Peyton Jones pushed to branch wip/T27828 at Glasgow Haskell Compiler / GHC
Commits:
3e346260 by Simon Peyton Jones at 2026-10-07T12:31:57+01:00
Refactor fundeps again
This MR fixes #27828; there was a bad scoping error in `trim_qtvs`.
The main changes are
* Refactor `trim_qtvs` completely to eliminate the bug.
* Remove a redundant `apartnessCheck` from `mkTopOpenFamEqFDs`.
* Lots of improvements to the Notes in FunDeps.hs
I also did a couple of pure refactors:
* I realised that we were carefully caching `cab_incomps` in each
`CoAxBranch`, to make it more efficient to reduce a type family application,
but we were not doing the same thing when computing relevance for functional
dependencies; see Note [Relevance] in GHC.Tc.Solver.FunDeps. So I added
`cab_overlaps`, which is now used in `noEarlierMatch`.
* Use a proper data types, `AmIUnifying` and `OuterKindsFlag`, for two
previously-Boolean arguments to `tc_unify_tys`. This is a pure refactor.
- - - - -
15 changed files:
- + changelog.d/T27828
- compiler/GHC/Builtin/WiredIn/Types/Box.hs
- compiler/GHC/Core/Coercion/Axiom.hs
- compiler/GHC/Core/FamInstEnv.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/Iface/Decl.hs
- compiler/GHC/Iface/Syntax.hs
- compiler/GHC/IfaceToCore.hs
- compiler/GHC/Tc/Instance/FunDeps.hs
- compiler/GHC/Tc/Solver/FunDeps.hs
- compiler/GHC/Tc/TyCl.hs
- + testsuite/tests/indexed-types/should_compile/T27828.hs
- + testsuite/tests/indexed-types/should_compile/T27828a.hs
- + testsuite/tests/indexed-types/should_compile/T27828b.hs
- testsuite/tests/indexed-types/should_compile/all.T
Changes:
=====================================
changelog.d/T27828
=====================================
@@ -0,0 +1,8 @@
+section: compiler
+synopsis: Fix a "No skolem info" compiler crash
+issues: #27828
+mrs: !16714
+
+description: {
+ There was a bug in the implementation of functional dependencies for type families.
+}
=====================================
compiler/GHC/Builtin/WiredIn/Types/Box.hs
=====================================
@@ -329,7 +329,8 @@ mkWiredInNewTyCon tc_name dc_name nt_co_uniq bndrs roles nt_fld_ty =
, cab_roles = roles
, cab_lhs = mkTyVarTys tvs
, cab_rhs = nt_fld_ty
- , cab_incomps = [] }
+ , cab_overlaps = []
+ , cab_incomps = [] }
-- | The wired-in @Box@ newtype:
--
=====================================
compiler/GHC/Core/Coercion/Axiom.hs
=====================================
@@ -18,7 +18,7 @@ module GHC.Core.Coercion.Axiom (
coAxiomSingleBranch, coAxBranchTyVars, coAxBranchCoVars,
coAxBranchRoles,
coAxBranchLHS, coAxBranchRHS, coAxBranchSpan, coAxBranchIncomps,
- placeHolderIncomps,
+ placeHolderIncomps, placeHolderOverlaps,
Role(..),
@@ -195,23 +195,44 @@ mapAccumBranches f (MkBranches arr)
Note [Storing compatibility]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-During axiom application, we need to be aware of which branches are compatible
-with which others. The full explanation is in Note [Compatibility] in
-GHc.Core.FamInstEnv. (The code is placed there to avoid a dependency from
-GHC.Core.Coercion.Axiom on the unification algorithm.) Although we could
-theoretically compute compatibility on the fly, this is silly, so we store it
-in a CoAxiom.
+A `CoAxBranch` caches some useful information in `cab_incomps` and `cab_overlaps`:
-Specifically, each branch refers to all other branches with which it is
-incompatible. This list might well be empty, and it will always be for the
-first branch of any axiom.
+* `cab_overlaps`: when computing "relevance", in the function
+ `GHC.Tc.Solver.FunDeps.getRelevantBranches`, we need to know which ealier branches
+ can match this one -- see `noEarlierMatch`.
-CoAxBranches that do not (yet) belong to a CoAxiom should have a panic thunk
-stored in cab_incomps. The incompatibilities are properly a property of the
-axiom as a whole, and they are computed only when the final axiom is built.
+ Again we could look at all earlier branches, but instead we cache in `cab_overlaps`
+ a list of all earlier branches that could overlap with this one.
-During serialization, the list is converted into a list of the indices
-of the branches.
+* `cab_incomps`: during axiom application, we need to be aware of which branches are
+ /compatible/ with which others. The full explanation is in Note [Compatibility] in
+ GHC.Core.FamInstEnv. (The code is placed there to avoid a dependency from
+ GHC.Core.Coercion.Axiom on the unification algorithm.)
+
+ Although we could readily compute compatibility on the fly, this is silly, so we
+ cache in `cab_incomps` a list of earlier branches that are /incompatible/ with
+ this one. (See Note [Compatibility] for a definition.)
+
+ Always a sub-list of `cab_overlaps`.
+
+Both lists can be empty, and always are for the first branch of any axiom.
+
+Some extra points:
+
+(SC1) A `CoAxBranch` that does not (yet) belong to a CoAxiom is initialised with panic
+ thunks, `placeHolderOverlaps` or `placeHolderIncomps`, for the two fields; see `mkCoAxBranch`.
+
+ Then, when a bunch of branches is grouped together in an axiom, we analyse the
+ branches as a whole and initialise the fields properly, using `computeAxiomIncomps`.
+ (For open type families, whose axioms have only one branch, we null out both lists
+ with `noAxiomIncomps`.)
+
+(SC2) We don't need to serialise `cab_overlaps` and `cab_incomps` into an interface
+ file, because we recompute them in `computeAxiomIncomps`. However, annoyingly,
+ the pretty printer converts to IfaceSyn before printing, and we do want to show
+ `cab_incomps` (see Note [Displaying axiom incompatibilities]). So, tiresomely,
+ `IfaceAxBranch` has a `ifaxbIncomps` field, used only for printing. For historical
+ reasons this is actually serialised. Yuk.
Note [CoAxioms are homogeneous]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -230,7 +251,9 @@ This is checked in FamInstEnv.mkCoAxBranch.
-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism] in GHC.Core.Lint
data CoAxiom br
- = CoAxiom -- Type equality axiom.
+ = -- `br` is Unbranched for each of the many axioms of an open type family
+ -- Branched for the single multi-branch axiom of a closed type family
+ CoAxiom -- Type equality axiom.
{ co_ax_unique :: Unique -- Unique identifier
, co_ax_name :: Name -- Name for pretty-printing
, co_ax_role :: Role -- Role of the axiom's equality
@@ -268,8 +291,15 @@ data CoAxBranch
, cab_rhs :: Type
-- ^ Right-hand side of the equality
-- See Note [CoAxioms are homogeneous]
+
+ , cab_overlaps :: [CoAxBranch]
+ -- ^ The preceding branches whose LHSs are /unify with/ this one
+ -- Order is unimportant
+ -- See Note [Storing compatibility]
+
, cab_incomps :: [CoAxBranch]
- -- ^ The previous incompatible branches
+ -- ^ The preceding branches that are /incompatible/ with this one
+ -- Order is unimportant
-- See Note [Storing compatibility]
}
deriving Data.Data
@@ -342,8 +372,9 @@ coAxBranchIncomps :: CoAxBranch -> [CoAxBranch]
coAxBranchIncomps = cab_incomps
-- See Note [Compatibility] in GHC.Core.FamInstEnv
-placeHolderIncomps :: [CoAxBranch]
-placeHolderIncomps = panic "placeHolderIncomps"
+placeHolderIncomps, placeHolderOverlaps :: [CoAxBranch]
+placeHolderIncomps = panic "placeHolderIncomps"
+placeHolderOverlaps = panic "placeHolderOverlaps"
{-
Note [CoAxBranch type variables]
=====================================
compiler/GHC/Core/FamInstEnv.hs
=====================================
@@ -19,7 +19,7 @@ module GHC.Core.FamInstEnv (
FamInstMatch(..),
lookupFamInstEnv, lookupFamInstEnvConflicts, lookupFamInstEnvByTyCon,
- isDominatedBy, apartnessCheck, compatibleBranches,
+ isDominatedBy, apartnessCheck, noEarlierMatchCheck, compatibleBranches,
-- Injectivity
InjectivityCheckResult(..),
@@ -487,20 +487,45 @@ in GHC.Core.Unify.)
Note [Compatibility]
~~~~~~~~~~~~~~~~~~~~
-Two patterns are /compatible/ if either of the following conditions hold:
-1) The patterns are apart.
-2) The patterns unify with a substitution S, and their right hand sides
-equal under that substitution.
+Consider a closed type family with two equations (X1) and (X2)
+ type family F a where
+ F lhs1 = rhs1 -- (X1)
+ ...
+ F lhs2 = rhs2 -- (X2)
+ ...
+Then equations (X1) and (X2) are /compatible/ if any target (F ty) that
+matches both equations yields the very same right hand side. Example:
+ And True True = True
+ And a True = a
+The target (And True True) matches both equations but they then both
+produce the same reduct True.
+
+More precisely (X1) and (X2) are /compatible/ iff
+ If LHSs unify with a substitution S, then S(rhs1) = S(rhs2)
+
+Conversely, (X1) and (X2) are /incompatible/ if
+ Their LHSs unify with S, and S(rhs1) /= S(rhs2)
For open type families, only compatible instances are allowed. For closed
-type families, the story is slightly more complicated. Consider the following:
+families, we use the Closed Family Matching Rule (see function `findBranch`):
-type family F a where
- F Int = Bool
- F a = Int
+ When looking up a target (F ty) in a closed type family F,
+ find an equation (branch) such that:
+ * the LHS matches the target
+ * the target is apart from every previous /incompatible/ equation for F
-g :: Show a => a -> F a
-g x = length (show x)
+We don't need to check the earlier equations that are compatible with the
+matching equation, because they are either irrelevant (clause 1 of compatible)
+or benign (clause 2 of compatible).
+
+Some examples:
+
+ type family F a where
+ F Int = Bool
+ F a = Int
+
+ g :: Show a => a -> F a
+ g x = length (show x)
Should that type-check? No. We need to allow for the possibility that 'a'
might be Int and therefore 'F a' should be Bool. We can simplify 'F a' to Int
@@ -516,12 +541,12 @@ potentially-overlapping group is closed.
As another example, consider this:
-type family G x where
- G Int = Bool
- G a = Double
+ type family G x where
+ G Int = Bool
+ G a = Double
-type family H y
--- no instances
+ type family H y
+ -- no instances
Now, we want to simplify (G (H Char)). We can't, because (H Char) might later
simplify to be Int. So, (G (H Char)) is stuck, for now.
@@ -529,18 +554,13 @@ simplify to be Int. So, (G (H Char)) is stuck, for now.
While everything above is quite sound, it isn't as expressive as we'd like.
Consider this:
-type family J a where
- J Int = Int
- J a = a
+ type family J a where
+ J Int = Int
+ J a = a
Can we simplify (J b) to b? Sure we can. Yes, the first equation matches if
b is instantiated with Int, but the RHSs coincide there, so it's all OK.
-
-So, the rule is this: when looking up a branch in a closed type family, we
-find a branch that matches the target, but then we make sure that the target
-is apart from every previous *incompatible* branch. We don't check the
-branches that are compatible with the matching branch, because they are either
-irrelevant (clause 1 of compatible) or benign (clause 2 of compatible).
+Hence the Closed Family Matching Rule.
Note [Compatibility of eta-reduced axioms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -572,15 +592,32 @@ fails anyway.
-- See Note [Compatibility]
compatibleBranches :: CoAxBranch -> CoAxBranch -> Bool
-compatibleBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
- (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
+compatibleBranches b1 b2
+ = case compareBranches b1 b2 of
+ BC_Apart -> True
+ BC_Compat -> True
+ BC_Incompat -> False
+
+data BranchCompatibility
+ = BC_Apart -- LHSs are apart
+ | BC_Compat -- LHSs unify with S, and S(rhs1)=S(rhs2)
+ | BC_Incompat -- LHSs unify with S, and S(rhs1)/=S(rhs2)
+
+compareBranches :: CoAxBranch -> CoAxBranch -> BranchCompatibility
+compareBranches (CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
+ (CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
= 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
- MaybeApart {} -> False
- Unifiable subst -> Type.substTyAddInScope subst rhs1 `eqType`
+ SurelyApart -> BC_Apart
+ Unifiable subst | Type.substTyAddInScope subst rhs1 `eqType`
Type.substTyAddInScope subst rhs2
+ -> BC_Compat
+ | otherwise
+ -> BC_Incompat
+ MaybeApart {} -> BC_Incompat
+ -- An occurs check yields MaybeApart;
+ -- see Note [Infinitary substitutions] in GHC.Core.Unify
where
(commonlhs1, commonlhs2) = zipAndUnzip lhs1 lhs2
-- See Note [Compatibility of eta-reduced axioms]
@@ -603,8 +640,7 @@ injectiveBranches injectivity
ax1@(CoAxBranch { cab_lhs = lhs1, cab_rhs = rhs1 })
ax2@(CoAxBranch { cab_lhs = lhs2, cab_rhs = rhs2 })
-- See Note [Verifying injectivity annotation], case 1.
- = case tcUnifyTysForInjectivity True [rhs1] [rhs2] of
- -- True = two-way pre-unification
+ = case tcUnifyTysForInjectivity Unifying [rhs1] [rhs2] of
Nothing -> InjectivityAccepted
-- RHS are different, so equations are injective.
-- This is case 1A from Note [Verifying injectivity annotation]
@@ -629,10 +665,11 @@ injectiveBranches injectivity
lhs1Subst = Type.substTys subst (getInjArgs lhs1)
lhs2Subst = Type.substTys subst (getInjArgs lhs2)
--- takes a CoAxiom with unknown branch incompatibilities and computes
--- the compatibilities
--- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom
computeAxiomIncomps :: [CoAxBranch] -> [CoAxBranch]
+-- Takes a CoAxiom for a closed type family that has place-holder
+-- `cab_incomps` and `cab_overlaps` fields, and computes those fields
+-- properly from the list of branches.
+-- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom
computeAxiomIncomps branches
= snd (mapAccumL go [] branches)
where
@@ -640,11 +677,23 @@ computeAxiomIncomps branches
go prev_brs cur_br
= (new_br : prev_brs, new_br)
where
- new_br = cur_br { cab_incomps = mk_incomps prev_brs cur_br }
-
- mk_incomps :: [CoAxBranch] -> CoAxBranch -> [CoAxBranch]
- mk_incomps prev_brs cur_br
- = filter (not . compatibleBranches cur_br) prev_brs
+ (overlaps,incomps) = get_cab [] [] prev_brs
+ new_br = cur_br { cab_overlaps = overlaps, cab_incomps = incomps }
+
+ get_cab :: [CoAxBranch] -> [CoAxBranch] -- Accumulators
+ -> [CoAxBranch]
+ -> ([CoAxBranch], [CoAxBranch])
+ get_cab overlaps incomps [] = (overlaps,incomps)
+ get_cab overlaps incomps (br:brs)
+ = case compareBranches cur_br br of
+ BC_Apart -> get_cab overlaps incomps brs
+ BC_Compat -> get_cab (br:overlaps) incomps brs
+ BC_Incompat -> get_cab (br:overlaps) (br:incomps) brs
+
+noAxiomIncomps :: CoAxBranch -> CoAxBranch
+-- Overwrite the placeholders for `cab_incomps` and `cab_overlaps`
+-- with [], because unbranched axioms have no "preceding" equations
+noAxiomIncomps branch = branch { cab_incomps = [], cab_overlaps = [] }
{-
************************************************************************
@@ -715,14 +764,17 @@ mkCoAxBranch :: [TyVar] -- original, possibly stale, tyvars
-> SrcSpan
-> CoAxBranch
mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc
- = CoAxBranch { cab_tvs = tvs'
- , cab_eta_tvs = eta_tvs'
- , cab_cvs = cvs'
- , cab_lhs = tidyTypes env lhs
- , cab_roles = roles
- , cab_rhs = tidyType env rhs
- , cab_loc = loc
- , cab_incomps = placeHolderIncomps }
+ = CoAxBranch { cab_tvs = tvs'
+ , cab_eta_tvs = eta_tvs'
+ , cab_cvs = cvs'
+ , cab_lhs = tidyTypes env lhs
+ , cab_roles = roles
+ , cab_rhs = tidyType env rhs
+ , cab_loc = loc
+
+ -- See (SC1) in Note [Storing compatibility]
+ , cab_overlaps = placeHolderOverlaps
+ , cab_incomps = placeHolderIncomps }
where
(env1, tvs') = tidyVarBndrs init_tidy_env tvs
(env2, eta_tvs') = tidyVarBndrs env1 eta_tvs
@@ -736,14 +788,16 @@ mkCoAxBranch tvs eta_tvs cvs lhs rhs roles loc
-- all of the following code is here to avoid mutual dependencies with
-- Coercion
-mkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
-mkBranchedCoAxiom ax_name fam_tc branches
+mkBranchedCoAxiom :: Role -> Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched
+mkBranchedCoAxiom role ax_name fam_tc branches
= CoAxiom { co_ax_unique = nameUnique ax_name
, co_ax_name = ax_name
, co_ax_tc = fam_tc
- , co_ax_role = Nominal
+ , co_ax_role = role
, co_ax_implicit = False
, co_ax_branches = manyBranches (computeAxiomIncomps branches) }
+ -- computeAxiomIncomps: see (SC1) in
+ -- Note [Storing compatibility]
mkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched
mkUnbranchedCoAxiom ax_name fam_tc branch
@@ -752,7 +806,9 @@ mkUnbranchedCoAxiom ax_name fam_tc branch
, co_ax_tc = fam_tc
, co_ax_role = Nominal
, co_ax_implicit = False
- , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
+ , co_ax_branches = unbranched (noAxiomIncomps branch) }
+ -- noAxiomIncomps: see (SC1) in
+ -- Note [Storing compatibility]
mkSingleCoAxiom :: Role -> Name
-> [TyVar] -> [TyVar] -> [CoVar]
@@ -767,7 +823,9 @@ mkSingleCoAxiom role ax_name tvs eta_tvs cvs fam_tc lhs_tys rhs_ty
, co_ax_tc = fam_tc
, co_ax_role = role
, co_ax_implicit = False
- , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
+ , co_ax_branches = unbranched (noAxiomIncomps branch) }
+ -- noAxiomIncomps: see (SC1) in
+ -- Note [Storing compatibility]
where
branch = mkCoAxBranch tvs eta_tvs cvs lhs_tys rhs_ty
(map (const Nominal) tvs)
@@ -785,7 +843,9 @@ mkNewTypeCoAxiom name tycon tvs roles rhs_ty
, co_ax_implicit = True -- See Note [Implicit axioms] in GHC.Core.TyCon
, co_ax_role = Representational
, co_ax_tc = tycon
- , co_ax_branches = unbranched (branch { cab_incomps = [] }) }
+ , co_ax_branches = unbranched (noAxiomIncomps branch) }
+ -- noAxiomIncomps: see (SC1) in
+ -- Note [Storing compatibility]
where
branch = mkCoAxBranch tvs [] [] (mkTyVarTys tvs) rhs_ty
roles (getSrcSpan name)
@@ -1223,7 +1283,9 @@ findBranch :: Array BranchIndex CoAxBranch
-> Maybe (BranchIndex, [Type], [Coercion])
-- coercions relate requested types to returned axiom LHS at role N
findBranch branches target_tys
- = foldr go Nothing (assocs branches)
+ = -- Implements the Closed Family Matching Rule
+ -- in Note [Compatibility]
+ foldr go Nothing (assocs branches)
where
go :: (BranchIndex, CoAxBranch)
-> Maybe (BranchIndex, [Type], [Coercion])
@@ -1258,6 +1320,20 @@ apartnessCheck target (CoAxBranch { cab_incomps = incomps })
isSurelyApart SurelyApart = True
isSurelyApart _ = False
+-- | Check whether an earlier branch matches these target types
+noEarlierMatchCheck
+ :: [Type]
+ -> CoAxBranch -- ^ The candidate equation we wish to use
+ -> Bool -- ^ True <=> equation can fire
+noEarlierMatchCheck target (CoAxBranch { cab_overlaps = overlaps })
+ -- NB: this is the /only/ use of the `cab_overlaps` field
+ -- See Note [Storing compatibility] and
+ -- (RW4) in Note [Relevance]
+ = not (any matches overlaps)
+ where
+ matches earlier_branch
+ = isJust (tcMatchTys (coAxBranchLHS earlier_branch) target)
+
{-
************************************************************************
* *
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -9,6 +9,7 @@ module GHC.Core.Unify (
tcMatchTyX_BM, ruleMatchTyKiX,
-- Side-effect free unification
+ AmIUnifying(..),
tcUnifyTy, tcUnifyTys, tcUnifyFunDeps, tcUnifyDebugger,
tcUnifyTysFG, tcUnifyTysForInjectivity,
BindTvFun, BindFamFun, BindFlag(..),
@@ -597,14 +598,14 @@ tcMatchTyX_BM :: HasDebugCallStack
=> BindTvFun -> Subst
-> Type -> Type -> Maybe Subst
tcMatchTyX_BM bind_tv subst ty1 ty2
- = tc_match_tys_x bind_tv False subst [ty1] [ty2]
+ = tc_match_tys_x bind_tv IgnoreOuterKinds 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 :: HasDebugCallStack => Type -> Type -> Maybe Subst
tcMatchTyKi ty1 ty2
- = tc_match_tys alwaysBindTv True [ty1] [ty2]
+ = tc_match_tys alwaysBindTv CheckOuterKinds [ty1] [ty2]
-- | This is similar to 'tcMatchTy', but extends a substitution
-- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -614,7 +615,7 @@ tcMatchTyX :: HasDebugCallStack
-> Type -- ^ Target
-> Maybe Subst
tcMatchTyX subst ty1 ty2
- = tc_match_tys_x alwaysBindTv False subst [ty1] [ty2]
+ = tc_match_tys_x alwaysBindTv IgnoreOuterKinds subst [ty1] [ty2]
-- | Like 'tcMatchTy' but over a list of types.
-- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -625,7 +626,7 @@ tcMatchTys :: HasDebugCallStack
-- variables could be free in the target
-- See (CU6) in Note [The Core unifier]
tcMatchTys tys1 tys2
- = tc_match_tys alwaysBindTv False tys1 tys2
+ = tc_match_tys alwaysBindTv IgnoreOuterKinds tys1 tys2
-- | Like 'tcMatchTyKi' but over a list of types.
-- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -635,7 +636,7 @@ tcMatchTyKis :: HasDebugCallStack
-> Maybe Subst -- ^ One-shot substitution
-- See (CU6) in Note [The Core unifier]
tcMatchTyKis tys1 tys2
- = tc_match_tys alwaysBindTv True tys1 tys2
+ = tc_match_tys alwaysBindTv CheckOuterKinds tys1 tys2
-- | Like 'tcMatchTys', but extending a substitution
-- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -645,7 +646,7 @@ tcMatchTysX :: HasDebugCallStack
-> [Type] -- ^ Target
-> Maybe Subst -- ^ One-shot substitution
tcMatchTysX subst tys1 tys2
- = tc_match_tys_x alwaysBindTv False subst tys1 tys2
+ = tc_match_tys_x alwaysBindTv IgnoreOuterKinds subst tys1 tys2
-- | Like 'tcMatchTyKis', but extending a substitution
-- See also Note [tcMatchTy vs tcMatchTyKi]
@@ -655,12 +656,12 @@ tcMatchTyKisX :: HasDebugCallStack
-> [Type] -- ^ Target
-> Maybe Subst -- ^ One-shot substitution
tcMatchTyKisX subst tys1 tys2
- = tc_match_tys_x alwaysBindTv True subst tys1 tys2
+ = tc_match_tys_x alwaysBindTv CheckOuterKinds subst tys1 tys2
-- | Same as tc_match_tys_x, but starts with an empty substitution
tc_match_tys :: HasDebugCallStack
=> BindTvFun
- -> Bool -- ^ match kinds?
+ -> OuterKindsFlag -- ^ Match kinds?
-> [Type]
-> [Type]
-> Maybe Subst
@@ -672,7 +673,7 @@ tc_match_tys bind_me match_kis tys1 tys2
-- | Worker for 'tcMatchTysX' and 'tcMatchTyKisX'
tc_match_tys_x :: HasDebugCallStack
=> BindTvFun
- -> Bool -- ^ match kinds?
+ -> OuterKindsFlag -- ^ Match kinds?
-> Subst
-> [Type]
-> [Type]
@@ -680,8 +681,8 @@ tc_match_tys_x :: HasDebugCallStack
tc_match_tys_x bind_tv match_kis (Subst in_scope id_env tv_env cv_env) tys1 tys2
= case tc_unify_tys neverBindFam -- (ATF7) in Note [Apartness and type families]
bind_tv
- False -- Matching, not unifying
- False -- Not an injectivity check
+ Matching -- Matching, not unifying
+ False -- Not an injectivity check
match_kis
RespectMultiplicities
(mkRnEnv2 in_scope) tv_env cv_env tys1 tys2 of
@@ -706,9 +707,9 @@ ruleMatchTyKiX tmpl_tvs rn_env tenv tmpl target
-- 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
+ Matching -- Matching, not unifying
False -- No doing an injectivity check
- True -- Match the kinds
+ CheckOuterKinds -- Match the kinds
IgnoreMultiplicities
-- See Note [Rewrite rules ignore multiplicities in FunTy]
rn_env tenv emptyCvSubstEnv [tmpl] [target] of
@@ -784,7 +785,7 @@ tcUnifyTy t1 t2 = tcUnifyTys alwaysBindTv [t1] [t2]
tcUnifyDebugger :: Type -> Type -> Maybe Subst
tcUnifyDebugger t1 t2
= case tc_unify_tys_fg
- True -- Unify kinds
+ CheckOuterKinds -- Unify kinds
neverBindFam -- Does not affect Unifiable, so pick max efficient
-- See (ATF8) in Note [Apartness and type families]
alwaysBindTv
@@ -798,7 +799,7 @@ tcUnifyFunDeps :: TyCoVarSet
-> Maybe Subst
tcUnifyFunDeps qtvs tys1 tys2
= case tc_unify_tys_fg
- True -- Unify kinds
+ CheckOuterKinds -- Unify kinds
dontCareBindFam -- Class-instance heads never mention type families
(matchBindTv qtvs)
tys1 tys2 of
@@ -821,7 +822,7 @@ tcUnifyTysForInjectivity unif tys1 tys2
= case tc_unify_tys alwaysBindFam alwaysBindTv
unif -- Am I unifying?
True -- Do injectivity checks
- False -- Don't check outermost kinds
+ IgnoreOuterKinds -- Don't check outermost kinds
RespectMultiplicities
rn_env emptyTvSubstEnv emptyCvSubstEnv
tys1 tys2 of
@@ -838,8 +839,9 @@ tcUnifyTysForInjectivity unif tys1 tys2
-- should never actually be done
maybe_fix tv_subst
- | unif = niFixSubst in_scope tv_subst
- | otherwise = mkTvSubst in_scope tv_subst
+ = case unif of
+ Unifying -> niFixSubst in_scope tv_subst
+ Matching -> mkTvSubst in_scope tv_subst
-- When matching, don't confuse domain with range; no fixpoint!
-----------------
@@ -866,15 +868,15 @@ tcUnifyTysFG :: BindFamFun -> BindTvFun
-> [Type] -> [Type]
-> UnifyResult
tcUnifyTysFG bind_fam bind_tv tys1 tys2
- = tc_unify_tys_fg False bind_fam bind_tv tys1 tys2
+ = tc_unify_tys_fg IgnoreOuterKinds bind_fam bind_tv tys1 tys2
-tc_unify_tys_fg :: Bool
+tc_unify_tys_fg :: OuterKindsFlag
-> 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
+ Unifying
False -- Not doing an injectivity check
match_kis -- Match outer kinds
RespectMultiplicities rn_env
@@ -888,10 +890,10 @@ tc_unify_tys_fg match_kis bind_fam bind_tv tys1 tys2
-- | 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
+ -> AmIUnifying -- ^ Unifying or matching
+ -> Bool -- ^ True <=> doing an injectivity check
+ -> OuterKindsFlag -- ^ Check outer kinds or not
+ -> MultiplicityFlag -- ^ see Note [Rewrite rules ignore multiplicities in FunTy] in GHC.Core.Unify
-> RnEnv2
-> TvSubstEnv -- ^ substitution to extend
-> CvSubstEnv
@@ -910,8 +912,9 @@ tc_unify_tys :: BindFamFun -> BindTvFun
-- 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
+ do { case match_kis of
+ CheckOuterKinds -> unify_tys env kis1 kis2
+ IgnoreOuterKinds -> return ()
; unify_tys env tys1 tys2 }
where
env = UMEnv { um_bind_tv_fun = bind_tv
@@ -926,6 +929,11 @@ tc_unify_tys bind_fam bind_tv unif inj_check match_kis match_mults rn_env tv_env
kis2 = map typeKind tys2
+data OuterKindsFlag
+ = CheckOuterKinds -- Unify or match the /kind/ of the two types
+ | IgnoreOuterKinds -- Just unify or match the types, ignoring kinds
+ -- (typically, we already know they are equal)
+
{- *********************************************************************
* *
UnifyResult, MaybeApart etc
@@ -1583,8 +1591,7 @@ c.f. Note [Comparing type synonyms] in GHC.Core.TyCo.Compare
-------------- unify_ty: the main workhorse -----------
-type AmIUnifying = Bool -- True <=> Unifying
- -- False <=> Matching
+data AmIUnifying = Matching | Unifying
type InType = Type -- Before applying the RnEnv2
type OutCoercion = Coercion -- After applying the RnEnv2
@@ -1618,7 +1625,7 @@ unify_ty env (CastTy ty1 co1) ty2 kco
-- See (KCU1) in Note [Kind coercions in Unify]
= maybeApart MARCast -- See (KCU2)
- | um_unif env
+ | Unifying <- um_unif env
= unify_ty env ty1 ty2 (co1 `mkTransCo` kco)
| otherwise -- We are matching, not unifying
@@ -1661,7 +1668,7 @@ unify_ty env (CoercionTy co1) (CoercionTy co2) kco
= do { c_subst <- getCvSubstEnv
; case co1 of
CoVarCo cv
- | not (um_unif env)
+ | Matching <- 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
@@ -1682,7 +1689,7 @@ 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
+ | Unifying <- um_unif env -- If unifying, can swap args; but not when matching
= uVarOrFam (umSwapRn env) (TyVarLHS tv2) ty1 (mkSymCo kco)
-- Deal with TyConApps
@@ -1692,7 +1699,7 @@ unify_ty env ty1 ty2 kco
| Just (tc,tys) <- mb_sat_fam_app1
= uVarOrFam env (TyFamLHS tc tys) ty2 kco
- | um_unif env
+ | Unifying <- um_unif env
, Just (tc,tys) <- mb_sat_fam_app2
= uVarOrFam (umSwapRn env) (TyFamLHS tc tys) ty1 (mkSymCo kco)
@@ -1820,7 +1827,7 @@ uVarOrFam env ty1 ty2 kco
go swapped substs lhs@(TyVarLHS 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
+ if | Unifying <- um_unif env -> unify_ty env ty1' ty2 kco
| (ty1' `mkCastTy` kco) `tcEqType` ty2 -> return ()
| otherwise -> surelyApart
-- Unifying: recurse into unify_ty
@@ -1842,9 +1849,9 @@ uVarOrFam env ty1 ty2 kco
| TyVarTy tv2 <- ty2
, let tv2' = umRnOccR env tv2
, tv1' == tv2'
- = if | um_unif env -> return ()
- | tv1_is_bindable -> extendTvEnv tv1' ty2
- | otherwise -> return ()
+ = if | Unifying <- um_unif env -> return ()
+ | tv1_is_bindable -> extendTvEnv tv1' ty2
+ | otherwise -> return ()
| tv1_is_bindable
, not (mentionsForAllBoundTyVarsR env ty2_fvs)
@@ -1858,9 +1865,9 @@ uVarOrFam env ty1 ty2 kco
-- 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
+ | Unifying <- um_unif env
, NotSwapped <- swapped -- If we have swapped already, don't do so again
- , Just lhs2 <- canEqLHS_maybe ty2
+ , Just lhs2 <- canEqLHS_maybe ty2
= go IsSwapped substs lhs2 (mkTyVarTy tv1) (mkSymCo kco)
| occurs_check = maybeApart MARInfinite -- Occurs check
@@ -1879,7 +1886,9 @@ uVarOrFam env ty1 ty2 kco
| otherwise
= False
- occurs_check = um_unif env && uOccursCheck substs foralld_tvs lhs rhs
+ occurs_check = case um_unif env of
+ Unifying -> uOccursCheck substs foralld_tvs lhs rhs
+ Matching -> False
-- Occurs check, only when unifying
-- see Note [Infinitary substitutions]
-- Make sure you include `kco` in rhs #14846
@@ -1893,7 +1902,7 @@ uVarOrFam env ty1 ty2 kco
-- Hence the RnEnv2 is empty
| not under_forall
, Just ty1' <- lookupFamEnv (um_fam_env substs) tc1 tys1
- = if | um_unif env -> unify_ty env ty1' ty2 kco
+ = if | Unifying <- um_unif env -> unify_ty env ty1' ty2 kco
-- Below here we are matching
-- The return () case deals with:
-- Template: (F a)..(F a)
@@ -1930,9 +1939,9 @@ uVarOrFam env ty1 ty2 kco
-- NB: a type family can appear on the template when matching
-- see (ATF6) in Note [Apartness and type families]
-- (Only worth doing this if we are not under a forall.)
- | um_unif env
+ | Unifying <- um_unif env
, NotSwapped <- swapped
- , Just lhs2 <- canEqLHS_maybe ty2
+ , Just lhs2 <- canEqLHS_maybe ty2
= go IsSwapped substs lhs2 (mkTyConApp tc1 tys1) (mkSymCo kco)
| otherwise -- See (ATF5) in Note [Apartness and type families]
@@ -1962,9 +1971,9 @@ uVarOrFam env ty1 ty2 kco
(inj_tys2, noninj_tys2) = partitionByList inj tys2
bind_fam_if_poss
- | not (um_unif env) -- Not when matching (ATF11-1)
+ | Matching <- um_unif env -- Not when matching (ATF11-1)
= return ()
- | under_forall -- Not under a forall (ATF3)
+ | under_forall -- Not under a forall (ATF3)
= return ()
| BindMe <- um_bind_fam_fun env tc tys1 rhs1
= unless (uOccursCheck substs emptyVarSet (TyFamLHS tc tys1) rhs1) $
=====================================
compiler/GHC/Iface/Decl.hs
=====================================
@@ -112,7 +112,7 @@ coAxBranchToIfaceBranch tc lhs_s
, ifaxbRoles = roles
, ifaxbRHS = toIfaceType rhs
, ifaxbIncomps = iface_incomps }
- where
+ where
iface_incomps = map (expectJust
. flip findIndex lhs_s
. eqTypes
=====================================
compiler/GHC/Iface/Syntax.hs
=====================================
@@ -338,7 +338,12 @@ data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars :: [IfaceTvBndr]
, ifaxbRoles :: [Role]
, ifaxbRHS :: IfaceType
, ifaxbIncomps :: [BranchIndex] }
- -- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom
+ -- We store the incompatibilities in IfaceAxBranch
+ -- just for (perhaps unnecessary) display purposes:
+ -- see Note [Displaying axiom incompatibilities]
+ -- When we construct a real CoAxBranch we compute cab_incomps directly
+ -- from the equations, ignoring the ifaxbIncomps.
+ -- We could consider getting rid of ifaxbIncomps altogether.
data IfaceConDecls
= IfAbstractTyCon -- c.f TyCon.AbstractTyCon
@@ -779,14 +784,13 @@ that is what is seen by importing module with --make
Note [Displaying axiom incompatibilities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-With -fprint-axiom-incomps we display which closed type family equations
-are incompatible with which. This information is sometimes necessary
-because GHC doesn't try equations in order: any equation can be used when
-all preceding equations that are incompatible with it do not apply.
-
-For example, the last "a && a = a" equation in Data.Type.Bool.&& is
-actually compatible with all previous equations, and can reduce at any
-time.
+With -fprint-axiom-incomps we display which closed type family equations are
+incompatible with which (see #15546). This information is sometimes necessary
+because GHC doesn't try equations in order: any equation can be used when all
+preceding equations that are incompatible with it do not apply.
+
+For example, the last "a && a = a" equation in Data.Type.Bool.&& is actually
+compatible with all previous equations, and can reduce at any time.
This is displayed as:
Prelude> :i Data.Type.Equality.==
=====================================
compiler/GHC/IfaceToCore.hs
=====================================
@@ -91,7 +91,6 @@ import GHC.Utils.Logger
import GHC.Data.Bag
import GHC.Data.Maybe
import GHC.Data.FastString
-import GHC.Data.List.SetOps
import GHC.Types.Annotations
import GHC.Types.SourceFile
@@ -903,12 +902,7 @@ tc_iface_decl _ _ (IfaceAxiom { ifName = tc_name, ifTyCon = tc
-- See #13803
; tc_branches <- forkM (text "Axiom branches" <+> ppr tc_name)
$ tc_ax_branches branches
- ; let axiom = CoAxiom { co_ax_unique = nameUnique tc_name
- , co_ax_name = tc_name
- , co_ax_tc = tc_tycon
- , co_ax_role = role
- , co_ax_branches = manyBranches tc_branches
- , co_ax_implicit = False }
+ ; let axiom = mkBranchedCoAxiom role tc_name tc_tycon tc_branches
; return (ACoAxiom axiom) }
tc_iface_decl _ _ (IfacePatSyn{ ifName = name
@@ -1116,15 +1110,14 @@ tc_fd (tvs1, tvs2) = do { tvs1' <- mapM tcIfaceTyVar tvs1
; return (tvs1', tvs2') }
tc_ax_branches :: [IfaceAxBranch] -> IfL [CoAxBranch]
-tc_ax_branches if_branches = foldlM tc_ax_branch [] if_branches
+tc_ax_branches if_branches = mapM tc_ax_branch if_branches
-tc_ax_branch :: [CoAxBranch] -> IfaceAxBranch -> IfL [CoAxBranch]
-tc_ax_branch prev_branches
- (IfaceAxBranch { ifaxbTyVars = tv_bndrs
+tc_ax_branch :: IfaceAxBranch -> IfL CoAxBranch
+tc_ax_branch (IfaceAxBranch { ifaxbTyVars = tv_bndrs
, ifaxbEtaTyVars = eta_tv_bndrs
, ifaxbCoVars = cv_bndrs
, ifaxbLHS = lhs, ifaxbRHS = rhs
- , ifaxbRoles = roles, ifaxbIncomps = incomps })
+ , ifaxbRoles = roles })
= bindIfaceTyConBinders_AT
(map (\b -> Bndr (IfaceTvBndr b) (NamedTCB Inferred)) tv_bndrs) $ \ tvs ->
-- The _AT variant is needed here; see Note [CoAxBranch type variables] in GHC.Core.Coercion.Axiom
@@ -1135,15 +1128,15 @@ tc_ax_branch prev_branches
; this_mod <- getIfModule
; let loc = mkGeneralSrcSpan (fsLit "module " `appendFS`
moduleNameFS (moduleName this_mod))
- br = CoAxBranch { cab_loc = loc
- , cab_tvs = binderVars tvs
- , cab_eta_tvs = eta_tvs
- , cab_cvs = cvs
- , cab_lhs = tc_lhs
- , cab_roles = roles
- , cab_rhs = tc_rhs
- , cab_incomps = map (prev_branches `getNth`) incomps }
- ; return (prev_branches ++ [br]) }
+ ; return (CoAxBranch { cab_loc = loc
+ , cab_tvs = binderVars tvs
+ , cab_eta_tvs = eta_tvs
+ , cab_cvs = cvs
+ , cab_lhs = tc_lhs
+ , cab_roles = roles
+ , cab_rhs = tc_rhs
+ , cab_overlaps = placeHolderOverlaps
+ , cab_incomps = placeHolderIncomps }) }
tcIfaceDataCons :: Name -> TyCon -> IfaceConDecls -> IfL AlgTyConRhs
tcIfaceDataCons tycon_name tycon if_cons
=====================================
compiler/GHC/Tc/Instance/FunDeps.hs
=====================================
@@ -136,10 +136,10 @@ data FunDepEqns -- Plural becuase fd_eqs has multiple equations
-- to fresh unification vars,
-- See (IMP2) in Note [Improving against instances]
- , fd_eqs :: [TypeEqn] -- Make these pairs of types equal
- -- Invariant: In each (Pair ty1 ty2), the fd_qtvs may be
- -- free in ty1 but not in ty2. See Wrinkle (1) of
- -- Note [Improving against instances]
+ , fd_eqs :: [TypeEqn] -- Make these pairs of types equal
+ -- Invariant: In each (Pair ty1 ty2), the fd_qtvs may be
+ -- free in ty1 but not in ty2. See Wrinkle (1) of
+ -- Note [Improving against instances]
}
instance Outputable FunDepEqns where
=====================================
compiler/GHC/Tc/Solver/FunDeps.hs
=====================================
@@ -26,20 +26,23 @@ import GHC.Core.Coercion
import GHC.Core.TyCo.Rep( Type(..) )
import GHC.Core.Predicate( EqRel(..) )
import GHC.Core.TyCon
-import GHC.Core.Unify( tcUnifyTysForInjectivity, typeListsAreApart )
+import GHC.Core.Unify( AmIUnifying(..)
+ , tcUnifyTysForInjectivity, typeListsAreApart )
import GHC.Core.Coercion.Axiom
-import GHC.Core.TyCo.Subst( elemSubst )
+import GHC.Core.TyCo.Subst( elemSubst, extendTvSubstWithClone )
import GHC.Builtin.WiredIn.TypeLits( tryInteractTopFam, tryInteractInertFam )
+import GHC.Types.Var( TyVar, tyVarKind, setTyVarKind )
import GHC.Types.Var.Set
+import GHC.Types.Var.Env( mkInScopeSet )
import GHC.Utils.Outputable
import GHC.Utils.Panic
import Control.Monad( unless )
import GHC.Data.Pair
-import Data.Maybe( isNothing, isJust, mapMaybe )
+import Data.Maybe( isJust, mapMaybe )
{- Note [Overview of functional dependencies in type inference]
@@ -109,7 +112,6 @@ Wrinkles
from fundeps, but that would require new evidence forms, and an extension to
FC, so we don't do that right now (Dec 14).
-
Note [FunDep and implicit parameter reactions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Currently, our story of interacting two dictionaries (or a dictionary
@@ -573,6 +575,7 @@ tryEqFunDeps work_item@(EqCt { eq_lhs = work_lhs
tryFamEqFunDeps :: TcSMode -> [EqCt] -> TyCon -> [TcType] -> EqCt -> SolverStage ()
+-- See Note [Type inference for type families with injectivity]
tryFamEqFunDeps mode eqs_for_me fam_tc work_args
work_item@(EqCt { eq_ev = ev, eq_rhs = work_rhs })
| Just ops <- builtInClosedTyFamTyCon_maybe fam_tc
@@ -583,6 +586,7 @@ tryFamEqFunDeps mode eqs_for_me fam_tc work_args
; tryFDEqns False fam_tc work_args work_item eqns
; unless (hasRelevantGiven eqs_for_me work_args work_item) $
+ -- hasRelevantGiven: See (CF1) in Note [Exploiting closed type families]
do { eqns <- mkTopBuiltinFamEqFDs fam_tc ops work_args work_rhs
; tryFDEqns True fam_tc work_args work_item eqns } }
@@ -599,8 +603,11 @@ tryFamEqFunDeps mode eqs_for_me fam_tc work_args
NotInjective -> nopStage ()
Injective inj -> do { eqns <- mkLocalFamEqFDs eqs_for_me fam_tc inj work_args work_rhs
; tryFDEqns False fam_tc work_args work_item eqns }
+ -- NB: tryFDEqns bales out on an insoluble fundep
+ -- See (CF4) in Note [Exploiting closed type families]
; unless (hasRelevantGiven eqs_for_me work_args work_item) $
+ -- hasRelevantGiven: See (CF1) in Note [Exploiting closed type families]
do { eqns <- mkTopFamEqFDs fam_tc work_args work_item
; tryFDEqns True fam_tc work_args work_item eqns } }
@@ -638,10 +645,11 @@ tryFDEqns is_top fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs= rhs }) f
-- User-defined type families
-----------------------------------------
mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> EqCt -> SolverStage [FunDepEqns]
+-- Implements (INJFAM:Wanted/top-closed)
+-- See Note [Exploiting closed type families]
-- Look at the top-level axioms; we effectively infer injectivity,
--- so we don't need tyConInjectivtyInfo. This works fine for closed
+-- so we don't need tyConInjectivityInfo. This works fine for closed
-- type families without injectivity info
--- See Note [Exploiting closed type families]
mkTopClosedFamEqFDs ax work_args (EqCt { eq_ev = ev, eq_rhs = work_rhs })
| isGenerativeType work_rhs -- See (CF5) in Note [Exploiting closed type families]
= Stage $
@@ -679,39 +687,46 @@ hasRelevantGiven eqs_for_me work_args (EqCt { eq_rhs = work_rhs })
relevant (EqCt { eq_ev = ev, eq_lhs = lhs, eq_rhs = rhs_ty })
| isGiven ev
, TyFamLHS _ lhs_tys <- lhs
- = isJust (tcUnifyTysForInjectivity True work_tys (rhs_ty:lhs_tys))
+ = isJust (tcUnifyTysForInjectivity Unifying work_tys (rhs_ty:lhs_tys))
| otherwise
= False
getRelevantBranches :: CoAxiom Branched -> [TcType] -> Xi -> [FunDepEqns]
-- Return the FunDepEqns that arise from each relevant branch
+-- Implements Note [Relevance]
getRelevantBranches ax work_args work_rhs
- = go [] (fromBranches (coAxiomBranches ax))
+ = go (fromBranches (coAxiomBranches ax))
where
work_tys = work_rhs : work_args
- go _ [] = []
- go preceding (branch:branches)
+ go [] = []
+ go (branch:branches)
= case is_relevant branch of
- Just eqn -> eqn : go (branch:preceding) branches
- Nothing -> go (branch:preceding) branches
+ Just eqn -> eqn : go branches
+ Nothing -> go branches
where
- is_relevant (CoAxBranch { cab_tvs = qtvs, cab_lhs = lhs_tys, cab_rhs = rhs_ty })
- | Just subst <- tcUnifyTysForInjectivity True (rhs_ty:lhs_tys) work_tys
- , let (subst', qtvs') = trim_qtvs subst qtvs
- lhs_tys' = substTys subst' lhs_tys
- rhs_ty' = substTy subst' rhs_ty
- , all (no_match lhs_tys') preceding
+ is_relevant branch@(CoAxBranch { cab_tvs = qtvs
+ , cab_lhs = lhs_tys
+ , cab_rhs = rhs_ty })
+ | Just subst <- tcUnifyTysForInjectivity Unifying (rhs_ty:lhs_tys) work_tys
+ -- See (RW1)-(RW3) in Note [Relevance]
+ -- This is a pre-/unification/ check (not matching)
+ -- so `subst` can bind both `qtvs` and fvs(work_tys)
+ , let (subst',qtvs') = trim_qtvs subst qtvs
+ lhs_tys' = substTys subst' lhs_tys
+ rhs_ty' = substTy subst' rhs_ty
+ branch_tys' = rhs_ty' : lhs_tys'
+ , noEarlierMatchCheck lhs_tys' branch -- See (RW4) in Note [Relevance]
= Just (FDEqns { fd_qtvs = qtvs'
- , fd_eqs = zipWith Pair (rhs_ty':lhs_tys') work_tys })
+ , fd_eqs = zipWith Pair branch_tys' work_tys })
+ -- Do not apply the substition to `work_tys`;
+ -- See (CF7) in Note [Exploiting closed type families]
| otherwise
= Nothing
- no_match lhs_tys (CoAxBranch { cab_lhs = lhs_tys1 })
- = isNothing (tcUnifyTysForInjectivity False lhs_tys1 lhs_tys)
-
mkTopOpenFamEqFDs :: TyCon -> [Bool] -> [TcType] -> EqCt -> TcS [FunDepEqns]
--- Implements (INJFAM:Wanted/top)
+-- Implements (INJFAM:Wanted/top-open)
+-- See Note [Exploiting open type families]
mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs })
= do { fam_envs <- getFamInstEnvs
; let branches :: [CoAxBranch]
@@ -720,15 +735,15 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs })
; return (mapMaybe do_one branches) }
where
do_one :: CoAxBranch -> Maybe FunDepEqns
- do_one branch@(CoAxBranch { cab_tvs = branch_tvs
- , cab_lhs = branch_lhs_tys
- , cab_rhs = branch_rhs })
- | Just subst <- tcUnifyTysForInjectivity False [branch_rhs] [work_rhs]
- -- False: matching, not unifying
- , let (subst', qtvs) = trim_qtvs subst branch_tvs
+ do_one (CoAxBranch { cab_tvs = branch_qtvs
+ , cab_lhs = branch_lhs_tys
+ , cab_rhs = branch_rhs })
+ | Just subst <- tcUnifyTysForInjectivity Matching [branch_rhs] [work_rhs]
+ , let (subst', qtvs') = trim_qtvs subst branch_qtvs
branch_lhs_tys' = substTys subst' branch_lhs_tys
- , apartnessCheck branch_lhs_tys' branch -- See (TIF3)
- = Just (mkInjectivityFDEqn inj_flags qtvs branch_lhs_tys' work_args)
+ -- No need for an apartness check here; for open type families
+ -- there are no "preceding" equations
+ = Just (mkInjectivityFDEqn inj_flags qtvs' branch_lhs_tys' work_args)
| otherwise
= Nothing
@@ -736,7 +751,7 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs })
mkLocalFamEqFDs :: [EqCt] -> TyCon -> [Bool] -> [TcType] -> Xi -> SolverStage [FunDepEqns]
-- Wanted constraints only
-- Both open and closed type families, but only ones with declared injectivity
--- See Note [Type inference for type families with injectivity] esp (TIF2)
+-- See Note [Exploiting local type-family injectivity]
mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs
= do { let -- eqns_from_inerts: see (INJFAM:Wanted/other)
eqns_from_inerts = mapMaybe do_one eqs_for_me
@@ -755,15 +770,23 @@ mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs
mk_eqn iargs = mkInjectivityFDEqn inj_flags [] work_args iargs
-trim_qtvs :: Subst -> [TcTyVar] -> (Subst,[TcTyVar])
--- Tricky stuff: see (TIF1) in
--- Note [Type inference for type families with injectivity]
-trim_qtvs subst [] = (subst, [])
-trim_qtvs subst (tv:tvs)
- | tv `elemSubst` subst = trim_qtvs subst tvs
- | otherwise = let !(subst1, tv') = substTyVarBndr subst tv
- !(subst', tvs') = trim_qtvs subst1 tvs
- in (subst', tv':tvs')
+trim_qtvs :: Subst -> [TyVar] -> (Subst, [TyVar])
+-- Tricky stuff: see (OF1) in Note [Exploiting open type families]
+trim_qtvs unif_subst qtvs
+ = go unif_subst qtvs
+ where
+ go :: Subst -> [TyVar] -> (Subst, [TyVar])
+ go subst [] = (subst, [])
+ go subst (tv:tvs)
+ | tv `elemSubst` unif_subst = go subst tvs
+ | otherwise = (subst'', tv':tvs')
+ where
+ !(subst'', tvs') = go subst' tvs
+ tv' = tv `setTyVarKind` substTy subst (tyVarKind tv)
+ subst' = extendTvSubstWithClone subst tv tv'
+ -- extendTvSubstWithClone: see (OF1b) in
+ -- Note [Exploiting open type families]
+
-----------------------------------------
-- Built-in type families
@@ -924,15 +947,20 @@ we attempt to exploit injectivity, via `mkLocalFamEqFDs`:
* (INJFAM:Wanted/other) see `mkLocalFamEqFDs`
work item: [W] F s1 s2 ~ rhs -- Wanted
inert: [G/W] F t2 t2 ~ rhs -- Same `rhs`, Given or Wanted
- We can generate FunDepEqns: (s2 ~ t2)
+ See Note [Exploiting local type-family injectivity]
+
+* (INJFAM:Wanted/top-open) for open type families: `mkTopOpenFamEqFDs`
+ type family F a b = r | r -> b
+ type instance F Int (Maybe a) = [G Int] -- G is a type family
+ [W] F alpha beta = [ty]
+ We can generate (Maybe gamma ~ beta)
+ See Note [Exploiting open type families]
-* (INJFAM:Wanted/top) see `mkTopUserFamEqFDs`
- work item: [W] F s1 s2 ~ rhs
- type instance forall a b c. F t1 t2 ~ top_rhs
- and we can /match/ the LHS, so that
- S(top_rhs) = rhs
- then we can generate the FunDepEqns: forall a c. s2 ~ S(t2)
- But see wrinkle (TIF1), (TIF3)
+* (INJFAM:Wanted/top-closed) for closed type families: `mkTopClosedFamEqFDs`
+ type family F a b where { ...eqns... }
+ [W] F alpha ~ Int
+ We may be able to generate some extra equalities to constraint `alpha`
+ See very clever Note [Exploiting closed type families]
For /built-in/ type families, it's pretty similar, except that
@@ -945,45 +973,36 @@ For /built-in/ type families, it's pretty similar, except that
* mkLocalBuiltinFamEqFDs
* mkTopBuiltinFamEqFDs
-(TIF1) Generating fundeps from a top-level type instance is covered in
- Section 5.2 in the Injective Type Families paper. It's a bit tricky.
- Consider
- type family F @k (a::k) (b::k) = r | r -> k b
- type instance forall k (a::k) (b::k). F @k (Proxy @k a) (Proxy @k b) = Proxy @k a
- [W] F @kappa alpha beta ~ Maybe (Proxy @kappa (delta::kappa))
-
- we match (Proxy @kappa delta) against the template (Proxy k a), succeeding
- with substitution [k:->kappa, a:->delta]. We want to generate this FunDepEqns
- FDEqn { fd_qtvs = [b:kappa], fd_eqs = [ beta ~ Proxy @kappa b ] }
- Notice that
- * we must quantify the FunDepEqns over `b`, which is not matched; for this
- we will generate a fresh unification variable in `instantiateFunDepEqn`.
- * we must substitute `k:->kappa` in the kind of `b`.
- This fancy footwork for `fd_qtvs` is done by `trim_qtvs` in
- `mkInjWantedFamEqTopEqns`.
-
-(TIF2) All this applies equally to /closed/ type families; it is /not/
- subsumed by Note [Exploiting closed type families]. Consider:
+Note [Exploiting local type-family injectivity] see `mkLocalFamEqFDs`
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have a type family with declared injectivity:
+ type family F a b = r | r -> b
+and we have
+ work item: [W] F s1 s2 ~ F t1 t2
+or
+ work item: [W] F s1 s2 ~ rhs -- Wanted
+ inert: [G/W] F t2 t2 ~ rhs -- Same `rhs`, Given or Wanted
+
+Then we can generate FunDepEqns: (s2 ~ t2)
+
+This applies equally to /closed/ type families; it is /not/ subsumed
+by Note [Exploiting closed type families]. Consider:
+
type family F a | r -> a where { .... }
[W] F t1 ~ a
[W] F t2 ~ a
- Then since F is declared injective, we can generate t1~t2.
+Then since F is declared injective, we can generate t1~t2.
- As for open type families, we insist on /user-declared/ injectivity only; we
- don't try to /infer/ injectivity even for a closed family. See Section 3.4
- of the "Injective type families" paper. (Arguably, we could /infer/
- injectivity for closed type families, and that would be more in the spirit of
- Note [Exploiting closed type families].)
+As for open type families, we insist on /user-declared/ injectivity only; we
+don't try to /infer/ injectivity even for a closed family. See Section 3.4
+of the "Injective type families" paper. (Arguably, we could /infer/
+injectivity for closed type families, and that would be more in the spirit of
+Note [Exploiting closed type families].)
-(TIF3) Further to (TIF1), if we are considering a /closed/ type family, we
- must ensure (see Section 5.2 of the paper) that after matching that
- equation would indeed be the one to fire. So we call `apartnessCheck`
- on the branch to ensure this, in `mkTopUserFamEqFDs`.
-
-Definition [Relevance]
-~~~~~~~~~~~~~~~~~~~~~~
+Note [Relevance]
+~~~~~~~~~~~~~~~~
We say that a closed-type-family equation `F lhs = rhs` is
/relevant/ for a Wanted [W] F wlhs ~ wrhs
iff
@@ -992,6 +1011,10 @@ iff
(R2) There is no earlier equation that matches S(lhs). See (RW4) below.
+The relevance check is implemented by `getRelevantBranches`, which actually
+returns the [FunDepEqns] described in the Closed Family Fundep Algorithm in
+Note [Exploiting closed type families].
+
(RW1) Pre-unification treats type-family applications as binding to anything,
rather like type variables. If two types don't even pre-unify, we say that they
are /apart/. It is done by `tcUnifyTysForInjectivity`.
@@ -1014,24 +1037,130 @@ iff
Clearly the RHS is apart from the first equation and we want to fire injectivity
on the second equation.
-(RW4) Why "no earlier equation matches" in conditoin (R2)? Consider the family
+(RW4) Why "no earlier equation matches" in condition (R2)? Consider the family
type family Bak a = r where
Bak Int = Char -- B1
Bak Char = Int -- B2
Bak a = a -- B3
- and [W] Bak alpha ~ Char. In fact, only (B2) is relevant for this Wanted.
+ and [W] Bak alpha ~ Char. In fact, only (B1) is relevant for this Wanted.
You might think that (B3) could be instantiated to Bak Char ~ Char; but
actually that instantiation will never fire because (B2) Bak Char ~ Int would
- fire first. So the only way to return a Char is if the argment is Int; so we
- can emit [W] alpha ~ Int. Hence (B3) is not relevant; only (B2) is relevant.
+ fire first. So the only way to return a Char is via (B1); so we
+ can emit [W] alpha ~ Int. Hence (B3) is not relevant; only (B1) is relevant.
That is the reason for condition (R2) in the definition of Relevance above.
A watertight proof that this is the Right Thing is not very easy. See more
- discussion in #23162.
-
-Note [Exploiting closed type families]
+ discussion in #23162, and Section 5.2 of the paper.
+
+ How, precisely, do we implement (R2)? We check that there is no earlier equation
+ that fires on S(lhs), in this case (on Bak Char). Notice that this is different
+ from the `apartnessCheck`, which checks that all preceding equations are apart
+ from S(lhs). Apartness checking uses /unification/; here we want /matching/.
+ Hence using `noEarlierMatchCheck`, not `apartnessCheck`.
+
+ Here's a good example from T27171_aux. T
+ type family TMessage m where
+ {- T1 -} TMessage @f @t (CustomMethod s :: Method f t) = ()
+ {- T2 -} TMessage @f @Req (m :: Method f Req) = TRequestMessage m
+ {- T3 -} TMessage @f @Not (m :: Method f Not) = TNotificationMessage m
+
+ [W] TMessage @SC @Req alpha ~# TRequestMessage alpha
+
+ There is only one relevant equation, namely (T2). If we apply its
+ pre-unification substitution [f :-> SC, m :-> alpha] to its LHS we get
+ TMessage @SC @Req alpha
+ and equation (T1) does not match that. (It does unify, but we don't care.)
+
+(RW5) `noEarlierMatchCheck`: in (RW4) We really do need to check that /no/
+ earlier equation matches, not just no earlier /incompatible/ equation
+ matches. Consider T27828a:
+ type family F a where
+ F Int = Int -- B1
+ F Char = Bool -- B2
+ F a = a -- B3
+
+ [W] F alpha ~ Int
+
+ (B1) is relevant, and (B2) is not. What about (B3)? It pre-unifies with
+ the Wanted via [alpha :-> Int, a :-> Int]. But under that substitution
+ (B1) would fire, so (B3) is not relevant.
+
+ And yet, (B1) is /compatible/ with (B3), so it's no good just looking at
+ the `cab_incomps` of (B3). Instead we look at `cab_overlaps`.
+
+Note [Exploiting open type families] see `mkTopOpenFamEqFDs`
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Generating fundeps from a top-level type instance is covered in Section 5.2 in
+the Injective Type Families paper. For open type families, suppose we have
+
+ type family F a = r | r -> a
+ type instance F [a] = a->a
+
+ [W] F alpha ~ Int->Int
+
+Then, since F has been checked as injective, and the RHS `a->a` (pre-)unifies
+with the `Int->Int` in the Wanted with substitution [a :-> Int], we can
+add a derived FunDepEqns
+ FDEqns{ fd_qtvs = [], fd_eqs = [ [Int] ~ alpha ] }
+and thereby emit (via `instantiateFunDepEqns`)
+ [W] [Int] ~ alpha
+
+Things are a bit trickier when not all the quantified variables of the
+instance are bound by the pre-unification step. Suppose we have
+
+ type family F a = r | r -> a
+ type instance F (Maybe a) = [G a] -- G is a type family
+
+ [W] F alpha ~ [ty]
+
+Then, the RHS [G a] pre-unifies with the RHS of the Wanted, but with an
+empty substitution, which does not fix `a`. So we get this FunDepEqns:
+ FDEqns{ fd_qtvs = a, fd_eqs = [ Maybe a ~ alpha ] }
+(note the fd_qtvs=a) and thereby emit (via `instantiateFunDepEqns`)
+ [W] Maybe gamma ~ alpha -- Fresh gamma
+We have learned that `alpha` must be a list, but that is all; we don't
+know what is inside it, hence the fresh `gamma`.
+
+In general we have:
+
+ type family F x1 ... xn = r | r -> x1 x3 (say)
+ type instance forall qs. F t1 ... tn = rhs
+ [W] F a1 ... an ~ b
+
+Suppose `b` pre-unifies with `rhs`, with substitution `S` that binds
+some (but perhaps not all) of the `qs`. Lets say
+ unbound_qs = qs \ dom(S)
+
+Then we generate the FunDepEqs
+ FDEqns{ fd_qtvs = unbound_qs
+ , fd_eqs = [ S(t1) ~ S(a1), S(t3) ~ S(a3) ]
+
+These 'fd_qtvs' are subsequently instantiated to fresh metavariables by
+'instantiateFunDepEqns'.
+
+(OF1) The computation of `unbound_qs` is done by `trim_qtvs`, but we
+ have to be careful. Suppose (OF1a)
+ qs = [ k::*, a::k ]
+ S = [ k :-> UnliftedType ]
+ Then we want
+ unbound_qs = [ a::UnliftedType ] -- Must apply S to q's kind!!
+
+ And (OF1b), although I'm not sure if this can acutally happen:
+ qs = [ k::*, a::(k::*), b::(a::k) ]
+ S = [ k :-> UnliftedType ]
+ We want
+ unbound_qs = [ a::UnliftedType, b::(a::UnliftedType) ]
+ Note that the occurrence of `a` in b's kind should be replaced by the
+ newly-kinded `a` not the original `a::k`.
+
+ This fancy footwork for `fd_qtvs` is done by `trim_qtvs`. It
+ * Drops a quantified tyvar that /is/ matched
+ * Substitutes in the kind of a quantified tyvar `a` that is /not/ matched
+ * Adds the substitution [a::k :-> a::S(k)] to the substitution
+
+Note [Exploiting closed type families] see `mkTopClosedFamEqFDs`
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
type family F a b where
@@ -1042,17 +1171,18 @@ Suppose we have
[W] F Int alpha ~ Char
The /only/ way to solve this Wanted is using (F2), so we can safely unify
-alpha:=Char without risking losing any solutions. That is what
-`mkTopClosedFamEqFDs` does. Ticket #23162 has lots of background detail
+alpha:=Char without risking losing any solutions. We don't even need any
+injectivity annotations. Ticket #23162 has lots of background detail.
-More precisely, here is the Closed Family Fundep Algorithm (CFFA)
+More precisely, here is the very clever Closed Family Fundep Algorithm (CFFA)
IF * F a is a closed type family.
* We are trying to solve [W] F wlhs ~ wrhs.
- * There are no "relevant" Givens [G] F lhs ~ rhs. See (CF1) below.
- * F has exactly one equation, F lhs = rhs that is "relevant" for that Wanted
+ * There are no "relevant Givens" [G] F lhs ~ rhs. See (CF1) below.
+ * F has exactly one equation, F lhs = rhs that is "relevant" for
+ that Wanted (see Note [Relevance])
THEN
- we can emit and solve the fundep equalities:
+ we can emit and solve the fundeps :: [FunDepEqns]:
[W] wlhs1 ~ lhs1
...
[W] wlhsn ~ lhsn
@@ -1060,7 +1190,10 @@ More precisely, here is the Closed Family Fundep Algorithm (CFFA)
with fresh unification vars in lhs and rhs for the quantified variables of the
equation.
-See Definition [Relevance] for what "relevant" means.
+ Actually we take advantage of the substitution generated by the relevance
+ check, see (CF7) below.
+
+See Note [Relevance] for what "relevant" means.
We need to take care about non-termination; see (CF3).
Key point: equations that are not relevant do not need to be considered for fundeps at all.
@@ -1166,6 +1299,8 @@ Key point: equations that are not relevant do not need to be considered for fund
I was looking at non-termination for closed type families, but it's a small
improvement in general.
+ This bale-out is implementedn in `tryFDEqns`.
+
(CF5) Consider (see "Yikes5" in #23162):
type family F a where
F (Just x) = Int
@@ -1196,7 +1331,7 @@ Key point: equations that are not relevant do not need to be considered for fund
type family I t = res | res -> t where
I TInt = Int |> g -- where g :: Type ~# IK k
and [W] I alpha ~ Int |> g2
- Here we definiteily want to take advantage of injectivity.
+ Here we definitely want to take advantage of injectivity.
(CF6) This machinery can also have a significant positive effect on the size of
proof terms. For example (simplification of T26426):
@@ -1204,7 +1339,8 @@ Key point: equations that are not relevant do not need to be considered for fund
type family (++) a b where { '[] ++ ys = ys; (x:xs) ++ ys = x : (xs ++ ys) }
type family MapId a where { MapId '[] = '[]; MapId (x:xs) = x : MapId xs }
- app :: (MapId xs ++ MapId ys ~ MapId (xs ++ ys)) => Proxy xs -> Proxy ys -> Proxy (xs ++ ys)
+ app :: (MapId xs ++ MapId ys ~ MapId (xs ++ ys))
+ => Proxy xs -> Proxy ys -> Proxy (xs ++ ys)
test :: Proxy [ty_1, ..., ty_n]
test = Proxy @'[ty_1]
@@ -1248,6 +1384,30 @@ Key point: equations that are not relevant do not need to be considered for fund
instead of relying on recursively built sub-proof terms, which brings down
coercion sizes (in certain situations) from O(n^3) to O(n^2).
+(CF7) Relevance. When computing relevance in the Closed Family Fundep Algorithm,
+ for [W] F wlhs1 wlhs2 ~ wrhs, against an equation F lhs1 lhs2 ~ rhs
+ we get back a pre-unifying substitution S that makes the two as equal as poss.
+ Then we use `trim_qtvs` in exactly the same way as in
+ (OF1) of Note [Exploiting open type families], to generate qtvs' and S'
+ Then we generate
+ FDEqns { fd_qtvs = qtvs', fd_eqs [ S'(lhs1) ~ wlhs1
+ , S'(lhs2) ~ wlhs2
+ , S'(rhs) ~ wrhs ] }
+ Notice that we do /not/ apply S' to wlhs/wrhs. These type contain unification
+ variables that we must actually unify! Example
+ type family F a b where
+ F [a] (Maybe b) = (a, G b)
+ [W] F alpha beta ~ (Int, [gamma])
+ Pre-unification gives [alpha :-> [a], beta :-> Maybe b, a :-> Int]
+ This substitution eliminates the quantified variable `a` but not `b`, so we
+ want this:
+ FDEqns { fd_qtvs = [b], fd_eqs [ [Int] ~ alpha
+ , Maybe b ~ beta
+ , (Int,G b) ~ (Int, [gamma]) ] }
+
+ Notice also that by applying the substitution to the template but not to the
+ Wanted, we uphold the `fd_eqs` invariant in `FDEqns` (see its data type decl)
+
Note [Cache-caused loops]
~~~~~~~~~~~~~~~~~~~~~~~~~
It is very dangerous to cache a rewritten wanted family equation as 'solved' in
@@ -1340,28 +1500,34 @@ solveFunDeps work_ev fd_eqns
; uPairsTcM uenv eqs }
instantiateFunDepEqns :: FunDepEqns -> TcM [TypeEqn]
-instantiateFunDepEqns (FDEqns { fd_qtvs = tvs, fd_eqs = eqs })
- | null tvs
+-- See GHC.Tc.Instance.Fundeps Note [Improving against instances]
+-- Wrinkle (IMP1)
+instantiateFunDepEqns (FDEqns { fd_qtvs = qtvs, fd_eqs = eqs })
+ | null qtvs
= return rev_eqs
| otherwise
- = do { TcM.traceTc "instantiateFunDepEqns" (ppr tvs $$ ppr eqs)
- ; (_, subst) <- instFlexiXTcM emptySubst tvs -- Takes account of kind substitution
+ = do { TcM.traceTc "instantiateFunDepEqns" (ppr qtvs $$ ppr eqs)
+ ; (_, subst) <- instFlexiXTcM empty_subst qtvs -- Takes account of kind substitution
; return (map (subst_pair subst) rev_eqs) }
where
rev_eqs = reverse eqs
-- (reverse eqs): See Note [Reverse order of fundep equations]
+ -- The kinds of `qtvs` can have free variables, because of `trim_qtvs`
+ -- Example: T27828b
+ empty_subst = mkEmptySubst $ mkInScopeSet $
+ tyCoVarsOfTypes (map tyVarKind qtvs)
+
subst_pair subst (Pair ty1 ty2)
- = Pair (substTyUnchecked subst' ty1) ty2
- -- ty2 does not mention fd_qtvs, so no need to subst it.
- -- See GHC.Tc.Instance.Fundeps Note [Improving against instances]
- -- Wrinkle (1)
+ = Pair (substTy subst' ty1) ty2
+ -- NB: ty2 does not mention fd_qtvs, so no need to subst it.
+ -- See invariant on `fv_eqs` in `data FunDepEqns`.
where
subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1)
-- The free vars of ty1 aren't just fd_qtvs: ty1 is the result
-- of matching with the [W] constraint. So we add its free
-- vars to InScopeSet, to satisfy substTy's invariants, even
- -- though ty1 will never (currently) be a poytype, so this
+ -- though ty1 will never (currently) be a polytype, so this
-- InScopeSet will never be looked at.
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -3462,7 +3462,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
; let mb_co_ax
| null eqns = Nothing -- mkBranchedCoAxiom fails on empty list
- | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches)
+ | otherwise = Just (mkBranchedCoAxiom Nominal co_ax_name fam_tc branches)
fam_tc = mkFamilyTyCon tc_name kind tc_bndrs 0 res_kind (resultVariableName sig)
(ClosedTypeFamilyTyCon $ CTF mb_co_ax) parent inj'
=====================================
testsuite/tests/indexed-types/should_compile/T27828.hs
=====================================
@@ -0,0 +1,50 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeAbstractions #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Bug where
+
+import Data.Functor.Identity (Identity(..))
+import Data.Kind (Type)
+import Data.Proxy (Proxy(..))
+import Data.Type.Equality ((:~:)(..))
+
+type TyFun :: Type -> Type -> Type
+data TyFun a b
+
+type (~>) :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+
+type Apply :: (k1 ~> k2) -> k1 -> k2
+type family Apply f x
+
+type Rep1 :: (k -> Type) -> k -> Type
+type family Rep1 f
+
+type To1 :: Rep1 f a -> f a
+type family To1 z
+
+type Par1 :: Type -> Type
+newtype Par1 p = Par1 p
+
+type To1Sym0 :: forall k (f :: k -> Type) (a :: k). Rep1 f a ~> f a
+data To1Sym0 z
+
+applyTo1Sym0 :: forall k (f :: k -> Type) (a :: k) (x :: Rep1 f a). Proxy x -> Apply @(Rep1 f a) @(f a) To1Sym0 x :~: To1 x
+applyTo1Sym0 _ = undefined
+
+type IdentitySym0 :: a ~> Identity a
+data IdentitySym0 z
+type instance Apply IdentitySym0 x = 'Identity x
+
+type Aux :: Rep1 Identity a -> Rep1 Identity a -> Identity a
+type family Aux x y where
+ Aux x ('Par1 wombat) = Apply IdentitySym0 wombat
+
+type instance Rep1 Identity = Par1
+type instance To1 @Identity y = Aux y y
+
+lemma :: forall a (z :: a). Apply @(Rep1 Identity a) @(Identity a) To1Sym0 ('Par1 z) :~: 'Identity z
+lemma = applyTo1Sym0 @Type @Identity @a (Proxy @('Par1 z))
+-- lemma = applyTo1Sym0 @Type @Identity @a @('Par1 z) (Proxy @('Par1 z))
=====================================
testsuite/tests/indexed-types/should_compile/T27828a.hs
=====================================
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T27828a where
+
+import Data.Proxy
+
+type family F a where
+ F Int = Int -- B1
+ F Char = Bool -- B2
+ F a = a -- B3
+
+h :: (F a ~ Int) => Proxy a -> ()
+h = error "urk"
+
+k :: ()
+k = h Proxy -- [W] F alpha ~ Int
=====================================
testsuite/tests/indexed-types/should_compile/T27828b.hs
=====================================
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies, KindSignatures, AllowAmbiguousTypes #-}
+
+module T27828b where
+
+type family IsJust (m :: Maybe k) :: Bool where
+ IsJust ('Just x) = 'True
+ IsJust 'Nothing = 'False
+
+f :: forall k (m :: Maybe k). (IsJust m ~ 'True) => Int -> Int
+f = error "urk"
+
+g _ = f 3 -- Triggered checkValidSubst error in `instantiateFunDepEqns`o
=====================================
testsuite/tests/indexed-types/should_compile/all.T
=====================================
@@ -316,3 +316,6 @@ test('T25611b', normal, compile, [''])
test('T25611c', normal, compile, [''])
test('T25611d', normal, compile, [''])
test('T25657', normal, compile, [''])
+test('T27828', normal, compile, [''])
+test('T27828a', normal, compile, [''])
+test('T27828b', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3e346260ea82eeb19d453b104cbb1a7ā¦
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3e346260ea82eeb19d453b104cbb1a7ā¦
You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help
1
0
[Git][ghc/ghc] Pushed new branch wip/andrea/with-signal-handlers
by Andrea Vezzosi (ļ¼ trac-Saizan) 07 Oct '26
by Andrea Vezzosi (ļ¼ trac-Saizan) 07 Oct '26
07 Oct '26
Andrea Vezzosi pushed new branch wip/andrea/with-signal-handlers at Glasgow Haskell Compiler / GHC
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/tree/wip/andrea/with-signal-handlers
You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help
1
0