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