Simon Peyton Jones pushed to branch wip/T27994 at Glasgow Haskell Compiler / GHC Commits: 565f8040 by Simon Peyton Jones at 2026-10-29T09:24:16+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`. - - - - - 7 changed files: - compiler/GHC/Core/Coercion/Axiom.hs - compiler/GHC/Core/Predicate.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/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 ) +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] @@ -739,11 +739,17 @@ 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 - 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) + -- 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 $ + if all (`elemSubst` subst) branch_qtvs -- See (OTF1) + then mkInjectivityFDEqn [] inj_flags + (substTys subst branch_lhs_tys) + work_args + else mkInjectivityFDEqn branch_qtvs (True: inj_flags) + (branch_rhs: branch_lhs_tys) + (work_rhs: work_args) | otherwise = Nothing @@ -756,9 +762,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 +774,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 +799,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 +892,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 +1120,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 +1135,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`) @@ -1127,42 +1143,65 @@ empty substitution, which does not fix `a`. So we get this FunDepEqns: 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 +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 ] } +becuase that `k`, hidden inside the kind of `a`, escapes into the solver. + +Previously we tried fancy footwork -- see Historical Note [trim_qtvs]. +But now we do the following, given + type family F a b = r | r -> b + type instance F lhs1 lhs2 = rhs + [W] F wlhs1 wlhs2 ~ wrhs + +* We can safely abandon the sustitution entirely and generate + FDEqns{ fd_qtvs = [a,b], fd_eqs = [ lhs2 ~ wlhs2, rhs ~ wrhs ] } + By generating (rhs ~ wrhs) we effectively make the solver re-generate the + substitution. This is also what we do for closed type families; see (CF7). + These 'fd_qtvs' are subsequently instantiated to fresh meta-variables by + 'instantiateFunDepEqns'. See Historical Note [trim_qtvs]. + +* As a fast-path optimisation, if the substitution (a /matching/ substition only, + remember) covers all the `qtvs` of the type instance, there's no hidden-kind problem. + Just apply the substitution and equate, with fd_qtvs = []: + FDEqns{ fd_qtvs = [], fd_eqs = [ S(lhs2) ~ wlhs2 } + +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 +1233,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 +1427,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 +1586,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/-/commit/565f804042073b1241adde95278e3839... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/565f804042073b1241adde95278e3839... 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