Simon Peyton Jones pushed to branch wip/spj-apporv-Oct24 at Glasgow Haskell Compiler / GHC Commits: 6beed081 by Simon Peyton Jones at 2026-03-31T15:21:03+01:00 Wibble comment [skip ci] Shorten Note [splitHsApps, XExpr and tcExprSigma] which is still very much in flux - - - - - 1 changed file: - compiler/GHC/Tc/Gen/App.hs Changes: ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -173,79 +173,42 @@ Note [Instantiation variables are short lived] {- Note [splitHsApps, XExpr and tcExprSigma] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The basic plan for applications, in tcApp, is this: + (1) Gather the arguments, using `splitHsApps`, yielding (fun, [arg]). + (2) /Infer/ the sigma-type of `fun`, using `tcInferAppHead`. + (3) Then instantiate with `tcInstFun` and do QuickLook as described in + the paper. -This implementation is WIP and is subject to change once MR!15811 is figured out +Some important wrinkles: -To simplify the implementation of `splitHsApps`, we do not look through -XExpr's, however, we still need to deal with cases such as: +(TCA1) Suppose `tcExpr` sees a naked variable: we /still/ delegate to `tcApp`, + with an empty argument list. Why? Because we must do the QuickLook stuff. + E.g. tcExpr `undefined` (Check ((forall a. a->a) -> Int)) + where undefined :: forall b. b + Here we must use QuickLooko to instantiate b:=(forall a. a->a) -> Int) + By far the easiest way to do this is to delegate to tcApp. - (XExpr (ExpandedThingRn f1 (f `HsApp` e1))) `HsApp` e2 `HsApp` e3 + So Step (2), `tcInferAppHead` must treat a naked variable specially, and + /not/ delegate to `tcExpr` -- because the later delegates to `tcApp`! -Otherwise stuff like overloaded labels (#19154) won't work. + This applies equally to `HsOverLit` as well as `HsVar`. -How do we do it? +(TCA2) Currently -- THIS IS SUBJECT TO CHANGE -- we do not expand XExprs in + `splitHsApps`. Instead, we infer the sigma-type of the function. -`splitHsApps` peals off the arguments until it hits an XExpr -From above example, + This is unsatisfactory, because + * We want QuickLook to work "across" expansions + * Ditto deep subsumption for constructors - splitHsApps ((XExpr (ExpandedThingRn f1 (f `HsApp` e1))) `HsApp` e2 `HsApp` e3) - = { head = XExpr (ExpandedThingRn f1 (f `HsApp` e1)) - , args = [e3, e2] -- NB: arguments are in the reverse order - } - -Now, we infer the type of head using tcInferAppHead/tcInferAppHead_maybe. -Which calls `tcExprSigma` on the XExpr. It performs a mini-`tcApp` -where it uses the CtOrigin obtained from f1, splits the application chain: f `HsApp` e1. -and finally returns an uninstantiated sigma type and a typechecked expression - -It is crucial for tcExprSigma to return an uninstantiated type so that visible type -applications with rebindable syntax works fine. Eg. T19167 - - - fromListN :: Int -> [elt] -> (forall list. (IsList list, elt ~ Item list) => list) - fromListN n l = Predule.fromListN n l - - shouldBeANonEmpty = ['x', 'y', 'z'] @(NonEmpty Char) - -here the RHS of `shouldBeNonEmpty` is expanded to - (XExpr (ExpandedThingRn (['x', 'y', 'z']) (fromListN 3 ['x', 'y', 'z']) `HsTypeApp` (NonEmpty Char) - -Now, if we were to instantiate the head of the expression, we will -fail to typecheck the expression as the type `NonEmpty Char`. - - -Wrinkle [DeepSubsumption Flag and Multiplicity] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Consider the expression: - - (1 :) $ [2, 3] - -Here, the head of the expression is ($) and it is applied to two arguments - Arg1 = (1 :) - Arg2 = [2, 3] - -Arg1 is an expanded expression as it is a left section wrapped with parenthesis - - Arg1 = HsPar (XExpr (ExpandedThingRn (HSE (1 :) ((:) 1)))) - -As `($)` is the head of the application chain, we perform QuickLook on the arguments -in `tcInstFun`. See Note [Quick Look for particular Ids] and Note [tcApp: typechecking applications]. - -Thus, Arg1 will be transformed into - - EValArgQL { eaql_tc_head = XExpr (ExpandedThingRn (HSE { hs_ctxt = 1 : , hs_expr = ((:) 1)))) - , eaql_arg_ty = [alpha] %1 -> [beta] - , eqql_args = [EPar] } - -Now, in `tcValArg` Arg1 is expected to have type [Int] -> [Int], -and according to Note [Typechecking data constructors], we ought to be able to -coerce the type [alpha] %1 -> [beta] into type [Int] -> [Int] in `checkResultTy` -because the "actual" head of Arg1 is (:), thus we need to traverse eaql_tc_head. - -The hope is that future refactoring simplifies this delicate and complicated process. + e.g (e1 `K`) e2 + where the (e1 `K`) is a left section + We really want this to behave exactly like (K e1 e2) + For now we have several annoying consequences: + * tcInferAppHead calls tcInferExprSigma to infer a sigma-type + * getDeepSubsumptionFlag_DataConHead must look down an application chain -} + -- Very similar to tcApp, but returns a sigma (uninstantiated) type -- CAUTION: Any changes to tcApp should be reflected here -- cf. T19167. the head is an expanded expression applied to a type View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6beed0814ab20adffa66042d31f1ff75... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6beed0814ab20adffa66042d31f1ff75... You're receiving this email because of your account on gitlab.haskell.org.