Simon Peyton Jones pushed to branch wip/T26331 at Glasgow Haskell Compiler / GHC Commits: 00478944 by Simon Peyton Jones at 2025-08-27T16:48:30+01:00 Comments only - - - - - a7884589 by Simon Peyton Jones at 2025-08-28T11:08:23+01:00 Type-family occurs check in unification The occurs check in `GHC.Core.Unify.uVarOrFam` was inadequate in dealing with type families. Better now. See Note [The occurs check in the Core unifier]. As I did this I realised that the whole apartness thing is trickier than I thought: see the new Note [Shortcomings of the apartness test] - - - - - 8adfc222 by sheaf at 2025-08-28T19:47:17-04:00 Fix orientation in HsWrapper composition (<.>) This commit fixes the order in which WpCast HsWrappers are composed, fixing a bug introduced in commit 56b32c5a2d5d7cad89a12f4d74dc940e086069d1. Fixes #26350 - - - - - 1ad0218f by Simon Peyton Jones at 2025-08-29T09:53:13+01:00 Fix deep subsumption again This commit fixed #26255: commit 56b32c5a2d5d7cad89a12f4d74dc940e086069d1 Author: sheaf Date: Mon Aug 11 15:50:47 2025 +0200 Improve deep subsumption This commit improves the DeepSubsumption sub-typing implementation in GHC.Tc.Utils.Unify.tc_sub_type_deep by being less eager to fall back to unification. But alas it still wasn't quite right for view patterns: #26331 This MR does a generalisation to fix it. A bit of a sledgehammer to crack a nut, but nice. * Add a field `ir_inst :: InferInstFlag` to `InferResult`, where ``` data InferInstFlag = IIF_Sigma | IIF_ShallowRho | IIF_DeepRho ``` * The flag says exactly how much `fillInferResult` should instantiate before filling the hole. * We can also use this to replace the previous very ad-hoc `tcInferSigma` that was used to implement GHCi's `:type` command. - - - - - 22 changed files: - compiler/GHC/Core/TyCo/Compare.hs - compiler/GHC/Core/Unify.hs - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Gen/Bind.hs - compiler/GHC/Tc/Gen/Expr.hs - compiler/GHC/Tc/Gen/Expr.hs-boot - compiler/GHC/Tc/Gen/Head.hs - compiler/GHC/Tc/Gen/HsType.hs - compiler/GHC/Tc/Gen/Match.hs - compiler/GHC/Tc/Gen/Pat.hs - compiler/GHC/Tc/Module.hs - compiler/GHC/Tc/Types/Evidence.hs - compiler/GHC/Tc/Utils/TcMType.hs - compiler/GHC/Tc/Utils/TcType.hs - compiler/GHC/Tc/Utils/Unify.hs - + testsuite/tests/patsyn/should_compile/T26331.hs - + testsuite/tests/patsyn/should_compile/T26331a.hs - testsuite/tests/patsyn/should_compile/all.T - + testsuite/tests/typecheck/should_compile/T26346.hs - + testsuite/tests/typecheck/should_compile/T26350.hs - + testsuite/tests/typecheck/should_compile/T26358.hs - testsuite/tests/typecheck/should_compile/all.T Changes: ===================================== compiler/GHC/Core/TyCo/Compare.hs ===================================== @@ -229,6 +229,8 @@ tcEqTyConApps tc1 args1 tc2 args2 = tc1 == tc2 && tcEqTyConAppArgs args1 args2 tcEqTyConAppArgs :: [Type] -> [Type] -> Bool +-- Args do not have to have equal length; +-- we discard the excess of the longer one tcEqTyConAppArgs args1 args2 = and (zipWith tcEqTypeNoKindCheck args1 args2) -- No kind check necessary: if both arguments are well typed, then ===================================== compiler/GHC/Core/Unify.hs ===================================== @@ -245,16 +245,21 @@ give up on), but for /substitutivity/. If we have (F x x), we can see that (F x can reduce to Double. So, it had better be the case that (F blah blah) can reduce to Double, no matter what (blah) is! -To achieve this, `go_fam` in `uVarOrFam` does this; +To achieve this, `go` in `uVarOrFam` does this; + +* We maintain /two/ substitutions, not just one: + * um_tv_env: the regular substitution, mapping TyVar :-> Type + * um_fam_env: maps (TyCon,[Type]) :-> Type, where the LHS is a type-fam application + In effect, these constitute one substitution mapping + CanEqLHS :-> Types * When we attempt to unify (G Float) ~ Int, we return MaybeApart.. - but we /also/ extend a "family substitution" [G Float :-> Int], - in `um_fam_env`, alongside the regular [tyvar :-> type] substitution in - `um_tv_env`. See the `BindMe` case of `go_fam` in `uVarOrFam`. + but we /also/ add a "family substitution" [G Float :-> Int], + to `um_fam_env`. See the `BindMe` case of `go` in `uVarOrFam`. * When we later encounter (G Float) ~ Bool, we apply the family substitution, very much as we apply the conventional [tyvar :-> type] substitution - when we encounter a type variable. See the `lookupFamEnv` in `go_fam` in + when we encounter a type variable. See the `lookupFamEnv` in `go` in `uVarOrFam`. So (G Float ~ Bool) becomes (Int ~ Bool) which is SurelyApart. Bingo. @@ -329,7 +334,7 @@ Wrinkles alternative path. So `noMatchableGivenDicts` must return False; so `mightMatchLater` must return False; so when um_bind_fam_fun returns `DontBindMe`, the unifier must return `SurelyApart`, not `MaybeApart`. See - `go_fam` in `uVarOrFam` + `go` in `uVarOrFam` (ATF6) When /matching/ can we ever have a type-family application on the LHS, in the template? You might think not, because type-class-instance and @@ -426,6 +431,9 @@ Wrinkles (ATF12) There is a horrid exception for the injectivity check. See (UR1) in in Note [Specification of unification]. +(ATF13) We have to be careful about the occurs check. + See Note [The occurs check in the Core unifier] + SIDE NOTE. The paper "Closed type families with overlapping equations" http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-ex... tries to achieve the same effect with a standard yes/no unifier, by "flattening" @@ -449,6 +457,49 @@ and all is lost. But with the current algorithm we have that a a ~ (Var A) (Var B) is SurelyApart, so the first equation definitely doesn't match and we can try the second, which does. END OF SIDE NOTE. + +Note [Shortcomings of the apartness test] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [Apartness and type families] is very clever. + +But it still has shortcomings (#26358). Consider unifying + [F a, F Int, Int] ~ [Bool, Char, a] +Working left to right you might think we would build the mapping + F a :-> Bool + F Int :-> Char +Now we discover that `a` unifies with `Int`. So really these two lists are Apart +because F Int can't be both Bool and Char. + +Just the same applies when adding a type-family binding to um_fam_env: + [F (G Float), F Int, G Float] ~ [Bool, Char, Iont] +Again these are Apart, because (G Float = Int), +and (F Int) can't be both Bool and Char + +But achieving this is very tricky! Perhaps whenever we unify a type variable, +or a type family, we should run it over the domain and (maybe range) of the +type-family mapping too? Sigh. + +For now we make no such attempt. +* The um_fam_env has only /un-substituted/ types. +* We look up only /un-substituted/ types in um_fam_env + +This may make us say MaybeApart when we could say SurelyApart, but it has no +effect on the correctness of unification: if we return Unifiable, it really is +Unifiable. + +This is all quite subtle. suppose we have: + um_tv_env: c :-> b + um_fam_env F b :-> a +and we are trying to add a :-> F c. We will call lookupFamEnv on (F, [c]), which will +fail because b and c are not equal. So we go ahead and add a :-> F c as a new tyvar eq, +getting: + um_tv_env: a :-> F c, c :-> b + um_fam_env F b :-> a + +Does that loop, like this: + a --> F c --> F b --> a? +No, because we do not substitute (F c) to (F b) and then look up in um_fam_env; +we look up only un-substituted types. -} {- ********************************************************************* @@ -1767,6 +1818,11 @@ uVarOrFam :: UMEnv -> CanEqLHS -> InType -> OutCoercion -> UM () -- Why saturated? See (ATF4) in Note [Apartness and type families] uVarOrFam env ty1 ty2 kco = do { substs <- getSubstEnvs +-- ; pprTrace "uVarOrFam" (vcat +-- [ text "ty1" <+> ppr ty1 +-- , text "ty2" <+> ppr ty2 +-- , text "tv_env" <+> ppr (um_tv_env substs) +-- , text "fam_env" <+> ppr (um_fam_env substs) ]) $ ; go NotSwapped substs ty1 ty2 kco } where -- `go` takes two bites at the cherry; if the first one fails @@ -1776,16 +1832,12 @@ uVarOrFam env ty1 ty2 kco -- E.g. a ~ F p q -- Starts with: go a (F p q) -- if `a` not bindable, swap to: go (F p q) a - go swapped substs (TyVarLHS tv1) ty2 kco - = go_tv swapped substs tv1 ty2 kco - - go swapped substs (TyFamLHS tc tys) ty2 kco - = go_fam swapped substs tc tys ty2 kco ----------------------------- - -- go_tv: LHS is a type variable + -- LHS is a type variable -- The sequence of tests is very similar to go_tv - go_tv swapped substs tv1 ty2 kco + go :: SwapFlag -> UMState -> CanEqLHS -> InType -> OutCoercion -> UM () + go swapped substs lhs@(TyVarLHS tv1) ty2 kco | Just ty1' <- lookupVarEnv (um_tv_env substs) tv1' = -- We already have a substitution for tv1 if | um_unif env -> unify_ty env ty1' ty2 kco @@ -1837,9 +1889,8 @@ uVarOrFam env ty1 ty2 kco where tv1' = umRnOccL env tv1 ty2_fvs = tyCoVarsOfType ty2 - rhs_fvs = ty2_fvs `unionVarSet` tyCoVarsOfCo kco rhs = ty2 `mkCastTy` mkSymCo kco - tv1_is_bindable | not (tv1' `elemVarSet` um_foralls env) + tv1_is_bindable | not (tv1' `elemVarSet` foralld_tvs) -- tv1' is not forall-bound, but tv1 can still differ -- from tv1; see Note [Cloning the template binders] -- in GHC.Core.Rules. So give tv1' to um_bind_tv_fun. @@ -1848,16 +1899,16 @@ uVarOrFam env ty1 ty2 kco | otherwise = False - occurs_check = um_unif env && - occursCheck (um_tv_env substs) tv1 rhs_fvs + foralld_tvs = um_foralls env + occurs_check = um_unif env && uOccursCheck substs foralld_tvs lhs rhs -- Occurs check, only when unifying -- see Note [Infinitary substitutions] - -- Make sure you include `kco` in rhs_tvs #14846 + -- Make sure you include `kco` in rhs #14846 ----------------------------- - -- go_fam: LHS is a saturated type-family application + -- LHS is a saturated type-family application -- Invariant: ty2 is not a TyVarTy - go_fam swapped substs tc1 tys1 ty2 kco + go swapped substs lhs@(TyFamLHS tc1 tys1) ty2 kco -- If we are under a forall, just give up and return MaybeApart -- see (ATF3) in Note [Apartness and type families] | not (isEmptyVarSet (um_foralls env)) @@ -1878,14 +1929,17 @@ uVarOrFam env ty1 ty2 kco -- Check for equality F tys1 ~ F tys2 | Just (tc2, tys2) <- isSatFamApp ty2 , tc1 == tc2 - = go_fam_fam tc1 tys1 tys2 kco + = go_fam_fam substs tc1 tys1 tys2 kco -- Now check if we can bind the (F tys) to the RHS -- This can happen even when matching: see (ATF7) | BindMe <- um_bind_fam_fun env tc1 tys1 rhs - = -- ToDo: do we need an occurs check here? - do { extendFamEnv tc1 tys1 rhs - ; maybeApart MARTypeFamily } + = if uOccursCheck substs emptyVarSet lhs rhs + then maybeApart MARInfinite + else do { extendFamEnv tc1 tys1 rhs + -- We don't substitute tys1 before extending + -- See Note [Shortcomings of the apartness test] + ; maybeApart MARTypeFamily } -- Swap in case of (F a b) ~ (G c d e) -- Maybe um_bind_fam_fun is False of (F a b) but true of (G c d e) @@ -1905,7 +1959,8 @@ uVarOrFam env ty1 ty2 kco ----------------------------- -- go_fam_fam: LHS and RHS are both saturated type-family applications, -- for the same type-family F - go_fam_fam tc tys1 tys2 kco + -- Precondition: um_foralls is empty + go_fam_fam substs tc tys1 tys2 kco -- Decompose (F tys1 ~ F tys2): (ATF9) -- Use injectivity information of F: (ATF10) -- But first bind the type-fam if poss: (ATF11) @@ -1925,13 +1980,13 @@ uVarOrFam env ty1 ty2 kco bind_fam_if_poss | not (um_unif env) -- Not when matching (ATF11-1) = return () - | tcEqTyConAppArgs tys1 tys2 -- Detect (F tys ~ F tys); - = return () -- otherwise we'd build an infinite substitution | BindMe <- um_bind_fam_fun env tc tys1 rhs1 - = extendFamEnv tc tys1 rhs1 - | um_unif env - , BindMe <- um_bind_fam_fun env tc tys2 rhs2 - = extendFamEnv tc tys2 rhs2 + = unless (uOccursCheck substs emptyVarSet (TyFamLHS tc tys1) rhs1) $ + extendFamEnv tc tys1 rhs1 + -- At this point um_unif=True, so we can unify either way + | BindMe <- um_bind_fam_fun env tc tys2 rhs2 + = unless (uOccursCheck substs emptyVarSet (TyFamLHS tc tys2) rhs2) $ + extendFamEnv tc tys2 rhs2 | otherwise = return () @@ -1939,17 +1994,92 @@ uVarOrFam env ty1 ty2 kco rhs2 = mkTyConApp tc tys1 `mkCastTy` kco -occursCheck :: TvSubstEnv -> TyVar -> TyCoVarSet -> Bool -occursCheck env tv1 tvs - = anyVarSet bad tvs +uOccursCheck :: UMState + -> TyVarSet -- Bound by enclosing foralls; see (OCU1) + -> CanEqLHS -> Type -- Can we unify (lhs := ty)? + -> Bool +-- See Note [The occurs check in the Core unifier] and (ATF13) +uOccursCheck (UMState { um_tv_env = tv_env, um_fam_env = fam_env }) bvs lhs ty + = go bvs ty where - bad tv | Just ty <- lookupVarEnv env tv - = anyVarSet bad (tyCoVarsOfType ty) - | otherwise - = tv == tv1 - -{- Note [Unifying coercion-foralls] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + go :: TyCoVarSet -- Bound by enclosing foralls; see (OCU1) + -> Type -> Bool + go bvs ty | Just ty' <- coreView ty = go bvs ty' + go bvs (TyVarTy tv) | Just ty' <- lookupVarEnv tv_env tv + = go bvs ty' + | TyVarLHS tv' <- lhs, tv==tv' + = True + | otherwise + = go bvs (tyVarKind tv) + go bvs (AppTy ty1 ty2) = go bvs ty1 || go bvs ty2 + go _ (LitTy {}) = False + go bvs (FunTy _ w arg res) = go bvs w || go bvs arg || go bvs res + go bvs (TyConApp tc tys) = go_tc bvs tc tys + + go bvs (ForAllTy (Bndr tv _) ty) + = go bvs (tyVarKind tv) || + (case lhs of + TyVarLHS tv' | tv==tv' -> False -- Shadowing + | otherwise -> go (bvs `extendVarSet` tv) ty + TyFamLHS {} -> False) -- Lookups don't happen under a forall + + go bvs (CastTy ty _co) = go bvs ty -- ToDo: should we worry about `co`? + go _ (CoercionTy _co) = False -- ToDo: should we worry about `co`? + + go_tc bvs tc tys + | isEmptyVarSet bvs -- Never look up in um_fam_env under a forall (ATF3) + , isTypeFamilyTyCon tc + , Just ty' <- lookupFamEnv fam_env tc (take arity tys) + -- NB: we look up /un-substituted/ types; + -- See Note [Shortcomings of the apartness test] + = go bvs ty' || any (go bvs) (drop arity tys) + + | TyFamLHS tc' tys' <- lhs + , tc == tc' + , tys `lengthAtLeast` arity -- Saturated, or over-saturated + , tcEqTyConAppArgs tys tys' + = True + + | otherwise + = any (go bvs) tys + where + arity = tyConArity tc + +{- Note [The occurs check in the Core unifier] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The unifier applies both substitutions (um_tv_env and um_fam_env) as it goes, +so we'll get an infinite loop if we have, for example + um_tv_env: a :-> F b -- (1) + um_fam_env F b :-> a -- (2) + +So (uOccursCheck substs lhs ty) returns True iff extending `substs` with `lhs :-> ty` +could lead to a loop. That is, could there by a type `s` such that + applySubsts( (substs + lhs:->ty), s ) is infinite + +It's vital that we do both at once: we might have (1) already and add (2); +or we might have (2) already and add (1). + +A very similar task is done by GHC.Tc.Utils.Unify.checkTyEqRhs. + +(OCU1) We keep track of the forall-bound variables because the um_fam_env is inactive + under a forall; indeed it is /unsound/ to consult it because we may have a binding + (F a :-> Int), and then unify (forall a. ...(F a)...) with something. We don't + want to map that (F a) to Int! + +(OCU2) Performance. Consider unifying + [a, b] ~ [big-ty, (a,a,a)] + We'll unify a:=big-ty. Then we'll attempt b:=(a,a,a), but must do an occurs check. + So we'll walk over big-ty, looking for `b`. And then again, and again, once for + each occurrence of `a`. A similar thing happens for + [a, (b,b,b)] ~ [big-ty, (a,a,a)] + albeit a bit less obviously. + + Potentially we could use a cache to record checks we have already done; + but I have not attempted that yet. Precisely similar remarks would apply + to GHC.Tc.Utils.Unify.checkTyEqRhs + +Note [Unifying coercion-foralls] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we try to unify (forall cv. t1) ~ (forall cv. t2). See Note [ForAllTy] in GHC.Core.TyCo.Rep. ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -16,7 +16,6 @@ module GHC.Tc.Gen.App ( tcApp - , tcInferSigma , tcExprPrag ) where import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcPolyExpr ) @@ -165,26 +164,6 @@ Note [Instantiation variables are short lived] -} -{- ********************************************************************* -* * - tcInferSigma -* * -********************************************************************* -} - -tcInferSigma :: Bool -> LHsExpr GhcRn -> TcM TcSigmaType --- Used only to implement :type; see GHC.Tc.Module.tcRnExpr --- True <=> instantiate -- return a rho-type --- False <=> don't instantiate -- return a sigma-type -tcInferSigma inst (L loc rn_expr) - = addExprCtxt rn_expr $ - setSrcSpanA loc $ - do { (fun@(rn_fun,fun_ctxt), rn_args) <- splitHsApps rn_expr - ; do_ql <- wantQuickLook rn_fun - ; (tc_fun, fun_sigma) <- tcInferAppHead fun - ; (inst_args, app_res_sigma) <- tcInstFun do_ql inst (tc_fun, fun_ctxt) fun_sigma rn_args - ; _ <- tcValArgs do_ql inst_args - ; return app_res_sigma } - {- ********************************************************************* * * Typechecking n-ary applications @@ -219,7 +198,7 @@ using the application chain route, and we can just recurse to tcExpr. A "head" has three special cases (for which we can infer a polytype using tcInferAppHead_maybe); otherwise is just any old expression (for -which we can infer a rho-type (via tcInfer). +which we can infer a rho-type (via runInferExpr). There is no special treatment for HsHole (HsVar ...), HsOverLit, etc, because we can't get a polytype from them. @@ -403,13 +382,22 @@ tcApp rn_expr exp_res_ty -- Step 2: Infer the type of `fun`, the head of the application ; (tc_fun, fun_sigma) <- tcInferAppHead fun ; let tc_head = (tc_fun, fun_ctxt) + -- inst_final: top-instantiate the result type of the application, + -- EXCEPT if we are trying to infer a sigma-type + inst_final = case exp_res_ty of + Check {} -> True + Infer (IR {ir_inst=iif}) -> + case iif of + IIF_ShallowRho -> True + IIF_DeepRho -> True + IIF_Sigma -> False -- Step 3: Instantiate the function type (taking a quick look at args) ; do_ql <- wantQuickLook rn_fun ; (inst_args, app_res_rho) <- setQLInstLevel do_ql $ -- See (TCAPP1) and (TCAPP2) in -- Note [tcApp: typechecking applications] - tcInstFun do_ql True tc_head fun_sigma rn_args + tcInstFun do_ql inst_final tc_head fun_sigma rn_args ; case do_ql of NoQL -> do { traceTc "tcApp:NoQL" (ppr rn_fun $$ ppr app_res_rho) @@ -420,6 +408,7 @@ tcApp rn_expr exp_res_ty app_res_rho exp_res_ty -- Step 4.2: typecheck the arguments ; tc_args <- tcValArgs NoQL inst_args + -- Step 4.3: wrap up ; finishApp tc_head tc_args app_res_rho res_wrap } @@ -427,15 +416,18 @@ tcApp rn_expr exp_res_ty -- Step 5.1: Take a quick look at the result type ; quickLookResultType app_res_rho exp_res_ty + -- Step 5.2: typecheck the arguments, and monomorphise -- any un-unified instantiation variables ; tc_args <- tcValArgs DoQL inst_args - -- Step 5.3: zonk to expose the polymophism hidden under + + -- Step 5.3: zonk to expose the polymorphism hidden under -- QuickLook instantiation variables in `app_res_rho` ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho + -- Step 5.4: subsumption check against the expected type ; res_wrap <- checkResultTy rn_expr tc_head inst_args - app_res_rho exp_res_ty + app_res_rho exp_res_ty -- Step 5.5: wrap up ; finishApp tc_head tc_args app_res_rho res_wrap } } @@ -470,32 +462,12 @@ checkResultTy :: HsExpr GhcRn -> (HsExpr GhcTc, AppCtxt) -- Head -> [HsExprArg p] -- Arguments, just error messages -> TcRhoType -- Inferred type of the application; zonked to - -- expose foralls, but maybe not deeply instantiated + -- expose foralls, but maybe not /deeply/ instantiated -> ExpRhoType -- Expected type; this is deeply skolemised -> TcM HsWrapper checkResultTy rn_expr _fun _inst_args app_res_rho (Infer inf_res) - = fillInferResultDS (exprCtOrigin rn_expr) app_res_rho inf_res - -- See Note [Deeply instantiate in checkResultTy when inferring] - -{- Note [Deeply instantiate in checkResultTy when inferring] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -To accept the following program (T26225b) with -XDeepSubsumption, we need to -deeply instantiate when inferring in checkResultTy: - - f :: Int -> (forall a. a->a) - g :: Int -> Bool -> Bool - - test b = - case b of - True -> f - False -> g - -If we don't deeply instantiate in the branches of the case expression, we will -try to unify the type of 'f' with that of 'g', which fails. If we instead -deeply instantiate 'f', we will fill the 'InferResult' with 'Int -> alpha -> alpha' -which then successfully unifies with the type of 'g' when we come to fill the -'InferResult' hole a second time for the second case branch. --} + = fillInferResult (exprCtOrigin rn_expr) app_res_rho inf_res + -- fillInferResult does deep instantiation if DeepSubsumption is on checkResultTy rn_expr (tc_fun, fun_ctxt) inst_args app_res_rho (Check res_ty) -- Unify with expected type from the context @@ -651,18 +623,16 @@ quickLookKeys = [dollarIdKey, leftSectionKey, rightSectionKey] ********************************************************************* -} tcInstFun :: QLFlag - -> Bool -- False <=> Instantiate only /inferred/ variables at the end + -> Bool -- False <=> Instantiate only /top-level, inferred/ variables; -- so may return a sigma-type - -- True <=> Instantiate all type variables at the end: - -- return a rho-type - -- The /only/ call site that passes in False is the one - -- in tcInferSigma, which is used only to implement :type - -- Otherwise we do eager instantiation; in Fig 5 of the paper + -- True <=> Instantiate /top-level, invisible/ type variables; + -- always return a rho-type (but not a deep-rho type) + -- Generally speaking we pass in True; in Fig 5 of the paper -- |-inst returns a rho-type -> (HsExpr GhcTc, AppCtxt) -> TcSigmaType -> [HsExprArg 'TcpRn] -> TcM ( [HsExprArg 'TcpInst] - , TcSigmaType ) + , TcSigmaType ) -- Does not instantiate trailing invisible foralls -- This crucial function implements the |-inst judgement in Fig 4, plus the -- modification in Fig 5, of the QL paper: -- "A quick look at impredicativity" (ICFP'20). @@ -704,13 +674,9 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args _ -> False inst_fun :: [HsExprArg 'TcpRn] -> ForAllTyFlag -> Bool - -- True <=> instantiate a tyvar with this ForAllTyFlag + -- True <=> instantiate a tyvar that has this ForAllTyFlag inst_fun [] | inst_final = isInvisibleForAllTyFlag | otherwise = const False - -- Using `const False` for `:type` avoids - -- `forall {r1} (a :: TYPE r1) {r2} (b :: TYPE r2). a -> b` - -- turning into `forall a {r2} (b :: TYPE r2). a -> b`. - -- See #21088. inst_fun (EValArg {} : _) = isInvisibleForAllTyFlag inst_fun _ = isInferredForAllTyFlag ===================================== compiler/GHC/Tc/Gen/Bind.hs ===================================== @@ -1305,8 +1305,8 @@ tcMonoBinds is_rec sig_fn no_gen do { mult <- newMultiplicityVar ; ((co_fn, matches'), rhs_ty') - <- tcInferFRR (FRRBinder name) $ \ exp_ty -> - -- tcInferFRR: the type of a let-binder must have + <- runInferRhoFRR (FRRBinder name) $ \ exp_ty -> + -- runInferRhoFRR: the type of a let-binder must have -- a fixed runtime rep. See #23176 tcExtendBinderStack [TcIdBndr_ExpType name exp_ty NotTopLevel] $ -- We extend the error context even for a non-recursive @@ -1333,8 +1333,8 @@ tcMonoBinds is_rec sig_fn no_gen = addErrCtxt (PatMonoBindsCtxt pat grhss) $ do { mult <- tcMultAnnOnPatBind mult_ann - ; (grhss', pat_ty) <- tcInferFRR FRRPatBind $ \ exp_ty -> - -- tcInferFRR: the type of each let-binder must have + ; (grhss', pat_ty) <- runInferRhoFRR FRRPatBind $ \ exp_ty -> + -- runInferRhoFRR: the type of each let-binder must have -- a fixed runtime rep. See #23176 tcGRHSsPat mult grhss exp_ty @@ -1522,7 +1522,7 @@ tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss, pat_mult = mult_a -- See Note [Typechecking pattern bindings] ; ((pat', nosig_mbis), pat_ty) <- addErrCtxt (PatMonoBindsCtxt pat grhss) $ - tcInferFRR FRRPatBind $ \ exp_ty -> + runInferSigmaFRR FRRPatBind $ \ exp_ty -> tcLetPat inst_sig_fun no_gen pat (Scaled mult exp_ty) $ -- The above inferred type get an unrestricted multiplicity. It may be -- worth it to try and find a finer-grained multiplicity here ===================================== compiler/GHC/Tc/Gen/Expr.hs ===================================== @@ -19,7 +19,7 @@ module GHC.Tc.Gen.Expr ( tcCheckPolyExpr, tcCheckPolyExprNC, tcCheckMonoExpr, tcCheckMonoExprNC, tcMonoExpr, tcMonoExprNC, - tcInferRho, tcInferRhoNC, + tcInferExpr, tcInferSigma, tcInferRho, tcInferRhoNC, tcPolyLExpr, tcPolyExpr, tcExpr, tcPolyLExprSig, tcSyntaxOp, tcSyntaxOpGen, SyntaxOpType(..), synKnownType, tcCheckId, @@ -233,17 +233,24 @@ tcPolyExprCheck expr res_ty * * ********************************************************************* -} +tcInferSigma :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcSigmaType) +tcInferSigma = tcInferExpr IIF_Sigma + tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType) -- Infer a *rho*-type. The return type is always instantiated. -tcInferRho (L loc expr) - = setSrcSpanA loc $ -- Set location /first/; see GHC.Tc.Utils.Monad +tcInferRho = tcInferExpr IIF_DeepRho +tcInferRhoNC = tcInferExprNC IIF_DeepRho + +tcInferExpr, tcInferExprNC :: InferInstFlag -> LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcType) +tcInferExpr iif (L loc expr) + = setSrcSpanA loc $ -- Set location /first/; see GHC.Tc.Utils.Monad addExprCtxt expr $ -- Note [Error contexts in generated code] - do { (expr', rho) <- tcInfer (tcExpr expr) + do { (expr', rho) <- runInfer iif IFRR_Any (tcExpr expr) ; return (L loc expr', rho) } -tcInferRhoNC (L loc expr) - = setSrcSpanA loc $ - do { (expr', rho) <- tcInfer (tcExpr expr) +tcInferExprNC iif (L loc expr) + = setSrcSpanA loc $ + do { (expr', rho) <- runInfer iif IFRR_Any (tcExpr expr) ; return (L loc expr', rho) } --------------- @@ -878,7 +885,7 @@ tcInferTupArgs boxity args ; return (Missing (Scaled mult arg_ty), arg_ty) } tc_infer_tup_arg i (Present x lexpr@(L l expr)) = do { (expr', arg_ty) <- case boxity of - Unboxed -> tcInferFRR (FRRUnboxedTuple i) (tcPolyExpr expr) + Unboxed -> runInferRhoFRR (FRRUnboxedTuple i) (tcPolyExpr expr) Boxed -> do { arg_ty <- newFlexiTyVarTy liftedTypeKind ; L _ expr' <- tcCheckPolyExpr lexpr arg_ty ; return (expr', arg_ty) } ===================================== compiler/GHC/Tc/Gen/Expr.hs-boot ===================================== @@ -1,8 +1,8 @@ module GHC.Tc.Gen.Expr where import GHC.Hs ( HsExpr, LHsExpr, SyntaxExprRn , SyntaxExprTc ) -import GHC.Tc.Utils.TcType ( TcRhoType, TcSigmaType, TcSigmaTypeFRR - , SyntaxOpType +import GHC.Tc.Utils.TcType ( TcType, TcRhoType, TcSigmaType, TcSigmaTypeFRR + , SyntaxOpType, InferInstFlag , ExpType, ExpRhoType, ExpSigmaType ) import GHC.Tc.Types ( TcM ) import GHC.Tc.Types.BasicTypes( TcCompleteSig ) @@ -33,6 +33,8 @@ tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc) tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType) +tcInferExpr :: InferInstFlag -> LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcType) + tcSyntaxOp :: CtOrigin -> SyntaxExprRn -> [SyntaxOpType] -- ^ shape of syntax operator arguments ===================================== compiler/GHC/Tc/Gen/Head.hs ===================================== @@ -556,7 +556,7 @@ tcInferAppHead (fun,ctxt) do { mb_tc_fun <- tcInferAppHead_maybe fun ; case mb_tc_fun of Just (fun', fun_sigma) -> return (fun', fun_sigma) - Nothing -> tcInfer (tcExpr fun) } + Nothing -> runInferRho (tcExpr fun) } tcInferAppHead_maybe :: HsExpr GhcRn -> TcM (Maybe (HsExpr GhcTc, TcSigmaType)) ===================================== compiler/GHC/Tc/Gen/HsType.hs ===================================== @@ -1063,9 +1063,9 @@ tc_infer_lhs_type mode (L span ty) -- | Infer the kind of a type and desugar. This is the "up" type-checker, -- as described in Note [Bidirectional type checking] tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind) - tc_infer_hs_type mode rn_ty - = tcInfer $ \exp_kind -> tcHsType mode rn_ty exp_kind + = runInferKind $ \exp_kind -> + tcHsType mode rn_ty exp_kind {- Note [Typechecking HsCoreTys] @@ -1985,7 +1985,7 @@ checkExpKind rn_ty ty ki (Check ki') = checkExpKind _rn_ty ty ki (Infer cell) = do -- NB: do not instantiate. -- See Note [Do not always instantiate eagerly in types] - co <- fillInferResult ki cell + co <- fillInferResultNoInst ki cell pure (ty `mkCastTy` co) --------------------------- ===================================== compiler/GHC/Tc/Gen/Match.hs ===================================== @@ -1034,7 +1034,7 @@ tcDoStmt ctxt (RecStmt { recS_stmts = L l stmts, recS_later_ids = later_names ; tcExtendIdEnv tup_ids $ do { ((stmts', (ret_op', tup_rets)), stmts_ty) - <- tcInfer $ \ exp_ty -> + <- runInferRho $ \ exp_ty -> tcStmtsAndThen ctxt tcDoStmt stmts exp_ty $ \ inner_res_ty -> do { tup_rets <- zipWithM tcCheckId tup_names (map mkCheckExpType tup_elt_tys) @@ -1046,7 +1046,7 @@ tcDoStmt ctxt (RecStmt { recS_stmts = L l stmts, recS_later_ids = later_names ; return (ret_op', tup_rets) } ; ((_, mfix_op'), mfix_res_ty) - <- tcInfer $ \ exp_ty -> + <- runInferRho $ \ exp_ty -> tcSyntaxOp DoOrigin mfix_op [synKnownType (mkVisFunTyMany tup_ty stmts_ty)] exp_ty $ \ _ _ -> return () @@ -1172,7 +1172,7 @@ tcApplicativeStmts tcApplicativeStmts ctxt pairs rhs_ty thing_inside = do { body_ty <- newFlexiTyVarTy liftedTypeKind ; let arity = length pairs - ; ts <- replicateM (arity-1) $ newInferExpType + ; ts <- replicateM (arity-1) $ newInferExpType IIF_DeepRho ; exp_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind ; pat_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind ; let fun_ty = mkVisFunTysMany pat_tys body_ty ===================================== compiler/GHC/Tc/Gen/Pat.hs ===================================== @@ -26,7 +26,7 @@ where import GHC.Prelude -import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferRho ) +import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferExpr ) import GHC.Hs import GHC.Hs.Syn.Type @@ -220,7 +220,7 @@ tcInferPat :: FixedRuntimeRepContext -> TcM a -> TcM ((LPat GhcTc, a), TcSigmaTypeFRR) tcInferPat frr_orig ctxt pat thing_inside - = tcInferFRR frr_orig $ \ exp_ty -> + = runInferSigmaFRR frr_orig $ \ exp_ty -> tc_lpat (unrestricted exp_ty) penv pat thing_inside where penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin } @@ -694,15 +694,17 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of -- restriction need to be put in place, if any, for linear view -- patterns to desugar to type-correct Core. - ; (expr',expr_ty) <- tcInferRho expr - -- Note [View patterns and polymorphism] + ; (expr', expr_rho) <- tcInferExpr IIF_ShallowRho expr + -- IIF_ShallowRho: do not perform deep instantiation, regardless of + -- DeepSubsumption (Note [View patterns and polymorphism]) + -- But we must do top-instantiation to expose the arrow to matchActualFunTy -- Expression must be a function ; let herald = ExpectedFunTyViewPat $ unLoc expr ; (expr_wrap1, Scaled _mult inf_arg_ty, inf_res_sigma) - <- matchActualFunTy herald (Just . HsExprRnThing $ unLoc expr) (1,expr_ty) expr_ty + <- matchActualFunTy herald (Just . HsExprRnThing $ unLoc expr) (1,expr_rho) expr_rho -- See Note [View patterns and polymorphism] - -- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_sigma) + -- expr_wrap1 :: expr_rho "->" (inf_arg_ty -> inf_res_sigma) -- Check that overall pattern is more polymorphic than arg type ; expr_wrap2 <- tc_sub_type penv (scaledThing pat_ty) inf_arg_ty @@ -715,18 +717,18 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of ; pat_ty <- readExpType h_pat_ty ; let expr_wrap2' = mkWpFun expr_wrap2 idHsWrapper (Scaled w pat_ty) inf_res_sigma - -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->" - -- (pat_ty -> inf_res_sigma) - -- NB: pat_ty comes from matchActualFunTy, so it has a - -- fixed RuntimeRep, as needed to call mkWpFun. - ; let + -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->" + -- (pat_ty -> inf_res_sigma) + -- NB: pat_ty comes from matchActualFunTy, so it has a + -- fixed RuntimeRep, as needed to call mkWpFun. + expr_wrap = expr_wrap2' <.> expr_wrap1 ; return $ (ViewPat pat_ty (mkLHsWrap expr_wrap expr') pat', res) } {- Note [View patterns and polymorphism] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider this exotic example: +Consider this exotic example (test T26331a): pair :: forall a. Bool -> a -> forall b. b -> (a,b) f :: Int -> blah @@ -735,11 +737,15 @@ Consider this exotic example: The expression (pair True) should have type pair True :: Int -> forall b. b -> (Int,b) so that it is ready to consume the incoming Int. It should be an -arrow type (t1 -> t2); hence using (tcInferRho expr). +arrow type (t1 -> t2); and we must not instantiate that `forall b`, +/even with DeepSubsumption/. Hence using `IIF_ShallowRho`; this is the only +place where `IIF_ShallowRho` is used. Then, when taking that arrow apart we want to get a *sigma* type (forall b. b->(Int,b)), because that's what we want to bind 'x' to. Fortunately that's what matchActualFunTy returns anyway. + +Another example is #26331. -} -- Type signatures in patterns @@ -768,8 +774,7 @@ Fortunately that's what matchActualFunTy returns anyway. penv pats thing_inside ; pat_ty <- readExpType (scaledThing pat_ty) ; return (mkHsWrapPat coi - (ListPat elt_ty pats') pat_ty, res) -} + (ListPat elt_ty pats') pat_ty, res) } TuplePat _ pats boxity -> do { let arity = length pats ===================================== compiler/GHC/Tc/Module.hs ===================================== @@ -62,7 +62,6 @@ import GHC.Tc.Gen.Match import GHC.Tc.Utils.Unify( checkConstraints, tcSubTypeSigma ) import GHC.Tc.Zonk.Type import GHC.Tc.Gen.Expr -import GHC.Tc.Gen.App( tcInferSigma ) import GHC.Tc.Utils.Monad import GHC.Tc.Gen.Export import GHC.Tc.Types.Evidence @@ -2628,10 +2627,11 @@ tcRnExpr hsc_env mode rdr_expr failIfErrsM ; -- Typecheck the expression - ((tclvl, res_ty), lie) + ((tclvl, (_tc_expr, res_ty)), lie) <- captureTopConstraints $ pushTcLevelM $ - tcInferSigma inst rn_expr ; + (if inst then tcInferRho rn_expr + else tcInferSigma rn_expr); -- Generalise uniq <- newUnique ; ===================================== compiler/GHC/Tc/Types/Evidence.hs ===================================== @@ -206,9 +206,15 @@ instance Monoid HsWrapper where (<.>) :: HsWrapper -> HsWrapper -> HsWrapper WpHole <.> c = c c <.> WpHole = c -WpCast c1 <.> WpCast c2 = WpCast (c1 `mkTransCo` c2) +WpCast c1 <.> WpCast c2 = WpCast (c2 `mkTransCo` c1) -- If we can represent the HsWrapper as a cast, try to do so: this may avoid -- unnecessary eta-expansion (see 'mkWpFun'). + -- + -- NB: <.> behaves like function composition: + -- + -- WpCast c1 <.> WpCast c2 :: coercionLKind c2 ~> coercionRKind c1 + -- + -- This is thus the same as WpCast (c2 ; c1) and not WpCast (c1 ; c2). c1 <.> c2 = c1 `WpCompose` c2 -- | Smart constructor to create a 'WpFun' 'HsWrapper', which avoids introducing ===================================== compiler/GHC/Tc/Utils/TcMType.hs ===================================== @@ -65,7 +65,7 @@ module GHC.Tc.Utils.TcMType ( -- Expected types ExpType(..), ExpSigmaType, ExpRhoType, mkCheckExpType, newInferExpType, newInferExpTypeFRR, - tcInfer, tcInferFRR, + runInfer, runInferRho, runInferSigma, runInferKind, runInferRhoFRR, runInferSigmaFRR, readExpType, readExpType_maybe, readScaledExpType, expTypeToType, scaledExpTypeToType, checkingExpType_maybe, checkingExpType, @@ -438,30 +438,29 @@ See test case T21325. -- actual data definition is in GHC.Tc.Utils.TcType -newInferExpType :: TcM ExpType -newInferExpType = new_inferExpType Nothing +newInferExpType :: InferInstFlag -> TcM ExpType +newInferExpType iif = new_inferExpType iif IFRR_Any -newInferExpTypeFRR :: FixedRuntimeRepContext -> TcM ExpTypeFRR -newInferExpTypeFRR frr_orig +newInferExpTypeFRR :: InferInstFlag -> FixedRuntimeRepContext -> TcM ExpTypeFRR +newInferExpTypeFRR iif frr_orig = do { th_lvl <- getThLevel - ; if - -- See [Wrinkle: Typed Template Haskell] - -- in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete. - | TypedBrack _ <- th_lvl - -> new_inferExpType Nothing + ; let mb_frr = case th_lvl of + TypedBrack {} -> IFRR_Any + _ -> IFRR_Check frr_orig + -- mb_frr: see [Wrinkle: Typed Template Haskell] + -- in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete. - | otherwise - -> new_inferExpType (Just frr_orig) } + ; new_inferExpType iif mb_frr } -new_inferExpType :: Maybe FixedRuntimeRepContext -> TcM ExpType -new_inferExpType mb_frr_orig +new_inferExpType :: InferInstFlag -> InferFRRFlag -> TcM ExpType +new_inferExpType iif ifrr = do { u <- newUnique ; tclvl <- getTcLevel ; traceTc "newInferExpType" (ppr u <+> ppr tclvl) ; ref <- newMutVar Nothing ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl - , ir_ref = ref - , ir_frr = mb_frr_orig })) } + , ir_inst = iif, ir_frr = ifrr + , ir_ref = ref })) } -- | Extract a type out of an ExpType, if one exists. But one should always -- exist. Unless you're quite sure you know what you're doing. @@ -515,12 +514,12 @@ inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl where -- See Note [TcLevel of ExpType] new_meta = case mb_frr of - Nothing -> do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy + IFRR_Any -> do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy ; newMetaTyVarTyAtLevel tc_lvl (mkTYPEapp rr) } - Just frr -> mdo { rr <- newConcreteTyVarTyAtLevel conc_orig tc_lvl runtimeRepTy - ; tau <- newMetaTyVarTyAtLevel tc_lvl (mkTYPEapp rr) - ; let conc_orig = ConcreteFRR $ FixedRuntimeRepOrigin tau frr - ; return tau } + IFRR_Check frr -> mdo { rr <- newConcreteTyVarTyAtLevel conc_orig tc_lvl runtimeRepTy + ; tau <- newMetaTyVarTyAtLevel tc_lvl (mkTYPEapp rr) + ; let conc_orig = ConcreteFRR $ FixedRuntimeRepOrigin tau frr + ; return tau } {- Note [inferResultToType] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -537,20 +536,31 @@ Note [fillInferResult] in GHC.Tc.Utils.Unify. -- | Infer a type using a fresh ExpType -- See also Note [ExpType] in "GHC.Tc.Utils.TcMType" -- --- Use 'tcInferFRR' if you require the type to have a fixed +-- Use 'runInferFRR' if you require the type to have a fixed -- runtime representation. -tcInfer :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) -tcInfer = tc_infer Nothing +runInferSigma :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) +runInferSigma = runInfer IIF_Sigma IFRR_Any --- | Like 'tcInfer', except it ensures that the resulting type +runInferRho :: (ExpRhoType -> TcM a) -> TcM (a, TcRhoType) +runInferRho = runInfer IIF_DeepRho IFRR_Any + +runInferKind :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) +-- Used for kind-checking types, where we never want deep instantiation, +-- nor FRR checks +runInferKind = runInfer IIF_Sigma IFRR_Any + +-- | Like 'runInferRho', except it ensures that the resulting type -- has a syntactically fixed RuntimeRep as per Note [Fixed RuntimeRep] in -- GHC.Tc.Utils.Concrete. -tcInferFRR :: FixedRuntimeRepContext -> (ExpSigmaTypeFRR -> TcM a) -> TcM (a, TcSigmaTypeFRR) -tcInferFRR frr_orig = tc_infer (Just frr_orig) +runInferRhoFRR :: FixedRuntimeRepContext -> (ExpRhoTypeFRR -> TcM a) -> TcM (a, TcRhoTypeFRR) +runInferRhoFRR frr_orig = runInfer IIF_DeepRho (IFRR_Check frr_orig) + +runInferSigmaFRR :: FixedRuntimeRepContext -> (ExpSigmaTypeFRR -> TcM a) -> TcM (a, TcSigmaTypeFRR) +runInferSigmaFRR frr_orig = runInfer IIF_Sigma (IFRR_Check frr_orig) -tc_infer :: Maybe FixedRuntimeRepContext -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) -tc_infer mb_frr tc_check - = do { res_ty <- new_inferExpType mb_frr +runInfer :: InferInstFlag -> InferFRRFlag -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) +runInfer iif mb_frr tc_check + = do { res_ty <- new_inferExpType iif mb_frr ; result <- tc_check res_ty ; res_ty <- readExpType res_ty ; return (result, res_ty) } ===================================== compiler/GHC/Tc/Utils/TcType.hs ===================================== @@ -24,14 +24,14 @@ module GHC.Tc.Utils.TcType ( -------------------------------- -- Types TcType, TcSigmaType, TcTypeFRR, TcSigmaTypeFRR, - TcRhoType, TcTauType, TcPredType, TcThetaType, + TcRhoType, TcRhoTypeFRR, TcTauType, TcPredType, TcThetaType, TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet, TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcInvisTVBinder, TcReqTVBinder, TcTyCon, MonoTcTyCon, PolyTcTyCon, TcTyConBinder, KnotTied, - ExpType(..), ExpKind, InferResult(..), + ExpType(..), ExpKind, InferResult(..), InferInstFlag(..), InferFRRFlag(..), ExpTypeFRR, ExpSigmaType, ExpSigmaTypeFRR, - ExpRhoType, + ExpRhoType, ExpRhoTypeFRR, mkCheckExpType, checkingExpType_maybe, checkingExpType, @@ -380,6 +380,7 @@ type TcSigmaType = TcType -- See Note [Return arguments with a fixed RuntimeRep. type TcSigmaTypeFRR = TcSigmaType -- TODO: consider making this a newtype. +type TcRhoTypeFRR = TcRhoType type TcRhoType = TcType -- Note [TcRhoType] type TcTauType = TcType @@ -408,9 +409,13 @@ data InferResult , ir_lvl :: TcLevel -- ^ See Note [TcLevel of ExpType] in GHC.Tc.Utils.TcMType - , ir_frr :: Maybe FixedRuntimeRepContext + , ir_frr :: InferFRRFlag -- ^ See Note [FixedRuntimeRep context in ExpType] in GHC.Tc.Utils.TcMType + , ir_inst :: InferInstFlag + -- ^ True <=> when DeepSubsumption is on, deeply instantiate before filling, + -- See Note [Instantiation of InferResult] in GHC.Tc.Utils.Unify + , ir_ref :: IORef (Maybe TcType) } -- ^ The type that fills in this hole should be a @Type@, -- that is, its kind should be @TYPE rr@ for some @rr :: RuntimeRep@. @@ -419,26 +424,48 @@ data InferResult -- @rr@ must be concrete, in the sense of Note [Concrete types] -- in GHC.Tc.Utils.Concrete. -type ExpSigmaType = ExpType +data InferFRRFlag + = IFRR_Check -- Check that the result type has a fixed runtime rep + FixedRuntimeRepContext -- Typically used for function arguments and lambdas + + | IFRR_Any -- No need to check for fixed runtime-rep + +data InferInstFlag -- Specifies whether the inference should return an uninstantiated + -- SigmaType, or a (possibly deeply) instantiated RhoType + -- See Note [Instantiation of InferResult] in GHC.Tc.Utils.Unify + + = IIF_Sigma -- Trying to infer a SigmaType + -- Don't instantiate at all, regardless of DeepSubsumption + -- Typically used when inferring the type of a pattern + + | IIF_ShallowRho -- Trying to infer a shallow RhoType (no foralls or => at the top) + -- Top-instantiate (only, regardless of DeepSubsumption) before filling the hole + -- Typically used when inferring the type of an expression + + | IIF_DeepRho -- Trying to infer a possibly-deep RhoType (depending on DeepSubsumption) + -- If DeepSubsumption is off, same as IIF_ShallowRho + -- If DeepSubsumption is on, instantiate deeply before filling the hole + +type ExpSigmaType = ExpType +type ExpRhoType = ExpType + -- Invariant: in ExpRhoType, if -XDeepSubsumption is on, + -- and we are in checking mode (i.e. the ExpRhoType is (Check rho)), + -- then the `rho` is deeply skolemised -- | An 'ExpType' which has a fixed RuntimeRep. -- -- For a 'Check' 'ExpType', the stored 'TcType' must have -- a fixed RuntimeRep. For an 'Infer' 'ExpType', the 'ir_frr' --- field must be of the form @Just frr_orig@. -type ExpTypeFRR = ExpType +-- field must be of the form @IFRR_Check frr_orig@. +type ExpTypeFRR = ExpType -- | Like 'TcSigmaTypeFRR', but for an expected type. -- -- See 'ExpTypeFRR'. type ExpSigmaTypeFRR = ExpTypeFRR +type ExpRhoTypeFRR = ExpTypeFRR -- TODO: consider making this a newtype. -type ExpRhoType = ExpType - -- Invariant: if -XDeepSubsumption is on, - -- and we are checking (i.e. the ExpRhoType is (Check rho)), - -- then the `rho` is deeply skolemised - -- | Like 'ExpType', but on kind level type ExpKind = ExpType @@ -447,12 +474,17 @@ instance Outputable ExpType where ppr (Infer ir) = ppr ir instance Outputable InferResult where - ppr (IR { ir_uniq = u, ir_lvl = lvl, ir_frr = mb_frr }) - = text "Infer" <> mb_frr_text <> braces (ppr u <> comma <> ppr lvl) + ppr (IR { ir_uniq = u, ir_lvl = lvl, ir_frr = mb_frr, ir_inst = inst }) + = text "Infer" <> parens (pp_inst <> pp_frr) + <> braces (ppr u <> comma <> ppr lvl) where - mb_frr_text = case mb_frr of - Just _ -> text "FRR" - Nothing -> empty + pp_inst = case inst of + IIF_Sigma -> text "Sigma" + IIF_ShallowRho -> text "ShallowRho" + IIF_DeepRho -> text "DeepRho" + pp_frr = case mb_frr of + IFRR_Check {} -> text ",FRR" + IFRR_Any -> empty -- | Make an 'ExpType' suitable for checking. mkCheckExpType :: TcType -> ExpType ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -27,7 +27,7 @@ module GHC.Tc.Utils.Unify ( -- Skolemisation DeepSubsumptionFlag(..), getDeepSubsumptionFlag, isRhoTyDS, tcSkolemise, tcSkolemiseCompleteSig, tcSkolemiseExpectedType, - deeplyInstantiate, + dsInstantiate, -- Various unifications unifyType, unifyKind, unifyInvisibleType, @@ -40,7 +40,6 @@ module GHC.Tc.Utils.Unify ( -------------------------------- -- Holes - tcInfer, matchExpectedListTy, matchExpectedTyConApp, matchExpectedAppTy, @@ -60,7 +59,7 @@ module GHC.Tc.Utils.Unify ( simpleUnifyCheck, UnifyCheckCaller(..), SimpleUnifyResult(..), - fillInferResult, fillInferResultDS + fillInferResult, fillInferResultNoInst ) where import GHC.Prelude @@ -801,13 +800,13 @@ matchExpectedFunTys :: forall a. -- If exp_ty is Infer {}, then [ExpPatType] and ExpRhoType results are all Infer{} matchExpectedFunTys herald _ctxt arity (Infer inf_res) thing_inside = do { arg_tys <- mapM (new_infer_arg_ty herald) [1 .. arity] - ; res_ty <- newInferExpType + ; res_ty <- newInferExpType (ir_inst inf_res) ; result <- thing_inside (map ExpFunPatTy arg_tys) res_ty ; arg_tys <- mapM (\(Scaled m t) -> Scaled m <$> readExpType t) arg_tys ; res_ty <- readExpType res_ty -- NB: mkScaledFunTys arg_tys res_ty does not contain any foralls -- (even nested ones), so no need to instantiate. - ; co <- fillInferResult (mkScaledFunTys arg_tys res_ty) inf_res + ; co <- fillInferResultNoInst (mkScaledFunTys arg_tys res_ty) inf_res ; return (mkWpCastN co, result) } matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside @@ -914,10 +913,10 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside ; co <- unifyType Nothing (mkScaledFunTys more_arg_tys res_ty) fun_ty ; return (mkWpCastN co, result) } -new_infer_arg_ty :: ExpectedFunTyOrigin -> Int -> TcM (Scaled ExpSigmaTypeFRR) +new_infer_arg_ty :: ExpectedFunTyOrigin -> Int -> TcM (Scaled ExpRhoTypeFRR) new_infer_arg_ty herald arg_pos -- position for error messages only = do { mult <- newFlexiTyVarTy multiplicityTy - ; inf_hole <- newInferExpTypeFRR (FRRExpectedFunTy herald arg_pos) + ; inf_hole <- newInferExpTypeFRR IIF_DeepRho (FRRExpectedFunTy herald arg_pos) ; return (mkScaled mult inf_hole) } new_check_arg_ty :: ExpectedFunTyOrigin -> Int -> TcM (Scaled TcType) @@ -1075,18 +1074,6 @@ matchExpectedAppTy orig_ty * ********************************************************************** -} -{- Note [inferResultToType] -~~~~~~~~~~~~~~~~~~~~~~~~~~~ -expTypeToType and inferResultType convert an InferResult to a monotype. -It must be a monotype because if the InferResult isn't already filled in, -we fill it in with a unification variable (hence monotype). So to preserve -order-independence we check for mono-type-ness even if it *is* filled in -already. - -See also Note [TcLevel of ExpType] in GHC.Tc.Utils.TcType, and -Note [fillInferResult]. --} - -- | Fill an 'InferResult' with the given type. -- -- If @co = fillInferResult t1 infer_res@, then @co :: t1 ~# t2@, @@ -1098,14 +1085,14 @@ Note [fillInferResult]. -- The stored type @t2@ is at the same level as given by the -- 'ir_lvl' field. -- - FRR invariant. --- Whenever the 'ir_frr' field is not @Nothing@, @t2@ is guaranteed +-- Whenever the 'ir_frr' field is `IFRR_Check`, @t2@ is guaranteed -- to have a syntactically fixed RuntimeRep, in the sense of -- Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. -fillInferResult :: TcType -> InferResult -> TcM TcCoercionN -fillInferResult act_res_ty (IR { ir_uniq = u - , ir_lvl = res_lvl - , ir_frr = mb_frr - , ir_ref = ref }) +fillInferResultNoInst :: TcType -> InferResult -> TcM TcCoercionN +fillInferResultNoInst act_res_ty (IR { ir_uniq = u + , ir_lvl = res_lvl + , ir_frr = mb_frr + , ir_ref = ref }) = do { mb_exp_res_ty <- readTcRef ref ; case mb_exp_res_ty of Just exp_res_ty @@ -1126,7 +1113,7 @@ fillInferResult act_res_ty (IR { ir_uniq = u ppr u <> colon <+> ppr act_res_ty <+> char '~' <+> ppr exp_res_ty ; cur_lvl <- getTcLevel ; unless (cur_lvl `sameDepthAs` res_lvl) $ - ensureMonoType act_res_ty + ensureMonoType act_res_ty -- See (FIR1) ; unifyType Nothing act_res_ty exp_res_ty } Nothing -> do { traceTc "Filling inferred ExpType" $ @@ -1140,16 +1127,28 @@ fillInferResult act_res_ty (IR { ir_uniq = u -- fixed RuntimeRep (if necessary, i.e. 'mb_frr' is not 'Nothing'). ; (frr_co, act_res_ty) <- case mb_frr of - Nothing -> return (mkNomReflCo act_res_ty, act_res_ty) - Just frr_orig -> hasFixedRuntimeRep frr_orig act_res_ty + IFRR_Any -> return (mkNomReflCo act_res_ty, act_res_ty) + IFRR_Check frr_orig -> hasFixedRuntimeRep frr_orig act_res_ty -- Compose the two coercions. ; let final_co = prom_co `mkTransCo` frr_co ; writeTcRef ref (Just act_res_ty) - ; return final_co } - } + ; return final_co } } + +fillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper +-- See Note [Instantiation of InferResult] +fillInferResult ct_orig res_ty ires@(IR { ir_inst = iif }) + = case iif of + IIF_Sigma -> do { co <- fillInferResultNoInst res_ty ires + ; return (mkWpCastN co) } + IIF_ShallowRho -> do { (wrap, res_ty') <- topInstantiate ct_orig res_ty + ; co <- fillInferResultNoInst res_ty' ires + ; return (mkWpCastN co <.> wrap) } + IIF_DeepRho -> do { (wrap, res_ty') <- dsInstantiate ct_orig res_ty + ; co <- fillInferResultNoInst res_ty' ires + ; return (mkWpCastN co <.> wrap) } {- Note [fillInferResult] ~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1210,39 +1209,96 @@ For (2), we simply look to see if the hole is filled already. - if it is filled, we simply unify with the type that is already there -There is one wrinkle. Suppose we have - case e of - T1 -> e1 :: (forall a. a->a) -> Int - G2 -> e2 -where T1 is not GADT or existential, but G2 is a GADT. Then suppose the -T1 alternative fills the hole with (forall a. a->a) -> Int, which is fine. -But now the G2 alternative must not *just* unify with that else we'd risk -allowing through (e2 :: (forall a. a->a) -> Int). If we'd checked G2 first -we'd have filled the hole with a unification variable, which enforces a -monotype. - -So if we check G2 second, we still want to emit a constraint that restricts -the RHS to be a monotype. This is done by ensureMonoType, and it works -by simply generating a constraint (alpha ~ ty), where alpha is a fresh +(FIR1) There is one wrinkle. Suppose we have + case e of + T1 -> e1 :: (forall a. a->a) -> Int + G2 -> e2 + where T1 is not GADT or existential, but G2 is a GADT. Then suppose the + T1 alternative fills the hole with (forall a. a->a) -> Int, which is fine. + But now the G2 alternative must not *just* unify with that else we'd risk + allowing through (e2 :: (forall a. a->a) -> Int). If we'd checked G2 first + we'd have filled the hole with a unification variable, which enforces a + monotype. + + So if we check G2 second, we still want to emit a constraint that restricts + the RHS to be a monotype. This is done by ensureMonoType, and it works + by simply generating a constraint (alpha ~ ty), where alpha is a fresh unification variable. We discard the evidence. --} +Note [Instantiation of InferResult] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When typechecking expressions (not types, not patterns), we always almost +always instantiate before filling in `InferResult`, so that the result is a +TcRhoType. This behaviour is controlled by the `ir_inst :: InferInstFlag` +field of `InferResult`. --- | A version of 'fillInferResult' that also performs deep instantiation --- when deep subsumption is enabled. --- --- See also Note [Instantiation of InferResult]. -fillInferResultDS :: CtOrigin -> TcRhoType -> InferResult -> TcM HsWrapper -fillInferResultDS ct_orig rho inf_res - = do { massertPpr (isRhoTy rho) $ - vcat [ text "fillInferResultDS: input type is not a rho-type" - , text "ty:" <+> ppr rho ] - ; ds_flag <- getDeepSubsumptionFlag - ; case ds_flag of - Shallow -> mkWpCastN <$> fillInferResult rho inf_res - Deep -> do { (inst_wrap, rho') <- deeplyInstantiate ct_orig rho - ; co <- fillInferResult rho' inf_res - ; return (mkWpCastN co <.> inst_wrap) } } +If we do instantiate (ir_inst = IIF_DeepRho), and DeepSubsumption is enabled, +we instantiate deeply. See `tcInferResult`. + +Usually this field is `IIF_DeepRho` meaning "return a (possibly deep) rho-type". +Why is this the common case? See #17173 for discussion. Here are some examples +of why: + +1. Consider + f x = (*) + We want to instantiate the type of (*) before returning, else we + will infer the type + f :: forall {a}. a -> forall b. Num b => b -> b -> b + This is surely confusing for users. + + And worse, the monomorphism restriction won't work properly. The MR is + dealt with in simplifyInfer, and simplifyInfer has no way of + instantiating. This could perhaps be worked around, but it may be + hard to know even when instantiation should happen. + +2. Another reason. Consider + f :: (?x :: Int) => a -> a + g y = let ?x = 3::Int in f + Here want to instantiate f's type so that the ?x::Int constraint + gets discharged by the enclosing implicit-parameter binding. + +3. Suppose one defines plus = (+). If we instantiate lazily, we will + infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism + restriction compels us to infer + plus :: Integer -> Integer -> Integer + (or similar monotype). Indeed, the only way to know whether to apply + the monomorphism restriction at all is to instantiate + +HOWEVER, not always! Here are places where we want `IIF_Sigma` meaning +"return a sigma-type": + +* IIF_Sigma: In GHC.Tc.Module.tcRnExpr, which implements GHCi's :type + command, we want to return a completely uninstantiated type. + See Note [Implementing :type] in GHC.Tc.Module. + +* IIF_Sigma: In types we can't lambda-abstract, so we must be careful not to instantiate + at all. See calls to `runInferHsType` + +* IIF_Sigma: in patterns we don't want to instantiate at all. See the use of + `runInferSigmaFRR` in GHC.Tc.Gen.Pat + +* IIF_ShallowRho: in the expression part of a view pattern, we must top-instantiate + but /not/ deeply instantiate (#26331). See Note [View patterns and polymorphism] + in GHC.Tc.Gen.Pat. This the only place we use IIF_ShallowRho. + +Why do we want to deeply instantiate, ever? Why isn't top-instantiation enough? +Answer: to accept the following program (T26225b) with -XDeepSubsumption, we +need to deeply instantiate when inferring in checkResultTy: + + f :: Int -> (forall a. a->a) + g :: Int -> Bool -> Bool + + test b = + case b of + True -> f + False -> g + +If we don't deeply instantiate in the branches of the case expression, we will +try to unify the type of 'f' with that of 'g', which fails. If we instead +deeply instantiate 'f', we will fill the 'InferResult' with 'Int -> alpha -> alpha' +which then successfully unifies with the type of 'g' when we come to fill the +'InferResult' hole a second time for the second case branch. +-} {- ************************************************************************ @@ -1337,7 +1393,7 @@ tcSubTypeMono rn_expr act_ty exp_ty , text "act_ty:" <+> ppr act_ty , text "rn_expr:" <+> ppr rn_expr]) $ case exp_ty of - Infer inf_res -> fillInferResult act_ty inf_res + Infer inf_res -> fillInferResultNoInst act_ty inf_res Check exp_ty -> unifyType (Just $ HsExprRnThing rn_expr) act_ty exp_ty ------------------------ @@ -1351,7 +1407,7 @@ tcSubTypePat inst_orig ctxt (Check ty_actual) ty_expected = tc_sub_type unifyTypeET inst_orig ctxt ty_actual ty_expected tcSubTypePat _ _ (Infer inf_res) ty_expected - = do { co <- fillInferResult ty_expected inf_res + = do { co <- fillInferResultNoInst ty_expected inf_res -- In patterns we do not instantatiate ; return (mkWpCastN (mkSymCo co)) } @@ -1377,7 +1433,7 @@ tcSubTypeDS rn_expr act_rho exp_rho -- | Checks that the 'actual' type is more polymorphic than the 'expected' type. tcSubType :: CtOrigin -- ^ Used when instantiating -> UserTypeCtxt -- ^ Used when skolemising - -> Maybe TypedThing -- ^ The expression that has type 'actual' (if known) + -> Maybe TypedThing -- ^ The expression that has type 'actual' (if known) -> TcSigmaType -- ^ Actual type -> ExpRhoType -- ^ Expected type -> TcM HsWrapper @@ -1386,10 +1442,7 @@ tcSubType inst_orig ctxt m_thing ty_actual res_ty Check ty_expected -> tc_sub_type (unifyType m_thing) inst_orig ctxt ty_actual ty_expected - Infer inf_res -> do { (wrap, rho) <- topInstantiate inst_orig ty_actual - -- See Note [Instantiation of InferResult] - ; inst <- fillInferResultDS inst_orig rho inf_res - ; return (inst <.> wrap) } + Infer inf_res -> fillInferResult inst_orig ty_actual inf_res --------------- tcSubTypeSigma :: CtOrigin -- where did the actual type arise / why are we @@ -1428,47 +1481,6 @@ addSubTypeCtxt ty_actual ty_expected thing_inside ; return (tidy_env, SubTypeCtxt ty_expected ty_actual) } -{- Note [Instantiation of InferResult] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When typechecking expressions (not types, not patterns), we always instantiate -before filling in InferResult, so that the result is a TcRhoType. -See #17173 for discussion. - -For example: - -1. Consider - f x = (*) - We want to instantiate the type of (*) before returning, else we - will infer the type - f :: forall {a}. a -> forall b. Num b => b -> b -> b - This is surely confusing for users. - - And worse, the monomorphism restriction won't work properly. The MR is - dealt with in simplifyInfer, and simplifyInfer has no way of - instantiating. This could perhaps be worked around, but it may be - hard to know even when instantiation should happen. - -2. Another reason. Consider - f :: (?x :: Int) => a -> a - g y = let ?x = 3::Int in f - Here want to instantiate f's type so that the ?x::Int constraint - gets discharged by the enclosing implicit-parameter binding. - -3. Suppose one defines plus = (+). If we instantiate lazily, we will - infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism - restriction compels us to infer - plus :: Integer -> Integer -> Integer - (or similar monotype). Indeed, the only way to know whether to apply - the monomorphism restriction at all is to instantiate - -There is one place where we don't want to instantiate eagerly, -namely in GHC.Tc.Module.tcRnExpr, which implements GHCi's :type -command. See Note [Implementing :type] in GHC.Tc.Module. - -This also means that, if DeepSubsumption is enabled, we should also instantiate -deeply; we do this by using fillInferResultDS. --} - --------------- tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify -> CtOrigin -- Used when instantiating @@ -2133,7 +2145,17 @@ deeplySkolemise skol_info ty = return (idHsWrapper, [], [], substTy subst ty) -- substTy is a quick no-op on an empty substitution +dsInstantiate :: CtOrigin -> TcType -> TcM (HsWrapper, Type) +-- Do topInstantiate or deeplyInstantiate, depending on -XDeepSubsumption +dsInstantiate orig ty + = do { ds_flag <- getDeepSubsumptionFlag + ; case ds_flag of + Shallow -> topInstantiate orig ty + Deep -> deeplyInstantiate orig ty } + deeplyInstantiate :: CtOrigin -> TcType -> TcM (HsWrapper, Type) +-- Instantiate invisible foralls, even ones nested +-- (to the right) under arrows deeplyInstantiate orig ty = go init_subst ty where @@ -3342,8 +3364,9 @@ mapCheck f xs -- | Options describing how to deal with a type equality -- in the eager unifier. See 'checkTyEqRhs' data TyEqFlags m a - -- | LHS is a type family application; we are not unifying. - = TEFTyFam + = -- | TFTyFam: LHS is a type family application + -- Invariant: we are not unifying; see `notUnifying_TEFTask` + TEFTyFam { tefTyFam_occursCheck :: CheckTyEqProblem -- ^ The 'CheckTyEqProblem' to report for occurs-check failures -- (soluble or insoluble) @@ -3352,7 +3375,8 @@ data TyEqFlags m a , tef_fam_app :: TyEqFamApp m a -- ^ How to deal with type family applications } - -- | LHS is a 'TyVar'. + + -- | TEFTyVar: LHS is a 'TyVar'. | TEFTyVar -- NB: this constructor does not actually store a 'TyVar', in order to -- support being called from 'makeTypeConcrete' (which works as if we ===================================== testsuite/tests/patsyn/should_compile/T26331.hs ===================================== @@ -0,0 +1,47 @@ +{-# LANGUAGE DeepSubsumption #-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE TypeAbstractions #-} +{-# LANGUAGE StandaloneKindSignatures #-} + +module T26331 where + +import Data.Kind (Constraint, Type) + +type Apply :: (k1 ~> k2) -> k1 -> k2 +type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 + +type (~>) :: Type -> Type -> Type +type a ~> b = TyFun a b -> Type +infixr 0 ~> + +data TyFun :: Type -> Type -> Type + +type Sing :: k -> Type +type family Sing @k :: k -> Type + +type SingFunction2 :: (a1 ~> a2 ~> b) -> Type +type SingFunction2 (f :: a1 ~> a2 ~> b) = + forall t1 t2. Sing t1 -> Sing t2 -> Sing (f `Apply` t1 `Apply` t2) + +unSingFun2 :: forall f. Sing f -> SingFunction2 f +-- unSingFun2 :: forall f. Sing f -> forall t1 t2. blah +unSingFun2 sf x = error "urk" + +singFun2 :: forall f. SingFunction2 f -> Sing f +singFun2 f = error "urk" + +-------- This is the tricky bit ------- +pattern SLambda2 :: forall f. SingFunction2 f -> Sing f +pattern SLambda2 x <- (unSingFun2 -> x) -- We want to push down (SingFunction2 f) + -- /uninstantiated/ into the pattern `x` + where + SLambda2 lam2 = singFun2 lam2 + ===================================== testsuite/tests/patsyn/should_compile/T26331a.hs ===================================== @@ -0,0 +1,11 @@ +{-# LANGUAGE DeepSubsumption #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE RankNTypes #-} + +module T26331a where + +pair :: forall a. Bool -> a -> forall b. b -> (a,b) +pair = error "urk" + +f :: Int -> ((Int,Bool),(Int,Char)) +f (pair True -> x) = (x True, x 'c') -- (x :: forall b. b -> (Int,b)) ===================================== testsuite/tests/patsyn/should_compile/all.T ===================================== @@ -85,3 +85,5 @@ test('T21531', [ grep_errmsg(r'INLINE') ], compile, ['-ddump-ds']) test('T22521', normal, compile, ['']) test('T23038', normal, compile_fail, ['']) test('T22328', normal, compile, ['']) +test('T26331', normal, compile, ['']) +test('T26331a', normal, compile, ['']) ===================================== testsuite/tests/typecheck/should_compile/T26346.hs ===================================== @@ -0,0 +1,103 @@ +{-# LANGUAGE GHC2024 #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +module T26346 (warble) where + +import Data.Kind (Type) +import Data.Type.Equality ((:~:)(..)) + +type Nat :: Type +data Nat = Z | S Nat + +type SNat :: Nat -> Type +data SNat n where + SZ :: SNat Z + SS :: SNat n -> SNat (S n) + +type NatPlus :: Nat -> Nat -> Nat +type family NatPlus a b where + NatPlus Z b = b + NatPlus (S a) b = S (NatPlus a b) + +sNatPlus :: + forall (a :: Nat) (b :: Nat). + SNat a -> + SNat b -> + SNat (NatPlus a b) +sNatPlus SZ b = b +sNatPlus (SS a) b = SS (sNatPlus a b) + +data Bin + = Zero + | Even Bin + | Odd Bin + +type SBin :: Bin -> Type +data SBin b where + SZero :: SBin Zero + SEven :: SBin n -> SBin (Even n) + SOdd :: SBin n -> SBin (Odd n) + +type Incr :: Bin -> Bin +type family Incr b where + Incr Zero = Odd Zero -- 0 + 1 = (2*0) + 1 + Incr (Even n) = Odd n -- 2n + 1 + Incr (Odd n) = Even (Incr n) -- (2n + 1) + 1 = 2*(n + 1) + +type BinToNat :: Bin -> Nat +type family BinToNat b where + BinToNat Zero = Z + BinToNat (Even n) = NatPlus (BinToNat n) (BinToNat n) + BinToNat (Odd n) = S (NatPlus (BinToNat n) (BinToNat n)) + +sBinToNat :: + forall (b :: Bin). + SBin b -> + SNat (BinToNat b) +sBinToNat SZero = SZ +sBinToNat (SEven n) = sNatPlus (sBinToNat n) (sBinToNat n) +sBinToNat (SOdd n) = SS (sNatPlus (sBinToNat n) (sBinToNat n)) + +warble :: + forall (b :: Bin). + SBin b -> + BinToNat (Incr b) :~: S (BinToNat b) +warble SZero = Refl +warble (SEven {}) = Refl +warble (SOdd sb) | Refl <- warble sb + , Refl <- plusComm sbn (SS sbn) + = Refl + where + sbn = sBinToNat sb + + plus0R :: + forall (n :: Nat). + SNat n -> + NatPlus n Z :~: n + plus0R SZ = Refl + plus0R (SS sn) + | Refl <- plus0R sn + = Refl + + plusSnR :: + forall (n :: Nat) (m :: Nat). + SNat n -> + SNat m -> + NatPlus n (S m) :~: S (NatPlus n m) + plusSnR SZ _ = Refl + plusSnR (SS sn) sm + | Refl <- plusSnR sn sm + = Refl + + plusComm :: + forall (n :: Nat) (m :: Nat). + SNat n -> + SNat m -> + NatPlus n m :~: NatPlus m n + plusComm SZ sm + | Refl <- plus0R sm + = Refl + plusComm (SS sn) sm + | Refl <- plusComm sn sm + , Refl <- plusSnR sm sn + = Refl ===================================== testsuite/tests/typecheck/should_compile/T26350.hs ===================================== @@ -0,0 +1,18 @@ +{-# LANGUAGE DeepSubsumption #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +{-# OPTIONS_GHC -dcore-lint #-} + +module T26350 where + +import Control.Arrow (first) + +infix 6 .-. + +class AffineSpace p where + type Diff p + (.-.) :: p -> p -> Diff p + +affineCombo :: (AffineSpace p, v ~ Diff p) => p -> (p,v) -> (v,v) +affineCombo z l = first (.-. z) l ===================================== testsuite/tests/typecheck/should_compile/T26358.hs ===================================== @@ -0,0 +1,48 @@ +{-# LANGUAGE TypeFamilies #-} + +module T26358 where +import Data.Kind +import Data.Proxy + +{- Two failing tests, described in GHC.Core.Unify + Note [Shortcomings of the apartness test] + +Explanation for TF2 +* We try to reduce + (TF2 (F (G Float)) (F Int) (G Float)) +* We can only do so if those arguments are apart from the first + equation of TF2, namely (Bool,Char,Int). +* So we try to unify + [F (G Float), F Int, G Float] ~ [Bool, Char, Int] +* They really are apart, but we can't quite spot that yet; + hence #26358 + +TF1 is similar. +-} + + +type TF1 :: Type -> Type -> Type -> Type +type family TF1 a b c where + TF1 Bool Char a = Word + TF1 a b c = (a,b,c) + +type F :: Type -> Type +type family F a where + +foo :: Proxy a + -> Proxy (TF1 (F a) (F Int) Int) + -> Proxy (F a, F Int, Int) +foo _ px = px + +type TF2 :: Type -> Type -> Type -> Type +type family TF2 a b c where + TF2 Bool Char Int = Word + TF2 a b c = (a,b,c) + +type G :: Type -> Type +type family G a where + +bar :: Proxy (TF2 (F (G Float)) (F Int) (G Float)) + -> Proxy (F (G Float), F Int, G Float) +bar px = px + ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -862,6 +862,7 @@ test('DeepSubsumption06', normal, compile, ['-XHaskell98']) test('DeepSubsumption07', normal, compile, ['-XHaskell2010']) test('DeepSubsumption08', normal, compile, ['']) test('DeepSubsumption09', normal, compile, ['']) +test('T26350', normal, compile, ['']) test('T26225', normal, compile, ['']) test('T26225b', normal, compile, ['']) test('T21765', normal, compile, ['']) @@ -945,3 +946,5 @@ test('T25992', normal, compile, ['']) test('T14010', normal, compile, ['']) test('T26256a', normal, compile, ['']) test('T25992a', normal, compile, ['']) +test('T26346', normal, compile, ['']) +test('T26358', expect_broken(26358), compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/299b483c9e86a26467ab3e460c13717... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/299b483c9e86a26467ab3e460c13717... You're receiving this email because of your account on gitlab.haskell.org.