Big tidy-up of deriving code
[ghc-hetmet.git] / compiler / typecheck / TcExpr.lhs
index 0da370b..0ac873e 100644 (file)
@@ -1,4 +1,5 @@
 %
+% (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
 \section[TcExpr]{Typecheck an expression}
@@ -11,73 +12,42 @@ module TcExpr ( tcPolyExpr, tcPolyExprNC,
 
 #ifdef GHCI    /* Only if bootstrapped */
 import {-# SOURCE #-}  TcSplice( tcSpliceExpr, tcBracket )
-import HsSyn           ( nlHsVar )
-import Id              ( Id )
-import Name            ( isExternalName )
-import TcType          ( isTauTy )
-import TcEnv           ( checkWellStaged )
-import HsSyn           ( nlHsApp )
 import qualified DsMeta
 #endif
 
-import HsSyn           ( HsExpr(..), LHsExpr, ArithSeqInfo(..), recBindFields,
-                         HsMatchContext(..), HsRecordBinds, 
-                         mkHsCoerce, mkHsApp, mkHsDictApp, mkHsTyApp )
-import TcHsSyn         ( hsLitType )
+import HsSyn
+import TcHsSyn
 import TcRnMonad
-import TcUnify         ( tcInfer, tcSubExp, tcFunResTy, tcGen, boxyUnify, subFunTys, zapToMonotype, stripBoxyType,
-                         boxySplitListTy, boxySplitTyConApp, wrapFunResCoercion, preSubType,
-                         unBox )
-import BasicTypes      ( Arity, isMarkedStrict )
-import Inst            ( newMethodFromName, newIPDict, instToId,
-                         newDicts, newMethodWithGivenTy, tcInstStupidTheta )
-import TcBinds         ( tcLocalBinds )
-import TcEnv           ( tcLookup, tcLookupId, tcLookupDataCon, tcLookupField )
-import TcArrows                ( tcProc )
-import TcMatches       ( tcMatchesCase, tcMatchLambda, tcDoStmts, TcMatchCtxt(..) )
-import TcHsType                ( tcHsSigType, UserTypeCtxt(..) )
-import TcPat           ( tcOverloadedLit, badFieldCon )
-import TcMType         ( tcInstTyVars, newFlexiTyVarTy, newBoxyTyVars, readFilledBox, zonkTcTypes )
-import TcType          ( TcType, TcSigmaType, TcRhoType, 
-                         BoxySigmaType, BoxyRhoType, ThetaType,
-                         mkTyVarTys, mkFunTys, 
-                         tcMultiSplitSigmaTy, tcSplitFunTysN, tcSplitTyConApp_maybe,
-                         isSigmaTy, mkFunTy, mkTyConApp, isLinearPred,
-                         exactTyVarsOfType, exactTyVarsOfTypes, 
-                         zipTopTvSubst, zipOpenTvSubst, substTys, substTyVar
-                       )
-import Kind            ( argTypeKind )
-
-import Id              ( Id, idType, idName, recordSelectorFieldLabel, 
-                         isRecordSelector, isNaughtyRecordSelector, isDataConId_maybe )
-import DataCon         ( DataCon, dataConFieldLabels, dataConStrictMarks, dataConSourceArity,
-                         dataConWrapId, isVanillaDataCon, dataConTyVars, dataConOrigArgTys )
-import Name            ( Name )
-import TyCon           ( FieldLabel, tyConStupidTheta, tyConDataCons, isEnumerationTyCon )
-import Type            ( substTheta, substTy )
-import Var             ( TyVar, tyVarKind )
-import VarSet          ( emptyVarSet, elemVarSet, unionVarSet )
-import TysWiredIn      ( boolTy, parrTyCon, tupleTyCon )
-import PrelNames       ( enumFromName, enumFromThenName, 
-                         enumFromToName, enumFromThenToName,
-                         enumFromToPName, enumFromThenToPName, negateName,
-                         hasKey
-                       )
-import PrimOp          ( tagToEnumKey )
-
+import TcUnify
+import BasicTypes
+import Inst
+import TcBinds
+import TcEnv
+import TcArrows
+import TcMatches
+import TcHsType
+import TcPat
+import TcMType
+import TcType
+import Id
+import DataCon
+import Name
+import TyCon
+import Type
+import Var
+import VarSet
+import TysWiredIn
+import PrelNames
+import PrimOp
 import DynFlags
-import StaticFlags     ( opt_NoMethodSharing )
-import HscTypes                ( TyThing(..) )
-import SrcLoc          ( Located(..), unLoc, noLoc, getLoc )
+import StaticFlags
+import HscTypes
+import SrcLoc
 import Util
-import ListSetOps      ( assocMaybe )
-import Maybes          ( catMaybes )
+import ListSetOps
+import Maybes
 import Outputable
 import FastString
-
-#ifdef DEBUG
-import TyCon           ( tyConArity )
-#endif
 \end{code}
 
 %************************************************************************
@@ -103,10 +73,11 @@ tcPolyExpr expr res_ty
 
 tcPolyExprNC expr res_ty 
   | isSigmaTy res_ty
-  = do { (gen_fn, expr') <- tcGen res_ty emptyVarSet (tcPolyExprNC expr)
+  = do { (gen_fn, expr') <- tcGen res_ty emptyVarSet (\_ -> tcPolyExprNC expr)
                -- Note the recursive call to tcPolyExpr, because the
                -- type may have multiple layers of for-alls
-       ; return (L (getLoc expr') (mkHsCoerce gen_fn (unLoc expr'))) }
+               -- E.g. forall a. Eq a => forall b. Ord b => ....
+       ; return (mkLHsWrap gen_fn expr') }
 
   | otherwise
   = tcMonoExpr expr res_ty
@@ -158,6 +129,9 @@ tcExpr (HsPar expr)     res_ty = do { expr' <- tcMonoExpr expr res_ty
 
 tcExpr (HsSCC lbl expr) res_ty = do { expr' <- tcMonoExpr expr res_ty
                                    ; returnM (HsSCC lbl expr') }
+tcExpr (HsTickPragma info expr) res_ty 
+                                      = do { expr' <- tcMonoExpr expr res_ty
+                                   ; returnM (HsTickPragma info expr') }
 
 tcExpr (HsCoreAnn lbl expr) res_ty      -- hdaume: core annotation
   = do { expr' <- tcMonoExpr expr res_ty
@@ -182,7 +156,7 @@ tcExpr (HsIPVar ip) res_ty
        ; co_fn <- tcSubExp ip_ty res_ty
        ; (ip', inst) <- newIPDict (IPOccOrigin ip) ip ip_ty
        ; extendLIE inst
-       ; return (mkHsCoerce co_fn (HsIPVar ip')) }
+       ; return (mkHsWrap co_fn (HsIPVar ip')) }
 
 tcExpr (HsApp e1 e2) res_ty 
   = go e1 [e2]
@@ -196,13 +170,18 @@ tcExpr (HsApp e1 e2) res_ty
 
 tcExpr (HsLam match) res_ty
   = do { (co_fn, match') <- tcMatchLambda match res_ty
-       ; return (mkHsCoerce co_fn (HsLam match')) }
+       ; return (mkHsWrap co_fn (HsLam match')) }
 
 tcExpr in_expr@(ExprWithTySig expr sig_ty) res_ty
  = do  { sig_tc_ty <- tcHsSigType ExprSigCtxt sig_ty
-       ; expr' <- tcPolyExpr expr sig_tc_ty
+
+       -- Remember to extend the lexical type-variable environment
+       ; (gen_fn, expr') <- tcGen sig_tc_ty emptyVarSet (\ skol_tvs res_ty ->
+                            tcExtendTyVarEnv2 (hsExplicitTvs sig_ty `zip` mkTyVarTys skol_tvs) $
+                            tcPolyExprNC expr res_ty)
+
        ; co_fn <- tcSubExp sig_tc_ty res_ty
-       ; return (mkHsCoerce co_fn (ExprWithTySigOut expr' sig_ty)) }
+       ; return (mkHsWrap co_fn (ExprWithTySigOut (mkLHsWrap gen_fn expr') sig_ty)) }
 
 tcExpr (HsType ty) res_ty
   = failWithTc (text "Can't handle type argument:" <+> ppr ty)
@@ -248,14 +227,16 @@ tcExpr in_expr@(SectionL arg1 lop@(L loc op)) res_ty
 tcExpr in_expr@(SectionR lop@(L loc op) arg2) res_ty
   = do { (co_fn, (op', arg2')) <- subFunTys doc 1 res_ty $ \ [arg1_ty'] res_ty' ->
                                   tcApp op 2 (tc_args arg1_ty') res_ty'
-       ; return (mkHsCoerce co_fn (SectionR (L loc op') arg2')) }
+       ; return (mkHsWrap co_fn (SectionR (L loc op') arg2')) }
   where
     doc = ptext SLIT("The section") <+> quotes (ppr in_expr)
                <+> ptext SLIT("takes one argument")
-    tc_args arg1_ty' [arg1_ty, arg2_ty] 
-       = do { boxyUnify arg1_ty' arg1_ty
-            ; tcArg lop (arg2, arg2_ty, 2) }
-    tc_args arg1_ty' other = panic "tcExpr SectionR"
+    tc_args arg1_ty' qtvs qtys [arg1_ty, arg2_ty] 
+       = do { boxyUnify arg1_ty' (substTyWith qtvs qtys arg1_ty)
+            ; arg2' <- tcArg lop 2 arg2 qtvs qtys arg2_ty 
+            ; qtys' <- mapM refineBox qtys     -- c.f. tcArgs 
+            ; return (qtys', arg2') }
+    tc_args arg1_ty' _ _ _ = panic "tcExpr SectionR"
 \end{code}
 
 \begin{code}
@@ -282,7 +263,7 @@ tcExpr (HsCase scrut matches) exp_ty
        ; return (HsCase scrut' matches') }
  where
     match_ctxt = MC { mc_what = CaseAlt,
-                     mc_body = tcPolyExpr }
+                     mc_body = tcBody }
 
 tcExpr (HsIf pred b1 b2) res_ty
   = do { pred' <- addErrCtxt (predCtxt pred) $
@@ -345,12 +326,15 @@ tcExpr expr@(RecordCon (L loc con_name) _ rbinds) res_ty
        ; checkMissingFields data_con rbinds
 
        ; let arity = dataConSourceArity data_con
-             check_fields arg_tys 
-                 = do  { rbinds' <- tcRecordBinds data_con arg_tys rbinds
-                       ; mapM unBox arg_tys 
-                       ; return rbinds' }
-               -- The unBox ensures that all the boxes in arg_tys are indeed
+             check_fields qtvs qtys arg_tys 
+                 = do  { let arg_tys' = substTys (zipOpenTvSubst qtvs qtys) arg_tys
+                       ; rbinds' <- tcRecordBinds data_con arg_tys' rbinds
+                       ; qtys' <- mapM refineBoxToTau qtys
+                       ; return (qtys', rbinds') }
+               -- The refineBoxToTau ensures that all the boxes in arg_tys are indeed
                -- filled, which is the invariant expected by tcIdApp
+               -- How could this not be the case?  Consider a record construction
+               -- that does not mention all the fields.
 
        ; (con_expr, rbinds') <- tcIdApp con_name arity check_fields res_ty
 
@@ -440,7 +424,7 @@ tcExpr expr@(RecordUpd record_expr rbinds _ _) res_ty
                -- A constructor is only relevant to this process if
                -- it contains *all* the fields that are being updated
        con1            = head relevant_cons    -- A representative constructor
-       con1_tyvars     = dataConTyVars con1
+       con1_tyvars     = dataConUnivTyVars con1 
        con1_flds       = dataConFieldLabels con1
        con1_arg_tys    = dataConOrigArgTys con1
        common_tyvars   = exactTyVarsOfTypes [ty | (fld,ty) <- con1_flds `zip` con1_arg_tys
@@ -481,17 +465,14 @@ tcExpr expr@(RecordUpd record_expr rbinds _ _) res_ty
        -- dictionaries for the data type context, since we are going to
        -- do pattern matching over the data cons.
        --
-       -- What dictionaries do we need?  
-       -- We just take the context of the first data constructor
-       -- This isn't right, but I just can't bear to union up all the relevant ones
+       -- What dictionaries do we need?  The tyConStupidTheta tells us.
     let
        theta' = substTheta inst_env (tyConStupidTheta tycon)
     in
-    newDicts RecordUpdOrigin theta'    `thenM` \ dicts ->
-    extendLIEs dicts                   `thenM_`
+    instStupidTheta RecordUpdOrigin theta'     `thenM_`
 
        -- Phew!
-    returnM (mkHsCoerce co_fn (RecordUpd record_expr' rbinds' record_ty result_record_ty))
+    returnM (mkHsWrap co_fn (RecordUpd record_expr' rbinds' record_ty result_record_ty))
 \end{code}
 
 
@@ -598,9 +579,9 @@ tcExpr other _ = pprPanic "tcMonoExpr" (ppr other)
 ---------------------------
 tcApp :: HsExpr Name                           -- Function
       -> Arity                                 -- Number of args reqd
-      -> ([BoxySigmaType] -> TcM arg_results)  -- Argument type-checker
+      -> ArgChecker results
       -> BoxyRhoType                           -- Result type
-      -> TcM (HsExpr TcId, arg_results)                
+      -> TcM (HsExpr TcId, results)            
 
 -- (tcFun fun n_args arg_checker res_ty)
 -- The argument type checker, arg_checker, will be passed exactly n_args types
@@ -609,19 +590,18 @@ tcApp (HsVar fun_name) n_args arg_checker res_ty
   = tcIdApp fun_name n_args arg_checker res_ty
 
 tcApp fun n_args arg_checker res_ty    -- The vanilla case (rula APP)
-  = do { arg_boxes <- newBoxyTyVars (replicate n_args argTypeKind)
-       ; fun'      <- tcExpr fun (mkFunTys (mkTyVarTys arg_boxes) res_ty)
-       ; arg_tys'  <- mapM readFilledBox arg_boxes
-       ; args'     <- arg_checker arg_tys'
+  = do { arg_boxes  <- newBoxyTyVars (replicate n_args argTypeKind)
+       ; fun'       <- tcExpr fun (mkFunTys (mkTyVarTys arg_boxes) res_ty)
+       ; arg_tys'   <- mapM readFilledBox arg_boxes
+       ; (_, args') <- arg_checker [] [] arg_tys'      -- Yuk
        ; return (fun', args') }
 
 ---------------------------
 tcIdApp :: Name                                        -- Function
         -> Arity                               -- Number of args reqd
-        -> ([BoxySigmaType] -> TcM arg_results)        -- Argument type-checker
-               -- The arg-checker guarantees to fill all boxes in the arg types
+        -> ArgChecker results  -- The arg-checker guarantees to fill all boxes in the arg types
         -> BoxyRhoType                         -- Result type
-        -> TcM (HsExpr TcId, arg_results)              
+        -> TcM (HsExpr TcId, results)          
 
 -- Call        (f e1 ... en) :: res_ty
 -- Type                f :: forall a b c. theta => fa_1 -> ... -> fa_k -> fres
@@ -633,10 +613,11 @@ tcIdApp :: Name                                   -- Function
 -- Then                fres <= bx_(k+1) -> ... -> bx_n -> res_ty
 
 tcIdApp fun_name n_args arg_checker res_ty
-  = do { fun_id <- lookupFun (OccurrenceOf fun_name) fun_name
+  = do { let orig = OccurrenceOf fun_name
+       ; (fun, fun_ty) <- lookupFun orig fun_name
 
        -- Split up the function type
-       ; let (tv_theta_prs, rho) = tcMultiSplitSigmaTy (idType fun_id)
+       ; let (tv_theta_prs, rho) = tcMultiSplitSigmaTy fun_ty
              (fun_arg_tys, fun_res_ty) = tcSplitFunTysN rho n_args
 
              qtvs = concatMap fst tv_theta_prs         -- Quantified tyvars
@@ -653,23 +634,16 @@ tcIdApp fun_name n_args arg_checker res_ty
        ; let extra_arg_tys' = mkTyVarTys extra_arg_boxes
              res_ty'        = mkFunTys extra_arg_tys' res_ty
        ; qtys' <- preSubType qtvs tau_qtvs fun_res_ty res_ty'
-       ; let arg_subst    = zipOpenTvSubst qtvs qtys'
-             fun_arg_tys' = substTys arg_subst fun_arg_tys
 
        -- Typecheck the arguments!
        -- Doing so will fill arg_qtvs and extra_arg_tys'
-       ; args' <- arg_checker (fun_arg_tys' ++ extra_arg_tys')
+       ; (qtys'', args') <- arg_checker qtvs qtys' (fun_arg_tys ++ extra_arg_tys')
 
        -- Strip boxes from the qtvs that have been filled in by the arg checking
-       -- AND any variables that are mentioned in neither arg nor result
-       -- the latter are mentioned only in constraints; stripBoxyType will 
-       -- fill them with a monotype
-       ; let strip qtv qty' | qtv `elemVarSet` arg_qtvs = stripBoxyType qty'
-                            | otherwise                 = return qty'
-       ; qtys'' <- zipWithM strip qtvs qtys'
        ; extra_arg_tys'' <- mapM readFilledBox extra_arg_boxes
 
        -- Result subsumption
+       -- This fills in res_qtvs
        ; let res_subst = zipOpenTvSubst qtvs qtys''
              fun_res_ty'' = substTy res_subst fun_res_ty
              res_ty'' = mkFunTys extra_arg_tys'' res_ty
@@ -678,9 +652,9 @@ tcIdApp fun_name n_args arg_checker res_ty
        -- And pack up the results
        -- By applying the coercion just to the *function* we can make
        -- tcFun work nicely for OpApp and Sections too
-       ; fun' <- instFun fun_id qtvs qtys'' tv_theta_prs
-       ; co_fn' <- wrapFunResCoercion fun_arg_tys' co_fn
-       ; return (mkHsCoerce co_fn' fun', args') }
+       ; fun' <- instFun orig fun res_subst tv_theta_prs
+       ; co_fn' <- wrapFunResCoercion (substTys res_subst fun_arg_tys) co_fn
+       ; return (mkHsWrap co_fn' fun', args') }
 \end{code}
 
 Note [Silly type synonyms in smart-app]
@@ -707,10 +681,10 @@ tcId :: InstOrigin
      -> TcM (HsExpr TcId)
 tcId orig fun_name res_ty
   = do { traceTc (text "tcId" <+> ppr fun_name <+> ppr res_ty)
-       ; fun_id <- lookupFun orig fun_name
+       ; (fun, fun_ty) <- lookupFun orig fun_name
 
        -- Split up the function type
-       ; let (tv_theta_prs, fun_tau) = tcMultiSplitSigmaTy (idType fun_id)
+       ; let (tv_theta_prs, fun_tau) = tcMultiSplitSigmaTy fun_ty
              qtvs = concatMap fst tv_theta_prs -- Quantified tyvars
              tau_qtvs = exactTyVarsOfType fun_tau      -- Mentioned in the tau part
        ; qtv_tys <- preSubType qtvs tau_qtvs fun_tau res_ty
@@ -722,8 +696,8 @@ tcId orig fun_name res_ty
        ; co_fn <- tcFunResTy fun_name fun_tau' res_ty
 
        -- And pack up the results
-       ; fun' <- instFun fun_id qtvs qtv_tys tv_theta_prs 
-       ; return (mkHsCoerce co_fn fun') }
+       ; fun' <- instFun orig fun res_subst tv_theta_prs 
+       ; return (mkHsWrap co_fn fun') }
 
 --     Note [Push result type in]
 --
@@ -756,63 +730,43 @@ tcSyntaxOp orig (HsVar op) ty = tcId orig op ty
 tcSyntaxOp orig other     ty = pprPanic "tcSyntaxOp" (ppr other)
 
 ---------------------------
-instFun :: TcId
-       -> [TyVar] -> [TcType]  -- Quantified type variables and 
-                               -- their instantiating types
-       -> [([TyVar], ThetaType)]       -- Stuff to instantiate
+instFun :: InstOrigin
+       -> HsExpr TcId
+       -> TvSubst                -- The instantiating substitution
+       -> [([TyVar], ThetaType)] -- Stuff to instantiate
        -> TcM (HsExpr TcId)    
-instFun fun_id qtvs qtv_tys []
-  = return (HsVar fun_id)      -- Common short cut
 
-instFun fun_id qtvs qtv_tys tv_theta_prs
-  = do         {       -- Horrid check for tagToEnum; see Note [tagToEnum#]
-         checkBadTagToEnumCall fun_id qtv_tys
+instFun orig fun subst []
+  = return fun         -- Common short cut
 
-       ; let subst = zipOpenTvSubst qtvs qtv_tys
-             ty_theta_prs' = map subst_pr tv_theta_prs
-             subst_pr (tvs, theta) = (map (substTyVar subst) tvs, 
-                                      substTheta subst theta)
+instFun orig fun subst tv_theta_prs
+  = do         { let ty_theta_prs' = map subst_pr tv_theta_prs
 
-               -- The ty_theta_prs' is always non-empty
-             ((tys1',theta1') : further_prs') = ty_theta_prs'
-               
-               -- First, chuck in the constraints from 
-               -- the "stupid theta" of a data constructor (sigh)
-       ; case isDataConId_maybe fun_id of
-               Just con -> tcInstStupidTheta con tys1'
-               Nothing  -> return ()
-
-       ; if want_method_inst theta1'
-         then do { meth_id <- newMethodWithGivenTy orig fun_id tys1'
-                       -- See Note [Multiple instantiation]
-                 ; go (HsVar meth_id) further_prs' }
-         else go (HsVar fun_id) ty_theta_prs'
-       }
+                -- Make two ad-hoc checks 
+       ; doStupidChecks fun ty_theta_prs'
+
+               -- Now do normal instantiation
+       ; go True fun ty_theta_prs' }
   where
-    orig = OccurrenceOf (idName fun_id)
+    subst_pr (tvs, theta) 
+       = (substTyVars subst tvs, substTheta subst theta)
+
+    go _ fun [] = return fun
 
-    go fun [] = return fun
+    go True (HsVar fun_id) ((tys,theta) : prs)
+       | want_method_inst theta
+       = do { meth_id <- newMethodWithGivenTy orig fun_id tys
+            ; go False (HsVar meth_id) prs }
+               -- Go round with 'False' to prevent further use
+               -- of newMethod: see Note [Multiple instantiation]
 
-    go fun ((tys, theta) : prs)
-       = do { dicts <- newDicts orig theta
-            ; extendLIEs dicts
-            ; let the_app = unLoc $ mkHsDictApp (mkHsTyApp (noLoc fun) tys)
-                                                (map instToId dicts)
-            ; go the_app prs }
+    go _ fun ((tys, theta) : prs)
+       = do { co_fn <- instCall orig tys theta
+            ; go False (HsWrap co_fn fun) prs }
 
-       --      Hack Alert (want_method_inst)!
        -- See Note [No method sharing]
-       -- If   f :: (%x :: T) => Int -> Int
-       -- Then if we have two separate calls, (f 3, f 4), we cannot
-       -- make a method constraint that then gets shared, thus:
-       --      let m = f %x in (m 3, m 4)
-       -- because that loses the linearity of the constraint.
-       -- The simplest thing to do is never to construct a method constraint
-       -- in the first place that has a linear implicit parameter in it.
-    want_method_inst theta =  not (null theta)                 -- Overloaded
-                          && not (any isLinearPred theta)      -- Not linear
+    want_method_inst theta =  not (null theta) -- Overloaded
                           && not opt_NoMethodSharing
-               -- See Note [No method sharing] below
 \end{code}
 
 Note [Multiple instantiation]
@@ -864,19 +818,45 @@ This gets a bit less sharing, but
        a) it's better for RULEs involving overloaded functions
        b) perhaps fewer separated lambdas
 
+Note [Left to right]
+~~~~~~~~~~~~~~~~~~~~
+tcArgs implements a left-to-right order, which goes beyond what is described in the
+impredicative type inference paper.  In particular, it allows
+       runST $ foo
+where runST :: (forall s. ST s a) -> a
+When typechecking the application of ($)::(a->b) -> a -> b, we first check that
+runST has type (a->b), thereby filling in a=forall s. ST s a.  Then we un-box this type
+before checking foo.  The left-to-right order really helps here.
+
 \begin{code}
 tcArgs :: LHsExpr Name                         -- The function (for error messages)
-       -> [LHsExpr Name] -> [TcSigmaType]      -- Actual arguments and expected arg types
-       -> TcM [LHsExpr TcId]                   -- Resulting args
+       -> [LHsExpr Name]                       -- Actual args
+       -> ArgChecker [LHsExpr TcId]
 
-tcArgs fun args expected_arg_tys
-  = mapM (tcArg fun) (zip3 args expected_arg_tys [1..])
+type ArgChecker results
+   = [TyVar] -> [TcSigmaType]          -- Current instantiation
+   -> [TcSigmaType]                    -- Expected arg types (**before** applying the instantiation)
+   -> TcM ([TcSigmaType], results)     -- Resulting instaniation and args
 
-tcArg :: LHsExpr Name                          -- The function (for error messages)
-       -> (LHsExpr Name, BoxySigmaType, Int)   -- Actual argument and expected arg type
-       -> TcM (LHsExpr TcId)                   -- Resulting argument
-tcArg fun (arg, ty, arg_no) = addErrCtxt (funAppCtxt fun arg arg_no) $
-                             tcPolyExprNC arg ty
+tcArgs fun args qtvs qtys arg_tys
+  = go 1 qtys args arg_tys
+  where
+    go n qtys [] [] = return (qtys, [])
+    go n qtys (arg:args) (arg_ty:arg_tys)
+       = do { arg' <- tcArg fun n arg qtvs qtys arg_ty
+            ; qtys' <- mapM refineBox qtys     -- Exploit new info
+            ; (qtys'', args') <- go (n+1) qtys' args arg_tys
+            ; return (qtys'', arg':args') }
+
+tcArg :: LHsExpr Name                          -- The function
+      -> Int                                   --   and arg number (for error messages)
+      -> LHsExpr Name
+      -> [TyVar] -> [TcSigmaType]              -- Instantiate the arg type like this
+      -> BoxySigmaType
+      -> TcM (LHsExpr TcId)                    -- Resulting argument
+tcArg fun arg_no arg qtvs qtys ty
+  = addErrCtxt (funAppCtxt fun arg arg_no) $
+    tcPolyExprNC arg (substTyWith qtvs qtys ty)
 \end{code}
 
 
@@ -895,20 +875,32 @@ Here's are two cases that should fail
 
 
 \begin{code}
-checkBadTagToEnumCall :: Id -> [TcType] -> TcM ()
-checkBadTagToEnumCall fun_id tys
-  | fun_id `hasKey` tagToEnumKey
+doStupidChecks :: HsExpr TcId
+              -> [([TcType], ThetaType)]
+              -> TcM ()
+-- Check two tiresome and ad-hoc cases
+-- (a) the "stupid theta" for a data con; add the constraints
+--     from the "stupid theta" of a data constructor (sigh)
+-- (b) deal with the tagToEnum# problem: see Note [tagToEnum#]
+
+doStupidChecks (HsVar fun_id) ((tys,_):_)
+  | Just con <- isDataConId_maybe fun_id   -- (a)
+  = addDataConStupidTheta con tys
+
+  | fun_id `hasKey` tagToEnumKey           -- (b)
   = do { tys' <- zonkTcTypes tys
        ; checkTc (ok tys') (tagToEnumError tys')
        }
-  | otherwise    -- Vastly common case
-  = return ()
   where
     ok []      = False
     ok (ty:tys) = case tcSplitTyConApp_maybe ty of
                        Just (tc,_) -> isEnumerationTyCon tc
                        Nothing     -> False
 
+doStupidChecks fun tv_theta_prs
+  = return () -- The common case
+                                     
+
 tagToEnumError tys
   = hang (ptext SLIT("Bad call to tagToEnum#") <+> at_type)
         2 (vcat [ptext SLIT("Specify the type by giving a type signature"),
@@ -925,40 +917,47 @@ tagToEnumError tys
 %************************************************************************
 
 \begin{code}
-lookupFun :: InstOrigin -> Name -> TcM TcId
+lookupFun :: InstOrigin -> Name -> TcM (HsExpr TcId, TcType)
 lookupFun orig id_name
   = do         { thing <- tcLookup id_name
        ; case thing of
-           AGlobal (ADataCon con) -> return (dataConWrapId con)
+           AGlobal (ADataCon con) -> return (HsVar wrap_id, idType wrap_id)
+                                  where
+                                     wrap_id = dataConWrapId con
 
            AGlobal (AnId id) 
                | isNaughtyRecordSelector id -> failWithTc (naughtyRecordSel id)
-               | otherwise                  -> return id
+               | otherwise                  -> return (HsVar id, idType id)
                -- A global cannot possibly be ill-staged
                -- nor does it need the 'lifting' treatment
 
-#ifndef GHCI
-           ATcId id th_level _ -> return id                    -- Non-TH case
-#else
-           ATcId id th_level _ -> do { use_stage <- getStage   -- TH case
-                                     ; thLocalId orig id_name id th_level use_stage }
-#endif
+           ATcId { tct_id = id, tct_type = ty, tct_co = mb_co, tct_level = lvl }
+               -> do { thLocalId orig id ty lvl
+                     ; case mb_co of
+                         Nothing -> return (HsVar id, ty)      -- Wobbly, or no free vars
+                         Just co -> return (mkHsWrap co (HsVar id), ty) }      
 
            other -> failWithTc (ppr other <+> ptext SLIT("used where a value identifer was expected"))
     }
 
-#ifdef GHCI  /* GHCI and TH is on */
+#ifndef GHCI  /* GHCI and TH is off */
 --------------------------------------
 -- thLocalId : Check for cross-stage lifting
-thLocalId orig id_name id th_bind_lvl (Brack use_lvl ps_var lie_var)
-  | use_lvl > th_bind_lvl
-  = thBrackId orig id_name id ps_var lie_var
-thLocalId orig id_name id th_bind_lvl use_stage
-  = do { checkWellStaged (quotes (ppr id)) th_bind_lvl use_stage
-       ; return id }
+thLocalId orig id id_ty th_bind_lvl
+  = return ()
+
+#else        /* GHCI and TH is on */
+thLocalId orig id id_ty th_bind_lvl 
+  = do { use_stage <- getStage -- TH case
+       ; case use_stage of
+           Brack use_lvl ps_var lie_var | use_lvl > th_bind_lvl
+                 -> thBrackId orig id ps_var lie_var
+           other -> do { checkWellStaged (quotes (ppr id)) th_bind_lvl use_stage
+                       ; return id }
+       }
 
 --------------------------------------
-thBrackId orig id_name id ps_var lie_var
+thBrackId orig id ps_var lie_var
   | isExternalName id_name
   =    -- Top-level identifiers in this module,
        -- (which have External Names)
@@ -1005,6 +1004,8 @@ thBrackId orig id_name id ps_var lie_var
        ; writeMutVar ps_var ((id_name, nlHsApp (nlHsVar lift) (nlHsVar id)) : ps)
 
        ; return id } }
+ where
+   id_name = idName id
 #endif /* GHCI */
 \end{code}
 
@@ -1048,7 +1049,7 @@ tcRecordBinds data_con arg_tys rbinds
       | Just field_ty <- assocMaybe flds_w_tys field_lbl
       = addErrCtxt (fieldCtxt field_lbl)       $
        do { rhs'   <- tcPolyExprNC rhs field_ty
-          ; sel_id <- tcLookupId field_lbl
+          ; sel_id <- tcLookupField field_lbl
           ; ASSERT( isRecordSelector sel_id )
             return (Just (L loc sel_id, rhs')) }
       | otherwise