+---------------------------
+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 (replicate n_args argTypeKind)
+ ; 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 (replicate n_missing_args argTypeKind)
+ ; 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 <- tcFunResTy fun_name 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}