| ... |
... |
@@ -173,79 +173,42 @@ Note [Instantiation variables are short lived] |
|
173
|
173
|
|
|
174
|
174
|
{- Note [splitHsApps, XExpr and tcExprSigma]
|
|
175
|
175
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
176
|
+The basic plan for applications, in tcApp, is this:
|
|
|
177
|
+ (1) Gather the arguments, using `splitHsApps`, yielding (fun, [arg]).
|
|
|
178
|
+ (2) /Infer/ the sigma-type of `fun`, using `tcInferAppHead`.
|
|
|
179
|
+ (3) Then instantiate with `tcInstFun` and do QuickLook as described in
|
|
|
180
|
+ the paper.
|
|
176
|
181
|
|
|
177
|
|
-This implementation is WIP and is subject to change once MR!15811 is figured out
|
|
|
182
|
+Some important wrinkles:
|
|
178
|
183
|
|
|
179
|
|
-To simplify the implementation of `splitHsApps`, we do not look through
|
|
180
|
|
-XExpr's, however, we still need to deal with cases such as:
|
|
|
184
|
+(TCA1) Suppose `tcExpr` sees a naked variable: we /still/ delegate to `tcApp`,
|
|
|
185
|
+ with an empty argument list. Why? Because we must do the QuickLook stuff.
|
|
|
186
|
+ E.g. tcExpr `undefined` (Check ((forall a. a->a) -> Int))
|
|
|
187
|
+ where undefined :: forall b. b
|
|
|
188
|
+ Here we must use QuickLooko to instantiate b:=(forall a. a->a) -> Int)
|
|
|
189
|
+ By far the easiest way to do this is to delegate to tcApp.
|
|
181
|
190
|
|
|
182
|
|
- (XExpr (ExpandedThingRn f1 (f `HsApp` e1))) `HsApp` e2 `HsApp` e3
|
|
|
191
|
+ So Step (2), `tcInferAppHead` must treat a naked variable specially, and
|
|
|
192
|
+ /not/ delegate to `tcExpr` -- because the later delegates to `tcApp`!
|
|
183
|
193
|
|
|
184
|
|
-Otherwise stuff like overloaded labels (#19154) won't work.
|
|
|
194
|
+ This applies equally to `HsOverLit` as well as `HsVar`.
|
|
185
|
195
|
|
|
186
|
|
-How do we do it?
|
|
|
196
|
+(TCA2) Currently -- THIS IS SUBJECT TO CHANGE -- we do not expand XExprs in
|
|
|
197
|
+ `splitHsApps`. Instead, we infer the sigma-type of the function.
|
|
187
|
198
|
|
|
188
|
|
-`splitHsApps` peals off the arguments until it hits an XExpr
|
|
189
|
|
-From above example,
|
|
|
199
|
+ This is unsatisfactory, because
|
|
|
200
|
+ * We want QuickLook to work "across" expansions
|
|
|
201
|
+ * Ditto deep subsumption for constructors
|
|
190
|
202
|
|
|
191
|
|
- splitHsApps ((XExpr (ExpandedThingRn f1 (f `HsApp` e1))) `HsApp` e2 `HsApp` e3)
|
|
192
|
|
- = { head = XExpr (ExpandedThingRn f1 (f `HsApp` e1))
|
|
193
|
|
- , args = [e3, e2] -- NB: arguments are in the reverse order
|
|
194
|
|
- }
|
|
195
|
|
-
|
|
196
|
|
-Now, we infer the type of head using tcInferAppHead/tcInferAppHead_maybe.
|
|
197
|
|
-Which calls `tcExprSigma` on the XExpr. It performs a mini-`tcApp`
|
|
198
|
|
-where it uses the CtOrigin obtained from f1, splits the application chain: f `HsApp` e1.
|
|
199
|
|
-and finally returns an uninstantiated sigma type and a typechecked expression
|
|
200
|
|
-
|
|
201
|
|
-It is crucial for tcExprSigma to return an uninstantiated type so that visible type
|
|
202
|
|
-applications with rebindable syntax works fine. Eg. T19167
|
|
203
|
|
-
|
|
204
|
|
-
|
|
205
|
|
- fromListN :: Int -> [elt] -> (forall list. (IsList list, elt ~ Item list) => list)
|
|
206
|
|
- fromListN n l = Predule.fromListN n l
|
|
207
|
|
-
|
|
208
|
|
- shouldBeANonEmpty = ['x', 'y', 'z'] @(NonEmpty Char)
|
|
209
|
|
-
|
|
210
|
|
-here the RHS of `shouldBeNonEmpty` is expanded to
|
|
211
|
|
- (XExpr (ExpandedThingRn (['x', 'y', 'z']) (fromListN 3 ['x', 'y', 'z']) `HsTypeApp` (NonEmpty Char)
|
|
212
|
|
-
|
|
213
|
|
-Now, if we were to instantiate the head of the expression, we will
|
|
214
|
|
-fail to typecheck the expression as the type `NonEmpty Char`.
|
|
215
|
|
-
|
|
216
|
|
-
|
|
217
|
|
-Wrinkle [DeepSubsumption Flag and Multiplicity]
|
|
218
|
|
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
219
|
|
-
|
|
220
|
|
-Consider the expression:
|
|
221
|
|
-
|
|
222
|
|
- (1 :) $ [2, 3]
|
|
223
|
|
-
|
|
224
|
|
-Here, the head of the expression is ($) and it is applied to two arguments
|
|
225
|
|
- Arg1 = (1 :)
|
|
226
|
|
- Arg2 = [2, 3]
|
|
227
|
|
-
|
|
228
|
|
-Arg1 is an expanded expression as it is a left section wrapped with parenthesis
|
|
229
|
|
-
|
|
230
|
|
- Arg1 = HsPar (XExpr (ExpandedThingRn (HSE (1 :) ((:) 1))))
|
|
231
|
|
-
|
|
232
|
|
-As `($)` is the head of the application chain, we perform QuickLook on the arguments
|
|
233
|
|
-in `tcInstFun`. See Note [Quick Look for particular Ids] and Note [tcApp: typechecking applications].
|
|
234
|
|
-
|
|
235
|
|
-Thus, Arg1 will be transformed into
|
|
236
|
|
-
|
|
237
|
|
- EValArgQL { eaql_tc_head = XExpr (ExpandedThingRn (HSE { hs_ctxt = 1 : , hs_expr = ((:) 1))))
|
|
238
|
|
- , eaql_arg_ty = [alpha] %1 -> [beta]
|
|
239
|
|
- , eqql_args = [EPar] }
|
|
240
|
|
-
|
|
241
|
|
-Now, in `tcValArg` Arg1 is expected to have type [Int] -> [Int],
|
|
242
|
|
-and according to Note [Typechecking data constructors], we ought to be able to
|
|
243
|
|
-coerce the type [alpha] %1 -> [beta] into type [Int] -> [Int] in `checkResultTy`
|
|
244
|
|
-because the "actual" head of Arg1 is (:), thus we need to traverse eaql_tc_head.
|
|
245
|
|
-
|
|
246
|
|
-The hope is that future refactoring simplifies this delicate and complicated process.
|
|
|
203
|
+ e.g (e1 `K`) e2
|
|
|
204
|
+ where the (e1 `K`) is a left section
|
|
|
205
|
+ We really want this to behave exactly like (K e1 e2)
|
|
247
|
206
|
|
|
|
207
|
+ For now we have several annoying consequences:
|
|
|
208
|
+ * tcInferAppHead calls tcInferExprSigma to infer a sigma-type
|
|
|
209
|
+ * getDeepSubsumptionFlag_DataConHead must look down an application chain
|
|
248
|
210
|
-}
|
|
|
211
|
+
|
|
249
|
212
|
-- Very similar to tcApp, but returns a sigma (uninstantiated) type
|
|
250
|
213
|
-- CAUTION: Any changes to tcApp should be reflected here
|
|
251
|
214
|
-- cf. T19167. the head is an expanded expression applied to a type
|