-tcBody :: Message -> LHsExpr Name -> BoxyRhoType -> TcM (LHsExpr TcId)
-tcBody ctxt body res_ty
- = -- addErrCtxt ctxt $ -- This context adds little that is useful
- tcPolyExpr body res_ty
+tcBody :: LHsExpr Name -> (Refinement, BoxyRhoType) -> TcM (LHsExpr TcId)
+tcBody body (reft, res_ty)
+ = do { traceTc (text "tcBody" <+> ppr res_ty <+> ppr reft)
+ ; let (co, res_ty') = refineResType reft res_ty
+ ; body' <- tcPolyExpr body res_ty'
+ ; return (mkLHsCoerce co body') }