Simon Peyton Jones pushed to branch wip/T27994 at Glasgow Haskell Compiler / GHC Commits: d2c3c7d7 by Simon Peyton Jones at 2026-10-30T16:24:52+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. - - - - - a5018b9a by Simon Peyton Jones at 2026-10-30T16:25:09+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. For /closed/ families we no longer call `trimQtvs` (was `trim_qtvs`). Open families still do use `trimQtvs`. See Note [trimQTvs] 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`. - - - - - 13 changed files: - + changelog.d/T27994 - 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/T27994b.hs - testsuite/tests/typecheck/should_compile/all.T Changes: ===================================== changelog.d/T27994 ===================================== @@ -0,0 +1,7 @@ +section: compiler +issues: #27994 +mrs: !16842 +synopsis: + Fix a compiler Lint error in a heavily kind-polymorphic program +description: + There was a subtle bug deep in the code for computing functional dependencies for type families. ===================================== 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,86 @@ 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 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]. + +Wrinkles: + +(DS1) Deep substitution risks being rather inefficient because it re-applies the + substitution 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. + +(DS2) Deep substitution, as implemented here, relies on invariant + (NoTypeShadowing); see Note [No type-shadowing in Core] in Core.hs. + Otherwise we may have e.g. + S = [r :-> LiftedRep] in-scope = {r, x} + T = forall (r :: RuntimeRep). (x :: TYPE r) -> ... + and we would want to apply the outer substitution S to the + occurrence of r in the kind of x. But we'll have removed it + from the subsitution when pasing the 'forall r'. +-} + +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 chains. 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,53 @@ 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! + +Historical Note: + Immediately prior to this solution there was a previous, more complicated + `niFixSubst` which involved finding the (deep) free variables and "re-kinding" + them. It accomplished essentially the same things, and it avoided the + potential duplication noted in Note [Deep substitution]. But it was pretty + subtle and this version is more obviously correct. +End of Historical Note -} 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 + subst = niFixSubst' 1 in_scope tenv - free_tvs = scopedSort (filterOut in_domain range_tvs) - - -- 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, elemSubst, extendTvSubstWithClone ) +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( TyVar, updateVarType, 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 @@ -694,6 +694,8 @@ hasRelevantGiven eqs_for_me work_args (EqCt { eq_rhs = work_rhs }) getRelevantBranches :: CoAxiom Branched -> [TcType] -> Xi -> [FunDepEqns] -- Return the FunDepEqns that arise from each relevant branch -- Implements Note [Relevance] +-- Caller will only use these FunDepEqns if there is just one relevant +-- equation, i.e. the returned [FunDepEqns] is a singleton. getRelevantBranches ax work_args work_rhs = go (fromBranches (coAxiomBranches ax)) where @@ -709,24 +711,33 @@ 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` + Just $ + if all (`elemSubst` subst) qtvs + then -- `subst` eliminates all qtvs; and no qtvs in range of subst + -- See (CF7)(A) in Note [Exploiting closed type families] + FDEqns { fd_qtvs = [] + , fd_eqs = zipWith Pair (substTy subst rhs_ty : lhs_tys') + work_tys } + -- Do not apply `subst` to `work_tys`; + -- See (CF9) in Note [Exploiting closed type families] + + else -- Abandon `subst`; re-create it from (rhs_ty ~ work_rhs) + -- See (CF7)(B) in Note [Exploiting closed type families] + FDEqns { fd_qtvs = qtvs + , fd_eqs = zipWith Pair (rhs_ty:lhs_tys) work_tys } + | 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] @@ -739,11 +750,14 @@ mkTopOpenFamEqFDs fam_tc inj_flags work_args (EqCt { eq_rhs = work_rhs }) , 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 + -- 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 + , let (subst', qtvs') = trimQtvs 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) + -- We must apply the substitution here see + -- the Basic Plan in Note [Exploiting open type families] + = Just (mkInjectivityFDEqn qtvs' inj_flags branch_lhs_tys' work_args) | otherwise = Nothing @@ -756,9 +770,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,11 +782,12 @@ 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 + -trim_qtvs :: Subst -> [TyVar] -> (Subst, [TyVar]) --- Tricky stuff: see (OF1) in Note [Exploiting open type families] -trim_qtvs unif_subst qtvs +trimQtvs :: Subst -> [TyVar] -> (Subst, [TyVar]) +-- Tricky stuff: see Note [Exploiting open type families] and Note [trimQtvs] +trimQtvs unif_subst qtvs = go unif_subst qtvs where go :: Subst -> [TyVar] -> (Subst, [TyVar]) @@ -786,10 +801,9 @@ trim_qtvs unif_subst qtvs go_fresh subst tv tvs = (subst'', tv':tvs') where !(subst'', tvs') = go subst' tvs - tv' = tv `setTyVarKind` substTy subst (tyVarKind tv) + tv' = updateVarType (substTy subst) tv subst' = extendTvSubstWithClone subst tv tv' - -- extendTvSubstWithClone: see (OF1b) in - -- Note [Exploiting open type families] + -- extendTvSubstWithClone: see (TQ1) in Note [trimQtvs] ----------------------------------------- @@ -883,15 +897,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 ] @@ -1096,73 +1117,108 @@ Note [Exploiting closed type families]. 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 +For an open type family, generating fundeps from a top-level type instance +is covered in Section 5.2 in the Injective Type Families paper. + +Basic plan: Suppose type family F a b = r | r -> b + and Wanted [W] F wlhs1 wlhs2 ~ wrhs + Then for each type instance (F lhs1 lhs2 = rhs) + * Pre-match `rhs` against `wrhs` to get a substitution S + * Generate fundep equalities S(lhs2) ~ wrhs + one for each fundep in the type family + +For example, suppose we have + type family F a b = r | r -> a + type instance F [a] Int = a->a + [W] F alpha beta ~ Int->Int +Then we pre-match template (a->a) against target (Int->Int) to get +substitution S = [a :-> Int]. Then we can generate FDEqns{ fd_qtvs = [], fd_eqs = [ [Int] ~ alpha ] } and thereby emit (via `instantiateFunDepEqns`) [W] [Int] ~ alpha +Note that `fd_qtvs = []`; we have substituted away the quantifed type variable `a`. 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 + type instance F (b -> Maybe a) = [(G a,b)] -- G is a type family + [W] F alpha ~ [(ty,Int)] - [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 ] } +Then, the RHS [(G a,b)] pre-matches with the RHS of the Wanted, but with +the substitution [b :-> Int], which does not fix `a`. So, after trimming +the quantified type variables, we get this FunDepEqns: + FDEqns{ fd_qtvs = [a], fd_eqs = [ (Int -> 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 + [W] (Int -> Maybe gamma) ~ alpha -- Fresh gamma +We have learned that `alpha` must be a list of functions, but that is all; +we don't know `gamma`. + +It gets tricker. Suppose we have + type family F @k a = r | r -> k,a + type instance F @k (Proxy @k (a::k)) = T k + [W] F alpha beta ~ T Type +Matching the RHS gives substitution [k :-> Type]. But we do /not/ want +to end up with this: + FDEqns{ fd_qtvs = [a::k], fd_eqs = [ Proxy @Type (a::k) ~ alpha ] } +because that `k`, hidden inside the kind of `a`, escapes into the solver. + +Instead we must not only "trim" the quantified variables of the equation, +but /substitute/ in the kinds of the leftover quantified ones: see Note [trimQtvs]. +Then we get + FDEqns{ fd_qtvs = [a::Type], fd_eqs = [ Proxy @Type (a::Type) ~ alpha ] } + +Side note: + +You might wonder whether we can use the same solution as we do for /closed/ +families, by generating an equality for the RHSs; see (CF7). But we can't. +Example: + type family G a where G Int = Char + type family F a b = r | r -> a + type instance F a [c] = (a, G a) -- (I1) + type instance F Int Bool = (Int, Bool) -- (I2) + [W] F alpha Bool ~ (Int,gamma) +Note that (I1) and (I2) are pariwise-injective: if the RHSs are the same, +the LHSs are the same /in the injective position(s)/. See Section 4.2 in +the "Injective Type Families" paper. We pre-match (I1) against the Wanted +giving substitution [a :-> Int]. We /cannot/ then generate + FDEqns { fd_qtvs = [a,c], fd_eqs = [ a~alpha + , (a,G a)~(Int,gamma) ] } +where the second equality (wrongly)equates the RHSs. This is wrong because we +can solve those fundeps unifying alpha:=Int, gamma:=Char, by reducing (G a) to +Char. So we end up with [W] F Int Char, which is insoluble. Bad. + +End of side note. + +Note [trimQtvs] +~~~~~~~~~~~~~~~ +In Note [Exploiting open type families], we needed to "trim" the quantified +type variables of the axiom, removing ones that are eliminated by the +auubstitution `S`. So can we just do this? + unbound_qs = qs \ dom(S) +so that we could make fresh meta-variables for only the unbound `qs`. +No, we can't. 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`. + +The function `trimQtvs` does the job. 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 + +We only use `trimQtvs` for /open/ families. For /closed/ families where we +/unify/ (rather than match) the equation with the Wanted, it just doesn't work +(#27994), because the substitution `S` has both meta-tyvars and instance-head +tyvars in the range. See (CF7). Note [Exploiting closed type families] see `mkTopClosedFamEqFDs` ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1194,9 +1250,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). @@ -1303,7 +1356,7 @@ 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`. + This bale-out is implemented in `tryFDEqns`. (CF5) Consider (see "Yikes5" in #23162): type family F a where @@ -1353,32 +1406,20 @@ Key point: equations that are not relevant do not need to be considered for fund `app` Proxy @'[ty_n] Every `app` call gives rise to a Wanted of the form: - [W] MapId acc_i ++ MapId '[ty_i] ~ MapId (acc_i ++ '[ty_i]) - while the overall result type gives us a Wanted of the form - [W] acc_n ++ '[ty_n] ~ [ty_1, ..., ty_n] - By using (CFFA) on this result Wanted, we deduce that we must have - acc_n ~ [ty_1, ..., ty_{n-1}] - which is a flat list. Repeating the process, (CFFA) allows us to deduce that - acc_i ~ [ty_1, ..., ty_{i-1}] - for all i. This allows the other Wanteds to be solved directly, giving rise to proof terms with the typical triangular O(n^2) shape - co_i = (O(i) proof that MapId acc_i ++ MapId '[ty_i] ~ acc_{i+1}) ; (O(i) proof that acc_{i+1} ~ MapId (acc_i ++ '[ty_i])) - However, /without/ (CFFA), 'acc_i' is not unified with a flat list but is left as the nested application: - acc_i ~ (... (('[ty_1] ++ '[ty_2]) ++ '[ty_3]) ... ++ '[ty_{i-1}]) - This means that 'MapId acc_i' is stuck until we reduce the above, which takes O(i^2) type family reduction steps, instead of O(i). The same applies to the other proof term involving 'MapId (acc_i ++ '[ty_i])'. @@ -1388,29 +1429,77 @@ 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 +(CF7) Relevance. The function `getRelevantBranches` finds the relevant branch(es) + using the (CFFA). Given an equation + type family F a b where { ...; F lhs1 lhs2 = rhs; ... } + is the equation relevant for this Wanted? + [W] F wlhs1 wlhs2 ~ wrhs + We pre-unify [wrhs,wlhs1,wlhs2] against [rhs,lhs1,lhs2], getting back a + substitution `S` that makes the two as equal as poss. 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 `S`. 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::k->*) ] + I tried using `trimQtvs` (see Note [trimQtvs]) but my head hurt + FAR too much: #27994 is an excellent example. + + So here's the plan: + (A) As a fast-path optimisation, if `S` binds all the quantified variables of + the type-family equation (which is common), it's all easy: generate + FDEqns { fd_qtvs = [] + , fd_eqs = [ S(lhs1) ~ wlhs1, S(lhs2) ~ wlhs2, S(rhs) ~ wrhs } + Note that we do not apply S to `wlhs1/2` or `wrhs`; see (CF9). + And note that `fd_qtvs` is empty, because `S` eliminates all the quantified + type variables. + + (B) If not, then /discard `S` entirely/ and instead generate + FDEqns { fd_qtvs = qtvs + , fd_eqs = [ lhs ~ wlhs1, lhs2 ~ wlhs2, rhs ~ wrhs } + Now `instantiateFDEqns` will generate fresh unification variables for the + `qtvs` and the solver will in effect reconstruct `S`. + +(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, in (CF7) when generating the fundep equations for the solver to + deal with, we do /not/ apply the pre-unifying substitution `S` to the Wanted types. + 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 +1606,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/T27994b.hs ===================================== @@ -0,0 +1,17 @@ +{-# LANGUAGE TypeFamilies, TypeFamilyDependencies #-} + + +module T27994b where +import Data.Proxy + +type family G a where G Int = Char +type family F a b = r | r -> a +type instance F a [c] = (a, G a) -- instance 1 +type instance F Int Bool = (Int, Bool) -- instance 2 + +h :: Proxy a -> F a Bool +h = h +k :: (Int, b) -> b +k = k + +test = k (h Proxy) `seq` () -- [W] F alpha Bool ~ (Int, gamma) ===================================== 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, ['']) +test('T27994b', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/0dbb47a8d2c3e0ccb6c0d47014cc286... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/0dbb47a8d2c3e0ccb6c0d47014cc286... 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