d7af47cb2a6a47d2441461af16fe4d0fc539445f
[ghc.git] / compiler / typecheck / TcExpr.lhs
1 c%
2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 %
5 \section[TcExpr]{Typecheck an expression}
6
7 \begin{code}
8 {-# LANGUAGE CPP #-}
9
10 module TcExpr ( tcPolyExpr, tcPolyExprNC, tcMonoExpr, tcMonoExprNC,
11                 tcInferRho, tcInferRhoNC,
12                 tcSyntaxOp, tcCheckId,
13                 addExprErrCtxt) where
14
15 #include "HsVersions.h"
16
17 import {-# SOURCE #-}   TcSplice( tcSpliceExpr, tcTypedBracket, tcUntypedBracket )
18 #ifdef GHCI
19 import DsMeta( liftStringName, liftName )
20 #endif
21
22 import HsSyn
23 import TcHsSyn
24 import TcRnMonad
25 import TcUnify
26 import BasicTypes
27 import Inst
28 import TcBinds
29 import FamInst          ( tcGetFamInstEnvs, tcLookupDataFamInst )
30 import TcEnv
31 import TcArrows
32 import TcMatches
33 import TcHsType
34 import TcPatSyn( tcPatSynBuilderOcc )
35 import TcPat
36 import TcMType
37 import TcType
38 import DsMonad hiding (Splice)
39 import Id
40 import ConLike
41 import DataCon
42 import RdrName
43 import Name
44 import TyCon
45 import Type
46 import TcEvidence
47 import Var
48 import VarSet
49 import VarEnv
50 import TysWiredIn
51 import TysPrim( intPrimTy, addrPrimTy )
52 import PrimOp( tagToEnumKey )
53 import PrelNames
54 import DynFlags
55 import SrcLoc
56 import Util
57 import ListSetOps
58 import Maybes
59 import ErrUtils
60 import Outputable
61 import FastString
62 import Control.Monad
63 import Class(classTyCon)
64 import Data.Function
65 import Data.List
66 import qualified Data.Set as Set
67 \end{code}
68
69 %************************************************************************
70 %*                                                                      *
71 \subsection{Main wrappers}
72 %*                                                                      *
73 %************************************************************************
74
75 \begin{code}
76 tcPolyExpr, tcPolyExprNC
77          :: LHsExpr Name        -- Expression to type check
78          -> TcSigmaType         -- Expected type (could be a polytype)
79          -> TcM (LHsExpr TcId)  -- Generalised expr with expected type
80
81 -- tcPolyExpr is a convenient place (frequent but not too frequent)
82 -- place to add context information.
83 -- The NC version does not do so, usually because the caller wants
84 -- to do so himself.
85
86 tcPolyExpr expr res_ty
87   = addExprErrCtxt expr $
88     do { traceTc "tcPolyExpr" (ppr res_ty); tcPolyExprNC expr res_ty }
89
90 tcPolyExprNC expr res_ty
91   = do { traceTc "tcPolyExprNC" (ppr res_ty)
92        ; (gen_fn, expr') <- tcGen GenSigCtxt res_ty $ \ _ rho ->
93                             tcMonoExprNC expr rho
94        ; return (mkLHsWrap gen_fn expr') }
95
96 ---------------
97 tcMonoExpr, tcMonoExprNC
98     :: LHsExpr Name      -- Expression to type check
99     -> TcRhoType         -- Expected type (could be a type variable)
100                          -- Definitely no foralls at the top
101     -> TcM (LHsExpr TcId)
102
103 tcMonoExpr expr res_ty
104   = addErrCtxt (exprCtxt expr) $
105     tcMonoExprNC expr res_ty
106
107 tcMonoExprNC (L loc expr) res_ty
108   = ASSERT( not (isSigmaTy res_ty) )
109     setSrcSpan loc $
110     do  { expr' <- tcExpr expr res_ty
111         ; return (L loc expr') }
112
113 ---------------
114 tcInferRho, tcInferRhoNC :: LHsExpr Name -> TcM (LHsExpr TcId, TcRhoType)
115 -- Infer a *rho*-type.  This is, in effect, a special case
116 -- for ids and partial applications, so that if
117 --     f :: Int -> (forall a. a -> a) -> Int
118 -- then we can infer
119 --     f 3 :: (forall a. a -> a) -> Int
120 -- And that in turn is useful
121 --  (a) for the function part of any application (see tcApp)
122 --  (b) for the special rule for '$'
123 tcInferRho expr = addErrCtxt (exprCtxt expr) (tcInferRhoNC expr)
124
125 tcInferRhoNC (L loc expr)
126   = setSrcSpan loc $
127     do { (expr', rho) <- tcInfer (tcExpr expr)
128        ; return (L loc expr', rho) }
129
130 tcHole :: OccName -> TcRhoType -> TcM (HsExpr TcId)
131 tcHole occ res_ty
132  = do { ty <- newFlexiTyVarTy liftedTypeKind
133       ; name <- newSysName occ
134       ; let ev = mkLocalId name ty
135       ; loc <- getCtLoc HoleOrigin
136       ; let can = CHoleCan { cc_ev = CtWanted ty ev loc, cc_occ = occ }
137       ; emitInsoluble can
138       ; tcWrapResult (HsVar ev) ty res_ty }
139 \end{code}
140
141
142 %************************************************************************
143 %*                                                                      *
144         tcExpr: the main expression typechecker
145 %*                                                                      *
146 %************************************************************************
147
148 \begin{code}
149 tcExpr :: HsExpr Name -> TcRhoType -> TcM (HsExpr TcId)
150 tcExpr e res_ty | debugIsOn && isSigmaTy res_ty     -- Sanity check
151                 = pprPanic "tcExpr: sigma" (ppr res_ty $$ ppr e)
152
153 tcExpr (HsVar name)  res_ty = tcCheckId name res_ty
154
155 tcExpr (HsApp e1 e2) res_ty = tcApp e1 [e2] res_ty
156
157 tcExpr (HsLit lit)   res_ty = do { let lit_ty = hsLitType lit
158                                  ; tcWrapResult (HsLit lit) lit_ty res_ty }
159
160 tcExpr (HsPar expr)  res_ty = do { expr' <- tcMonoExprNC expr res_ty
161                                  ; return (HsPar expr') }
162
163 tcExpr (HsSCC lbl expr) res_ty
164   = do { expr' <- tcMonoExpr expr res_ty
165        ; return (HsSCC lbl expr') }
166
167 tcExpr (HsTickPragma info expr) res_ty
168   = do { expr' <- tcMonoExpr expr res_ty
169        ; return (HsTickPragma info expr') }
170
171 tcExpr (HsCoreAnn lbl expr) res_ty
172   = do  { expr' <- tcMonoExpr expr res_ty
173         ; return (HsCoreAnn lbl expr') }
174
175 tcExpr (HsOverLit lit) res_ty
176   = do  { lit' <- newOverloadedLit (LiteralOrigin lit) lit res_ty
177         ; return (HsOverLit lit') }
178
179 tcExpr (NegApp expr neg_expr) res_ty
180   = do  { neg_expr' <- tcSyntaxOp NegateOrigin neg_expr
181                                   (mkFunTy res_ty res_ty)
182         ; expr' <- tcMonoExpr expr res_ty
183         ; return (NegApp expr' neg_expr') }
184
185 tcExpr (HsIPVar x) res_ty
186   = do { let origin = IPOccOrigin x
187        ; ipClass <- tcLookupClass ipClassName
188            {- Implicit parameters must have a *tau-type* not a.
189               type scheme.  We enforce this by creating a fresh
190               type variable as its type.  (Because res_ty may not
191               be a tau-type.) -}
192        ; ip_ty <- newFlexiTyVarTy openTypeKind
193        ; let ip_name = mkStrLitTy (hsIPNameFS x)
194        ; ip_var <- emitWanted origin (mkClassPred ipClass [ip_name, ip_ty])
195        ; tcWrapResult (fromDict ipClass ip_name ip_ty (HsVar ip_var)) ip_ty res_ty }
196   where
197   -- Coerces a dictionary for `IP "x" t` into `t`.
198   fromDict ipClass x ty =
199     case unwrapNewTyCon_maybe (classTyCon ipClass) of
200       Just (_,_,ax) -> HsWrap $ mkWpCast $ mkTcUnbranchedAxInstCo Representational ax [x,ty]
201       Nothing       -> panic "The dictionary for `IP` is not a newtype?"
202
203 tcExpr (HsLam match) res_ty
204   = do  { (co_fn, match') <- tcMatchLambda match res_ty
205         ; return (mkHsWrap co_fn (HsLam match')) }
206
207 tcExpr e@(HsLamCase _ matches) res_ty
208   = do  { (co_fn, [arg_ty], body_ty) <- matchExpectedFunTys msg 1 res_ty
209         ; matches' <- tcMatchesCase match_ctxt arg_ty matches body_ty
210         ; return $ mkHsWrapCo co_fn $ HsLamCase arg_ty matches' }
211   where msg = sep [ ptext (sLit "The function") <+> quotes (ppr e)
212                   , ptext (sLit "requires")]
213         match_ctxt = MC { mc_what = CaseAlt, mc_body = tcBody }
214
215 tcExpr (ExprWithTySig expr sig_ty) res_ty
216  = do { sig_tc_ty <- tcHsSigType ExprSigCtxt sig_ty
217
218       ; (gen_fn, expr')
219             <- tcGen ExprSigCtxt sig_tc_ty $ \ skol_tvs res_ty ->
220
221                   -- Remember to extend the lexical type-variable environment
222                   -- See Note [More instantiated than scoped] in TcBinds
223                tcExtendTyVarEnv2 
224                   [(n,tv) | (Just n, tv) <- findScopedTyVars sig_ty sig_tc_ty skol_tvs] $
225
226                tcMonoExprNC expr res_ty
227
228       ; let inner_expr = ExprWithTySigOut (mkLHsWrap gen_fn expr') sig_ty
229
230       ; (inst_wrap, rho) <- deeplyInstantiate ExprSigOrigin sig_tc_ty
231       ; tcWrapResult (mkHsWrap inst_wrap inner_expr) rho res_ty }
232
233 tcExpr (HsType ty) _
234   = failWithTc (text "Can't handle type argument:" <+> ppr ty)
235         -- This is the syntax for type applications that I was planning
236         -- but there are difficulties (e.g. what order for type args)
237         -- so it's not enabled yet.
238         -- Can't eliminate it altogether from the parser, because the
239         -- same parser parses *patterns*.
240 tcExpr (HsUnboundVar v) res_ty
241   = tcHole (rdrNameOcc v) res_ty
242 \end{code}
243
244
245 %************************************************************************
246 %*                                                                      *
247                 Infix operators and sections
248 %*                                                                      *
249 %************************************************************************
250
251 Note [Left sections]
252 ~~~~~~~~~~~~~~~~~~~~
253 Left sections, like (4 *), are equivalent to
254         \ x -> (*) 4 x,
255 or, if PostfixOperators is enabled, just
256         (*) 4
257 With PostfixOperators we don't actually require the function to take
258 two arguments at all.  For example, (x `not`) means (not x); you get
259 postfix operators!  Not Haskell 98, but it's less work and kind of
260 useful.
261
262 Note [Typing rule for ($)]
263 ~~~~~~~~~~~~~~~~~~~~~~~~~~
264 People write
265    runST $ blah
266 so much, where
267    runST :: (forall s. ST s a) -> a
268 that I have finally given in and written a special type-checking
269 rule just for saturated appliations of ($).
270   * Infer the type of the first argument
271   * Decompose it; should be of form (arg2_ty -> res_ty),
272        where arg2_ty might be a polytype
273   * Use arg2_ty to typecheck arg2
274
275 Note [Typing rule for seq]
276 ~~~~~~~~~~~~~~~~~~~~~~~~~~
277 We want to allow
278        x `seq` (# p,q #)
279 which suggests this type for seq:
280    seq :: forall (a:*) (b:??). a -> b -> b,
281 with (b:??) meaning that be can be instantiated with an unboxed tuple.
282 But that's ill-kinded!  Function arguments can't be unboxed tuples.
283 And indeed, you could not expect to do this with a partially-applied
284 'seq'; it's only going to work when it's fully applied.  so it turns
285 into
286     case x of _ -> (# p,q #)
287
288 For a while I slid by by giving 'seq' an ill-kinded type, but then
289 the simplifier eta-reduced an application of seq and Lint blew up
290 with a kind error.  It seems more uniform to treat 'seq' as it it
291 was a language construct.
292
293 See Note [seqId magic] in MkId, and
294
295
296 \begin{code}
297 tcExpr (OpApp arg1 op fix arg2) res_ty
298   | (L loc (HsVar op_name)) <- op
299   , op_name `hasKey` seqIdKey           -- Note [Typing rule for seq]
300   = do { arg1_ty <- newFlexiTyVarTy liftedTypeKind
301        ; let arg2_ty = res_ty
302        ; arg1' <- tcArg op (arg1, arg1_ty, 1)
303        ; arg2' <- tcArg op (arg2, arg2_ty, 2)
304        ; op_id <- tcLookupId op_name
305        ; let op' = L loc (HsWrap (mkWpTyApps [arg1_ty, arg2_ty]) (HsVar op_id))
306        ; return $ OpApp arg1' op' fix arg2' }
307
308   | (L loc (HsVar op_name)) <- op
309   , op_name `hasKey` dollarIdKey        -- Note [Typing rule for ($)]
310   = do { traceTc "Application rule" (ppr op)
311        ; (arg1', arg1_ty) <- tcInferRho arg1
312
313        ; let doc = ptext (sLit "The first argument of ($) takes")
314        ; (co_arg1, [arg2_ty], op_res_ty) <- matchExpectedFunTys doc 1 arg1_ty
315          -- arg1_ty = arg2_ty -> op_res_ty
316          -- And arg2_ty maybe polymorphic; that's the point
317
318        -- Make sure that the argument type has kind '*'
319        -- Eg we do not want to allow  (D#  $  4.0#)   Trac #5570
320        --    (which gives a seg fault)
321        -- We do this by unifying with a MetaTv; but of course
322        -- it must allow foralls in the type it unifies with (hence ReturnTv)!
323        --
324        -- The result type can have any kind (Trac #8739),
325        -- so we can just use res_ty
326
327        -- ($) :: forall (a:*) (b:Open). (a->b) -> a -> b
328        ; a_tv <- newReturnTyVar liftedTypeKind
329        ; let a_ty = mkTyVarTy a_tv
330
331        ; arg2' <- tcArg op (arg2, arg2_ty, 2)
332
333        ; co_a   <- unifyType arg2_ty   a_ty      -- arg2 ~ a
334        ; co_b   <- unifyType op_res_ty res_ty    -- op_res ~ res
335        ; op_id  <- tcLookupId op_name
336
337        ; let op' = L loc (HsWrap (mkWpTyApps [a_ty, res_ty]) (HsVar op_id))
338        ; return $
339          OpApp (mkLHsWrapCo (mkTcFunCo Nominal co_a co_b) $
340                 mkLHsWrapCo co_arg1 arg1')
341                op' fix
342                (mkLHsWrapCo co_a arg2') }
343
344   | otherwise
345   = do { traceTc "Non Application rule" (ppr op)
346        ; (op', op_ty) <- tcInferFun op
347        ; (co_fn, arg_tys, op_res_ty) <- unifyOpFunTysWrap op 2 op_ty
348        ; co_res <- unifyType op_res_ty res_ty
349        ; [arg1', arg2'] <- tcArgs op [arg1, arg2] arg_tys
350        ; return $ mkHsWrapCo co_res $
351          OpApp arg1' (mkLHsWrapCo co_fn op') fix arg2' }
352
353 -- Right sections, equivalent to \ x -> x `op` expr, or
354 --      \ x -> op x expr
355
356 tcExpr (SectionR op arg2) res_ty
357   = do { (op', op_ty) <- tcInferFun op
358        ; (co_fn, [arg1_ty, arg2_ty], op_res_ty) <- unifyOpFunTysWrap op 2 op_ty
359        ; co_res <- unifyType (mkFunTy arg1_ty op_res_ty) res_ty
360        ; arg2' <- tcArg op (arg2, arg2_ty, 2)
361        ; return $ mkHsWrapCo co_res $
362          SectionR (mkLHsWrapCo co_fn op') arg2' }
363
364 tcExpr (SectionL arg1 op) res_ty
365   = do { (op', op_ty) <- tcInferFun op
366        ; dflags <- getDynFlags      -- Note [Left sections]
367        ; let n_reqd_args | xopt Opt_PostfixOperators dflags = 1
368                          | otherwise                        = 2
369
370        ; (co_fn, (arg1_ty:arg_tys), op_res_ty) <- unifyOpFunTysWrap op n_reqd_args op_ty
371        ; co_res <- unifyType (mkFunTys arg_tys op_res_ty) res_ty
372        ; arg1' <- tcArg op (arg1, arg1_ty, 1)
373        ; return $ mkHsWrapCo co_res $
374          SectionL arg1' (mkLHsWrapCo co_fn op') }
375
376 tcExpr (ExplicitTuple tup_args boxity) res_ty
377   | all tupArgPresent tup_args
378   = do { let tup_tc = tupleTyCon (boxityNormalTupleSort boxity) (length tup_args)
379        ; (coi, arg_tys) <- matchExpectedTyConApp tup_tc res_ty
380        ; tup_args1 <- tcTupArgs tup_args arg_tys
381        ; return $ mkHsWrapCo coi (ExplicitTuple tup_args1 boxity) }
382
383   | otherwise
384   = -- The tup_args are a mixture of Present and Missing (for tuple sections)
385     do { let kind = case boxity of { Boxed   -> liftedTypeKind
386                                    ; Unboxed -> openTypeKind }
387              arity = length tup_args
388              tup_tc = tupleTyCon (boxityNormalTupleSort boxity) arity
389
390        ; arg_tys <- newFlexiTyVarTys (tyConArity tup_tc) kind
391        ; let actual_res_ty
392                = mkFunTys [ty | (ty, L _ (Missing _)) <- arg_tys `zip` tup_args]
393                           (mkTyConApp tup_tc arg_tys)
394
395        ; coi <- unifyType actual_res_ty res_ty
396
397        -- Handle tuple sections where
398        ; tup_args1 <- tcTupArgs tup_args arg_tys
399
400        ; return $ mkHsWrapCo coi (ExplicitTuple tup_args1 boxity) }
401
402 tcExpr (ExplicitList _ witness exprs) res_ty
403   = case witness of
404       Nothing   -> do  { (coi, elt_ty) <- matchExpectedListTy res_ty
405                        ; exprs' <- mapM (tc_elt elt_ty) exprs
406                        ; return $ mkHsWrapCo coi (ExplicitList elt_ty Nothing exprs') }
407
408       Just fln -> do  { list_ty <- newFlexiTyVarTy liftedTypeKind
409                      ; fln' <- tcSyntaxOp ListOrigin fln (mkFunTys [intTy, list_ty] res_ty)
410                      ; (coi, elt_ty) <- matchExpectedListTy list_ty
411                      ; exprs' <- mapM (tc_elt elt_ty) exprs
412                      ; return $ mkHsWrapCo coi (ExplicitList elt_ty (Just fln') exprs') }
413      where tc_elt elt_ty expr = tcPolyExpr expr elt_ty
414
415 tcExpr (ExplicitPArr _ exprs) res_ty    -- maybe empty
416   = do  { (coi, elt_ty) <- matchExpectedPArrTy res_ty
417         ; exprs' <- mapM (tc_elt elt_ty) exprs
418         ; return $ mkHsWrapCo coi (ExplicitPArr elt_ty exprs') }
419   where
420     tc_elt elt_ty expr = tcPolyExpr expr elt_ty
421 \end{code}
422
423 %************************************************************************
424 %*                                                                      *
425                 Let, case, if, do
426 %*                                                                      *
427 %************************************************************************
428
429 \begin{code}
430 tcExpr (HsLet binds expr) res_ty
431   = do  { (binds', expr') <- tcLocalBinds binds $
432                              tcMonoExpr expr res_ty
433         ; return (HsLet binds' expr') }
434
435 tcExpr (HsCase scrut matches) exp_ty
436   = do  {  -- We used to typecheck the case alternatives first.
437            -- The case patterns tend to give good type info to use
438            -- when typechecking the scrutinee.  For example
439            --   case (map f) of
440            --     (x:xs) -> ...
441            -- will report that map is applied to too few arguments
442            --
443            -- But now, in the GADT world, we need to typecheck the scrutinee
444            -- first, to get type info that may be refined in the case alternatives
445           (scrut', scrut_ty) <- tcInferRho scrut
446
447         ; traceTc "HsCase" (ppr scrut_ty)
448         ; matches' <- tcMatchesCase match_ctxt scrut_ty matches exp_ty
449         ; return (HsCase scrut' matches') }
450  where
451     match_ctxt = MC { mc_what = CaseAlt,
452                       mc_body = tcBody }
453
454 tcExpr (HsIf Nothing pred b1 b2) res_ty    -- Ordinary 'if'
455   = do { pred' <- tcMonoExpr pred boolTy
456        ; b1' <- tcMonoExpr b1 res_ty
457        ; b2' <- tcMonoExpr b2 res_ty
458        ; return (HsIf Nothing pred' b1' b2') }
459
460 tcExpr (HsIf (Just fun) pred b1 b2) res_ty   -- Note [Rebindable syntax for if]
461   = do { pred_ty <- newFlexiTyVarTy openTypeKind
462        ; b1_ty   <- newFlexiTyVarTy openTypeKind
463        ; b2_ty   <- newFlexiTyVarTy openTypeKind
464        ; let if_ty = mkFunTys [pred_ty, b1_ty, b2_ty] res_ty
465        ; fun'  <- tcSyntaxOp IfOrigin fun if_ty
466        ; pred' <- tcMonoExpr pred pred_ty
467        ; b1'   <- tcMonoExpr b1 b1_ty
468        ; b2'   <- tcMonoExpr b2 b2_ty
469        -- Fundamentally we are just typing (ifThenElse e1 e2 e3)
470        -- so maybe we should use the code for function applications
471        -- (which would allow ifThenElse to be higher rank).
472        -- But it's a little awkward, so I'm leaving it alone for now
473        -- and it maintains uniformity with other rebindable syntax
474        ; return (HsIf (Just fun') pred' b1' b2') }
475
476 tcExpr (HsMultiIf _ alts) res_ty
477   = do { alts' <- mapM (wrapLocM $ tcGRHS match_ctxt res_ty) alts
478        ; return $ HsMultiIf res_ty alts' }
479   where match_ctxt = MC { mc_what = IfAlt, mc_body = tcBody }
480
481 tcExpr (HsDo do_or_lc stmts _) res_ty
482   = tcDoStmts do_or_lc stmts res_ty
483
484 tcExpr (HsProc pat cmd) res_ty
485   = do  { (pat', cmd', coi) <- tcProc pat cmd res_ty
486         ; return $ mkHsWrapCo coi (HsProc pat' cmd') }
487 \end{code}
488
489 Note [Rebindable syntax for if]
490 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
491 The rebindable syntax for 'if' uses the most flexible possible type
492 for conditionals:
493   ifThenElse :: p -> b1 -> b2 -> res
494 to support expressions like this:
495
496  ifThenElse :: Maybe a -> (a -> b) -> b -> b
497  ifThenElse (Just a) f _ = f a
498  ifThenElse Nothing  _ e = e
499
500  example :: String
501  example = if Just 2
502               then \v -> show v
503               else "No value"
504
505
506 %************************************************************************
507 %*                                                                      *
508                 Record construction and update
509 %*                                                                      *
510 %************************************************************************
511
512 \begin{code}
513 tcExpr (RecordCon (L loc con_name) _ rbinds) res_ty
514   = do  { data_con <- tcLookupDataCon con_name
515
516         -- Check for missing fields
517         ; checkMissingFields data_con rbinds
518
519         ; (con_expr, con_tau) <- tcInferId con_name
520         ; let arity = dataConSourceArity data_con
521               (arg_tys, actual_res_ty) = tcSplitFunTysN con_tau arity
522               con_id = dataConWrapId data_con
523
524         ; co_res <- unifyType actual_res_ty res_ty
525         ; rbinds' <- tcRecordBinds data_con arg_tys rbinds
526         ; return $ mkHsWrapCo co_res $
527           RecordCon (L loc con_id) con_expr rbinds' }
528 \end{code}
529
530 Note [Type of a record update]
531 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
532 The main complication with RecordUpd is that we need to explicitly
533 handle the *non-updated* fields.  Consider:
534
535         data T a b c = MkT1 { fa :: a, fb :: (b,c) }
536                      | MkT2 { fa :: a, fb :: (b,c), fc :: c -> c }
537                      | MkT3 { fd :: a }
538
539         upd :: T a b c -> (b',c) -> T a b' c
540         upd t x = t { fb = x}
541
542 The result type should be (T a b' c)
543 not (T a b c),   because 'b' *is not* mentioned in a non-updated field
544 not (T a b' c'), because 'c' *is*     mentioned in a non-updated field
545 NB that it's not good enough to look at just one constructor; we must
546 look at them all; cf Trac #3219
547
548 After all, upd should be equivalent to:
549         upd t x = case t of
550                         MkT1 p q -> MkT1 p x
551                         MkT2 a b -> MkT2 p b
552                         MkT3 d   -> error ...
553
554 So we need to give a completely fresh type to the result record,
555 and then constrain it by the fields that are *not* updated ("p" above).
556 We call these the "fixed" type variables, and compute them in getFixedTyVars.
557
558 Note that because MkT3 doesn't contain all the fields being updated,
559 its RHS is simply an error, so it doesn't impose any type constraints.
560 Hence the use of 'relevant_cont'.
561
562 Note [Implicit type sharing]
563 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
564 We also take into account any "implicit" non-update fields.  For example
565         data T a b where { MkT { f::a } :: T a a; ... }
566 So the "real" type of MkT is: forall ab. (a~b) => a -> T a b
567
568 Then consider
569         upd t x = t { f=x }
570 We infer the type
571         upd :: T a b -> a -> T a b
572         upd (t::T a b) (x::a)
573            = case t of { MkT (co:a~b) (_:a) -> MkT co x }
574 We can't give it the more general type
575         upd :: T a b -> c -> T c b
576
577 Note [Criteria for update]
578 ~~~~~~~~~~~~~~~~~~~~~~~~~~
579 We want to allow update for existentials etc, provided the updated
580 field isn't part of the existential. For example, this should be ok.
581   data T a where { MkT { f1::a, f2::b->b } :: T a }
582   f :: T a -> b -> T b
583   f t b = t { f1=b }
584
585 The criterion we use is this:
586
587   The types of the updated fields
588   mention only the universally-quantified type variables
589   of the data constructor
590
591 NB: this is not (quite) the same as being a "naughty" record selector
592 (See Note [Naughty record selectors]) in TcTyClsDecls), at least
593 in the case of GADTs. Consider
594    data T a where { MkT :: { f :: a } :: T [a] }
595 Then f is not "naughty" because it has a well-typed record selector.
596 But we don't allow updates for 'f'.  (One could consider trying to
597 allow this, but it makes my head hurt.  Badly.  And no one has asked
598 for it.)
599
600 In principle one could go further, and allow
601   g :: T a -> T a
602   g t = t { f2 = \x -> x }
603 because the expression is polymorphic...but that seems a bridge too far.
604
605 Note [Data family example]
606 ~~~~~~~~~~~~~~~~~~~~~~~~~~
607     data instance T (a,b) = MkT { x::a, y::b }
608   --->
609     data :TP a b = MkT { a::a, y::b }
610     coTP a b :: T (a,b) ~ :TP a b
611
612 Suppose r :: T (t1,t2), e :: t3
613 Then  r { x=e } :: T (t3,t1)
614   --->
615       case r |> co1 of
616         MkT x y -> MkT e y |> co2
617       where co1 :: T (t1,t2) ~ :TP t1 t2
618             co2 :: :TP t3 t2 ~ T (t3,t2)
619 The wrapping with co2 is done by the constructor wrapper for MkT
620
621 Outgoing invariants
622 ~~~~~~~~~~~~~~~~~~~
623 In the outgoing (HsRecordUpd scrut binds cons in_inst_tys out_inst_tys):
624
625   * cons are the data constructors to be updated
626
627   * in_inst_tys, out_inst_tys have same length, and instantiate the
628         *representation* tycon of the data cons.  In Note [Data
629         family example], in_inst_tys = [t1,t2], out_inst_tys = [t3,t2]
630
631 \begin{code}
632 tcExpr (RecordUpd record_expr rbinds _ _ _) res_ty
633   = ASSERT( notNull upd_fld_names )
634     do  {
635         -- STEP 0
636         -- Check that the field names are really field names
637         ; sel_ids <- mapM tcLookupField upd_fld_names
638                         -- The renamer has already checked that
639                         -- selectors are all in scope
640         ; let bad_guys = [ setSrcSpan loc $ addErrTc (notSelector fld_name)
641                          | (fld, sel_id) <- rec_flds rbinds `zip` sel_ids,
642                            not (isRecordSelector sel_id),       -- Excludes class ops
643                            let L loc fld_name = hsRecFieldId (unLoc fld) ]
644         ; unless (null bad_guys) (sequence bad_guys >> failM)
645
646         -- STEP 1
647         -- Figure out the tycon and data cons from the first field name
648         ; let   -- It's OK to use the non-tc splitters here (for a selector)
649               sel_id : _  = sel_ids
650               (tycon, _)  = recordSelectorFieldLabel sel_id     -- We've failed already if
651               data_cons   = tyConDataCons tycon                 -- it's not a field label
652                 -- NB: for a data type family, the tycon is the instance tycon
653
654               relevant_cons   = filter is_relevant data_cons
655               is_relevant con = all (`elem` dataConFieldLabels con) upd_fld_names
656                 -- A constructor is only relevant to this process if
657                 -- it contains *all* the fields that are being updated
658                 -- Other ones will cause a runtime error if they occur
659
660                 -- Take apart a representative constructor
661               con1 = ASSERT( not (null relevant_cons) ) head relevant_cons
662               (con1_tvs, _, _, _, con1_arg_tys, _) = dataConFullSig con1
663               con1_flds = dataConFieldLabels con1
664               con1_res_ty = mkFamilyTyConApp tycon (mkTyVarTys con1_tvs)
665
666         -- Step 2
667         -- Check that at least one constructor has all the named fields
668         -- i.e. has an empty set of bad fields returned by badFields
669         ; checkTc (not (null relevant_cons)) (badFieldsUpd rbinds data_cons)
670
671         -- STEP 3    Note [Criteria for update]
672         -- Check that each updated field is polymorphic; that is, its type
673         -- mentions only the universally-quantified variables of the data con
674         ; let flds1_w_tys = zipEqual "tcExpr:RecConUpd" con1_flds con1_arg_tys
675               upd_flds1_w_tys = filter is_updated flds1_w_tys
676               is_updated (fld,_) = fld `elem` upd_fld_names
677
678               bad_upd_flds = filter bad_fld upd_flds1_w_tys
679               con1_tv_set = mkVarSet con1_tvs
680               bad_fld (fld, ty) = fld `elem` upd_fld_names &&
681                                       not (tyVarsOfType ty `subVarSet` con1_tv_set)
682         ; checkTc (null bad_upd_flds) (badFieldTypes bad_upd_flds)
683
684         -- STEP 4  Note [Type of a record update]
685         -- Figure out types for the scrutinee and result
686         -- Both are of form (T a b c), with fresh type variables, but with
687         -- common variables where the scrutinee and result must have the same type
688         -- These are variables that appear in *any* arg of *any* of the
689         -- relevant constructors *except* in the updated fields
690         --
691         ; let fixed_tvs = getFixedTyVars con1_tvs relevant_cons
692               is_fixed_tv tv = tv `elemVarSet` fixed_tvs
693
694               mk_inst_ty :: TvSubst -> (TKVar, TcType) -> TcM (TvSubst, TcType)
695               -- Deals with instantiation of kind variables
696               --   c.f. TcMType.tcInstTyVars
697               mk_inst_ty subst (tv, result_inst_ty)
698                 | is_fixed_tv tv   -- Same as result type
699                 = return (extendTvSubst subst tv result_inst_ty, result_inst_ty)
700                 | otherwise        -- Fresh type, of correct kind
701                 = do { new_ty <- newFlexiTyVarTy (TcType.substTy subst (tyVarKind tv))
702                      ; return (extendTvSubst subst tv new_ty, new_ty) }
703
704         ; (result_subst, con1_tvs') <- tcInstTyVars con1_tvs
705         ; let result_inst_tys = mkTyVarTys con1_tvs'
706
707         ; (scrut_subst, scrut_inst_tys) <- mapAccumLM mk_inst_ty emptyTvSubst
708                                                       (con1_tvs `zip` result_inst_tys)
709
710         ; let rec_res_ty    = TcType.substTy result_subst con1_res_ty
711               scrut_ty      = TcType.substTy scrut_subst  con1_res_ty
712               con1_arg_tys' = map (TcType.substTy result_subst) con1_arg_tys
713
714         ; co_res <- unifyType rec_res_ty res_ty
715
716         -- STEP 5
717         -- Typecheck the thing to be updated, and the bindings
718         ; record_expr' <- tcMonoExpr record_expr scrut_ty
719         ; rbinds'      <- tcRecordBinds con1 con1_arg_tys' rbinds
720
721         -- STEP 6: Deal with the stupid theta
722         ; let theta' = substTheta scrut_subst (dataConStupidTheta con1)
723         ; instStupidTheta RecordUpdOrigin theta'
724
725         -- Step 7: make a cast for the scrutinee, in the case that it's from a type family
726         ; let scrut_co | Just co_con <- tyConFamilyCoercion_maybe tycon
727                        = mkWpCast (mkTcUnbranchedAxInstCo Representational co_con scrut_inst_tys)
728                        | otherwise
729                        = idHsWrapper
730         -- Phew!
731         ; return $ mkHsWrapCo co_res $
732           RecordUpd (mkLHsWrap scrut_co record_expr') rbinds'
733                     relevant_cons scrut_inst_tys result_inst_tys  }
734   where
735     upd_fld_names = hsRecFields rbinds
736
737     getFixedTyVars :: [TyVar] -> [DataCon] -> TyVarSet
738     -- These tyvars must not change across the updates
739     getFixedTyVars tvs1 cons
740       = mkVarSet [tv1 | con <- cons
741                       , let (tvs, theta, arg_tys, _) = dataConSig con
742                             flds = dataConFieldLabels con
743                             fixed_tvs = exactTyVarsOfTypes fixed_tys
744                                     -- fixed_tys: See Note [Type of a record update]
745                                         `unionVarSet` tyVarsOfTypes theta
746                                     -- Universally-quantified tyvars that
747                                     -- appear in any of the *implicit*
748                                     -- arguments to the constructor are fixed
749                                     -- See Note [Implicit type sharing]
750
751                             fixed_tys = [ty | (fld,ty) <- zip flds arg_tys
752                                             , not (fld `elem` upd_fld_names)]
753                       , (tv1,tv) <- tvs1 `zip` tvs      -- Discards existentials in tvs
754                       , tv `elemVarSet` fixed_tvs ]
755 \end{code}
756
757 %************************************************************************
758 %*                                                                      *
759         Arithmetic sequences                    e.g. [a,b..]
760         and their parallel-array counterparts   e.g. [: a,b.. :]
761
762 %*                                                                      *
763 %************************************************************************
764
765 \begin{code}
766 tcExpr (ArithSeq _ witness seq) res_ty
767   = tcArithSeq witness seq res_ty
768
769 tcExpr (PArrSeq _ seq@(FromTo expr1 expr2)) res_ty
770   = do  { (coi, elt_ty) <- matchExpectedPArrTy res_ty
771         ; expr1' <- tcPolyExpr expr1 elt_ty
772         ; expr2' <- tcPolyExpr expr2 elt_ty
773         ; enumFromToP <- initDsTc $ dsDPHBuiltin enumFromToPVar
774         ; enum_from_to <- newMethodFromName (PArrSeqOrigin seq)
775                                  (idName enumFromToP) elt_ty
776         ; return $ mkHsWrapCo coi
777                      (PArrSeq enum_from_to (FromTo expr1' expr2')) }
778
779 tcExpr (PArrSeq _ seq@(FromThenTo expr1 expr2 expr3)) res_ty
780   = do  { (coi, elt_ty) <- matchExpectedPArrTy res_ty
781         ; expr1' <- tcPolyExpr expr1 elt_ty
782         ; expr2' <- tcPolyExpr expr2 elt_ty
783         ; expr3' <- tcPolyExpr expr3 elt_ty
784         ; enumFromThenToP <- initDsTc $ dsDPHBuiltin enumFromThenToPVar
785         ; eft <- newMethodFromName (PArrSeqOrigin seq)
786                       (idName enumFromThenToP) elt_ty        -- !!!FIXME: chak
787         ; return $ mkHsWrapCo coi
788                      (PArrSeq eft (FromThenTo expr1' expr2' expr3')) }
789
790 tcExpr (PArrSeq _ _) _
791   = panic "TcExpr.tcExpr: Infinite parallel array!"
792     -- the parser shouldn't have generated it and the renamer shouldn't have
793     -- let it through
794 \end{code}
795
796
797 %************************************************************************
798 %*                                                                      *
799                 Template Haskell
800 %*                                                                      *
801 %************************************************************************
802
803 \begin{code}
804 tcExpr (HsSpliceE is_ty splice)  res_ty
805   = ASSERT( is_ty )   -- Untyped splices are expanded by the renamer
806    tcSpliceExpr splice res_ty
807
808 tcExpr (HsBracket brack)         res_ty = tcTypedBracket   brack res_ty
809 tcExpr (HsRnBracketOut brack ps) res_ty = tcUntypedBracket brack ps res_ty
810 \end{code}
811
812
813 %************************************************************************
814 %*                                                                      *
815                 Catch-all
816 %*                                                                      *
817 %************************************************************************
818
819 \begin{code}
820 tcExpr other _ = pprPanic "tcMonoExpr" (ppr other)
821   -- Include ArrForm, ArrApp, which shouldn't appear at all
822   -- Also HsTcBracketOut, HsQuasiQuoteE
823 \end{code}
824
825
826 %************************************************************************
827 %*                                                                      *
828                 Arithmetic sequences [a..b] etc
829 %*                                                                      *
830 %************************************************************************
831
832 \begin{code}
833 tcArithSeq :: Maybe (SyntaxExpr Name) -> ArithSeqInfo Name -> TcRhoType
834            -> TcM (HsExpr TcId)
835
836 tcArithSeq witness seq@(From expr) res_ty
837   = do { (coi, elt_ty, wit') <- arithSeqEltType witness res_ty
838        ; expr' <- tcPolyExpr expr elt_ty
839        ; enum_from <- newMethodFromName (ArithSeqOrigin seq)
840                               enumFromName elt_ty
841        ; return $ mkHsWrapCo coi (ArithSeq enum_from wit' (From expr')) }
842
843 tcArithSeq witness seq@(FromThen expr1 expr2) res_ty
844   = do { (coi, elt_ty, wit') <- arithSeqEltType witness res_ty
845        ; expr1' <- tcPolyExpr expr1 elt_ty
846        ; expr2' <- tcPolyExpr expr2 elt_ty
847        ; enum_from_then <- newMethodFromName (ArithSeqOrigin seq)
848                               enumFromThenName elt_ty
849        ; return $ mkHsWrapCo coi (ArithSeq enum_from_then wit' (FromThen expr1' expr2')) }
850
851 tcArithSeq witness seq@(FromTo expr1 expr2) res_ty
852   = do { (coi, elt_ty, wit') <- arithSeqEltType witness res_ty
853        ; expr1' <- tcPolyExpr expr1 elt_ty
854        ; expr2' <- tcPolyExpr expr2 elt_ty
855        ; enum_from_to <- newMethodFromName (ArithSeqOrigin seq)
856                               enumFromToName elt_ty
857        ; return $ mkHsWrapCo coi (ArithSeq enum_from_to wit' (FromTo expr1' expr2')) }
858
859 tcArithSeq witness seq@(FromThenTo expr1 expr2 expr3) res_ty
860   = do { (coi, elt_ty, wit') <- arithSeqEltType witness res_ty
861         ; expr1' <- tcPolyExpr expr1 elt_ty
862         ; expr2' <- tcPolyExpr expr2 elt_ty
863         ; expr3' <- tcPolyExpr expr3 elt_ty
864         ; eft <- newMethodFromName (ArithSeqOrigin seq)
865                               enumFromThenToName elt_ty
866         ; return $ mkHsWrapCo coi (ArithSeq eft wit' (FromThenTo expr1' expr2' expr3')) }
867
868 -----------------
869 arithSeqEltType :: Maybe (SyntaxExpr Name) -> TcRhoType
870               -> TcM (TcCoercion, TcType, Maybe (SyntaxExpr Id))
871 arithSeqEltType Nothing res_ty
872   = do { (coi, elt_ty) <- matchExpectedListTy res_ty
873        ; return (coi, elt_ty, Nothing) }
874 arithSeqEltType (Just fl) res_ty
875   = do { list_ty <- newFlexiTyVarTy liftedTypeKind
876        ; fl' <- tcSyntaxOp ListOrigin fl (mkFunTy list_ty res_ty)
877        ; (coi, elt_ty) <- matchExpectedListTy list_ty
878        ; return (coi, elt_ty, Just fl') }
879 \end{code}
880
881 %************************************************************************
882 %*                                                                      *
883                 Applications
884 %*                                                                      *
885 %************************************************************************
886
887 \begin{code}
888 tcApp :: LHsExpr Name -> [LHsExpr Name] -- Function and args
889       -> TcRhoType -> TcM (HsExpr TcId) -- Translated fun and args
890
891 tcApp (L _ (HsPar e)) args res_ty
892   = tcApp e args res_ty
893
894 tcApp (L _ (HsApp e1 e2)) args res_ty
895   = tcApp e1 (e2:args) res_ty   -- Accumulate the arguments
896
897 tcApp (L loc (HsVar fun)) args res_ty
898   | fun `hasKey` tagToEnumKey
899   , [arg] <- args
900   = tcTagToEnum loc fun arg res_ty
901
902   | fun `hasKey` seqIdKey
903   , [arg1,arg2] <- args
904   = tcSeq loc fun arg1 arg2 res_ty
905
906 tcApp fun args res_ty
907   = do  {   -- Type-check the function
908         ; (fun1, fun_tau) <- tcInferFun fun
909
910             -- Extract its argument types
911         ; (co_fun, expected_arg_tys, actual_res_ty)
912               <- matchExpectedFunTys (mk_app_msg fun) (length args) fun_tau
913
914         -- Typecheck the result, thereby propagating
915         -- info (if any) from result into the argument types
916         -- Both actual_res_ty and res_ty are deeply skolemised
917         -- Rather like tcWrapResult, but (perhaps for historical reasons)
918         -- we do this before typechecking the arguments
919         ; wrap_res <- addErrCtxtM (funResCtxt True (unLoc fun) actual_res_ty res_ty) $
920                       tcSubTypeDS_NC GenSigCtxt actual_res_ty res_ty
921
922         -- Typecheck the arguments
923         ; args1 <- tcArgs fun args expected_arg_tys
924
925         -- Assemble the result
926         ; let fun2 = mkLHsWrapCo co_fun fun1
927               app  = mkLHsWrap wrap_res (foldl mkHsApp fun2 args1)
928
929         ; return (unLoc app) }
930
931
932 mk_app_msg :: LHsExpr Name -> SDoc
933 mk_app_msg fun = sep [ ptext (sLit "The function") <+> quotes (ppr fun)
934                      , ptext (sLit "is applied to")]
935
936 ----------------
937 tcInferFun :: LHsExpr Name -> TcM (LHsExpr TcId, TcRhoType)
938 -- Infer and instantiate the type of a function
939 tcInferFun (L loc (HsVar name))
940   = do { (fun, ty) <- setSrcSpan loc (tcInferId name)
941                -- Don't wrap a context around a plain Id
942        ; return (L loc fun, ty) }
943
944 tcInferFun fun
945   = do { (fun, fun_ty) <- tcInfer (tcMonoExpr fun)
946
947          -- Zonk the function type carefully, to expose any polymorphism
948          -- E.g. (( \(x::forall a. a->a). blah ) e)
949          -- We can see the rank-2 type of the lambda in time to generalise e
950        ; fun_ty' <- zonkTcType fun_ty
951
952        ; (wrap, rho) <- deeplyInstantiate AppOrigin fun_ty'
953        ; return (mkLHsWrap wrap fun, rho) }
954
955 ----------------
956 tcArgs :: LHsExpr Name                          -- The function (for error messages)
957        -> [LHsExpr Name] -> [TcSigmaType]       -- Actual arguments and expected arg types
958        -> TcM [LHsExpr TcId]                    -- Resulting args
959
960 tcArgs fun args expected_arg_tys
961   = mapM (tcArg fun) (zip3 args expected_arg_tys [1..])
962
963 ----------------
964 tcArg :: LHsExpr Name                           -- The function (for error messages)
965        -> (LHsExpr Name, TcSigmaType, Int)      -- Actual argument and expected arg type
966        -> TcM (LHsExpr TcId)                    -- Resulting argument
967 tcArg fun (arg, ty, arg_no) = addErrCtxt (funAppCtxt fun arg arg_no)
968                                          (tcPolyExprNC arg ty)
969
970 ----------------
971 tcTupArgs :: [LHsTupArg Name] -> [TcSigmaType] -> TcM [LHsTupArg TcId]
972 tcTupArgs args tys
973   = ASSERT( equalLength args tys ) mapM go (args `zip` tys)
974   where
975     go (L l (Missing {}),   arg_ty) = return (L l (Missing arg_ty))
976     go (L l (Present expr), arg_ty) = do { expr' <- tcPolyExpr expr arg_ty
977                                          ; return (L l (Present expr')) }
978
979 ----------------
980 unifyOpFunTysWrap :: LHsExpr Name -> Arity -> TcRhoType
981                   -> TcM (TcCoercion, [TcSigmaType], TcRhoType)
982 -- A wrapper for matchExpectedFunTys
983 unifyOpFunTysWrap op arity ty = matchExpectedFunTys herald arity ty
984   where
985     herald = ptext (sLit "The operator") <+> quotes (ppr op) <+> ptext (sLit "takes")
986
987 ---------------------------
988 tcSyntaxOp :: CtOrigin -> HsExpr Name -> TcType -> TcM (HsExpr TcId)
989 -- Typecheck a syntax operator, checking that it has the specified type
990 -- The operator is always a variable at this stage (i.e. renamer output)
991 -- This version assumes res_ty is a monotype
992 tcSyntaxOp orig (HsVar op) res_ty = do { (expr, rho) <- tcInferIdWithOrig orig op
993                                        ; tcWrapResult expr rho res_ty }
994 tcSyntaxOp _ other         _      = pprPanic "tcSyntaxOp" (ppr other)
995 \end{code}
996
997
998 Note [Push result type in]
999 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1000 Unify with expected result before type-checking the args so that the
1001 info from res_ty percolates to args.  This is when we might detect a
1002 too-few args situation.  (One can think of cases when the opposite
1003 order would give a better error message.)
1004 experimenting with putting this first.
1005
1006 Here's an example where it actually makes a real difference
1007
1008    class C t a b | t a -> b
1009    instance C Char a Bool
1010
1011    data P t a = forall b. (C t a b) => MkP b
1012    data Q t   = MkQ (forall a. P t a)
1013
1014    f1, f2 :: Q Char;
1015    f1 = MkQ (MkP True)
1016    f2 = MkQ (MkP True :: forall a. P Char a)
1017
1018 With the change, f1 will type-check, because the 'Char' info from
1019 the signature is propagated into MkQ's argument. With the check
1020 in the other order, the extra signature in f2 is reqd.
1021
1022
1023 %************************************************************************
1024 %*                                                                      *
1025                  tcInferId
1026 %*                                                                      *
1027 %************************************************************************
1028
1029 \begin{code}
1030 tcCheckId :: Name -> TcRhoType -> TcM (HsExpr TcId)
1031 tcCheckId name res_ty
1032   = do { (expr, actual_res_ty) <- tcInferId name
1033        ; traceTc "tcCheckId" (vcat [ppr name, ppr actual_res_ty, ppr res_ty])
1034        ; addErrCtxtM (funResCtxt False (HsVar name) actual_res_ty res_ty) $
1035          tcWrapResult expr actual_res_ty res_ty }
1036
1037 ------------------------
1038 tcInferId :: Name -> TcM (HsExpr TcId, TcRhoType)
1039 -- Infer type, and deeply instantiate
1040 tcInferId n = tcInferIdWithOrig (OccurrenceOf n) n
1041
1042 ------------------------
1043 tcInferIdWithOrig :: CtOrigin -> Name -> TcM (HsExpr TcId, TcRhoType)
1044 -- Look up an occurrence of an Id, and instantiate it (deeply)
1045
1046 tcInferIdWithOrig orig id_name
1047   | id_name `hasKey` tagToEnumKey
1048   = failWithTc (ptext (sLit "tagToEnum# must appear applied to one argument"))
1049         -- tcApp catches the case (tagToEnum# arg)
1050
1051   | id_name `hasKey` assertIdKey
1052   = do { dflags <- getDynFlags
1053        ; if gopt Opt_IgnoreAsserts dflags
1054          then tc_infer_id orig id_name
1055          else tc_infer_assert dflags orig }
1056
1057   | otherwise
1058   = tc_infer_id orig id_name
1059
1060 tc_infer_assert :: DynFlags -> CtOrigin -> TcM (HsExpr TcId, TcRhoType)
1061 -- Deal with an occurrence of 'assert'
1062 -- See Note [Adding the implicit parameter to 'assert']
1063 tc_infer_assert dflags orig
1064   = do { sloc <- getSrcSpanM
1065        ; assert_error_id <- tcLookupId assertErrorName
1066        ; (wrap, id_rho) <- deeplyInstantiate orig (idType assert_error_id)
1067        ; let (arg_ty, res_ty) = case tcSplitFunTy_maybe id_rho of
1068                                    Nothing      -> pprPanic "assert type" (ppr id_rho)
1069                                    Just arg_res -> arg_res
1070        ; ASSERT( arg_ty `tcEqType` addrPrimTy )
1071          return (HsApp (L sloc (mkHsWrap wrap (HsVar assert_error_id)))
1072                        (L sloc (srcSpanPrimLit dflags sloc))
1073                 , res_ty) }
1074
1075 tc_infer_id :: CtOrigin -> Name -> TcM (HsExpr TcId, TcRhoType)
1076 -- Return type is deeply instantiated
1077 tc_infer_id orig id_name
1078  = do { thing <- tcLookup id_name
1079       ; case thing of
1080              ATcId { tct_id = id }
1081                -> do { check_naughty id        -- Note [Local record selectors]
1082                      ; checkThLocalId id
1083                      ; inst_normal_id id }
1084
1085              AGlobal (AnId id)
1086                -> do { check_naughty id
1087                      ; inst_normal_id id }
1088                     -- A global cannot possibly be ill-staged
1089                     -- nor does it need the 'lifting' treatment
1090                     -- hence no checkTh stuff here
1091
1092              AGlobal (AConLike cl) -> case cl of
1093                  RealDataCon con -> inst_data_con con
1094                  PatSynCon ps    -> tcPatSynBuilderOcc orig ps
1095
1096              _ -> failWithTc $
1097                   ppr thing <+> ptext (sLit "used where a value identifer was expected") }
1098   where
1099     inst_normal_id id
1100       = do { (wrap, rho) <- deeplyInstantiate orig (idType id)
1101            ; return (mkHsWrap wrap (HsVar id), rho) }
1102
1103     inst_data_con con
1104        -- For data constructors,
1105        --   * Must perform the stupid-theta check
1106        --   * No need to deeply instantiate because type has all foralls at top
1107        = do { let wrap_id           = dataConWrapId con
1108                   (tvs, theta, rho) = tcSplitSigmaTy (idType wrap_id)
1109             ; (subst, tvs') <- tcInstTyVars tvs
1110             ; let tys'   = mkTyVarTys tvs'
1111                   theta' = substTheta subst theta
1112                   rho'   = substTy subst rho
1113             ; wrap <- instCall orig tys' theta'
1114             ; addDataConStupidTheta con tys'
1115             ; return (mkHsWrap wrap (HsVar wrap_id), rho') }
1116
1117     check_naughty id
1118       | isNaughtyRecordSelector id = failWithTc (naughtyRecordSel id)
1119       | otherwise                  = return ()
1120
1121 srcSpanPrimLit :: DynFlags -> SrcSpan -> HsExpr TcId
1122 srcSpanPrimLit dflags span
1123     = HsLit (HsStringPrim "" (unsafeMkByteString
1124                              (showSDocOneLine dflags (ppr span))))
1125 \end{code}
1126
1127 Note [Adding the implicit parameter to 'assert']
1128 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1129 The typechecker transforms (assert e1 e2) to (assertError "Foo.hs:27"
1130 e1 e2).  This isn't really the Right Thing because there's no way to
1131 "undo" if you want to see the original source code in the typechecker
1132 output.  We'll have fix this in due course, when we care more about
1133 being able to reconstruct the exact original program.
1134
1135 Note [tagToEnum#]
1136 ~~~~~~~~~~~~~~~~~
1137 Nasty check to ensure that tagToEnum# is applied to a type that is an
1138 enumeration TyCon.  Unification may refine the type later, but this
1139 check won't see that, alas.  It's crude, because it relies on our
1140 knowing *now* that the type is ok, which in turn relies on the
1141 eager-unification part of the type checker pushing enough information
1142 here.  In theory the Right Thing to do is to have a new form of
1143 constraint but I definitely cannot face that!  And it works ok as-is.
1144
1145 Here's are two cases that should fail
1146         f :: forall a. a
1147         f = tagToEnum# 0        -- Can't do tagToEnum# at a type variable
1148
1149         g :: Int
1150         g = tagToEnum# 0        -- Int is not an enumeration
1151
1152 When data type families are involved it's a bit more complicated.
1153      data family F a
1154      data instance F [Int] = A | B | C
1155 Then we want to generate something like
1156      tagToEnum# R:FListInt 3# |> co :: R:FListInt ~ F [Int]
1157 Usually that coercion is hidden inside the wrappers for
1158 constructors of F [Int] but here we have to do it explicitly.
1159
1160 It's all grotesquely complicated.
1161
1162 \begin{code}
1163 tcSeq :: SrcSpan -> Name -> LHsExpr Name -> LHsExpr Name
1164       -> TcRhoType -> TcM (HsExpr TcId)
1165 -- (seq e1 e2) :: res_ty
1166 -- We need a special typing rule because res_ty can be unboxed
1167 tcSeq loc fun_name arg1 arg2 res_ty
1168   = do  { fun <- tcLookupId fun_name
1169         ; (arg1', arg1_ty) <- tcInfer (tcMonoExpr arg1)
1170         ; arg2' <- tcMonoExpr arg2 res_ty
1171         ; let fun'    = L loc (HsWrap ty_args (HsVar fun))
1172               ty_args = WpTyApp res_ty <.> WpTyApp arg1_ty
1173         ; return (HsApp (L loc (HsApp fun' arg1')) arg2') }
1174
1175 tcTagToEnum :: SrcSpan -> Name -> LHsExpr Name -> TcRhoType -> TcM (HsExpr TcId)
1176 -- tagToEnum# :: forall a. Int# -> a
1177 -- See Note [tagToEnum#]   Urgh!
1178 tcTagToEnum loc fun_name arg res_ty
1179   = do  { fun <- tcLookupId fun_name
1180         ; ty' <- zonkTcType res_ty
1181
1182         -- Check that the type is algebraic
1183         ; let mb_tc_app = tcSplitTyConApp_maybe ty'
1184               Just (tc, tc_args) = mb_tc_app
1185         ; checkTc (isJust mb_tc_app)
1186                   (mk_error ty' doc1)
1187
1188         -- Look through any type family
1189         ; fam_envs <- tcGetFamInstEnvs
1190         ; let (rep_tc, rep_args, coi) = tcLookupDataFamInst fam_envs tc tc_args
1191              -- coi :: tc tc_args ~ rep_tc rep_args
1192
1193         ; checkTc (isEnumerationTyCon rep_tc)
1194                   (mk_error ty' doc2)
1195
1196         ; arg' <- tcMonoExpr arg intPrimTy
1197         ; let fun' = L loc (HsWrap (WpTyApp rep_ty) (HsVar fun))
1198               rep_ty = mkTyConApp rep_tc rep_args
1199
1200         ; return (mkHsWrapCoR (mkTcSymCo coi) $ HsApp fun' arg') }
1201                   -- coi is a Representational coercion
1202   where
1203     doc1 = vcat [ ptext (sLit "Specify the type by giving a type signature")
1204                 , ptext (sLit "e.g. (tagToEnum# x) :: Bool") ]
1205     doc2 = ptext (sLit "Result type must be an enumeration type")
1206
1207     mk_error :: TcType -> SDoc -> SDoc
1208     mk_error ty what
1209       = hang (ptext (sLit "Bad call to tagToEnum#")
1210                <+> ptext (sLit "at type") <+> ppr ty)
1211            2 what
1212 \end{code}
1213
1214
1215 %************************************************************************
1216 %*                                                                      *
1217                  Template Haskell checks
1218 %*                                                                      *
1219 %************************************************************************
1220
1221 \begin{code}
1222 checkThLocalId :: Id -> TcM ()
1223 #ifndef GHCI  /* GHCI and TH is off */
1224 --------------------------------------
1225 -- Check for cross-stage lifting
1226 checkThLocalId _id
1227   = return ()
1228
1229 #else         /* GHCI and TH is on */
1230 checkThLocalId id
1231   = do  { mb_local_use <- getStageAndBindLevel (idName id)
1232         ; case mb_local_use of
1233              Just (top_lvl, bind_lvl, use_stage)
1234                 | thLevel use_stage > bind_lvl
1235                 , isNotTopLevel top_lvl
1236                 -> checkCrossStageLifting id use_stage
1237              _  -> return ()   -- Not a locally-bound thing, or
1238                                -- no cross-stage link
1239     }
1240
1241 --------------------------------------
1242 checkCrossStageLifting :: Id -> ThStage -> TcM ()
1243 -- If we are inside brackets, and (use_lvl > bind_lvl)
1244 -- we must check whether there's a cross-stage lift to do
1245 -- Examples   \x -> [| x |]
1246 --            [| map |]
1247 -- There is no error-checking to do, because the renamer did that
1248
1249 checkCrossStageLifting id (Brack _ (TcPending ps_var lie_var))
1250   =     -- Nested identifiers, such as 'x' in
1251         -- E.g. \x -> [| h x |]
1252         -- We must behave as if the reference to x was
1253         --      h $(lift x)
1254         -- We use 'x' itself as the splice proxy, used by
1255         -- the desugarer to stitch it all back together.
1256         -- If 'x' occurs many times we may get many identical
1257         -- bindings of the same splice proxy, but that doesn't
1258         -- matter, although it's a mite untidy.
1259     do  { let id_ty = idType id
1260         ; checkTc (isTauTy id_ty) (polySpliceErr id)
1261                -- If x is polymorphic, its occurrence sites might
1262                -- have different instantiations, so we can't use plain
1263                -- 'x' as the splice proxy name.  I don't know how to
1264                -- solve this, and it's probably unimportant, so I'm
1265                -- just going to flag an error for now
1266
1267         ; lift <- if isStringTy id_ty then
1268                      do { sid <- tcLookupId DsMeta.liftStringName
1269                                      -- See Note [Lifting strings]
1270                         ; return (HsVar sid) }
1271                   else
1272                      setConstraintVar lie_var   $
1273                           -- Put the 'lift' constraint into the right LIE
1274                      newMethodFromName (OccurrenceOf (idName id))
1275                                        DsMeta.liftName id_ty
1276
1277                    -- Update the pending splices
1278         ; ps <- readMutVar ps_var
1279         ; let pending_splice = PendSplice (idName id) (nlHsApp (noLoc lift) (nlHsVar id))
1280         ; writeMutVar ps_var (pending_splice : ps)
1281
1282         ; return () }
1283
1284 checkCrossStageLifting _ _ = return ()
1285
1286 polySpliceErr :: Id -> SDoc
1287 polySpliceErr id
1288   = ptext (sLit "Can't splice the polymorphic local variable") <+> quotes (ppr id)
1289 #endif /* GHCI */
1290 \end{code}
1291
1292 Note [Lifting strings]
1293 ~~~~~~~~~~~~~~~~~~~~~~
1294 If we see $(... [| s |] ...) where s::String, we don't want to
1295 generate a mass of Cons (CharL 'x') (Cons (CharL 'y') ...)) etc.
1296 So this conditional short-circuits the lifting mechanism to generate
1297 (liftString "xy") in that case.  I didn't want to use overlapping instances
1298 for the Lift class in TH.Syntax, because that can lead to overlapping-instance
1299 errors in a polymorphic situation.
1300
1301 If this check fails (which isn't impossible) we get another chance; see
1302 Note [Converting strings] in Convert.lhs
1303
1304 Local record selectors
1305 ~~~~~~~~~~~~~~~~~~~~~~
1306 Record selectors for TyCons in this module are ordinary local bindings,
1307 which show up as ATcIds rather than AGlobals.  So we need to check for
1308 naughtiness in both branches.  c.f. TcTyClsBindings.mkAuxBinds.
1309
1310
1311 %************************************************************************
1312 %*                                                                      *
1313 \subsection{Record bindings}
1314 %*                                                                      *
1315 %************************************************************************
1316
1317 Game plan for record bindings
1318 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1319 1. Find the TyCon for the bindings, from the first field label.
1320
1321 2. Instantiate its tyvars and unify (T a1 .. an) with expected_ty.
1322
1323 For each binding field = value
1324
1325 3. Instantiate the field type (from the field label) using the type
1326    envt from step 2.
1327
1328 4  Type check the value using tcArg, passing the field type as
1329    the expected argument type.
1330
1331 This extends OK when the field types are universally quantified.
1332
1333
1334 \begin{code}
1335 tcRecordBinds
1336         :: DataCon
1337         -> [TcType]     -- Expected type for each field
1338         -> HsRecordBinds Name
1339         -> TcM (HsRecordBinds TcId)
1340
1341 tcRecordBinds data_con arg_tys (HsRecFields rbinds dd)
1342   = do  { mb_binds <- mapM do_bind rbinds
1343         ; return (HsRecFields (catMaybes mb_binds) dd) }
1344   where
1345     flds_w_tys = zipEqual "tcRecordBinds" (dataConFieldLabels data_con) arg_tys
1346     do_bind (L l fld@(HsRecField { hsRecFieldId = L loc field_lbl
1347                                  , hsRecFieldArg = rhs }))
1348       | Just field_ty <- assocMaybe flds_w_tys field_lbl
1349       = addErrCtxt (fieldCtxt field_lbl)        $
1350         do { rhs' <- tcPolyExprNC rhs field_ty
1351            ; let field_id = mkUserLocal (nameOccName field_lbl)
1352                                         (nameUnique field_lbl)
1353                                         field_ty loc
1354                 -- Yuk: the field_id has the *unique* of the selector Id
1355                 --          (so we can find it easily)
1356                 --      but is a LocalId with the appropriate type of the RHS
1357                 --          (so the desugarer knows the type of local binder to make)
1358            ; return (Just (L l (fld { hsRecFieldId = L loc field_id
1359                                     , hsRecFieldArg = rhs' }))) }
1360       | otherwise
1361       = do { addErrTc (badFieldCon (RealDataCon data_con) field_lbl)
1362            ; return Nothing }
1363
1364 checkMissingFields :: DataCon -> HsRecordBinds Name -> TcM ()
1365 checkMissingFields data_con rbinds
1366   | null field_labels   -- Not declared as a record;
1367                         -- But C{} is still valid if no strict fields
1368   = if any isBanged field_strs then
1369         -- Illegal if any arg is strict
1370         addErrTc (missingStrictFields data_con [])
1371     else
1372         return ()
1373
1374   | otherwise = do              -- A record
1375     unless (null missing_s_fields)
1376            (addErrTc (missingStrictFields data_con missing_s_fields))
1377
1378     warn <- woptM Opt_WarnMissingFields
1379     unless (not (warn && notNull missing_ns_fields))
1380            (warnTc True (missingFields data_con missing_ns_fields))
1381
1382   where
1383     missing_s_fields
1384         = [ fl | (fl, str) <- field_info,
1385                  isBanged str,
1386                  not (fl `elem` field_names_used)
1387           ]
1388     missing_ns_fields
1389         = [ fl | (fl, str) <- field_info,
1390                  not (isBanged str),
1391                  not (fl `elem` field_names_used)
1392           ]
1393
1394     field_names_used = hsRecFields rbinds
1395     field_labels     = dataConFieldLabels data_con
1396
1397     field_info = zipEqual "missingFields"
1398                           field_labels
1399                           field_strs
1400
1401     field_strs = dataConStrictMarks data_con
1402 \end{code}
1403
1404 %************************************************************************
1405 %*                                                                      *
1406 \subsection{Errors and contexts}
1407 %*                                                                      *
1408 %************************************************************************
1409
1410 Boring and alphabetical:
1411 \begin{code}
1412 addExprErrCtxt :: LHsExpr Name -> TcM a -> TcM a
1413 addExprErrCtxt expr = addErrCtxt (exprCtxt expr)
1414
1415 exprCtxt :: LHsExpr Name -> SDoc
1416 exprCtxt expr
1417   = hang (ptext (sLit "In the expression:")) 2 (ppr expr)
1418
1419 fieldCtxt :: Name -> SDoc
1420 fieldCtxt field_name
1421   = ptext (sLit "In the") <+> quotes (ppr field_name) <+> ptext (sLit "field of a record")
1422
1423 funAppCtxt :: LHsExpr Name -> LHsExpr Name -> Int -> SDoc
1424 funAppCtxt fun arg arg_no
1425   = hang (hsep [ ptext (sLit "In the"), speakNth arg_no, ptext (sLit "argument of"),
1426                     quotes (ppr fun) <> text ", namely"])
1427        2 (quotes (ppr arg))
1428
1429 funResCtxt :: Bool  -- There is at least one argument
1430            -> HsExpr Name -> TcType -> TcType
1431            -> TidyEnv -> TcM (TidyEnv, MsgDoc)
1432 -- When we have a mis-match in the return type of a function
1433 -- try to give a helpful message about too many/few arguments
1434 --
1435 -- Used for naked variables too; but with has_args = False
1436 funResCtxt has_args fun fun_res_ty env_ty tidy_env
1437   = do { fun_res' <- zonkTcType fun_res_ty
1438        ; env'     <- zonkTcType env_ty
1439        ; let (args_fun, res_fun) = tcSplitFunTys fun_res'
1440              (args_env, res_env) = tcSplitFunTys env'
1441              n_fun = length args_fun
1442              n_env = length args_env
1443              info  | n_fun == n_env = Outputable.empty
1444                    | n_fun > n_env
1445                    , not_fun res_env = ptext (sLit "Probable cause:") <+> quotes (ppr fun)
1446                                        <+> ptext (sLit "is applied to too few arguments")
1447                    | has_args
1448                    , not_fun res_fun = ptext (sLit "Possible cause:") <+> quotes (ppr fun)
1449                                        <+> ptext (sLit "is applied to too many arguments")
1450                    | otherwise       = Outputable.empty  -- Never suggest that a naked variable is
1451                                                          -- applied to too many args!
1452        ; return (tidy_env, info) }
1453   where
1454     not_fun ty   -- ty is definitely not an arrow type,
1455                  -- and cannot conceivably become one
1456       = case tcSplitTyConApp_maybe ty of
1457           Just (tc, _) -> isAlgTyCon tc
1458           Nothing      -> False
1459
1460 badFieldTypes :: [(Name,TcType)] -> SDoc
1461 badFieldTypes prs
1462   = hang (ptext (sLit "Record update for insufficiently polymorphic field")
1463                          <> plural prs <> colon)
1464        2 (vcat [ ppr f <+> dcolon <+> ppr ty | (f,ty) <- prs ])
1465
1466 badFieldsUpd
1467   :: HsRecFields Name a -- Field names that don't belong to a single datacon
1468   -> [DataCon] -- Data cons of the type which the first field name belongs to
1469   -> SDoc
1470 badFieldsUpd rbinds data_cons
1471   = hang (ptext (sLit "No constructor has all these fields:"))
1472        2 (pprQuotedList conflictingFields)
1473           -- See Note [Finding the conflicting fields]
1474   where
1475     -- A (preferably small) set of fields such that no constructor contains
1476     -- all of them.  See Note [Finding the conflicting fields]
1477     conflictingFields = case nonMembers of
1478         -- nonMember belongs to a different type.
1479         (nonMember, _) : _ -> [aMember, nonMember]
1480         [] -> let
1481             -- All of rbinds belong to one type. In this case, repeatedly add
1482             -- a field to the set until no constructor contains the set.
1483
1484             -- Each field, together with a list indicating which constructors
1485             -- have all the fields so far.
1486             growingSets :: [(Name, [Bool])]
1487             growingSets = scanl1 combine membership
1488             combine (_, setMem) (field, fldMem)
1489               = (field, zipWith (&&) setMem fldMem)
1490             in
1491             -- Fields that don't change the membership status of the set
1492             -- are redundant and can be dropped.
1493             map (fst . head) $ groupBy ((==) `on` snd) growingSets
1494
1495     aMember = ASSERT( not (null members) ) fst (head members)
1496     (members, nonMembers) = partition (or . snd) membership
1497
1498     -- For each field, which constructors contain the field?
1499     membership :: [(Name, [Bool])]
1500     membership = sortMembership $
1501         map (\fld -> (fld, map (Set.member fld) fieldLabelSets)) $
1502           hsRecFields rbinds
1503
1504     fieldLabelSets :: [Set.Set Name]
1505     fieldLabelSets = map (Set.fromList . dataConFieldLabels) data_cons
1506
1507     -- Sort in order of increasing number of True, so that a smaller
1508     -- conflicting set can be found.
1509     sortMembership =
1510       map snd .
1511       sortBy (compare `on` fst) .
1512       map (\ item@(_, membershipRow) -> (countTrue membershipRow, item))
1513
1514     countTrue = length . filter id
1515 \end{code}
1516
1517 Note [Finding the conflicting fields]
1518 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1519 Suppose we have
1520   data A = A {a0, a1 :: Int}
1521          | B {b0, b1 :: Int}
1522 and we see a record update
1523   x { a0 = 3, a1 = 2, b0 = 4, b1 = 5 }
1524 Then we'd like to find the smallest subset of fields that no
1525 constructor has all of.  Here, say, {a0,b0}, or {a0,b1}, etc.
1526 We don't really want to report that no constructor has all of
1527 {a0,a1,b0,b1}, because when there are hundreds of fields it's 
1528 hard to see what was really wrong.
1529
1530 We may need more than two fields, though; eg
1531   data T = A { x,y :: Int, v::Int } 
1532           | B { y,z :: Int, v::Int } 
1533           | C { z,x :: Int, v::Int }
1534 with update
1535    r { x=e1, y=e2, z=e3 }, we
1536
1537 Finding the smallest subset is hard, so the code here makes
1538 a decent stab, no more.  See Trac #7989. 
1539
1540 \begin{code}
1541 naughtyRecordSel :: TcId -> SDoc
1542 naughtyRecordSel sel_id
1543   = ptext (sLit "Cannot use record selector") <+> quotes (ppr sel_id) <+>
1544     ptext (sLit "as a function due to escaped type variables") $$
1545     ptext (sLit "Probable fix: use pattern-matching syntax instead")
1546
1547 notSelector :: Name -> SDoc
1548 notSelector field
1549   = hsep [quotes (ppr field), ptext (sLit "is not a record selector")]
1550
1551 missingStrictFields :: DataCon -> [FieldLabel] -> SDoc
1552 missingStrictFields con fields
1553   = header <> rest
1554   where
1555     rest | null fields = Outputable.empty  -- Happens for non-record constructors
1556                                            -- with strict fields
1557          | otherwise   = colon <+> pprWithCommas ppr fields
1558
1559     header = ptext (sLit "Constructor") <+> quotes (ppr con) <+>
1560              ptext (sLit "does not have the required strict field(s)")
1561
1562 missingFields :: DataCon -> [FieldLabel] -> SDoc
1563 missingFields con fields
1564   = ptext (sLit "Fields of") <+> quotes (ppr con) <+> ptext (sLit "not initialised:")
1565         <+> pprWithCommas ppr fields
1566
1567 -- callCtxt fun args = ptext (sLit "In the call") <+> parens (ppr (foldl mkHsApp fun args))
1568 \end{code}