now since the type checking monad TcM is nondeterministic we can use the same monad in PGF.Forest.getAbsTrees

3 files changed, 166 insertions, 141 deletions

diff --git a/src/runtime/haskell/PGF/Forest.hs b/src/runtime/haskell/PGF/Forest.hs
index a843e7e1d..54204cabb 100644
--- a/src/runtime/haskell/PGF/Forest.hs
+++ b/src/runtime/haskell/PGF/Forest.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE TypeSynonymInstances #-}

+

 -------------------------------------------------

 -- |

 -- Module      : PGF

@@ -29,6 +31,7 @@ import qualified Data.Map as Map
 import qualified Data.IntSet as IntSet

 import qualified Data.IntMap as IntMap

 import Control.Monad

+import Control.Monad.State

 import GF.Data.SortedList

 

 data Forest

@@ -114,41 +117,39 @@ isLindefCId id
 -- the same as the startup category.

 getAbsTrees :: Forest -> PArg -> Maybe Type -> Either [(FId,TcError)] [Expr]

 getAbsTrees (Forest abs cnc forest root) arg@(PArg _ fid) ty =

-  let (res,err) = unTcFM (do e <- go Set.empty emptyScope arg (fmap (TTyp []) ty)

-                             e <- runTcM abs fid (refineExpr e)

-                             runTcM abs fid (checkResolvedMetaStore emptyScope e)

-                             return e) IntMap.empty

+  let (err,res) = runTcM abs (do e <- go Set.empty emptyScope (fmap (TTyp []) ty) arg

+                                 e <- refineExpr e

+                                 checkResolvedMetaStore emptyScope e

+                                 return e) fid IntMap.empty

   in if null res

        then Left  (nub err)

-       else Right (nubsort (map snd res))

+       else Right (nubsort [e | (_,_,e) <- res])

   where

-    go rec_ scope_ (PArg hypos fid) mb_tty_

+    go rec_ scope_ mb_tty_ (PArg hypos fid)

       | fid < totalCats cnc = case mb_tty of

-                                Just tty -> do i <- runTcM abs fid (newMeta scope tty)

+                                Just tty -> do i <- newMeta scope tty

                                                return (mkAbs (EMeta i))

                                 Nothing  -> mzero

       | Set.member fid rec_ = mzero

       | otherwise           = foldForest (\funid args trees ->

                                                   do let CncFun fn lins = cncfuns cnc ! funid

                                                      case isLindefCId fn of

-                                                       Just _  -> do arg <- go (Set.insert fid rec_) scope (head args) mb_tty

+                                                       Just _  -> do arg <- bracket (go (Set.insert fid rec_) scope mb_tty) arg

                                                                      return (mkAbs arg)

-                                                       Nothing -> do ty_fn <- runTcM abs fid (lookupFunType fn)

+                                                       Nothing -> do ty_fn <- lookupFunType fn

                                                                      (e,tty0) <- foldM (\(e1,tty) arg -> goArg (Set.insert fid rec_) scope fid e1 arg tty)

                                                                                        (EFun fn,TTyp [] ty_fn) args

                                                                      case mb_tty of

-                                                                       Just tty -> runTcM abs fid $ do

-                                                                                     i <- newGuardedMeta e

-                                                                                     eqType scope (scopeSize scope) i tty tty0

+                                                                       Just tty -> do i <- newGuardedMeta e

+                                                                                      eqType scope (scopeSize scope) i tty tty0

                                                                        Nothing  -> return ()

                                                                      return (mkAbs e)

                                                   `mplus`

                                                   trees)

                                          (\const _ trees -> do

-                                                  const <- runTcM abs fid $

-                                                             case mb_tty of

-                                                               Just tty ->            tcExpr  scope const tty

-                                                               Nothing  -> fmap fst $ infExpr scope const

+                                                  const <- case mb_tty of

+                                                             Just tty ->            tcExpr  scope const tty

+                                                             Nothing  -> fmap fst $ infExpr scope const

                                                   return (mkAbs const)

                                                   `mplus`

                                                   trees)

@@ -157,13 +158,13 @@ getAbsTrees (Forest abs cnc forest root) arg@(PArg _ fid) ty =
         (scope,mkAbs,mb_tty) = updateScope hypos scope_ id mb_tty_

 

     goArg rec_ scope fid e1 arg (TTyp delta (DTyp ((bt,x,ty):hs) c es)) = do

