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.
