Check for bogus quantified tyvars in partial type sigs
[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 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_qtv_prs <- zonkSigTyVarPairs annotated_tvs
943
944 -- Check whether the quantified variables of the
945 -- partial signature have been unified together
946 -- See Note [Quantified variables in partial type signatures]
947 ; mapM_ report_dup_sig_tv_err (findDupSigTvs psig_qtv_prs)
948
949 -- Check whether a quantified variable of the partial type
950 -- signature is not actually quantified. How can that happen?
951 -- See Note [Quantification and partial signatures] Wrinkle 4
952 -- in TcSimplify
953 ; mapM_ report_mono_sig_tv_err [ n | (n,tv) <- psig_qtv_prs
954 , not (tv `elem` qtvs) ]
955
956 ; let psig_qtvs = mkVarSet (map snd psig_qtv_prs)
957
958 ; annotated_theta <- zonkTcTypes annotated_theta
959 ; (free_tvs, my_theta) <- choose_psig_context psig_qtvs annotated_theta wcx
960
961 ; let keep_me = free_tvs `unionVarSet` psig_qtvs
962 final_qtvs = [ mkTyVarBinder vis tv
963 | tv <- qtvs -- Pulling from qtvs maintains original order
964 , tv `elemVarSet` keep_me
965 , let vis | tv `elemVarSet` psig_qtvs = Specified
966 | otherwise = Inferred ]
967
968 ; return (final_qtvs, my_theta) }
969 where
970 report_dup_sig_tv_err (n1,n2)
971 | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
972 = addErrTc (hang (text "Couldn't match" <+> quotes (ppr n1)
973 <+> text "with" <+> quotes (ppr n2))
974 2 (hang (text "both bound by the partial type signature:")
975 2 (ppr fn_name <+> dcolon <+> ppr hs_ty)))
976
977 | otherwise -- Can't happen; by now we know it's a partial sig
978 = pprPanic "report_sig_tv_err" (ppr sig)
979
980 report_mono_sig_tv_err n
981 | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
982 = addErrTc (hang (text "Can't quantify over" <+> quotes (ppr n))
983 2 (hang (text "bound by the partial type signature:")
984 2 (ppr fn_name <+> dcolon <+> ppr hs_ty)))
985 | otherwise -- Can't happen; by now we know it's a partial sig
986 = pprPanic "report_sig_tv_err" (ppr sig)
987
988 choose_psig_context :: VarSet -> TcThetaType -> Maybe TcTyVar
989 -> TcM (VarSet, TcThetaType)
990 choose_psig_context _ annotated_theta Nothing
991 = do { let free_tvs = closeOverKinds (tyCoVarsOfTypes annotated_theta
992 `unionVarSet` tau_tvs)
993 ; return (free_tvs, annotated_theta) }
994
995 choose_psig_context psig_qtvs annotated_theta (Just wc_var)
996 = do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta seed_tvs)
997 -- growThetaVars just like the no-type-sig case
998 -- Omitting this caused #12844
999 seed_tvs = tyCoVarsOfTypes annotated_theta -- These are put there
1000 `unionVarSet` tau_tvs -- by the user
1001
1002 ; let keep_me = psig_qtvs `unionVarSet` free_tvs
1003 my_theta = pickCapturedPreds keep_me inferred_theta
1004
1005 -- Fill in the extra-constraints wildcard hole with inferred_theta,
1006 -- so that the Hole constraint we have already emitted
1007 -- (in tcHsPartialSigType) can report what filled it in.
1008 -- NB: my_theta already includes all the annotated constraints
1009 ; let inferred_diff = [ pred
1010 | pred <- my_theta
1011 , all (not . (`eqType` pred)) annotated_theta ]
1012 ; ctuple <- mk_ctuple inferred_diff
1013 ; writeMetaTyVar wc_var ctuple
1014
1015 ; traceTc "completeTheta" $
1016 vcat [ ppr sig
1017 , ppr annotated_theta, ppr inferred_theta
1018 , ppr inferred_diff ]
1019 ; return (free_tvs, my_theta) }
1020
1021 mk_ctuple preds = return (mkBoxedTupleTy preds)
1022 -- Hack alert! See TcHsType:
1023 -- Note [Extra-constraint holes in partial type signatures]
1024
1025
1026 mk_impedance_match_msg :: MonoBindInfo
1027 -> TcType -> TcType
1028 -> TidyEnv -> TcM (TidyEnv, SDoc)
1029 -- This is a rare but rather awkward error messages
1030 mk_impedance_match_msg (MBI { mbi_poly_name = name, mbi_sig = mb_sig })
1031 inf_ty sig_ty tidy_env
1032 = do { (tidy_env1, inf_ty) <- zonkTidyTcType tidy_env inf_ty
1033 ; (tidy_env2, sig_ty) <- zonkTidyTcType tidy_env1 sig_ty
1034 ; let msg = vcat [ text "When checking that the inferred type"
1035 , nest 2 $ ppr name <+> dcolon <+> ppr inf_ty
1036 , text "is as general as its" <+> what <+> text "signature"
1037 , nest 2 $ ppr name <+> dcolon <+> ppr sig_ty ]
1038 ; return (tidy_env2, msg) }
1039 where
1040 what = case mb_sig of
1041 Nothing -> text "inferred"
1042 Just sig | isPartialSig sig -> text "(partial)"
1043 | otherwise -> empty
1044
1045
1046 mk_inf_msg :: Name -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
1047 mk_inf_msg poly_name poly_ty tidy_env
1048 = do { (tidy_env1, poly_ty) <- zonkTidyTcType tidy_env poly_ty
1049 ; let msg = vcat [ text "When checking the inferred type"
1050 , nest 2 $ ppr poly_name <+> dcolon <+> ppr poly_ty ]
1051 ; return (tidy_env1, msg) }
1052
1053
1054 -- | Warn the user about polymorphic local binders that lack type signatures.
1055 localSigWarn :: WarningFlag -> Id -> Maybe TcIdSigInst -> TcM ()
1056 localSigWarn flag id mb_sig
1057 | Just _ <- mb_sig = return ()
1058 | not (isSigmaTy (idType id)) = return ()
1059 | otherwise = warnMissingSignatures flag msg id
1060 where
1061 msg = text "Polymorphic local binding with no type signature:"
1062
1063 warnMissingSignatures :: WarningFlag -> SDoc -> Id -> TcM ()
1064 warnMissingSignatures flag msg id
1065 = do { env0 <- tcInitTidyEnv
1066 ; let (env1, tidy_ty) = tidyOpenType env0 (idType id)
1067 ; addWarnTcM (Reason flag) (env1, mk_msg tidy_ty) }
1068 where
1069 mk_msg ty = sep [ msg, nest 2 $ pprPrefixName (idName id) <+> dcolon <+> ppr ty ]
1070
1071 checkOverloadedSig :: Bool -> TcIdSigInst -> TcM ()
1072 -- Example:
1073 -- f :: Eq a => a -> a
1074 -- K f = e
1075 -- The MR applies, but the signature is overloaded, and it's
1076 -- best to complain about this directly
1077 -- c.f Trac #11339
1078 checkOverloadedSig monomorphism_restriction_applies sig
1079 | not (null (sig_inst_theta sig))
1080 , monomorphism_restriction_applies
1081 , let orig_sig = sig_inst_sig sig
1082 = setSrcSpan (sig_loc orig_sig) $
1083 failWith $
1084 hang (text "Overloaded signature conflicts with monomorphism restriction")
1085 2 (ppr orig_sig)
1086 | otherwise
1087 = return ()
1088
1089 {- Note [Partial type signatures and generalisation]
1090 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1091 If /any/ of the signatures in the gropu is a partial type signature
1092 f :: _ -> Int
1093 then we *always* use the InferGen plan, and hence tcPolyInfer.
1094 We do this even for a local binding with -XMonoLocalBinds, when
1095 we normally use NoGen.
1096
1097 Reasons:
1098 * The TcSigInfo for 'f' has a unification variable for the '_',
1099 whose TcLevel is one level deeper than the current level.
1100 (See pushTcLevelM in tcTySig.) But NoGen doesn't increase
1101 the TcLevel like InferGen, so we lose the level invariant.
1102
1103 * The signature might be f :: forall a. _ -> a
1104 so it really is polymorphic. It's not clear what it would
1105 mean to use NoGen on this, and indeed the ASSERT in tcLhs,
1106 in the (Just sig) case, checks that if there is a signature
1107 then we are using LetLclBndr, and hence a nested AbsBinds with
1108 increased TcLevel
1109
1110 It might be possible to fix these difficulties somehow, but there
1111 doesn't seem much point. Indeed, adding a partial type signature is a
1112 way to get per-binding inferred generalisation.
1113
1114 We apply the MR if /all/ of the partial signatures lack a context.
1115 In particular (Trac #11016):
1116 f2 :: (?loc :: Int) => _
1117 f2 = ?loc
1118 It's stupid to apply the MR here. This test includes an extra-constraints
1119 wildcard; that is, we don't apply the MR if you write
1120 f3 :: _ => blah
1121
1122 Note [Quantified variables in partial type signatures]
1123 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1124 Consider
1125 f :: forall a. a -> a -> _
1126 f x y = g x y
1127 g :: forall b. b -> b -> _
1128 g x y = [x, y]
1129
1130 Here, 'f' and 'g' are mutually recursive, and we end up unifying 'a' and 'b'
1131 together, which is fine. So we bind 'a' and 'b' to SigTvs, which can then
1132 unify with each other.
1133
1134 But now consider:
1135 f :: forall a b. a -> b -> _
1136 f x y = [x, y]
1137
1138 We want to get an error from this, because 'a' and 'b' get unified.
1139 So we make a test, one per parital signature, to check that the
1140 explicitly-quantified type variables have not been unified together.
1141 Trac #14449 showed this up.
1142
1143
1144 Note [Validity of inferred types]
1145 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1146 We need to check inferred type for validity, in case it uses language
1147 extensions that are not turned on. The principle is that if the user
1148 simply adds the inferred type to the program source, it'll compile fine.
1149 See #8883.
1150
1151 Examples that might fail:
1152 - the type might be ambiguous
1153
1154 - an inferred theta that requires type equalities e.g. (F a ~ G b)
1155 or multi-parameter type classes
1156 - an inferred type that includes unboxed tuples
1157
1158
1159 Note [Impedance matching]
1160 ~~~~~~~~~~~~~~~~~~~~~~~~~
1161 Consider
1162 f 0 x = x
1163 f n x = g [] (not x)
1164
1165 g [] y = f 10 y
1166 g _ y = f 9 y
1167
1168 After typechecking we'll get
1169 f_mono_ty :: a -> Bool -> Bool
1170 g_mono_ty :: [b] -> Bool -> Bool
1171 with constraints
1172 (Eq a, Num a)
1173
1174 Note that f is polymorphic in 'a' and g in 'b'; and these are not linked.
1175 The types we really want for f and g are
1176 f :: forall a. (Eq a, Num a) => a -> Bool -> Bool
1177 g :: forall b. [b] -> Bool -> Bool
1178
1179 We can get these by "impedance matching":
1180 tuple :: forall a b. (Eq a, Num a) => (a -> Bool -> Bool, [b] -> Bool -> Bool)
1181 tuple a b d1 d1 = let ...bind f_mono, g_mono in (f_mono, g_mono)
1182
1183 f a d1 d2 = case tuple a Any d1 d2 of (f, g) -> f
1184 g b = case tuple Integer b dEqInteger dNumInteger of (f,g) -> g
1185
1186 Suppose the shared quantified tyvars are qtvs and constraints theta.
1187 Then we want to check that
1188 forall qtvs. theta => f_mono_ty is more polymorphic than f's polytype
1189 and the proof is the impedance matcher.
1190
1191 Notice that the impedance matcher may do defaulting. See Trac #7173.
1192
1193 It also cleverly does an ambiguity check; for example, rejecting
1194 f :: F a -> F a
1195 where F is a non-injective type function.
1196 -}
1197
1198 {- *********************************************************************
1199 * *
1200 Vectorisation
1201 * *
1202 ********************************************************************* -}
1203
1204 tcVectDecls :: [LVectDecl GhcRn] -> TcM ([LVectDecl GhcTcId])
1205 tcVectDecls decls
1206 = do { decls' <- mapM (wrapLocM tcVect) decls
1207 ; let ids = [lvectDeclName decl | decl <- decls', not $ lvectInstDecl decl]
1208 dups = findDupsEq (==) ids
1209 ; mapM_ reportVectDups dups
1210 ; traceTcConstraints "End of tcVectDecls"
1211 ; return decls'
1212 }
1213 where
1214 reportVectDups (first :| (_second:_more))
1215 = addErrAt (getSrcSpan first) $
1216 text "Duplicate vectorisation declarations for" <+> ppr first
1217 reportVectDups _ = return ()
1218
1219 --------------
1220 tcVect :: VectDecl GhcRn -> TcM (VectDecl GhcTcId)
1221 -- FIXME: We can't typecheck the expression of a vectorisation declaration against the vectorised
1222 -- type of the original definition as this requires internals of the vectoriser not available
1223 -- during type checking. Instead, constrain the rhs of a vectorisation declaration to be a single
1224 -- identifier (this is checked in 'rnHsVectDecl'). Fix this by enabling the use of 'vectType'
1225 -- from the vectoriser here.
1226 tcVect (HsVect s name rhs)
1227 = addErrCtxt (vectCtxt name) $
1228 do { var <- wrapLocM tcLookupId name
1229 ; let L rhs_loc (HsVar (L lv rhs_var_name)) = rhs
1230 ; rhs_id <- tcLookupId rhs_var_name
1231 ; return $ HsVect s var (L rhs_loc (HsVar (L lv rhs_id)))
1232 }
1233
1234 tcVect (HsNoVect s name)
1235 = addErrCtxt (vectCtxt name) $
1236 do { var <- wrapLocM tcLookupId name
1237 ; return $ HsNoVect s var
1238 }
1239 tcVect (HsVectTypeIn _ isScalar lname rhs_name)
1240 = addErrCtxt (vectCtxt lname) $
1241 do { tycon <- tcLookupLocatedTyCon lname
1242 ; checkTc ( not isScalar -- either we have a non-SCALAR declaration
1243 || isJust rhs_name -- or we explicitly provide a vectorised type
1244 || tyConArity tycon == 0 -- otherwise the type constructor must be nullary
1245 )
1246 scalarTyConMustBeNullary
1247
1248 ; rhs_tycon <- fmapMaybeM (tcLookupTyCon . unLoc) rhs_name
1249 ; return $ HsVectTypeOut isScalar tycon rhs_tycon
1250 }
1251 tcVect (HsVectTypeOut _ _ _)
1252 = panic "TcBinds.tcVect: Unexpected 'HsVectTypeOut'"
1253 tcVect (HsVectClassIn _ lname)
1254 = addErrCtxt (vectCtxt lname) $
1255 do { cls <- tcLookupLocatedClass lname
1256 ; return $ HsVectClassOut cls
1257 }
1258 tcVect (HsVectClassOut _)
1259 = panic "TcBinds.tcVect: Unexpected 'HsVectClassOut'"
1260 tcVect (HsVectInstIn linstTy)
1261 = addErrCtxt (vectCtxt linstTy) $
1262 do { (cls, tys) <- tcHsVectInst linstTy
1263 ; inst <- tcLookupInstance cls tys
1264 ; return $ HsVectInstOut inst
1265 }
1266 tcVect (HsVectInstOut _)
1267 = panic "TcBinds.tcVect: Unexpected 'HsVectInstOut'"
1268
1269 vectCtxt :: Outputable thing => thing -> SDoc
1270 vectCtxt thing = text "When checking the vectorisation declaration for" <+> ppr thing
1271
1272 scalarTyConMustBeNullary :: MsgDoc
1273 scalarTyConMustBeNullary = text "VECTORISE SCALAR type constructor must be nullary"
1274
1275 {-
1276 Note [SPECIALISE pragmas]
1277 ~~~~~~~~~~~~~~~~~~~~~~~~~
1278 There is no point in a SPECIALISE pragma for a non-overloaded function:
1279 reverse :: [a] -> [a]
1280 {-# SPECIALISE reverse :: [Int] -> [Int] #-}
1281
1282 But SPECIALISE INLINE *can* make sense for GADTS:
1283 data Arr e where
1284 ArrInt :: !Int -> ByteArray# -> Arr Int
1285 ArrPair :: !Int -> Arr e1 -> Arr e2 -> Arr (e1, e2)
1286
1287 (!:) :: Arr e -> Int -> e
1288 {-# SPECIALISE INLINE (!:) :: Arr Int -> Int -> Int #-}
1289 {-# SPECIALISE INLINE (!:) :: Arr (a, b) -> Int -> (a, b) #-}
1290 (ArrInt _ ba) !: (I# i) = I# (indexIntArray# ba i)
1291 (ArrPair _ a1 a2) !: i = (a1 !: i, a2 !: i)
1292
1293 When (!:) is specialised it becomes non-recursive, and can usefully
1294 be inlined. Scary! So we only warn for SPECIALISE *without* INLINE
1295 for a non-overloaded function.
1296
1297 ************************************************************************
1298 * *
1299 tcMonoBinds
1300 * *
1301 ************************************************************************
1302
1303 @tcMonoBinds@ deals with a perhaps-recursive group of HsBinds.
1304 The signatures have been dealt with already.
1305 -}
1306
1307 data MonoBindInfo = MBI { mbi_poly_name :: Name
1308 , mbi_sig :: Maybe TcIdSigInst
1309 , mbi_mono_id :: TcId }
1310
1311 tcMonoBinds :: RecFlag -- Whether the binding is recursive for typechecking purposes
1312 -- i.e. the binders are mentioned in their RHSs, and
1313 -- we are not rescued by a type signature
1314 -> TcSigFun -> LetBndrSpec
1315 -> [LHsBind GhcRn]
1316 -> TcM (LHsBinds GhcTcId, [MonoBindInfo])
1317 tcMonoBinds is_rec sig_fn no_gen
1318 [ L b_loc (FunBind { fun_id = L nm_loc name,
1319 fun_matches = matches, bind_fvs = fvs })]
1320 -- Single function binding,
1321 | NonRecursive <- is_rec -- ...binder isn't mentioned in RHS
1322 , Nothing <- sig_fn name -- ...with no type signature
1323 = -- Note [Single function non-recursive binding special-case]
1324 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1325 -- In this very special case we infer the type of the
1326 -- right hand side first (it may have a higher-rank type)
1327 -- and *then* make the monomorphic Id for the LHS
1328 -- e.g. f = \(x::forall a. a->a) -> <body>
1329 -- We want to infer a higher-rank type for f
1330 setSrcSpan b_loc $
1331 do { ((co_fn, matches'), rhs_ty)
1332 <- tcInferInst $ \ exp_ty ->
1333 -- tcInferInst: see TcUnify,
1334 -- Note [Deep instantiation of InferResult]
1335 tcExtendBinderStack [TcIdBndr_ExpType name exp_ty NotTopLevel] $
1336 -- We extend the error context even for a non-recursive
1337 -- function so that in type error messages we show the
1338 -- type of the thing whose rhs we are type checking
1339 tcMatchesFun (L nm_loc name) matches exp_ty
1340
1341 ; mono_id <- newLetBndr no_gen name rhs_ty
1342 ; return (unitBag $ L b_loc $
1343 FunBind { fun_id = L nm_loc mono_id,
1344 fun_matches = matches', bind_fvs = fvs,
1345 fun_co_fn = co_fn, fun_tick = [] },
1346 [MBI { mbi_poly_name = name
1347 , mbi_sig = Nothing
1348 , mbi_mono_id = mono_id }]) }
1349
1350 tcMonoBinds _ sig_fn no_gen binds
1351 = do { tc_binds <- mapM (wrapLocM (tcLhs sig_fn no_gen)) binds
1352
1353 -- Bring the monomorphic Ids, into scope for the RHSs
1354 ; let mono_infos = getMonoBindInfo tc_binds
1355 rhs_id_env = [ (name, mono_id)
1356 | MBI { mbi_poly_name = name
1357 , mbi_sig = mb_sig
1358 , mbi_mono_id = mono_id } <- mono_infos
1359 , case mb_sig of
1360 Just sig -> isPartialSig sig
1361 Nothing -> True ]
1362 -- A monomorphic binding for each term variable that lacks
1363 -- a complete type sig. (Ones with a sig are already in scope.)
1364
1365 ; traceTc "tcMonoBinds" $ vcat [ ppr n <+> ppr id <+> ppr (idType id)
1366 | (n,id) <- rhs_id_env]
1367 ; binds' <- tcExtendRecIds rhs_id_env $
1368 mapM (wrapLocM tcRhs) tc_binds
1369
1370 ; return (listToBag binds', mono_infos) }
1371
1372
1373 ------------------------
1374 -- tcLhs typechecks the LHS of the bindings, to construct the environment in which
1375 -- we typecheck the RHSs. Basically what we are doing is this: for each binder:
1376 -- if there's a signature for it, use the instantiated signature type
1377 -- otherwise invent a type variable
1378 -- You see that quite directly in the FunBind case.
1379 --
1380 -- But there's a complication for pattern bindings:
1381 -- data T = MkT (forall a. a->a)
1382 -- MkT f = e
1383 -- Here we can guess a type variable for the entire LHS (which will be refined to T)
1384 -- but we want to get (f::forall a. a->a) as the RHS environment.
1385 -- The simplest way to do this is to typecheck the pattern, and then look up the
1386 -- bound mono-ids. Then we want to retain the typechecked pattern to avoid re-doing
1387 -- it; hence the TcMonoBind data type in which the LHS is done but the RHS isn't
1388
1389 data TcMonoBind -- Half completed; LHS done, RHS not done
1390 = TcFunBind MonoBindInfo SrcSpan (MatchGroup GhcRn (LHsExpr GhcRn))
1391 | TcPatBind [MonoBindInfo] (LPat GhcTcId) (GRHSs GhcRn (LHsExpr GhcRn))
1392 TcSigmaType
1393
1394 tcLhs :: TcSigFun -> LetBndrSpec -> HsBind GhcRn -> TcM TcMonoBind
1395 -- Only called with plan InferGen (LetBndrSpec = LetLclBndr)
1396 -- or NoGen (LetBndrSpec = LetGblBndr)
1397 -- CheckGen is used only for functions with a complete type signature,
1398 -- and tcPolyCheck doesn't use tcMonoBinds at all
1399
1400 tcLhs sig_fn no_gen (FunBind { fun_id = L nm_loc name, fun_matches = matches })
1401 | Just (TcIdSig sig) <- sig_fn name
1402 = -- There is a type signature.
1403 -- It must be partial; if complete we'd be in tcPolyCheck!
1404 -- e.g. f :: _ -> _
1405 -- f x = ...g...
1406 -- Just g = ...f...
1407 -- Hence always typechecked with InferGen
1408 do { mono_info <- tcLhsSigId no_gen (name, sig)
1409 ; return (TcFunBind mono_info nm_loc matches) }
1410
1411 | otherwise -- No type signature
1412 = do { mono_ty <- newOpenFlexiTyVarTy
1413 ; mono_id <- newLetBndr no_gen name mono_ty
1414 ; let mono_info = MBI { mbi_poly_name = name
1415 , mbi_sig = Nothing
1416 , mbi_mono_id = mono_id }
1417 ; return (TcFunBind mono_info nm_loc matches) }
1418
1419 tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss })
1420 = -- See Note [Typechecking pattern bindings]
1421 do { sig_mbis <- mapM (tcLhsSigId no_gen) sig_names
1422
1423 ; let inst_sig_fun = lookupNameEnv $ mkNameEnv $
1424 [ (mbi_poly_name mbi, mbi_mono_id mbi)
1425 | mbi <- sig_mbis ]
1426
1427 -- See Note [Existentials in pattern bindings]
1428 ; ((pat', nosig_mbis), pat_ty)
1429 <- addErrCtxt (patMonoBindsCtxt pat grhss) $
1430 tcInferNoInst $ \ exp_ty ->
1431 tcLetPat inst_sig_fun no_gen pat exp_ty $
1432 mapM lookup_info nosig_names
1433
1434 ; let mbis = sig_mbis ++ nosig_mbis
1435
1436 ; traceTc "tcLhs" (vcat [ ppr id <+> dcolon <+> ppr (idType id)
1437 | mbi <- mbis, let id = mbi_mono_id mbi ]
1438 $$ ppr no_gen)
1439
1440 ; return (TcPatBind mbis pat' grhss pat_ty) }
1441 where
1442 bndr_names = collectPatBinders pat
1443 (nosig_names, sig_names) = partitionWith find_sig bndr_names
1444
1445 find_sig :: Name -> Either Name (Name, TcIdSigInfo)
1446 find_sig name = case sig_fn name of
1447 Just (TcIdSig sig) -> Right (name, sig)
1448 _ -> Left name
1449
1450 -- After typechecking the pattern, look up the binder
1451 -- names that lack a signature, which the pattern has brought
1452 -- into scope.
1453 lookup_info :: Name -> TcM MonoBindInfo
1454 lookup_info name
1455 = do { mono_id <- tcLookupId name
1456 ; return (MBI { mbi_poly_name = name
1457 , mbi_sig = Nothing
1458 , mbi_mono_id = mono_id }) }
1459
1460 tcLhs _ _ other_bind = pprPanic "tcLhs" (ppr other_bind)
1461 -- AbsBind, VarBind impossible
1462
1463 -------------------
1464 tcLhsSigId :: LetBndrSpec -> (Name, TcIdSigInfo) -> TcM MonoBindInfo
1465 tcLhsSigId no_gen (name, sig)
1466 = do { inst_sig <- tcInstSig sig
1467 ; mono_id <- newSigLetBndr no_gen name inst_sig
1468 ; return (MBI { mbi_poly_name = name
1469 , mbi_sig = Just inst_sig
1470 , mbi_mono_id = mono_id }) }
1471
1472 ------------
1473 newSigLetBndr :: LetBndrSpec -> Name -> TcIdSigInst -> TcM TcId
1474 newSigLetBndr (LetGblBndr prags) name (TISI { sig_inst_sig = id_sig })
1475 | CompleteSig { sig_bndr = poly_id } <- id_sig
1476 = addInlinePrags poly_id (lookupPragEnv prags name)
1477 newSigLetBndr no_gen name (TISI { sig_inst_tau = tau })
1478 = newLetBndr no_gen name tau
1479
1480 -------------------
1481 tcRhs :: TcMonoBind -> TcM (HsBind GhcTcId)
1482 tcRhs (TcFunBind info@(MBI { mbi_sig = mb_sig, mbi_mono_id = mono_id })
1483 loc matches)
1484 = tcExtendIdBinderStackForRhs [info] $
1485 tcExtendTyVarEnvForRhs mb_sig $
1486 do { traceTc "tcRhs: fun bind" (ppr mono_id $$ ppr (idType mono_id))
1487 ; (co_fn, matches') <- tcMatchesFun (L loc (idName mono_id))
1488 matches (mkCheckExpType $ idType mono_id)
1489 ; return ( FunBind { fun_id = L loc mono_id
1490 , fun_matches = matches'
1491 , fun_co_fn = co_fn
1492 , bind_fvs = placeHolderNamesTc
1493 , fun_tick = [] } ) }
1494
1495 tcRhs (TcPatBind infos pat' grhss pat_ty)
1496 = -- When we are doing pattern bindings we *don't* bring any scoped
1497 -- type variables into scope unlike function bindings
1498 -- Wny not? They are not completely rigid.
1499 -- That's why we have the special case for a single FunBind in tcMonoBinds
1500 tcExtendIdBinderStackForRhs infos $
1501 do { traceTc "tcRhs: pat bind" (ppr pat' $$ ppr pat_ty)
1502 ; grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $
1503 tcGRHSsPat grhss pat_ty
1504 ; return ( PatBind { pat_lhs = pat', pat_rhs = grhss'
1505 , pat_rhs_ty = pat_ty
1506 , bind_fvs = placeHolderNamesTc
1507 , pat_ticks = ([],[]) } )}
1508
1509 tcExtendTyVarEnvForRhs :: Maybe TcIdSigInst -> TcM a -> TcM a
1510 tcExtendTyVarEnvForRhs Nothing thing_inside
1511 = thing_inside
1512 tcExtendTyVarEnvForRhs (Just sig) thing_inside
1513 = tcExtendTyVarEnvFromSig sig thing_inside
1514
1515 tcExtendTyVarEnvFromSig :: TcIdSigInst -> TcM a -> TcM a
1516 tcExtendTyVarEnvFromSig sig_inst thing_inside
1517 | TISI { sig_inst_skols = skol_prs, sig_inst_wcs = wcs } <- sig_inst
1518 = tcExtendTyVarEnv2 wcs $
1519 tcExtendTyVarEnv2 skol_prs $
1520 thing_inside
1521
1522 tcExtendIdBinderStackForRhs :: [MonoBindInfo] -> TcM a -> TcM a
1523 -- Extend the TcBinderStack for the RHS of the binding, with
1524 -- the monomorphic Id. That way, if we have, say
1525 -- f = \x -> blah
1526 -- and something goes wrong in 'blah', we get a "relevant binding"
1527 -- looking like f :: alpha -> beta
1528 -- This applies if 'f' has a type signature too:
1529 -- f :: forall a. [a] -> [a]
1530 -- f x = True
1531 -- We can't unify True with [a], and a relevant binding is f :: [a] -> [a]
1532 -- If we had the *polymorphic* version of f in the TcBinderStack, it
1533 -- would not be reported as relevant, because its type is closed
1534 tcExtendIdBinderStackForRhs infos thing_inside
1535 = tcExtendBinderStack [ TcIdBndr mono_id NotTopLevel
1536 | MBI { mbi_mono_id = mono_id } <- infos ]
1537 thing_inside
1538 -- NotTopLevel: it's a monomorphic binding
1539
1540 ---------------------
1541 getMonoBindInfo :: [Located TcMonoBind] -> [MonoBindInfo]
1542 getMonoBindInfo tc_binds
1543 = foldr (get_info . unLoc) [] tc_binds
1544 where
1545 get_info (TcFunBind info _ _) rest = info : rest
1546 get_info (TcPatBind infos _ _ _) rest = infos ++ rest
1547
1548
1549 {- Note [Typechecking pattern bindings]
1550 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1551 Look at:
1552 - typecheck/should_compile/ExPat
1553 - Trac #12427, typecheck/should_compile/T12427{a,b}
1554
1555 data T where
1556 MkT :: Integral a => a -> Int -> T
1557
1558 and suppose t :: T. Which of these pattern bindings are ok?
1559
1560 E1. let { MkT p _ = t } in <body>
1561
1562 E2. let { MkT _ q = t } in <body>
1563
1564 E3. let { MkT (toInteger -> r) _ = t } in <body>
1565
1566 * (E1) is clearly wrong because the existential 'a' escapes.
1567 What type could 'p' possibly have?
1568
1569 * (E2) is fine, despite the existential pattern, because
1570 q::Int, and nothing escapes.
1571
1572 * Even (E3) is fine. The existential pattern binds a dictionary
1573 for (Integral a) which the view pattern can use to convert the
1574 a-valued field to an Integer, so r :: Integer.
1575
1576 An easy way to see all three is to imagine the desugaring.
1577 For (E2) it would look like
1578 let q = case t of MkT _ q' -> q'
1579 in <body>
1580
1581
1582 We typecheck pattern bindings as follows. First tcLhs does this:
1583
1584 1. Take each type signature q :: ty, partial or complete, and
1585 instantiate it (with tcLhsSigId) to get a MonoBindInfo. This
1586 gives us a fresh "mono_id" qm :: instantiate(ty), where qm has
1587 a fresh name.
1588
1589 Any fresh unification variables in instantiate(ty) born here, not
1590 deep under implications as would happen if we allocated them when
1591 we encountered q during tcPat.
1592
1593 2. Build a little environment mapping "q" -> "qm" for those Ids
1594 with signatures (inst_sig_fun)
1595
1596 3. Invoke tcLetPat to typecheck the pattern.
1597
1598 - We pass in the current TcLevel. This is captured by
1599 TcPat.tcLetPat, and put into the pc_lvl field of PatCtxt, in
1600 PatEnv.
1601
1602 - When tcPat finds an existential constructor, it binds fresh
1603 type variables and dictionaries as usual, increments the TcLevel,
1604 and emits an implication constraint.
1605
1606 - When we come to a binder (TcPat.tcPatBndr), it looks it up
1607 in the little environment (the pc_sig_fn field of PatCtxt).
1608
1609 Success => There was a type signature, so just use it,
1610 checking compatibility with the expected type.
1611
1612 Failure => No type sigature.
1613 Infer case: (happens only outside any constructor pattern)
1614 use a unification variable
1615 at the outer level pc_lvl
1616
1617 Check case: use promoteTcType to promote the type
1618 to the outer level pc_lvl. This is the
1619 place where we emit a constraint that'll blow
1620 up if existential capture takes place
1621
1622 Result: the type of the binder is always at pc_lvl. This is
1623 crucial.
1624
1625 4. Throughout, when we are making up an Id for the pattern-bound variables
1626 (newLetBndr), we have two cases:
1627
1628 - If we are generalising (generalisation plan is InferGen or
1629 CheckGen), then the let_bndr_spec will be LetLclBndr. In that case
1630 we want to bind a cloned, local version of the variable, with the
1631 type given by the pattern context, *not* by the signature (even if
1632 there is one; see Trac #7268). The mkExport part of the
1633 generalisation step will do the checking and impedance matching
1634 against the signature.
1635
1636 - If for some some reason we are not generalising (plan = NoGen), the
1637 LetBndrSpec will be LetGblBndr. In that case we must bind the
1638 global version of the Id, and do so with precisely the type given
1639 in the signature. (Then we unify with the type from the pattern
1640 context type.)
1641
1642
1643 And that's it! The implication constraints check for the skolem
1644 escape. It's quite simple and neat, and more expressive than before
1645 e.g. GHC 8.0 rejects (E2) and (E3).
1646
1647 Example for (E1), starting at level 1. We generate
1648 p :: beta:1, with constraints (forall:3 a. Integral a => a ~ beta)
1649 The (a~beta) can't float (because of the 'a'), nor be solved (because
1650 beta is untouchable.)
1651
1652 Example for (E2), we generate
1653 q :: beta:1, with constraint (forall:3 a. Integral a => Int ~ beta)
1654 The beta is untoucable, but floats out of the constraint and can
1655 be solved absolutely fine.
1656
1657 ************************************************************************
1658 * *
1659 Generalisation
1660 * *
1661 ********************************************************************* -}
1662
1663 data GeneralisationPlan
1664 = NoGen -- No generalisation, no AbsBinds
1665
1666 | InferGen -- Implicit generalisation; there is an AbsBinds
1667 Bool -- True <=> apply the MR; generalise only unconstrained type vars
1668
1669 | CheckGen (LHsBind GhcRn) TcIdSigInfo
1670 -- One FunBind with a signature
1671 -- Explicit generalisation
1672
1673 -- A consequence of the no-AbsBinds choice (NoGen) is that there is
1674 -- no "polymorphic Id" and "monmomorphic Id"; there is just the one
1675
1676 instance Outputable GeneralisationPlan where
1677 ppr NoGen = text "NoGen"
1678 ppr (InferGen b) = text "InferGen" <+> ppr b
1679 ppr (CheckGen _ s) = text "CheckGen" <+> ppr s
1680
1681 decideGeneralisationPlan
1682 :: DynFlags -> [LHsBind GhcRn] -> IsGroupClosed -> TcSigFun
1683 -> GeneralisationPlan
1684 decideGeneralisationPlan dflags lbinds closed sig_fn
1685 | has_partial_sigs = InferGen (and partial_sig_mrs)
1686 | Just (bind, sig) <- one_funbind_with_sig = CheckGen bind sig
1687 | do_not_generalise closed = NoGen
1688 | otherwise = InferGen mono_restriction
1689 where
1690 binds = map unLoc lbinds
1691
1692 partial_sig_mrs :: [Bool]
1693 -- One for each partial signature (so empty => no partial sigs)
1694 -- The Bool is True if the signature has no constraint context
1695 -- so we should apply the MR
1696 -- See Note [Partial type signatures and generalisation]
1697 partial_sig_mrs
1698 = [ null theta
1699 | TcIdSig (PartialSig { psig_hs_ty = hs_ty })
1700 <- mapMaybe sig_fn (collectHsBindListBinders lbinds)
1701 , let (_, L _ theta, _) = splitLHsSigmaTy (hsSigWcType hs_ty) ]
1702
1703 has_partial_sigs = not (null partial_sig_mrs)
1704
1705 mono_restriction = xopt LangExt.MonomorphismRestriction dflags
1706 && any restricted binds
1707
1708 do_not_generalise (IsGroupClosed _ True) = False
1709 -- The 'True' means that all of the group's
1710 -- free vars have ClosedTypeId=True; so we can ignore
1711 -- -XMonoLocalBinds, and generalise anyway
1712 do_not_generalise _ = xopt LangExt.MonoLocalBinds dflags
1713
1714 -- With OutsideIn, all nested bindings are monomorphic
1715 -- except a single function binding with a signature
1716 one_funbind_with_sig
1717 | [lbind@(L _ (FunBind { fun_id = v }))] <- lbinds
1718 , Just (TcIdSig sig) <- sig_fn (unLoc v)
1719 = Just (lbind, sig)
1720 | otherwise
1721 = Nothing
1722
1723 -- The Haskell 98 monomorphism restriction
1724 restricted (PatBind {}) = True
1725 restricted (VarBind { var_id = v }) = no_sig v
1726 restricted (FunBind { fun_id = v, fun_matches = m }) = restricted_match m
1727 && no_sig (unLoc v)
1728 restricted b = pprPanic "isRestrictedGroup/unrestricted" (ppr b)
1729
1730 restricted_match mg = matchGroupArity mg == 0
1731 -- No args => like a pattern binding
1732 -- Some args => a function binding
1733
1734 no_sig n = not (hasCompleteSig sig_fn n)
1735
1736 isClosedBndrGroup :: TcTypeEnv -> Bag (LHsBind GhcRn) -> IsGroupClosed
1737 isClosedBndrGroup type_env binds
1738 = IsGroupClosed fv_env type_closed
1739 where
1740 type_closed = allUFM (nameSetAll is_closed_type_id) fv_env
1741
1742 fv_env :: NameEnv NameSet
1743 fv_env = mkNameEnv $ concatMap (bindFvs . unLoc) binds
1744
1745 bindFvs :: HsBindLR GhcRn idR -> [(Name, NameSet)]
1746 bindFvs (FunBind { fun_id = L _ f, bind_fvs = fvs })
1747 = let open_fvs = filterNameSet (not . is_closed) fvs
1748 in [(f, open_fvs)]
1749 bindFvs (PatBind { pat_lhs = pat, bind_fvs = fvs })
1750 = let open_fvs = filterNameSet (not . is_closed) fvs
1751 in [(b, open_fvs) | b <- collectPatBinders pat]
1752 bindFvs _
1753 = []
1754
1755 is_closed :: Name -> ClosedTypeId
1756 is_closed name
1757 | Just thing <- lookupNameEnv type_env name
1758 = case thing of
1759 AGlobal {} -> True
1760 ATcId { tct_info = ClosedLet } -> True
1761 _ -> False
1762
1763 | otherwise
1764 = True -- The free-var set for a top level binding mentions
1765
1766
1767 is_closed_type_id :: Name -> Bool
1768 -- We're already removed Global and ClosedLet Ids
1769 is_closed_type_id name
1770 | Just thing <- lookupNameEnv type_env name
1771 = case thing of
1772 ATcId { tct_info = NonClosedLet _ cl } -> cl
1773 ATcId { tct_info = NotLetBound } -> False
1774 ATyVar {} -> False
1775 -- In-scope type variables are not closed!
1776 _ -> pprPanic "is_closed_id" (ppr name)
1777
1778 | otherwise
1779 = True -- The free-var set for a top level binding mentions
1780 -- imported things too, so that we can report unused imports
1781 -- These won't be in the local type env.
1782 -- Ditto class method etc from the current module
1783
1784
1785 {- *********************************************************************
1786 * *
1787 Error contexts and messages
1788 * *
1789 ********************************************************************* -}
1790
1791 -- This one is called on LHS, when pat and grhss are both Name
1792 -- and on RHS, when pat is TcId and grhss is still Name
1793 patMonoBindsCtxt :: (SourceTextX p, OutputableBndrId p, Outputable body)
1794 => LPat p -> GRHSs GhcRn body -> SDoc
1795 patMonoBindsCtxt pat grhss
1796 = hang (text "In a pattern binding:") 2 (pprPatBind pat grhss)