-      e2' <- go rec_ scope arg (Just (TTyp delta ty))

+      e2' <- bracket (go rec_ scope (Just (TTyp delta ty))) arg

       let e2 = case bt of

                  Explicit -> e2'

                  Implicit -> EImplArg e2'

       if x == wildCId

         then return (EApp e1 e2,TTyp delta (DTyp hs c es))

-        else do v2 <- runTcM abs fid (eval (scopeEnv scope) e2')

+        else do v2 <- eval (scopeEnv scope) e2'

                 return (EApp e1 e2,TTyp (v2:delta) (DTyp hs c es))

 

     updateScope []              scope mkAbs mb_tty = (scope,mkAbs,mb_tty)

@@ -181,31 +182,15 @@ getAbsTrees (Forest abs cnc forest root) arg@(PArg _ fid) ty =
       where

         (x:_) | fid == fidVar = [wildCId]

               | otherwise     = [x | PConst _ (EFun x) _ <- maybe [] Set.toList (IntMap.lookup fid forest)]

+              

+    bracket f arg@(PArg _ fid) = do

+      fid0 <- get

+      put fid

+      x <- f arg

+      put fid0

+      return x

 

 

-newtype TcFM a = TcFM {unTcFM :: MetaStore () -> ([(MetaStore (),a)],[(FId,TcError)])}

-

-instance Functor TcFM where

-  fmap f g = TcFM (\ms -> let (res_g,err_g) = unTcFM g ms

-                          in ([(ms,f x) | (ms,x) <- res_g],err_g))

-

-instance Monad TcFM where

-  return x = TcFM (\ms -> ([(ms,x)],[]))

-  f >>= g  = TcFM (\ms -> case unTcFM f ms of

-                            (res,err) -> let (res',err') = unzip [unTcFM (g x) ms | (ms,x) <- res]

-                                         in (concat res',concat (err:err')))

-

-instance MonadPlus TcFM where

-  mzero = TcFM (\ms -> ([],[]))

-  mplus f g = TcFM (\ms -> let (res_f,err_f) = unTcFM f ms

-                               (res_g,err_g) = unTcFM g ms

-                           in (res_f++res_g,err_f++err_g))

-

-runTcM :: Abstr -> FId -> TcM () a -> TcFM a

-runTcM abstr fid f = TcFM (\ms -> case unTcM f abstr () ms of

-                                    Ok _ ms x -> ([(ms,x)],[]         )

-                                    Fail err  -> ([],      [(fid,err)]))

-

 foldForest :: (FunId -> [PArg] -> b -> b) -> (Expr -> [String] -> b -> b) -> b -> FId -> IntMap.IntMap (Set.Set Production) -> b

 foldForest f g b fcat forest =

   case IntMap.lookup fcat forest of

@@ -215,3 +200,20 @@ foldForest f g b fcat forest =
     foldProd (PCoerce fcat)        b = foldForest f g b fcat forest

     foldProd (PApply funid args)   b = f funid args b

     foldProd (PConst _ const toks) b = g const toks b

+

+

+------------------------------------------------------------------------------

+-- Selectors

+

+instance Selector FId where

+  splitSelector s = (s,s)

+  select cat dp = TcM (\abstr s ms -> case Map.lookup cat (cats abstr) of

+                                        Just (_,fns) -> iter abstr s ms fns

+                                        Nothing      -> Fail s (UnknownCat cat))

+    where

+      iter abstr s ms []           = Zero

+      iter abstr s ms ((_,fn):fns) = Plus (select_helper fn abstr s ms) (iter abstr s ms fns)

+

+select_helper fn = unTcM $ do

+  ty <- lookupFunType fn

+  return (EFun fn,ty)

diff --git a/src/runtime/haskell/PGF/Generate.hs b/src/runtime/haskell/PGF/Generate.hs
index 3e4285617..cbd3d23ab 100644
--- a/src/runtime/haskell/PGF/Generate.hs
+++ b/src/runtime/haskell/PGF/Generate.hs
@@ -12,12 +12,17 @@ import PGF.Macros
 import PGF.TypeCheck
 import PGF.Probabilistic
 
+import Data.Maybe (fromMaybe)
 import qualified Data.Map as Map
 import qualified Data.IntMap as IntMap
 import Control.Monad
 import Control.Monad.Identity
 import System.Random
 
