6feab9e7280d57997d9b2d927b919437f3d4e012
[ghc.git] / compiler / typecheck / TcBinds.lhs
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 \begin{code}
8 {-# LANGUAGE CPP, RankNTypes, ScopedTypeVariables #-}
9
10 module TcBinds ( tcLocalBinds, tcTopBinds, tcRecSelBinds,
11                  tcHsBootSigs, tcPolyCheck,
12                  PragFun, tcSpecPrags, tcVectDecls, mkPragFun, 
13                  TcSigInfo(..), TcSigFun, 
14                  instTcTySig, instTcTySigFromId, findScopedTyVars,
15                  badBootDeclErr ) where
16
17 import {-# SOURCE #-} TcMatches ( tcGRHSsPat, tcMatchesFun )
18 import {-# SOURCE #-} TcExpr  ( tcMonoExpr )
19 import {-# SOURCE #-} TcPatSyn ( tcPatSynDecl, tcPatSynWrapper )
20
21 import DynFlags
22 import HsSyn
23 import HscTypes( isHsBoot )
24 import TcRnMonad
25 import TcEnv
26 import TcUnify
27 import TcSimplify
28 import TcEvidence
29 import TcHsType
30 import TcPat
31 import TcMType
32 import PatSyn
33 import ConLike
34 import Type( tidyOpenType )
35 import FunDeps( growThetaTyVars )
36 import TyCon
37 import TcType
38 import TysPrim
39 import Id
40 import Var
41 import VarSet
42 import VarEnv( TidyEnv )
43 import Module
44 import Name
45 import NameSet
46 import NameEnv
47 import SrcLoc
48 import Bag
49 import ListSetOps
50 import ErrUtils
51 import Digraph
52 import Maybes
53 import Util
54 import BasicTypes
55 import Outputable
56 import FastString
57 import Type(mkStrLitTy)
58 import Class(classTyCon)
59 import PrelNames(ipClassName)
60 import TcValidity (checkValidType)
61
62 import Control.Monad
63
64 #include "HsVersions.h"
65 \end{code}
66
67
68 %************************************************************************
69 %*                                                                      *
70 \subsection{Type-checking bindings}
71 %*                                                                      *
72 %************************************************************************
73
74 @tcBindsAndThen@ typechecks a @HsBinds@.  The "and then" part is because
75 it needs to know something about the {\em usage} of the things bound,
76 so that it can create specialisations of them.  So @tcBindsAndThen@
77 takes a function which, given an extended environment, E, typechecks
78 the scope of the bindings returning a typechecked thing and (most
79 important) an LIE.  It is this LIE which is then used as the basis for
80 specialising the things bound.
81
82 @tcBindsAndThen@ also takes a "combiner" which glues together the
83 bindings and the "thing" to make a new "thing".
84
85 The real work is done by @tcBindWithSigsAndThen@.
86
87 Recursive and non-recursive binds are handled in essentially the same
88 way: because of uniques there are no scoping issues left.  The only
89 difference is that non-recursive bindings can bind primitive values.
90
91 Even for non-recursive binding groups we add typings for each binder
92 to the LVE for the following reason.  When each individual binding is
93 checked the type of its LHS is unified with that of its RHS; and
94 type-checking the LHS of course requires that the binder is in scope.
95
96 At the top-level the LIE is sure to contain nothing but constant
97 dictionaries, which we resolve at the module level.
98
99 Note [Polymorphic recursion]
100 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
101 The game plan for polymorphic recursion in the code above is 
102
103         * Bind any variable for which we have a type signature
104           to an Id with a polymorphic type.  Then when type-checking 
105           the RHSs we'll make a full polymorphic call.
106
107 This fine, but if you aren't a bit careful you end up with a horrendous
108 amount of partial application and (worse) a huge space leak. For example:
109
110         f :: Eq a => [a] -> [a]
111         f xs = ...f...
112
113 If we don't take care, after typechecking we get
114
115         f = /\a -> \d::Eq a -> let f' = f a d
116                                in
117                                \ys:[a] -> ...f'...
118
119 Notice the the stupid construction of (f a d), which is of course
120 identical to the function we're executing.  In this case, the
121 polymorphic recursion isn't being used (but that's a very common case).
122 This can lead to a massive space leak, from the following top-level defn
123 (post-typechecking)
124
125         ff :: [Int] -> [Int]
126         ff = f Int dEqInt
127
128 Now (f dEqInt) evaluates to a lambda that has f' as a free variable; but
129 f' is another thunk which evaluates to the same thing... and you end
130 up with a chain of identical values all hung onto by the CAF ff.
131
132         ff = f Int dEqInt
133
134            = let f' = f Int dEqInt in \ys. ...f'...
135
136            = let f' = let f' = f Int dEqInt in \ys. ...f'...
137                       in \ys. ...f'...
138
139 Etc.
140
141 NOTE: a bit of arity anaysis would push the (f a d) inside the (\ys...),
142 which would make the space leak go away in this case
143
144 Solution: when typechecking the RHSs we always have in hand the
145 *monomorphic* Ids for each binding.  So we just need to make sure that
146 if (Method f a d) shows up in the constraints emerging from (...f...)
147 we just use the monomorphic Id.  We achieve this by adding monomorphic Ids
148 to the "givens" when simplifying constraints.  That's what the "lies_avail"
149 is doing.
150
151 Then we get
152
153         f = /\a -> \d::Eq a -> letrec
154                                  fm = \ys:[a] -> ...fm...
155                                in
156                                fm
157
158 \begin{code}
159 tcTopBinds :: HsValBinds Name -> TcM (TcGblEnv, TcLclEnv)
160 -- The TcGblEnv contains the new tcg_binds and tcg_spects
161 -- The TcLclEnv has an extended type envt for the new bindings
162 tcTopBinds (ValBindsOut binds sigs)
163   = do  { -- Pattern synonym bindings populate the global environment
164           (binds', (tcg_env, tcl_env)) <- tcValBinds TopLevel binds sigs $
165             do { gbl <- getGblEnv
166                ; lcl <- getLclEnv
167                ; return (gbl, lcl) }
168         ; specs <- tcImpPrags sigs   -- SPECIALISE prags for imported Ids
169
170         ; let { tcg_env' = tcg_env { tcg_binds = foldr (unionBags . snd)
171                                                        (tcg_binds tcg_env)
172                                                        binds'
173                                    , tcg_imp_specs = specs ++ tcg_imp_specs tcg_env } }
174
175         ; return (tcg_env', tcl_env) }
176         -- The top level bindings are flattened into a giant 
177         -- implicitly-mutually-recursive LHsBinds
178
179 tcTopBinds (ValBindsIn {}) = panic "tcTopBinds"
180
181 tcRecSelBinds :: HsValBinds Name -> TcM TcGblEnv
182 tcRecSelBinds (ValBindsOut binds sigs)
183   = tcExtendGlobalValEnv [sel_id | L _ (IdSig sel_id) <- sigs] $
184     do { (rec_sel_binds, tcg_env) <- discardWarnings (tcValBinds TopLevel binds sigs getGblEnv)
185        ; let tcg_env' 
186               | isHsBoot (tcg_src tcg_env) = tcg_env
187               | otherwise = tcg_env { tcg_binds = foldr (unionBags . snd)
188                                                         (tcg_binds tcg_env)
189                                                         rec_sel_binds }
190               -- Do not add the code for record-selector bindings when 
191               -- compiling hs-boot files
192        ; return tcg_env' }
193 tcRecSelBinds (ValBindsIn {}) = panic "tcRecSelBinds"
194
195 tcHsBootSigs :: HsValBinds Name -> TcM [Id]
196 -- A hs-boot file has only one BindGroup, and it only has type
197 -- signatures in it.  The renamer checked all this
198 tcHsBootSigs (ValBindsOut binds sigs)
199   = do  { checkTc (null binds) badBootDeclErr
200         ; concat <$> mapM (addLocM tc_boot_sig) (filter isTypeLSig sigs) }
201   where
202     tc_boot_sig (TypeSig lnames ty) = mapM f lnames
203       where
204         f (L _ name) = do  { sigma_ty <- tcHsSigType (FunSigCtxt name) ty
205                            ; return (mkVanillaGlobal name sigma_ty) }
206         -- Notice that we make GlobalIds, not LocalIds
207     tc_boot_sig s = pprPanic "tcHsBootSigs/tc_boot_sig" (ppr s)
208 tcHsBootSigs groups = pprPanic "tcHsBootSigs" (ppr groups)
209
210 badBootDeclErr :: MsgDoc
211 badBootDeclErr = ptext (sLit "Illegal declarations in an hs-boot file")
212
213 ------------------------
214 tcLocalBinds :: HsLocalBinds Name -> TcM thing
215              -> TcM (HsLocalBinds TcId, thing)
216
217 tcLocalBinds EmptyLocalBinds thing_inside 
218   = do  { thing <- thing_inside
219         ; return (EmptyLocalBinds, thing) }
220
221 tcLocalBinds (HsValBinds (ValBindsOut binds sigs)) thing_inside
222   = do  { (binds', thing) <- tcValBinds NotTopLevel binds sigs thing_inside
223         ; return (HsValBinds (ValBindsOut binds' sigs), thing) }
224 tcLocalBinds (HsValBinds (ValBindsIn {})) _ = panic "tcLocalBinds"
225
226 tcLocalBinds (HsIPBinds (IPBinds ip_binds _)) thing_inside
227   = do  { ipClass <- tcLookupClass ipClassName
228         ; (given_ips, ip_binds') <-
229             mapAndUnzipM (wrapLocSndM (tc_ip_bind ipClass)) ip_binds
230
231         -- If the binding binds ?x = E, we  must now 
232         -- discharge any ?x constraints in expr_lie
233         -- See Note [Implicit parameter untouchables]
234         ; (ev_binds, result) <- checkConstraints (IPSkol ips) 
235                                   [] given_ips thing_inside
236
237         ; return (HsIPBinds (IPBinds ip_binds' ev_binds), result) }
238   where
239     ips = [ip | L _ (IPBind (Left ip) _) <- ip_binds]
240
241         -- I wonder if we should do these one at at time
242         -- Consider     ?x = 4
243         --              ?y = ?x + 1
244     tc_ip_bind ipClass (IPBind (Left ip) expr)
245        = do { ty <- newFlexiTyVarTy openTypeKind
246             ; let p = mkStrLitTy $ hsIPNameFS ip
247             ; ip_id <- newDict ipClass [ p, ty ]
248             ; expr' <- tcMonoExpr expr ty
249             ; let d = toDict ipClass p ty `fmap` expr'
250             ; return (ip_id, (IPBind (Right ip_id) d)) }
251     tc_ip_bind _ (IPBind (Right {}) _) = panic "tc_ip_bind"
252
253     -- Coerces a `t` into a dictionry for `IP "x" t`.
254     -- co : t -> IP "x" t
255     toDict ipClass x ty =
256       case unwrapNewTyCon_maybe (classTyCon ipClass) of
257         Just (_,_,ax) -> HsWrap $ mkWpCast $ mkTcSymCo $ mkTcUnbranchedAxInstCo Representational ax [x,ty]
258         Nothing       -> panic "The dictionary for `IP` is not a newtype?"
259
260
261 \end{code}
262
263 Note [Implicit parameter untouchables]
264 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
265 We add the type variables in the types of the implicit parameters
266 as untouchables, not so much because we really must not unify them,
267 but rather because we otherwise end up with constraints like this
268     Num alpha, Implic { wanted = alpha ~ Int }
269 The constraint solver solves alpha~Int by unification, but then
270 doesn't float that solved constraint out (it's not an unsolved 
271 wanted).  Result disaster: the (Num alpha) is again solved, this
272 time by defaulting.  No no no.
273
274 However [Oct 10] this is all handled automatically by the 
275 untouchable-range idea.
276
277 Note [Placeholder PatSyn kinds]
278 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
279 Consider this (Trac #9161)
280
281   {-# LANGUAGE PatternSynonyms, DataKinds #-}
282   pattern A = ()
283   b :: A
284   b = undefined
285
286 Here, the type signature for b mentions A.  But A is a pattern
287 synonym, which is typechecked (for very good reasons; a view pattern
288 in the RHS may mention a value binding) as part of a group of
289 bindings.  It is entirely resonable to reject this, but to do so
290 we need A to be in the kind environment when kind-checking the signature for B.
291
292 Hence the tcExtendKindEnv2 patsyn_placeholder_kinds, which adds a binding
293     A -> AGlobal (AConLike (PatSynCon _|_))
294 to the environment. Then TcHsType.tcTyVar will find A in the kind environment,
295 and will give a 'wrongThingErr' as a result.  But the lookup of A won't fail.
296
297 The _|_ (= panic "fakePatSynCon") works because the wrongThingErr call, in
298 tcTyVar, doesn't look inside the TcTyThing.
299
300
301 \begin{code}
302 tcValBinds :: TopLevelFlag 
303            -> [(RecFlag, LHsBinds Name)] -> [LSig Name]
304            -> TcM thing
305            -> TcM ([(RecFlag, LHsBinds TcId)], thing) 
306
307 tcValBinds top_lvl binds sigs thing_inside
308   = do  {  -- Typecheck the signature
309         ; (poly_ids, sig_fn) <- tcExtendKindEnv2 patsyn_placeholder_kinds $
310                                      -- See Note [Placeholder PatSyn kinds]
311                                 tcTySigs sigs
312
313         ; let prag_fn = mkPragFun sigs (foldr (unionBags . snd) emptyBag binds)
314
315                 -- Extend the envt right away with all 
316                 -- the Ids declared with type signatures
317                 -- Use tcExtendIdEnv2 to avoid extending the TcIdBinder stack
318         ; tcExtendIdEnv2 [(idName id, id) | id <- poly_ids] $ do
319             { (binds', (extra_binds', thing)) <- tcBindGroups top_lvl sig_fn prag_fn binds $ do
320                    { thing <- thing_inside
321                      -- See Note [Pattern synonym wrappers don't yield dependencies]
322                    ; patsyn_wrappers <- mapM tcPatSynWrapper patsyns
323                    ; let extra_binds = [ (NonRecursive, wrapper) | wrapper <- patsyn_wrappers ]
324                    ; return (extra_binds, thing) }
325              ; return (binds' ++ extra_binds', thing) }}
326   where
327     patsyns
328       = [psb | (_, lbinds) <- binds, L _ (PatSynBind psb) <- bagToList lbinds]
329     patsyn_placeholder_kinds -- See Note [Placeholder PatSyn kinds]
330       = [(name, placeholder_patsyn_tything)| PSB{ psb_id = L _ name } <- patsyns ]
331     placeholder_patsyn_tything
332       = AGlobal $ AConLike $ PatSynCon $ panic "fakePatSynCon"
333
334 ------------------------
335 tcBindGroups :: TopLevelFlag -> TcSigFun -> PragFun
336              -> [(RecFlag, LHsBinds Name)] -> TcM thing
337              -> TcM ([(RecFlag, LHsBinds TcId)], thing)
338 -- Typecheck a whole lot of value bindings,
339 -- one strongly-connected component at a time
340 -- Here a "strongly connected component" has the strightforward
341 -- meaning of a group of bindings that mention each other, 
342 -- ignoring type signatures (that part comes later)
343
344 tcBindGroups _ _ _ [] thing_inside
345   = do  { thing <- thing_inside
346         ; return ([], thing) }
347
348 tcBindGroups top_lvl sig_fn prag_fn (group : groups) thing_inside
349   = do  { (group', (groups', thing))
350                 <- tc_group top_lvl sig_fn prag_fn group $ 
351                    tcBindGroups top_lvl sig_fn prag_fn groups thing_inside
352         ; return (group' ++ groups', thing) }
353
354 ------------------------
355 tc_group :: forall thing. 
356             TopLevelFlag -> TcSigFun -> PragFun
357          -> (RecFlag, LHsBinds Name) -> TcM thing
358          -> TcM ([(RecFlag, LHsBinds TcId)], thing)
359
360 -- Typecheck one strongly-connected component of the original program.
361 -- We get a list of groups back, because there may 
362 -- be specialisations etc as well
363
364 tc_group top_lvl sig_fn prag_fn (NonRecursive, binds) thing_inside
365         -- A single non-recursive binding
366         -- We want to keep non-recursive things non-recursive
367         -- so that we desugar unlifted bindings correctly
368   = do { let bind = case bagToList binds of
369                  [] -> panic "tc_group: empty list of binds"
370                  [bind] -> bind
371                  _ -> panic "tc_group: NonRecursive binds is not a singleton bag"
372        ; (bind', thing) <- tc_single top_lvl sig_fn prag_fn bind thing_inside
373        ; return ( [(NonRecursive, bind')], thing) }
374
375 tc_group top_lvl sig_fn prag_fn (Recursive, binds) thing_inside
376   =     -- To maximise polymorphism, we do a new 
377         -- strongly-connected-component analysis, this time omitting 
378         -- any references to variables with type signatures.
379         -- (This used to be optional, but isn't now.)
380     do  { traceTc "tc_group rec" (pprLHsBinds binds)
381         ; when hasPatSyn $ recursivePatSynErr binds
382         ; (binds1, _ids, thing) <- go sccs
383              -- Here is where we should do bindInstsOfLocalFuns
384              -- if we start having Methods again
385         ; return ([(Recursive, binds1)], thing) }
386                 -- Rec them all together
387   where
388     hasPatSyn = anyBag (isPatSyn . unLoc) binds
389     isPatSyn PatSynBind{} = True
390     isPatSyn _ = False
391
392     sccs :: [SCC (LHsBind Name)]
393     sccs = stronglyConnCompFromEdgedVertices (mkEdges sig_fn binds)
394
395     go :: [SCC (LHsBind Name)] -> TcM (LHsBinds TcId, [TcId], thing)
396     go (scc:sccs) = do  { (binds1, ids1, closed) <- tc_scc scc
397                         ; (binds2, ids2, thing)  <- tcExtendLetEnv top_lvl closed ids1 $ 
398                                                     go sccs
399                         ; return (binds1 `unionBags` binds2, ids1 ++ ids2, thing) }
400     go []         = do  { thing <- thing_inside; return (emptyBag, [], thing) }
401
402     tc_scc (AcyclicSCC bind) = tc_sub_group NonRecursive [bind]
403     tc_scc (CyclicSCC binds) = tc_sub_group Recursive    binds
404
405     tc_sub_group = tcPolyBinds top_lvl sig_fn prag_fn Recursive
406
407 recursivePatSynErr :: OutputableBndr name => LHsBinds name -> TcM a
408 recursivePatSynErr binds
409   = failWithTc $
410     hang (ptext (sLit "Recursive pattern synonym definition with following bindings:"))
411        2 (vcat $ map pprLBind . bagToList $ binds)
412   where
413     pprLoc loc  = parens (ptext (sLit "defined at") <+> ppr loc)
414     pprLBind (L loc bind) = pprWithCommas ppr (collectHsBindBinders bind) <+>
415                             pprLoc loc
416
417 tc_single :: forall thing.
418             TopLevelFlag -> TcSigFun -> PragFun
419           -> LHsBind Name -> TcM thing
420           -> TcM (LHsBinds TcId, thing)
421 tc_single _top_lvl _sig_fn _prag_fn (L _ (PatSynBind psb)) thing_inside
422   = do { (pat_syn, aux_binds) <- tcPatSynDecl psb
423
424        ; let tything = AConLike (PatSynCon pat_syn)
425              implicit_ids = (patSynMatcher pat_syn) :
426                             (maybeToList (patSynWrapper pat_syn))
427
428        ; thing <- tcExtendGlobalEnv [tything] $
429                   tcExtendGlobalEnvImplicit (map AnId implicit_ids) $
430                   thing_inside
431        ; return (aux_binds, thing)
432        }
433 tc_single top_lvl sig_fn prag_fn lbind thing_inside
434   = do { (binds1, ids, closed) <- tcPolyBinds top_lvl sig_fn prag_fn
435                                     NonRecursive NonRecursive
436                                     [lbind]
437        ; thing <- tcExtendLetEnv top_lvl closed ids thing_inside
438        ; return (binds1, thing) }
439           
440 ------------------------
441 mkEdges :: TcSigFun -> LHsBinds Name
442         -> [(LHsBind Name, BKey, [BKey])]
443
444 type BKey  = Int -- Just number off the bindings
445
446 mkEdges sig_fn binds
447   = [ (bind, key, [key | n <- nameSetToList (bind_fvs (unLoc bind)),
448                          Just key <- [lookupNameEnv key_map n], no_sig n ])
449     | (bind, key) <- keyd_binds
450     ]
451   where
452     no_sig :: Name -> Bool
453     no_sig n = isNothing (sig_fn n)
454
455     keyd_binds = bagToList binds `zip` [0::BKey ..]
456
457     key_map :: NameEnv BKey     -- Which binding it comes from
458     key_map = mkNameEnv [(bndr, key) | (L _ bind, key) <- keyd_binds
459                                      , bndr <- bindersOfHsBind bind ]
460
461 bindersOfHsBind :: HsBind Name -> [Name]
462 bindersOfHsBind (PatBind { pat_lhs = pat })           = collectPatBinders pat
463 bindersOfHsBind (FunBind { fun_id = L _ f })          = [f]
464 bindersOfHsBind (PatSynBind PSB{ psb_id = L _ psyn }) = [psyn]
465 bindersOfHsBind (AbsBinds {})                         = panic "bindersOfHsBind AbsBinds"
466 bindersOfHsBind (VarBind {})                          = panic "bindersOfHsBind VarBind"
467
468 ------------------------
469 tcPolyBinds :: TopLevelFlag -> TcSigFun -> PragFun
470             -> RecFlag       -- Whether the group is really recursive
471             -> RecFlag       -- Whether it's recursive after breaking
472                              -- dependencies based on type signatures
473             -> [LHsBind Name]
474             -> TcM (LHsBinds TcId, [TcId], TopLevelFlag)
475
476 -- Typechecks a single bunch of bindings all together, 
477 -- and generalises them.  The bunch may be only part of a recursive
478 -- group, because we use type signatures to maximise polymorphism
479 --
480 -- Returns a list because the input may be a single non-recursive binding,
481 -- in which case the dependency order of the resulting bindings is
482 -- important.  
483 -- 
484 -- Knows nothing about the scope of the bindings
485
486 tcPolyBinds top_lvl sig_fn prag_fn rec_group rec_tc bind_list
487   = setSrcSpan loc                              $
488     recoverM (recoveryCode binder_names sig_fn) $ do 
489         -- Set up main recover; take advantage of any type sigs
490
491     { traceTc "------------------------------------------------" empty
492     ; traceTc "Bindings for {" (ppr binder_names)
493     ; dflags   <- getDynFlags
494     ; type_env <- getLclTypeEnv
495     ; let plan = decideGeneralisationPlan dflags type_env 
496                          binder_names bind_list sig_fn
497     ; traceTc "Generalisation plan" (ppr plan)
498     ; result@(tc_binds, poly_ids, _) <- case plan of
499          NoGen               -> tcPolyNoGen rec_tc prag_fn sig_fn bind_list
500          InferGen mn cl      -> tcPolyInfer rec_tc prag_fn sig_fn mn cl bind_list
501          CheckGen lbind sig  -> tcPolyCheck rec_tc prag_fn sig lbind
502
503         -- Check whether strict bindings are ok
504         -- These must be non-recursive etc, and are not generalised
505         -- They desugar to a case expression in the end
506     ; checkStrictBinds top_lvl rec_group bind_list tc_binds poly_ids
507     ; traceTc "} End of bindings for" (vcat [ ppr binder_names, ppr rec_group
508                                             , vcat [ppr id <+> ppr (idType id) | id <- poly_ids]
509                                           ])
510
511     ; return result }
512   where
513     binder_names = collectHsBindListBinders bind_list
514     loc = foldr1 combineSrcSpans (map getLoc bind_list)
515          -- The mbinds have been dependency analysed and 
516          -- may no longer be adjacent; so find the narrowest
517          -- span that includes them all
518
519 ------------------
520 tcPolyNoGen     -- No generalisation whatsoever
521   :: RecFlag       -- Whether it's recursive after breaking
522                    -- dependencies based on type signatures
523   -> PragFun -> TcSigFun
524   -> [LHsBind Name]
525   -> TcM (LHsBinds TcId, [TcId], TopLevelFlag)
526
527 tcPolyNoGen rec_tc prag_fn tc_sig_fn bind_list
528   = do { (binds', mono_infos) <- tcMonoBinds rec_tc tc_sig_fn
529                                              (LetGblBndr prag_fn) 
530                                              bind_list
531        ; mono_ids' <- mapM tc_mono_info mono_infos
532        ; return (binds', mono_ids', NotTopLevel) }
533   where
534     tc_mono_info (name, _, mono_id)
535       = do { mono_ty' <- zonkTcType (idType mono_id)
536              -- Zonk, mainly to expose unboxed types to checkStrictBinds
537            ; let mono_id' = setIdType mono_id mono_ty'
538            ; _specs <- tcSpecPrags mono_id' (prag_fn name)
539            ; return mono_id' }
540            -- NB: tcPrags generates error messages for
541            --     specialisation pragmas for non-overloaded sigs
542            -- Indeed that is why we call it here!
543            -- So we can safely ignore _specs
544
545 ------------------
546 tcPolyCheck :: RecFlag       -- Whether it's recursive after breaking
547                              -- dependencies based on type signatures
548             -> PragFun -> TcSigInfo 
549             -> LHsBind Name
550             -> TcM (LHsBinds TcId, [TcId], TopLevelFlag)
551 -- There is just one binding, 
552 --   it binds a single variable,
553 --   it has a signature,
554 tcPolyCheck rec_tc prag_fn
555             sig@(TcSigInfo { sig_id = poly_id, sig_tvs = tvs_w_scoped 
556                            , sig_theta = theta, sig_tau = tau, sig_loc = loc })
557             bind
558   = do { ev_vars <- newEvVars theta
559        ; let skol_info = SigSkol (FunSigCtxt (idName poly_id)) (mkPhiTy theta tau)
560              prag_sigs = prag_fn (idName poly_id)
561              tvs = map snd tvs_w_scoped
562        ; (ev_binds, (binds', [mono_info])) 
563             <- setSrcSpan loc $  
564                checkConstraints skol_info tvs ev_vars $
565                tcExtendTyVarEnv2 [(n,tv) | (Just n, tv) <- tvs_w_scoped] $
566                tcMonoBinds rec_tc (\_ -> Just sig) LetLclBndr [bind]
567
568        ; spec_prags <- tcSpecPrags poly_id prag_sigs
569        ; poly_id    <- addInlinePrags poly_id prag_sigs
570
571        ; let (_, _, mono_id) = mono_info
572              export = ABE { abe_wrap = idHsWrapper
573                           , abe_poly = poly_id
574                           , abe_mono = mono_id
575                           , abe_prags = SpecPrags spec_prags }
576              abs_bind = L loc $ AbsBinds 
577                         { abs_tvs = tvs
578                         , abs_ev_vars = ev_vars, abs_ev_binds = ev_binds
579                         , abs_exports = [export], abs_binds = binds' }
580              closed | isEmptyVarSet (tyVarsOfType (idType poly_id)) = TopLevel
581                     | otherwise                                     = NotTopLevel
582        ; return (unitBag abs_bind, [poly_id], closed) }
583
584 ------------------
585 tcPolyInfer 
586   :: RecFlag       -- Whether it's recursive after breaking
587                    -- dependencies based on type signatures
588   -> PragFun -> TcSigFun 
589   -> Bool         -- True <=> apply the monomorphism restriction
590   -> Bool         -- True <=> free vars have closed types
591   -> [LHsBind Name]
592   -> TcM (LHsBinds TcId, [TcId], TopLevelFlag)
593 tcPolyInfer rec_tc prag_fn tc_sig_fn mono closed bind_list
594   = do { ((binds', mono_infos), wanted)
595              <- captureConstraints $
596                 tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list
597
598        ; let name_taus = [(name, idType mono_id) | (name, _, mono_id) <- mono_infos]
599        ; traceTc "simplifyInfer call" (ppr name_taus $$ ppr wanted)
600        ; (qtvs, givens, mr_bites, ev_binds)
601                  <- simplifyInfer closed mono name_taus wanted
602
603        ; theta   <- zonkTcThetaType (map evVarPred givens)
604        ; exports <- checkNoErrs $ mapM (mkExport prag_fn qtvs theta) mono_infos
605        ; loc <- getSrcSpanM
606        ; let poly_ids = map abe_poly exports
607              final_closed | closed && not mr_bites = TopLevel
608                           | otherwise              = NotTopLevel
609              abs_bind = L loc $ 
610                         AbsBinds { abs_tvs = qtvs
611                                  , abs_ev_vars = givens, abs_ev_binds = ev_binds
612                                  , abs_exports = exports, abs_binds = binds' }
613
614        ; traceTc "Binding:" (ppr final_closed $$
615                              ppr (poly_ids `zip` map idType poly_ids))
616        ; return (unitBag abs_bind, poly_ids, final_closed) }
617          -- poly_ids are guaranteed zonked by mkExport
618
619 --------------
620 mkExport :: PragFun
621          -> [TyVar] -> TcThetaType      -- Both already zonked
622          -> MonoBindInfo
623          -> TcM (ABExport Id)
624 -- Only called for generalisation plan IferGen, not by CheckGen or NoGen
625 --
626 -- mkExport generates exports with
627 --      zonked type variables,
628 --      zonked poly_ids
629 -- The former is just because no further unifications will change
630 -- the quantified type variables, so we can fix their final form
631 -- right now.
632 -- The latter is needed because the poly_ids are used to extend the
633 -- type environment; see the invariant on TcEnv.tcExtendIdEnv
634
635 -- Pre-condition: the qtvs and theta are already zonked
636
637 mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id)
638   = do  { mono_ty <- zonkTcType (idType mono_id)
639
640         ; poly_id <- case mb_sig of
641                        Just sig -> return (sig_id sig)
642                        Nothing  -> mkInferredPolyId poly_name qtvs theta mono_ty
643
644         -- NB: poly_id has a zonked type
645         ; poly_id <- addInlinePrags poly_id prag_sigs
646         ; spec_prags <- tcSpecPrags poly_id prag_sigs
647                 -- tcPrags requires a zonked poly_id
648
649         ; let sel_poly_ty = mkSigmaTy qtvs theta mono_ty
650         ; traceTc "mkExport: check sig"
651                   (ppr poly_name $$ ppr sel_poly_ty $$ ppr (idType poly_id))
652
653         -- Perform the impedence-matching and ambiguity check
654         -- right away.  If it fails, we want to fail now (and recover
655         -- in tcPolyBinds).  If we delay checking, we get an error cascade.
656         -- Remember we are in the tcPolyInfer case, so the type envt is
657         -- closed (unless we are doing NoMonoLocalBinds in which case all bets
658         -- are off)
659         -- See Note [Impedence matching]
660         ; (wrap, wanted) <- addErrCtxtM (mk_bind_msg inferred True poly_name (idType poly_id)) $
661                             captureConstraints $
662                             tcSubType origin sig_ctxt sel_poly_ty (idType poly_id)
663         ; ev_binds <- simplifyTop wanted
664
665         ; return (ABE { abe_wrap = mkWpLet (EvBinds ev_binds) <.> wrap
666                       , abe_poly = poly_id
667                       , abe_mono = mono_id
668                       , abe_prags = SpecPrags spec_prags }) }
669   where
670     inferred = isNothing mb_sig
671     prag_sigs = prag_fn poly_name
672     origin    = AmbigOrigin sig_ctxt
673     sig_ctxt  = InfSigCtxt poly_name
674
675 mkInferredPolyId :: Name -> [TyVar] -> TcThetaType -> TcType -> TcM Id
676 -- In the inference case (no signature) this stuff figures out
677 -- the right type variables and theta to quantify over
678 -- See Note [Validity of inferred types]
679 mkInferredPolyId poly_name qtvs theta mono_ty
680   = addErrCtxtM (mk_bind_msg True False poly_name inferred_poly_ty) $
681     do { checkValidType (InfSigCtxt poly_name) inferred_poly_ty
682        ; return (mkLocalId poly_name inferred_poly_ty) }
683   where
684     my_tvs2 = closeOverKinds (growThetaTyVars theta (tyVarsOfType mono_ty))
685                   -- Include kind variables!  Trac #7916
686     my_tvs   = filter (`elemVarSet` my_tvs2) qtvs   -- Maintain original order
687     my_theta = filter (quantifyPred my_tvs2) theta
688     inferred_poly_ty = mkSigmaTy my_tvs my_theta mono_ty
689
690 mk_bind_msg :: Bool -> Bool -> Name -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
691 mk_bind_msg inferred want_ambig poly_name poly_ty tidy_env
692  = return (tidy_env', msg)
693  where
694    msg = vcat [ ptext (sLit "When checking that") <+> quotes (ppr poly_name)
695                 <+> ptext (sLit "has the") <+> what <+> ptext (sLit "type")
696               , nest 2 (ppr poly_name <+> dcolon <+> ppr tidy_ty)
697               , ppWhen want_ambig $
698                 ptext (sLit "Probable cause: the inferred type is ambiguous") ]
699    what | inferred  = ptext (sLit "inferred")
700         | otherwise = ptext (sLit "specified")
701    (tidy_env', tidy_ty) = tidyOpenType tidy_env poly_ty
702 \end{code}
703
704 Note [Validity of inferred types]
705 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
706 We need to check inferred type for validity, in case it uses language 
707 extensions that are not turned on.  The principle is that if the user
708 simply adds the inferred type to the program source, it'll compile fine.
709 See #8883.
710
711 Examples that might fail:
712  - an inferred theta that requires type equalities e.g. (F a ~ G b)
713                                 or multi-parameter type classes
714  - an inferred type that includes unboxed tuples
715
716 However we don't do the ambiguity check (checkValidType omits it for
717 InfSigCtxt) because the impedence-matching stage, which follows 
718 immediately, will do it and we don't want two error messages.
719 Moreover, because of the impedence matching stage, the ambiguity-check
720 suggestion of -XAllowAmbiguiousTypes will not work.
721
722
723 Note [Impedence matching]
724 ~~~~~~~~~~~~~~~~~~~~~~~~~
725 Consider
726    f 0 x = x
727    f n x = g [] (not x)
728
729    g [] y = f 10 y
730    g _  y = f 9  y
731
732 After typechecking we'll get
733   f_mono_ty :: a -> Bool -> Bool   
734   g_mono_ty :: [b] -> Bool -> Bool 
735 with constraints
736   (Eq a, Num a)
737
738 Note that f is polymorphic in 'a' and g in 'b'; and these are not linked.
739 The types we really want for f and g are
740    f :: forall a. (Eq a, Num a) => a -> Bool -> Bool
741    g :: forall b. [b] -> Bool -> Bool
742
743 We can get these by "impedence matching":
744    tuple :: forall a b. (Eq a, Num a) => (a -> Bool -> Bool, [b] -> Bool -> Bool)
745    tuple a b d1 d1 = let ...bind f_mono, g_mono in (f_mono, g_mono)
746
747    f a d1 d2 = case tuple a Any d1 d2 of (f, g) -> f
748    g b = case tuple Integer b dEqInteger dNumInteger of (f,g) -> g
749
750 Suppose the shared quantified tyvars are qtvs and constraints theta.
751 Then we want to check that 
752    f's polytype  is more polymorphic than   forall qtvs. theta => f_mono_ty
753 and the proof is the impedence matcher.  
754
755 Notice that the impedence matcher may do defaulting.  See Trac #7173.
756
757 It also cleverly does an ambiguity check; for example, rejecting
758    f :: F a -> a
759 where F is a non-injective type function.
760
761
762 \begin{code}
763 type PragFun = Name -> [LSig Name]
764
765 mkPragFun :: [LSig Name] -> LHsBinds Name -> PragFun
766 mkPragFun sigs binds = \n -> lookupNameEnv prag_env n `orElse` []
767   where
768     prs = mapMaybe get_sig sigs
769
770     get_sig :: LSig Name -> Maybe (Located Name, LSig Name)
771     get_sig (L l (SpecSig nm ty inl)) = Just (nm, L l $ SpecSig  nm ty (add_arity nm inl))
772     get_sig (L l (InlineSig nm inl))  = Just (nm, L l $ InlineSig nm   (add_arity nm inl))
773     get_sig _                         = Nothing
774
775     add_arity (L _ n) inl_prag   -- Adjust inl_sat field to match visible arity of function
776       | Just ar <- lookupNameEnv ar_env n,
777         Inline <- inl_inline inl_prag     = inl_prag { inl_sat = Just ar }
778         -- add arity only for real INLINE pragmas, not INLINABLE
779       | otherwise                         = inl_prag
780
781     prag_env :: NameEnv [LSig Name]
782     prag_env = foldl add emptyNameEnv prs
783     add env (L _ n,p) = extendNameEnv_Acc (:) singleton env n p
784
785     -- ar_env maps a local to the arity of its definition
786     ar_env :: NameEnv Arity
787     ar_env = foldrBag lhsBindArity emptyNameEnv binds
788
789 lhsBindArity :: LHsBind Name -> NameEnv Arity -> NameEnv Arity
790 lhsBindArity (L _ (FunBind { fun_id = id, fun_matches = ms })) env
791   = extendNameEnv env (unLoc id) (matchGroupArity ms)
792 lhsBindArity _ env = env        -- PatBind/VarBind
793
794 ------------------
795 tcSpecPrags :: Id -> [LSig Name]
796             -> TcM [LTcSpecPrag]
797 -- Add INLINE and SPECIALSE pragmas
798 --    INLINE prags are added to the (polymorphic) Id directly
799 --    SPECIALISE prags are passed to the desugarer via TcSpecPrags
800 -- Pre-condition: the poly_id is zonked
801 -- Reason: required by tcSubExp
802 tcSpecPrags poly_id prag_sigs
803   = do { traceTc "tcSpecPrags" (ppr poly_id <+> ppr spec_sigs)
804        ; unless (null bad_sigs) warn_discarded_sigs
805        ; mapAndRecoverM (wrapLocM (tcSpec poly_id)) spec_sigs }
806   where
807     spec_sigs = filter isSpecLSig prag_sigs
808     bad_sigs  = filter is_bad_sig prag_sigs
809     is_bad_sig s = not (isSpecLSig s || isInlineLSig s)
810
811     warn_discarded_sigs = warnPrags poly_id bad_sigs $
812                           ptext (sLit "Discarding unexpected pragmas for")
813
814
815 --------------
816 tcSpec :: TcId -> Sig Name -> TcM TcSpecPrag
817 tcSpec poly_id prag@(SpecSig fun_name hs_ty inl) 
818   -- The Name fun_name in the SpecSig may not be the same as that of the poly_id
819   -- Example: SPECIALISE for a class method: the Name in the SpecSig is
820   --          for the selector Id, but the poly_id is something like $cop
821   -- However we want to use fun_name in the error message, since that is
822   -- what the user wrote (Trac #8537)
823   = addErrCtxt (spec_ctxt prag) $
824     do  { spec_ty <- tcHsSigType sig_ctxt hs_ty
825         ; warnIf (not (isOverloadedTy poly_ty || isInlinePragma inl))
826                  (ptext (sLit "SPECIALISE pragma for non-overloaded function") 
827                   <+> quotes (ppr fun_name))
828                   -- Note [SPECIALISE pragmas]
829         ; wrap <- tcSubType origin sig_ctxt (idType poly_id) spec_ty
830         ; return (SpecPrag poly_id wrap inl) }
831   where
832     name      = idName poly_id
833     poly_ty   = idType poly_id
834     origin    = SpecPragOrigin name
835     sig_ctxt  = FunSigCtxt name
836     spec_ctxt prag = hang (ptext (sLit "In the SPECIALISE pragma")) 2 (ppr prag)
837
838 tcSpec _ prag = pprPanic "tcSpec" (ppr prag)
839
840 --------------
841 tcImpPrags :: [LSig Name] -> TcM [LTcSpecPrag]
842 -- SPECIALISE pragmas for imported things
843 tcImpPrags prags
844   = do { this_mod <- getModule
845        ; dflags <- getDynFlags
846        ; if (not_specialising dflags) then
847             return []
848          else
849             mapAndRecoverM (wrapLocM tcImpSpec) 
850             [L loc (name,prag) | (L loc prag@(SpecSig (L _ name) _ _)) <- prags
851                                , not (nameIsLocalOrFrom this_mod name) ] }
852   where
853     -- Ignore SPECIALISE pragmas for imported things
854     -- when we aren't specialising, or when we aren't generating
855     -- code.  The latter happens when Haddocking the base library;
856     -- we don't wnat complaints about lack of INLINABLE pragmas 
857     not_specialising dflags
858       | not (gopt Opt_Specialise dflags) = True
859       | otherwise = case hscTarget dflags of
860                       HscNothing -> True
861                       HscInterpreted -> True
862                       _other         -> False
863
864 tcImpSpec :: (Name, Sig Name) -> TcM TcSpecPrag
865 tcImpSpec (name, prag)
866  = do { id <- tcLookupId name
867       ; unless (isAnyInlinePragma (idInlinePragma id))
868                (addWarnTc (impSpecErr name))
869       ; tcSpec id prag }
870
871 impSpecErr :: Name -> SDoc
872 impSpecErr name
873   = hang (ptext (sLit "You cannot SPECIALISE") <+> quotes (ppr name))
874        2 (vcat [ ptext (sLit "because its definition has no INLINE/INLINABLE pragma")
875                , parens $ sep 
876                    [ ptext (sLit "or its defining module") <+> quotes (ppr mod)
877                    , ptext (sLit "was compiled without -O")]])
878   where
879     mod = nameModule name
880
881 --------------
882 tcVectDecls :: [LVectDecl Name] -> TcM ([LVectDecl TcId])
883 tcVectDecls decls 
884   = do { decls' <- mapM (wrapLocM tcVect) decls
885        ; let ids  = [lvectDeclName decl | decl <- decls', not $ lvectInstDecl decl]
886              dups = findDupsEq (==) ids
887        ; mapM_ reportVectDups dups
888        ; traceTcConstraints "End of tcVectDecls"
889        ; return decls'
890        }
891   where
892     reportVectDups (first:_second:_more) 
893       = addErrAt (getSrcSpan first) $
894           ptext (sLit "Duplicate vectorisation declarations for") <+> ppr first
895     reportVectDups _ = return ()
896
897 --------------
898 tcVect :: VectDecl Name -> TcM (VectDecl TcId)
899 -- FIXME: We can't typecheck the expression of a vectorisation declaration against the vectorised
900 --   type of the original definition as this requires internals of the vectoriser not available
901 --   during type checking.  Instead, constrain the rhs of a vectorisation declaration to be a single
902 --   identifier (this is checked in 'rnHsVectDecl').  Fix this by enabling the use of 'vectType'
903 --   from the vectoriser here.
904 tcVect (HsVect name rhs)
905   = addErrCtxt (vectCtxt name) $
906     do { var <- wrapLocM tcLookupId name
907        ; let L rhs_loc (HsVar rhs_var_name) = rhs
908        ; rhs_id <- tcLookupId rhs_var_name
909        ; return $ HsVect var (L rhs_loc (HsVar rhs_id))
910        }
911
912 {- OLD CODE:
913          -- turn the vectorisation declaration into a single non-recursive binding
914        ; let bind    = L loc $ mkTopFunBind name [mkSimpleMatch [] rhs] 
915              sigFun  = const Nothing
916              pragFun = mkPragFun [] (unitBag bind)
917
918          -- perform type inference (including generalisation)
919        ; (binds, [id'], _) <- tcPolyInfer False True sigFun pragFun NonRecursive [bind]
920        
921        ; traceTc "tcVect inferred type" $ ppr (varType id')
922        ; traceTc "tcVect bindings"      $ ppr binds
923        
924          -- add all bindings, including the type variable and dictionary bindings produced by type
925          -- generalisation to the right-hand side of the vectorisation declaration
926        ; let [AbsBinds tvs evs _ evBinds actualBinds] = (map unLoc . bagToList) binds
927        ; let [bind']                                  = bagToList actualBinds
928              MatchGroup 
929                [L _ (Match _ _ (GRHSs [L _ (GRHS _ rhs')] _))]
930                _                                      = (fun_matches . unLoc) bind'
931              rhsWrapped                               = mkHsLams tvs evs (mkHsDictLet evBinds rhs')
932         
933         -- We return the type-checked 'Id', to propagate the inferred signature
934         -- to the vectoriser - see "Note [Typechecked vectorisation pragmas]" in HsDecls
935        ; return $ HsVect (L loc id') (Just rhsWrapped)
936        }
937  -}
938 tcVect (HsNoVect name)
939   = addErrCtxt (vectCtxt name) $
940     do { var <- wrapLocM tcLookupId name
941        ; return $ HsNoVect var
942        }
943 tcVect (HsVectTypeIn isScalar lname rhs_name)
944   = addErrCtxt (vectCtxt lname) $
945     do { tycon <- tcLookupLocatedTyCon lname
946        ; checkTc (   not isScalar             -- either    we have a non-SCALAR declaration
947                  || isJust rhs_name           -- or        we explicitly provide a vectorised type
948                  || tyConArity tycon == 0     -- otherwise the type constructor must be nullary
949                  )
950                  scalarTyConMustBeNullary
951
952        ; rhs_tycon <- fmapMaybeM (tcLookupTyCon . unLoc) rhs_name
953        ; return $ HsVectTypeOut isScalar tycon rhs_tycon
954        }
955 tcVect (HsVectTypeOut _ _ _)
956   = panic "TcBinds.tcVect: Unexpected 'HsVectTypeOut'"
957 tcVect (HsVectClassIn lname)
958   = addErrCtxt (vectCtxt lname) $
959     do { cls <- tcLookupLocatedClass lname
960        ; return $ HsVectClassOut cls
961        }
962 tcVect (HsVectClassOut _)
963   = panic "TcBinds.tcVect: Unexpected 'HsVectClassOut'"
964 tcVect (HsVectInstIn linstTy)
965   = addErrCtxt (vectCtxt linstTy) $
966     do { (cls, tys) <- tcHsVectInst linstTy
967        ; inst       <- tcLookupInstance cls tys
968        ; return $ HsVectInstOut inst
969        }
970 tcVect (HsVectInstOut _)
971   = panic "TcBinds.tcVect: Unexpected 'HsVectInstOut'"
972
973 vectCtxt :: Outputable thing => thing -> SDoc
974 vectCtxt thing = ptext (sLit "When checking the vectorisation declaration for") <+> ppr thing
975
976 scalarTyConMustBeNullary :: MsgDoc
977 scalarTyConMustBeNullary = ptext (sLit "VECTORISE SCALAR type constructor must be nullary")
978
979 --------------
980 -- If typechecking the binds fails, then return with each
981 -- signature-less binder given type (forall a.a), to minimise 
982 -- subsequent error messages
983 recoveryCode :: [Name] -> TcSigFun -> TcM (LHsBinds TcId, [Id], TopLevelFlag)
984 recoveryCode binder_names sig_fn
985   = do  { traceTc "tcBindsWithSigs: error recovery" (ppr binder_names)
986         ; poly_ids <- mapM mk_dummy binder_names
987         ; return (emptyBag, poly_ids, if all is_closed poly_ids
988                                       then TopLevel else NotTopLevel) }
989   where
990     mk_dummy name 
991         | isJust (sig_fn name) = tcLookupId name        -- Had signature; look it up
992         | otherwise            = return (mkLocalId name forall_a_a)    -- No signature
993
994     is_closed poly_id = isEmptyVarSet (tyVarsOfType (idType poly_id))
995
996 forall_a_a :: TcType
997 forall_a_a = mkForAllTy openAlphaTyVar (mkTyVarTy openAlphaTyVar)
998 \end{code}
999
1000 Note [SPECIALISE pragmas]
1001 ~~~~~~~~~~~~~~~~~~~~~~~~~
1002 There is no point in a SPECIALISE pragma for a non-overloaded function:
1003    reverse :: [a] -> [a]
1004    {-# SPECIALISE reverse :: [Int] -> [Int] #-}
1005
1006 But SPECIALISE INLINE *can* make sense for GADTS:
1007    data Arr e where
1008      ArrInt :: !Int -> ByteArray# -> Arr Int
1009      ArrPair :: !Int -> Arr e1 -> Arr e2 -> Arr (e1, e2)
1010
1011    (!:) :: Arr e -> Int -> e
1012    {-# SPECIALISE INLINE (!:) :: Arr Int -> Int -> Int #-}  
1013    {-# SPECIALISE INLINE (!:) :: Arr (a, b) -> Int -> (a, b) #-}
1014    (ArrInt _ ba)     !: (I# i) = I# (indexIntArray# ba i)
1015    (ArrPair _ a1 a2) !: i      = (a1 !: i, a2 !: i)
1016
1017 When (!:) is specialised it becomes non-recursive, and can usefully
1018 be inlined.  Scary!  So we only warn for SPECIALISE *without* INLINE
1019 for a non-overloaded function.
1020
1021 %************************************************************************
1022 %*                                                                      *
1023 \subsection{tcMonoBind}
1024 %*                                                                      *
1025 %************************************************************************
1026
1027 @tcMonoBinds@ deals with a perhaps-recursive group of HsBinds.
1028 The signatures have been dealt with already.
1029
1030 Note [Pattern bindings]
1031 ~~~~~~~~~~~~~~~~~~~~~~~
1032 The rule for typing pattern bindings is this:
1033
1034     ..sigs..
1035     p = e
1036
1037 where 'p' binds v1..vn, and 'e' may mention v1..vn, 
1038 typechecks exactly like
1039
1040     ..sigs..
1041     x = e       -- Inferred type
1042     v1 = case x of p -> v1
1043     ..
1044     vn = case x of p -> vn
1045
1046 Note that  
1047     (f :: forall a. a -> a) = id
1048 should not typecheck because
1049        case id of { (f :: forall a. a->a) -> f }
1050 will not typecheck.
1051
1052 \begin{code}
1053 tcMonoBinds :: RecFlag  -- Whether the binding is recursive for typechecking purposes
1054                         -- i.e. the binders are mentioned in their RHSs, and
1055                         --      we are not rescued by a type signature
1056             -> TcSigFun -> LetBndrSpec 
1057             -> [LHsBind Name]
1058             -> TcM (LHsBinds TcId, [MonoBindInfo])
1059
1060 tcMonoBinds is_rec sig_fn no_gen
1061            [ L b_loc (FunBind { fun_id = L nm_loc name, fun_infix = inf,
1062                                 fun_matches = matches, bind_fvs = fvs })]
1063                              -- Single function binding, 
1064   | NonRecursive <- is_rec   -- ...binder isn't mentioned in RHS
1065   , Nothing <- sig_fn name   -- ...with no type signature
1066   =     -- In this very special case we infer the type of the
1067         -- right hand side first (it may have a higher-rank type)
1068         -- and *then* make the monomorphic Id for the LHS
1069         -- e.g.         f = \(x::forall a. a->a) -> <body>
1070         --      We want to infer a higher-rank type for f
1071     setSrcSpan b_loc    $
1072     do  { rhs_ty  <- newFlexiTyVarTy openTypeKind
1073         ; mono_id <- newNoSigLetBndr no_gen name rhs_ty
1074         ; (co_fn, matches') <- tcExtendIdBndrs [TcIdBndr mono_id NotTopLevel] $
1075                                  -- We extend the error context even for a non-recursive 
1076                                  -- function so that in type error messages we show the 
1077                                  -- type of the thing whose rhs we are type checking
1078                                tcMatchesFun name inf matches rhs_ty
1079
1080         ; return (unitBag $ L b_loc (FunBind { fun_id = L nm_loc mono_id, fun_infix = inf,
1081                                                fun_matches = matches', bind_fvs = fvs,
1082                                                fun_co_fn = co_fn, fun_tick = Nothing }),
1083                   [(name, Nothing, mono_id)]) }
1084
1085 tcMonoBinds _ sig_fn no_gen binds
1086   = do  { tc_binds <- mapM (wrapLocM (tcLhs sig_fn no_gen)) binds
1087
1088         -- Bring the monomorphic Ids, into scope for the RHSs
1089         ; let mono_info  = getMonoBindInfo tc_binds
1090               rhs_id_env = [(name,mono_id) | (name, Nothing, mono_id) <- mono_info]
1091                     -- A monomorphic binding for each term variable that lacks 
1092                     -- a type sig.  (Ones with a sig are already in scope.)
1093
1094         ; traceTc "tcMonoBinds" $ vcat [ ppr n <+> ppr id <+> ppr (idType id) 
1095                                        | (n,id) <- rhs_id_env]
1096         ; binds' <- tcExtendIdEnv2 rhs_id_env $ 
1097                     mapM (wrapLocM tcRhs) tc_binds
1098         ; return (listToBag binds', mono_info) }
1099
1100 ------------------------
1101 -- tcLhs typechecks the LHS of the bindings, to construct the environment in which
1102 -- we typecheck the RHSs.  Basically what we are doing is this: for each binder:
1103 --      if there's a signature for it, use the instantiated signature type
1104 --      otherwise invent a type variable
1105 -- You see that quite directly in the FunBind case.
1106 -- 
1107 -- But there's a complication for pattern bindings:
1108 --      data T = MkT (forall a. a->a)
1109 --      MkT f = e
1110 -- Here we can guess a type variable for the entire LHS (which will be refined to T)
1111 -- but we want to get (f::forall a. a->a) as the RHS environment.
1112 -- The simplest way to do this is to typecheck the pattern, and then look up the
1113 -- bound mono-ids.  Then we want to retain the typechecked pattern to avoid re-doing
1114 -- it; hence the TcMonoBind data type in which the LHS is done but the RHS isn't
1115
1116 data TcMonoBind         -- Half completed; LHS done, RHS not done
1117   = TcFunBind  MonoBindInfo  SrcSpan Bool (MatchGroup Name (LHsExpr Name)) 
1118   | TcPatBind [MonoBindInfo] (LPat TcId) (GRHSs Name (LHsExpr Name)) TcSigmaType
1119
1120 type MonoBindInfo = (Name, Maybe TcSigInfo, TcId)
1121         -- Type signature (if any), and
1122         -- the monomorphic bound things
1123
1124 tcLhs :: TcSigFun -> LetBndrSpec -> HsBind Name -> TcM TcMonoBind
1125 tcLhs sig_fn no_gen (FunBind { fun_id = L nm_loc name, fun_infix = inf, fun_matches = matches })
1126   | Just sig <- sig_fn name
1127   = ASSERT2( case no_gen of { LetLclBndr -> True; LetGblBndr {} -> False }
1128            , ppr name )  -- { f :: ty; f x = e } is always done via CheckGen
1129                          -- which gives rise to LetLclBndr.  It wouldn't make
1130                          -- sense to have a *polymorphic* function Id at this point
1131     do  { mono_name <- newLocalName name
1132         ; let mono_id = mkLocalId mono_name (sig_tau sig)
1133         ; return (TcFunBind (name, Just sig, mono_id) nm_loc inf matches) }
1134   | otherwise
1135   = do  { mono_ty <- newFlexiTyVarTy openTypeKind
1136         ; mono_id <- newNoSigLetBndr no_gen name mono_ty
1137         ; return (TcFunBind (name, Nothing, mono_id) nm_loc inf matches) }
1138
1139 tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss })
1140   = do  { let tc_pat exp_ty = tcLetPat sig_fn no_gen pat exp_ty $
1141                               mapM lookup_info (collectPatBinders pat)
1142
1143                 -- After typechecking the pattern, look up the binder
1144                 -- names, which the pattern has brought into scope.
1145               lookup_info :: Name -> TcM MonoBindInfo
1146               lookup_info name = do { mono_id <- tcLookupId name
1147                                     ; return (name, sig_fn name, mono_id) }
1148
1149         ; ((pat', infos), pat_ty) <- addErrCtxt (patMonoBindsCtxt pat grhss) $
1150                                      tcInfer tc_pat
1151
1152         ; return (TcPatBind infos pat' grhss pat_ty) }
1153
1154 tcLhs _ _ other_bind = pprPanic "tcLhs" (ppr other_bind)
1155         -- AbsBind, VarBind impossible
1156
1157 -------------------
1158 tcRhs :: TcMonoBind -> TcM (HsBind TcId)
1159 -- When we are doing pattern bindings, or multiple function bindings at a time
1160 -- we *don't* bring any scoped type variables into scope
1161 -- Wny not?  They are not completely rigid.
1162 -- That's why we have the special case for a single FunBind in tcMonoBinds
1163 tcRhs (TcFunBind (_,_,mono_id) loc inf matches)
1164   = tcExtendIdBndrs [TcIdBndr mono_id NotTopLevel] $
1165             -- NotTopLevel: it's a monomorphic binding
1166     do  { traceTc "tcRhs: fun bind" (ppr mono_id $$ ppr (idType mono_id))
1167         ; (co_fn, matches') <- tcMatchesFun (idName mono_id) inf 
1168                                             matches (idType mono_id)
1169         ; return (FunBind { fun_id = L loc mono_id, fun_infix = inf
1170                           , fun_matches = matches'
1171                           , fun_co_fn = co_fn 
1172                           , bind_fvs = placeHolderNamesTc
1173                           , fun_tick = Nothing }) }
1174
1175 tcRhs (TcPatBind infos pat' grhss pat_ty)
1176   = tcExtendIdBndrs [ TcIdBndr mono_id NotTopLevel | (_,_,mono_id) <- infos ] $
1177             -- NotTopLevel: it's a monomorphic binding
1178     do  { traceTc "tcRhs: pat bind" (ppr pat' $$ ppr pat_ty)
1179         ; grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $
1180                     tcGRHSsPat grhss pat_ty
1181         ; return (PatBind { pat_lhs = pat', pat_rhs = grhss', pat_rhs_ty = pat_ty 
1182                           , bind_fvs = placeHolderNamesTc
1183                           , pat_ticks = (Nothing,[]) }) }
1184
1185
1186 ---------------------
1187 getMonoBindInfo :: [Located TcMonoBind] -> [MonoBindInfo]
1188 getMonoBindInfo tc_binds
1189   = foldr (get_info . unLoc) [] tc_binds
1190   where
1191     get_info (TcFunBind info _ _ _)  rest = info : rest
1192     get_info (TcPatBind infos _ _ _) rest = infos ++ rest
1193 \end{code}
1194
1195
1196
1197 %************************************************************************
1198 %*                                                                      *
1199                 Signatures
1200 %*                                                                      *
1201 %************************************************************************
1202
1203 Type signatures are tricky.  See Note [Signature skolems] in TcType
1204
1205 @tcSigs@ checks the signatures for validity, and returns a list of
1206 {\em freshly-instantiated} signatures.  That is, the types are already
1207 split up, and have fresh type variables installed.  All non-type-signature
1208 "RenamedSigs" are ignored.
1209
1210 The @TcSigInfo@ contains @TcTypes@ because they are unified with
1211 the variable's type, and after that checked to see whether they've
1212 been instantiated.
1213
1214 Note [Scoped tyvars]
1215 ~~~~~~~~~~~~~~~~~~~~
1216 The -XScopedTypeVariables flag brings lexically-scoped type variables
1217 into scope for any explicitly forall-quantified type variables:
1218         f :: forall a. a -> a
1219         f x = e
1220 Then 'a' is in scope inside 'e'.
1221
1222 However, we do *not* support this 
1223   - For pattern bindings e.g
1224         f :: forall a. a->a
1225         (f,g) = e
1226
1227 Note [Signature skolems]
1228 ~~~~~~~~~~~~~~~~~~~~~~~~
1229 When instantiating a type signature, we do so with either skolems or
1230 SigTv meta-type variables depending on the use_skols boolean.  This
1231 variable is set True when we are typechecking a single function
1232 binding; and False for pattern bindings and a group of several
1233 function bindings.
1234
1235 Reason: in the latter cases, the "skolems" can be unified together, 
1236         so they aren't properly rigid in the type-refinement sense.
1237 NB: unless we are doing H98, each function with a sig will be done
1238     separately, even if it's mutually recursive, so use_skols will be True
1239
1240
1241 Note [Only scoped tyvars are in the TyVarEnv]
1242 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1243 We are careful to keep only the *lexically scoped* type variables in
1244 the type environment.  Why?  After all, the renamer has ensured
1245 that only legal occurrences occur, so we could put all type variables
1246 into the type env.
1247
1248 But we want to check that two distinct lexically scoped type variables
1249 do not map to the same internal type variable.  So we need to know which
1250 the lexically-scoped ones are... and at the moment we do that by putting
1251 only the lexically scoped ones into the environment.
1252
1253 Note [Instantiate sig with fresh variables]
1254 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1255 It's vital to instantiate a type signature with fresh variables.
1256 For example:
1257       type T = forall a. [a] -> [a]
1258       f :: T; 
1259       f = g where { g :: T; g = <rhs> }
1260
1261  We must not use the same 'a' from the defn of T at both places!!
1262 (Instantiation is only necessary because of type synonyms.  Otherwise,
1263 it's all cool; each signature has distinct type variables from the renamer.)
1264
1265 Note [Fail eagerly on bad signatures]
1266 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1267 If a type signaure is wrong, fail immediately:
1268
1269  * the type sigs may bind type variables, so proceeding without them
1270    can lead to a cascade of errors
1271
1272  * the type signature might be ambiguous, in which case checking
1273    the code against the signature will give a very similar error
1274    to the ambiguity error.
1275
1276 ToDo: this means we fall over if any type sig
1277 is wrong (eg at the top level of the module), 
1278 which is over-conservative
1279
1280 \begin{code}
1281 tcTySigs :: [LSig Name] -> TcM ([TcId], TcSigFun)
1282 tcTySigs hs_sigs
1283   = checkNoErrs $   -- See Note [Fail eagerly on bad signatures]
1284     do { ty_sigs_s<- mapAndRecoverM tcTySig hs_sigs
1285        ; let ty_sigs = concat ty_sigs_s
1286              env = mkNameEnv [(idName (sig_id sig), sig) | sig <- ty_sigs]
1287        ; return (map sig_id ty_sigs, lookupNameEnv env) }
1288
1289 tcTySig :: LSig Name -> TcM [TcSigInfo]
1290 tcTySig (L loc (IdSig id))
1291   = do { sig <- instTcTySigFromId loc id
1292        ; return [sig] }
1293 tcTySig (L loc (TypeSig names@(L _ name1 : _) hs_ty))
1294   = setSrcSpan loc $ 
1295     do { sigma_ty <- tcHsSigType (FunSigCtxt name1) hs_ty
1296        ; mapM (instTcTySig hs_ty sigma_ty) (map unLoc names) }
1297 tcTySig _ = return []
1298
1299 instTcTySigFromId :: SrcSpan -> Id -> TcM TcSigInfo
1300 instTcTySigFromId loc id
1301   = do { (tvs, theta, tau) <- tcInstType (tcInstSigTyVarsLoc loc)
1302                                          (idType id)
1303        ; return (TcSigInfo { sig_id = id, sig_loc = loc
1304                            , sig_tvs = [(Nothing, tv) | tv <- tvs]
1305                            , sig_theta = theta, sig_tau = tau }) }
1306   where
1307     -- Hack: in an instance decl we use the selector id as
1308     -- the template; but we do *not* want the SrcSpan on the Name of
1309     -- those type variables to refer to the class decl, rather to
1310     -- the instance decl
1311
1312 instTcTySig :: LHsType Name -> TcType    -- HsType and corresponding TcType
1313             -> Name -> TcM TcSigInfo
1314 instTcTySig hs_ty@(L loc _) sigma_ty name
1315   = do { (inst_tvs, theta, tau) <- tcInstType tcInstSigTyVars sigma_ty
1316        ; return (TcSigInfo { sig_id = mkLocalId name sigma_ty
1317                            , sig_loc = loc
1318                            , sig_tvs = findScopedTyVars hs_ty sigma_ty inst_tvs
1319                            , sig_theta = theta, sig_tau = tau }) }
1320
1321 -------------------------------
1322 data GeneralisationPlan
1323   = NoGen               -- No generalisation, no AbsBinds
1324
1325   | InferGen            -- Implicit generalisation; there is an AbsBinds
1326        Bool             --   True <=> apply the MR; generalise only unconstrained type vars
1327        Bool             --   True <=> bindings mention only variables with closed types
1328                         --            See Note [Bindings with closed types] in TcRnTypes
1329
1330   | CheckGen (LHsBind Name) TcSigInfo
1331                         -- One binding with a signature
1332                         -- Explicit generalisation; there is an AbsBinds
1333
1334 -- A consequence of the no-AbsBinds choice (NoGen) is that there is
1335 -- no "polymorphic Id" and "monmomorphic Id"; there is just the one
1336
1337 instance Outputable GeneralisationPlan where
1338   ppr NoGen          = ptext (sLit "NoGen")
1339   ppr (InferGen b c) = ptext (sLit "InferGen") <+> ppr b <+> ppr c
1340   ppr (CheckGen _ s) = ptext (sLit "CheckGen") <+> ppr s
1341
1342 decideGeneralisationPlan
1343    :: DynFlags -> TcTypeEnv -> [Name]
1344    -> [LHsBind Name] -> TcSigFun -> GeneralisationPlan
1345 decideGeneralisationPlan dflags type_env bndr_names lbinds sig_fn
1346   | strict_pat_binds                                 = NoGen
1347   | Just (lbind, sig) <- one_funbind_with_sig lbinds = CheckGen lbind sig
1348   | mono_local_binds                                 = NoGen
1349   | otherwise                                        = InferGen mono_restriction closed_flag
1350
1351   where
1352     bndr_set = mkNameSet bndr_names
1353     binds = map unLoc lbinds
1354
1355     strict_pat_binds = any isStrictHsBind binds
1356        -- Strict patterns (top level bang or unboxed tuple) must not
1357        -- be polymorphic, because we are going to force them
1358        -- See Trac #4498, #8762
1359
1360     mono_restriction  = xopt Opt_MonomorphismRestriction dflags
1361                      && any restricted binds
1362
1363     is_closed_ns :: NameSet -> Bool -> Bool
1364     is_closed_ns ns b = foldNameSet ((&&) . is_closed_id) b ns
1365         -- ns are the Names referred to from the RHS of this bind
1366
1367     is_closed_id :: Name -> Bool
1368     -- See Note [Bindings with closed types] in TcRnTypes
1369     is_closed_id name
1370       | name `elemNameSet` bndr_set
1371       = True              -- Ignore binders in this groups, of course
1372       | Just thing <- lookupNameEnv type_env name
1373       = case thing of
1374           ATcId { tct_closed = cl } -> isTopLevel cl  -- This is the key line
1375           ATyVar {}                 -> False          -- In-scope type variables
1376           AGlobal {}                -> True           --    are not closed!
1377           _                         -> pprPanic "is_closed_id" (ppr name)
1378       | otherwise
1379       = WARN( isInternalName name, ppr name ) True
1380         -- The free-var set for a top level binding mentions
1381         -- imported things too, so that we can report unused imports
1382         -- These won't be in the local type env.
1383         -- Ditto class method etc from the current module
1384
1385     closed_flag = foldr (is_closed_ns . bind_fvs) True binds
1386
1387     mono_local_binds = xopt Opt_MonoLocalBinds dflags
1388                     && not closed_flag
1389
1390     no_sig n = isNothing (sig_fn n)
1391
1392     -- With OutsideIn, all nested bindings are monomorphic
1393     -- except a single function binding with a signature
1394     one_funbind_with_sig [lbind@(L _ (FunBind { fun_id = v }))]
1395       = case sig_fn (unLoc v) of
1396         Nothing -> Nothing
1397         Just sig -> Just (lbind, sig)
1398     one_funbind_with_sig _
1399       = Nothing
1400
1401     -- The Haskell 98 monomorphism resetriction
1402     restricted (PatBind {})                              = True
1403     restricted (VarBind { var_id = v })                  = no_sig v
1404     restricted (FunBind { fun_id = v, fun_matches = m }) = restricted_match m
1405                                                            && no_sig (unLoc v)
1406     restricted (PatSynBind {}) = panic "isRestrictedGroup/unrestricted PatSynBind"
1407     restricted (AbsBinds {}) = panic "isRestrictedGroup/unrestricted AbsBinds"
1408
1409     restricted_match (MG { mg_alts = L _ (Match [] _ _) : _ }) = True
1410     restricted_match _                                         = False
1411         -- No args => like a pattern binding
1412         -- Some args => a function binding
1413
1414 -------------------
1415 checkStrictBinds :: TopLevelFlag -> RecFlag
1416                  -> [LHsBind Name]
1417                  -> LHsBinds TcId -> [Id]
1418                  -> TcM ()
1419 -- Check that non-overloaded unlifted bindings are
1420 --      a) non-recursive,
1421 --      b) not top level,
1422 --      c) not a multiple-binding group (more or less implied by (a))
1423
1424 checkStrictBinds top_lvl rec_group orig_binds tc_binds poly_ids
1425   | unlifted_bndrs || any_strict_pat   -- This binding group must be matched strictly
1426   = do  { checkTc (isNotTopLevel top_lvl)
1427                   (strictBindErr "Top-level" unlifted_bndrs orig_binds)
1428         ; checkTc (isNonRec rec_group)
1429                   (strictBindErr "Recursive" unlifted_bndrs orig_binds)
1430
1431         ; checkTc (all is_monomorphic (bagToList tc_binds))
1432                   (polyBindErr orig_binds)
1433             -- data Ptr a = Ptr Addr#
1434             -- f x = let p@(Ptr y) = ... in ...
1435             -- Here the binding for 'p' is polymorphic, but does
1436             -- not mix with an unlifted binding for 'y'.  You should
1437             -- use a bang pattern.  Trac #6078.
1438
1439         ; checkTc (isSingleton orig_binds)
1440                   (strictBindErr "Multiple" unlifted_bndrs orig_binds)
1441
1442         -- Complain about a binding that looks lazy
1443         --    e.g.    let I# y = x in ...
1444         -- Remember, in checkStrictBinds we are going to do strict
1445         -- matching, so (for software engineering reasons) we insist
1446         -- that the strictness is manifest on each binding
1447         -- However, lone (unboxed) variables are ok
1448         ; checkTc (not any_pat_looks_lazy)
1449                   (unliftedMustBeBang orig_binds) }
1450   | otherwise
1451   = traceTc "csb2" (ppr poly_ids) >>
1452     return ()
1453   where
1454     unlifted_bndrs     = any is_unlifted poly_ids
1455     any_strict_pat     = any (isStrictHsBind   . unLoc) orig_binds
1456     any_pat_looks_lazy = any (looksLazyPatBind . unLoc) orig_binds
1457
1458     is_unlifted id = case tcSplitSigmaTy (idType id) of
1459                        (_, _, rho) -> isUnLiftedType rho
1460           -- For the is_unlifted check, we need to look inside polymorphism
1461           -- and overloading.  E.g.  x = (# 1, True #)
1462           -- would get type forall a. Num a => (# a, Bool #)
1463           -- and we want to reject that.  See Trac #9140
1464
1465     is_monomorphic (L _ (AbsBinds { abs_tvs = tvs, abs_ev_vars = evs }))
1466                      = null tvs && null evs
1467     is_monomorphic _ = True
1468
1469 unliftedMustBeBang :: [LHsBind Name] -> SDoc
1470 unliftedMustBeBang binds
1471   = hang (text "Pattern bindings containing unlifted types should use an outermost bang pattern:")
1472        2 (vcat (map ppr binds))
1473
1474 polyBindErr :: [LHsBind Name] -> SDoc
1475 polyBindErr binds
1476   = hang (ptext (sLit "You can't mix polymorphic and unlifted bindings"))
1477        2 (vcat [vcat (map ppr binds), 
1478                 ptext (sLit "Probable fix: use a bang pattern")])
1479
1480 strictBindErr :: String -> Bool -> [LHsBind Name] -> SDoc
1481 strictBindErr flavour unlifted_bndrs binds
1482   = hang (text flavour <+> msg <+> ptext (sLit "aren't allowed:")) 
1483        2 (vcat (map ppr binds))
1484   where
1485     msg | unlifted_bndrs = ptext (sLit "bindings for unlifted types")
1486         | otherwise      = ptext (sLit "bang-pattern or unboxed-tuple bindings")
1487 \end{code}
1488
1489 Note [Binding scoped type variables]
1490 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1491
1492 %************************************************************************
1493 %*                                                                      *
1494 \subsection[TcBinds-errors]{Error contexts and messages}
1495 %*                                                                      *
1496 %************************************************************************
1497
1498
1499 \begin{code}
1500 -- This one is called on LHS, when pat and grhss are both Name 
1501 -- and on RHS, when pat is TcId and grhss is still Name
1502 patMonoBindsCtxt :: (OutputableBndr id, Outputable body) => LPat id -> GRHSs Name body -> SDoc
1503 patMonoBindsCtxt pat grhss
1504   = hang (ptext (sLit "In a pattern binding:")) 2 (pprPatBind pat grhss)
1505 \end{code}