never executed always true always false
1
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE RankNTypes #-}
4 {-# LANGUAGE ScopedTypeVariables #-}
5 {-# LANGUAGE TypeApplications #-}
6 {-# LANGUAGE TypeFamilies #-}
7
8 {-
9 (c) The University of Glasgow 2006
10 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
11
12 -}
13
14 module GHC.Tc.Gen.Bind
15 ( tcLocalBinds
16 , tcTopBinds
17 , tcValBinds
18 , tcHsBootSigs
19 , tcPolyCheck
20 , chooseInferredQuantifiers
21 )
22 where
23
24 import GHC.Prelude
25
26 import {-# SOURCE #-} GHC.Tc.Gen.Match ( tcGRHSsPat, tcMatchesFun )
27 import {-# SOURCE #-} GHC.Tc.Gen.Expr ( tcCheckMonoExpr )
28 import {-# SOURCE #-} GHC.Tc.TyCl.PatSyn ( tcPatSynDecl, tcPatSynBuilderBind )
29
30 import GHC.Types.Tickish (CoreTickish, GenTickish (..))
31 import GHC.Types.CostCentre (mkUserCC, CCFlavour(DeclCC))
32 import GHC.Driver.Session
33 import GHC.Data.FastString
34 import GHC.Hs
35 import GHC.Tc.Errors.Types
36 import GHC.Tc.Gen.Sig
37 import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep )
38 import GHC.Tc.Utils.Monad
39 import GHC.Tc.Types.Origin
40 import GHC.Tc.Utils.Env
41 import GHC.Tc.Utils.Unify
42 import GHC.Tc.Solver
43 import GHC.Tc.Types.Evidence
44 import GHC.Tc.Gen.HsType
45 import GHC.Tc.Gen.Pat
46 import GHC.Tc.Utils.TcMType
47 import GHC.Core.Reduction ( Reduction(..) )
48 import GHC.Core.Multiplicity
49 import GHC.Core.FamInstEnv( normaliseType )
50 import GHC.Tc.Instance.Family( tcGetFamInstEnvs )
51 import GHC.Tc.Utils.TcType
52 import GHC.Core.Type (mkStrLitTy, tidyOpenType, mkCastTy)
53 import GHC.Builtin.Types ( mkBoxedTupleTy )
54 import GHC.Builtin.Types.Prim
55 import GHC.Types.SourceText
56 import GHC.Types.Id
57 import GHC.Types.Var as Var
58 import GHC.Types.Var.Set
59 import GHC.Types.Var.Env( TidyEnv )
60 import GHC.Unit.Module
61 import GHC.Types.Name
62 import GHC.Types.Name.Set
63 import GHC.Types.Name.Env
64 import GHC.Types.SrcLoc
65 import GHC.Data.Bag
66 import GHC.Utils.Error
67 import GHC.Data.Graph.Directed
68 import GHC.Data.Maybe
69 import GHC.Utils.Misc
70 import GHC.Types.Basic
71 import GHC.Types.CompleteMatch
72 import GHC.Utils.Outputable as Outputable
73 import GHC.Utils.Panic
74 import GHC.Builtin.Names( ipClassName )
75 import GHC.Tc.Validity (checkValidType)
76 import GHC.Types.Unique.FM
77 import GHC.Types.Unique.DSet
78 import GHC.Types.Unique.Set
79 import qualified GHC.LanguageExtensions as LangExt
80
81 import Control.Monad
82 import Data.Foldable (find)
83
84 {-
85 ************************************************************************
86 * *
87 \subsection{Type-checking bindings}
88 * *
89 ************************************************************************
90
91 @tcBindsAndThen@ typechecks a @HsBinds@. The "and then" part is because
92 it needs to know something about the {\em usage} of the things bound,
93 so that it can create specialisations of them. So @tcBindsAndThen@
94 takes a function which, given an extended environment, E, typechecks
95 the scope of the bindings returning a typechecked thing and (most
96 important) an LIE. It is this LIE which is then used as the basis for
97 specialising the things bound.
98
99 @tcBindsAndThen@ also takes a "combiner" which glues together the
100 bindings and the "thing" to make a new "thing".
101
102 The real work is done by @tcBindWithSigsAndThen@.
103
104 Recursive and non-recursive binds are handled in essentially the same
105 way: because of uniques there are no scoping issues left. The only
106 difference is that non-recursive bindings can bind primitive values.
107
108 Even for non-recursive binding groups we add typings for each binder
109 to the LVE for the following reason. When each individual binding is
110 checked the type of its LHS is unified with that of its RHS; and
111 type-checking the LHS of course requires that the binder is in scope.
112
113 At the top-level the LIE is sure to contain nothing but constant
114 dictionaries, which we resolve at the module level.
115
116 Note [Polymorphic recursion]
117 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
118 The game plan for polymorphic recursion in the code above is
119
120 * Bind any variable for which we have a type signature
121 to an Id with a polymorphic type. Then when type-checking
122 the RHSs we'll make a full polymorphic call.
123
124 This fine, but if you aren't a bit careful you end up with a horrendous
125 amount of partial application and (worse) a huge space leak. For example:
126
127 f :: Eq a => [a] -> [a]
128 f xs = ...f...
129
130 If we don't take care, after typechecking we get
131
132 f = /\a -> \d::Eq a -> let f' = f a d
133 in
134 \ys:[a] -> ...f'...
135
136 Notice the stupid construction of (f a d), which is of course
137 identical to the function we're executing. In this case, the
138 polymorphic recursion isn't being used (but that's a very common case).
139 This can lead to a massive space leak, from the following top-level defn
140 (post-typechecking)
141
142 ff :: [Int] -> [Int]
143 ff = f Int dEqInt
144
145 Now (f dEqInt) evaluates to a lambda that has f' as a free variable; but
146 f' is another thunk which evaluates to the same thing... and you end
147 up with a chain of identical values all hung onto by the CAF ff.
148
149 ff = f Int dEqInt
150
151 = let f' = f Int dEqInt in \ys. ...f'...
152
153 = let f' = let f' = f Int dEqInt in \ys. ...f'...
154 in \ys. ...f'...
155
156 Etc.
157
158 NOTE: a bit of arity analysis would push the (f a d) inside the (\ys...),
159 which would make the space leak go away in this case
160
161 Solution: when typechecking the RHSs we always have in hand the
162 *monomorphic* Ids for each binding. So we just need to make sure that
163 if (Method f a d) shows up in the constraints emerging from (...f...)
164 we just use the monomorphic Id. We achieve this by adding monomorphic Ids
165 to the "givens" when simplifying constraints. That's what the "lies_avail"
166 is doing.
167
168 Then we get
169
170 f = /\a -> \d::Eq a -> letrec
171 fm = \ys:[a] -> ...fm...
172 in
173 fm
174 -}
175
176 tcTopBinds :: [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn]
177 -> TcM (TcGblEnv, TcLclEnv)
178 -- The TcGblEnv contains the new tcg_binds and tcg_spects
179 -- The TcLclEnv has an extended type envt for the new bindings
180 tcTopBinds binds sigs
181 = do { -- Pattern synonym bindings populate the global environment
182 (binds', (tcg_env, tcl_env)) <- tcValBinds TopLevel binds sigs $
183 do { gbl <- getGblEnv
184 ; lcl <- getLclEnv
185 ; return (gbl, lcl) }
186 ; specs <- tcImpPrags sigs -- SPECIALISE prags for imported Ids
187
188 ; complete_matches <- setEnvs (tcg_env, tcl_env) $ tcCompleteSigs sigs
189 ; traceTc "complete_matches" (ppr binds $$ ppr sigs)
190 ; traceTc "complete_matches" (ppr complete_matches)
191
192 ; let { tcg_env' = tcg_env { tcg_imp_specs
193 = specs ++ tcg_imp_specs tcg_env
194 , tcg_complete_matches
195 = complete_matches
196 ++ tcg_complete_matches tcg_env }
197 `addTypecheckedBinds` map snd binds' }
198
199 ; return (tcg_env', tcl_env) }
200 -- The top level bindings are flattened into a giant
201 -- implicitly-mutually-recursive LHsBinds
202
203 tcCompleteSigs :: [LSig GhcRn] -> TcM [CompleteMatch]
204 tcCompleteSigs sigs =
205 let
206 doOne :: LSig GhcRn -> TcM (Maybe CompleteMatch)
207 -- We don't need to "type-check" COMPLETE signatures anymore; if their
208 -- combinations are invalid it will be found so at match sites.
209 -- There it is also where we consider if the type of the pattern match is
210 -- compatible with the result type constructor 'mb_tc'.
211 doOne (L loc c@(CompleteMatchSig _ext _src_txt (L _ ns) mb_tc_nm))
212 = fmap Just $ setSrcSpanA loc $ addErrCtxt (text "In" <+> ppr c) $ do
213 cls <- mkUniqDSet <$> mapM (addLocMA tcLookupConLike) ns
214 mb_tc <- traverse @Maybe tcLookupLocatedTyCon mb_tc_nm
215 pure CompleteMatch { cmConLikes = cls, cmResultTyCon = mb_tc }
216 doOne _ = return Nothing
217
218 -- For some reason I haven't investigated further, the signatures come in
219 -- backwards wrt. declaration order. So we reverse them here, because it makes
220 -- a difference for incomplete match suggestions.
221 in mapMaybeM doOne $ reverse sigs
222
223 tcHsBootSigs :: [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn] -> TcM [Id]
224 -- A hs-boot file has only one BindGroup, and it only has type
225 -- signatures in it. The renamer checked all this
226 tcHsBootSigs binds sigs
227 = do { checkTc (null binds) TcRnIllegalHsBootFileDecl
228 ; concatMapM (addLocMA tc_boot_sig) (filter isTypeLSig sigs) }
229 where
230 tc_boot_sig (TypeSig _ lnames hs_ty) = mapM f lnames
231 where
232 f (L _ name)
233 = do { sigma_ty <- tcHsSigWcType (FunSigCtxt name NoRRC) hs_ty
234 ; return (mkVanillaGlobal name sigma_ty) }
235 -- Notice that we make GlobalIds, not LocalIds
236 tc_boot_sig s = pprPanic "tcHsBootSigs/tc_boot_sig" (ppr s)
237
238 ------------------------
239 tcLocalBinds :: HsLocalBinds GhcRn -> TcM thing
240 -> TcM (HsLocalBinds GhcTc, thing)
241
242 tcLocalBinds (EmptyLocalBinds x) thing_inside
243 = do { thing <- thing_inside
244 ; return (EmptyLocalBinds x, thing) }
245
246 tcLocalBinds (HsValBinds x (XValBindsLR (NValBinds binds sigs))) thing_inside
247 = do { (binds', thing) <- tcValBinds NotTopLevel binds sigs thing_inside
248 ; return (HsValBinds x (XValBindsLR (NValBinds binds' sigs)), thing) }
249 tcLocalBinds (HsValBinds _ (ValBinds {})) _ = panic "tcLocalBinds"
250
251 tcLocalBinds (HsIPBinds x (IPBinds _ ip_binds)) thing_inside
252 = do { ipClass <- tcLookupClass ipClassName
253 ; (given_ips, ip_binds') <-
254 mapAndUnzipM (wrapLocSndMA (tc_ip_bind ipClass)) ip_binds
255
256 -- If the binding binds ?x = E, we must now
257 -- discharge any ?x constraints in expr_lie
258 -- See Note [Implicit parameter untouchables]
259 ; (ev_binds, result) <- checkConstraints (IPSkol ips)
260 [] given_ips thing_inside
261
262 ; return (HsIPBinds x (IPBinds ev_binds ip_binds') , result) }
263 where
264 ips = [ip | (L _ (IPBind _ (Left (L _ ip)) _)) <- ip_binds]
265
266 -- I wonder if we should do these one at a time
267 -- Consider ?x = 4
268 -- ?y = ?x + 1
269 tc_ip_bind ipClass (IPBind _ (Left (L _ ip)) expr)
270 = do { ty <- newOpenFlexiTyVarTy
271 ; let p = mkStrLitTy $ hsIPNameFS ip
272 ; ip_id <- newDict ipClass [ p, ty ]
273 ; expr' <- tcCheckMonoExpr expr ty
274 ; let d = toDict ipClass p ty `fmap` expr'
275 ; return (ip_id, (IPBind noAnn (Right ip_id) d)) }
276 tc_ip_bind _ (IPBind _ (Right {}) _) = panic "tc_ip_bind"
277
278 -- Coerces a `t` into a dictionary for `IP "x" t`.
279 -- co : t -> IP "x" t
280 toDict ipClass x ty = mkHsWrap $ mkWpCastR $
281 wrapIP $ mkClassPred ipClass [x,ty]
282
283 {- Note [Implicit parameter untouchables]
284 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
285 We add the type variables in the types of the implicit parameters
286 as untouchables, not so much because we really must not unify them,
287 but rather because we otherwise end up with constraints like this
288 Num alpha, Implic { wanted = alpha ~ Int }
289 The constraint solver solves alpha~Int by unification, but then
290 doesn't float that solved constraint out (it's not an unsolved
291 wanted). Result disaster: the (Num alpha) is again solved, this
292 time by defaulting. No no no.
293
294 However [Oct 10] this is all handled automatically by the
295 untouchable-range idea.
296 -}
297
298 tcValBinds :: TopLevelFlag
299 -> [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn]
300 -> TcM thing
301 -> TcM ([(RecFlag, LHsBinds GhcTc)], thing)
302
303 tcValBinds top_lvl binds sigs thing_inside
304 = do { -- Typecheck the signatures
305 -- It's easier to do so now, once for all the SCCs together
306 -- because a single signature f,g :: <type>
307 -- might relate to more than one SCC
308 (poly_ids, sig_fn) <- tcAddPatSynPlaceholders patsyns $
309 tcTySigs sigs
310
311 -- Extend the envt right away with all the Ids
312 -- declared with complete type signatures
313 -- Do not extend the TcBinderStack; instead
314 -- we extend it on a per-rhs basis in tcExtendForRhs
315 -- See Note [Relevant bindings and the binder stack]
316 --
317 -- For the moment, let bindings and top-level bindings introduce
318 -- only unrestricted variables.
319 ; tcExtendSigIds top_lvl poly_ids $
320 do { (binds', (extra_binds', thing))
321 <- tcBindGroups top_lvl sig_fn prag_fn binds $
322 do { thing <- thing_inside
323 -- See Note [Pattern synonym builders don't yield dependencies]
324 -- in GHC.Rename.Bind
325 ; patsyn_builders <- mapM (tcPatSynBuilderBind prag_fn) patsyns
326 ; let extra_binds = [ (NonRecursive, builder)
327 | builder <- patsyn_builders ]
328 ; return (extra_binds, thing) }
329 ; return (binds' ++ extra_binds', thing) }}
330 where
331 patsyns = getPatSynBinds binds
332 prag_fn = mkPragEnv sigs (foldr (unionBags . snd) emptyBag binds)
333
334 ------------------------
335 tcBindGroups :: TopLevelFlag -> TcSigFun -> TcPragEnv
336 -> [(RecFlag, LHsBinds GhcRn)] -> TcM thing
337 -> TcM ([(RecFlag, LHsBinds GhcTc)], thing)
338 -- Typecheck a whole lot of value bindings,
339 -- one strongly-connected component at a time
340 -- Here a "strongly connected component" has the straightforward
341 -- meaning of a group of bindings that mention each other,
342 -- ignoring type signatures (that part comes later)
343
344 tcBindGroups _ _ _ [] thing_inside
345 = do { thing <- thing_inside
346 ; return ([], thing) }
347
348 tcBindGroups top_lvl sig_fn prag_fn (group : groups) thing_inside
349 = do { -- See Note [Closed binder groups]
350 type_env <- getLclTypeEnv
351 ; let closed = isClosedBndrGroup type_env (snd group)
352 ; (group', (groups', thing))
353 <- tc_group top_lvl sig_fn prag_fn group closed $
354 tcBindGroups top_lvl sig_fn prag_fn groups thing_inside
355 ; return (group' ++ groups', thing) }
356
357 -- Note [Closed binder groups]
358 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~
359 --
360 -- A mutually recursive group is "closed" if all of the free variables of
361 -- the bindings are closed. For example
362 --
363 -- > h = \x -> let f = ...g...
364 -- > g = ....f...x...
365 -- > in ...
366 --
367 -- Here @g@ is not closed because it mentions @x@; and hence neither is @f@
368 -- closed.
369 --
370 -- So we need to compute closed-ness on each strongly connected components,
371 -- before we sub-divide it based on what type signatures it has.
372 --
373
374 ------------------------
375 tc_group :: forall thing.
376 TopLevelFlag -> TcSigFun -> TcPragEnv
377 -> (RecFlag, LHsBinds GhcRn) -> IsGroupClosed -> TcM thing
378 -> TcM ([(RecFlag, LHsBinds GhcTc)], thing)
379
380 -- Typecheck one strongly-connected component of the original program.
381 -- We get a list of groups back, because there may
382 -- be specialisations etc as well
383
384 tc_group top_lvl sig_fn prag_fn (NonRecursive, binds) closed thing_inside
385 -- A single non-recursive binding
386 -- We want to keep non-recursive things non-recursive
387 -- so that we desugar unlifted bindings correctly
388 = do { let bind = case bagToList binds of
389 [bind] -> bind
390 [] -> panic "tc_group: empty list of binds"
391 _ -> panic "tc_group: NonRecursive binds is not a singleton bag"
392 ; (bind', thing) <- tc_single top_lvl sig_fn prag_fn bind closed
393 thing_inside
394 ; return ( [(NonRecursive, bind')], thing) }
395
396 tc_group top_lvl sig_fn prag_fn (Recursive, binds) closed thing_inside
397 = -- To maximise polymorphism, we do a new
398 -- strongly-connected-component analysis, this time omitting
399 -- any references to variables with type signatures.
400 -- (This used to be optional, but isn't now.)
401 -- See Note [Polymorphic recursion] in "GHC.Hs.Binds".
402 do { traceTc "tc_group rec" (pprLHsBinds binds)
403 ; whenIsJust mbFirstPatSyn $ \lpat_syn ->
404 recursivePatSynErr (locA $ getLoc lpat_syn) binds
405 ; (binds1, thing) <- go sccs
406 ; return ([(Recursive, binds1)], thing) }
407 -- Rec them all together
408 where
409 mbFirstPatSyn = find (isPatSyn . unLoc) binds
410 isPatSyn PatSynBind{} = True
411 isPatSyn _ = False
412
413 sccs :: [SCC (LHsBind GhcRn)]
414 sccs = stronglyConnCompFromEdgedVerticesUniq (mkEdges sig_fn binds)
415
416 go :: [SCC (LHsBind GhcRn)] -> TcM (LHsBinds GhcTc, thing)
417 go (scc:sccs) = do { (binds1, ids1) <- tc_scc scc
418 -- recursive bindings must be unrestricted
419 -- (the ids added to the environment here are the name of the recursive definitions).
420 ; (binds2, thing) <- tcExtendLetEnv top_lvl sig_fn closed ids1
421 (go sccs)
422 ; return (binds1 `unionBags` binds2, thing) }
423 go [] = do { thing <- thing_inside; return (emptyBag, thing) }
424
425 tc_scc (AcyclicSCC bind) = tc_sub_group NonRecursive [bind]
426 tc_scc (CyclicSCC binds) = tc_sub_group Recursive binds
427
428 tc_sub_group rec_tc binds =
429 tcPolyBinds sig_fn prag_fn Recursive rec_tc closed binds
430
431 recursivePatSynErr
432 :: SrcSpan -- ^ The location of the first pattern synonym binding
433 -- (for error reporting)
434 -> LHsBinds GhcRn
435 -> TcM a
436 recursivePatSynErr loc binds
437 = failAt loc $ TcRnRecursivePatternSynonym binds
438
439 tc_single :: forall thing.
440 TopLevelFlag -> TcSigFun -> TcPragEnv
441 -> LHsBind GhcRn -> IsGroupClosed -> TcM thing
442 -> TcM (LHsBinds GhcTc, thing)
443 tc_single _top_lvl sig_fn prag_fn
444 (L _ (PatSynBind _ psb@PSB{ psb_id = L _ name }))
445 _ thing_inside
446 = do { (aux_binds, tcg_env) <- tcPatSynDecl psb (sig_fn name) prag_fn
447 ; thing <- setGblEnv tcg_env thing_inside
448 ; return (aux_binds, thing)
449 }
450
451 tc_single top_lvl sig_fn prag_fn lbind closed thing_inside
452 = do { (binds1, ids) <- tcPolyBinds sig_fn prag_fn
453 NonRecursive NonRecursive
454 closed
455 [lbind]
456 -- since we are defining a non-recursive binding, it is not necessary here
457 -- to define an unrestricted binding. But we do so until toplevel linear bindings are supported.
458 ; thing <- tcExtendLetEnv top_lvl sig_fn closed ids thing_inside
459 ; return (binds1, thing) }
460
461 ------------------------
462 type BKey = Int -- Just number off the bindings
463
464 mkEdges :: TcSigFun -> LHsBinds GhcRn -> [Node BKey (LHsBind GhcRn)]
465 -- See Note [Polymorphic recursion] in "GHC.Hs.Binds".
466 mkEdges sig_fn binds
467 = [ DigraphNode bind key [key | n <- nonDetEltsUniqSet (bind_fvs (unLoc bind)),
468 Just key <- [lookupNameEnv key_map n], no_sig n ]
469 | (bind, key) <- keyd_binds
470 ]
471 -- It's OK to use nonDetEltsUFM here as stronglyConnCompFromEdgedVertices
472 -- is still deterministic even if the edges are in nondeterministic order
473 -- as explained in Note [Deterministic SCC] in GHC.Data.Graph.Directed.
474 where
475 bind_fvs (FunBind { fun_ext = fvs }) = fvs
476 bind_fvs (PatBind { pat_ext = fvs }) = fvs
477 bind_fvs _ = emptyNameSet
478
479 no_sig :: Name -> Bool
480 no_sig n = not (hasCompleteSig sig_fn n)
481
482 keyd_binds = bagToList binds `zip` [0::BKey ..]
483
484 key_map :: NameEnv BKey -- Which binding it comes from
485 key_map = mkNameEnv [(bndr, key) | (L _ bind, key) <- keyd_binds
486 , bndr <- collectHsBindBinders CollNoDictBinders bind ]
487
488 ------------------------
489 tcPolyBinds :: TcSigFun -> TcPragEnv
490 -> RecFlag -- Whether the group is really recursive
491 -> RecFlag -- Whether it's recursive after breaking
492 -- dependencies based on type signatures
493 -> IsGroupClosed -- Whether the group is closed
494 -> [LHsBind GhcRn] -- None are PatSynBind
495 -> TcM (LHsBinds GhcTc, [TcId])
496
497 -- Typechecks a single bunch of values bindings all together,
498 -- and generalises them. The bunch may be only part of a recursive
499 -- group, because we use type signatures to maximise polymorphism
500 --
501 -- Returns a list because the input may be a single non-recursive binding,
502 -- in which case the dependency order of the resulting bindings is
503 -- important.
504 --
505 -- Knows nothing about the scope of the bindings
506 -- None of the bindings are pattern synonyms
507
508 tcPolyBinds sig_fn prag_fn rec_group rec_tc closed bind_list
509 = setSrcSpan loc $
510 recoverM (recoveryCode binder_names sig_fn) $ do
511 -- Set up main recover; take advantage of any type sigs
512
513 { traceTc "------------------------------------------------" Outputable.empty
514 ; traceTc "Bindings for {" (ppr binder_names)
515 ; dflags <- getDynFlags
516 ; let plan = decideGeneralisationPlan dflags bind_list closed sig_fn
517 ; traceTc "Generalisation plan" (ppr plan)
518 ; result@(_, poly_ids) <- case plan of
519 NoGen -> tcPolyNoGen rec_tc prag_fn sig_fn bind_list
520 InferGen mn -> tcPolyInfer rec_tc prag_fn sig_fn mn bind_list
521 CheckGen lbind sig -> tcPolyCheck prag_fn sig lbind
522
523 ; _concrete_evs <-
524 mapM (\ poly_id ->
525 hasFixedRuntimeRep (FRRBinder $ idName poly_id) (idType poly_id))
526 poly_ids
527
528 ; traceTc "} End of bindings for" (vcat [ ppr binder_names, ppr rec_group
529 , vcat [ppr id <+> ppr (idType id) | id <- poly_ids]
530 ])
531
532 ; return result }
533 where
534 binder_names = collectHsBindListBinders CollNoDictBinders bind_list
535 loc = foldr1 combineSrcSpans (map (locA . getLoc) bind_list)
536 -- The mbinds have been dependency analysed and
537 -- may no longer be adjacent; so find the narrowest
538 -- span that includes them all
539
540 --------------
541 -- If typechecking the binds fails, then return with each
542 -- signature-less binder given type (forall a.a), to minimise
543 -- subsequent error messages
544 recoveryCode :: [Name] -> TcSigFun -> TcM (LHsBinds GhcTc, [Id])
545 recoveryCode binder_names sig_fn
546 = do { traceTc "tcBindsWithSigs: error recovery" (ppr binder_names)
547 ; let poly_ids = map mk_dummy binder_names
548 ; return (emptyBag, poly_ids) }
549 where
550 mk_dummy name
551 | Just sig <- sig_fn name
552 , Just poly_id <- completeSigPolyId_maybe sig
553 = poly_id
554 | otherwise
555 = mkLocalId name Many forall_a_a
556
557 forall_a_a :: TcType
558 -- At one point I had (forall r (a :: TYPE r). a), but of course
559 -- that type is ill-formed: its mentions 'r' which escapes r's scope.
560 -- Another alternative would be (forall (a :: TYPE kappa). a), where
561 -- kappa is a unification variable. But I don't think we need that
562 -- complication here. I'm going to just use (forall (a::*). a).
563 -- See #15276
564 forall_a_a = mkSpecForAllTys [alphaTyVar] alphaTy
565
566 {- *********************************************************************
567 * *
568 tcPolyNoGen
569 * *
570 ********************************************************************* -}
571
572 tcPolyNoGen -- No generalisation whatsoever
573 :: RecFlag -- Whether it's recursive after breaking
574 -- dependencies based on type signatures
575 -> TcPragEnv -> TcSigFun
576 -> [LHsBind GhcRn]
577 -> TcM (LHsBinds GhcTc, [TcId])
578
579 tcPolyNoGen rec_tc prag_fn tc_sig_fn bind_list
580 = do { (binds', mono_infos) <- tcMonoBinds rec_tc tc_sig_fn
581 (LetGblBndr prag_fn)
582 bind_list
583 ; mono_ids' <- mapM tc_mono_info mono_infos
584 ; return (binds', mono_ids') }
585 where
586 tc_mono_info (MBI { mbi_poly_name = name, mbi_mono_id = mono_id })
587 = do { _specs <- tcSpecPrags mono_id (lookupPragEnv prag_fn name)
588 ; return mono_id }
589 -- NB: tcPrags generates error messages for
590 -- specialisation pragmas for non-overloaded sigs
591 -- Indeed that is why we call it here!
592 -- So we can safely ignore _specs
593
594
595 {- *********************************************************************
596 * *
597 tcPolyCheck
598 * *
599 ********************************************************************* -}
600
601 tcPolyCheck :: TcPragEnv
602 -> TcIdSigInfo -- Must be a complete signature
603 -> LHsBind GhcRn -- Must be a FunBind
604 -> TcM (LHsBinds GhcTc, [TcId])
605 -- There is just one binding,
606 -- it is a FunBind
607 -- it has a complete type signature,
608 tcPolyCheck prag_fn
609 (CompleteSig { sig_bndr = poly_id
610 , sig_ctxt = ctxt
611 , sig_loc = sig_loc })
612 (L bind_loc (FunBind { fun_id = L nm_loc name
613 , fun_matches = matches }))
614 = do { traceTc "tcPolyCheck" (ppr poly_id $$ ppr sig_loc)
615
616 ; mono_name <- newNameAt (nameOccName name) (locA nm_loc)
617 ; (wrap_gen, (wrap_res, matches'))
618 <- setSrcSpan sig_loc $ -- Sets the binding location for the skolems
619 tcSkolemiseScoped ctxt (idType poly_id) $ \rho_ty ->
620 -- Unwraps multiple layers; e.g
621 -- f :: forall a. Eq a => forall b. Ord b => blah
622 -- NB: tcSkolemise makes fresh type variables
623 -- See Note [Instantiate sig with fresh variables]
624
625 let mono_id = mkLocalId mono_name (varMult poly_id) rho_ty in
626 tcExtendBinderStack [TcIdBndr mono_id NotTopLevel] $
627 -- Why mono_id in the BinderStack?
628 -- See Note [Relevant bindings and the binder stack]
629
630 setSrcSpanA bind_loc $
631 tcMatchesFun (L nm_loc mono_id) matches
632 (mkCheckExpType rho_ty)
633
634 -- We make a funny AbsBinds, abstracting over nothing,
635 -- just so we have somewhere to put the SpecPrags.
636 -- Otherwise we could just use the FunBind
637 -- Hence poly_id2 is just a clone of poly_id;
638 -- We re-use mono-name, but we could equally well use a fresh one
639
640 ; let prag_sigs = lookupPragEnv prag_fn name
641 poly_id2 = mkLocalId mono_name (idMult poly_id) (idType poly_id)
642 ; spec_prags <- tcSpecPrags poly_id prag_sigs
643 ; poly_id <- addInlinePrags poly_id prag_sigs
644
645 ; mod <- getModule
646 ; tick <- funBindTicks (locA nm_loc) poly_id mod prag_sigs
647
648 ; let bind' = FunBind { fun_id = L nm_loc poly_id2
649 , fun_matches = matches'
650 , fun_ext = wrap_gen <.> wrap_res
651 , fun_tick = tick }
652
653 export = ABE { abe_ext = noExtField
654 , abe_wrap = idHsWrapper
655 , abe_poly = poly_id
656 , abe_mono = poly_id2
657 , abe_prags = SpecPrags spec_prags }
658
659 abs_bind = L bind_loc $
660 AbsBinds { abs_ext = noExtField
661 , abs_tvs = []
662 , abs_ev_vars = []
663 , abs_ev_binds = []
664 , abs_exports = [export]
665 , abs_binds = unitBag (L bind_loc bind')
666 , abs_sig = True }
667
668 ; return (unitBag abs_bind, [poly_id]) }
669
670 tcPolyCheck _prag_fn sig bind
671 = pprPanic "tcPolyCheck" (ppr sig $$ ppr bind)
672
673 funBindTicks :: SrcSpan -> TcId -> Module -> [LSig GhcRn]
674 -> TcM [CoreTickish]
675 funBindTicks loc fun_id mod sigs
676 | (mb_cc_str : _) <- [ cc_name | L _ (SCCFunSig _ _ _ cc_name) <- sigs ]
677 -- this can only be a singleton list, as duplicate pragmas are rejected
678 -- by the renamer
679 , let cc_str
680 | Just cc_str <- mb_cc_str
681 = sl_fs $ unLoc cc_str
682 | otherwise
683 = getOccFS (Var.varName fun_id)
684 cc_name = moduleNameFS (moduleName mod) `appendFS` consFS '.' cc_str
685 = do
686 flavour <- DeclCC <$> getCCIndexTcM cc_name
687 let cc = mkUserCC cc_name mod loc flavour
688 return [ProfNote cc True True]
689 | otherwise
690 = return []
691
692 {- Note [Instantiate sig with fresh variables]
693 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
694 It's vital to instantiate a type signature with fresh variables.
695 For example:
696 type T = forall a. [a] -> [a]
697 f :: T;
698 f = g where { g :: T; g = <rhs> }
699
700 We must not use the same 'a' from the defn of T at both places!!
701 (Instantiation is only necessary because of type synonyms. Otherwise,
702 it's all cool; each signature has distinct type variables from the renamer.)
703 -}
704
705
706 {- *********************************************************************
707 * *
708 tcPolyInfer
709 * *
710 ********************************************************************* -}
711
712 tcPolyInfer
713 :: RecFlag -- Whether it's recursive after breaking
714 -- dependencies based on type signatures
715 -> TcPragEnv -> TcSigFun
716 -> Bool -- True <=> apply the monomorphism restriction
717 -> [LHsBind GhcRn]
718 -> TcM (LHsBinds GhcTc, [TcId])
719 tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
720 = do { (tclvl, wanted, (binds', mono_infos))
721 <- pushLevelAndCaptureConstraints $
722 tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list
723
724 ; let name_taus = [ (mbi_poly_name info, idType (mbi_mono_id info))
725 | info <- mono_infos ]
726 sigs = [ sig | MBI { mbi_sig = Just sig } <- mono_infos ]
727 infer_mode = if mono then ApplyMR else NoRestrictions
728
729 ; mapM_ (checkOverloadedSig mono) sigs
730
731 ; traceTc "simplifyInfer call" (ppr tclvl $$ ppr name_taus $$ ppr wanted)
732 ; (qtvs, givens, ev_binds, insoluble)
733 <- simplifyInfer tclvl infer_mode sigs name_taus wanted
734
735 ; let inferred_theta = map evVarPred givens
736 ; exports <- checkNoErrs $
737 mapM (mkExport prag_fn insoluble qtvs inferred_theta) mono_infos
738
739 ; loc <- getSrcSpanM
740 ; let poly_ids = map abe_poly exports
741 abs_bind = L (noAnnSrcSpan loc) $
742 AbsBinds { abs_ext = noExtField
743 , abs_tvs = qtvs
744 , abs_ev_vars = givens, abs_ev_binds = [ev_binds]
745 , abs_exports = exports, abs_binds = binds'
746 , abs_sig = False }
747
748 ; traceTc "Binding:" (ppr (poly_ids `zip` map idType poly_ids))
749 ; return (unitBag abs_bind, poly_ids) }
750 -- poly_ids are guaranteed zonked by mkExport
751
752 --------------
753 mkExport :: TcPragEnv
754 -> Bool -- True <=> there was an insoluble type error
755 -- when typechecking the bindings
756 -> [TyVar] -> TcThetaType -- Both already zonked
757 -> MonoBindInfo
758 -> TcM (ABExport GhcTc)
759 -- Only called for generalisation plan InferGen, not by CheckGen or NoGen
760 --
761 -- mkExport generates exports with
762 -- zonked type variables,
763 -- zonked poly_ids
764 -- The former is just because no further unifications will change
765 -- the quantified type variables, so we can fix their final form
766 -- right now.
767 -- The latter is needed because the poly_ids are used to extend the
768 -- type environment; see the invariant on GHC.Tc.Utils.Env.tcExtendIdEnv
769
770 -- Pre-condition: the qtvs and theta are already zonked
771
772 mkExport prag_fn insoluble qtvs theta
773 mono_info@(MBI { mbi_poly_name = poly_name
774 , mbi_sig = mb_sig
775 , mbi_mono_id = mono_id })
776 = do { mono_ty <- zonkTcType (idType mono_id)
777 ; poly_id <- mkInferredPolyId insoluble qtvs theta poly_name mb_sig mono_ty
778
779 -- NB: poly_id has a zonked type
780 ; poly_id <- addInlinePrags poly_id prag_sigs
781 ; spec_prags <- tcSpecPrags poly_id prag_sigs
782 -- tcPrags requires a zonked poly_id
783
784 -- See Note [Impedance matching]
785 -- NB: we have already done checkValidType, including an ambiguity check,
786 -- on the type; either when we checked the sig or in mkInferredPolyId
787 ; let poly_ty = idType poly_id
788 sel_poly_ty = mkInfSigmaTy qtvs theta mono_ty
789 -- This type is just going into tcSubType,
790 -- so Inferred vs. Specified doesn't matter
791
792 ; wrap <- if sel_poly_ty `eqType` poly_ty -- NB: eqType ignores visibility
793 then return idHsWrapper -- Fast path; also avoids complaint when we infer
794 -- an ambiguous type and have AllowAmbiguousType
795 -- e..g infer x :: forall a. F a -> Int
796 else addErrCtxtM (mk_impedance_match_msg mono_info sel_poly_ty poly_ty) $
797 tcSubTypeSigma sig_ctxt sel_poly_ty poly_ty
798
799 ; localSigWarn poly_id mb_sig
800
801 ; return (ABE { abe_ext = noExtField
802 , abe_wrap = wrap
803 -- abe_wrap :: idType poly_id ~ (forall qtvs. theta => mono_ty)
804 , abe_poly = poly_id
805 , abe_mono = mono_id
806 , abe_prags = SpecPrags spec_prags }) }
807 where
808 prag_sigs = lookupPragEnv prag_fn poly_name
809 sig_ctxt = InfSigCtxt poly_name
810
811 mkInferredPolyId :: Bool -- True <=> there was an insoluble error when
812 -- checking the binding group for this Id
813 -> [TyVar] -> TcThetaType
814 -> Name -> Maybe TcIdSigInst -> TcType
815 -> TcM TcId
816 mkInferredPolyId insoluble qtvs inferred_theta poly_name mb_sig_inst mono_ty
817 | Just (TISI { sig_inst_sig = sig }) <- mb_sig_inst
818 , CompleteSig { sig_bndr = poly_id } <- sig
819 = return poly_id
820
821 | otherwise -- Either no type sig or partial type sig
822 = checkNoErrs $ -- The checkNoErrs ensures that if the type is ambiguous
823 -- we don't carry on to the impedance matching, and generate
824 -- a duplicate ambiguity error. There is a similar
825 -- checkNoErrs for complete type signatures too.
826 do { fam_envs <- tcGetFamInstEnvs
827 ; let mono_ty' = reductionReducedType $ normaliseType fam_envs Nominal mono_ty
828 -- Unification may not have normalised the type,
829 -- so do it here to make it as uncomplicated as possible.
830 -- Example: f :: [F Int] -> Bool
831 -- should be rewritten to f :: [Char] -> Bool, if possible
832 --
833 -- We can discard the coercion _co, because we'll reconstruct
834 -- it in the call to tcSubType below
835
836 ; (binders, theta') <- chooseInferredQuantifiers inferred_theta
837 (tyCoVarsOfType mono_ty') qtvs mb_sig_inst
838
839 ; let inferred_poly_ty = mkInvisForAllTys binders (mkPhiTy theta' mono_ty')
840
841 ; traceTc "mkInferredPolyId" (vcat [ppr poly_name, ppr qtvs, ppr theta'
842 , ppr inferred_poly_ty])
843 ; unless insoluble $
844 addErrCtxtM (mk_inf_msg poly_name inferred_poly_ty) $
845 checkValidType (InfSigCtxt poly_name) inferred_poly_ty
846 -- See Note [Validity of inferred types]
847 -- If we found an insoluble error in the function definition, don't
848 -- do this check; otherwise (#14000) we may report an ambiguity
849 -- error for a rather bogus type.
850
851 ; return (mkLocalId poly_name Many inferred_poly_ty) }
852
853
854 chooseInferredQuantifiers :: TcThetaType -- inferred
855 -> TcTyVarSet -- tvs free in tau type
856 -> [TcTyVar] -- inferred quantified tvs
857 -> Maybe TcIdSigInst
858 -> TcM ([InvisTVBinder], TcThetaType)
859 chooseInferredQuantifiers inferred_theta tau_tvs qtvs Nothing
860 = -- No type signature (partial or complete) for this binder,
861 do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta tau_tvs)
862 -- Include kind variables! #7916
863 my_theta = pickCapturedPreds free_tvs inferred_theta
864 binders = [ mkTyVarBinder InferredSpec tv
865 | tv <- qtvs
866 , tv `elemVarSet` free_tvs ]
867 ; return (binders, my_theta) }
868
869 chooseInferredQuantifiers inferred_theta tau_tvs qtvs
870 (Just (TISI { sig_inst_sig = sig -- Always PartialSig
871 , sig_inst_wcx = wcx
872 , sig_inst_theta = annotated_theta
873 , sig_inst_skols = annotated_tvs }))
874 = -- Choose quantifiers for a partial type signature
875 do { let (psig_qtv_nms, psig_qtv_bndrs) = unzip annotated_tvs
876 ; psig_qtv_bndrs <- mapM zonkInvisTVBinder psig_qtv_bndrs
877 ; let psig_qtvs = map binderVar psig_qtv_bndrs
878 psig_qtv_set = mkVarSet psig_qtvs
879 psig_qtv_prs = psig_qtv_nms `zip` psig_qtvs
880
881
882 -- Check whether the quantified variables of the
883 -- partial signature have been unified together
884 -- See Note [Quantified variables in partial type signatures]
885 ; mapM_ report_dup_tyvar_tv_err (findDupTyVarTvs psig_qtv_prs)
886
887 -- Check whether a quantified variable of the partial type
888 -- signature is not actually quantified. How can that happen?
889 -- See Note [Quantification and partial signatures] Wrinkle 4
890 -- in GHC.Tc.Solver
891 ; mapM_ report_mono_sig_tv_err [ n | (n,tv) <- psig_qtv_prs
892 , not (tv `elem` qtvs) ]
893
894 ; annotated_theta <- zonkTcTypes annotated_theta
895 ; (free_tvs, my_theta) <- choose_psig_context psig_qtv_set annotated_theta wcx
896
897 ; let keep_me = free_tvs `unionVarSet` psig_qtv_set
898 final_qtvs = [ mkTyVarBinder vis tv
899 | tv <- qtvs -- Pulling from qtvs maintains original order
900 , tv `elemVarSet` keep_me
901 , let vis = case lookupVarBndr tv psig_qtv_bndrs of
902 Just spec -> spec
903 Nothing -> InferredSpec ]
904
905 ; return (final_qtvs, my_theta) }
906 where
907 report_dup_tyvar_tv_err (n1,n2)
908 | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
909 = addErrTc (TcRnPartialTypeSigTyVarMismatch n1 n2 fn_name hs_ty)
910 | otherwise -- Can't happen; by now we know it's a partial sig
911 = pprPanic "report_tyvar_tv_err" (ppr sig)
912
913 report_mono_sig_tv_err n
914 | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
915 = addErrTc (TcRnPartialTypeSigBadQuantifier n fn_name hs_ty)
916 | otherwise -- Can't happen; by now we know it's a partial sig
917 = pprPanic "report_mono_sig_tv_err" (ppr sig)
918
919 choose_psig_context :: VarSet -> TcThetaType -> Maybe TcType
920 -> TcM (VarSet, TcThetaType)
921 choose_psig_context _ annotated_theta Nothing
922 = do { let free_tvs = closeOverKinds (tyCoVarsOfTypes annotated_theta
923 `unionVarSet` tau_tvs)
924 ; return (free_tvs, annotated_theta) }
925
926 choose_psig_context psig_qtvs annotated_theta (Just wc_var_ty)
927 = do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta seed_tvs)
928 -- growThetaVars just like the no-type-sig case
929 -- Omitting this caused #12844
930 seed_tvs = tyCoVarsOfTypes annotated_theta -- These are put there
931 `unionVarSet` tau_tvs -- by the user
932
933 ; let keep_me = psig_qtvs `unionVarSet` free_tvs
934 my_theta = pickCapturedPreds keep_me inferred_theta
935
936 -- Fill in the extra-constraints wildcard hole with inferred_theta,
937 -- so that the Hole constraint we have already emitted
938 -- (in tcHsPartialSigType) can report what filled it in.
939 -- NB: my_theta already includes all the annotated constraints
940 ; diff_theta <- findInferredDiff annotated_theta my_theta
941
942 ; case tcGetCastedTyVar_maybe wc_var_ty of
943 -- We know that wc_co must have type kind(wc_var) ~ Constraint, as it
944 -- comes from the checkExpectedKind in GHC.Tc.Gen.HsType.tcAnonWildCardOcc.
945 -- So, to make the kinds work out, we reverse the cast here.
946 Just (wc_var, wc_co) -> writeMetaTyVar wc_var (mk_ctuple diff_theta
947 `mkCastTy` mkTcSymCo wc_co)
948 Nothing -> pprPanic "chooseInferredQuantifiers 1" (ppr wc_var_ty)
949
950 ; traceTc "completeTheta" $
951 vcat [ ppr sig
952 , text "annotated_theta:" <+> ppr annotated_theta
953 , text "inferred_theta:" <+> ppr inferred_theta
954 , text "my_theta:" <+> ppr my_theta
955 , text "diff_theta:" <+> ppr diff_theta ]
956 ; return (free_tvs, annotated_theta ++ diff_theta) }
957 -- Return (annotated_theta ++ diff_theta)
958 -- See Note [Extra-constraints wildcards]
959
960 mk_ctuple preds = mkBoxedTupleTy preds
961 -- Hack alert! See GHC.Tc.Gen.HsType:
962 -- Note [Extra-constraint holes in partial type signatures]
963
964 mk_impedance_match_msg :: MonoBindInfo
965 -> TcType -> TcType
966 -> TidyEnv -> TcM (TidyEnv, SDoc)
967 -- This is a rare but rather awkward error messages
968 mk_impedance_match_msg (MBI { mbi_poly_name = name, mbi_sig = mb_sig })
969 inf_ty sig_ty tidy_env
970 = do { (tidy_env1, inf_ty) <- zonkTidyTcType tidy_env inf_ty
971 ; (tidy_env2, sig_ty) <- zonkTidyTcType tidy_env1 sig_ty
972 ; let msg = vcat [ text "When checking that the inferred type"
973 , nest 2 $ ppr name <+> dcolon <+> ppr inf_ty
974 , text "is as general as its" <+> what <+> text "signature"
975 , nest 2 $ ppr name <+> dcolon <+> ppr sig_ty ]
976 ; return (tidy_env2, msg) }
977 where
978 what = case mb_sig of
979 Nothing -> text "inferred"
980 Just sig | isPartialSig sig -> text "(partial)"
981 | otherwise -> empty
982
983
984 mk_inf_msg :: Name -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
985 mk_inf_msg poly_name poly_ty tidy_env
986 = do { (tidy_env1, poly_ty) <- zonkTidyTcType tidy_env poly_ty
987 ; let msg = vcat [ text "When checking the inferred type"
988 , nest 2 $ ppr poly_name <+> dcolon <+> ppr poly_ty ]
989 ; return (tidy_env1, msg) }
990
991
992 -- | Warn the user about polymorphic local binders that lack type signatures.
993 localSigWarn :: Id -> Maybe TcIdSigInst -> TcM ()
994 localSigWarn id mb_sig
995 | Just _ <- mb_sig = return ()
996 | not (isSigmaTy (idType id)) = return ()
997 | otherwise = warnMissingSignatures id
998
999 warnMissingSignatures :: Id -> TcM ()
1000 warnMissingSignatures id
1001 = do { env0 <- tcInitTidyEnv
1002 ; let (env1, tidy_ty) = tidyOpenType env0 (idType id)
1003 ; let dia = TcRnPolymorphicBinderMissingSig (idName id) tidy_ty
1004 ; addDiagnosticTcM (env1, dia) }
1005
1006 checkOverloadedSig :: Bool -> TcIdSigInst -> TcM ()
1007 -- Example:
1008 -- f :: Eq a => a -> a
1009 -- K f = e
1010 -- The MR applies, but the signature is overloaded, and it's
1011 -- best to complain about this directly
1012 -- c.f #11339
1013 checkOverloadedSig monomorphism_restriction_applies sig
1014 | not (null (sig_inst_theta sig))
1015 , monomorphism_restriction_applies
1016 , let orig_sig = sig_inst_sig sig
1017 = setSrcSpan (sig_loc orig_sig) $
1018 failWith $ TcRnOverloadedSig orig_sig
1019 | otherwise
1020 = return ()
1021
1022 {- Note [Partial type signatures and generalisation]
1023 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1024 If /any/ of the signatures in the group is a partial type signature
1025 f :: _ -> Int
1026 then we *always* use the InferGen plan, and hence tcPolyInfer.
1027 We do this even for a local binding with -XMonoLocalBinds, when
1028 we normally use NoGen.
1029
1030 Reasons:
1031 * The TcSigInfo for 'f' has a unification variable for the '_',
1032 whose TcLevel is one level deeper than the current level.
1033 (See pushTcLevelM in tcTySig.) But NoGen doesn't increase
1034 the TcLevel like InferGen, so we lose the level invariant.
1035
1036 * The signature might be f :: forall a. _ -> a
1037 so it really is polymorphic. It's not clear what it would
1038 mean to use NoGen on this, and indeed the ASSERT in tcLhs,
1039 in the (Just sig) case, checks that if there is a signature
1040 then we are using LetLclBndr, and hence a nested AbsBinds with
1041 increased TcLevel
1042
1043 It might be possible to fix these difficulties somehow, but there
1044 doesn't seem much point. Indeed, adding a partial type signature is a
1045 way to get per-binding inferred generalisation.
1046
1047 We apply the MR if /all/ of the partial signatures lack a context.
1048 In particular (#11016):
1049 f2 :: (?loc :: Int) => _
1050 f2 = ?loc
1051 It's stupid to apply the MR here. This test includes an extra-constraints
1052 wildcard; that is, we don't apply the MR if you write
1053 f3 :: _ => blah
1054
1055 Note [Quantified variables in partial type signatures]
1056 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1057 Consider
1058 f :: forall a. a -> a -> _
1059 f x y = g x y
1060 g :: forall b. b -> b -> _
1061 g x y = [x, y]
1062
1063 Here, 'f' and 'g' are mutually recursive, and we end up unifying 'a' and 'b'
1064 together, which is fine. So we bind 'a' and 'b' to TyVarTvs, which can then
1065 unify with each other.
1066
1067 But now consider:
1068 f :: forall a b. a -> b -> _
1069 f x y = [x, y]
1070
1071 We want to get an error from this, because 'a' and 'b' get unified.
1072 So we make a test, one per partial signature, to check that the
1073 explicitly-quantified type variables have not been unified together.
1074 #14449 showed this up.
1075
1076 Note [Extra-constraints wildcards]
1077 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1078 Consider this from #18646
1079 class Foo x where
1080 foo :: x
1081
1082 bar :: (Foo (), _) => f ()
1083 bar = pure foo
1084
1085 We get [W] Foo (), [W] Applicative f. When we do pickCapturedPreds in
1086 choose_psig_context, we'll discard Foo ()! Usually would not quantify over
1087 such (closed) predicates. So my_theta will be (Applicative f). But we really
1088 do want to quantify over (Foo ()) -- it was speicfied by the programmer.
1089 Solution: always return annotated_theta (user-specified) plus the extra piece
1090 diff_theta.
1091
1092 Note [Validity of inferred types]
1093 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1094 We need to check inferred type for validity, in case it uses language
1095 extensions that are not turned on. The principle is that if the user
1096 simply adds the inferred type to the program source, it'll compile fine.
1097 See #8883.
1098
1099 Examples that might fail:
1100 - the type might be ambiguous
1101
1102 - an inferred theta that requires type equalities e.g. (F a ~ G b)
1103 or multi-parameter type classes
1104 - an inferred type that includes unboxed tuples
1105
1106
1107 Note [Impedance matching]
1108 ~~~~~~~~~~~~~~~~~~~~~~~~~
1109 Consider
1110 f 0 x = x
1111 f n x = g [] (not x)
1112
1113 g [] y = f 10 y
1114 g _ y = f 9 y
1115
1116 After typechecking we'll get
1117 f_mono_ty :: a -> Bool -> Bool
1118 g_mono_ty :: [b] -> Bool -> Bool
1119 with constraints
1120 (Eq a, Num a)
1121
1122 Note that f is polymorphic in 'a' and g in 'b'; and these are not linked.
1123 The types we really want for f and g are
1124 f :: forall a. (Eq a, Num a) => a -> Bool -> Bool
1125 g :: forall b. [b] -> Bool -> Bool
1126
1127 We can get these by "impedance matching":
1128 tuple :: forall a b. (Eq a, Num a) => (a -> Bool -> Bool, [b] -> Bool -> Bool)
1129 tuple a b d1 d1 = let ...bind f_mono, g_mono in (f_mono, g_mono)
1130
1131 f a d1 d2 = case tuple a Any d1 d2 of (f, g) -> f
1132 g b = case tuple Integer b dEqInteger dNumInteger of (f,g) -> g
1133
1134 Suppose the shared quantified tyvars are qtvs and constraints theta.
1135 Then we want to check that
1136 forall qtvs. theta => f_mono_ty is more polymorphic than f's polytype
1137 and the proof is the impedance matcher.
1138
1139 Notice that the impedance matcher may do defaulting. See #7173.
1140
1141 It also cleverly does an ambiguity check; for example, rejecting
1142 f :: F a -> F a
1143 where F is a non-injective type function.
1144 -}
1145
1146
1147 {-
1148 Note [SPECIALISE pragmas]
1149 ~~~~~~~~~~~~~~~~~~~~~~~~~
1150 There is no point in a SPECIALISE pragma for a non-overloaded function:
1151 reverse :: [a] -> [a]
1152 {-# SPECIALISE reverse :: [Int] -> [Int] #-}
1153
1154 But SPECIALISE INLINE *can* make sense for GADTS:
1155 data Arr e where
1156 ArrInt :: !Int -> ByteArray# -> Arr Int
1157 ArrPair :: !Int -> Arr e1 -> Arr e2 -> Arr (e1, e2)
1158
1159 (!:) :: Arr e -> Int -> e
1160 {-# SPECIALISE INLINE (!:) :: Arr Int -> Int -> Int #-}
1161 {-# SPECIALISE INLINE (!:) :: Arr (a, b) -> Int -> (a, b) #-}
1162 (ArrInt _ ba) !: (I# i) = I# (indexIntArray# ba i)
1163 (ArrPair _ a1 a2) !: i = (a1 !: i, a2 !: i)
1164
1165 When (!:) is specialised it becomes non-recursive, and can usefully
1166 be inlined. Scary! So we only warn for SPECIALISE *without* INLINE
1167 for a non-overloaded function.
1168
1169 ************************************************************************
1170 * *
1171 tcMonoBinds
1172 * *
1173 ************************************************************************
1174
1175 @tcMonoBinds@ deals with a perhaps-recursive group of HsBinds.
1176 The signatures have been dealt with already.
1177 -}
1178
1179 data MonoBindInfo = MBI { mbi_poly_name :: Name
1180 , mbi_sig :: Maybe TcIdSigInst
1181 , mbi_mono_id :: TcId }
1182
1183 tcMonoBinds :: RecFlag -- Whether the binding is recursive for typechecking purposes
1184 -- i.e. the binders are mentioned in their RHSs, and
1185 -- we are not rescued by a type signature
1186 -> TcSigFun -> LetBndrSpec
1187 -> [LHsBind GhcRn]
1188 -> TcM (LHsBinds GhcTc, [MonoBindInfo])
1189
1190 -- SPECIAL CASE 1: see Note [Special case for non-recursive function bindings]
1191 tcMonoBinds is_rec sig_fn no_gen
1192 [ L b_loc (FunBind { fun_id = L nm_loc name
1193 , fun_matches = matches })]
1194 -- Single function binding,
1195 | NonRecursive <- is_rec -- ...binder isn't mentioned in RHS
1196 , Nothing <- sig_fn name -- ...with no type signature
1197 = setSrcSpanA b_loc $
1198 do { ((co_fn, matches'), mono_id, _) <- fixM $ \ ~(_, _, rhs_ty) ->
1199 -- See Note [fixM for rhs_ty in tcMonoBinds]
1200 do { mono_id <- newLetBndr no_gen name Many rhs_ty
1201 ; (matches', rhs_ty')
1202 <- tcInfer $ \ exp_ty ->
1203 tcExtendBinderStack [TcIdBndr_ExpType name exp_ty NotTopLevel] $
1204 -- We extend the error context even for a non-recursive
1205 -- function so that in type error messages we show the
1206 -- type of the thing whose rhs we are type checking
1207 tcMatchesFun (L nm_loc mono_id) matches exp_ty
1208 ; return (matches', mono_id, rhs_ty')
1209 }
1210
1211 ; return (unitBag $ L b_loc $
1212 FunBind { fun_id = L nm_loc mono_id,
1213 fun_matches = matches',
1214 fun_ext = co_fn, fun_tick = [] },
1215 [MBI { mbi_poly_name = name
1216 , mbi_sig = Nothing
1217 , mbi_mono_id = mono_id }]) }
1218
1219 -- SPECIAL CASE 2: see Note [Special case for non-recursive pattern bindings]
1220 tcMonoBinds is_rec sig_fn no_gen
1221 [L b_loc (PatBind { pat_lhs = pat, pat_rhs = grhss })]
1222 | NonRecursive <- is_rec -- ...binder isn't mentioned in RHS
1223 , all (isNothing . sig_fn) bndrs
1224 = addErrCtxt (patMonoBindsCtxt pat grhss) $
1225 do { (grhss', pat_ty) <- tcInfer $ \ exp_ty ->
1226 tcGRHSsPat grhss exp_ty
1227
1228 ; let exp_pat_ty :: Scaled ExpSigmaType
1229 exp_pat_ty = unrestricted (mkCheckExpType pat_ty)
1230 ; (pat', mbis) <- tcLetPat (const Nothing) no_gen pat exp_pat_ty $
1231 mapM lookupMBI bndrs
1232
1233 ; return ( unitBag $ L b_loc $
1234 PatBind { pat_lhs = pat', pat_rhs = grhss'
1235 , pat_ext = pat_ty, pat_ticks = ([],[]) }
1236
1237 , mbis ) }
1238 where
1239 bndrs = collectPatBinders CollNoDictBinders pat
1240
1241 -- GENERAL CASE
1242 tcMonoBinds _ sig_fn no_gen binds
1243 = do { tc_binds <- mapM (wrapLocMA (tcLhs sig_fn no_gen)) binds
1244
1245 -- Bring the monomorphic Ids, into scope for the RHSs
1246 ; let mono_infos = getMonoBindInfo tc_binds
1247 rhs_id_env = [ (name, mono_id)
1248 | MBI { mbi_poly_name = name
1249 , mbi_sig = mb_sig
1250 , mbi_mono_id = mono_id } <- mono_infos
1251 , case mb_sig of
1252 Just sig -> isPartialSig sig
1253 Nothing -> True ]
1254 -- A monomorphic binding for each term variable that lacks
1255 -- a complete type sig. (Ones with a sig are already in scope.)
1256
1257 ; traceTc "tcMonoBinds" $ vcat [ ppr n <+> ppr id <+> ppr (idType id)
1258 | (n,id) <- rhs_id_env]
1259 ; binds' <- tcExtendRecIds rhs_id_env $
1260 mapM (wrapLocMA tcRhs) tc_binds
1261
1262 ; return (listToBag binds', mono_infos) }
1263
1264 {- Note [Special case for non-recursive function bindings]
1265 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1266 In the special case of
1267 * A non-recursive FunBind
1268 * With no type signature
1269 we infer the type of the right hand side first (it may have a
1270 higher-rank type) and *then* make the monomorphic Id for the LHS e.g.
1271 f = \(x::forall a. a->a) -> <body>
1272
1273 We want to infer a higher-rank type for f
1274
1275 Note [Special case for non-recursive pattern bindings]
1276 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1277 In the special case of
1278 * A pattern binding
1279 * With no type signature for any of the binders
1280 we can /infer/ the type of the RHS, and /check/ the pattern
1281 against that type. For example (#18323)
1282
1283 ids :: [forall a. a -> a]
1284 combine :: (forall a . [a] -> a) -> [forall a. a -> a]
1285 -> ((forall a . [a] -> a), [forall a. a -> a])
1286
1287 (x,y) = combine head ids
1288
1289 with -XImpredicativeTypes we can infer a good type for
1290 (combine head ids), and use that to tell us the polymorphic
1291 types of x and y.
1292
1293 We don't need to check -XImpredicativeTypes beucase without it
1294 these types like [forall a. a->a] are illegal anyway, so this
1295 special case code only really has an effect if -XImpredicativeTypes
1296 is on. Small exception:
1297 (x) = e
1298 is currently treated as a pattern binding so, even absent
1299 -XImpredicativeTypes, we will get a small improvement in behaviour.
1300 But I don't think it's worth an extension flag.
1301
1302 Why do we require no type signatures on /any/ of the binders?
1303 Consider
1304 x :: forall a. a->a
1305 y :: forall a. a->a
1306 (x,y) = (id,id)
1307
1308 Here we should /check/ the RHS with expected type
1309 (forall a. a->a, forall a. a->a).
1310
1311 If we have no signatures, we can the approach of this Note
1312 to /infer/ the type of the RHS.
1313
1314 But what if we have some signatures, but not all? Say this:
1315 p :: forall a. a->a
1316 (p,q) = (id, (\(x::forall b. b->b). x True))
1317
1318 Here we want to push p's signature inwards, i.e. /checking/, to
1319 correctly elaborate 'id'. But we want to /infer/ q's higher rank
1320 type. There seems to be no way to do this. So currently we only
1321 switch to inference when we have no signature for any of the binders.
1322
1323 Note [fixM for rhs_ty in tcMonoBinds]
1324 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1325 In order to create mono_id we need rhs_ty but we don't have it yet,
1326 we only get it from tcMatchesFun later (which needs mono_id to put
1327 into HsMatchContext for pretty printing). To solve this, create
1328 a thunk of rhs_ty with fixM that we fill in later.
1329
1330 This is fine only because neither newLetBndr or tcMatchesFun look
1331 at the varType field of the Id. tcMatchesFun only looks at idName
1332 of mono_id.
1333
1334 Also see #20415 for the bigger picture of why tcMatchesFun needs
1335 mono_id in the first place.
1336 -}
1337
1338
1339 ------------------------
1340 -- tcLhs typechecks the LHS of the bindings, to construct the environment in which
1341 -- we typecheck the RHSs. Basically what we are doing is this: for each binder:
1342 -- if there's a signature for it, use the instantiated signature type
1343 -- otherwise invent a type variable
1344 -- You see that quite directly in the FunBind case.
1345 --
1346 -- But there's a complication for pattern bindings:
1347 -- data T = MkT (forall a. a->a)
1348 -- MkT f = e
1349 -- Here we can guess a type variable for the entire LHS (which will be refined to T)
1350 -- but we want to get (f::forall a. a->a) as the RHS environment.
1351 -- The simplest way to do this is to typecheck the pattern, and then look up the
1352 -- bound mono-ids. Then we want to retain the typechecked pattern to avoid re-doing
1353 -- it; hence the TcMonoBind data type in which the LHS is done but the RHS isn't
1354
1355 data TcMonoBind -- Half completed; LHS done, RHS not done
1356 = TcFunBind MonoBindInfo SrcSpan (MatchGroup GhcRn (LHsExpr GhcRn))
1357 | TcPatBind [MonoBindInfo] (LPat GhcTc) (GRHSs GhcRn (LHsExpr GhcRn))
1358 TcSigmaType
1359
1360 tcLhs :: TcSigFun -> LetBndrSpec -> HsBind GhcRn -> TcM TcMonoBind
1361 -- Only called with plan InferGen (LetBndrSpec = LetLclBndr)
1362 -- or NoGen (LetBndrSpec = LetGblBndr)
1363 -- CheckGen is used only for functions with a complete type signature,
1364 -- and tcPolyCheck doesn't use tcMonoBinds at all
1365
1366 tcLhs sig_fn no_gen (FunBind { fun_id = L nm_loc name
1367 , fun_matches = matches })
1368 | Just (TcIdSig sig) <- sig_fn name
1369 = -- There is a type signature.
1370 -- It must be partial; if complete we'd be in tcPolyCheck!
1371 -- e.g. f :: _ -> _
1372 -- f x = ...g...
1373 -- Just g = ...f...
1374 -- Hence always typechecked with InferGen
1375 do { mono_info <- tcLhsSigId no_gen (name, sig)
1376 ; return (TcFunBind mono_info (locA nm_loc) matches) }
1377
1378 | otherwise -- No type signature
1379 = do { mono_ty <- newOpenFlexiTyVarTy
1380 ; mono_id <- newLetBndr no_gen name Many mono_ty
1381 -- This ^ generates a binder with Many multiplicity because all
1382 -- let/where-binders are unrestricted. When we introduce linear let
1383 -- binders, we will need to retrieve the multiplicity information.
1384 ; let mono_info = MBI { mbi_poly_name = name
1385 , mbi_sig = Nothing
1386 , mbi_mono_id = mono_id }
1387 ; return (TcFunBind mono_info (locA nm_loc) matches) }
1388
1389 tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss })
1390 = -- See Note [Typechecking pattern bindings]
1391 do { sig_mbis <- mapM (tcLhsSigId no_gen) sig_names
1392
1393 ; let inst_sig_fun = lookupNameEnv $ mkNameEnv $
1394 [ (mbi_poly_name mbi, mbi_mono_id mbi)
1395 | mbi <- sig_mbis ]
1396
1397 -- See Note [Existentials in pattern bindings]
1398 ; ((pat', nosig_mbis), pat_ty)
1399 <- addErrCtxt (patMonoBindsCtxt pat grhss) $
1400 tcInfer $ \ exp_ty ->
1401 tcLetPat inst_sig_fun no_gen pat (unrestricted exp_ty) $
1402 -- The above inferred type get an unrestricted multiplicity. It may be
1403 -- worth it to try and find a finer-grained multiplicity here
1404 -- if examples warrant it.
1405 mapM lookupMBI nosig_names
1406
1407 ; let mbis = sig_mbis ++ nosig_mbis
1408
1409 ; traceTc "tcLhs" (vcat [ ppr id <+> dcolon <+> ppr (idType id)
1410 | mbi <- mbis, let id = mbi_mono_id mbi ]
1411 $$ ppr no_gen)
1412
1413 ; return (TcPatBind mbis pat' grhss pat_ty) }
1414 where
1415 bndr_names = collectPatBinders CollNoDictBinders pat
1416 (nosig_names, sig_names) = partitionWith find_sig bndr_names
1417
1418 find_sig :: Name -> Either Name (Name, TcIdSigInfo)
1419 find_sig name = case sig_fn name of
1420 Just (TcIdSig sig) -> Right (name, sig)
1421 _ -> Left name
1422
1423 tcLhs _ _ other_bind = pprPanic "tcLhs" (ppr other_bind)
1424 -- AbsBind, VarBind impossible
1425
1426 lookupMBI :: Name -> TcM MonoBindInfo
1427 -- After typechecking the pattern, look up the binder
1428 -- names that lack a signature, which the pattern has brought
1429 -- into scope.
1430 lookupMBI name
1431 = do { mono_id <- tcLookupId name
1432 ; return (MBI { mbi_poly_name = name
1433 , mbi_sig = Nothing
1434 , mbi_mono_id = mono_id }) }
1435
1436 -------------------
1437 tcLhsSigId :: LetBndrSpec -> (Name, TcIdSigInfo) -> TcM MonoBindInfo
1438 tcLhsSigId no_gen (name, sig)
1439 = do { inst_sig <- tcInstSig sig
1440 ; mono_id <- newSigLetBndr no_gen name inst_sig
1441 ; return (MBI { mbi_poly_name = name
1442 , mbi_sig = Just inst_sig
1443 , mbi_mono_id = mono_id }) }
1444
1445 ------------
1446 newSigLetBndr :: LetBndrSpec -> Name -> TcIdSigInst -> TcM TcId
1447 newSigLetBndr (LetGblBndr prags) name (TISI { sig_inst_sig = id_sig })
1448 | CompleteSig { sig_bndr = poly_id } <- id_sig
1449 = addInlinePrags poly_id (lookupPragEnv prags name)
1450 newSigLetBndr no_gen name (TISI { sig_inst_tau = tau })
1451 = newLetBndr no_gen name Many tau
1452 -- Binders with a signature are currently always of multiplicity
1453 -- Many. Because they come either from toplevel, let, or where
1454 -- declarations. Which are all unrestricted currently.
1455
1456 -------------------
1457 tcRhs :: TcMonoBind -> TcM (HsBind GhcTc)
1458 tcRhs (TcFunBind info@(MBI { mbi_sig = mb_sig, mbi_mono_id = mono_id })
1459 loc matches)
1460 = tcExtendIdBinderStackForRhs [info] $
1461 tcExtendTyVarEnvForRhs mb_sig $
1462 do { traceTc "tcRhs: fun bind" (ppr mono_id $$ ppr (idType mono_id))
1463 ; (co_fn, matches') <- tcMatchesFun (L (noAnnSrcSpan loc) mono_id)
1464 matches (mkCheckExpType $ idType mono_id)
1465 ; return ( FunBind { fun_id = L (noAnnSrcSpan loc) mono_id
1466 , fun_matches = matches'
1467 , fun_ext = co_fn
1468 , fun_tick = [] } ) }
1469
1470 tcRhs (TcPatBind infos pat' grhss pat_ty)
1471 = -- When we are doing pattern bindings we *don't* bring any scoped
1472 -- type variables into scope unlike function bindings
1473 -- Wny not? They are not completely rigid.
1474 -- That's why we have the special case for a single FunBind in tcMonoBinds
1475 tcExtendIdBinderStackForRhs infos $
1476 do { traceTc "tcRhs: pat bind" (ppr pat' $$ ppr pat_ty)
1477 ; grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $
1478 tcGRHSsPat grhss (mkCheckExpType pat_ty)
1479
1480 ; return ( PatBind { pat_lhs = pat', pat_rhs = grhss'
1481 , pat_ext = pat_ty
1482 , pat_ticks = ([],[]) } )}
1483
1484 tcExtendTyVarEnvForRhs :: Maybe TcIdSigInst -> TcM a -> TcM a
1485 tcExtendTyVarEnvForRhs Nothing thing_inside
1486 = thing_inside
1487 tcExtendTyVarEnvForRhs (Just sig) thing_inside
1488 = tcExtendTyVarEnvFromSig sig thing_inside
1489
1490 tcExtendTyVarEnvFromSig :: TcIdSigInst -> TcM a -> TcM a
1491 tcExtendTyVarEnvFromSig sig_inst thing_inside
1492 | TISI { sig_inst_skols = skol_prs, sig_inst_wcs = wcs } <- sig_inst
1493 = tcExtendNameTyVarEnv wcs $
1494 tcExtendNameTyVarEnv (mapSnd binderVar skol_prs) $
1495 thing_inside
1496
1497 tcExtendIdBinderStackForRhs :: [MonoBindInfo] -> TcM a -> TcM a
1498 -- See Note [Relevant bindings and the binder stack]
1499 tcExtendIdBinderStackForRhs infos thing_inside
1500 = tcExtendBinderStack [ TcIdBndr mono_id NotTopLevel
1501 | MBI { mbi_mono_id = mono_id } <- infos ]
1502 thing_inside
1503 -- NotTopLevel: it's a monomorphic binding
1504
1505 ---------------------
1506 getMonoBindInfo :: [LocatedA TcMonoBind] -> [MonoBindInfo]
1507 getMonoBindInfo tc_binds
1508 = foldr (get_info . unLoc) [] tc_binds
1509 where
1510 get_info (TcFunBind info _ _) rest = info : rest
1511 get_info (TcPatBind infos _ _ _) rest = infos ++ rest
1512
1513
1514 {- Note [Relevant bindings and the binder stack]
1515 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1516 When typecking a binding we extend the TcBinderStack for the RHS of
1517 the binding, with the /monomorphic/ Id. That way, if we have, say
1518 f = \x -> blah
1519 and something goes wrong in 'blah', we get a "relevant binding"
1520 looking like f :: alpha -> beta
1521 This applies if 'f' has a type signature too:
1522 f :: forall a. [a] -> [a]
1523 f x = True
1524 We can't unify True with [a], and a relevant binding is f :: [a] -> [a]
1525 If we had the *polymorphic* version of f in the TcBinderStack, it
1526 would not be reported as relevant, because its type is closed.
1527 (See TcErrors.relevantBindings.)
1528
1529 Note [Typechecking pattern bindings]
1530 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1531 Look at:
1532 - typecheck/should_compile/ExPat
1533 - #12427, typecheck/should_compile/T12427{a,b}
1534
1535 data T where
1536 MkT :: Integral a => a -> Int -> T
1537
1538 and suppose t :: T. Which of these pattern bindings are ok?
1539
1540 E1. let { MkT p _ = t } in <body>
1541
1542 E2. let { MkT _ q = t } in <body>
1543
1544 E3. let { MkT (toInteger -> r) _ = t } in <body>
1545
1546 * (E1) is clearly wrong because the existential 'a' escapes.
1547 What type could 'p' possibly have?
1548
1549 * (E2) is fine, despite the existential pattern, because
1550 q::Int, and nothing escapes.
1551
1552 * Even (E3) is fine. The existential pattern binds a dictionary
1553 for (Integral a) which the view pattern can use to convert the
1554 a-valued field to an Integer, so r :: Integer.
1555
1556 An easy way to see all three is to imagine the desugaring.
1557 For (E2) it would look like
1558 let q = case t of MkT _ q' -> q'
1559 in <body>
1560
1561
1562 We typecheck pattern bindings as follows. First tcLhs does this:
1563
1564 1. Take each type signature q :: ty, partial or complete, and
1565 instantiate it (with tcLhsSigId) to get a MonoBindInfo. This
1566 gives us a fresh "mono_id" qm :: instantiate(ty), where qm has
1567 a fresh name.
1568
1569 Any fresh unification variables in instantiate(ty) born here, not
1570 deep under implications as would happen if we allocated them when
1571 we encountered q during tcPat.
1572
1573 2. Build a little environment mapping "q" -> "qm" for those Ids
1574 with signatures (inst_sig_fun)
1575
1576 3. Invoke tcLetPat to typecheck the pattern.
1577
1578 - We pass in the current TcLevel. This is captured by
1579 GHC.Tc.Gen.Pat.tcLetPat, and put into the pc_lvl field of PatCtxt, in
1580 PatEnv.
1581
1582 - When tcPat finds an existential constructor, it binds fresh
1583 type variables and dictionaries as usual, increments the TcLevel,
1584 and emits an implication constraint.
1585
1586 - When we come to a binder (GHC.Tc.Gen.Pat.tcPatBndr), it looks it up
1587 in the little environment (the pc_sig_fn field of PatCtxt).
1588
1589 Success => There was a type signature, so just use it,
1590 checking compatibility with the expected type.
1591
1592 Failure => No type signature.
1593 Infer case: (happens only outside any constructor pattern)
1594 use a unification variable
1595 at the outer level pc_lvl
1596
1597 Check case: use promoteTcType to promote the type
1598 to the outer level pc_lvl. This is the
1599 place where we emit a constraint that'll blow
1600 up if existential capture takes place
1601
1602 Result: the type of the binder is always at pc_lvl. This is
1603 crucial.
1604
1605 4. Throughout, when we are making up an Id for the pattern-bound variables
1606 (newLetBndr), we have two cases:
1607
1608 - If we are generalising (generalisation plan is InferGen or
1609 CheckGen), then the let_bndr_spec will be LetLclBndr. In that case
1610 we want to bind a cloned, local version of the variable, with the
1611 type given by the pattern context, *not* by the signature (even if
1612 there is one; see #7268). The mkExport part of the
1613 generalisation step will do the checking and impedance matching
1614 against the signature.
1615
1616 - If for some reason we are not generalising (plan = NoGen), the
1617 LetBndrSpec will be LetGblBndr. In that case we must bind the
1618 global version of the Id, and do so with precisely the type given
1619 in the signature. (Then we unify with the type from the pattern
1620 context type.)
1621
1622
1623 And that's it! The implication constraints check for the skolem
1624 escape. It's quite simple and neat, and more expressive than before
1625 e.g. GHC 8.0 rejects (E2) and (E3).
1626
1627 Example for (E1), starting at level 1. We generate
1628 p :: beta:1, with constraints (forall:3 a. Integral a => a ~ beta)
1629 The (a~beta) can't float (because of the 'a'), nor be solved (because
1630 beta is untouchable.)
1631
1632 Example for (E2), we generate
1633 q :: beta:1, with constraint (forall:3 a. Integral a => Int ~ beta)
1634 The beta is untouchable, but floats out of the constraint and can
1635 be solved absolutely fine.
1636
1637
1638 ************************************************************************
1639 * *
1640 Generalisation
1641 * *
1642 ********************************************************************* -}
1643
1644 data GeneralisationPlan
1645 = NoGen -- No generalisation, no AbsBinds
1646
1647 | InferGen -- Implicit generalisation; there is an AbsBinds
1648 Bool -- True <=> apply the MR; generalise only unconstrained type vars
1649
1650 | CheckGen (LHsBind GhcRn) TcIdSigInfo
1651 -- One FunBind with a signature
1652 -- Explicit generalisation
1653
1654 -- A consequence of the no-AbsBinds choice (NoGen) is that there is
1655 -- no "polymorphic Id" and "monmomorphic Id"; there is just the one
1656
1657 instance Outputable GeneralisationPlan where
1658 ppr NoGen = text "NoGen"
1659 ppr (InferGen b) = text "InferGen" <+> ppr b
1660 ppr (CheckGen _ s) = text "CheckGen" <+> ppr s
1661
1662 decideGeneralisationPlan
1663 :: DynFlags -> [LHsBind GhcRn] -> IsGroupClosed -> TcSigFun
1664 -> GeneralisationPlan
1665 decideGeneralisationPlan dflags lbinds closed sig_fn
1666 | has_partial_sigs = InferGen (and partial_sig_mrs)
1667 | Just (bind, sig) <- one_funbind_with_sig = CheckGen bind sig
1668 | do_not_generalise closed = NoGen
1669 | otherwise = InferGen mono_restriction
1670 where
1671 binds = map unLoc lbinds
1672
1673 partial_sig_mrs :: [Bool]
1674 -- One for each partial signature (so empty => no partial sigs)
1675 -- The Bool is True if the signature has no constraint context
1676 -- so we should apply the MR
1677 -- See Note [Partial type signatures and generalisation]
1678 partial_sig_mrs
1679 = [ null $ fromMaybeContext mtheta
1680 | TcIdSig (PartialSig { psig_hs_ty = hs_ty })
1681 <- mapMaybe sig_fn (collectHsBindListBinders CollNoDictBinders lbinds)
1682 , let (mtheta, _) = splitLHsQualTy (hsSigWcType hs_ty) ]
1683
1684 has_partial_sigs = not (null partial_sig_mrs)
1685
1686 mono_restriction = xopt LangExt.MonomorphismRestriction dflags
1687 && any restricted binds
1688
1689 do_not_generalise (IsGroupClosed _ True) = False
1690 -- The 'True' means that all of the group's
1691 -- free vars have ClosedTypeId=True; so we can ignore
1692 -- -XMonoLocalBinds, and generalise anyway
1693 do_not_generalise _ = xopt LangExt.MonoLocalBinds dflags
1694
1695 -- With OutsideIn, all nested bindings are monomorphic
1696 -- except a single function binding with a signature
1697 one_funbind_with_sig
1698 | [lbind@(L _ (FunBind { fun_id = v }))] <- lbinds
1699 , Just (TcIdSig sig) <- sig_fn (unLoc v)
1700 = Just (lbind, sig)
1701 | otherwise
1702 = Nothing
1703
1704 -- The Haskell 98 monomorphism restriction
1705 restricted (PatBind {}) = True
1706 restricted (VarBind { var_id = v }) = no_sig v
1707 restricted (FunBind { fun_id = v, fun_matches = m }) = restricted_match m
1708 && no_sig (unLoc v)
1709 restricted b = pprPanic "isRestrictedGroup/unrestricted" (ppr b)
1710
1711 restricted_match mg = matchGroupArity mg == 0
1712 -- No args => like a pattern binding
1713 -- Some args => a function binding
1714
1715 no_sig n = not (hasCompleteSig sig_fn n)
1716
1717 isClosedBndrGroup :: TcTypeEnv -> Bag (LHsBind GhcRn) -> IsGroupClosed
1718 isClosedBndrGroup type_env binds
1719 = IsGroupClosed fv_env type_closed
1720 where
1721 type_closed = allUFM (nameSetAll is_closed_type_id) fv_env
1722
1723 fv_env :: NameEnv NameSet
1724 fv_env = mkNameEnv $ concatMap (bindFvs . unLoc) binds
1725
1726 bindFvs :: HsBindLR GhcRn GhcRn -> [(Name, NameSet)]
1727 bindFvs (FunBind { fun_id = L _ f
1728 , fun_ext = fvs })
1729 = let open_fvs = get_open_fvs fvs
1730 in [(f, open_fvs)]
1731 bindFvs (PatBind { pat_lhs = pat, pat_ext = fvs })
1732 = let open_fvs = get_open_fvs fvs
1733 in [(b, open_fvs) | b <- collectPatBinders CollNoDictBinders pat]
1734 bindFvs _
1735 = []
1736
1737 get_open_fvs fvs = filterNameSet (not . is_closed) fvs
1738
1739 is_closed :: Name -> ClosedTypeId
1740 is_closed name
1741 | Just thing <- lookupNameEnv type_env name
1742 = case thing of
1743 AGlobal {} -> True
1744 ATcId { tct_info = ClosedLet } -> True
1745 _ -> False
1746
1747 | otherwise
1748 = True -- The free-var set for a top level binding mentions
1749
1750
1751 is_closed_type_id :: Name -> Bool
1752 -- We're already removed Global and ClosedLet Ids
1753 is_closed_type_id name
1754 | Just thing <- lookupNameEnv type_env name
1755 = case thing of
1756 ATcId { tct_info = NonClosedLet _ cl } -> cl
1757 ATcId { tct_info = NotLetBound } -> False
1758 ATyVar {} -> False
1759 -- In-scope type variables are not closed!
1760 _ -> pprPanic "is_closed_id" (ppr name)
1761
1762 | otherwise
1763 = True -- The free-var set for a top level binding mentions
1764 -- imported things too, so that we can report unused imports
1765 -- These won't be in the local type env.
1766 -- Ditto class method etc from the current module
1767
1768
1769 {- *********************************************************************
1770 * *
1771 Error contexts and messages
1772 * *
1773 ********************************************************************* -}
1774
1775 -- This one is called on LHS, when pat and grhss are both Name
1776 -- and on RHS, when pat is TcId and grhss is still Name
1777 patMonoBindsCtxt :: (OutputableBndrId p)
1778 => LPat (GhcPass p) -> GRHSs GhcRn (LHsExpr GhcRn) -> SDoc
1779 patMonoBindsCtxt pat grhss
1780 = hang (text "In a pattern binding:") 2 (pprPatBind pat grhss)