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