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/2af969356bdfd6bf677d19eddcab9a12... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2af969356bdfd6bf677d19eddcab9a12... 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