Simon Peyton Jones pushed to branch wip/T27994 at Glasgow Haskell Compiler / GHC Commits: ed2fd53d by Simon Peyton Jones at 2026-10-29T00:07:13+00:00 Make niFixSubst idempotent I discovered (when fixing #27994) that `niFixSubst` didn't actually generate an idempotent subsitution despite its claims. It could return a substitution that mentions domain variables on in its range, when those variables are hidden inside the kind of a type variable occurrence. As a result it can generate ill-kinded types. Boo! The fix is simple, and uses deep substitution. See Note [Finding the substitution fixpoint] I don't think it actually /caused/ any bugs, so there is no regression test. - - - - - ecc5ab3d by Simon Peyton Jones at 2026-10-29T00:07:13+00:00 Fix a nasty bug in fundeps This MR fixes #27994, which turned out to be very tricky. See Note [Exploiting closed type famililes], especially (CF7). I was ending up with TyVars (not TcTyVars) in the solver, because the substitution computed in `getRelevantBranches` mixed the two. The code was just too clever. I ended up simplifying it quite a bit, eliminating fancy footwork in a function `trim_qtvs`. I left behind Historical Note [trim_qtvs] to explain. This patch also fixes one other buglet in the same code. * Over-saturated type families were being mis-handled. See the new use of `saturatedFamApp_maybe`. - - - - - 11 changed files: - compiler/GHC/Core/Coercion/Axiom.hs - compiler/GHC/Core/Predicate.hs - compiler/GHC/Core/TyCo/FVs.hs - compiler/GHC/Core/TyCo/Subst.hs - compiler/GHC/Core/Type.hs - compiler/GHC/Core/Unify.hs - compiler/GHC/Tc/Instance/Family.hs - compiler/GHC/Tc/Solver/FunDeps.hs - + testsuite/tests/typecheck/should_compile/T27994.hs - + testsuite/tests/typecheck/should_compile/T27994a.hs - testsuite/tests/typecheck/should_compile/all.T Changes: ===================================== compiler/GHC/Core/Coercion/Axiom.hs ===================================== @@ -277,8 +277,8 @@ data CoAxBranch -- See Note [CoAxBranch type variables] , cab_eta_tvs :: [TyVar] -- ^ Eta-reduced tyvars - -- cab_tvs and cab_lhs may be eta-reduced; see - -- Note [Eta reduction for data families] + -- For a data family (only) cab_tvs and cab_lhs may be eta-reduced + -- See Note [Eta reduction for data families] , cab_cvs :: [CoVar] -- ^ Bound coercion variables -- Always empty, for now. @@ -286,8 +286,14 @@ data CoAxBranch -- in GHC.Tc.TyCl , cab_roles :: [Role] -- ^ See Note [CoAxBranch roles] + , cab_lhs :: [Type] -- ^ Type patterns to match against + -- For a data family `cab_lhs` may be shorter than the arity + -- of the data type + -- For a type family `cab_lhs` is exactly the family arity + -- See Note [Eta reduction for data families] + , cab_rhs :: Type -- ^ Right-hand side of the equality -- See Note [CoAxioms are homogeneous] ===================================== compiler/GHC/Core/Predicate.hs ===================================== @@ -36,7 +36,7 @@ module GHC.Core.Predicate ( -- Equality left-hand sides CanEqLHS(..), canEqLHS_maybe, canTyFamEqLHS_maybe, - canEqLHSKind, canEqLHSType, eqCanEqLHS + canEqLHSKind, canEqLHSType, eqCanEqLHS, saturatedFamApp_maybe ) where @@ -61,6 +61,8 @@ import GHC.Utils.Misc import GHC.Utils.Panic import GHC.Data.FastString +import GHC.Exts( inline ) + {- ********************************************************************* * * @@ -700,7 +702,9 @@ types/kinds are fully settled and zonked. -- See also Note [Ordering of implicit variables] in "GHC.Rename.HsType" scopedSort :: [Var] -> [Var] -scopedSort = go [] [] +scopedSort xs + | null xs = [] + | otherwise = go [] [] xs where go :: [Var] -- already sorted, in reverse order -> [TyCoVarSet] -- each set contains all the variables which must be placed @@ -781,13 +785,19 @@ canEqLHS_maybe xi | otherwise = canTyFamEqLHS_maybe xi -canTyFamEqLHS_maybe :: Type -> Maybe CanEqLHS -canTyFamEqLHS_maybe xi +saturatedFamApp_maybe :: Type -> Maybe (TyCon,[Type]) +saturatedFamApp_maybe xi | Just (tc, args) <- tcSplitTyConApp_maybe xi , isTypeFamilyTyCon tc , args `lengthIs` tyConArity tc - = Just $ TyFamLHS tc args + = Just (tc,args) + | otherwise + = Nothing +canTyFamEqLHS_maybe :: Type -> Maybe CanEqLHS +canTyFamEqLHS_maybe xi + | Just (tc, args) <- inline saturatedFamApp_maybe xi + = Just $ TyFamLHS tc args | otherwise = Nothing ===================================== compiler/GHC/Core/TyCo/FVs.hs ===================================== @@ -1159,10 +1159,12 @@ nice tight loops. {-# INLINE afvFolder #-} -- See Note [Any-free-var folder] afvFolder :: TyCoFolder (FV (BoundVars, TyCoVar -> Bool) DM.Any) -- 'afvFolder' is short for "any-free-var folder", good for checking --- if any /deep/ free var of a type satisfies a predicate `check_fv` +-- if any /shallow/ free var of a type satisfies a predicate `check_fv` -- The "env" of the (FV env Any) is a pair (bvs,pred) of -- the bound variables (which are definitely not free), and -- an "interesting var" predicate which the client supplies +-- +-- You can get "deep" by supplying a predicate that also looks in the kind afvFolder = TyCoFolder { tcf_view = noView -- See Note [Free vars and synonyms] , tcf_tyvar = do_tcv , tcf_covar = do_tcv @@ -1173,8 +1175,7 @@ afvFolder = TyCoFolder { tcf_view = noView -- See Note [Free vars and synonyms] -- Check the variable itself with check_fv, -- and check its kind (this is a deep folder) do_tcv tcv = MkFV $ \ (bvs,check_fv) -> - Any (not (tcv `elemVarSet` bvs) && - (check_fv tcv || runAny check_fv (afv_type (varType tcv)))) + Any (not (tcv `elemVarSet` bvs) && check_fv tcv) do_hole hole = do_tcv (coHoleCoVar hole) afv_type :: Type -> FV (BoundVars, TyVar -> Bool) DM.Any @@ -1186,16 +1187,32 @@ runAny :: (TyVar -> Bool) -> FV (BoundVars, TyCoVar -> Bool) DM.Any -> Bool {-# INLINE runAny #-} runAny check_fv fvs = DM.getAny (runFV fvs (emptyVarSet, check_fv)) +--------------------------------------------- +-- anyShallowFreeVarsOfType and friends look only for shallow free vars +-- (Currently not needed, left here in case we need it one day) +-- anyShallowFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool +-- {-# INLINE anyShallowFreeVarsOfType #-} +-- anyShallowFreeVarsOfType check_fv ty = runAny check_fv (afv_type ty) + +--------------------------------------------- +-- anyFreeVarsOfType and friends look for deep free vars + +deep_check :: (TyCoVar -> Bool) -> TyCoVar -> Bool +-- This is inefficient because if one tyvar occurs many times +-- in a type, it'll look in its kind at each occurrence. Boo. +deep_check check_fv tcv = check_fv tcv || anyFreeVarsOfType check_fv (varType tcv) + anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool {-# INLINE anyFreeVarsOfType #-} -anyFreeVarsOfType check_fv ty = runAny check_fv (afv_type ty) +-- Looks deeply, into the kinds of the free vars +anyFreeVarsOfType check_fv ty = runAny (deep_check check_fv) (afv_type ty) anyFreeVarsOfTypes :: (TyCoVar -> Bool) -> [Type] -> Bool {-# INLINE anyFreeVarsOfTypes #-} -anyFreeVarsOfTypes check_fv tys = runAny check_fv (afv_types tys) +anyFreeVarsOfTypes check_fv tys = runAny (deep_check check_fv) (afv_types tys) anyFreeVarsOfCo :: (TyCoVar -> Bool) -> Coercion -> Bool -anyFreeVarsOfCo check_fv co = runAny check_fv (afv_co co) +anyFreeVarsOfCo check_fv co = runAny (deep_check check_fv) (afv_co co) noFreeVarsOfType :: Type -> Bool noFreeVarsOfType ty = not $ runAny (const True) (afv_type ty) @@ -1206,6 +1223,7 @@ noFreeVarsOfTypes tys = not $ runAny (const True) (afv_types tys) noFreeVarsOfCo :: Coercion -> Bool noFreeVarsOfCo co = not $ runAny (const True) (afv_co co) + {- ************************************************************************ * * ===================================== compiler/GHC/Core/TyCo/Subst.hs ===================================== @@ -48,6 +48,8 @@ module GHC.Core.TyCo.Subst substTyCoBndr, substVarBndrUsing, checkValidSubst, isValidTCvSubst, + + deepSubstTy ) where import GHC.Prelude @@ -775,9 +777,15 @@ substThetaUnchecked = substTysUnchecked -- building no thunks. See Note [Specialising mappers] in GHC.Core.TyCo.Make type SubstM = StrictReaderT Subst StrictIdentity -runSubstM :: SubstM a -> Subst -> a -runSubstM m subst = runStrictIdentity (runStrictReaderT m subst) +runSubstM :: forall a. (a -> SubstM a) -> Subst -> a -> a {-# INLINE runSubstM #-} +runSubstM tx subst x = runStrictIdentity (runStrictReaderT (tx x) subst) + +subst_ty :: Subst -> Type -> Type +subst_co :: Subst -> Coercion -> Coercion +(subst_ty, subst_co) + = case mapTyCo substTyCoMapper of + (ms_ty, _, ms_co, _) -> (runSubstM ms_ty, runSubstM ms_co) substTyCoMapper :: TyCoMapper SubstM substTyCoMapper @@ -785,8 +793,8 @@ substTyCoMapper , tcm_covar = subst_cv , tcm_hole = subst_ch , tcm_tycobinder = tcv_bndr - , tcm_tcapp_ty = tcapp_ty - , tcm_tcapp_co = tcapp_co + , tcm_tcapp_ty = nopTcAppTy + , tcm_tcapp_co = nopTcAppCo } where subst_tv tv = StrictReaderT $ \subst -> return (substTyVar subst tv) @@ -802,23 +810,15 @@ substTyCoMapper -- Avoid allocation in this very -- common case (E.g. Int, LiftedRep etc) - tcapp_ty :: Type -> TyCon -> [Type] -> SubstM Type - tcapp_ty ty tc tys' - | null tys' = return ty - | otherwise = return (mkTyConApp tc tys') - tcapp_co :: Coercion -> Role -> TyCon -> [Coercion] -> SubstM Coercion - tcapp_co co r tc cos' - | null cos' = return co - | otherwise = return (mkTyConAppCo r tc cos') +nopTcAppTy :: Type -> TyCon -> [Type] -> SubstM Type +nopTcAppTy ty tc tys' + | null tys' = return ty + | otherwise = return (mkTyConApp tc tys') -subst_ty :: Subst -> Type -> Type -subst_co :: Subst -> Coercion -> Coercion -(subst_ty, subst_co) - = case mapTyCo substTyCoMapper of - (ms_ty, _, ms_co, _) -> (run ms_ty, run ms_co) - where - run :: forall a. (a -> SubstM a) -> Subst -> a -> a - run ms subst x = runSubstM (ms x) subst +nopTcAppCo :: Coercion -> Role -> TyCon -> [Coercion] -> SubstM Coercion +nopTcAppCo co r tc cos' + | null cos' = return co + | otherwise = return (mkTyConAppCo r tc cos') substTyVar :: Subst -> TyVar -> Type substTyVar (Subst _ _ tenv _) tv @@ -1019,3 +1019,75 @@ it is /very/ valuable to /keep/ it empty: If the substitution is empty, this is a no-op -- but only if it is empty! -} + + +{- ********************************************************************** +%* * + Deep substitution +%* * +%********************************************************************* -} + +{- Note [Deep substitution] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Deep substitution applies the substitution to the /kinds/ of un-substituted +type variables. Suppose the substitution is + [ k :-> Type ] +and we apply it to the type + Proxy k (a :: k) +Ordinary shallow substitution will give + Proxy Type (a :: k) +which is ill-kinded. Deep substitution will give + Proxy Type (a :: Type) + +Ordinary (shallow) substitution is usually fine, because we will substitute for +`a` as well, but not always. In particular, the pure unifier in in GHC.Core.Unify +uses `niFixSubst` to find a fixpoint, and we really don't want domain tyvars +appearing in the range.See Note [Finding the substitution fixpoint]. + +Deep substitution risks being rather inefficient because it re-applies the +subsitution to the kind at /each occurrence/ of a free variable. We could +perhaps find the free vars, and build a re-kinding substitution, but that's a +bit more complicated. +-} + +deepSubstTyCoMapper :: TyCoMapper SubstM +deepSubstTyCoMapper + = TyCoMapper { tcm_tyvar = subst_tv + , tcm_covar = subst_cv + , tcm_hole = subst_ch + , tcm_tycobinder = tcv_bndr + , tcm_tcapp_ty = nopTcAppTy + , tcm_tcapp_co = nopTcAppCo + } + where + subst_tv tv = StrictReaderT $ \subst -> return (deepSubstTyVar subst tv) + subst_cv cv = StrictReaderT $ \subst -> return (deepSubstCoVar subst cv) + subst_ch ch = StrictReaderT $ \subst -> return (deepSubstCoHole subst ch) + + tcv_bndr :: TyCoVar -> ForAllTyFlag -> (TyCoVar -> SubstM r) -> SubstM r + tcv_bndr tcv _vis k + = StrictReaderT $ \subst -> + let !(subst', tcv') = substVarBndrUsing deepSubstTy subst tcv + in runStrictReaderT (k tcv') subst' + +deepSubstTy :: Subst -> Type -> Type +deepSubstTy = case mapTyCo deepSubstTyCoMapper of + (subst_ty, _, _, _) -> runSubstM subst_ty + +deepSubstTyVar :: Subst -> TyVar -> Type +deepSubstTyVar subst@(Subst _ _ tenv _) tv + = assert (isTyVar tv) $ + case lookupVarEnv tenv tv of + Just ty -> ty + Nothing -> TyVarTy (updateVarType (deepSubstTy subst) tv) + +deepSubstCoVar :: Subst -> CoVar -> Coercion +deepSubstCoVar subst@(Subst _ _ _ cenv) cv + = case lookupVarEnv cenv cv of + Just co -> co + Nothing -> CoVarCo (updateVarType (deepSubstTy subst) cv) + +deepSubstCoHole :: Subst -> CoercionHole -> Coercion +-- See Note [Substituting in a coercion hole] +deepSubstCoHole subst h@(CH { ch_co_var = cv }) + = HoleCo (h { ch_co_var = updateVarType (deepSubstTy subst) cv }) ===================================== compiler/GHC/Core/Type.hs ===================================== @@ -483,7 +483,7 @@ expandTypeSynonyms ty expandTypeSynonymsX :: Subst -> Type -> Type expandTypeSynonymsX = case mapTyCo expandTypeSynonymMapper of - (exp_ty, _, _, _) -> \subst ty -> runSubstM (exp_ty ty) subst + (exp_ty, _, _, _) -> runSubstM exp_ty expandTypeSynonymMapper :: TyCoMapper SubstM -- Just like substitution, but treat TyConApp specially ===================================== compiler/GHC/Core/Unify.hs ===================================== @@ -28,13 +28,12 @@ import GHC.Types.Var.Env import GHC.Types.Var.Set import GHC.Core.Type hiding ( getTvSubstEnv ) import GHC.Core.Coercion hiding ( getCvSubstEnv ) -import GHC.Core.Predicate( scopedSort ) import GHC.Core.TyCon import GHC.Core.Predicate( CanEqLHS(..), canEqLHS_maybe ) import GHC.Core.TyCon.Env import GHC.Core.TyCo.Rep import GHC.Core.TyCo.Compare ( eqType, tcEqType, tcEqTyConAppArgs ) -import GHC.Core.TyCo.Subst ( mkTvSubst ) +import GHC.Core.TyCo.Subst ( mkTvSubst, deepSubstTy ) import GHC.Core.Map.Type import GHC.Core.Multiplicity @@ -1063,21 +1062,31 @@ During unification we use a TvSubstEnv/CvSubstEnv pair that is Note [Finding the substitution fixpoint] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Finding the fixpoint of a non-idempotent substitution arising from a -unification is much trickier than it looks, because of kinds. Consider +We want an /idempotent/ substitution, so `niFixSubst` takes a non-idempotent +one and composes it with itself until it becomes idempotent. Thus if the original +is S0, we compute S1 = S0 o S0, S2 = S1 o S1, etc. + +A variable chain v0 :-> v1 :-> ... :-> vm therefore takes about log2 m rounds, +The unifier can build such. For example: + (a, a, a, ..., a) ~ (x1, x2, x3, ..., xm) +produces a :-> x1, x1 :-> x2, ..., x(m-1) :-> xm. + +Finding the fixpoint is much trickier than it looks, because of kinds. +Consider T k (H k (f:k)) ~ T * (g:*) If we unify, we get the substitution [ k -> * , g -> H k (f:k) ] +This isn't idempotent: it mentions `k` in the range. + To make it idempotent we don't want to get just [ k -> * , g -> H * (f:k) ] -We also want to substitute inside f's kind, to get - [ k -> * - , g -> H k (f:*) ] -If we don't do this, we may apply the substitution to something, -and get an ill-formed type, i.e. one where typeKind will fail. +because (H * (f:k)) is itself ill-kinded, and `typeKind` will fail. This happened, for example, in #9106. +So (yuckily) we must also substitute inside f's kind, to get + [ k -> * + , g -> H * (f:*) ] It gets worse. In #14164 we wanted to take the fixpoint of this substitution @@ -1090,84 +1099,45 @@ the invocation of F! We don't have a function that recursively applies substitutions inside the kinds of variable occurrences (and probably rightly so). -So, we work as follows: - - 1. Start with the current substitution (which we are - trying to fixpoint - [ xs :-> F a (z :: a) (rest :: G a (z :: a)) - , a :-> b ] - - 2. Take all the free vars of the range of the substitution: - {a, z, rest, b} - NB: the free variable finder closes over - the kinds of variable occurrences - - 3. If none are in the domain of the substitution, stop. - We have found a fixpoint. - - 4. Remove the variables that are bound by the substitution, leaving - {z, rest, b} - - 5. Do a topo-sort to put them in dependency order: - [ b :: *, z :: a, rest :: G a z ] - - 6. Apply the substitution left-to-right to the kinds of these - tyvars, extending it each time with a new binding, so we - finish up with - [ xs :-> ..as before.. - , a :-> b - , b :-> b :: * - , z :-> z :: b - , rest :-> rest :: G b (z :: b) ] - Note that rest now has the right kind - - 7. Apply this extended substitution (once) to the range of the - /original/ substitution. (Note that the extended substitution - would go on forever if you tried to find its fixpoint, because it - maps z to z.) - - 8. And go back to step 1 - -In Step 6 we use the free vars from Step 2 as the initial -in-scope set, because all of those variables appear in the -range of the substitution, so they must all be in the in-scope -set. But NB that the type substitution engine does not look up -variables in the in-scope set; it is used only to ensure no -shadowing. +Ugh! This whole thing is pretty horrible. But the solution is simple enough: + + Use deep substitution (deepSubstTy) + +(deepSubst `s` (Proxy k (a::k)) applies the substitution `s` not only to +the occurrence of `k` in the argument of `Proxy`, but also to the `k` inside +the kind of `a`. See Note [Deep substitution] in GHC.Core.TyCo.Subst. + +So `niFixSubst` just applies the substitution /deeply/ to the types in its +range, until we reach a fixed point. Easy! -} niFixSubst :: InScopeSet -> TvSubstEnv -> Subst -- Find the idempotent fixed point of the non-idempotent substitution -- This is surprisingly tricky: -- see Note [Finding the substitution fixpoint] --- ToDo: use laziness instead of iteration? niFixSubst in_scope tenv - | not_fixpoint = niFixSubst in_scope (mapVarEnv (substTy subst) tenv) - | otherwise = tenv_subst + | isEmptyVarEnv tenv -- Fast path for common case + = mkEmptySubst in_scope + | otherwise + = -- pprTrace "niFixSubst" (vcat [ text "In: " <+> ppr tenv + -- , text "Out:" <+> ppr (S.getTvSubstEnv subst) ]) + subst where - tenv_subst = mkTvSubst in_scope tenv -- This is our starting point - - range_tvs :: [TyVar] - range_tvs = nonDetVarSetElems $ - tyCoVarsOfTypes $ - nonDetEltsUFM tenv - -- It's OK to use nonDetEltsUFM (twice) here because - -- the order of range_tvs is immaterial - - not_fixpoint = any in_domain range_tvs - in_domain tv = tv `elemVarEnv` tenv - - free_tvs = scopedSort (filterOut in_domain range_tvs) + subst = niFixSubst' 1 in_scope tenv - -- See Note [Finding the substitution fixpoint], Step 6 - subst = foldl' add_free_tv tenv_subst free_tvs - - add_free_tv :: Subst -> TyVar -> Subst - add_free_tv subst tv - | isTyVar tv = extendTvSubst subst tv (mkTyVarTy tv') - | otherwise = subst -- Ignore free coercion variables - where - tv' = updateTyVarKind (substTy subst) tv +niFixSubst' :: Int -> InScopeSet -> TvSubstEnv -> Subst +niFixSubst' n in_scope tenv_orig + | fixpoint_found = mkTvSubst in_scope tenv_orig + | otherwise = niFixSubst' (n+1) in_scope tenv_new + where + in_dom tv = tv `elemVarEnv` tenv_orig + tenv_new = mapVarEnv (deepSubstTy subst) tenv_orig + subst = mkTvSubst in_scope tenv_orig + + fixpoint_found = nonDetStrictFoldUFM and_fix True tenv_orig + and_fix :: Type -> Bool -> Bool + and_fix _ False = False + and_fix ty _ = not (anyFreeVarsOfType in_dom ty) {- ************************************************************************ ===================================== compiler/GHC/Tc/Instance/Family.hs ===================================== @@ -16,6 +16,7 @@ import GHC.Prelude import GHC.Driver.DynFlags import GHC.Driver.Env +import GHC.Core.Predicate( saturatedFamApp_maybe ) import GHC.Core.FamInstEnv import GHC.Core.Coercion import GHC.Core.TyCon @@ -715,15 +716,9 @@ reportInjectivityErrors dflags fi_ax axiom inj when wrong_bare_rhs $ reportBareVariableInRHSErr fam_tc bare_variables axiom -- | Is type headed by a type family application? -isTFHeaded :: Type -> Bool -- See Note [Verifying injectivity annotation], case 3. -isTFHeaded ty | Just ty' <- coreView ty - = isTFHeaded ty' -isTFHeaded ty | (TyConApp tc args) <- ty - , isTypeFamilyTyCon tc - = args `lengthIs` tyConArity tc -isTFHeaded _ = False - +isTFHeaded :: Type -> Bool +isTFHeaded ty = isJust (saturatedFamApp_maybe ty) -- | If a RHS is a bare type variable return a set of LHS patterns that are not -- bare type variables. ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -24,16 +24,16 @@ import GHC.Tc.Types.Constraint import GHC.Core.FamInstEnv import GHC.Core.Coercion import GHC.Core.TyCo.Rep( Type(..) ) -import GHC.Core.Predicate( EqRel(..) ) +import GHC.Core.TyCo.Subst( deepSubstTy ) +import GHC.Core.Predicate( EqRel(..), saturatedFamApp_maybe ) import GHC.Core.TyCon import GHC.Core.Unify( AmIUnifying(..) , tcUnifyTysForInjectivity, typeListsAreApart ) import GHC.Core.Coercion.Axiom -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( tyVarKind ) import GHC.Types.Var.Set import GHC.Types.Var.Env( mkInScopeSet ) @@ -57,7 +57,6 @@ Here is our plan for dealing with functional dependencies * send the current constraint back to the start of the pipeline; it might now be soluble, and it probably isn't inert - * Once a unification is done, it can't be un-done. So we must be very careful not to threaten completeness by doing a unification when there might be another way to solve the constraint. @@ -613,6 +612,7 @@ tryFamEqFunDeps mode eqs_for_me fam_tc work_args mkTopFamEqFDs :: TyCon -> [TcType] -> EqCt -> SolverStage [FunDepEqns] mkTopFamEqFDs fam_tc work_args work_item + -- NB: work_args exactly saturate fam_tc | isOpenTypeFamilyTyCon fam_tc , Injective inj_flags <- tyConInjectivityInfo fam_tc = -- Open, injective type families @@ -709,24 +709,24 @@ getRelevantBranches ax work_args work_rhs , 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' + -- See (RW1)-(RW3) in Note [Relevance] + , let lhs_tys' = map (deepSubstTy subst) lhs_tys + -- deepSubstTy: see (CF8) in Note [Exploiting closed type families] , noEarlierMatchCheck lhs_tys' branch -- See (RW4) in Note [Relevance] - = Just (FDEqns { fd_qtvs = qtvs' - , fd_eqs = zipWith Pair branch_tys' work_tys }) - -- Do not apply the substition to `work_tys`; - -- See (CF7) in Note [Exploiting closed type families] + = -- Ignore the substitution, except for `noEarlierMatchCheck` + -- See (CF7) in Note [Exploiting closed type families] + Just (FDEqns { fd_qtvs = qtvs + , fd_eqs = zipWith Pair (rhs_ty:lhs_tys) work_tys }) + -- Do not apply the substitution to `work_tys`; + -- See (CF9) in Note [Exploiting closed type families] + | otherwise = Nothing mkTopOpenFamEqFDs :: TyCon -> [Bool] -> [TcType] -> EqCt -> TcS [FunDepEqns] -- Implements (INJFAM:Wanted/top-open) -- See Note [Exploiting open type families] +-- NB: work_args exactly saturate fam_tc mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs }) = do { fam_envs <- getFamInstEnvs ; let branches :: [CoAxBranch] @@ -738,12 +738,11 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs }) 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 - -- 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) + | Just {} <- tcUnifyTysForInjectivity Matching [branch_rhs] [work_rhs] + -- No need for an apartness check here; + -- for open type families there are no "preceding" equations + -- Both branch_lhs_tys and work_args exactly saturate fam_tc + = Just (mkInjectivityFDEqn branch_qtvs inj_flags branch_lhs_tys work_args) | otherwise = Nothing @@ -756,9 +755,9 @@ 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 -- eqns_from_self: see (INJFAM:Wanted/Self) - eqns_from_self = case tcSplitTyConApp_maybe work_rhs of - Just (tc,rhs_tys) | tc==fam_tc -> [mk_eqn rhs_tys] - _ -> [] + eqns_from_self = case saturatedFamApp_maybe work_rhs of + Just (tc, rhs_tys) | fam_tc == tc -> [mk_eqn rhs_tys] + _ -> [] ; return (eqns_from_inerts ++ eqns_from_self) } where @@ -768,7 +767,10 @@ mkLocalFamEqFDs eqs_for_me fam_tc inj_flags work_args work_rhs | otherwise = Nothing do_one _ = pprPanic "interactFunEq 2" (ppr fam_tc) -- TyVarLHS - mk_eqn iargs = mkInjectivityFDEqn inj_flags [] work_args iargs + mk_eqn iargs = mkInjectivityFDEqn [] inj_flags work_args iargs + + +{- See Historical Note [trim_qtvs] trim_qtvs :: Subst -> [TyVar] -> (Subst, [TyVar]) -- Tricky stuff: see (OF1) in Note [Exploiting open type families] @@ -790,7 +792,7 @@ trim_qtvs unif_subst qtvs subst' = extendTvSubstWithClone subst tv tv' -- extendTvSubstWithClone: see (OF1b) in -- Note [Exploiting open type families] - +-} ----------------------------------------- -- Built-in type families @@ -883,15 +885,22 @@ mkLocalBuiltinFamEqFDs eqs_for_me fam_tc ops work_args work_rhs ; return (eqns_from_inerts ++ eqns_from_self) } -------------------- -mkInjectivityFDEqn :: [Bool] -- Injectivity flags - -> [TcTyVar] -- Quantify these +mkInjectivityFDEqn :: [TcTyVar] -- Quantify these + -> [Bool] -- Injectivity flags -> [TcType] -> [TcType] -- Make these equal -> FunDepEqns -- When F s1 s2 s3 ~ F t1 t2 t3, and F has injectivity info [True,False,True] -- return the FDEqns { fd_eqs = [Pair s1 t1, Pair s3 t3] } --- The injectivity flags [Bool] will not all be False, but nothing goes wrong if they are -mkInjectivityFDEqn inj_args qtvs lhs_args rhs_args - = FDEqns { fd_qtvs = qtvs, fd_eqs = eqs } +-- The injectivity flags [Bool] will not all be False, +-- but nothing goes wrong if they are +mkInjectivityFDEqn qtvs inj_args lhs_args rhs_args + = assertPpr (let len = length inj_args in + len == length lhs_args && len == length rhs_args) + (vcat [ text "inj_args:" <+> ppr inj_args + , text "lhs_args:" <+> ppr lhs_args + , text "rhs_args:" <+> ppr rhs_args ]) $ + -- Need inj_args lhs_args and rhs_args to be same length for zip3 + FDEqns { fd_qtvs = qtvs, fd_eqs = eqs } where eqs = [ Pair lhs_arg rhs_arg | (True, lhs_arg, rhs_arg) <- zip3 inj_args lhs_args rhs_args ] @@ -1104,7 +1113,7 @@ the Injective Type Families paper. For open type families, suppose we have [W] F alpha ~ Int->Int -Then, since F has been checked as injective, and the RHS `a->a` (pre-)unifies +Then, since F has been checked as injective, and the RHS `a->a` (pre-)matches with the `Int->Int` in the Wanted with substitution [a :-> Int], we can add a derived FunDepEqns FDEqns{ fd_qtvs = [], fd_eqs = [ [Int] ~ alpha ] } @@ -1119,7 +1128,7 @@ instance are bound by the pre-unification step. Suppose we have [W] F alpha ~ [ty] -Then, the RHS [G a] pre-unifies with the RHS of the Wanted, but with an +Then, the RHS [G a] pre-matches 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`) @@ -1133,36 +1142,44 @@ In general we have: 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 +Suppose `b` pre-matches with `rhs`, with substitution `S`. We /ignore/ +`S` and simply generate the FunDepEqs + FDEqns{ fd_qtvs = qs, fd_eqs = [ t1 ~ a1, t3 ~ a3 ] +These 'fd_qtvs' are subsequently instantiated to fresh meta-variables by +'instantiateFunDepEqns'. See Historical Note [trim_qtvs]. + +Historical Note [trim_qtvs] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In Note [Exploiting open type families], we previously tried to make use of +the matching substitution `S`, by defining + unbound_qs = qs \ dom(S) +so that we could make fresh meta-variables for only the unbound `qs`. +But it turned out to be tricky. Suppose (TQ1) + qs = [ k::*, a::k ] + S = [ k :-> UnliftedType ] +Then we want + unbound_qs = [ a::UnliftedType ] -- Must apply S to q's kind!! + +And (TQ2), although I'm not sure if this can actually 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` used to be 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 + +(TQ3) This was hard enough for open type type families, which use matching. +But it was ridiculously hard for /closed/ type families which use pre-/unification/ +so that the substitution `S` has both meta-tyvars and instance-head tyvars in +the range. + +It's much easier to drop all this and just make fresh meta-tyvars for +all the quantified type variables. Note [Exploiting closed type families] see `mkTopClosedFamEqFDs` ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1194,9 +1211,6 @@ More precisely, here is the very clever Closed Family Fundep Algorithm (CFFA) with fresh unification vars in lhs and rhs for the quantified variables of the equation. - 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). @@ -1391,26 +1405,59 @@ Key point: equations that are not relevant do not need to be considered for fund (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 + This substitution can bind both /quantified/ type variables from the instance, + and /unification variables/ from the solver. Moreover, both kind of type variable + can appear in the range of the substitution. + + That's pretty complicated, so we are very cautious about using the returned + substitution. I had a long struggle (#27994) when we were previously trying to + apply that returned substitution as an optimisation. But because type variables + can occur in kinds, it was a losing battle -- I ended up with TyVars from the + instance head escaping into the solver. Consider + + type F :: forall k. k -> * + type instance F k a where + F (k->*) (b::k->*) = Int + + [W] F kappa (alpha::kappa) ~ Int + + We unify the Wanted with the equation to get the substitution + [ kappa :-> k->*, b :-> alpha ] + I tried using `trim_qtvs` (see Historical Note [trim_qtvs]) but my head hurt + FAR too much: #27994 is an excellent example. I gave up and now just ignore + the substitution, making a fresh meta-var for each quantified variable. + +(CF8) When computing relevance (Note [Relevance] (R2)) we use `noEarlierMatch` + on S(lhs). But we must use /deep/ substitution on LHS. Consider + type family F (a :: k) r where + F @Type (Maybe Bool) r = r -- B0 + F @Type ((f :: Type -> Type) Int) r = Bool -- B1 + F @k ((g :: Type -> k) Int) r = r -- B2 + + [W] F @Type alpha Char ~ Char + The `tcUnifyTysForInjectivity` will return substitution + [k :-> Type, r :-> Char, alpha :-> (g :: Type->Type) Int], with g unbound + If we used `substTy` on the LHS-tys for B2 we'd get + lhs_tys' = [Type, (g :: Type -> k) Int, Char] + That's ill-kinded because of the free `k`; and (worse) when `noEarlierMatch` matches + lhs_tys' against earlier equations, (B1) will fail to match. So (B2) will be + judged relevant, even though it isn't. Bad, bad. Use deep substitution. + +(CF9) Notice that, when generating the fundep equations for the solver to deal + with, we do /not/ apply the pre-unifying substitution S. The types wlhs,wrhs + contain meta-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) + We don't want to substitute `alpha` away! In fact we just generate these eqns: + FDEqns { fd_qtvs = [a,b], fd_eqs [ [a] ~ alpha + , Maybe b ~ beta + , (a, G b) ~ (Int, [gamma]) ] } + with `fd_qtvs` being the quantified variables of the equation, the LHSs + being the types from the equation and the RHSs being the types from the Wanted. + Notice that we thereby uphold the `fd_eqs` invariant in `FDEqns` (see its data + type decl). Note [Cache-caused loops] ~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1517,8 +1564,8 @@ instantiateFunDepEqns (FDEqns { fd_qtvs = qtvs, fd_eqs = eqs }) 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 + -- The kinds of `qtvs` can have free variables; + -- in the FDEqns produced by GHC.Tc.Instance.FunDeps.improveFromInstEnv empty_subst = mkEmptySubst $ mkInScopeSet $ tyCoVarsOfTypes (map tyVarKind qtvs) ===================================== testsuite/tests/typecheck/should_compile/T27994.hs ===================================== @@ -0,0 +1,48 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeFamilies #-} +module T27994a (l2) where + +import Data.Kind (Constraint, Type) + +l1 :: [String] +l1 = ["hello", "world!"] + +l2 :: [Int] +l2 = gmap (HCons length HNil) l1 + +----- + +type HList :: [Type] -> Type +data HList p where + HNil :: HList '[] + HCons :: x -> HList xs -> HList (x:xs) + +type ($$) :: k -> [Type] -> Type +type family s $$ p where + (s :: Type) $$ '[] = s + (s :: Type -> k) $$ (a:b) = s a $$ b + +type Doms :: [Type] -> [Type] +type family Doms t where + Doms '[] = '[] + Doms ((a -> b) : t) = a : Doms t + +type Codoms :: [Type] -> [Type] +type family Codoms t where + Codoms '[] = '[] + Codoms ((a -> b) : t) = b : Codoms t + +type GMap :: k -> [Type] -> Constraint +class GMap (s :: k) t | t -> k where + gmap :: HList t -> s $$ Doms t -> s $$ Codoms t + +instance GMap [] '[a -> b] where + gmap :: HList '[a -> b] -> [a] -> [b] + gmap (HCons f HNil) = go + where + go :: [a] -> [b] + go [] = [] + go (x:xs) = f x : go xs ===================================== testsuite/tests/typecheck/should_compile/T27994a.hs ===================================== @@ -0,0 +1,53 @@ +{-# LANGUAGE DataKinds, TypeFamilies, PolyKinds, GADTs, AllowAmbiguousTypes #-} +module T27994 where + +import Data.Kind (Type) +import Data.Proxy (Proxy) + +type F :: forall{k}. k -> Type -> Type +type family F s x where + F (s :: Type -> k) (Proxy s) = Int + +f :: forall k (s :: k) x. F s x -> x +f _ = undefined + +g :: Proxy Maybe -> () +g _ = () + +data T a where + MkT :: T Int + +test :: T a -> () +test t = (\y -> case t of MkT -> g y) (f (3 :: Int)) + +{- [W] F @k_azX (s_azY::k_azX) p_azN ~ Int + +unify [*->k, s::*->k, Proxy @(*->k) (s::*->k), Int] + ~ [k_azX, s_azY::k_azX, p_azN, Int] + + --> [ k_azX :-> (* -> k) + , s :-> s_azY::k_azX + , p_azN :-> Proxy @(*->k) (s::*->k) ] + + fixpt --> [ k_azX :-> Type -> k + , s :-> s_azY::(Type -> k) + , p_azN :-> Proxy @(Type->k) (s::k_azX) ] + +Generate a [W] for each pair + [W] k ~ k_azX + [W] s ~ s_azY + [W] Proxy s ~ p_azN + [W] Int ~ Int +As an opt (claim) apply subst first + [W] k_azX ~ k_azX + [W] s_azY ~ s_azY + [W] Proxy s_azY ~ p_azN + [W] Int ~ Int + +-- [W] F @k_azX s_azY[tau] p_azN ~ Int +-- Want: fresh k' s' +-- [W] k' ~ k_azX +-- [W] s':k' ~ s_azY:k_azX +-- [W] Proxy s' ~ x +-} + ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -972,4 +972,6 @@ test('T27557', normal, compile, ['']) test('T27664', normal, compile, ['']) test('T27916', normal, compile, ['']) test('T26543_orig', normal, compile, ['']) +test('T27994', normal, compile, ['']) +test('T27994a', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/6af2da8dddf42eb3aa8ae999b3a8b5f... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/6af2da8dddf42eb3aa8ae999b3a8b5f... 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