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