add crude Monad type class

diff --git a/src/General.v b/src/General.v
index 3c82528..7e0af43 100644 (file)
--- a/src/General.v
+++ b/src/General.v
@@ -633,6 +633,12 @@ Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
 Variable eol : string.
 Extract Constant eol  => "'\n':[]".
 
+Class Monad {T:Type->Type} :=
+{ returnM : forall {a},     a -> T a
+; bindM   : forall {a}{b},  T a -> (a -> T b) -> T b
+}.
+Implicit Arguments Monad [ ].
+Notation "a >>>= b" := (@bindM _ _ _ _ a b) (at level 50, left associativity).
 
 (* the Error monad *)
 Inductive OrError (T:Type) :=
@@ -709,3 +715,5 @@ Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(
     rewrite e in v; apply OK; apply v.
     apply (Error (error_message (length l) n)).
     Defined.
+
+

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index c4bd768..055d588 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -218,9 +218,8 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
         | WCoerVar _  => Error "found a coercion variable in a case"
         | WExprVar ev => 
         coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
-        coreExprToWeakExpr e >>= fun e' =>
           expectTyConApp te' nil >>= fun tca =>
-            let (tc,lt) := tca in
+            let (tc,lt) := tca:(TyCon * list WeakType) in
           ((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar)))
                 : ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
             match branches with