Simon Peyton Jones pushed to branch wip/T27828 at Glasgow Haskell Compiler / GHC Commits: 545fd4fb by ARATA Mizuki at 2026-09-22T15:03:24-04:00 Change the C types of hs_{bitrev,bswap}{16,32} to match the Haskell types bitReverse{16,32}# and byteSwap{16,32}# have the type Word# -> Word#, but their C correspondents took and returned StgWord{16,32}. The mismatch on bitReverse16# led to the problem reported in #27299. Although no similar issue is reported for bitReverse32# and byteSwap{16,32}#, it seemed wise to change them proactively. This commit fixes the mismatch by changing the C type. Fixes #27299 - - - - - bf17f289 by fendor at 2026-09-22T15:04:05-04:00 Don't lose instances from shadowed imported modules with the same name When we look for instances below the current module, we need to check the unit id as well when we check for whether the module is the current module, otherwise we ignore modules we import that have the same name as the import module. Adds regression test. - - - - - b1803ff5 by Simon Peyton Jones at 2026-09-23T22:02:23+01:00 Refactor fundeps yet 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`. * Use a proper data types, `AmIUnifying` and `OuterKindsFlag`, for two previously-Boolean arguments to `tc_unify_tys`. This is a pure refactor. * Lots of improvements to the Notes in FunDeps.hs - - - - - 24 changed files: - + changelog.d/26610 - + changelog.d/T27828 - compiler/GHC/Core/Coercion/Axiom.hs - compiler/GHC/Core/FamInstEnv.hs - compiler/GHC/Core/Unify.hs - compiler/GHC/Driver/Env.hs - compiler/GHC/Tc/Instance/FunDeps.hs - compiler/GHC/Tc/Solver/FunDeps.hs - rts/include/stg/Prim.h - rts/prim/bitrev.c - rts/prim/bswap.c - + testsuite/tests/ghci/prog-mhu008/Makefile - + testsuite/tests/ghci/prog-mhu008/a/M.hs - + testsuite/tests/ghci/prog-mhu008/all.T - + testsuite/tests/ghci/prog-mhu008/b/M.hs - + testsuite/tests/ghci/prog-mhu008/prog-mhu008.script - + testsuite/tests/ghci/prog-mhu008/prog-mhu008.stdout - + testsuite/tests/ghci/prog-mhu008/unitA - + testsuite/tests/ghci/prog-mhu008/unitB - + testsuite/tests/indexed-types/should_compile/T27828.hs - testsuite/tests/indexed-types/should_compile/all.T - + testsuite/tests/primops/should_run/T27299.hs - + testsuite/tests/primops/should_run/T27299.stdout - testsuite/tests/primops/should_run/all.T Changes: ===================================== changelog.d/26610 ===================================== @@ -0,0 +1,7 @@ +section: compiler +synopsis: Fix instance resolution for shadowed modules +description: + Instances imported from modules with the same module name as the importing module + were dropped accidentally since we didn't account for the unit id of the imported module. +mrs: !16648 +issues: #26610 ===================================== 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 implemenation of functional dependencies for type families. +} ===================================== compiler/GHC/Core/Coercion/Axiom.hs ===================================== @@ -197,14 +197,19 @@ 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.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. -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. +Specifically, the `cab_incomps :: [CoAxBranch]` field of a `CoAxBranch` +lists all /earlier/ branches with which it is /incompatible/. That is, +earlier branches where + 1) the patterns are not apart from the patterns of this branch, and + 2) if the patterns unify, the rhss are different + +This list might well be empty, and it will always be for the first branch of +any axiom. 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 @@ -230,7 +235,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 ===================================== 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(..), @@ -488,9 +488,11 @@ 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. + + 1) The patterns are apart. + + 2) The patterns unify with a substitution S, and their right hand sides + are equal under that substitution. For open type families, only compatible instances are allowed. For closed type families, the story is slightly more complicated. Consider the following: @@ -603,8 +605,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] @@ -1258,6 +1259,17 @@ 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_incomps = incomps }) + = not (any matches incomps) + 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 of 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/Driver/Env.hs ===================================== @@ -263,13 +263,13 @@ hugCompleteSigsBelow hsc uid mn = foldr (++) [] <$> -- | Find instances visible from the given set of imports hugInstancesBelow :: HscEnv -> UnitId -> ModuleNameWithIsBoot -> IO (InstEnv, [FamInst]) hugInstancesBelow hsc_env uid mnwib = do - let mn = gwib_mod mnwib + let mn = mkModule uid (gwib_mod mnwib) (insts, famInsts) <- unzip . concat <$> hugSomeThingsBelowUs (\mod_info -> let details = hm_details mod_info -- Don't include instances for the current module - in if moduleName (mi_module (hm_iface mod_info)) == mn + in if fmap toUnitId (mi_module (hm_iface mod_info)) == mn then [] else [(md_insts details, md_fam_insts details)]) True -- Include -hi-boot ===================================== 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,12 +26,14 @@ 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.Builtin.WiredIn.TypeLits( tryInteractTopFam, tryInteractInertFam ) +import GHC.Types.Var( TyVar, tyVarKind, setTyVarKind ) import GHC.Types.Var.Set import GHC.Utils.Outputable @@ -39,7 +41,7 @@ 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 +111,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 +574,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 +585,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 +602,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 +644,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 +686,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 +734,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 +750,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 +769,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] +-- The returned substitution is identical to the incoming one, except that +-- its in-scope set is extended with the returned [TyVar] +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 + tv' = tv `setTyVarKind` substTy subst (tyVarKind tv) + subst' = subst `extendSubstInScope` tv' + !(subst'', tvs') = go subst' tvs + ----------------------------------------- -- Built-in type families @@ -924,15 +946,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 +972,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)) +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 - 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`. +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: -(TIF2) All 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 +1010,10 @@ iff (R2) There is no earlier equation that matches S(lhs). See (RW4) below. +The relevance check is implemented by `getRelevantBranches`, which acutally +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 +1036,82 @@ 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 + 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 (B2) 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. + discussion in #23162, and Section 5.2 of the paper. -Note [Exploiting closed type families] + 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.) + +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 b = r | r -> b + type instance F Int (Maybe a) = [G Int] -- G is a type family + + [W] F alpha beta = [ty] + +Then, since F has been checked as injective, and the RHS [G Int] +pre-unifies with [ty], we can add a derived FunDepEqns + FDEqns{ fd_qtvs = a, fd_eqs = [ Maybe a ~ beta ] } +and thereby emit + [W] Maybe gamma ~ beta -- Fresh gamma + +Wrinkles + +(OF1) 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) = Maybe (Proxy @k a) + + [W] F @kappa alpha beta ~ Maybe (Proxy @kappa (delta::kappa)) + + We match the target (Maybe (Proxy @kappa delta)) + against the template (Maybe (Proxy @k a)) + succeeding with substitution [k:->kappa, a:->delta]. We want to generate this: + FDEqn { fd_qtvs = [b::kappa], fd_eqs = [ Proxy @kappa b ] ~ beta } + 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`. It + * Drops a quantified tyvar that /is/ matched + * Substitutes in the kind of a quantified tyvar that is /not/ matched + * Adds the not-matched tyvar to the in-scope set of the substitution + +Note [Exploiting closed type families] see `mkTopClosedFamEqFDs` ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have type family F a b where @@ -1042,17 +1122,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 +1141,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 +1250,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 +1282,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 +1290,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 +1335,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 closed 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 familiy 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 +1451,29 @@ solveFunDeps work_ev fd_eqns ; uPairsTcM uenv eqs } instantiateFunDepEqns :: FunDepEqns -> TcM [TypeEqn] -instantiateFunDepEqns (FDEqns { fd_qtvs = tvs, fd_eqs = eqs }) - | null tvs +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 emptySubst 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] subst_pair subst (Pair ty1 ty2) - = Pair (substTyUnchecked subst' ty1) ty2 + = Pair (substTy subst' ty1) (substTy subst' ty2) +-- ToDo not correct! -- ty2 does not mention fd_qtvs, so no need to subst it. -- See GHC.Tc.Instance.Fundeps Note [Improving against instances] - -- Wrinkle (1) + -- Wrinkle (IMP1) where - subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1) + subst' = extendSubstInScopeSet subst (tyCoVarsOfTypes [ty1,ty2]) -- 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. ===================================== rts/include/stg/Prim.h ===================================== @@ -59,16 +59,16 @@ StgWord hs_xchg32(StgWord x, StgWord val); StgWord64 hs_xchg64(StgWord x, StgWord64 val); /* rts/prim/bswap.c */ -StgWord16 hs_bswap16(StgWord16 x); -StgWord32 hs_bswap32(StgWord32 x); +StgWord hs_bswap16(StgWord x); +StgWord hs_bswap32(StgWord x); StgWord64 hs_bswap64(StgWord64 x); /* rts/prim/bitrev.c This was done as part of issue #16164. See Note [Bit reversal primop] for more details about the implementation.*/ StgWord hs_bitrev8(StgWord x); -StgWord16 hs_bitrev16(StgWord16 x); -StgWord32 hs_bitrev32(StgWord32 x); +StgWord hs_bitrev16(StgWord x); +StgWord hs_bitrev32(StgWord x); StgWord64 hs_bitrev64(StgWord64 x); /* rts/prim/longlong.c */ ===================================== rts/prim/bitrev.c ===================================== @@ -36,8 +36,8 @@ hs_bitrev8(StgWord x) return x; } -StgWord16 -hs_bitrev16(StgWord16 x) +StgWord +hs_bitrev16(StgWord x) { x = ((x >> 1) & 0x5555) | ((x & 0x5555) << 1 ); x = ((x >> 2) & 0x3333) | ((x & 0x3333) << 2 ); @@ -46,14 +46,14 @@ hs_bitrev16(StgWord16 x) return x; } -StgWord32 -hs_bitrev32(StgWord32 x) +StgWord +hs_bitrev32(StgWord x) { - x = ((x >> 1) & 0x55555555) | ((x & 0x55555555) << 1 ); - x = ((x >> 2) & 0x33333333) | ((x & 0x33333333) << 2 ); - x = ((x >> 4) & 0x0F0F0F0F) | ((x & 0x0F0F0F0F) << 4 ); - x = ((x >> 8) & 0x00FF00FF) | ((x & 0x00FF00FF) << 8 ); - x = ( x >> 16 ) | ( x << 16 ); + x = ((x >> 1) & 0x55555555) | ((x & 0x55555555) << 1 ); + x = ((x >> 2) & 0x33333333) | ((x & 0x33333333) << 2 ); + x = ((x >> 4) & 0x0F0F0F0F) | ((x & 0x0F0F0F0F) << 4 ); + x = ((x >> 8) & 0x00FF00FF) | ((x & 0x00FF00FF) << 8 ); + x = ((x >> 16) & 0x0000FFFF) | ((x & 0x0000FFFF) << 16); return x; } ===================================== rts/prim/bswap.c ===================================== @@ -1,16 +1,18 @@ #include "Rts.h" -StgWord16 -hs_bswap16(StgWord16 x) +StgWord +hs_bswap16(StgWord x) { - return ((x >> 8) | (x << 8)); + x = (StgWord16)x; + return (StgWord16)((x >> 8) | (x << 8)); } -StgWord32 -hs_bswap32(StgWord32 x) +StgWord +hs_bswap32(StgWord x) { - return ((x >> 24) | ((x >> 8) & 0xff00) | - (x << 24) | ((x & 0xff00) << 8)); + x = (StgWord32)x; + return (StgWord32)((x >> 24) | ((x >> 8) & 0xff00) | + (x << 24) | ((x & 0xff00) << 8)); } StgWord64 ===================================== testsuite/tests/ghci/prog-mhu008/Makefile ===================================== @@ -0,0 +1,3 @@ +TOP=../../.. +include $(TOP)/mk/boilerplate.mk +include $(TOP)/mk/test.mk ===================================== testsuite/tests/ghci/prog-mhu008/a/M.hs ===================================== @@ -0,0 +1,4 @@ +module M (T (..)) where + +newtype T = MkT Int + deriving (Eq, Ord) ===================================== testsuite/tests/ghci/prog-mhu008/all.T ===================================== @@ -0,0 +1,5 @@ +test('prog-mhu008', + [extra_files(['a/', 'b/', 'unitA', 'unitB']), + cmd_prefix('ghciWayFlags=' + config.ghci_way_flags), + req_interp], + ghci_multiunit_script, [['unitA', 'unitB'], 'prog-mhu008.script']) ===================================== testsuite/tests/ghci/prog-mhu008/b/M.hs ===================================== @@ -0,0 +1,11 @@ +{-# LANGUAGE PackageImports #-} + +module M + ( module Export + , cmp + ) where + +import "a" M as Export + +cmp :: T -> T -> Bool +cmp x y = x <= y ===================================== testsuite/tests/ghci/prog-mhu008/prog-mhu008.script ===================================== @@ -0,0 +1,5 @@ +:set -XPackageImports +import "a" M qualified as MA +import "b" M qualified as MB + +MB.cmp (MA.MkT 1) (MA.MkT 2) ===================================== testsuite/tests/ghci/prog-mhu008/prog-mhu008.stdout ===================================== @@ -0,0 +1 @@ +True ===================================== testsuite/tests/ghci/prog-mhu008/unitA ===================================== @@ -0,0 +1,5 @@ +-this-unit-id a-0-inplace +-this-package-name a +-i +-ia +M ===================================== testsuite/tests/ghci/prog-mhu008/unitB ===================================== @@ -0,0 +1,6 @@ +-this-unit-id b-0-inplace +-this-package-name b +-package-id a-0-inplace +-i +-ib +M ===================================== 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/all.T ===================================== @@ -316,3 +316,4 @@ test('T25611b', normal, compile, ['']) test('T25611c', normal, compile, ['']) test('T25611d', normal, compile, ['']) test('T25657', normal, compile, ['']) +test('T27828', normal, compile, ['']) ===================================== testsuite/tests/primops/should_run/T27299.hs ===================================== @@ -0,0 +1,23 @@ +{-# LANGUAGE MagicHash #-} +import GHC.Exts +import GHC.Word +import Numeric + +main :: IO () +main = do + putStrLn $ showHex (W# (bitReverse8# 0x55##)) "" + putStrLn $ showHex (W# (bitReverse8# 0xAA##)) "" + putStrLn $ showHex (W# (bitReverse16# 0x5555##)) "" + putStrLn $ showHex (W# (bitReverse16# 0xAAAA##)) "" + putStrLn $ showHex (W# (bitReverse32# 0x5555_5555##)) "" + putStrLn $ showHex (W# (bitReverse32# 0xAAAA_AAAA##)) "" + putStrLn $ showHex (W# (byteSwap16# 0xABCD##)) "" + putStrLn $ showHex (W# (byteSwap32# 0xABCD_EF12##)) "" + putStrLn $ showHex (W# (noinline bitReverse8# 0x55##)) "" + putStrLn $ showHex (W# (noinline bitReverse8# 0xAA##)) "" + putStrLn $ showHex (W# (noinline bitReverse16# 0x5555##)) "" + putStrLn $ showHex (W# (noinline bitReverse16# 0xAAAA##)) "" + putStrLn $ showHex (W# (noinline bitReverse32# 0x5555_5555##)) "" + putStrLn $ showHex (W# (noinline bitReverse32# 0xAAAA_AAAA##)) "" + putStrLn $ showHex (W# (noinline byteSwap16# 0xABCD##)) "" + putStrLn $ showHex (W# (noinline byteSwap32# 0xABCD_EF12##)) "" ===================================== testsuite/tests/primops/should_run/T27299.stdout ===================================== @@ -0,0 +1,16 @@ +aa +55 +aaaa +5555 +aaaaaaaa +55555555 +cdab +12efcdab +aa +55 +aaaa +5555 +aaaaaaaa +55555555 +cdab +12efcdab ===================================== testsuite/tests/primops/should_run/all.T ===================================== @@ -91,3 +91,4 @@ test('T24496' ] , compile_and_run, ['-O']) test('T6026', normal, compile_and_run, ['']) +test('T27299', normal, compile_and_run, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/500bcd9f97f5ff9e157b688bb701016... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/500bcd9f97f5ff9e157b688bb701016... 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