+
+------------------------------------------------------------------------------
+-- The API
+
 -- | Generates an exhaustive possibly infinite list of
 -- abstract syntax expressions.
 generateAll :: PGF -> Type -> [Expr]
@@ -66,24 +71,23 @@ generateRandomFromDepth g pgf e dp =
 
 generate :: Selector sel => sel -> PGF -> Type -> Maybe Int -> [Expr]
 generate sel pgf ty dp =
-  [value2expr (funs (abstract pgf),lookupMeta ms) 0 v |
-        (ms,v) <- runGenM (abstract pgf) (prove emptyScope (TTyp [] ty) dp) sel emptyMetaStore]
+  [e | (_,ms,e) <- snd $ runTcM (abstract pgf) (prove emptyScope (TTyp [] ty) dp >>= refineExpr) sel emptyMetaStore]
 
 generateForMetas :: Selector sel => sel -> PGF -> Expr -> Maybe Int -> [Expr]
 generateForMetas sel pgf e dp =
   case unTcM (infExpr emptyScope e) abs sel emptyMetaStore of
     Ok sel ms (e,_) -> let gen = do fillinVariables $ \scope tty -> do 
-                                      v <- prove scope tty dp
-                                      return (value2expr (funs abs,lookupMeta ms) 0 v)
+                                       prove scope tty dp
                                     refineExpr e
-                       in [e | (ms,e) <- runGenM abs gen sel ms]
-    Fail _          -> []
+                       in [e | (_,ms,e) <- snd $ runTcM abs gen sel ms]
+    Fail _ _        -> []
   where
     abs = abstract pgf
 
-prove :: Selector sel => Scope -> TType -> Maybe Int -> TcM sel Value
+prove :: Selector sel => Scope -> TType -> Maybe Int -> TcM sel Expr
 prove scope (TTyp env1 (DTyp [] cat es1)) dp = do
-  (fn,DTyp hypos _ es2) <- clauses cat
+  (fe,DTyp hypos _ es2) <- select cat dp
+  if fe == EFun (mkCId "plus") then mzero else return ()
   case dp of
     Just 0 | not (null hypos) -> mzero
     _                         -> return ()
@@ -91,55 +95,34 @@ prove scope (TTyp env1 (DTyp [] cat es1)) dp = do
   vs1 <- mapM (PGF.TypeCheck.eval env1) es1
   vs2 <- mapM (PGF.TypeCheck.eval env2) es2
   sequence_ [eqValue mzero suspend (scopeSize scope) v1 v2 | (v1,v2) <- zip vs1 vs2]
-  vs <- mapM descend args
-  return (VApp fn vs)
+  es <- mapM descend args
+  return (foldl EApp fe es)
   where
     suspend i c = do
       mv <- getMeta i
       case mv of
         MBound e -> c e
-        MUnbound scope tty cs -> do v <- prove scope tty dp
-                                    e <- TcM (\abs sel ms -> Ok sel ms (value2expr (funs abs,lookupMeta ms) 0 v))
+        MUnbound scope tty cs -> do e <- prove scope tty dp
                                     setMeta i (MBound e)
                                     sequence_ [c e | c <- (c:cs)]
 
-    clauses cat = do
-      fn <- select cat
-      if fn == mkCId "plus" then mzero else return ()
-      ty <- lookupFunType fn
-      return (fn,ty)
-
     mkEnv env []                = return (env,[])
     mkEnv env ((bt,x,ty):hypos) = do
       (env,arg) <- if x /= wildCId
                     then do i <- newMeta scope (TTyp env ty)
-                            let v = VMeta i env []
-                            return (v : env,Right v)
+                            return (VMeta i env [] : env,Right (EMeta i))
                     else return (env,Left (TTyp env ty))
       (env,args) <- mkEnv env hypos
       return (env,(bt,arg):args)
 
     descend (bt,arg) = do let dp' = fmap (flip (-) 1) dp
-                          v <- case arg of
-                                 Right v  -> return v
+                          e <- case arg of
+                                 Right e  -> return e
                                  Left tty -> prove scope tty dp'
