compiler/typecheck/TcExpr.lhs

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