-tcApp :: RenamedHsExpr -> [RenamedHsExpr] -- Function and args
- -> Expected TcRhoType -- Expected result type of application
- -> TcM TcExpr -- Translated fun and args
-
-tcApp (HsApp e1 e2) args res_ty
- = tcApp e1 (e2:args) res_ty -- Accumulate the arguments
-
-tcApp fun args res_ty
- = -- First type-check the function
- tcInferRho fun `thenM` \ (fun', fun_ty) ->
-
- addErrCtxt (wrongArgsCtxt "too many" fun args) (
- traceTc (text "tcApp" <+> (ppr fun $$ ppr fun_ty)) `thenM_`
- split_fun_ty fun_ty (length args)
- ) `thenM` \ (expected_arg_tys, actual_result_ty) ->
-
- -- 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_result_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.]
+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)
+
+ go fun [] = return fun
+
+ 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 }
+
+ -- 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
+ && not opt_NoMethodSharing
+ -- See Note [No method sharing] below
+\end{code}
+
+Note [Multiple instantiation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We are careful never to make a MethodInst that has, as its meth_id, another MethodInst.
+For example, consider
+ f :: forall a. Eq a => forall b. Ord b => a -> b
+At a call to f, at say [Int, Bool], it's tempting to translate the call to
+
+ f_m1
+ where
+ f_m1 :: forall b. Ord b => Int -> b
+ f_m1 = f Int dEqInt