never executed always true always false
1
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE FlexibleContexts #-}
4 {-# LANGUAGE GADTs #-}
5 {-# LANGUAGE LambdaCase #-}
6 {-# LANGUAGE ScopedTypeVariables #-}
7 {-# LANGUAGE TypeFamilies #-}
8 {-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow]
9
10 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
11
12 {-
13 %
14 (c) The University of Glasgow 2006
15 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
16 -}
17
18 module GHC.Tc.Gen.App
19 ( tcApp
20 , tcInferSigma
21 , tcExprPrag ) where
22
23 import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcPolyExpr )
24
25 import GHC.Types.Basic ( Arity )
26 import GHC.Types.Id ( idArity, idName, hasNoBinding )
27 import GHC.Types.Name ( isWiredInName )
28 import GHC.Types.Var
29 import GHC.Builtin.Types ( multiplicityTy )
30 import GHC.Core.ConLike ( ConLike(..) )
31 import GHC.Core.DataCon ( dataConRepArity
32 , isNewDataCon, isUnboxedSumDataCon, isUnboxedTupleDataCon )
33 import GHC.Tc.Gen.Head
34 import GHC.Hs
35 import GHC.Tc.Errors.Types
36 import GHC.Tc.Utils.Monad
37 import GHC.Tc.Utils.Unify
38 import GHC.Tc.Utils.Instantiate
39 import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep )
40 import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst_maybe )
41 import GHC.Tc.Gen.HsType
42 import GHC.Tc.Utils.TcMType
43 import GHC.Tc.Types.Origin
44 import GHC.Tc.Utils.TcType as TcType
45 import GHC.Core.TyCon
46 import GHC.Core.TyCo.Rep
47 import GHC.Core.TyCo.Ppr
48 import GHC.Core.TyCo.Subst (substTyWithInScope)
49 import GHC.Core.TyCo.FVs( shallowTyCoVarsOfType )
50 import GHC.Core.Type
51 import GHC.Tc.Types.Evidence
52 import GHC.Types.Var.Set
53 import GHC.Builtin.PrimOps( tagToEnumKey )
54 import GHC.Builtin.Names
55 import GHC.Driver.Session
56 import GHC.Types.SrcLoc
57 import GHC.Types.Var.Env ( emptyTidyEnv, mkInScopeSet )
58 import GHC.Data.Maybe
59 import GHC.Utils.Misc
60 import GHC.Utils.Outputable as Outputable
61 import GHC.Utils.Panic
62 import qualified GHC.LanguageExtensions as LangExt
63
64 import Control.Monad
65 import Data.Function
66
67 import GHC.Prelude
68
69 {- *********************************************************************
70 * *
71 Quick Look overview
72 * *
73 ********************************************************************* -}
74
75 {- Note [Quick Look]
76 ~~~~~~~~~~~~~~~~~~~~
77 The implementation of Quick Look closely follows the QL paper
78 A quick look at impredicativity, Serrano et al, ICFP 2020
79 https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/
80
81 All the moving parts are in this module, GHC.Tc.Gen.App, so named
82 because it deal with n-ary application. The main workhorse is tcApp.
83
84 Some notes relative to the paper
85
86 * The "instantiation variables" of the paper are ordinary unification
87 variables. We keep track of which variables are instantiation variables
88 by keeping a set Delta of instantiation variables.
89
90 * When we learn what an instantiation variable must be, we simply unify
91 it with that type; this is done in qlUnify, which is the function mgu_ql(t1,t2)
92 of the paper. This may fill in a (mutable) instantiation variable with
93 a polytype.
94
95 * When QL is done, we don't need to turn the un-filled-in
96 instantiation variables into unification variables -- they
97 already /are/ unification varibles! See also
98 Note [Instantiation variables are short lived].
99
100 * We cleverly avoid the quadratic cost of QL, alluded to in the paper.
101 See Note [Quick Look at value arguments]
102
103 Note [Instantiation variables are short lived]
104 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
105 By the time QL is done, all filled-in occurrences of instantiation
106 variables have been zonked away (see "Crucial step" in tcValArgs),
107 and so the constraint /generator/ never subsequently sees a meta-type
108 variable filled in with a polytype -- a meta type variable stands
109 (only) for a monotype. See Section 4.3 "Applications and instantiation"
110 of the paper.
111
112 However, the constraint /solver/ can see a meta-type-variable filled
113 in with a polytype (#18987). Suppose
114 f :: forall a. Dict a => [a] -> [a]
115 xs :: [forall b. b->b]
116 and consider the call (f xs). QL will
117 * Instantiate f, with a := kappa, where kappa is an instantiation variable
118 * Emit a constraint (Dict kappa), via instantiateSigma, called from tcInstFun
119 * Do QL on the argument, to discover kappa := forall b. b->b
120
121 But by the time the third step has happened, the constraint has been
122 emitted into the monad. The constraint solver will later find it, and
123 rewrite it to (Dict (forall b. b->b)). That's fine -- the constraint
124 solver does no implicit instantiation (which is what makes it so
125 tricky to have foralls hiding inside unification variables), so there
126 is no difficulty with allowing those filled-in kappa's to persist.
127 (We could find them and zonk them away, but that would cost code and
128 execution time, for no purpose.)
129
130 Since the constraint solver does not do implicit instantiation (as the
131 constraint generator does), the fact that a unification variable might
132 stand for a polytype does not matter.
133 -}
134
135
136 {- *********************************************************************
137 * *
138 tcInferSigma
139 * *
140 ********************************************************************* -}
141
142 tcInferSigma :: Bool -> LHsExpr GhcRn -> TcM TcSigmaType
143 -- Used only to implement :type; see GHC.Tc.Module.tcRnExpr
144 -- True <=> instantiate -- return a rho-type
145 -- False <=> don't instantiate -- return a sigma-type
146 tcInferSigma inst (L loc rn_expr)
147 | (fun@(rn_fun,_), rn_args) <- splitHsApps rn_expr
148 = addExprCtxt rn_expr $
149 setSrcSpanA loc $
150 do { do_ql <- wantQuickLook rn_fun
151 ; (_tc_fun, fun_sigma) <- tcInferAppHead fun rn_args
152 ; (_delta, inst_args, app_res_sigma) <- tcInstFun do_ql inst fun fun_sigma rn_args
153 ; _tc_args <- tcValArgs do_ql inst_args
154 ; return app_res_sigma }
155
156 {- *********************************************************************
157 * *
158 Typechecking n-ary applications
159 * *
160 ********************************************************************* -}
161
162 {- Note [Application chains and heads]
163 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
164 Quick Look treats application chains specially. What is an
165 "application chain"? See Fig 2, of the QL paper: "A quick look at
166 impredicativity" (ICFP'20). Here's the syntax:
167
168 app :: head
169 | app expr -- HsApp: ordinary application
170 | app @type -- HsTypeApp: VTA
171 | expr `head` expr -- OpApp: infix applications
172 | ( app ) -- HsPar: parens
173 | {-# PRAGMA #-} app -- HsPragE: pragmas
174
175 head ::= f -- HsVar: variables
176 | fld -- HsRecSel: record field selectors
177 | (expr :: ty) -- ExprWithTySig: expr with user type sig
178 | lit -- HsOverLit: overloaded literals
179 | other_expr -- Other expressions
180
181 When tcExpr sees something that starts an application chain (namely,
182 any of the constructors in 'app' or 'head'), it invokes tcApp to
183 typecheck it: see Note [tcApp: typechecking applications]. However,
184 for HsPar and HsPragE, there is no tcWrapResult (which would
185 instantiate types, bypassing Quick Look), so nothing is gained by
186 using the application chain route, and we can just recurse to tcExpr.
187
188 A "head" has three special cases (for which we can infer a polytype
189 using tcInferAppHead_maybe); otherwise is just any old expression (for
190 which we can infer a rho-type (via tcInfer).
191
192 There is no special treatment for HsUnboundVar, HsOverLit etc, because
193 we can't get a polytype from them.
194
195 Left and right sections (e.g. (x +) and (+ x)) are not yet supported.
196 Probably left sections (x +) would be esay to add, since x is the
197 first arg of (+); but right sections are not so easy. For symmetry
198 reasons I've left both unchanged, in GHC.Tc.Gen.Expr.
199
200 It may not be immediately obvious why ExprWithTySig (e::ty) should be
201 dealt with by tcApp, even when it is not applied to anything. Consider
202 f :: [forall a. a->a] -> Int
203 ...(f (undefined :: forall b. b))...
204 Clearly this should work! But it will /only/ work because if we
205 instantiate that (forall b. b) impredicatively! And that only happens
206 in tcApp.
207
208 Note [tcApp: typechecking applications]
209 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
210 tcApp implements the APP-Downarrow/Uparrow rule of
211 Fig 3, plus the modification in Fig 5, of the QL paper:
212 "A quick look at impredicativity" (ICFP'20).
213
214 It treats application chains (f e1 @ty e2) specially:
215
216 * So we can report errors like "in the third arument of a call of f"
217
218 * So we can do Visible Type Application (VTA), for which we must not
219 eagerly instantiate the function part of the application.
220
221 * So that we can do Quick Look impredicativity.
222
223 tcApp works like this:
224
225 1. Use splitHsApps, which peels off
226 HsApp, HsTypeApp, HsPrag, HsPar
227 returning the function in the corner and the arguments
228
229 splitHsApps can deal with infix as well as prefix application,
230 and returns a Rebuilder to re-assemble the the application after
231 typechecking.
232
233 The "list of arguments" is [HsExprArg], described in Note [HsExprArg].
234 in GHC.Tc.Gen.Head
235
236 2. Use tcInferAppHead to infer the type of the function,
237 as an (uninstantiated) TcSigmaType
238 There are special cases for
239 HsVar, HsRecSel, and ExprWithTySig
240 Otherwise, delegate back to tcExpr, which
241 infers an (instantiated) TcRhoType
242
243 3. Use tcInstFun to instantiate the function, Quick-Looking as we go.
244 This implements the |-inst judgement in Fig 4, plus the
245 modification in Fig 5, of the QL paper:
246 "A quick look at impredicativity" (ICFP'20).
247
248 In tcInstFun we take a quick look at value arguments, using
249 quickLookArg. See Note [Quick Look at value arguments].
250
251 4. Use quickLookResultType to take a quick look at the result type,
252 when in checking mode. This is the shaded part of APP-Downarrow
253 in Fig 5.
254
255 5. Use unifyResultType to match up the result type of the call
256 with that expected by the context. See Note [Unify with
257 expected type before typechecking arguments]
258
259 6. Use tcValArgs to typecheck the value arguments
260
261 7. After a gruesome special case for tagToEnum, rebuild the result.
262
263
264 Some cases that /won't/ work:
265
266 1. Consider this (which uses visible type application):
267
268 (let { f :: forall a. a -> a; f x = x } in f) @Int
269
270 Since 'let' is not among the special cases for tcInferAppHead,
271 we'll delegate back to tcExpr, which will instantiate f's type
272 and the type application to @Int will fail. Too bad!
273
274 Note [Quick Look for particular Ids]
275 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
276 We switch on Quick Look (regardless of -XImpredicativeTypes) for certain
277 particular Ids:
278
279 * ($): For a long time GHC has had a special typing rule for ($), that
280 allows it to type (runST $ foo), which requires impredicative instantiation
281 of ($), without language flags. It's a bit ad-hoc, but it's been that
282 way for ages. Using quickLookKeys is the only special treatment ($) needs
283 now, which is a lot better.
284
285 * leftSection, rightSection: these are introduced by the expansion step in
286 the renamer (Note [Handling overloaded and rebindable constructs] in
287 GHC.Rename.Expr), and we want them to be instantiated impredicatively
288 so that (f `op`), say, will work OK even if `f` is higher rank.
289
290 Note [Unify with expected type before typechecking arguments]
291 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
292 Consider this (#19364)
293 data Pair a b = Pair a b
294 baz :: MkPair Int Bool
295 baz = MkPair "yes" "no"
296
297 We instantiate MkPair with `alpha`, `beta`, and push its argument
298 types (`alpha` and `beta`) into the arguments ("yes" and "no").
299 But if we first unify the result type (Pair alpha beta) with the expected
300 type (Pair Int Bool) we will push the much more informative types
301 `Int` and `Bool` into the arguments. This makes a difference:
302
303 Unify result type /after/ typechecking the args
304 • Couldn't match type ‘[Char]’ with ‘Bool’
305 Expected type: Pair Foo Bar
306 Actual type: Pair [Char] [Char]
307 • In the expression: Pair "yes" "no"
308
309 Unify result type /before/ typechecking the args
310 • Couldn't match type ‘[Char]’ with ‘Bool’
311 Expected: Foo
312 Actual: String
313 • In the first argument of ‘Pair’, namely ‘"yes"’
314
315 The latter is much better. That is why we call unifyExpectedType
316 before tcValArgs.
317 -}
318
319 tcApp :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
320 -- See Note [tcApp: typechecking applications]
321 tcApp rn_expr exp_res_ty
322 | (fun@(rn_fun, fun_ctxt), rn_args) <- splitHsApps rn_expr
323 = do { (tc_fun, fun_sigma) <- tcInferAppHead fun rn_args
324
325 -- Instantiate
326 ; do_ql <- wantQuickLook rn_fun
327 ; (delta, inst_args, app_res_rho) <- tcInstFun do_ql True fun fun_sigma rn_args
328
329 -- Check for representation polymorphism in the case that
330 -- the head of the application is a primop or data constructor
331 -- which has argument types that are representation-polymorphic.
332 -- This amounts to checking that the leftover argument types,
333 -- up until the arity, are not representation-polymorphic,
334 -- so that we can perform eta-expansion later without introducing
335 -- representation-polymorphic binders.
336 --
337 -- See Note [Checking for representation-polymorphic built-ins]
338 ; traceTc "tcApp FRR" $
339 vcat
340 [ text "tc_fun =" <+> ppr tc_fun
341 , text "inst_args =" <+> ppr inst_args
342 , text "app_res_rho =" <+> ppr app_res_rho ]
343 ; hasFixedRuntimeRep_remainingValArgs inst_args app_res_rho tc_fun
344
345 -- Quick look at result
346 ; app_res_rho <- if do_ql
347 then quickLookResultType delta app_res_rho exp_res_ty
348 else return app_res_rho
349
350 -- Unify with expected type from the context
351 -- See Note [Unify with expected type before typechecking arguments]
352 --
353 -- perhaps_add_res_ty_ctxt: Inside an expansion, the addFunResCtxt stuff is
354 -- more confusing than helpful because the function at the head isn't in
355 -- the source program; it was added by the renamer. See
356 -- Note [Handling overloaded and rebindable constructs] in GHC.Rename.Expr
357 ; let perhaps_add_res_ty_ctxt thing_inside
358 | insideExpansion fun_ctxt
359 = thing_inside
360 | otherwise
361 = addFunResCtxt rn_fun rn_args app_res_rho exp_res_ty $
362 thing_inside
363
364 ; res_co <- perhaps_add_res_ty_ctxt $
365 unifyExpectedType rn_expr app_res_rho exp_res_ty
366
367 ; whenDOptM Opt_D_dump_tc_trace $
368 do { inst_args <- mapM zonkArg inst_args -- Only when tracing
369 ; traceTc "tcApp" (vcat [ text "rn_fun" <+> ppr rn_fun
370 , text "inst_args" <+> brackets (pprWithCommas pprHsExprArgTc inst_args)
371 , text "do_ql: " <+> ppr do_ql
372 , text "fun_sigma: " <+> ppr fun_sigma
373 , text "delta: " <+> ppr delta
374 , text "app_res_rho:" <+> ppr app_res_rho
375 , text "exp_res_ty:" <+> ppr exp_res_ty
376 , text "rn_expr:" <+> ppr rn_expr ]) }
377
378 -- Typecheck the value arguments
379 ; tc_args <- tcValArgs do_ql inst_args
380
381 -- Reconstruct, with a special cases for tagToEnum#.
382 ; tc_expr <-
383 if isTagToEnum rn_fun
384 then tcTagToEnum tc_fun fun_ctxt tc_args app_res_rho
385 else do return (rebuildHsApps tc_fun fun_ctxt tc_args)
386
387 -- Wrap the result
388 ; return (mkHsWrapCo res_co tc_expr) }
389
390 {-
391 Note [Checking for representation-polymorphic built-ins]
392 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
393 We cannot have representation-polymorphic or levity-polymorphic
394 function arguments. See Note [Representation polymorphism invariants]
395 in GHC.Core. That is checked by the calls to `hasFixedRuntimeRep ` in
396 `tcEValArg`.
397
398 But some /built-in/ functions are representation-polymorphic. Users
399 can't define such Ids; they are all GHC built-ins or data
400 constructors. Specifically they are:
401
402 1. A few wired-in Ids like unsafeCoerce#, with compulsory unfoldings.
403 2. Primops, such as raise#
404 3. Newtype constructors with `UnliftedNewtypes` that have
405 a representation-polymorphic argument.
406 4. Representation-polymorphic data constructors: unboxed tuples
407 and unboxed sums.
408
409 For (1) consider
410 badId :: forall r (a :: TYPE r). a -> a
411 badId = unsafeCoerce# @r @r @a @a
412
413 The wired-in function
414 unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
415 (a :: TYPE r1) (b :: TYPE r2).
416 a -> b
417 has a convenient but representation-polymorphic type. It has no
418 binding; instead it has a compulsory unfolding, after which we
419 would have
420 badId = /\r /\(a :: TYPE r). \(x::a). ...body of unsafeCorece#...
421 And this is no good because of that rep-poly \(x::a). So we want
422 to reject this.
423
424 On the other hand
425 goodId :: forall (a :: Type). a -> a
426 goodId = unsafeCoerce# @LiftedRep @LiftedRep @a @a
427
428 is absolutely fine, because after we inline the unfolding, the \(x::a)
429 is representation-monomorphic.
430
431 Test cases: T14561, RepPolyWrappedVar2.
432
433 For primops (2) the situation is similar; they are eta-expanded in
434 CorePrep to be saturated, and that eta-expansion must not add a
435 representation-polymorphic lambda.
436
437 Test cases: T14561b, RepPolyWrappedVar, UnliftedNewtypesCoerceFail.
438
439 For (3), consider a representation-polymorphic newtype with
440 UnliftedNewtypes:
441
442 type Id :: forall r. TYPE r -> TYPE r
443 newtype Id a where { MkId :: a }
444
445 bad :: forall r (a :: TYPE r). a -> Id a
446 bad = MkId @r @a -- Want to reject
447
448 good :: forall (a :: Type). a -> Id a
449 good = MkId @LiftedRep @a -- Want to accept
450
451 Test cases: T18481, UnliftedNewtypesLevityBinder
452
453 So these three cases need special treatment. We add a special case
454 in tcApp to check whether an application of an Id has any remaining
455 representation-polymorphic arguments, after instantiation and application
456 of previous arguments. This is achieved by the hasFixedRuntimeRep_remainingValArgs
457 function, which computes the types of the remaining value arguments, and checks
458 that each of these have a fixed runtime representation using hasFixedRuntimeRep.
459
460 Wrinkles
461
462 * Because of Note [Typechecking data constructors] in GHC.Tc.Gen.Head,
463 we desugar a representation-polymorphic data constructor application
464 like this:
465 (/\(r :: RuntimeRep) (a :: TYPE r) \(x::a). K r a x) @LiftedRep Int 4
466 That is, a rep-poly lambda applied to arguments that instantiate it in
467 a rep-mono way. It's a bit like a compulsory unfolding that has been
468 inlined, but not yet beta-reduced.
469
470 Because we want to accept this, we switch off Lint's representation
471 polymorphism checks when Lint checks the output of the desugarer;
472 see the lf_check_fixed_repy flag in GHC.Core.Lint.lintCoreBindings.
473
474 * Arity. We don't want to check for arguments past the
475 arity of the function. For example
476
477 raise# :: forall {r :: RuntimeRep} (a :: Type) (b :: TYPE r). a -> b
478
479 has arity 1, so an instantiation such as:
480
481 foo :: forall w r (z :: TYPE r). w -> z -> z
482 foo = raise# @w @(z -> z)
483
484 is unproblematic. This means we must take care not to perform a
485 representation-polymorphism check on `z`.
486
487 To achieve this, we consult the arity of the 'Id' which is the head
488 of the application (or just use 1 for a newtype constructor),
489 and keep track of how many value-level arguments we have seen,
490 to ensure we stop checking once we reach the arity.
491 This is slightly complicated by the need to include both visible
492 and invisible arguments, as the arity counts both:
493 see GHC.Tc.Gen.Head.countVisAndInvisValArgs.
494
495 Test cases: T20330{a,b}
496
497 -}
498
499 -- | Check for representation-polymorphism in the remaining argument types
500 -- of a variable or data constructor, after it has been instantiated and applied to some arguments.
501 --
502 -- See Note [Checking for representation-polymorphic built-ins]
503 hasFixedRuntimeRep_remainingValArgs :: [HsExprArg 'TcpInst] -> TcRhoType -> HsExpr GhcTc -> TcM ()
504 hasFixedRuntimeRep_remainingValArgs applied_args app_res_rho = \case
505
506 HsVar _ (L _ fun_id)
507
508 -- (1): unsafeCoerce#
509 -- 'unsafeCoerce#' is peculiar: it is patched in manually as per
510 -- Note [Wiring in unsafeCoerce#] in GHC.HsToCore.
511 -- Unfortunately, even though its arity is set to 1 in GHC.HsToCore.mkUnsafeCoercePrimPair,
512 -- at this stage, if we query idArity, we get 0. This is because
513 -- we end up looking at the non-patched version of unsafeCoerce#
514 -- defined in Unsafe.Coerce, and that one indeed has arity 0.
515 --
516 -- We thus manually specify the correct arity of 1 here.
517 | idName fun_id == unsafeCoercePrimName
518 -> check_thing fun_id 1 (FRRNoBindingResArg fun_id)
519
520 -- (2): primops and other wired-in representation-polymorphic functions,
521 -- such as 'rightSection', 'oneShot', etc; see bindings with Compulsory unfoldings
522 -- in GHC.Types.Id.Make
523 | isWiredInName (idName fun_id) && hasNoBinding fun_id
524 -> check_thing fun_id (idArity fun_id) (FRRNoBindingResArg fun_id)
525 -- NB: idArity consults the IdInfo of the Id. This can be a problem
526 -- in the presence of hs-boot files, as we might not have finished
527 -- typechecking; inspecting the IdInfo at this point can cause
528 -- strange Core Lint errors (see #20447).
529 -- We avoid this entirely by only checking wired-in names,
530 -- as those are the only ones this check is applicable to anyway.
531
532
533 XExpr (ConLikeTc (RealDataCon con) _ _)
534 -- (3): Representation-polymorphic newtype constructors.
535 | isNewDataCon con
536 -- (4): Unboxed tuples and unboxed sums
537 || isUnboxedTupleDataCon con
538 || isUnboxedSumDataCon con
539 -> check_thing con (dataConRepArity con) (FRRDataConArg con)
540
541 _ -> return ()
542
543 where
544 nb_applied_vis_val_args :: Int
545 nb_applied_vis_val_args = count isHsValArg applied_args
546
547 nb_applied_val_args :: Int
548 nb_applied_val_args = countVisAndInvisValArgs applied_args
549
550 arg_tys :: [TyCoBinder]
551 arg_tys = fst $ splitPiTys app_res_rho
552 -- We do not need to zonk app_res_rho first, because the number of arrows
553 -- in the (possibly instantiated) inferred type of the function will
554 -- be at least the arity of the function.
555
556 check_thing :: Outputable thing => thing -> Arity -> (Int -> FRROrigin) -> TcM ()
557 check_thing thing arity mk_frr_orig = do
558 traceTc "tcApp remainingValArgs check_thing" (debug_msg thing arity)
559 go (nb_applied_vis_val_args + 1) (nb_applied_val_args + 1) arg_tys
560 where
561 go :: Int -- ^ visible value argument index
562 -- (only used to report the argument position in error messages)
563 -> Int -- ^ value argument index
564 -- used to count up to the arity to ensure we don't check too many argument types
565 -> [TyCoBinder]
566 -> TcM ()
567 go _ i_val _
568 | i_val > arity
569 = return ()
570 go _ _ []
571 -- Should never happen: it would mean that the arity is higher
572 -- than the number of arguments apparent from the type
573 = pprPanic "hasFixedRuntimeRep_remainingValArgs" (debug_msg thing arity)
574 go i_visval !i_val (Anon af (Scaled _ arg_ty) : tys)
575 = case af of
576 InvisArg ->
577 go i_visval (i_val + 1) tys
578 VisArg -> do
579 _concrete_ev <- hasFixedRuntimeRep (mk_frr_orig i_visval) arg_ty
580 go (i_visval + 1) (i_val + 1) tys
581 go i_visval i_val (_: tys)
582 = go i_visval i_val tys
583
584 -- A message containing all the relevant info, in case this functions
585 -- needs to be debugged again at some point.
586 debug_msg :: Outputable thing => thing -> Arity -> SDoc
587 debug_msg thing arity =
588 vcat
589 [ text "thing =" <+> ppr thing
590 , text "arity =" <+> ppr arity
591 , text "applied_args =" <+> ppr applied_args
592 , text "nb_applied_vis_val_args =" <+> ppr nb_applied_vis_val_args
593 , text "nb_applied_val_args =" <+> ppr nb_applied_val_args
594 , text "arg_tys =" <+> ppr arg_tys ]
595
596 --------------------
597 wantQuickLook :: HsExpr GhcRn -> TcM Bool
598 -- GHC switches on impredicativity all the time for ($)
599 wantQuickLook (HsVar _ (L _ f))
600 | getUnique f `elem` quickLookKeys = return True
601 wantQuickLook _ = xoptM LangExt.ImpredicativeTypes
602
603 quickLookKeys :: [Unique]
604 -- See Note [Quick Look for particular Ids]
605 quickLookKeys = [dollarIdKey, leftSectionKey, rightSectionKey]
606
607 zonkQuickLook :: Bool -> TcType -> TcM TcType
608 -- After all Quick Look unifications are done, zonk to ensure that all
609 -- instantiation variables are substituted away
610 --
611 -- So far as the paper is concerned, this step applies
612 -- the poly-substitution Theta, learned by QL, so that we
613 -- "see" the polymorphism in that type
614 --
615 -- In implementation terms this ensures that no unification variable
616 -- linger on that have been filled in with a polytype
617 zonkQuickLook do_ql ty
618 | do_ql = zonkTcType ty
619 | otherwise = return ty
620
621 -- zonkArg is used *only* during debug-tracing, to make it easier to
622 -- see what is going on. For that reason, it is not a full zonk: add
623 -- more if you need it.
624 zonkArg :: HsExprArg 'TcpInst -> TcM (HsExprArg 'TcpInst)
625 zonkArg eva@(EValArg { eva_arg_ty = Scaled m ty })
626 = do { ty' <- zonkTcType ty
627 ; return (eva { eva_arg_ty = Scaled m ty' }) }
628 zonkArg arg = return arg
629
630
631
632 ----------------
633 tcValArgs :: Bool -- Quick-look on?
634 -> [HsExprArg 'TcpInst] -- Actual argument
635 -> TcM [HsExprArg 'TcpTc] -- Resulting argument
636 tcValArgs do_ql args
637 = mapM tc_arg args
638 where
639 tc_arg :: HsExprArg 'TcpInst -> TcM (HsExprArg 'TcpTc)
640 tc_arg (EPrag l p) = return (EPrag l (tcExprPrag p))
641 tc_arg (EWrap w) = return (EWrap w)
642 tc_arg (ETypeArg l hs_ty ty) = return (ETypeArg l hs_ty ty)
643
644 tc_arg eva@(EValArg { eva_arg = arg, eva_arg_ty = Scaled mult arg_ty
645 , eva_ctxt = ctxt })
646 = do { -- Crucial step: expose QL results before checking arg_ty
647 -- So far as the paper is concerned, this step applies
648 -- the poly-substitution Theta, learned by QL, so that we
649 -- "see" the polymorphism in that argument type. E.g.
650 -- (:) e ids, where ids :: [forall a. a->a]
651 -- (:) :: forall p. p->[p]->[p]
652 -- Then Theta = [p :-> forall a. a->a], and we want
653 -- to check 'e' with expected type (forall a. a->a)
654 -- See Note [Instantiation variables are short lived]
655 arg_ty <- zonkQuickLook do_ql arg_ty
656
657 -- Now check the argument
658 ; arg' <- tcScalingUsage mult $
659 do { traceTc "tcEValArg" $
660 vcat [ ppr ctxt
661 , text "arg type:" <+> ppr arg_ty
662 , text "arg:" <+> ppr arg ]
663 ; tcEValArg ctxt arg arg_ty }
664
665 ; return (eva { eva_arg = ValArg arg'
666 , eva_arg_ty = Scaled mult arg_ty }) }
667
668 tcEValArg :: AppCtxt -> EValArg 'TcpInst -> TcSigmaType -> TcM (LHsExpr GhcTc)
669 -- Typecheck one value argument of a function call
670 tcEValArg ctxt (ValArg larg@(L arg_loc arg)) exp_arg_sigma
671 = addArgCtxt ctxt larg $
672 do { arg' <- tcPolyExpr arg (mkCheckExpType exp_arg_sigma)
673 ; _concrete_ev <- hasFixedRuntimeRep (FRRApp arg) exp_arg_sigma
674 ; return (L arg_loc arg') }
675
676 tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc arg)
677 , va_fun = (inner_fun, fun_ctxt)
678 , va_args = inner_args
679 , va_ty = app_res_rho }) exp_arg_sigma
680 = addArgCtxt ctxt larg $
681 do { traceTc "tcEValArgQL {" (vcat [ ppr inner_fun <+> ppr inner_args ])
682 ; tc_args <- tcValArgs True inner_args
683 ; co <- unifyType Nothing app_res_rho exp_arg_sigma
684 ; _concrete_ev <- hasFixedRuntimeRep (FRRApp arg) exp_arg_sigma
685 ; traceTc "tcEValArg }" empty
686 ; return (L arg_loc $ mkHsWrapCo co $
687 rebuildHsApps inner_fun fun_ctxt tc_args) }
688
689 {- *********************************************************************
690 * *
691 Instantiating the call
692 * *
693 ********************************************************************* -}
694
695 type Delta = TcTyVarSet -- Set of instantiation variables,
696 -- written \kappa in the QL paper
697 -- Just a set of ordinary unification variables,
698 -- but ones that QL may fill in with polytypes
699
700 tcInstFun :: Bool -- True <=> Do quick-look
701 -> Bool -- False <=> Instantiate only /inferred/ variables at the end
702 -- so may return a sigma-typex
703 -- True <=> Instantiate all type variables at the end:
704 -- return a rho-type
705 -- The /only/ call site that passes in False is the one
706 -- in tcInferSigma, which is used only to implement :type
707 -- Otherwise we do eager instantiation; in Fig 5 of the paper
708 -- |-inst returns a rho-type
709 -> (HsExpr GhcRn, AppCtxt) -- Error messages only
710 -> TcSigmaType -> [HsExprArg 'TcpRn]
711 -> TcM ( Delta
712 , [HsExprArg 'TcpInst]
713 , TcSigmaType )
714 -- This function implements the |-inst judgement in Fig 4, plus the
715 -- modification in Fig 5, of the QL paper:
716 -- "A quick look at impredicativity" (ICFP'20).
717 tcInstFun do_ql inst_final (rn_fun, fun_ctxt) fun_sigma rn_args
718 = do { traceTc "tcInstFun" (vcat [ ppr rn_fun, ppr fun_sigma
719 , text "args:" <+> ppr rn_args
720 , text "do_ql" <+> ppr do_ql ])
721 ; go emptyVarSet [] [] fun_sigma rn_args }
722 where
723 fun_loc = appCtxtLoc fun_ctxt
724 fun_orig = exprCtOrigin (case fun_ctxt of
725 VAExpansion e _ -> e
726 VACall e _ _ -> e)
727 set_fun_ctxt thing_inside
728 | not (isGoodSrcSpan fun_loc) -- noSrcSpan => no arguments
729 = thing_inside -- => context is already set
730 | otherwise
731 = setSrcSpan fun_loc $
732 case fun_ctxt of
733 VAExpansion orig _ -> addExprCtxt orig thing_inside
734 VACall {} -> thing_inside
735
736 herald = sep [ text "The function" <+> quotes (ppr rn_fun)
737 , text "is applied to"]
738
739 -- Count value args only when complaining about a function
740 -- applied to too many value args
741 -- See Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify.
742 n_val_args = count isHsValArg rn_args
743
744 fun_is_out_of_scope -- See Note [VTA for out-of-scope functions]
745 = case rn_fun of
746 HsUnboundVar {} -> True
747 _ -> False
748
749 inst_all :: ArgFlag -> Bool
750 inst_all (Invisible {}) = True
751 inst_all Required = False
752
753 inst_inferred :: ArgFlag -> Bool
754 inst_inferred (Invisible InferredSpec) = True
755 inst_inferred (Invisible SpecifiedSpec) = False
756 inst_inferred Required = False
757
758 inst_fun :: [HsExprArg 'TcpRn] -> ArgFlag -> Bool
759 inst_fun [] | inst_final = inst_all
760 | otherwise = inst_inferred
761 inst_fun (EValArg {} : _) = inst_all
762 inst_fun _ = inst_inferred
763
764 -----------
765 go, go1 :: Delta
766 -> [HsExprArg 'TcpInst] -- Accumulator, reversed
767 -> [Scaled TcSigmaType] -- Value args to which applied so far
768 -> TcSigmaType -> [HsExprArg 'TcpRn]
769 -> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
770
771 -- go: If fun_ty=kappa, look it up in Theta
772 go delta acc so_far fun_ty args
773 | Just kappa <- tcGetTyVar_maybe fun_ty
774 , kappa `elemVarSet` delta
775 = do { cts <- readMetaTyVar kappa
776 ; case cts of
777 Indirect fun_ty' -> go delta acc so_far fun_ty' args
778 Flexi -> go1 delta acc so_far fun_ty args }
779 | otherwise
780 = go1 delta acc so_far fun_ty args
781
782 -- go1: fun_ty is not filled-in instantiation variable
783 -- ('go' dealt with that case)
784
785 -- Rule IALL from Fig 4 of the QL paper
786 -- c.f. GHC.Tc.Utils.Instantiate.topInstantiate
787 go1 delta acc so_far fun_ty args
788 | (tvs, body1) <- tcSplitSomeForAllTyVars (inst_fun args) fun_ty
789 , (theta, body2) <- tcSplitPhiTy body1
790 , not (null tvs && null theta)
791 = do { (inst_tvs, wrap, fun_rho) <- set_fun_ctxt $
792 instantiateSigma fun_orig tvs theta body2
793 -- set_fun_ctxt: important for the class constraints
794 -- that may be emitted from instantiating fun_sigma
795 ; go (delta `extendVarSetList` inst_tvs)
796 (addArgWrap wrap acc) so_far fun_rho args }
797 -- Going around again means we deal easily with
798 -- nested forall a. Eq a => forall b. Show b => blah
799
800 -- Rule IRESULT from Fig 4 of the QL paper
801 go1 delta acc _ fun_ty []
802 = do { traceTc "tcInstFun:ret" (ppr fun_ty)
803 ; return (delta, reverse acc, fun_ty) }
804
805 go1 delta acc so_far fun_ty (EWrap w : args)
806 = go1 delta (EWrap w : acc) so_far fun_ty args
807
808 go1 delta acc so_far fun_ty (EPrag sp prag : args)
809 = go1 delta (EPrag sp prag : acc) so_far fun_ty args
810
811 -- Rule ITYARG from Fig 4 of the QL paper
812 go1 delta acc so_far fun_ty ( ETypeArg { eva_ctxt = ctxt, eva_hs_ty = hs_ty }
813 : rest_args )
814 | fun_is_out_of_scope -- See Note [VTA for out-of-scope functions]
815 = go delta acc so_far fun_ty rest_args
816
817 | otherwise
818 = do { (ty_arg, inst_ty) <- tcVTA fun_ty hs_ty
819 ; let arg' = ETypeArg { eva_ctxt = ctxt, eva_hs_ty = hs_ty, eva_ty = ty_arg }
820 ; go delta (arg' : acc) so_far inst_ty rest_args }
821
822 -- Rule IVAR from Fig 4 of the QL paper:
823 go1 delta acc so_far fun_ty args@(EValArg {} : _)
824 | Just kappa <- tcGetTyVar_maybe fun_ty
825 , kappa `elemVarSet` delta
826 = -- Function type was of form f :: forall a b. t1 -> t2 -> b
827 -- with 'b', one of the quantified type variables, in the corner
828 -- but the call applies it to three or more value args.
829 -- Suppose b is instantiated by kappa. Then we want to make fresh
830 -- instantiation variables nu1, nu2, and set kappa := nu1 -> nu2
831 --
832 -- In principle what is happening here is not unlike matchActualFunTysRho
833 -- but there are many small differences:
834 -- - We know that the function type in unfilled meta-tyvar
835 -- matchActualFunTysRho is much more general, has a loop, etc.
836 -- - We must be sure to actually update the variable right now,
837 -- not defer in any way, because this is a QL instantiation variable.
838 -- - We need the freshly allocated unification variables, to extend
839 -- delta with.
840 -- It's easier just to do the job directly here.
841 do { let valArgsCount = countLeadingValArgs args
842 ; arg_nus <- replicateM valArgsCount newOpenFlexiTyVar
843 -- We need variables for multiplicity (#18731)
844 -- Otherwise, 'undefined x' wouldn't be linear in x
845 ; mults <- replicateM valArgsCount (newFlexiTyVarTy multiplicityTy)
846 ; res_nu <- newOpenFlexiTyVar
847 ; kind_co <- unifyKind Nothing liftedTypeKind (tyVarKind kappa)
848 ; let delta' = delta `extendVarSetList` (res_nu:arg_nus)
849 arg_tys = mkTyVarTys arg_nus
850 res_ty = mkTyVarTy res_nu
851 fun_ty' = mkVisFunTys (zipWithEqual "tcInstFun" mkScaled mults arg_tys) res_ty
852 co_wrap = mkWpCastN (mkTcGReflLeftCo Nominal fun_ty' kind_co)
853 acc' = addArgWrap co_wrap acc
854 -- Suppose kappa :: kk
855 -- Then fun_ty :: kk, fun_ty' :: Type, kind_co :: Type ~ kk
856 -- co_wrap :: (fun_ty' |> kind_co) ~ fun_ty'
857 ; writeMetaTyVar kappa (mkCastTy fun_ty' kind_co)
858 -- kappa is uninstantiated ('go' already checked that)
859 ; go delta' acc' so_far fun_ty' args }
860
861 -- Rule IARG from Fig 4 of the QL paper:
862 go1 delta acc so_far fun_ty
863 (eva@(EValArg { eva_arg = ValArg arg, eva_ctxt = ctxt }) : rest_args)
864 = do { (wrap, arg_ty, res_ty) <- matchActualFunTySigma herald
865 (Just (ppr rn_fun))
866 (n_val_args, so_far) fun_ty
867 ; (delta', arg') <- if do_ql
868 then addArgCtxt ctxt arg $
869 -- Context needed for constraints
870 -- generated by calls in arg
871 quickLookArg delta arg arg_ty
872 else return (delta, ValArg arg)
873 ; let acc' = eva { eva_arg = arg', eva_arg_ty = arg_ty }
874 : addArgWrap wrap acc
875 ; go delta' acc' (arg_ty:so_far) res_ty rest_args }
876
877
878 addArgCtxt :: AppCtxt -> LHsExpr GhcRn
879 -> TcM a -> TcM a
880 -- Adds a "In the third argument of f, namely blah"
881 -- context, unless we are in generated code, in which case
882 -- use "In the expression: arg"
883 ---See Note [Rebindable syntax and HsExpansion] in GHC.Hs.Expr
884 addArgCtxt (VACall fun arg_no _) (L arg_loc arg) thing_inside
885 = setSrcSpanA arg_loc $
886 addErrCtxt (funAppCtxt fun arg arg_no) $
887 thing_inside
888
889 addArgCtxt (VAExpansion {}) (L arg_loc arg) thing_inside
890 = setSrcSpanA arg_loc $
891 addExprCtxt arg $ -- Auto-suppressed if arg_loc is generated
892 thing_inside
893
894 {- *********************************************************************
895 * *
896 Visible type application
897 * *
898 ********************************************************************* -}
899
900 tcVTA :: TcType -- Function type
901 -> LHsWcType GhcRn -- Argument type
902 -> TcM (TcType, TcType)
903 -- Deal with a visible type application
904 -- The function type has already had its Inferred binders instantiated
905 tcVTA fun_ty hs_ty
906 | Just (tvb, inner_ty) <- tcSplitForAllTyVarBinder_maybe fun_ty
907 , binderArgFlag tvb == Specified
908 -- It really can't be Inferred, because we've just
909 -- instantiated those. But, oddly, it might just be Required.
910 -- See Note [Required quantifiers in the type of a term]
911 = do { let tv = binderVar tvb
912 kind = tyVarKind tv
913 ; ty_arg <- tcHsTypeApp hs_ty kind
914
915 ; inner_ty <- zonkTcType inner_ty
916 -- See Note [Visible type application zonk]
917
918 ; let in_scope = mkInScopeSet (tyCoVarsOfTypes [fun_ty, ty_arg])
919 insted_ty = substTyWithInScope in_scope [tv] [ty_arg] inner_ty
920 -- NB: tv and ty_arg have the same kind, so this
921 -- substitution is kind-respecting
922 ; traceTc "VTA" (vcat [ppr tv, debugPprType kind
923 , debugPprType ty_arg
924 , debugPprType (tcTypeKind ty_arg)
925 , debugPprType inner_ty
926 , debugPprType insted_ty ])
927 ; return (ty_arg, insted_ty) }
928
929 | otherwise
930 = do { (_, fun_ty) <- zonkTidyTcType emptyTidyEnv fun_ty
931 ; failWith $ TcRnInvalidTypeApplication fun_ty hs_ty }
932
933 {- Note [Required quantifiers in the type of a term]
934 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
935 Consider (#15859)
936
937 data A k :: k -> Type -- A :: forall k -> k -> Type
938 type KindOf (a :: k) = k -- KindOf :: forall k. k -> Type
939 a = (undefined :: KindOf A) @Int
940
941 With ImpredicativeTypes (thin ice, I know), we instantiate
942 KindOf at type (forall k -> k -> Type), so
943 KindOf A = forall k -> k -> Type
944 whose first argument is Required
945
946 We want to reject this type application to Int, but in earlier
947 GHCs we had an ASSERT that Required could not occur here.
948
949 The ice is thin; c.f. Note [No Required TyCoBinder in terms]
950 in GHC.Core.TyCo.Rep.
951
952 Note [VTA for out-of-scope functions]
953 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
954 Suppose 'wurble' is not in scope, and we have
955 (wurble @Int @Bool True 'x')
956
957 Then the renamer will make (HsUnboundVar "wurble) for 'wurble',
958 and the typechecker will typecheck it with tcUnboundId, giving it
959 a type 'alpha', and emitting a deferred Hole constraint, to
960 be reported later.
961
962 But then comes the visible type application. If we do nothing, we'll
963 generate an immediate failure (in tc_app_err), saying that a function
964 of type 'alpha' can't be applied to Bool. That's insane! And indeed
965 users complain bitterly (#13834, #17150.)
966
967 The right error is the Hole, which has /already/ been emitted by
968 tcUnboundId. It later reports 'wurble' as out of scope, and tries to
969 give its type.
970
971 Fortunately in tcInstFun we still have access to the function, so we
972 can check if it is a HsUnboundVar. We use this info to simply skip
973 over any visible type arguments. We've already inferred the type of
974 the function (in tcInferAppHead), so we'll /already/ have emitted a
975 Hole constraint; failing preserves that constraint.
976
977 We do /not/ want to fail altogether in this case (via failM) because
978 that may abandon an entire instance decl, which (in the presence of
979 -fdefer-type-errors) leads to leading to #17792.
980
981 Downside; the typechecked term has lost its visible type arguments; we
982 don't even kind-check them. But let's jump that bridge if we come to
983 it. Meanwhile, let's not crash!
984
985
986 Note [Visible type application zonk]
987 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
988 * Substitutions should be kind-preserving, so we need kind(tv) = kind(ty_arg).
989
990 * tcHsTypeApp only guarantees that
991 - ty_arg is zonked
992 - kind(zonk(tv)) = kind(ty_arg)
993 (checkExpectedKind zonks as it goes).
994
995 So we must zonk inner_ty as well, to guarantee consistency between zonk(tv)
996 and inner_ty. Otherwise we can build an ill-kinded type. An example was #14158,
997 where we had:
998 id :: forall k. forall (cat :: k -> k -> *). forall (a :: k). cat a a
999 and we had the visible type application
1000 id @(->)
1001
1002 * We instantiated k := kappa, yielding
1003 forall (cat :: kappa -> kappa -> *). forall (a :: kappa). cat a a
1004 * Then we called tcHsTypeApp (->) with expected kind (kappa -> kappa -> *).
1005 * That instantiated (->) as ((->) q1 q1), and unified kappa := q1,
1006 Here q1 :: RuntimeRep
1007 * Now we substitute
1008 cat :-> (->) q1 q1 :: TYPE q1 -> TYPE q1 -> *
1009 but we must first zonk the inner_ty to get
1010 forall (a :: TYPE q1). cat a a
1011 so that the result of substitution is well-kinded
1012 Failing to do so led to #14158.
1013
1014 -}
1015
1016 {- *********************************************************************
1017 * *
1018 Quick Look
1019 * *
1020 ********************************************************************* -}
1021
1022 {- Note [Quick Look at value arguments]
1023 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1024 The function quickLookArg implements the "QL argument" judgement of
1025 the QL paper, in Fig 5 of "A quick look at impredicativity" (ICFP 2020),
1026 rather directly.
1027
1028 Wrinkles:
1029
1030 * We avoid zonking, so quickLookArg thereby sees the argument type /before/
1031 the QL substitution Theta is applied to it. So we achieve argument-order
1032 independence for free (see 5.7 in the paper).
1033
1034 * When we quick-look at an argument, we save the work done, by returning
1035 an EValArg with a ValArgQL inside it. (It started life with a ValArg
1036 inside.) The ValArgQL remembers all the work that QL did (notably,
1037 decomposing the argument and instantiating) so that tcValArgs does
1038 not need to repeat it. Rather neat, and remarkably easy.
1039 -}
1040
1041 ----------------
1042 quickLookArg :: Delta
1043 -> LHsExpr GhcRn -- Argument
1044 -> Scaled TcSigmaType -- Type expected by the function
1045 -> TcM (Delta, EValArg 'TcpInst)
1046 -- See Note [Quick Look at value arguments]
1047 --
1048 -- The returned Delta is a superset of the one passed in
1049 -- with added instantiation variables from
1050 -- (a) the call itself
1051 -- (b) the arguments of the call
1052 quickLookArg delta larg (Scaled _ arg_ty)
1053 | isEmptyVarSet delta = skipQuickLook delta larg
1054 | otherwise = go arg_ty
1055 where
1056 guarded = isGuardedTy arg_ty
1057 -- NB: guardedness is computed based on the original,
1058 -- unzonked arg_ty, so we deliberately do not exploit
1059 -- guardedness that emerges a result of QL on earlier args
1060
1061 go arg_ty | not (isRhoTy arg_ty)
1062 = skipQuickLook delta larg
1063
1064 -- This top-level zonk step, which is the reason
1065 -- we need a local 'go' loop, is subtle
1066 -- See Section 9 of the QL paper
1067 | Just kappa <- tcGetTyVar_maybe arg_ty
1068 , kappa `elemVarSet` delta
1069 = do { info <- readMetaTyVar kappa
1070 ; case info of
1071 Indirect arg_ty' -> go arg_ty'
1072 Flexi -> quickLookArg1 guarded delta larg arg_ty }
1073
1074 | otherwise
1075 = quickLookArg1 guarded delta larg arg_ty
1076
1077 isGuardedTy :: TcType -> Bool
1078 isGuardedTy ty
1079 | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
1080 | Just {} <- tcSplitAppTy_maybe ty = True
1081 | otherwise = False
1082
1083 quickLookArg1 :: Bool -> Delta -> LHsExpr GhcRn -> TcSigmaType
1084 -> TcM (Delta, EValArg 'TcpInst)
1085 quickLookArg1 guarded delta larg@(L _ arg) arg_ty
1086 = do { let (fun@(rn_fun, fun_ctxt), rn_args) = splitHsApps arg
1087 ; mb_fun_ty <- tcInferAppHead_maybe rn_fun rn_args
1088 ; traceTc "quickLookArg 1" $
1089 vcat [ text "arg:" <+> ppr arg
1090 , text "head:" <+> ppr rn_fun <+> dcolon <+> ppr mb_fun_ty
1091 , text "args:" <+> ppr rn_args ]
1092
1093 ; case mb_fun_ty of {
1094 Nothing -> -- fun is too complicated
1095 skipQuickLook delta larg ;
1096 Just (tc_fun, fun_sigma) ->
1097
1098 do { let no_free_kappas = findNoQuantVars fun_sigma rn_args
1099 ; traceTc "quickLookArg 2" $
1100 vcat [ text "no_free_kappas:" <+> ppr no_free_kappas
1101 , text "guarded:" <+> ppr guarded
1102 , text "tc_fun:" <+> ppr tc_fun
1103 , text "fun_sigma:" <+> ppr fun_sigma ]
1104 ; if not (guarded || no_free_kappas)
1105 then skipQuickLook delta larg
1106 else
1107 do { do_ql <- wantQuickLook rn_fun
1108 ; (delta_app, inst_args, app_res_rho) <- tcInstFun do_ql True fun fun_sigma rn_args
1109 ; traceTc "quickLookArg 3" $
1110 vcat [ text "arg:" <+> ppr arg
1111 , text "delta:" <+> ppr delta
1112 , text "delta_app:" <+> ppr delta_app
1113 , text "arg_ty:" <+> ppr arg_ty
1114 , text "app_res_rho:" <+> ppr app_res_rho ]
1115
1116 -- Do quick-look unification
1117 -- NB: arg_ty may not be zonked, but that's ok
1118 ; let delta' = delta `unionVarSet` delta_app
1119 ; qlUnify delta' arg_ty app_res_rho
1120
1121 ; let ql_arg = ValArgQL { va_expr = larg
1122 , va_fun = (tc_fun, fun_ctxt)
1123 , va_args = inst_args
1124 , va_ty = app_res_rho }
1125 ; return (delta', ql_arg) } } } }
1126
1127 skipQuickLook :: Delta -> LHsExpr GhcRn -> TcM (Delta, EValArg 'TcpInst)
1128 skipQuickLook delta larg = return (delta, ValArg larg)
1129
1130 ----------------
1131 quickLookResultType :: Delta -> TcRhoType -> ExpRhoType -> TcM TcRhoType
1132 -- This function implements the shaded bit of rule APP-Downarrow in
1133 -- Fig 5 of the QL paper: "A quick look at impredicativity" (ICFP'20).
1134 -- It returns its second argument, but with any variables in Delta
1135 -- substituted out, so no variables in Delta escape
1136
1137 quickLookResultType delta app_res_rho (Check exp_rho)
1138 = -- In checking mode only, do qlUnify with the expected result type
1139 do { unless (isEmptyVarSet delta) $ -- Optimisation only
1140 qlUnify delta app_res_rho exp_rho
1141 ; return app_res_rho }
1142
1143 quickLookResultType _ app_res_rho (Infer {})
1144 = zonkTcType app_res_rho
1145 -- Zonk the result type, to ensure that we substitute out any
1146 -- filled-in instantiation variable before calling
1147 -- unifyExpectedType. In the Check case, this isn't necessary,
1148 -- because unifyExpectedType just drops to tcUnify; but in the
1149 -- Infer case a filled-in instantiation variable (filled in by
1150 -- tcInstFun) might perhaps escape into the constraint
1151 -- generator. The safe thing to do is to zonk any instantiation
1152 -- variables away. See Note [Instantiation variables are short lived]
1153
1154 ---------------------
1155 qlUnify :: Delta -> TcType -> TcType -> TcM ()
1156 -- Unify ty1 with ty2, unifying only variables in delta
1157 qlUnify delta ty1 ty2
1158 = do { traceTc "qlUnify" (ppr delta $$ ppr ty1 $$ ppr ty2)
1159 ; go (emptyVarSet,emptyVarSet) ty1 ty2 }
1160 where
1161 go :: (TyVarSet, TcTyVarSet)
1162 -> TcType -> TcType
1163 -> TcM ()
1164 -- The TyVarSets give the variables bound by enclosing foralls
1165 -- for the corresponding type. Don't unify with these.
1166 go bvs (TyVarTy tv) ty2
1167 | tv `elemVarSet` delta = go_kappa bvs tv ty2
1168
1169 go (bvs1, bvs2) ty1 (TyVarTy tv)
1170 | tv `elemVarSet` delta = go_kappa (bvs2,bvs1) tv ty1
1171
1172 go bvs (CastTy ty1 _) ty2 = go bvs ty1 ty2
1173 go bvs ty1 (CastTy ty2 _) = go bvs ty1 ty2
1174
1175 go _ (TyConApp tc1 []) (TyConApp tc2 [])
1176 | tc1 == tc2 -- See GHC.Tc.Utils.Unify
1177 = return () -- Note [Expanding synonyms during unification]
1178
1179 -- Now, and only now, expand synonyms
1180 go bvs rho1 rho2
1181 | Just rho1 <- tcView rho1 = go bvs rho1 rho2
1182 | Just rho2 <- tcView rho2 = go bvs rho1 rho2
1183
1184 go bvs (TyConApp tc1 tys1) (TyConApp tc2 tys2)
1185 | tc1 == tc2
1186 , not (isTypeFamilyTyCon tc1)
1187 , tys1 `equalLength` tys2
1188 = zipWithM_ (go bvs) tys1 tys2
1189
1190 -- Decompose (arg1 -> res1) ~ (arg2 -> res2)
1191 -- and (c1 => res1) ~ (c2 => res2)
1192 -- But for the latter we only learn instantiation info from t1~t2
1193 -- We look at the multiplicity too, although the chances of getting
1194 -- impredicative instantiation info from there seems...remote.
1195 go bvs (FunTy { ft_af = af1, ft_arg = arg1, ft_res = res1, ft_mult = mult1 })
1196 (FunTy { ft_af = af2, ft_arg = arg2, ft_res = res2, ft_mult = mult2 })
1197 | af1 == af2
1198 = do { when (af1 == VisArg) $
1199 do { go bvs arg1 arg2; go bvs mult1 mult2 }
1200 ; go bvs res1 res2 }
1201
1202 -- ToDo: c.f. Tc.Utils.unify.uType,
1203 -- which does not split FunTy here
1204 -- Also NB tcRepSplitAppTy here, which does not split (c => t)
1205 go bvs (AppTy t1a t1b) ty2
1206 | Just (t2a, t2b) <- tcRepSplitAppTy_maybe ty2
1207 = do { go bvs t1a t2a; go bvs t1b t2b }
1208
1209 go bvs ty1 (AppTy t2a t2b)
1210 | Just (t1a, t1b) <- tcRepSplitAppTy_maybe ty1
1211 = do { go bvs t1a t2a; go bvs t1b t2b }
1212
1213 go (bvs1, bvs2) (ForAllTy bv1 ty1) (ForAllTy bv2 ty2)
1214 = go (bvs1',bvs2') ty1 ty2
1215 where
1216 bvs1' = bvs1 `extendVarSet` binderVar bv1
1217 bvs2' = bvs2 `extendVarSet` binderVar bv2
1218
1219 go _ _ _ = return ()
1220
1221
1222 ----------------
1223 go_kappa bvs kappa ty2
1224 = assertPpr (isMetaTyVar kappa) (ppr kappa) $
1225 do { info <- readMetaTyVar kappa
1226 ; case info of
1227 Indirect ty1 -> go bvs ty1 ty2
1228 Flexi -> do { ty2 <- zonkTcType ty2
1229 ; go_flexi bvs kappa ty2 } }
1230
1231 ----------------
1232 go_flexi (_,bvs2) kappa ty2 -- ty2 is zonked
1233 | -- See Note [Actual unification in qlUnify]
1234 let ty2_tvs = shallowTyCoVarsOfType ty2
1235 , not (ty2_tvs `intersectsVarSet` bvs2)
1236 -- Can't instantiate a delta-varto a forall-bound variable
1237 , Just ty2 <- occCheckExpand [kappa] ty2
1238 -- Passes the occurs check
1239 = do { let ty2_kind = typeKind ty2
1240 kappa_kind = tyVarKind kappa
1241 ; co <- unifyKind (Just (ppr ty2)) ty2_kind kappa_kind
1242 -- unifyKind: see Note [Actual unification in qlUnify]
1243
1244 ; traceTc "qlUnify:update" $
1245 vcat [ hang (ppr kappa <+> dcolon <+> ppr kappa_kind)
1246 2 (text ":=" <+> ppr ty2 <+> dcolon <+> ppr ty2_kind)
1247 , text "co:" <+> ppr co ]
1248 ; writeMetaTyVar kappa (mkCastTy ty2 co) }
1249
1250 | otherwise
1251 = return () -- Occurs-check or forall-bound varialbe
1252
1253
1254 {- Note [Actual unification in qlUnify]
1255 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1256 In qlUnify, if we find (kappa ~ ty), we are going to update kappa := ty.
1257 That is the entire point of qlUnify! Wrinkles:
1258
1259 * We must not unify with anything bound by an enclosing forall; e.g.
1260 (forall a. kappa -> Int) ~ forall a. a -> Int)
1261 That's tracked by the 'bvs' arg of 'go'.
1262
1263 * We must not make an occurs-check; we use occCheckExpand for that.
1264
1265 * checkTypeEq also checks for various other things, including
1266 - foralls, and predicate types (which we want to allow here)
1267 - type families (relates to a very specific and exotic performance
1268 question, that is unlikely to bite here)
1269 - blocking coercion holes
1270 After some thought we believe that none of these are relevant
1271 here
1272
1273 * What if kappa and ty have different kinds? We solve that problem by
1274 calling unifyKind, producing a coercion perhaps emitting some deferred
1275 equality constraints. That is /different/ from the approach we use in
1276 the main constraint solver for herterogeneous equalities; see Note
1277 [Equalities with incompatible kinds] in Solver.Canonical
1278
1279 Why different? Because:
1280 - We can't use qlUnify to solve the kind constraint because qlUnify
1281 won't unify ordinary (non-instantiation) unification variables.
1282 (It would have to worry about lots of things like untouchability
1283 if it did.)
1284 - qlUnify can't give up if the kinds look un-equal because that would
1285 mean that it might succeed some times (when the eager unifier
1286 has already unified those kinds) but not others -- order
1287 dependence.
1288 - We can't use the ordinary unifier/constraint solver instead,
1289 because it doesn't unify polykinds, and has all kinds of other
1290 magic. qlUnify is very focused.
1291
1292 TL;DR Calling unifyKind seems like the lesser evil.
1293 -}
1294
1295 {- *********************************************************************
1296 * *
1297 Guardedness
1298 * *
1299 ********************************************************************* -}
1300
1301 findNoQuantVars :: TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
1302 -- True <=> there are no free quantified variables
1303 -- in the result of the call
1304 -- E.g. in the call (f e1 e2), if
1305 -- f :: forall a b. a -> b -> Int return True
1306 -- f :: forall a b. a -> b -> b return False (b is free)
1307 findNoQuantVars fun_ty args
1308 = go emptyVarSet fun_ty args
1309 where
1310 need_instantiation [] = True
1311 need_instantiation (EValArg {} : _) = True
1312 need_instantiation _ = False
1313
1314 go :: TyVarSet -> TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
1315 go bvs fun_ty args
1316 | need_instantiation args
1317 , (tvs, theta, rho) <- tcSplitSigmaTy fun_ty
1318 , not (null tvs && null theta)
1319 = go (bvs `extendVarSetList` tvs) rho args
1320
1321 go bvs fun_ty [] = tyCoVarsOfType fun_ty `disjointVarSet` bvs
1322
1323 go bvs fun_ty (EWrap {} : args) = go bvs fun_ty args
1324 go bvs fun_ty (EPrag {} : args) = go bvs fun_ty args
1325
1326 go bvs fun_ty args@(ETypeArg {} : rest_args)
1327 | (tvs, body1) <- tcSplitSomeForAllTyVars (== Inferred) fun_ty
1328 , (theta, body2) <- tcSplitPhiTy body1
1329 , not (null tvs && null theta)
1330 = go (bvs `extendVarSetList` tvs) body2 args
1331 | Just (_tv, res_ty) <- tcSplitForAllTyVarBinder_maybe fun_ty
1332 = go bvs res_ty rest_args
1333 | otherwise
1334 = False -- E.g. head ids @Int
1335
1336 go bvs fun_ty (EValArg {} : rest_args)
1337 | Just (_, res_ty) <- tcSplitFunTy_maybe fun_ty
1338 = go bvs res_ty rest_args
1339 | otherwise
1340 = False -- E.g. head id 'x'
1341
1342
1343 {- *********************************************************************
1344 * *
1345 tagToEnum#
1346 * *
1347 ********************************************************************* -}
1348
1349 {- Note [tagToEnum#]
1350 ~~~~~~~~~~~~~~~~~~~~
1351 Nasty check to ensure that tagToEnum# is applied to a type that is an
1352 enumeration TyCon. It's crude, because it relies on our
1353 knowing *now* that the type is ok, which in turn relies on the
1354 eager-unification part of the type checker pushing enough information
1355 here. In theory the Right Thing to do is to have a new form of
1356 constraint but I definitely cannot face that! And it works ok as-is.
1357
1358 Here's are two cases that should fail
1359 f :: forall a. a
1360 f = tagToEnum# 0 -- Can't do tagToEnum# at a type variable
1361
1362 g :: Int
1363 g = tagToEnum# 0 -- Int is not an enumeration
1364
1365 When data type families are involved it's a bit more complicated.
1366 data family F a
1367 data instance F [Int] = A | B | C
1368 Then we want to generate something like
1369 tagToEnum# R:FListInt 3# |> co :: R:FListInt ~ F [Int]
1370 Usually that coercion is hidden inside the wrappers for
1371 constructors of F [Int] but here we have to do it explicitly.
1372
1373 It's all grotesquely complicated.
1374 -}
1375
1376 isTagToEnum :: HsExpr GhcRn -> Bool
1377 isTagToEnum (HsVar _ (L _ fun_id)) = fun_id `hasKey` tagToEnumKey
1378 isTagToEnum _ = False
1379
1380 tcTagToEnum :: HsExpr GhcTc -> AppCtxt -> [HsExprArg 'TcpTc]
1381 -> TcRhoType
1382 -> TcM (HsExpr GhcTc)
1383 -- tagToEnum# :: forall a. Int# -> a
1384 -- See Note [tagToEnum#] Urgh!
1385 tcTagToEnum tc_fun fun_ctxt tc_args res_ty
1386 | [val_arg] <- dropWhile (not . isHsValArg) tc_args
1387 = do { res_ty <- zonkTcType res_ty
1388
1389 -- Check that the type is algebraic
1390 ; case tcSplitTyConApp_maybe res_ty of {
1391 Nothing -> do { addErrTc (TcRnTagToEnumUnspecifiedResTy res_ty)
1392 ; vanilla_result } ;
1393 Just (tc, tc_args) ->
1394
1395 do { -- Look through any type family
1396 ; fam_envs <- tcGetFamInstEnvs
1397 ; case tcLookupDataFamInst_maybe fam_envs tc tc_args of {
1398 Nothing -> do { check_enumeration res_ty tc
1399 ; vanilla_result } ;
1400 Just (rep_tc, rep_args, coi) ->
1401
1402 do { -- coi :: tc tc_args ~R rep_tc rep_args
1403 check_enumeration res_ty rep_tc
1404 ; let rep_ty = mkTyConApp rep_tc rep_args
1405 tc_fun' = mkHsWrap (WpTyApp rep_ty) tc_fun
1406 tc_expr = rebuildHsApps tc_fun' fun_ctxt [val_arg]
1407 df_wrap = mkWpCastR (mkTcSymCo coi)
1408 ; return (mkHsWrap df_wrap tc_expr) }}}}}
1409
1410 | otherwise
1411 = failWithTc TcRnTagToEnumMissingValArg
1412
1413 where
1414 vanilla_result = return (rebuildHsApps tc_fun fun_ctxt tc_args)
1415
1416 check_enumeration ty' tc
1417 | isEnumerationTyCon tc = return ()
1418 | otherwise = addErrTc (TcRnTagToEnumResTyNotAnEnum ty')
1419
1420
1421 {- *********************************************************************
1422 * *
1423 Pragmas on expressions
1424 * *
1425 ********************************************************************* -}
1426
1427 tcExprPrag :: HsPragE GhcRn -> HsPragE GhcTc
1428 tcExprPrag (HsPragSCC x1 src ann) = HsPragSCC x1 src ann