Make do-notation a bit more flexible (Trac #1537)
authorsimonpj@microsoft.com <unknown>
Tue, 5 Feb 2008 16:48:16 +0000 (16:48 +0000)
committersimonpj@microsoft.com <unknown>
Tue, 5 Feb 2008 16:48:16 +0000 (16:48 +0000)
This is a second attempt to fix #1537: to make the static typechecking
of do-notation behave just like the desugared version of the same thing.
This should allow parameterised monads to work properly (see Oleg's comment
in the above ticket).

We can probably merge to 6.8.3 if it goes smoothly.

Incidentally, the resulting setup suffers from greater type ambiguity
if (>>=) has a very general type.  So test rebindable6 no longer works
(at least not without more type signatures), and rebindable5 requires
extra functional dependencies.  But they are weird tests.

compiler/deSugar/DsExpr.lhs
compiler/typecheck/TcMatches.lhs

index 5191afe..f4f2c56 100644 (file)
@@ -548,13 +548,15 @@ dsDo stmts body result_ty
 
     go (BindStmt pat rhs bind_op fail_op : stmts)
       = 
-       do { body  <- go stmts
+       do  { body     <- go stmts
+           ; rhs'     <- dsLExpr rhs
+          ; bind_op' <- dsExpr bind_op
           ; var   <- selectSimpleMatchVarL pat
+          ; let bind_ty = exprType bind_op'    -- rhs -> (pat -> res1) -> res2
+                res1_ty = funResultTy (funArgTy (funResultTy bind_ty))
           ; match <- matchSinglePat (Var var) (StmtCtxt DoExpr) pat
-                                 result_ty (cantFailMatchResult body)
+                                    res1_ty (cantFailMatchResult body)
           ; match_code <- handle_failure pat match fail_op
-           ; rhs'       <- dsLExpr rhs
-          ; bind_op'   <- dsExpr bind_op
           ; return (mkApps bind_op' [rhs', Lam var match_code]) }
     
     -- In a do expression, pattern-match failure just calls
index 6fdbd66..f02b74a 100644 (file)
@@ -467,7 +467,7 @@ tcLcStmt m_tc ctxt stmt elt_ty thing_inside
 
 tcDoStmt :: TcStmtChecker
 
-tcDoStmt ctxt (BindStmt pat rhs bind_op fail_op) reft_res_ty@(_,res_ty) thing_inside
+tcDoStmt ctxt (BindStmt pat rhs bind_op fail_op) (reft,res_ty) thing_inside
   = do { (rhs', rhs_ty) <- tcInferRho rhs
                -- We should use type *inference* for the RHS computations, becuase of GADTs. 
                --      do { pat <- rhs; <rest> }
@@ -476,31 +476,37 @@ tcDoStmt ctxt (BindStmt pat rhs bind_op fail_op) reft_res_ty@(_,res_ty) thing_in
                -- We do inference on rhs, so that information about its type can be refined
                -- when type-checking the pattern. 
 
-       -- Deal with rebindable syntax; (>>=) :: rhs_ty -> (a -> res_ty) -> res_ty
-       ; (bind_op', pat_ty) <- 
+       -- Deal with rebindable syntax:
+       --       (>>=) :: rhs_ty -> (pat_ty -> new_res_ty) -> res_ty
+       -- This level of generality is needed for using do-notation
+       -- in full generality; see Trac #1537
+       ; ((bind_op', new_res_ty), pat_ty) <- 
             withBox liftedTypeKind $ \ pat_ty ->
+            withBox liftedTypeKind $ \ new_res_ty ->
             tcSyntaxOp DoOrigin bind_op 
-                       (mkFunTys [rhs_ty, mkFunTy pat_ty res_ty] res_ty)
+                       (mkFunTys [rhs_ty, mkFunTy pat_ty new_res_ty] res_ty)
 
                -- If (but only if) the pattern can fail, 
                -- typecheck the 'fail' operator
        ; fail_op' <- if isIrrefutableHsPat pat 
                      then return noSyntaxExpr
-                     else tcSyntaxOp DoOrigin fail_op (mkFunTy stringTy res_ty)
+                     else tcSyntaxOp DoOrigin fail_op (mkFunTy stringTy new_res_ty)
 
-       ; (pat', thing) <- tcLamPat pat pat_ty reft_res_ty thing_inside
+       ; (pat', thing) <- tcLamPat pat pat_ty (reft, new_res_ty) thing_inside
 
        ; return (BindStmt pat' rhs' bind_op' fail_op', thing) }
 
 
-tcDoStmt ctxt (ExprStmt rhs then_op _) reft_res_ty@(_,res_ty) thing_inside
+tcDoStmt ctxt (ExprStmt rhs then_op _) (reft,res_ty) thing_inside
   = do { (rhs', rhs_ty) <- tcInferRho rhs
 
-       -- Deal with rebindable syntax; (>>) :: rhs_ty -> res_ty -> res_ty
-       ; then_op' <- tcSyntaxOp DoOrigin then_op 
-                                (mkFunTys [rhs_ty, res_ty] res_ty)
+       -- Deal with rebindable syntax; (>>) :: rhs_ty -> new_res_ty -> res_ty
+       ; (then_op', new_res_ty) <-
+               withBox liftedTypeKind $ \ new_res_ty ->
+               tcSyntaxOp DoOrigin then_op 
+                          (mkFunTys [rhs_ty, new_res_ty] res_ty)
 
-       ; thing <- thing_inside reft_res_ty
+       ; thing <- thing_inside (reft, new_res_ty)
        ; return (ExprStmt rhs' then_op' rhs_ty, thing) }
 
 tcDoStmt ctxt stmt res_ty thing_inside