+tcExpr :: RenamedHsExpr -- Expession to type check
+ -> TcType -- Expected type (could be a polytpye)
+ -> TcM s (TcExpr, LIE)
+
+tcExpr expr ty | isForAllTy ty = -- Polymorphic case
+ tcPolyExpr expr ty `thenTc` \ (expr', lie, _, _, _) ->
+ returnTc (expr', lie)
+
+ | otherwise = -- Monomorphic case
+ tcMonoExpr expr ty
+\end{code}
+
+
+%************************************************************************
+%* *
+\subsection{@tcPolyExpr@ typchecks an application}
+%* *
+%************************************************************************
+
+\begin{code}
+-- tcPolyExpr is like tcMonoExpr, except that the expected type
+-- can be a polymorphic one.
+tcPolyExpr :: RenamedHsExpr
+ -> TcType -- Expected type
+ -> TcM s (TcExpr, LIE, -- Generalised expr with expected type, and LIE
+ TcExpr, TcTauType, LIE) -- Same thing, but instantiated; tau-type returned
+
+tcPolyExpr arg expected_arg_ty
+ = -- Ha! The argument type of the function is a for-all type,
+ -- An example of rank-2 polymorphism.
+
+ -- To ensure that the forall'd type variables don't get unified with each
+ -- other or any other types, we make fresh copy of the alleged type
+ tcInstTcType expected_arg_ty `thenNF_Tc` \ (sig_tyvars, sig_rho) ->
+ let
+ (sig_theta, sig_tau) = splitRhoTy sig_rho
+ in
+ -- Type-check the arg and unify with expected type
+ tcMonoExpr arg sig_tau `thenTc` \ (arg', lie_arg) ->
+
+ -- Check that the sig_tyvars havn't been constrained
+ -- The interesting bit here is that we must include the free variables
+ -- of the expected arg ty. Here's an example:
+ -- runST (newVar True)
+ -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
+ -- for (newVar True), with s fresh. Then we unify with the runST's arg type
+ -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
+ -- So now s' isn't unconstrained because it's linked to a.
+ -- Conclusion: include the free vars of the expected arg type in the
+ -- list of "free vars" for the signature check.
+
+ tcExtendGlobalTyVars (tyVarsOfType expected_arg_ty) $
+ tcAddErrCtxtM (sigCtxt sig_msg expected_arg_ty) $
+
+ checkSigTyVars sig_tyvars `thenTc` \ zonked_sig_tyvars ->
+
+ newDicts SignatureOrigin sig_theta `thenNF_Tc` \ (sig_dicts, dict_ids) ->
+ -- ToDo: better origin
+ tcSimplifyAndCheck
+ (text "the type signature of an expression")
+ (mkVarSet zonked_sig_tyvars)
+ sig_dicts lie_arg `thenTc` \ (free_insts, inst_binds) ->
+
+ let
+ -- This HsLet binds any Insts which came out of the simplification.
+ -- It's a bit out of place here, but using AbsBind involves inventing
+ -- a couple of new names which seems worse.
+ generalised_arg = TyLam zonked_sig_tyvars $
+ DictLam dict_ids $
+ mkHsLet inst_binds $
+ arg'
+ in
+ returnTc ( generalised_arg, free_insts,
+ arg', sig_tau, lie_arg )
+ where
+ sig_msg ty = sep [ptext SLIT("In an expression with expected type:"),
+ nest 4 (ppr ty)]