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