-                          v <- case bt of
-                                 Implicit -> return (VImplArg v)
-                                 Explicit -> return v
-                          return v
-
-
-------------------------------------------------------------------------------
--- Generation Monad
-
-
-runGenM :: Abstr -> TcM s a -> s -> MetaStore s -> [(MetaStore s,a)]
-runGenM abs f s ms = toList (unTcM f abs s ms) []
-  where
-    toList (Ok s ms x)  xs = (ms,x) : xs
-    toList (Fail _)     xs = xs
-    toList (Zero)       xs = xs
-    toList (Plus b1 b2) xs = toList b1 (toList b2 xs)
+                          e <- case bt of
+                                 Implicit -> return (EImplArg e)
+                                 Explicit -> return e
+                          return e
 
 
 -- Helper function for random generation. After every
@@ -150,3 +133,57 @@ restart g f =
   in case f g1 of
        []     -> []
        (x:xs) -> x : restart g2 f
+
+
+------------------------------------------------------------------------------
+-- Selectors
+
+instance Selector () where
+  splitSelector s = (s,s)
+  select cat dp
+    | cat == cidInt    = return (ELit (LInt 999),  DTyp [] cat [])
+    | cat == cidFloat  = return (ELit (LFlt 3.14), DTyp [] cat [])
+    | cat == cidString = return (ELit (LStr "Foo"),DTyp [] cat [])
+    | otherwise        = TcM (\abstr s ms -> case Map.lookup cat (cats abstr) of
+                                               Just (_,fns) -> iter abstr ms fns
+                                               Nothing      -> Fail s (UnknownCat cat))
+    where
+      iter abstr ms []           = Zero
+      iter abstr ms ((_,fn):fns) = Plus (select_helper fn abstr () ms) (iter abstr ms fns)
+
+instance RandomGen g => Selector (Identity g) where
+  splitSelector (Identity g) = let (g1,g2) = split g
+                               in (Identity g1, Identity g2)
+
+  select cat dp
+    | cat == cidInt    = TcM (\abstr (Identity g) ms ->
+                                  let (n,g') = maybe random (\d -> randomR ((-10)*d,10*d)) dp g
+                                  in Ok (Identity g) ms (ELit (LInt n),DTyp [] cat []))
+    | cat == cidFloat  = TcM (\abstr (Identity g) ms ->
+                                  let (d,g') = maybe random (\d' -> let d = fromIntegral d'
+                                                                    in randomR ((-pi)*d,pi*d)) dp g
+                                  in Ok (Identity g) ms (ELit (LFlt d),DTyp [] cat []))
+    | cat == cidString = TcM (\abstr (Identity g) ms ->
+                                  let (g1,g2) = split g
+                                      s = take (fromMaybe 10 dp) (randomRs ('A','Z') g1)
+                                  in Ok (Identity g2) ms (ELit (LStr s),DTyp [] cat []))
+    | otherwise        = TcM (\abstr (Identity g) ms ->
+                                  case Map.lookup cat (cats abstr) of
+                                    Just (_,fns) -> do_rand abstr g ms 1.0 fns
+                                    Nothing      -> Fail (Identity g) (UnknownCat cat))
+    where
+      do_rand abstr g ms p []  = Zero
+      do_rand abstr g ms p fns = let (d,g')    = randomR (0.0,p) g
+                                     (g1,g2)   = split g'
+                                     (p',fn,fns') = hit d fns
+                                 in Plus (select_helper fn abstr (Identity g1) ms) (do_rand abstr g2 ms (p-p') fns')
+
+      hit :: Double -> [(Double,a)] -> (Double,a,[(Double,a)])
+      hit d (px@(p,x):xs)
+        | d < p     = (p,x,xs)
+        | otherwise = let (p',x',xs') = hit (d-p) xs
+                      in (p,x',px:xs')
+
+select_helper fn = unTcM $ do
+  ty <- lookupFunType fn
+  return (EFun fn,ty)
diff --git a/src/runtime/haskell/PGF/TypeCheck.hs b/src/runtime/haskell/PGF/TypeCheck.hs
index d7225dd0b..843326e4c 100644
--- a/src/runtime/haskell/PGF/TypeCheck.hs
+++ b/src/runtime/haskell/PGF/TypeCheck.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE FlexibleContexts, RankNTypes #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, RankNTypes #-}
 
 ----------------------------------------------------------------------
 -- |
@@ -20,7 +20,7 @@ module PGF.TypeCheck ( checkType, checkExpr, inferExpr
                      -- internals needed for the typechecking of forests
                      , MetaStore, emptyMetaStore, newMeta, newGuardedMeta, fillinVariables, getMeta, setMeta, MetaValue(..)
                      , Scope, emptyScope, scopeSize, scopeEnv, addScopedVar
-                     , TcM(..), TcResult(..), TType(..), Selector(..), tcError
+                     , TcM(..), TcResult(..), runTcM, TType(..), Selector(..)
                      , tcExpr, infExpr, eqType, eqValue
                      , lookupFunType, eval
                      , refineExpr, checkResolvedMetaStore, lookupMeta
@@ -38,8 +38,9 @@ import Data.Maybe as Maybe
 import Data.List as List
 import Control.Monad
 import Control.Monad.Identity
+import Control.Monad.State
+import Control.Monad.Error
 import Text.PrettyPrint
-import System.Random as Random
 
 -----------------------------------------------------
 -- The Scope
@@ -85,16 +86,20 @@ data MetaValue s
 newtype TcM s a = TcM {unTcM :: Abstr -> s -> MetaStore s -> TcResult s a}
 data TcResult s a
   = Ok s (MetaStore s) a
-  | Fail TcError
+  | Fail s TcError
   | Zero
   | Plus (TcResult s a) (TcResult s a)
 
+class Selector s where
+  splitSelector :: s -> (s,s)
+  select        :: CId -> Maybe Int -> TcM s (Expr,Type)
+
 instance Monad (TcM s) where
   return x = TcM (\abstr s ms -> Ok s ms x)
   f >>= g  = TcM (\abstr s ms -> iter abstr (unTcM f abstr s ms))
     where
       iter abstr (Ok s ms x)  = unTcM (g x) abstr s ms
-      iter abstr (Fail e)     = Fail e
+      iter abstr (Fail s e)   = Fail s e
       iter abstr Zero         = Zero
       iter abstr (Plus b1 b2) = Plus (iter abstr b1) (iter abstr b2)
 
@@ -103,23 +108,44 @@ instance Selector s => MonadPlus (TcM s) where
   mplus f g = TcM (\abstr s ms -> let (s1,s2) = splitSelector s
                                   in Plus (unTcM f abstr s1 ms) (unTcM g abstr s2 ms))
 
+instance MonadState s (TcM s) where
+  get = TcM (\abstr s ms -> Ok s ms s)
+  put s = TcM (\abstr _ ms -> Ok s ms ())
+
+instance MonadError TcError (TcM s) where
+  throwError e = TcM (\abstr s ms -> Fail s e)
+  catchError f h = TcM (\abstr s ms -> iter abstr ms (unTcM f abstr s ms))
+    where
+      iter abstr _  (Ok s ms x)  = Ok s ms x
+      iter abstr ms (Fail s e)   = unTcM (h e) abstr s ms
+      iter abstr _  Zero         = Zero
+      iter abstr ms (Plus b1 b2) = Plus (iter abstr ms b1) (iter abstr ms b2)
+
 instance Functor (TcM s) where
   fmap f x = TcM (\abstr s ms -> iter (unTcM x abstr s ms))
     where
       iter (Ok s ms x)  = Ok s ms (f x)
-      iter (Fail e)     = Fail e
+      iter (Fail s e)   = Fail s e
       iter Zero         = Zero
       iter (Plus b1 b2) = Plus (iter b1) (iter b2)
 
+runTcM :: Abstr -> TcM s a -> s -> MetaStore s -> ([(s,TcError)],[(s,MetaStore s,a)])
+runTcM abs f s ms = collect (unTcM f abs s ms) ([],[])
+  where
+    collect (Ok _ ms x)  (es,xs) = (es,(s,ms,x) : xs)
+    collect (Fail s e)   (es,xs) = ((s,e) : es,xs)
+    collect (Zero)       exs     = exs
+    collect (Plus b1 b2) exs     = collect b1 (collect b2 exs)
+
 lookupCatHyps :: CId -> TcM s [Hypo]
 lookupCatHyps cat = TcM (\abstr s ms -> case Map.lookup cat (cats abstr) of
                                           Just (hyps,_) -> Ok s ms hyps
-                                          Nothing       -> Fail (UnknownCat cat))
+                                          Nothing       -> Fail s (UnknownCat cat))
 
 lookupFunType :: CId -> TcM s Type
 lookupFunType fun = TcM (\abstr s ms -> case Map.lookup fun (funs abstr) of
                                           Just (ty,_,_,_) -> Ok s ms ty
-                                          Nothing         -> Fail (UnknownFun fun))
+                                          Nothing         -> Fail s (UnknownFun fun))
 
 emptyMetaStore :: MetaStore s
 emptyMetaStore = IntMap.empty
@@ -157,9 +183,6 @@ fillinVariables f = do
                              sequence_ [c e | c <- cs]
                              fillinVariables f
 
-tcError :: TcError -> TcM s a
-tcError e = TcM (\abstr s ms -> Fail e)
-
 addConstraint :: MetaId -> MetaId -> (Expr -> TcM s ()) -> TcM s ()
 addConstraint i j c = do
   mv   <- getMeta j
@@ -221,43 +244,6 @@ ppTcError (UnexpectedImplArg xs e)     = braces (ppExpr 0 xs e) <+> text "is imp
 ppTcError (UnsolvableGoal xs metaid ty)= text "The goal:" <+> ppMeta metaid <+> colon <+> ppType 0 xs ty $$
                                          text "cannot be solved"
 
-------------------------------------------------------------------------------
--- Selectors
-
-class Selector s where
-  splitSelector :: s -> (s,s)
-  select        :: CId -> TcM s CId
-
-instance Selector () where
-  splitSelector s = (s,s)
-  select cat = TcM (\abstr s ms -> case Map.lookup cat (cats abstr) of
-                                     Just (_,fns) -> iter ms fns
-                                     Nothing      -> Fail (UnknownCat cat))
-    where
-      iter ms []           = Zero
-      iter ms ((_,fn):fns) = Plus (Ok () ms fn) (iter ms fns)
-
-instance RandomGen g => Selector (Identity g) where
-  splitSelector (Identity g) = let (g1,g2) = Random.split g
-                               in (Identity g1, Identity g2)
-
-  select cat = TcM (\abstr (Identity g) ms ->
-                               case Map.lookup cat (cats abstr) of
-                                 Just (_,fns) -> do_rand g ms 1.0 fns
-                                 Nothing      -> Fail (UnknownCat cat))
-    where
-      do_rand g ms p []  = Zero
-      do_rand g ms p fns = let (d,g')    = randomR (0.0,p) g
-                               (g1,g2)   = Random.split g'
-                               (p',fn,fns') = hit d fns
-                           in Plus (Ok (Identity g1) ms fn) (do_rand g2 ms (p-p') fns')
-
-      hit :: Double -> [(Double,a)] -> (Double,a,[(Double,a)])
-      hit d (px@(p,x):xs)
-        | d < p     = (p,x,xs)
-        | otherwise = let (p',x',xs') = hit (d-p) xs
-                      in (p,x',px:xs')
-
 -----------------------------------------------------
 -- checkType
 -----------------------------------------------------
@@ -268,7 +254,7 @@ checkType :: PGF -> Type -> Either TcError Type
 checkType pgf ty = 
   case unTcM (tcType emptyScope ty >>= refineType) (abstract pgf) () emptyMetaStore of
     Ok s ms ty -> Right ty
-    Fail err   -> Left  err
+    Fail _ err -> Left  err
 
 tcType :: Scope -> Type -> TcM s Type
 tcType scope ty@(DTyp hyps cat es) = do
@@ -294,7 +280,7 @@ tcHypo scope (b,x,ty) = do
     else return (addScopedVar x (TTyp (scopeEnv scope) ty) scope,(b,x,ty))
 
 tcCatArgs scope []              delta []                   ty0 n m = return (delta,[])
-tcCatArgs scope (EImplArg e:es) delta ((Explicit,x,ty):hs) ty0 n m = tcError (UnexpectedImplArg (scopeVars scope) e)
+tcCatArgs scope (EImplArg e:es) delta ((Explicit,x,ty):hs) ty0 n m = throwError (UnexpectedImplArg (scopeVars scope) e)
 tcCatArgs scope (EImplArg e:es) delta ((Implicit,x,ty):hs) ty0 n m = do
   e <- tcExpr scope e (TTyp delta ty)
   (delta,es) <- if x == wildCId
@@ -316,7 +302,7 @@ tcCatArgs scope (e:es) delta ((Explicit,x,ty):hs) ty0 n m = do
                           tcCatArgs scope es (v:delta) hs ty0 n m
   return (delta,e:es)
 tcCatArgs scope _ delta _ ty0@(DTyp _ cat _) n m = do
-  tcError (WrongCatArgs (scopeVars scope) ty0 cat n m)
+  throwError (WrongCatArgs (scopeVars scope) ty0 cat n m)
 
 -----------------------------------------------------
 -- checkExpr
@@ -329,8 +315,8 @@ checkExpr pgf e ty =
                  e <- refineExpr e
                  checkResolvedMetaStore emptyScope e
                  return e) (abstract pgf) () emptyMetaStore of
-    Ok _ ms e -> Right e
-    Fail err  -> Left err
+    Ok _ ms e  -> Right e
+    Fail _ err -> Left err
 
 tcExpr :: Scope -> Expr -> TType -> TcM s Expr
 tcExpr scope e0@(EAbs Implicit x e) tty =
@@ -342,7 +328,7 @@ tcExpr scope e0@(EAbs Implicit x e) tty =
                                                                          e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es))
                                                       return (EAbs Implicit x e)
     _                                           -> do ty <- evalType (scopeSize scope) tty
-                                                      tcError (NotFunType (scopeVars scope) e0 ty)
+                                                      throwError (NotFunType (scopeVars scope) e0 ty)
 tcExpr scope e0 (TTyp delta (DTyp ((Implicit,y,ty):hs) c es)) = do
   e0 <- if y == wildCId
           then tcExpr (addScopedVar wildCId (TTyp delta ty) scope)
@@ -359,7 +345,7 @@ tcExpr scope e0@(EAbs Explicit x e) tty =
                                                                          e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es))
                                                       return (EAbs Explicit x e)
     _                                           -> do ty <- evalType (scopeSize scope) tty
-                                                      tcError (NotFunType (scopeVars scope) e0 ty)
+                                                      throwError (NotFunType (scopeVars scope) e0 ty)
 tcExpr scope (EMeta _) tty = do
   i <- newMeta scope tty
   return (EMeta i)
@@ -386,7 +372,7 @@ inferExpr pgf e =
                  ty <- evalType 0 tty
                  return (e,ty)) (abstract pgf) () emptyMetaStore of
     Ok _ ms (e,ty) -> Right (e,ty)
