+\subsection{Subsumption}
+%* *
+%************************************************************************
+
+All the tcSub calls have the form
+
+ tcSub expected_ty offered_ty
+which checks
+ offered_ty <= expected_ty
+
+That is, that a value of type offered_ty is acceptable in
+a place expecting a value of type expected_ty.
+
+It returns a coercion function
+ co_fn :: offered_ty -> expected_ty
+which takes an HsExpr of type offered_ty into one of type
+expected_ty.
+
+\begin{code}
+-----------------------
+-- tcSubExp is used for expressions
+tcSubExp :: Expected TcRhoType -> TcRhoType -> TcM ExprCoFn
+
+tcSubExp (Infer hole) offered_ty
+ = do { offered' <- zonkTcType offered_ty
+ -- Note [Zonk return type]
+ -- zonk to take advantage of the current GADT type refinement.
+ -- If we don't we get spurious "existential type variable escapes":
+ -- case (x::Maybe a) of
+ -- Just b (y::b) -> y
+ -- We need the refinement [b->a] to be applied to the result type
+ ; writeMutVar hole offered'
+ ; return idCoercion }
+
+tcSubExp (Check expected_ty) offered_ty
+ = tcSub expected_ty offered_ty
+
+-----------------------
+-- tcSubPat is used for patterns
+tcSubPat :: TcSigmaType -- Pattern type signature
+ -> Expected TcSigmaType -- Type from context
+ -> TcM ()
+-- In patterns we insist on an exact match; hence no CoFn returned
+-- See Note [Pattern coercions] in TcPat
+-- However, we can't call unify directly, because both types might be
+-- polymorphic; hence the call to tcSub, followed by a check for
+-- the identity coercion
+
+tcSubPat sig_ty (Infer hole)
+ = do { sig_ty' <- zonkTcType sig_ty
+ ; writeMutVar hole sig_ty' -- See notes with tcSubExp above
+ ; return () }
+
+tcSubPat sig_ty (Check exp_ty)
+ = do { co_fn <- tcSub sig_ty exp_ty
+
+ ; if isIdCoercion co_fn then
+ return ()
+ else
+ unifyMisMatch sig_ty exp_ty }
+\end{code}
+
+
+
+%************************************************************************
+%* *
+ tcSub: main subsumption-check code
+%* *
+%************************************************************************
+
+No holes expected now. Add some error-check context info.
+
+\begin{code}
+-----------------
+tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn -- Locally used only
+ -- tcSub exp act checks that
+ -- act <= exp
+tcSub expected_ty actual_ty
+ = traceTc (text "tcSub" <+> details) `thenM_`
+ addErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
+ (tc_sub expected_ty expected_ty actual_ty actual_ty)
+ where
+ details = vcat [text "Expected:" <+> ppr expected_ty,
+ text "Actual: " <+> ppr actual_ty]
+
+-----------------
+tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms
+ -> TcSigmaType -- ..and after
+ -> TcSigmaType -- actual_ty, before
+ -> TcSigmaType -- ..and after
+ -> TcM ExprCoFn
+
+-----------------------------------
+-- Expand synonyms
+tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
+tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
+
+-----------------------------------
+-- Generalisation case
+-- actual_ty: d:Eq b => b->b
+-- expected_ty: forall a. Ord a => a->a
+-- co_fn e /\a. \d2:Ord a. let d = eqFromOrd d2 in e
+
+-- It is essential to do this *before* the specialisation case
+-- Example: f :: (Eq a => a->a) -> ...
+-- g :: Ord b => b->b
+-- Consider f g !
+
+tc_sub exp_sty expected_ty act_sty actual_ty
+ | isSigmaTy expected_ty
+ = tcGen expected_ty (tyVarsOfType actual_ty) (
+ -- It's really important to check for escape wrt the free vars of
+ -- both expected_ty *and* actual_ty
+ \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
+ ) `thenM` \ (gen_fn, co_fn) ->
+ returnM (gen_fn <.> co_fn)
+
+-----------------------------------
+-- Specialisation case:
+-- actual_ty: forall a. Ord a => a->a
+-- expected_ty: Int -> Int
+-- co_fn e = e Int dOrdInt
+
+tc_sub exp_sty expected_ty act_sty actual_ty
+ | isSigmaTy actual_ty
+ = tcInstCall InstSigOrigin actual_ty `thenM` \ (inst_fn, _, body_ty) ->
+ tc_sub exp_sty expected_ty body_ty body_ty `thenM` \ co_fn ->
+ returnM (co_fn <.> inst_fn)
+
+-----------------------------------
+-- Function case
+
+tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
+ = tcSub_fun exp_arg exp_res act_arg act_res
+
+-----------------------------------
+-- Type variable meets function: imitate
+--
+-- NB 1: we can't just unify the type variable with the type
+-- because the type might not be a tau-type, and we aren't
+-- allowed to instantiate an ordinary type variable with
+-- a sigma-type
+--
+-- NB 2: can we short-cut to an error case?
+-- when the arg/res is not a tau-type?
+-- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int
+-- then x = (f,f)
+-- is perfectly fine, because we can instantiate f's type to a monotype
+--
+-- However, we get can get jolly unhelpful error messages.
+-- e.g. foo = id runST
+--
+-- Inferred type is less polymorphic than expected
+-- Quantified type variable `s' escapes
+-- Expected type: ST s a -> t
+-- Inferred type: (forall s1. ST s1 a) -> a
+-- In the first argument of `id', namely `runST'
+-- In a right-hand side of function `foo': id runST
+--
+-- I'm not quite sure what to do about this!
+
+tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ act_ty
+ = do { ([act_arg], act_res) <- unifyFunTys 1 act_ty
+ ; tcSub_fun exp_arg exp_res act_arg act_res }
+
+tc_sub _ exp_ty act_sty act_ty@(FunTy act_arg act_res)
+ = do { ([exp_arg], exp_res) <- unifyFunTys 1 exp_ty
+ ; tcSub_fun exp_arg exp_res act_arg act_res }
+
+-----------------------------------
+-- Unification case
+-- If none of the above match, we revert to the plain unifier
+tc_sub exp_sty expected_ty act_sty actual_ty
+ = uTys True exp_sty expected_ty True act_sty actual_ty `thenM_`
+ returnM idCoercion
+\end{code}
+
+\begin{code}
+tcSub_fun exp_arg exp_res act_arg act_res
+ = tc_sub act_arg act_arg exp_arg exp_arg `thenM` \ co_fn_arg ->
+ tc_sub exp_res exp_res act_res act_res `thenM` \ co_fn_res ->
+ newUnique `thenM` \ uniq ->
+ let
+ -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
+ -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
+ -- co_fn :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
+ arg_id = mkSysLocal FSLIT("sub") uniq exp_arg
+ coercion | isIdCoercion co_fn_arg,
+ isIdCoercion co_fn_res = idCoercion
+ | otherwise = mkCoercion co_fn
+
+ co_fn e = DictLam [arg_id]
+ (noLoc (co_fn_res <$> (HsApp (noLoc e) (noLoc (co_fn_arg <$> HsVar arg_id)))))
+ -- Slight hack; using a "DictLam" to get an ordinary simple lambda
+ -- HsVar arg_id :: HsExpr exp_arg
+ -- co_fn_arg $it :: HsExpr act_arg
+ -- HsApp e $it :: HsExpr act_res
+ -- co_fn_res $it :: HsExpr exp_res
+ in
+ returnM coercion
+\end{code}
+
+
+%************************************************************************
+%* *
+\subsection{Generalisation}
+%* *
+%************************************************************************
+
+\begin{code}
+tcGen :: TcSigmaType -- expected_ty
+ -> TcTyVarSet -- Extra tyvars that the universally
+ -- quantified tyvars of expected_ty
+ -- must not be unified
+ -> (TcRhoType -> TcM result) -- spec_ty
+ -> TcM (ExprCoFn, result)
+ -- The expression has type: spec_ty -> expected_ty
+
+tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
+ -- If not, the call is a no-op
+ = do { -- We want the GenSkol info in the skolemised type variables to
+ -- mention the *instantiated* tyvar names, so that we get a
+ -- good error message "Rigid variable 'a' is bound by (forall a. a->a)"
+ -- Hence the tiresome but innocuous fixM
+ ((forall_tvs, theta, rho_ty), skol_info) <- fixM (\ ~(_, skol_info) ->
+ do { (forall_tvs, theta, rho_ty) <- tcSkolType skol_info expected_ty
+ ; span <- getSrcSpanM
+ ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) span
+ ; return ((forall_tvs, theta, rho_ty), skol_info) })
+
+#ifdef DEBUG
+ ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
+ text "expected_ty" <+> ppr expected_ty,
+ text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr rho_ty,
+ text "free_tvs" <+> ppr free_tvs,
+ text "forall_tvs" <+> ppr forall_tvs])
+#endif
+
+ -- Type-check the arg and unify with poly type
+ ; (result, lie) <- getLIE (thing_inside rho_ty)
+
+ -- Check that the "forall_tvs" havn't been constrained
+ -- The interesting bit here is that we must include the free variables
+ -- of the expected_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_ty in the
+ -- list of "free vars" for the signature check.
+
+ ; dicts <- newDicts (SigOrigin skol_info) theta
+ ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie
+
+ ; checkSigTyVarsWrt free_tvs forall_tvs
+ ; traceTc (text "tcGen:done")
+
+ ; 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.
+ dict_ids = map instToId dicts
+ co_fn e = TyLam forall_tvs (mkHsDictLam dict_ids (mkHsLet inst_binds (noLoc e)))
+ ; returnM (mkCoercion co_fn, result) }
+ where
+ free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
+ sig_msg = ptext SLIT("expected type of an expression")
+\end{code}
+
+
+
+%************************************************************************
+%* *