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