-    Fail err       -> Left err
+    Fail _ err     -> Left err
 
 infExpr :: Scope -> Expr -> TcM s (Expr,TType)
 infExpr scope e0@(EApp e1 e2) = do
@@ -413,12 +399,12 @@ infExpr scope (ETyped e ty) = do
 infExpr scope (EImplArg e) = do
   (e,tty)  <- infExpr scope e
   return (EImplArg e,tty)
-infExpr scope e = tcError (CannotInferType (scopeVars scope) e)
+infExpr scope e = throwError (CannotInferType (scopeVars scope) e)
 
 tcArg scope e1 e2 delta ty0@(DTyp [] c es) = do
   ty1 <- evalType (scopeSize scope) (TTyp delta ty0)
-  tcError (NotFunType (scopeVars scope) e1 ty1)
-tcArg scope e1 (EImplArg e2) delta ty0@(DTyp ((Explicit,x,ty):hs) c es) = tcError (UnexpectedImplArg (scopeVars scope) e2)
+  throwError (NotFunType (scopeVars scope) e1 ty1)
+tcArg scope e1 (EImplArg e2) delta ty0@(DTyp ((Explicit,x,ty):hs) c es) = throwError (UnexpectedImplArg (scopeVars scope) e2)
 tcArg scope e1 (EImplArg e2) delta ty0@(DTyp ((Implicit,x,ty):hs) c es) = do
   e2 <- tcExpr scope e2 (TTyp delta ty)
   if x == wildCId
@@ -450,7 +436,7 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
     raiseTypeMatchError = do ty1 <- evalType k tty1
                              ty2 <- evalType k tty2
                              e   <- refineExpr (EMeta i0)
-                             tcError (TypeMismatch (scopeVars scope) e ty1 ty2)
+                             throwError (TypeMismatch (scopeVars scope) e ty1 ty2)
 
     eqHyps :: Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM s (Int,Env,Env)
     eqHyps k delta1 []                 delta2 []                 =
@@ -558,7 +544,7 @@ checkResolvedMetaStore scope e = TcM (\abstr s ms ->
   let xs = [i | (i,mv) <- IntMap.toList ms, not (isResolved mv)]
   in if List.null xs
        then Ok s ms ()
-       else Fail (UnresolvedMetaVars (scopeVars scope) e xs))
+       else Fail s (UnresolvedMetaVars (scopeVars scope) e xs))
   where
     isResolved (MUnbound _ _ []) = True
     isResolved (MGuarded  _ _ _) = True