Remove HasSourceText and SourceTextX classes
[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, tcRecSelBinds,
13 tcHsBootSigs, tcPolyCheck,
14 tcVectDecls, 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 ( tcInferPatSynDecl, tcCheckPatSynDecl
23 , 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 ListSetOps
57 import ErrUtils
58 import Digraph
59 import Maybes
60 import Util
61 import BasicTypes
62 import Outputable
63 import PrelNames( ipClassName )
64 import TcValidity (checkValidType)
65 import UniqFM
66 import UniqSet
67 import qualified GHC.LanguageExtensions as LangExt
68 import ConLike
69
70 import Control.Monad
71 import Data.List.NonEmpty ( NonEmpty(..) )
72
73 #include "HsVersions.h"
74
75 {- *********************************************************************
76 * *
77 A useful helper function
78 * *
79 ********************************************************************* -}
80
81 addTypecheckedBinds :: TcGblEnv -> [LHsBinds GhcTc] -> TcGblEnv
82 addTypecheckedBinds tcg_env binds
83 | isHsBootOrSig (tcg_src tcg_env) = tcg_env
84 -- Do not add the code for record-selector bindings
85 -- when compiling hs-boot files
86 | otherwise = tcg_env { tcg_binds = foldr unionBags
87 (tcg_binds tcg_env)
88 binds }
89
90 {-
91 ************************************************************************
92 * *
93 \subsection{Type-checking bindings}
94 * *
95 ************************************************************************
96
97 @tcBindsAndThen@ typechecks a @HsBinds@. The "and then" part is because
98 it needs to know something about the {\em usage} of the things bound,
99 so that it can create specialisations of them. So @tcBindsAndThen@
100 takes a function which, given an extended environment, E, typechecks
101 the scope of the bindings returning a typechecked thing and (most
102 important) an LIE. It is this LIE which is then used as the basis for
103 specialising the things bound.
104
105 @tcBindsAndThen@ also takes a "combiner" which glues together the
106 bindings and the "thing" to make a new "thing".
107
108 The real work is done by @tcBindWithSigsAndThen@.
109
110 Recursive and non-recursive binds are handled in essentially the same
111 way: because of uniques there are no scoping issues left. The only
112 difference is that non-recursive bindings can bind primitive values.
113
114 Even for non-recursive binding groups we add typings for each binder
115 to the LVE for the following reason. When each individual binding is
116 checked the type of its LHS is unified with that of its RHS; and
117 type-checking the LHS of course requires that the binder is in scope.
118
119 At the top-level the LIE is sure to contain nothing but constant
120 dictionaries, which we resolve at the module level.
121
122 Note [Polymorphic recursion]
123 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
124 The game plan for polymorphic recursion in the code above is
125
126 * Bind any variable for which we have a type signature
127 to an Id with a polymorphic type. Then when type-checking
128 the RHSs we'll make a full polymorphic call.
129
130 This fine, but if you aren't a bit careful you end up with a horrendous
131 amount of partial application and (worse) a huge space leak. For example:
132
133 f :: Eq a => [a] -> [a]
134 f xs = ...f...
135
136 If we don't take care, after typechecking we get
137
138 f = /\a -> \d::Eq a -> let f' = f a d
139 in
140 \ys:[a] -> ...f'...
141
142 Notice the stupid construction of (f a d), which is of course
143 identical to the function we're executing. In this case, the
144 polymorphic recursion isn't being used (but that's a very common case).
145 This can lead to a massive space leak, from the following top-level defn
146 (post-typechecking)
147
148 ff :: [Int] -> [Int]
149 ff = f Int dEqInt
150
151 Now (f dEqInt) evaluates to a lambda that has f' as a free variable; but
152 f' is another thunk which evaluates to the same thing... and you end
153 up with a chain of identical values all hung onto by the CAF ff.
154
155 ff = f Int dEqInt
156
157 = let f' = f Int dEqInt in \ys. ...f'...
158
159 = let f' = let f' = f Int dEqInt in \ys. ...f'...
160 in \ys. ...f'...
161
162 Etc.
163
164 NOTE: a bit of arity anaysis would push the (f a d) inside the (\ys...),
165 which would make the space leak go away in this case
166
167 Solution: when typechecking the RHSs we always have in hand the
168 *monomorphic* Ids for each binding. So we just need to make sure that
169 if (Method f a d) shows up in the constraints emerging from (...f...)
170 we just use the monomorphic Id. We achieve this by adding monomorphic Ids
171 to the "givens" when simplifying constraints. That's what the "lies_avail"
172 is doing.
173
174 Then we get
175
176 f = /\a -> \d::Eq a -> letrec
177 fm = \ys:[a] -> ...fm...
178 in
179 fm
180 -}
181
182 tcTopBinds :: [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn]
183 -> TcM (TcGblEnv, TcLclEnv)
184 -- The TcGblEnv contains the new tcg_binds and tcg_spects
185 -- The TcLclEnv has an extended type envt for the new bindings
186 tcTopBinds binds sigs
187 = do { -- Pattern synonym bindings populate the global environment
188 (binds', (tcg_env, tcl_env)) <- tcValBinds TopLevel binds sigs $
189 do { gbl <- getGblEnv
190 ; lcl <- getLclEnv
191 ; return (gbl, lcl) }
192 ; specs <- tcImpPrags sigs -- SPECIALISE prags for imported Ids
193
194 ; complete_matches <- setEnvs (tcg_env, tcl_env) $ tcCompleteSigs sigs
195 ; traceTc "complete_matches" (ppr binds $$ ppr sigs)
196 ; traceTc "complete_matches" (ppr complete_matches)
197
198 ; let { tcg_env' = tcg_env { tcg_imp_specs
199 = specs ++ tcg_imp_specs tcg_env
200 , tcg_complete_matches
201 = complete_matches
202 ++ tcg_complete_matches tcg_env }
203 `addTypecheckedBinds` map snd binds' }
204
205 ; return (tcg_env', tcl_env) }
206 -- The top level bindings are flattened into a giant
207 -- implicitly-mutually-recursive LHsBinds
208
209
210 -- Note [Typechecking Complete Matches]
211 -- Much like when a user bundled a pattern synonym, the result types of
212 -- all the constructors in the match pragma must be consistent.
213 --
214 -- If we allowed pragmas with inconsistent types then it would be
215 -- impossible to ever match every constructor in the list and so
216 -- the pragma would be useless.
217
218
219
220
221
222 -- This is only used in `tcCompleteSig`. We fold over all the conlikes,
223 -- this accumulator keeps track of the first `ConLike` with a concrete
224 -- return type. After fixing the return type, all other constructors with
225 -- a fixed return type must agree with this.
226 --
227 -- The fields of `Fixed` cache the first conlike and its return type so
228 -- that that we can compare all the other conlikes to it. The conlike is
229 -- stored for error messages.
230 --
231 -- `Nothing` in the case that the type is fixed by a type signature
232 data CompleteSigType = AcceptAny | Fixed (Maybe ConLike) TyCon
233
234 tcCompleteSigs :: [LSig GhcRn] -> TcM [CompleteMatch]
235 tcCompleteSigs sigs =
236 let
237 doOne :: Sig GhcRn -> TcM (Maybe CompleteMatch)
238 doOne c@(CompleteMatchSig _ lns mtc)
239 = fmap Just $ do
240 addErrCtxt (text "In" <+> ppr c) $
241 case mtc of
242 Nothing -> infer_complete_match
243 Just tc -> check_complete_match tc
244 where
245
246 checkCLTypes acc = foldM checkCLType (acc, []) (unLoc lns)
247
248 infer_complete_match = do
249 (res, cls) <- checkCLTypes AcceptAny
250 case res of
251 AcceptAny -> failWithTc ambiguousError
252 Fixed _ tc -> return $ mkMatch cls tc
253
254 check_complete_match tc_name = do
255 ty_con <- tcLookupLocatedTyCon tc_name
256 (_, cls) <- checkCLTypes (Fixed Nothing ty_con)
257 return $ mkMatch cls ty_con
258
259 mkMatch :: [ConLike] -> TyCon -> CompleteMatch
260 mkMatch cls ty_con = CompleteMatch {
261 completeMatchConLikes = map conLikeName cls,
262 completeMatchTyCon = tyConName ty_con
263 }
264 doOne _ = return Nothing
265
266 ambiguousError :: SDoc
267 ambiguousError =
268 text "A type signature must be provided for a set of polymorphic"
269 <+> text "pattern synonyms."
270
271
272 -- See note [Typechecking Complete Matches]
273 checkCLType :: (CompleteSigType, [ConLike]) -> Located Name
274 -> TcM (CompleteSigType, [ConLike])
275 checkCLType (cst, cs) n = do
276 cl <- addLocM tcLookupConLike n
277 let (_,_,_,_,_,_, res_ty) = conLikeFullSig cl
278 res_ty_con = fst <$> splitTyConApp_maybe res_ty
279 case (cst, res_ty_con) of
280 (AcceptAny, Nothing) -> return (AcceptAny, cl:cs)
281 (AcceptAny, Just tc) -> return (Fixed (Just cl) tc, cl:cs)
282 (Fixed mfcl tc, Nothing) -> return (Fixed mfcl tc, cl:cs)
283 (Fixed mfcl tc, Just tc') ->
284 if tc == tc'
285 then return (Fixed mfcl tc, cl:cs)
286 else case mfcl of
287 Nothing ->
288 addErrCtxt (text "In" <+> ppr cl) $
289 failWithTc typeSigErrMsg
290 Just cl -> failWithTc (errMsg cl)
291 where
292 typeSigErrMsg :: SDoc
293 typeSigErrMsg =
294 text "Couldn't match expected type"
295 <+> quotes (ppr tc)
296 <+> text "with"
297 <+> quotes (ppr tc')
298
299 errMsg :: ConLike -> SDoc
300 errMsg fcl =
301 text "Cannot form a group of complete patterns from patterns"
302 <+> quotes (ppr fcl) <+> text "and" <+> quotes (ppr cl)
303 <+> text "as they match different type constructors"
304 <+> parens (quotes (ppr tc)
305 <+> text "resp."
306 <+> quotes (ppr tc'))
307 in mapMaybeM (addLocM doOne) sigs
308
309 tcRecSelBinds :: HsValBinds GhcRn -> TcM TcGblEnv
310 tcRecSelBinds (ValBindsOut binds sigs)
311 = tcExtendGlobalValEnv [sel_id | L _ (IdSig sel_id) <- sigs] $
312 do { (rec_sel_binds, tcg_env) <- discardWarnings $
313 tcValBinds TopLevel binds sigs getGblEnv
314 ; let tcg_env' = tcg_env `addTypecheckedBinds` map snd rec_sel_binds
315 ; return tcg_env' }
316 tcRecSelBinds (ValBindsIn {}) = panic "tcRecSelBinds"
317
318 tcHsBootSigs :: [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn] -> TcM [Id]
319 -- A hs-boot file has only one BindGroup, and it only has type
320 -- signatures in it. The renamer checked all this
321 tcHsBootSigs binds sigs
322 = do { checkTc (null binds) badBootDeclErr
323 ; concat <$> mapM (addLocM tc_boot_sig) (filter isTypeLSig sigs) }
324 where
325 tc_boot_sig (TypeSig lnames hs_ty) = mapM f lnames
326 where
327 f (L _ name)
328 = do { sigma_ty <- tcHsSigWcType (FunSigCtxt name False) hs_ty
329 ; return (mkVanillaGlobal name sigma_ty) }
330 -- Notice that we make GlobalIds, not LocalIds
331 tc_boot_sig s = pprPanic "tcHsBootSigs/tc_boot_sig" (ppr s)
332
333 badBootDeclErr :: MsgDoc
334 badBootDeclErr = text "Illegal declarations in an hs-boot file"
335
336 ------------------------
337 tcLocalBinds :: HsLocalBinds GhcRn -> TcM thing
338 -> TcM (HsLocalBinds GhcTcId, thing)
339
340 tcLocalBinds EmptyLocalBinds thing_inside
341 = do { thing <- thing_inside
342 ; return (EmptyLocalBinds, thing) }
343
344 tcLocalBinds (HsValBinds (ValBindsOut binds sigs)) thing_inside
345 = do { (binds', thing) <- tcValBinds NotTopLevel binds sigs thing_inside
346 ; return (HsValBinds (ValBindsOut binds' sigs), thing) }
347 tcLocalBinds (HsValBinds (ValBindsIn {})) _ = panic "tcLocalBinds"
348
349 tcLocalBinds (HsIPBinds (IPBinds ip_binds _)) thing_inside
350 = do { ipClass <- tcLookupClass ipClassName
351 ; (given_ips, ip_binds') <-
352 mapAndUnzipM (wrapLocSndM (tc_ip_bind ipClass)) ip_binds
353
354 -- If the binding binds ?x = E, we must now
355 -- discharge any ?x constraints in expr_lie
356 -- See Note [Implicit parameter untouchables]
357 ; (ev_binds, result) <- checkConstraints (IPSkol ips)
358 [] given_ips thing_inside
359
360 ; return (HsIPBinds (IPBinds ip_binds' ev_binds), result) }
361 where
362 ips = [ip | L _ (IPBind (Left (L _ ip)) _) <- ip_binds]
363
364 -- I wonder if we should do these one at at time
365 -- Consider ?x = 4
366 -- ?y = ?x + 1
367 tc_ip_bind ipClass (IPBind (Left (L _ ip)) expr)
368 = do { ty <- newOpenFlexiTyVarTy
369 ; let p = mkStrLitTy $ hsIPNameFS ip
370 ; ip_id <- newDict ipClass [ p, ty ]
371 ; expr' <- tcMonoExpr expr (mkCheckExpType ty)
372 ; let d = toDict ipClass p ty `fmap` expr'
373 ; return (ip_id, (IPBind (Right ip_id) d)) }
374 tc_ip_bind _ (IPBind (Right {}) _) = panic "tc_ip_bind"
375
376 -- Coerces a `t` into a dictionry for `IP "x" t`.
377 -- co : t -> IP "x" t
378 toDict ipClass x ty = mkHsWrap $ mkWpCastR $
379 wrapIP $ mkClassPred ipClass [x,ty]
380
381 {- Note [Implicit parameter untouchables]
382 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
383 We add the type variables in the types of the implicit parameters
384 as untouchables, not so much because we really must not unify them,
385 but rather because we otherwise end up with constraints like this
386 Num alpha, Implic { wanted = alpha ~ Int }
387 The constraint solver solves alpha~Int by unification, but then
388 doesn't float that solved constraint out (it's not an unsolved
389 wanted). Result disaster: the (Num alpha) is again solved, this
390 time by defaulting. No no no.
391
392 However [Oct 10] this is all handled automatically by the
393 untouchable-range idea.
394 -}
395
396 tcValBinds :: TopLevelFlag
397 -> [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn]
398 -> TcM thing
399 -> TcM ([(RecFlag, LHsBinds GhcTcId)], thing)
400
401 tcValBinds top_lvl binds sigs thing_inside
402 = do { let patsyns = getPatSynBinds binds
403
404 -- Typecheck the signature
405 ; (poly_ids, sig_fn) <- tcAddPatSynPlaceholders patsyns $
406 tcTySigs sigs
407
408 ; let prag_fn = mkPragEnv sigs (foldr (unionBags . snd) emptyBag binds)
409
410 -- Extend the envt right away with all the Ids
411 -- declared with complete type signatures
412 -- Do not extend the TcBinderStack; instead
413 -- we extend it on a per-rhs basis in tcExtendForRhs
414 ; tcExtendSigIds top_lvl poly_ids $ do
415 { (binds', (extra_binds', thing)) <- tcBindGroups top_lvl sig_fn prag_fn binds $ do
416 { thing <- thing_inside
417 -- See Note [Pattern synonym builders don't yield dependencies]
418 -- in RnBinds
419 ; patsyn_builders <- mapM tcPatSynBuilderBind patsyns
420 ; let extra_binds = [ (NonRecursive, builder) | builder <- patsyn_builders ]
421 ; return (extra_binds, thing) }
422 ; return (binds' ++ extra_binds', thing) }}
423
424 ------------------------
425 tcBindGroups :: TopLevelFlag -> TcSigFun -> TcPragEnv
426 -> [(RecFlag, LHsBinds GhcRn)] -> TcM thing
427 -> TcM ([(RecFlag, LHsBinds GhcTcId)], thing)
428 -- Typecheck a whole lot of value bindings,
429 -- one strongly-connected component at a time
430 -- Here a "strongly connected component" has the strightforward
431 -- meaning of a group of bindings that mention each other,
432 -- ignoring type signatures (that part comes later)
433
434 tcBindGroups _ _ _ [] thing_inside
435 = do { thing <- thing_inside
436 ; return ([], thing) }
437
438 tcBindGroups top_lvl sig_fn prag_fn (group : groups) thing_inside
439 = do { -- See Note [Closed binder groups]
440 type_env <- getLclTypeEnv
441 ; let closed = isClosedBndrGroup type_env (snd group)
442 ; (group', (groups', thing))
443 <- tc_group top_lvl sig_fn prag_fn group closed $
444 tcBindGroups top_lvl sig_fn prag_fn groups thing_inside
445 ; return (group' ++ groups', thing) }
446
447 -- Note [Closed binder groups]
448 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~
449 --
450 -- A mutually recursive group is "closed" if all of the free variables of
451 -- the bindings are closed. For example
452 --
453 -- > h = \x -> let f = ...g...
454 -- > g = ....f...x...
455 -- > in ...
456 --
457 -- Here @g@ is not closed because it mentions @x@; and hence neither is @f@
458 -- closed.
459 --
460 -- So we need to compute closed-ness on each strongly connected components,
461 -- before we sub-divide it based on what type signatures it has.
462 --
463
464 ------------------------
465 tc_group :: forall thing.
466 TopLevelFlag -> TcSigFun -> TcPragEnv
467 -> (RecFlag, LHsBinds GhcRn) -> IsGroupClosed -> TcM thing
468 -> TcM ([(RecFlag, LHsBinds GhcTcId)], thing)
469
470 -- Typecheck one strongly-connected component of the original program.
471 -- We get a list of groups back, because there may
472 -- be specialisations etc as well
473
474 tc_group top_lvl sig_fn prag_fn (NonRecursive, binds) closed thing_inside
475 -- A single non-recursive binding
476 -- We want to keep non-recursive things non-recursive
477 -- so that we desugar unlifted bindings correctly
478 = do { let bind = case bagToList binds of
479 [bind] -> bind
480 [] -> panic "tc_group: empty list of binds"
481 _ -> panic "tc_group: NonRecursive binds is not a singleton bag"
482 ; (bind', thing) <- tc_single top_lvl sig_fn prag_fn bind closed
483 thing_inside
484 ; return ( [(NonRecursive, bind')], thing) }
485
486 tc_group top_lvl sig_fn prag_fn (Recursive, binds) closed thing_inside
487 = -- To maximise polymorphism, we do a new
488 -- strongly-connected-component analysis, this time omitting
489 -- any references to variables with type signatures.
490 -- (This used to be optional, but isn't now.)
491 -- See Note [Polymorphic recursion] in HsBinds.
492 do { traceTc "tc_group rec" (pprLHsBinds binds)
493 ; when hasPatSyn $ recursivePatSynErr binds
494 ; (binds1, thing) <- go sccs
495 ; return ([(Recursive, binds1)], thing) }
496 -- Rec them all together
497 where
498 hasPatSyn = anyBag (isPatSyn . unLoc) binds
499 isPatSyn PatSynBind{} = True
500 isPatSyn _ = False
501
502 sccs :: [SCC (LHsBind GhcRn)]
503 sccs = stronglyConnCompFromEdgedVerticesUniq (mkEdges sig_fn binds)
504
505 go :: [SCC (LHsBind GhcRn)] -> TcM (LHsBinds GhcTcId, thing)
506 go (scc:sccs) = do { (binds1, ids1) <- tc_scc scc
507 ; (binds2, thing) <- tcExtendLetEnv top_lvl sig_fn
508 closed ids1 $
509 go sccs
510 ; return (binds1 `unionBags` binds2, thing) }
511 go [] = do { thing <- thing_inside; return (emptyBag, thing) }
512
513 tc_scc (AcyclicSCC bind) = tc_sub_group NonRecursive [bind]
514 tc_scc (CyclicSCC binds) = tc_sub_group Recursive binds
515
516 tc_sub_group rec_tc binds =
517 tcPolyBinds sig_fn prag_fn Recursive rec_tc closed binds
518
519 recursivePatSynErr :: OutputableBndrId name => LHsBinds name -> TcM a
520 recursivePatSynErr binds
521 = failWithTc $
522 hang (text "Recursive pattern synonym definition with following bindings:")
523 2 (vcat $ map pprLBind . bagToList $ binds)
524 where
525 pprLoc loc = parens (text "defined at" <+> ppr loc)
526 pprLBind (L loc bind) = pprWithCommas ppr (collectHsBindBinders bind) <+>
527 pprLoc loc
528
529 tc_single :: forall thing.
530 TopLevelFlag -> TcSigFun -> TcPragEnv
531 -> LHsBind GhcRn -> IsGroupClosed -> TcM thing
532 -> TcM (LHsBinds GhcTcId, thing)
533 tc_single _top_lvl sig_fn _prag_fn
534 (L _ (PatSynBind psb@PSB{ psb_id = L _ name }))
535 _ thing_inside
536 = do { (aux_binds, tcg_env) <- tc_pat_syn_decl
537 ; thing <- setGblEnv tcg_env thing_inside
538 ; return (aux_binds, thing)
539 }
540 where
541 tc_pat_syn_decl :: TcM (LHsBinds GhcTcId, TcGblEnv)
542 tc_pat_syn_decl = case sig_fn name of
543 Nothing -> tcInferPatSynDecl psb
544 Just (TcPatSynSig tpsi) -> tcCheckPatSynDecl psb tpsi
545 Just _ -> panic "tc_single"
546
547 tc_single top_lvl sig_fn prag_fn lbind closed thing_inside
548 = do { (binds1, ids) <- tcPolyBinds sig_fn prag_fn
549 NonRecursive NonRecursive
550 closed
551 [lbind]
552 ; thing <- tcExtendLetEnv top_lvl sig_fn closed ids thing_inside
553 ; return (binds1, thing) }
554
555 ------------------------
556 type BKey = Int -- Just number off the bindings
557
558 mkEdges :: TcSigFun -> LHsBinds GhcRn -> [Node BKey (LHsBind GhcRn)]
559 -- See Note [Polymorphic recursion] in HsBinds.
560 mkEdges sig_fn binds
561 = [ DigraphNode bind key [key | n <- nonDetEltsUniqSet (bind_fvs (unLoc bind)),
562 Just key <- [lookupNameEnv key_map n], no_sig n ]
563 | (bind, key) <- keyd_binds
564 ]
565 -- It's OK to use nonDetEltsUFM here as stronglyConnCompFromEdgedVertices
566 -- is still deterministic even if the edges are in nondeterministic order
567 -- as explained in Note [Deterministic SCC] in Digraph.
568 where
569 no_sig :: Name -> Bool
570 no_sig n = not (hasCompleteSig sig_fn n)
571
572 keyd_binds = bagToList binds `zip` [0::BKey ..]
573
574 key_map :: NameEnv BKey -- Which binding it comes from
575 key_map = mkNameEnv [(bndr, key) | (L _ bind, key) <- keyd_binds
576 , bndr <- collectHsBindBinders bind ]
577
578 ------------------------
579 tcPolyBinds :: TcSigFun -> TcPragEnv
580 -> RecFlag -- Whether the group is really recursive
581 -> RecFlag -- Whether it's recursive after breaking
582 -- dependencies based on type signatures
583 -> IsGroupClosed -- Whether the group is closed
584 -> [LHsBind GhcRn] -- None are PatSynBind
585 -> TcM (LHsBinds GhcTcId, [TcId])
586
587 -- Typechecks a single bunch of values bindings all together,
588 -- and generalises them. The bunch may be only part of a recursive
589 -- group, because we use type signatures to maximise polymorphism
590 --
591 -- Returns a list because the input may be a single non-recursive binding,
592 -- in which case the dependency order of the resulting bindings is
593 -- important.
594 --
595 -- Knows nothing about the scope of the bindings
596 -- None of the bindings are pattern synonyms
597
598 tcPolyBinds sig_fn prag_fn rec_group rec_tc closed bind_list
599 = setSrcSpan loc $
600 recoverM (recoveryCode binder_names sig_fn) $ do
601 -- Set up main recover; take advantage of any type sigs
602
603 { traceTc "------------------------------------------------" Outputable.empty
604 ; traceTc "Bindings for {" (ppr binder_names)
605 ; dflags <- getDynFlags
606 ; let plan = decideGeneralisationPlan dflags bind_list closed sig_fn
607 ; traceTc "Generalisation plan" (ppr plan)
608 ; result@(_, poly_ids) <- case plan of
609 NoGen -> tcPolyNoGen rec_tc prag_fn sig_fn bind_list
610 InferGen mn -> tcPolyInfer rec_tc prag_fn sig_fn mn bind_list
611 CheckGen lbind sig -> tcPolyCheck prag_fn sig lbind
612
613 ; traceTc "} End of bindings for" (vcat [ ppr binder_names, ppr rec_group
614 , vcat [ppr id <+> ppr (idType id) | id <- poly_ids]
615 ])
616
617 ; return result }
618 where
619 binder_names = collectHsBindListBinders bind_list
620 loc = foldr1 combineSrcSpans (map getLoc bind_list)
621 -- The mbinds have been dependency analysed and
622 -- may no longer be adjacent; so find the narrowest
623 -- span that includes them all
624
625 --------------
626 -- If typechecking the binds fails, then return with each
627 -- signature-less binder given type (forall a.a), to minimise
628 -- subsequent error messages
629 recoveryCode :: [Name] -> TcSigFun -> TcM (LHsBinds GhcTcId, [Id])
630 recoveryCode binder_names sig_fn
631 = do { traceTc "tcBindsWithSigs: error recovery" (ppr binder_names)
632 ; let poly_ids = map mk_dummy binder_names
633 ; return (emptyBag, poly_ids) }
634 where
635 mk_dummy name
636 | Just sig <- sig_fn name
637 , Just poly_id <- completeSigPolyId_maybe sig
638 = poly_id
639 | otherwise
640 = mkLocalId name forall_a_a
641
642 forall_a_a :: TcType
643 forall_a_a = mkSpecForAllTys [runtimeRep1TyVar, openAlphaTyVar] openAlphaTy
644
645 {- *********************************************************************
646 * *
647 tcPolyNoGen
648 * *
649 ********************************************************************* -}
650
651 tcPolyNoGen -- No generalisation whatsoever
652 :: RecFlag -- Whether it's recursive after breaking
653 -- dependencies based on type signatures
654 -> TcPragEnv -> TcSigFun
655 -> [LHsBind GhcRn]
656 -> TcM (LHsBinds GhcTcId, [TcId])
657
658 tcPolyNoGen rec_tc prag_fn tc_sig_fn bind_list
659 = do { (binds', mono_infos) <- tcMonoBinds rec_tc tc_sig_fn
660 (LetGblBndr prag_fn)
661 bind_list
662 ; mono_ids' <- mapM tc_mono_info mono_infos
663 ; return (binds', mono_ids') }
664 where
665 tc_mono_info (MBI { mbi_poly_name = name, mbi_mono_id = mono_id })
666 = do { _specs <- tcSpecPrags mono_id (lookupPragEnv prag_fn name)
667 ; return mono_id }
668 -- NB: tcPrags generates error messages for
669 -- specialisation pragmas for non-overloaded sigs
670 -- Indeed that is why we call it here!
671 -- So we can safely ignore _specs
672
673
674 {- *********************************************************************
675 * *
676 tcPolyCheck
677 * *
678 ********************************************************************* -}
679
680 tcPolyCheck :: TcPragEnv
681 -> TcIdSigInfo -- Must be a complete signature
682 -> LHsBind GhcRn -- Must be a FunBind
683 -> TcM (LHsBinds GhcTcId, [TcId])
684 -- There is just one binding,
685 -- it is a Funbind
686 -- it has a complete type signature,
687 tcPolyCheck prag_fn
688 (CompleteSig { sig_bndr = poly_id
689 , sig_ctxt = ctxt
690 , sig_loc = sig_loc })
691 (L loc (FunBind { fun_id = L nm_loc name
692 , fun_matches = matches }))
693 = setSrcSpan sig_loc $
694 do { traceTc "tcPolyCheck" (ppr poly_id $$ ppr sig_loc)
695 ; (tv_prs, theta, tau) <- tcInstType tcInstSkolTyVars poly_id
696 -- See Note [Instantiate sig with fresh variables]
697
698 ; mono_name <- newNameAt (nameOccName name) nm_loc
699 ; ev_vars <- newEvVars theta
700 ; let mono_id = mkLocalId mono_name tau
701 skol_info = SigSkol ctxt (idType poly_id) tv_prs
702 skol_tvs = map snd tv_prs
703
704 ; (ev_binds, (co_fn, matches'))
705 <- checkConstraints skol_info skol_tvs ev_vars $
706 tcExtendBinderStack [TcIdBndr mono_id NotTopLevel] $
707 tcExtendTyVarEnv2 tv_prs $
708 setSrcSpan loc $
709 tcMatchesFun (L nm_loc mono_name) matches (mkCheckExpType tau)
710
711 ; let prag_sigs = lookupPragEnv prag_fn name
712 ; spec_prags <- tcSpecPrags poly_id prag_sigs
713 ; poly_id <- addInlinePrags poly_id prag_sigs
714
715 ; mod <- getModule
716 ; tick <- funBindTicks nm_loc mono_id mod prag_sigs
717 ; let bind' = FunBind { fun_id = L nm_loc mono_id
718 , fun_matches = matches'
719 , fun_co_fn = co_fn
720 , bind_fvs = placeHolderNamesTc
721 , fun_tick = tick }
722
723 export = ABE { abe_wrap = idHsWrapper
724 , abe_poly = poly_id
725 , abe_mono = mono_id
726 , abe_prags = SpecPrags spec_prags }
727
728 abs_bind = L loc $
729 AbsBinds { abs_tvs = skol_tvs
730 , abs_ev_vars = ev_vars
731 , abs_ev_binds = [ev_binds]
732 , abs_exports = [export]
733 , abs_binds = unitBag (L 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 | 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, insoluble)
801 <- simplifyInfer tclvl infer_mode sigs name_taus wanted
802
803 ; let inferred_theta = map evVarPred givens
804 ; exports <- checkNoErrs $
805 mapM (mkExport prag_fn insoluble qtvs inferred_theta) mono_infos
806
807 ; loc <- getSrcSpanM
808 ; let poly_ids = map abe_poly exports
809 abs_bind = L loc $
810 AbsBinds { abs_tvs = qtvs
811 , abs_ev_vars = givens, abs_ev_binds = [ev_binds]
812 , abs_exports = exports, abs_binds = binds'
813 , abs_sig = False }
814
815 ; traceTc "Binding:" (ppr (poly_ids `zip` map idType poly_ids))
816 ; return (unitBag abs_bind, poly_ids) }
817 -- poly_ids are guaranteed zonked by mkExport
818
819 --------------
820 mkExport :: TcPragEnv
821 -> Bool -- True <=> there was an insoluble type error
822 -- when typechecking the bindings
823 -> [TyVar] -> TcThetaType -- Both already zonked
824 -> MonoBindInfo
825 -> TcM (ABExport GhcTc)
826 -- Only called for generalisation plan InferGen, not by CheckGen or NoGen
827 --
828 -- mkExport generates exports with
829 -- zonked type variables,
830 -- zonked poly_ids
831 -- The former is just because no further unifications will change
832 -- the quantified type variables, so we can fix their final form
833 -- right now.
834 -- The latter is needed because the poly_ids are used to extend the
835 -- type environment; see the invariant on TcEnv.tcExtendIdEnv
836
837 -- Pre-condition: the qtvs and theta are already zonked
838
839 mkExport prag_fn insoluble qtvs theta
840 mono_info@(MBI { mbi_poly_name = poly_name
841 , mbi_sig = mb_sig
842 , mbi_mono_id = mono_id })
843 = do { mono_ty <- zonkTcType (idType mono_id)
844 ; poly_id <- mkInferredPolyId insoluble qtvs theta poly_name mb_sig mono_ty
845
846 -- NB: poly_id has a zonked type
847 ; poly_id <- addInlinePrags poly_id prag_sigs
848 ; spec_prags <- tcSpecPrags poly_id prag_sigs
849 -- tcPrags requires a zonked poly_id
850
851 -- See Note [Impedance matching]
852 -- NB: we have already done checkValidType, including an ambiguity check,
853 -- on the type; either when we checked the sig or in mkInferredPolyId
854 ; let poly_ty = idType poly_id
855 sel_poly_ty = mkInfSigmaTy qtvs theta mono_ty
856 -- This type is just going into tcSubType,
857 -- so Inferred vs. Specified doesn't matter
858
859 ; wrap <- if sel_poly_ty `eqType` poly_ty -- NB: eqType ignores visibility
860 then return idHsWrapper -- Fast path; also avoids complaint when we infer
861 -- an ambiguous type and have AllowAmbiguousType
862 -- e..g infer x :: forall a. F a -> Int
863 else addErrCtxtM (mk_impedance_match_msg mono_info sel_poly_ty poly_ty) $
864 tcSubType_NC sig_ctxt sel_poly_ty poly_ty
865
866 ; warn_missing_sigs <- woptM Opt_WarnMissingLocalSignatures
867 ; when warn_missing_sigs $
868 localSigWarn Opt_WarnMissingLocalSignatures poly_id mb_sig
869
870 ; return (ABE { 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 <- zonkSigTyVarPairs 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_sig_tv_err (findDupSigTvs 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_sig_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_sig_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_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 SigTvs, 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 Vectorisation
1209 * *
1210 ********************************************************************* -}
1211
1212 tcVectDecls :: [LVectDecl GhcRn] -> TcM ([LVectDecl GhcTcId])
1213 tcVectDecls decls
1214 = do { decls' <- mapM (wrapLocM tcVect) decls
1215 ; let ids = [lvectDeclName decl | decl <- decls', not $ lvectInstDecl decl]
1216 dups = findDupsEq (==) ids
1217 ; mapM_ reportVectDups dups
1218 ; traceTcConstraints "End of tcVectDecls"
1219 ; return decls'
1220 }
1221 where
1222 reportVectDups (first :| (_second:_more))
1223 = addErrAt (getSrcSpan first) $
1224 text "Duplicate vectorisation declarations for" <+> ppr first
1225 reportVectDups _ = return ()
1226
1227 --------------
1228 tcVect :: VectDecl GhcRn -> TcM (VectDecl GhcTcId)
1229 -- FIXME: We can't typecheck the expression of a vectorisation declaration against the vectorised
1230 -- type of the original definition as this requires internals of the vectoriser not available
1231 -- during type checking. Instead, constrain the rhs of a vectorisation declaration to be a single
1232 -- identifier (this is checked in 'rnHsVectDecl'). Fix this by enabling the use of 'vectType'
1233 -- from the vectoriser here.
1234 tcVect (HsVect s name rhs)
1235 = addErrCtxt (vectCtxt name) $
1236 do { var <- wrapLocM tcLookupId name
1237 ; let L rhs_loc (HsVar (L lv rhs_var_name)) = rhs
1238 ; rhs_id <- tcLookupId rhs_var_name
1239 ; return $ HsVect s var (L rhs_loc (HsVar (L lv rhs_id)))
1240 }
1241
1242 tcVect (HsNoVect s name)
1243 = addErrCtxt (vectCtxt name) $
1244 do { var <- wrapLocM tcLookupId name
1245 ; return $ HsNoVect s var
1246 }
1247 tcVect (HsVectTypeIn _ isScalar lname rhs_name)
1248 = addErrCtxt (vectCtxt lname) $
1249 do { tycon <- tcLookupLocatedTyCon lname
1250 ; checkTc ( not isScalar -- either we have a non-SCALAR declaration
1251 || isJust rhs_name -- or we explicitly provide a vectorised type
1252 || tyConArity tycon == 0 -- otherwise the type constructor must be nullary
1253 )
1254 scalarTyConMustBeNullary
1255
1256 ; rhs_tycon <- fmapMaybeM (tcLookupTyCon . unLoc) rhs_name
1257 ; return $ HsVectTypeOut isScalar tycon rhs_tycon
1258 }
1259 tcVect (HsVectTypeOut _ _ _)
1260 = panic "TcBinds.tcVect: Unexpected 'HsVectTypeOut'"
1261 tcVect (HsVectClassIn _ lname)
1262 = addErrCtxt (vectCtxt lname) $
1263 do { cls <- tcLookupLocatedClass lname
1264 ; return $ HsVectClassOut cls
1265 }
1266 tcVect (HsVectClassOut _)
1267 = panic "TcBinds.tcVect: Unexpected 'HsVectClassOut'"
1268 tcVect (HsVectInstIn linstTy)
1269 = addErrCtxt (vectCtxt linstTy) $
1270 do { (cls, tys) <- tcHsVectInst linstTy
1271 ; inst <- tcLookupInstance cls tys
1272 ; return $ HsVectInstOut inst
1273 }
1274 tcVect (HsVectInstOut _)
1275 = panic "TcBinds.tcVect: Unexpected 'HsVectInstOut'"
1276
1277 vectCtxt :: Outputable thing => thing -> SDoc
1278 vectCtxt thing = text "When checking the vectorisation declaration for" <+> ppr thing
1279
1280 scalarTyConMustBeNullary :: MsgDoc
1281 scalarTyConMustBeNullary = text "VECTORISE SCALAR type constructor must be nullary"
1282
1283 {-
1284 Note [SPECIALISE pragmas]
1285 ~~~~~~~~~~~~~~~~~~~~~~~~~
1286 There is no point in a SPECIALISE pragma for a non-overloaded function:
1287 reverse :: [a] -> [a]
1288 {-# SPECIALISE reverse :: [Int] -> [Int] #-}
1289
1290 But SPECIALISE INLINE *can* make sense for GADTS:
1291 data Arr e where
1292 ArrInt :: !Int -> ByteArray# -> Arr Int
1293 ArrPair :: !Int -> Arr e1 -> Arr e2 -> Arr (e1, e2)
1294
1295 (!:) :: Arr e -> Int -> e
1296 {-# SPECIALISE INLINE (!:) :: Arr Int -> Int -> Int #-}
1297 {-# SPECIALISE INLINE (!:) :: Arr (a, b) -> Int -> (a, b) #-}
1298 (ArrInt _ ba) !: (I# i) = I# (indexIntArray# ba i)
1299 (ArrPair _ a1 a2) !: i = (a1 !: i, a2 !: i)
1300
1301 When (!:) is specialised it becomes non-recursive, and can usefully
1302 be inlined. Scary! So we only warn for SPECIALISE *without* INLINE
1303 for a non-overloaded function.
1304
1305 ************************************************************************
1306 * *
1307 tcMonoBinds
1308 * *
1309 ************************************************************************
1310
1311 @tcMonoBinds@ deals with a perhaps-recursive group of HsBinds.
1312 The signatures have been dealt with already.
1313 -}
1314
1315 data MonoBindInfo = MBI { mbi_poly_name :: Name
1316 , mbi_sig :: Maybe TcIdSigInst
1317 , mbi_mono_id :: TcId }
1318
1319 tcMonoBinds :: RecFlag -- Whether the binding is recursive for typechecking purposes
1320 -- i.e. the binders are mentioned in their RHSs, and
1321 -- we are not rescued by a type signature
1322 -> TcSigFun -> LetBndrSpec
1323 -> [LHsBind GhcRn]
1324 -> TcM (LHsBinds GhcTcId, [MonoBindInfo])
1325 tcMonoBinds is_rec sig_fn no_gen
1326 [ L b_loc (FunBind { fun_id = L nm_loc name,
1327 fun_matches = matches, bind_fvs = fvs })]
1328 -- Single function binding,
1329 | NonRecursive <- is_rec -- ...binder isn't mentioned in RHS
1330 , Nothing <- sig_fn name -- ...with no type signature
1331 = -- Note [Single function non-recursive binding special-case]
1332 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1333 -- In this very special case we infer the type of the
1334 -- right hand side first (it may have a higher-rank type)
1335 -- and *then* make the monomorphic Id for the LHS
1336 -- e.g. f = \(x::forall a. a->a) -> <body>
1337 -- We want to infer a higher-rank type for f
1338 setSrcSpan b_loc $
1339 do { ((co_fn, matches'), rhs_ty)
1340 <- tcInferInst $ \ exp_ty ->
1341 -- tcInferInst: see TcUnify,
1342 -- Note [Deep instantiation of InferResult]
1343 tcExtendBinderStack [TcIdBndr_ExpType name exp_ty NotTopLevel] $
1344 -- We extend the error context even for a non-recursive
1345 -- function so that in type error messages we show the
1346 -- type of the thing whose rhs we are type checking
1347 tcMatchesFun (L nm_loc name) matches exp_ty
1348
1349 ; mono_id <- newLetBndr no_gen name rhs_ty
1350 ; return (unitBag $ L b_loc $
1351 FunBind { fun_id = L nm_loc mono_id,
1352 fun_matches = matches', bind_fvs = fvs,
1353 fun_co_fn = co_fn, fun_tick = [] },
1354 [MBI { mbi_poly_name = name
1355 , mbi_sig = Nothing
1356 , mbi_mono_id = mono_id }]) }
1357
1358 tcMonoBinds _ sig_fn no_gen binds
1359 = do { tc_binds <- mapM (wrapLocM (tcLhs sig_fn no_gen)) binds
1360
1361 -- Bring the monomorphic Ids, into scope for the RHSs
1362 ; let mono_infos = getMonoBindInfo tc_binds
1363 rhs_id_env = [ (name, mono_id)
1364 | MBI { mbi_poly_name = name
1365 , mbi_sig = mb_sig
1366 , mbi_mono_id = mono_id } <- mono_infos
1367 , case mb_sig of
1368 Just sig -> isPartialSig sig
1369 Nothing -> True ]
1370 -- A monomorphic binding for each term variable that lacks
1371 -- a complete type sig. (Ones with a sig are already in scope.)
1372
1373 ; traceTc "tcMonoBinds" $ vcat [ ppr n <+> ppr id <+> ppr (idType id)
1374 | (n,id) <- rhs_id_env]
1375 ; binds' <- tcExtendRecIds rhs_id_env $
1376 mapM (wrapLocM tcRhs) tc_binds
1377
1378 ; return (listToBag binds', mono_infos) }
1379
1380
1381 ------------------------
1382 -- tcLhs typechecks the LHS of the bindings, to construct the environment in which
1383 -- we typecheck the RHSs. Basically what we are doing is this: for each binder:
1384 -- if there's a signature for it, use the instantiated signature type
1385 -- otherwise invent a type variable
1386 -- You see that quite directly in the FunBind case.
1387 --
1388 -- But there's a complication for pattern bindings:
1389 -- data T = MkT (forall a. a->a)
1390 -- MkT f = e
1391 -- Here we can guess a type variable for the entire LHS (which will be refined to T)
1392 -- but we want to get (f::forall a. a->a) as the RHS environment.
1393 -- The simplest way to do this is to typecheck the pattern, and then look up the
1394 -- bound mono-ids. Then we want to retain the typechecked pattern to avoid re-doing
1395 -- it; hence the TcMonoBind data type in which the LHS is done but the RHS isn't
1396
1397 data TcMonoBind -- Half completed; LHS done, RHS not done
1398 = TcFunBind MonoBindInfo SrcSpan (MatchGroup GhcRn (LHsExpr GhcRn))
1399 | TcPatBind [MonoBindInfo] (LPat GhcTcId) (GRHSs GhcRn (LHsExpr GhcRn))
1400 TcSigmaType
1401
1402 tcLhs :: TcSigFun -> LetBndrSpec -> HsBind GhcRn -> TcM TcMonoBind
1403 -- Only called with plan InferGen (LetBndrSpec = LetLclBndr)
1404 -- or NoGen (LetBndrSpec = LetGblBndr)
1405 -- CheckGen is used only for functions with a complete type signature,
1406 -- and tcPolyCheck doesn't use tcMonoBinds at all
1407
1408 tcLhs sig_fn no_gen (FunBind { fun_id = L nm_loc name, fun_matches = matches })
1409 | Just (TcIdSig sig) <- sig_fn name
1410 = -- There is a type signature.
1411 -- It must be partial; if complete we'd be in tcPolyCheck!
1412 -- e.g. f :: _ -> _
1413 -- f x = ...g...
1414 -- Just g = ...f...
1415 -- Hence always typechecked with InferGen
1416 do { mono_info <- tcLhsSigId no_gen (name, sig)
1417 ; return (TcFunBind mono_info nm_loc matches) }
1418
1419 | otherwise -- No type signature
1420 = do { mono_ty <- newOpenFlexiTyVarTy
1421 ; mono_id <- newLetBndr no_gen name mono_ty
1422 ; let mono_info = MBI { mbi_poly_name = name
1423 , mbi_sig = Nothing
1424 , mbi_mono_id = mono_id }
1425 ; return (TcFunBind mono_info nm_loc matches) }
1426
1427 tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss })
1428 = -- See Note [Typechecking pattern bindings]
1429 do { sig_mbis <- mapM (tcLhsSigId no_gen) sig_names
1430
1431 ; let inst_sig_fun = lookupNameEnv $ mkNameEnv $
1432 [ (mbi_poly_name mbi, mbi_mono_id mbi)
1433 | mbi <- sig_mbis ]
1434
1435 -- See Note [Existentials in pattern bindings]
1436 ; ((pat', nosig_mbis), pat_ty)
1437 <- addErrCtxt (patMonoBindsCtxt pat grhss) $
1438 tcInferNoInst $ \ exp_ty ->
1439 tcLetPat inst_sig_fun no_gen pat exp_ty $
1440 mapM lookup_info nosig_names
1441
1442 ; let mbis = sig_mbis ++ nosig_mbis
1443
1444 ; traceTc "tcLhs" (vcat [ ppr id <+> dcolon <+> ppr (idType id)
1445 | mbi <- mbis, let id = mbi_mono_id mbi ]
1446 $$ ppr no_gen)
1447
1448 ; return (TcPatBind mbis pat' grhss pat_ty) }
1449 where
1450 bndr_names = collectPatBinders pat
1451 (nosig_names, sig_names) = partitionWith find_sig bndr_names
1452
1453 find_sig :: Name -> Either Name (Name, TcIdSigInfo)
1454 find_sig name = case sig_fn name of
1455 Just (TcIdSig sig) -> Right (name, sig)
1456 _ -> Left name
1457
1458 -- After typechecking the pattern, look up the binder
1459 -- names that lack a signature, which the pattern has brought
1460 -- into scope.
1461 lookup_info :: Name -> TcM MonoBindInfo
1462 lookup_info name
1463 = do { mono_id <- tcLookupId name
1464 ; return (MBI { mbi_poly_name = name
1465 , mbi_sig = Nothing
1466 , mbi_mono_id = mono_id }) }
1467
1468 tcLhs _ _ other_bind = pprPanic "tcLhs" (ppr other_bind)
1469 -- AbsBind, VarBind impossible
1470
1471 -------------------
1472 tcLhsSigId :: LetBndrSpec -> (Name, TcIdSigInfo) -> TcM MonoBindInfo
1473 tcLhsSigId no_gen (name, sig)
1474 = do { inst_sig <- tcInstSig sig
1475 ; mono_id <- newSigLetBndr no_gen name inst_sig
1476 ; return (MBI { mbi_poly_name = name
1477 , mbi_sig = Just inst_sig
1478 , mbi_mono_id = mono_id }) }
1479
1480 ------------
1481 newSigLetBndr :: LetBndrSpec -> Name -> TcIdSigInst -> TcM TcId
1482 newSigLetBndr (LetGblBndr prags) name (TISI { sig_inst_sig = id_sig })
1483 | CompleteSig { sig_bndr = poly_id } <- id_sig
1484 = addInlinePrags poly_id (lookupPragEnv prags name)
1485 newSigLetBndr no_gen name (TISI { sig_inst_tau = tau })
1486 = newLetBndr no_gen name tau
1487
1488 -------------------
1489 tcRhs :: TcMonoBind -> TcM (HsBind GhcTcId)
1490 tcRhs (TcFunBind info@(MBI { mbi_sig = mb_sig, mbi_mono_id = mono_id })
1491 loc matches)
1492 = tcExtendIdBinderStackForRhs [info] $
1493 tcExtendTyVarEnvForRhs mb_sig $
1494 do { traceTc "tcRhs: fun bind" (ppr mono_id $$ ppr (idType mono_id))
1495 ; (co_fn, matches') <- tcMatchesFun (L loc (idName mono_id))
1496 matches (mkCheckExpType $ idType mono_id)
1497 ; return ( FunBind { fun_id = L loc mono_id
1498 , fun_matches = matches'
1499 , fun_co_fn = co_fn
1500 , bind_fvs = placeHolderNamesTc
1501 , fun_tick = [] } ) }
1502
1503 tcRhs (TcPatBind infos pat' grhss pat_ty)
1504 = -- When we are doing pattern bindings we *don't* bring any scoped
1505 -- type variables into scope unlike function bindings
1506 -- Wny not? They are not completely rigid.
1507 -- That's why we have the special case for a single FunBind in tcMonoBinds
1508 tcExtendIdBinderStackForRhs infos $
1509 do { traceTc "tcRhs: pat bind" (ppr pat' $$ ppr pat_ty)
1510 ; grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $
1511 tcGRHSsPat grhss pat_ty
1512 ; return ( PatBind { pat_lhs = pat', pat_rhs = grhss'
1513 , pat_rhs_ty = pat_ty
1514 , bind_fvs = placeHolderNamesTc
1515 , pat_ticks = ([],[]) } )}
1516
1517 tcExtendTyVarEnvForRhs :: Maybe TcIdSigInst -> TcM a -> TcM a
1518 tcExtendTyVarEnvForRhs Nothing thing_inside
1519 = thing_inside
1520 tcExtendTyVarEnvForRhs (Just sig) thing_inside
1521 = tcExtendTyVarEnvFromSig sig thing_inside
1522
1523 tcExtendTyVarEnvFromSig :: TcIdSigInst -> TcM a -> TcM a
1524 tcExtendTyVarEnvFromSig sig_inst thing_inside
1525 | TISI { sig_inst_skols = skol_prs, sig_inst_wcs = wcs } <- sig_inst
1526 -- Note [Use tcExtendTyVar not scopeTyVars in tcRhs]
1527 = tcExtendTyVarEnv2 wcs $
1528 tcExtendTyVarEnv2 skol_prs $
1529 thing_inside
1530
1531 tcExtendIdBinderStackForRhs :: [MonoBindInfo] -> TcM a -> TcM a
1532 -- Extend the TcBinderStack for the RHS of the binding, with
1533 -- the monomorphic Id. That way, if we have, say
1534 -- f = \x -> blah
1535 -- and something goes wrong in 'blah', we get a "relevant binding"
1536 -- looking like f :: alpha -> beta
1537 -- This applies if 'f' has a type signature too:
1538 -- f :: forall a. [a] -> [a]
1539 -- f x = True
1540 -- We can't unify True with [a], and a relevant binding is f :: [a] -> [a]
1541 -- If we had the *polymorphic* version of f in the TcBinderStack, it
1542 -- would not be reported as relevant, because its type is closed
1543 tcExtendIdBinderStackForRhs infos thing_inside
1544 = tcExtendBinderStack [ TcIdBndr mono_id NotTopLevel
1545 | MBI { mbi_mono_id = mono_id } <- infos ]
1546 thing_inside
1547 -- NotTopLevel: it's a monomorphic binding
1548
1549 ---------------------
1550 getMonoBindInfo :: [Located TcMonoBind] -> [MonoBindInfo]
1551 getMonoBindInfo tc_binds
1552 = foldr (get_info . unLoc) [] tc_binds
1553 where
1554 get_info (TcFunBind info _ _) rest = info : rest
1555 get_info (TcPatBind infos _ _ _) rest = infos ++ rest
1556
1557
1558 {- Note [Typechecking pattern bindings]
1559 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1560 Look at:
1561 - typecheck/should_compile/ExPat
1562 - Trac #12427, typecheck/should_compile/T12427{a,b}
1563
1564 data T where
1565 MkT :: Integral a => a -> Int -> T
1566
1567 and suppose t :: T. Which of these pattern bindings are ok?
1568
1569 E1. let { MkT p _ = t } in <body>
1570
1571 E2. let { MkT _ q = t } in <body>
1572
1573 E3. let { MkT (toInteger -> r) _ = t } in <body>
1574
1575 * (E1) is clearly wrong because the existential 'a' escapes.
1576 What type could 'p' possibly have?
1577
1578 * (E2) is fine, despite the existential pattern, because
1579 q::Int, and nothing escapes.
1580
1581 * Even (E3) is fine. The existential pattern binds a dictionary
1582 for (Integral a) which the view pattern can use to convert the
1583 a-valued field to an Integer, so r :: Integer.
1584
1585 An easy way to see all three is to imagine the desugaring.
1586 For (E2) it would look like
1587 let q = case t of MkT _ q' -> q'
1588 in <body>
1589
1590
1591 We typecheck pattern bindings as follows. First tcLhs does this:
1592
1593 1. Take each type signature q :: ty, partial or complete, and
1594 instantiate it (with tcLhsSigId) to get a MonoBindInfo. This
1595 gives us a fresh "mono_id" qm :: instantiate(ty), where qm has
1596 a fresh name.
1597
1598 Any fresh unification variables in instantiate(ty) born here, not
1599 deep under implications as would happen if we allocated them when
1600 we encountered q during tcPat.
1601
1602 2. Build a little environment mapping "q" -> "qm" for those Ids
1603 with signatures (inst_sig_fun)
1604
1605 3. Invoke tcLetPat to typecheck the pattern.
1606
1607 - We pass in the current TcLevel. This is captured by
1608 TcPat.tcLetPat, and put into the pc_lvl field of PatCtxt, in
1609 PatEnv.
1610
1611 - When tcPat finds an existential constructor, it binds fresh
1612 type variables and dictionaries as usual, increments the TcLevel,
1613 and emits an implication constraint.
1614
1615 - When we come to a binder (TcPat.tcPatBndr), it looks it up
1616 in the little environment (the pc_sig_fn field of PatCtxt).
1617
1618 Success => There was a type signature, so just use it,
1619 checking compatibility with the expected type.
1620
1621 Failure => No type sigature.
1622 Infer case: (happens only outside any constructor pattern)
1623 use a unification variable
1624 at the outer level pc_lvl
1625
1626 Check case: use promoteTcType to promote the type
1627 to the outer level pc_lvl. This is the
1628 place where we emit a constraint that'll blow
1629 up if existential capture takes place
1630
1631 Result: the type of the binder is always at pc_lvl. This is
1632 crucial.
1633
1634 4. Throughout, when we are making up an Id for the pattern-bound variables
1635 (newLetBndr), we have two cases:
1636
1637 - If we are generalising (generalisation plan is InferGen or
1638 CheckGen), then the let_bndr_spec will be LetLclBndr. In that case
1639 we want to bind a cloned, local version of the variable, with the
1640 type given by the pattern context, *not* by the signature (even if
1641 there is one; see Trac #7268). The mkExport part of the
1642 generalisation step will do the checking and impedance matching
1643 against the signature.
1644
1645 - If for some some reason we are not generalising (plan = NoGen), the
1646 LetBndrSpec will be LetGblBndr. In that case we must bind the
1647 global version of the Id, and do so with precisely the type given
1648 in the signature. (Then we unify with the type from the pattern
1649 context type.)
1650
1651
1652 And that's it! The implication constraints check for the skolem
1653 escape. It's quite simple and neat, and more expressive than before
1654 e.g. GHC 8.0 rejects (E2) and (E3).
1655
1656 Example for (E1), starting at level 1. We generate
1657 p :: beta:1, with constraints (forall:3 a. Integral a => a ~ beta)
1658 The (a~beta) can't float (because of the 'a'), nor be solved (because
1659 beta is untouchable.)
1660
1661 Example for (E2), we generate
1662 q :: beta:1, with constraint (forall:3 a. Integral a => Int ~ beta)
1663 The beta is untoucable, but floats out of the constraint and can
1664 be solved absolutely fine.
1665
1666 Note [Use tcExtendTyVar not scopeTyVars in tcRhs]
1667 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1668 Normally, any place that corresponds to Λ or ∀ in Core should be flagged
1669 with a call to scopeTyVars, which arranges for an implication constraint
1670 to be made, bumps the TcLevel, and (crucially) prevents a unification
1671 variable created outside the scope of a local skolem to unify with that
1672 skolem.
1673
1674 We do not need to do this here, however.
1675
1676 - Note that this happens only in the case of a partial signature.
1677 Complete signatures go via tcPolyCheck, not tcPolyInfer.
1678
1679 - The TcLevel is incremented in tcPolyInfer, right outside the call
1680 to tcMonoBinds. We thus don't have to worry about outer metatvs unifying
1681 with local skolems.
1682
1683 - The other potential concern is that we need SkolemInfo associated with
1684 the skolems. This, too, is OK, though: the constraints pass through
1685 simplifyInfer (which doesn't report errors), at the end of which
1686 the skolems will get quantified and put into an implication constraint.
1687 Thus, by the time any errors are reported, the SkolemInfo will be
1688 in place.
1689
1690 ************************************************************************
1691 * *
1692 Generalisation
1693 * *
1694 ********************************************************************* -}
1695
1696 data GeneralisationPlan
1697 = NoGen -- No generalisation, no AbsBinds
1698
1699 | InferGen -- Implicit generalisation; there is an AbsBinds
1700 Bool -- True <=> apply the MR; generalise only unconstrained type vars
1701
1702 | CheckGen (LHsBind GhcRn) TcIdSigInfo
1703 -- One FunBind with a signature
1704 -- Explicit generalisation
1705
1706 -- A consequence of the no-AbsBinds choice (NoGen) is that there is
1707 -- no "polymorphic Id" and "monmomorphic Id"; there is just the one
1708
1709 instance Outputable GeneralisationPlan where
1710 ppr NoGen = text "NoGen"
1711 ppr (InferGen b) = text "InferGen" <+> ppr b
1712 ppr (CheckGen _ s) = text "CheckGen" <+> ppr s
1713
1714 decideGeneralisationPlan
1715 :: DynFlags -> [LHsBind GhcRn] -> IsGroupClosed -> TcSigFun
1716 -> GeneralisationPlan
1717 decideGeneralisationPlan dflags lbinds closed sig_fn
1718 | has_partial_sigs = InferGen (and partial_sig_mrs)
1719 | Just (bind, sig) <- one_funbind_with_sig = CheckGen bind sig
1720 | do_not_generalise closed = NoGen
1721 | otherwise = InferGen mono_restriction
1722 where
1723 binds = map unLoc lbinds
1724
1725 partial_sig_mrs :: [Bool]
1726 -- One for each partial signature (so empty => no partial sigs)
1727 -- The Bool is True if the signature has no constraint context
1728 -- so we should apply the MR
1729 -- See Note [Partial type signatures and generalisation]
1730 partial_sig_mrs
1731 = [ null theta
1732 | TcIdSig (PartialSig { psig_hs_ty = hs_ty })
1733 <- mapMaybe sig_fn (collectHsBindListBinders lbinds)
1734 , let (_, L _ theta, _) = splitLHsSigmaTy (hsSigWcType hs_ty) ]
1735
1736 has_partial_sigs = not (null partial_sig_mrs)
1737
1738 mono_restriction = xopt LangExt.MonomorphismRestriction dflags
1739 && any restricted binds
1740
1741 do_not_generalise (IsGroupClosed _ True) = False
1742 -- The 'True' means that all of the group's
1743 -- free vars have ClosedTypeId=True; so we can ignore
1744 -- -XMonoLocalBinds, and generalise anyway
1745 do_not_generalise _ = xopt LangExt.MonoLocalBinds dflags
1746
1747 -- With OutsideIn, all nested bindings are monomorphic
1748 -- except a single function binding with a signature
1749 one_funbind_with_sig
1750 | [lbind@(L _ (FunBind { fun_id = v }))] <- lbinds
1751 , Just (TcIdSig sig) <- sig_fn (unLoc v)
1752 = Just (lbind, sig)
1753 | otherwise
1754 = Nothing
1755
1756 -- The Haskell 98 monomorphism restriction
1757 restricted (PatBind {}) = True
1758 restricted (VarBind { var_id = v }) = no_sig v
1759 restricted (FunBind { fun_id = v, fun_matches = m }) = restricted_match m
1760 && no_sig (unLoc v)
1761 restricted b = pprPanic "isRestrictedGroup/unrestricted" (ppr b)
1762
1763 restricted_match mg = matchGroupArity mg == 0
1764 -- No args => like a pattern binding
1765 -- Some args => a function binding
1766
1767 no_sig n = not (hasCompleteSig sig_fn n)
1768
1769 isClosedBndrGroup :: TcTypeEnv -> Bag (LHsBind GhcRn) -> IsGroupClosed
1770 isClosedBndrGroup type_env binds
1771 = IsGroupClosed fv_env type_closed
1772 where
1773 type_closed = allUFM (nameSetAll is_closed_type_id) fv_env
1774
1775 fv_env :: NameEnv NameSet
1776 fv_env = mkNameEnv $ concatMap (bindFvs . unLoc) binds
1777
1778 bindFvs :: HsBindLR GhcRn idR -> [(Name, NameSet)]
1779 bindFvs (FunBind { fun_id = L _ f, bind_fvs = fvs })
1780 = let open_fvs = filterNameSet (not . is_closed) fvs
1781 in [(f, open_fvs)]
1782 bindFvs (PatBind { pat_lhs = pat, bind_fvs = fvs })
1783 = let open_fvs = filterNameSet (not . is_closed) fvs
1784 in [(b, open_fvs) | b <- collectPatBinders pat]
1785 bindFvs _
1786 = []
1787
1788 is_closed :: Name -> ClosedTypeId
1789 is_closed name
1790 | Just thing <- lookupNameEnv type_env name
1791 = case thing of
1792 AGlobal {} -> True
1793 ATcId { tct_info = ClosedLet } -> True
1794 _ -> False
1795
1796 | otherwise
1797 = True -- The free-var set for a top level binding mentions
1798
1799
1800 is_closed_type_id :: Name -> Bool
1801 -- We're already removed Global and ClosedLet Ids
1802 is_closed_type_id name
1803 | Just thing <- lookupNameEnv type_env name
1804 = case thing of
1805 ATcId { tct_info = NonClosedLet _ cl } -> cl
1806 ATcId { tct_info = NotLetBound } -> False
1807 ATyVar {} -> False
1808 -- In-scope type variables are not closed!
1809 _ -> pprPanic "is_closed_id" (ppr name)
1810
1811 | otherwise
1812 = True -- The free-var set for a top level binding mentions
1813 -- imported things too, so that we can report unused imports
1814 -- These won't be in the local type env.
1815 -- Ditto class method etc from the current module
1816
1817
1818 {- *********************************************************************
1819 * *
1820 Error contexts and messages
1821 * *
1822 ********************************************************************* -}
1823
1824 -- This one is called on LHS, when pat and grhss are both Name
1825 -- and on RHS, when pat is TcId and grhss is still Name
1826 patMonoBindsCtxt :: (OutputableBndrId (GhcPass p), Outputable body)
1827 => LPat (GhcPass p) -> GRHSs GhcRn body -> SDoc
1828 patMonoBindsCtxt pat grhss
1829 = hang (text "In a pattern binding:") 2 (pprPatBind pat grhss)