Simon Peyton Jones pushed to branch wip/ani/no-ds-flag-cache at Glasgow Haskell Compiler / GHC Commits: 80ef7754 by Simon Peyton Jones at 2026-03-31T12:12:19+01:00 Update comments - - - - - 57261072 by Simon Peyton Jones at 2026-03-31T12:12:59+01:00 Unused imports - - - - - 2 changed files: - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Utils/Unify.hs Changes: ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -461,11 +461,8 @@ checkResultTy :: HsExpr GhcRn -> TcM HsWrapper checkResultTy rn_expr (tc_fun,_) _ app_res_rho (Infer inf_res) = do { ds_flag <- getDeepSubsumptionFlag_DataConHead tc_fun - -- We must deeply-instantiate data constructors - -- E.g. data T = MkT Int int - -- f = K 3 - -- We must infer f :: Int ->{many} T - -- and not f :: Int ->{one} T + -- Why the "DataConHead" bit? See (IIR5) in + -- Note [Instantiation of InferResult] in GHC.Tc.Utils.Unify. ; fillInferResult ds_flag (exprCtOrigin rn_expr) app_res_rho inf_res } checkResultTy rn_expr (tc_fun, fun_loc) inst_args app_res_rho (Check res_ty) ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -99,13 +99,13 @@ import qualified GHC.LanguageExtensions as LangExt import GHC.Builtin.Types import GHC.Types.Name -import GHC.Types.Id( idType, isDataConId ) +import GHC.Types.Id( idType ) import GHC.Types.Var as Var import GHC.Types.Var.Set import GHC.Types.Var.Env import GHC.Types.Basic import GHC.Types.Unique.Set (nonDetEltsUniqSet) -import GHC.Types.SrcLoc (unLoc, GenLocated (..)) +import GHC.Types.SrcLoc ( GenLocated (..) ) import GHC.Utils.Misc import GHC.Utils.Outputable as Outputable @@ -1305,7 +1305,7 @@ 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 +(IIR1) Consider f x = (*) We want to instantiate the type of (*) before returning, else we will infer the type @@ -1317,21 +1317,46 @@ of why: instantiating. This could perhaps be worked around, but it may be hard to know even when instantiation should happen. -2. Another reason. Consider +(IIR2) 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 +(IIR3) 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": +(IIR4) When -XDeepSubsumption is on, we /deeply/ instantiate. 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. + +(IIR5) When inferring, even /without/ -XDeepSubsumption, we must deeply instantiate + the types of data constructors. E.g + data T = MkT Int int + f = MkT 3 + We must infer MkT 3 :: Int ->{mu} T (fresh mu) + and not MkT 3 :: Int ->{one} T + See Note [Typechecking data constructors] in GHC.Tc.Gen.Head + Hence the use of `getDeepSubsumptionFlag_DataConHead` in `checkResultTy`. + +HOWEVER, `ir_inst` is not always `IIF_DeepRho`! Here are places when it isn't: * IIF_Sigma: In GHC.Tc.Module.tcRnExpr, which implements GHCi's :type command, we want to return a completely uninstantiated type. @@ -1347,23 +1372,6 @@ HOWEVER, not always! Here are places where we want `IIF_Sigma` meaning 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. -} {- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/3418bdbadd44cd7bf8b7cb47cf912c2... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/3418bdbadd44cd7bf8b7cb47cf912c2... You're receiving this email because of your account on gitlab.haskell.org.