+tcGuardedCmd :: CmdEnv -> LHsExpr Name -> CmdStack
+ -> (Refinement, TcTauType) -> TcM (LHsExpr TcId)
+-- A wrapper that deals with the refinement (if any)
+tcGuardedCmd env expr stk (reft, res_ty)
+ = do { let (co, res_ty') = refineResType reft res_ty
+ ; body <- tcCmd env expr (stk, res_ty')
+ ; return (mkLHsCoerce co body) }
+