+\subsection{Subsumption}
+%* *
+%************************************************************************
+
+Example:
+ f :: (forall a. a->a) -> Int -> Int
+ f (g::Int->Int) y = g y
+This is ok: the type signature allows fewer callers than
+the (more general) signature f :: (Int->Int) -> Int -> Int
+I.e. (forall a. a->a) <= Int -> Int
+We end up translating this to:
+ f = \g' :: (forall a. a->a). let g = g' Int in g' y
+
+tcSubPat does the work
+ sig_ty is the signature on the pattern itself
+ (Int->Int in the example)
+ expected_ty is the type passed inwards from the context
+ (forall a. a->a in the example)
+
+\begin{code}
+tcSubPat :: TcSigmaType -> TcHoleType -> TcM (PatCoFn, LIE)
+
+tcSubPat sig_ty exp_ty
+ = tcSubOff sig_ty exp_ty `thenTc` \ (co_fn, lie) ->
+ -- co_fn is a coercion on *expressions*, and we
+ -- need to make a coercion on *patterns*
+ if isIdCoercion co_fn then
+ ASSERT( isEmptyLIE lie )
+ returnNF_Tc (idCoercion, emptyLIE)
+ else
+ tcGetUnique `thenNF_Tc` \ uniq ->
+ let
+ arg_id = mkSysLocal FSLIT("sub") uniq exp_ty
+ the_fn = DictLam [arg_id] (co_fn <$> HsVar arg_id)
+ pat_co_fn p = SigPat p exp_ty the_fn
+ in
+ returnNF_Tc (mkCoercion pat_co_fn, lie)
+\end{code}
+
+
+%************************************************************************
+%* *