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