+---------------------------
+tcApp :: HsExpr Name -- Function
+ -> Arity -- Number of args reqd
+ -> ([BoxySigmaType] -> TcM arg_results) -- Argument type-checker
+ -> BoxyRhoType -- Result type
+ -> TcM (HsExpr TcId, arg_results)
+
+-- (tcFun fun n_args arg_checker res_ty)
+-- The argument type checker, arg_checker, will be passed exactly n_args types
+
+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 n_args
+ ; fun' <- tcExpr fun (mkFunTys (mkTyVarTys arg_boxes) res_ty)
+ ; arg_tys' <- mapM readFilledBox arg_boxes
+ ; args' <- arg_checker arg_tys'
+ ; 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
+ -> BoxyRhoType -- Result type
+ -> TcM (HsExpr TcId, arg_results)
+
+-- Call (f e1 ... en) :: res_ty
+-- Type f :: forall a b c. theta => fa_1 -> ... -> fa_k -> fres
+-- (where k <= n; fres has the rest)
+-- NB: if k < n then the function doesn't have enough args, and
+-- presumably fres is a type variable that we are going to
+-- instantiate with a function type
+--
+-- 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
+
+ -- Split up the function type
+ ; let (tv_theta_prs, rho) = tcMultiSplitSigmaTy (idType fun_id)
+ (fun_arg_tys, fun_res_ty) = tcSplitFunTysN rho n_args
+
+ qtvs = concatMap fst tv_theta_prs -- Quantified tyvars
+ arg_qtvs = exactTyVarsOfTypes fun_arg_tys
+ res_qtvs = exactTyVarsOfType fun_res_ty
+ -- NB: exactTyVarsOfType. See Note [Silly type synonyms in smart-app]
+ tau_qtvs = arg_qtvs `unionVarSet` res_qtvs
+ k = length fun_arg_tys -- k <= n_args
+ n_missing_args = n_args - k -- Always >= 0
+
+ -- Match the result type of the function with the
+ -- result type of the context, to get an inital substitution
+ ; extra_arg_boxes <- newBoxyTyVars n_missing_args
+ ; let extra_arg_tys' = mkTyVarTys extra_arg_boxes
+ res_ty' = mkFunTys extra_arg_tys' res_ty
+ subst = boxySubMatchType arg_qtvs fun_res_ty res_ty'
+ -- Only bind arg_qtvs, since only they will be
+ -- *definitely* be filled in by arg_checker
+ -- E.g. error :: forall a. String -> a
+ -- (error "foo") :: bx5
+ -- Don't make subst [a |-> bx5]
+ -- because then the result subsumption becomes
+ -- bx5 ~ bx5
+ -- and the unifer doesn't expect the
+ -- same box on both sides
+ inst_qtv tv | Just boxy_ty <- lookupTyVar subst tv = return boxy_ty
+ | tv `elemVarSet` tau_qtvs = do { tv' <- tcInstBoxyTyVar tv
+ ; return (mkTyVarTy tv') }
+ | otherwise = do { tv' <- tcInstTyVar tv
+ ; return (mkTyVarTy tv') }
+ -- The 'otherwise' case handles type variables that are
+ -- mentioned only in the constraints, not in argument or
+ -- result types. We'll make them tau-types
+
+ ; qtys' <- mapM inst_qtv qtvs
+ ; 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')
+
+ ; 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
+ ; let res_subst = zipOpenTvSubst qtvs qtys''
+ fun_res_ty'' = substTy res_subst fun_res_ty
+ res_ty'' = mkFunTys extra_arg_tys'' res_ty
+ ; co_fn <- addErrCtxtM (checkFunResCtxt fun_name res_ty fun_res_ty'') $
+ tcSubExp fun_res_ty'' 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') }
+\end{code}
+
+Note [Silly type synonyms in smart-app]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we call sripBoxyType, all of the boxes should be filled
+in. But we need to be careful about type synonyms:
+ type T a = Int
+ f :: T a -> Int
+ ...(f x)...
+In the call (f x) we'll typecheck x, expecting it to have type
+(T box). Usually that would fill in the box, but in this case not;
+because 'a' is discarded by the silly type synonym T. So we must
+use exactTyVarsOfType to figure out which type variables are free
+in the argument type.
+
+\begin{code}
+-- tcId is a specialisation of tcIdApp when there are no arguments
+-- tcId f ty = do { (res, _) <- tcIdApp f [] (\[] -> return ()) ty
+-- ; return res }
+
+tcId :: InstOrigin
+ -> Name -- Function
+ -> BoxyRhoType -- Result type
+ -> 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
+
+ -- Split up the function type
+ ; let (tv_theta_prs, fun_tau) = tcMultiSplitSigmaTy (idType fun_id)
+ qtvs = concatMap fst tv_theta_prs -- Quantified tyvars
+ tau_qtvs = exactTyVarsOfType fun_tau -- Mentiond in the tau part
+ inst_qtv tv | tv `elemVarSet` tau_qtvs = do { tv' <- tcInstBoxyTyVar tv
+ ; return (mkTyVarTy tv') }
+ | otherwise = do { tv' <- tcInstTyVar tv
+ ; return (mkTyVarTy tv') }
+
+ -- Do the subsumption check wrt the result type
+ ; qtv_tys <- mapM inst_qtv qtvs
+ ; let res_subst = zipTopTvSubst qtvs qtv_tys
+ fun_tau' = substTy res_subst fun_tau
+
+ ; co_fn <- addErrCtxtM (checkFunResCtxt fun_name res_ty fun_tau') $
+ tcSubExp fun_tau' res_ty
+
+ -- And pack up the results
+ ; fun' <- instFun fun_id qtvs qtv_tys tv_theta_prs
+ ; return (mkHsCoerce co_fn fun') }
+
+-- Note [Push result type in]
+--
+-- Unify with expected result before (was: after) type-checking the args
+-- so that the info from res_ty (was: args) percolates to args (was actual_res_ty).
+-- This is when we might detect a too-few args situation.
+-- (One can think of cases when the opposite order would give
+-- a better error message.)
+-- [March 2003: I'm experimenting with putting this first. Here's an
+-- example where it actually makes a real difference
+-- class C t a b | t a -> b
+-- instance C Char a Bool
+--
+-- data P t a = forall b. (C t a b) => MkP b
+-- data Q t = MkQ (forall a. P t a)
+
+-- f1, f2 :: Q Char;
+-- f1 = MkQ (MkP True)
+-- f2 = MkQ (MkP True :: forall a. P Char a)
+--
+-- With the change, f1 will type-check, because the 'Char' info from
+-- the signature is propagated into MkQ's argument. With the check
+-- in the other order, the extra signature in f2 is reqd.]
+
+---------------------------
+tcSyntaxOp :: InstOrigin -> HsExpr Name -> TcType -> TcM (HsExpr TcId)
+-- Typecheck a syntax operator, checking that it has the specified type
+-- The operator is always a variable at this stage (i.e. renamer output)
+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
+ -> 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 { 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)
+
+ -- 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'
+ }
+ where
+ orig = OccurrenceOf (idName fun_id)