diff --git a/Ivor/Datatype.lhs b/Ivor/Datatype.lhs
--- a/Ivor/Datatype.lhs
+++ b/Ivor/Datatype.lhs
@@ -5,6 +5,7 @@
 > import Ivor.Typecheck
 > import Ivor.Nobby
 > import Ivor.PatternDefs
+> import Ivor.Errors
 
 > import Debug.Trace
 
@@ -52,7 +53,7 @@
 schemes, and returns a DataType, ready for compilation to entries in
 the context and an executable elimination rule.
 
-> checkType :: Monad m => Gamma Name -> RawDatatype -> m (Datatype Name)
+> checkType :: Gamma Name -> RawDatatype -> IvorM (Datatype Name)
 > checkType gamma (RData (ty,kind) cons numps (er,erty) (cr,crty) eschemes cschemes) = 
 >     do (kv, _) <- typecheck gamma kind
 >        let erdata = Elims er cr (map fst cons)
@@ -61,12 +62,12 @@
 >	 (ev, _) <- typecheck gamma'' erty
 >	 (cv, _) <- typecheck gamma'' crty
 >	 -- let gamma''' = extend gamma'' (er,G (ElimRule dummyRule) ev defplicit)
->        (esch, _, _, _) <- checkDef gamma'' er erty eschemes False False
->        (csch, _, _, _) <- checkDef gamma'' cr crty cschemes False False
+>        ([(_, esch, _)], _, _) <- checkDef gamma'' er erty eschemes False False
+>        ([(_, csch, _)], _, _) <- checkDef gamma'' cr crty cschemes False False
 >	 return (Data (ty,G (TCon (arity gamma kv) erdata) kv defplicit) consv numps
 >                    (er,ev) (cr,cv) (Just esch) (Just csch) eschemes cschemes)
 
-> checkTypeNoElim :: Monad m => Gamma Name -> RawDatatype -> m (Datatype Name)
+> checkTypeNoElim :: Gamma Name -> RawDatatype -> IvorM (Datatype Name)
 > checkTypeNoElim gamma (RData (ty,kind) cons numps (er,erty) (cr,crty) eschemes cschemes) = 
 >     do (kv, _) <- typecheck gamma kind
 >        let erdata = Elims er cr (map fst cons)
@@ -96,9 +97,8 @@
 we get V 0 = pn ... V n = p0
 then pattern variables are retrieved by projection with Proj in typechecked t.
 
-> checkScheme :: Monad m =>
->	          Gamma Name -> Name -> RawScheme -> m (Scheme Name)
-> checkScheme gamma n (RSch pats ret) = 
+> checkScheme :: Gamma Name -> Name -> RawScheme -> IvorM (Scheme Name)
+> checkScheme gamma n (RSch pats (RWRet ret)) = 
 >     do let ps = map (mkPat gamma) pats
 >	 let rhsvars = getPatVars gamma ps
 >        let rhs = substVars gamma n rhsvars ret
@@ -116,8 +116,10 @@
 > mkPat gam (RApp f a) = pat' (unwind f a)
 >   where unwind (RApp f s) a = let (f',as) = unwind f s in
 >				    (f',(mkPat gam a):as)
+>         unwind (RFileLoc _ _ t) a = unwind t a
 >	  unwind t a = (t, [mkPat gam a])
 >         pat' (Var n, as) = mkPatV n (lookupval n gam) (reverse as)
+>         pat' (RFileLoc _ _ t, as) = pat' (t, as)
 >         pat' _ = PTerm
 
 >         mkPatV n (Just (DCon t x)) as = PCon t n tyname as
@@ -126,6 +128,7 @@
 >         tyname = case (getTyName gam (getname (getappfun f))) of
 >                    Just x -> x
 >         getname (Var n) = n
+>         getname (RFileLoc _ _ t) = getname t
 > mkPat gam _ {-(RBind _ _ _)-} = PTerm
 > {-
 > TODO: If a datatype has a placeholder in its indices, the value should
@@ -178,6 +181,7 @@
 >			    (Just i) -> i
 >	   sv' (RApp f a) = App (sv' f) (sv' a)
 >          sv' (RConst c) = Const c
+>          sv' (RFileLoc _ _ t) = sv' t
 
 >          mkGood x = case (lookupval x gam) of
 >	       (Just (DCon t i)) -> Con t x i
diff --git a/Ivor/Errors.lhs b/Ivor/Errors.lhs
new file mode 100644
--- /dev/null
+++ b/Ivor/Errors.lhs
@@ -0,0 +1,22 @@
+> {-# OPTIONS_GHC -fglasgow-exts #-}
+
+> module Ivor.Errors where
+
+> import Ivor.TTCore
+> import Control.Monad.Error
+
+> data IError = ICantUnify (Indexed Name) (Indexed Name)
+>             | INotConvertible (Indexed Name) (Indexed Name)
+>             | IMessage String
+>             | IUnbound (Indexed Name) (Indexed Name) (Indexed Name) (Indexed Name) [Name]
+>             | INoSuchVar Name
+>             | IContext String IError
+>   deriving (Show, Eq)
+
+> instance Error IError where
+>     noMsg = IMessage "Ivor Error"
+>     strMsg s = IMessage s
+
+> type IvorM = Either IError
+
+> ifail = Left
diff --git a/Ivor/MakeData.lhs b/Ivor/MakeData.lhs
--- a/Ivor/MakeData.lhs
+++ b/Ivor/MakeData.lhs
@@ -29,8 +29,7 @@
 >         cischemes = mkSchemes False name (ruleName name "Case") 
 >                               params datacons motiveName methNames
 >         tycontype = mkCon params contype in
->         return $ -- (trace (show eischemes)) $  
->          RData (name,tycontype) datacons (length params)
+>         return $ RData (name,tycontype) datacons (length params)
 >                    (ruleName name "Elim", ecasetype) -- elim rule
 >                    (ruleName name "Case", ccasetype) -- case rule
 >                    eischemes -- elim rule iota schemes
@@ -49,8 +48,8 @@
 >              = (mkScheme rec n ername ps c cty motive mns m):(mks cs ms mns)
 
 > mkScheme rec n ername ps c cty motive mns meth 
->     = RSch (mkIArgs ps c cty motive mns) 
->            (mkIRet rec n ername meth motive mns ps cty)
+>     = RSch (mkIArgs ps c cty motive mns)
+>            (RWRet (mkIRet rec n ername meth motive mns ps cty))
 
 > mkIArgs ps c cty motive mns = getappargs (getrettype cty) ++
 >                               [mkapp (Var c) (map Var (getargnames cty))] ++
@@ -62,6 +61,7 @@
 >            | isrec ty tyname && rec 
 >                = (Var n):(mkRecApp ername ty n motive mns):(mkArgs sc)
 >            | otherwise = (Var n):(mkArgs sc)
+>         mkArgs (RFileLoc f l t) = mkArgs t
 >         mkArgs _ = []
 >         mkRecApp en ty n motive mns = 
 >             mkapp (Var en) $ (getappargs ty)++(map Var (n:motive:mns))
@@ -91,6 +91,7 @@
 
 > bindIndices (RBind n (B Pi ty) sc) rest 
 >     = (RBind n (B Pi ty) (bindIndices sc rest))
+> bindIndices (RFileLoc f l t) rest = bindIndices t rest
 > bindIndices sc rest = rest
 
 > bindTarget x n ps ty rest 
@@ -111,6 +112,7 @@
 >            | isrec argtype tyname && rec
 >                = (RBind a (B Pi argtype) (mkrec a argtype sc))
 >            | otherwise = (RBind a (B Pi argtype) (methtype sc))
+>        methtype (RFileLoc _ _ t) = methtype t
 >        methtype sc = mkapp (Var p) $ (getindices sc)++
 >              [mkapp (Var n) (map Var ((map fst ps)++(getargnames ty)))]
 >        mkrec a argtype sc = (RBind (ih a) (B Pi (rectype a argtype p)) 
diff --git a/Ivor/PatternDefs.lhs b/Ivor/PatternDefs.lhs
--- a/Ivor/PatternDefs.lhs
+++ b/Ivor/PatternDefs.lhs
@@ -7,6 +7,7 @@
 > import Ivor.Nobby
 > import Ivor.Typecheck
 > import Ivor.Unify
+> import Ivor.Errors
 
 > import Debug.Trace
 > import Data.List
@@ -14,14 +15,15 @@
 
 Use the iota schemes from Datatype to represent pattern matching definitions.
 
-Return the definition and its type, as well as any other names which need
+Return the definition, and auxiliary definitions,
+and their types, as well as any other names which need
 to be defined to complete the definition.
 Also return whether the function is definitely total.
 
-> checkDef :: Monad m => Gamma Name -> Name -> Raw -> [PMRaw] -> 
+> checkDef :: Gamma Name -> Name -> Raw -> [PMRaw] -> 
 >             Bool -> -- Check for coverage
 >             Bool -> -- Check for well-foundedness
->             m (PMFun Name, Indexed Name, [(Name, Indexed Name)], Bool)
+>             IvorM ([(Name, PMFun Name, Indexed Name)], [(Name, Indexed Name)], Bool)
 > checkDef gam fn tyin pats cover wellfounded = do
 >   --x <- expandCon gam (mkapp (Var (UN "S")) [mkapp (Var (UN "S")) [Var (UN "x")]])
 >   --x <- expandCon gam (mkapp (Var (UN "vcons")) [RInfer,RInfer,RInfer,mkapp (Var (UN "vnil")) [Var (UN "foo")]])
@@ -33,15 +35,16 @@
 >   checkNotExists fn gam
 >   gam' <- gInsert fn (G Undefined ty defplicit) gam
 >   clauses' <- validClauses gam' fn ty clauses'
->   (pmdef, newdefs, covers) <- matchClauses gam' fn pats tyin cover clauses'
->   wf <- if wellfounded then
+>   (pmdefs, newdefs, covers) <- matchClauses gam' fn pats tyin ty cover clauses'
+>   wf <- return True 
+>         {- if wellfounded then
 >             do checkWellFounded gam fn [0..arity-1] pmdef
 >                return True
 >            else case checkWellFounded gam fn [0..arity-1] pmdef of
 >                   Nothing -> return False
->                   _ -> return True
+>                   _ -> return True -}
 >   let total = wf && covers
->   return (PMFun arity pmdef, ty, newdefs, total)
+>   return (pmdefs, newdefs, total)
 >     where checkNotExists n gam = case lookupval n gam of
 >                                 Just Undefined -> return ()
 >                                 Just _ -> fail $ show n ++ " already defined"
@@ -65,11 +68,10 @@
 2) Alternatively, a definition is well founded if in every recursive call
 there are no increasing arguments and at least one decreasing argument.
 
-> checkWellFounded :: Monad m =>
->                     Gamma Name ->
+> checkWellFounded :: Gamma Name ->
 >                     Name -> -- recursive function name
 >                     [Int] -> -- set of well founded args
->                     [PMDef Name] -> m ()
+>                     [PMDef Name] -> IvorM ()
 > checkWellFounded gam fn args cs = case cwf1 fn args cs of
 >                                     Failure err -> cwf2 fn cs err
 >                                     Success v -> return ()
@@ -171,20 +173,24 @@
 Match up the inferred arguments to the names (so getting the types of the
 names bound in patterns) then type check the right hand side.
 
-> matchClauses :: Monad m => Gamma Name -> Name -> [PMRaw] -> Raw ->
+Each clause may generate auxiliary definitions, so return all definitons created.
+
+> matchClauses :: Gamma Name -> Name -> [PMRaw] -> Raw -> Indexed Name -> 
 >                 Bool -> -- Check coverage
 >                 [(Indexed Name, Indexed Name)] -> 
->                 m ([PMDef Name], [(Name, Indexed Name)], Bool)
-> matchClauses gam fn pats tyin cover gen = do
+>                 IvorM ([(Name, PMFun Name, Indexed Name)], [(Name, Indexed Name)], Bool)
+> matchClauses gam fn pats tyin ty@(Ind ty') cover gen = do
 >    let raws = zip (map mkRaw pats) (map getRet pats)
->    (checkpats, newdefs) <- mytypechecks gam raws [] []
+>    (checkpats, newdefs, aux, covers) <- mytypechecks gam raws [] [] [] True
 >    cv <- if cover then 
 >              do checkCoverage (map fst checkpats) (map fst gen)
 >                 return True
 >              else case checkCoverage (map fst checkpats) (map fst gen) of
->                 Nothing -> return False
+>                 Left err -> return False
 >                 _ -> return True
->    return $ (map (mkScheme gam) checkpats, newdefs, cv)
+>    let pmdef = map (mkScheme gam) checkpats
+>    let arity = length (getExpected ty')
+>    return $ ((fn, PMFun arity pmdef, ty) : aux , newdefs, cv && covers)
 
     where mkRaw (RSch pats r) = mkPBind pats tyin r
           mkPBind [] _ r = r
@@ -193,14 +199,13 @@
 
 >   where mkRaw (RSch pats r) = mkapp (Var fn) pats
 >         getRet (RSch pats r) = r
->         mytypechecks gam [] acc defs = return (reverse acc, defs)
->         mytypechecks gam (c:cs) acc defs
->             = do (cl, cr, newdefs) <- mytypecheck gam c
->                  mytypechecks gam cs ((cl,cr):acc) (defs++newdefs)
->         mytypecheck gam (clause, ret) = 
+>         mytypechecks gam [] acc defs auxdefs cov = return (reverse acc, auxdefs, defs, cov)
+>         mytypechecks gam (c:cs) acc defs auxdefs cov =
+>             do ((cl, cr, _), newdefs, aux', covd) <- mytypecheck gam c (length cs)
+>                mytypechecks gam cs ((cl,cr):acc) (defs++newdefs) (auxdefs++aux') (cov && covd)
+>         mytypecheck gam (clause, (RWRet ret)) i = 
 >             do (tm@(Ind tmtt), pty,
->                 rtm@(Ind rtmtt), rty, env, newdefs) <-
->                   checkAndBindPair gam clause ret
+>                 rtm@(Ind rtmtt), rty, env, newdefs) <- checkAndBindPair gam clause ret
 >                unified <- unifyenv gam env pty rty
 >                let gam' = foldl (\g (n,t) -> extend g (n,G Undefined t 0))
 >                                   gam newdefs
@@ -208,17 +213,73 @@
 >                -- checkConvEnv env gam pty rty $ "Pattern error: " ++ show pty ++ " and " ++ show rty ++ " are not convertible " ++ show unify
 >                let namesret = filter (notGlobal gam') $ getNames (Sc rtmtt')
 >                let namesbound = getNames (Sc tmtt)
->                checkAllBound namesret namesbound (Ind rtmtt') tmtt
->                return (tm, Ind rtmtt', newdefs)
+>                checkAllBound (fileLine ret) namesret namesbound (Ind rtmtt') tmtt rty pty
+>                -- trace (show (unified, rtmtt, tm, rtmtt')) $ 
+>                return ((tm, Ind rtmtt', newdefs), [], newdefs, True)
+>         mytypecheck gam (clause, (RWith scr pats)) i =
+>             do -- Get the type of scrutinee, construct the type of the auxiliary definition
+>                (tm@(Ind clausett), clausety, _, scrty@(Ind stt), env) <- checkAndBindWith gam clause scr fn
+>                let args = getRawArgs clause
+>                let restTyin = addLastArg tyin (forget scrty)
+>                margs <- getMatches tm tm
+>                let margNames = nub (map fst margs)
+>                let newargs = filter (\ (x,ty) -> x `elem` margNames) env
+>                newpats <- mapM (getNewPat tm 1) pats
+>                let newfntyin = mkNewTy (newargs ++ [(UN "__scr", B Pi stt)]) clausety
+>                (newfnTy, _) <- check gam env (forget newfntyin) (Just (Ind Star))
+>                -- Make a name for the new function, clauses in 'pats' need the new name,
+>                -- and form a definition of type restTy
+>                let newname = mkNewName fn i
+>                -- TODO: All pats have to match against args ++ [_]
+>                -- Final clause returns newname applied to args++scrutinee
+>                let ret = rawApp (Var newname) ((map Var (map fst newargs)) ++ [scr])
+>                let gam' = insertGam newname (G Undefined newfnTy 0) gam
+>                newpdef <- mapM (newp tm newargs 1) (zip newpats pats)
+>                (chk, auxdefs, _, _) <- mytypecheck gam' (clause, (RWRet ret)) i
+>                (auxdefs', newdefs, covers) <- checkDef gam' newname (forget newfnTy) newpdef False cover
+>                return (chk, auxdefs++auxdefs', newdefs, covers)
+
+>         addLastArg (RBind n (B Pi arg) x) ty = RBind n (B Pi arg) (addLastArg x ty)
+>         addLastArg x ty = RBind (UN "X") (B Pi ty) x
+>         rawApp f [] = f
+>         rawApp f (a:as) = rawApp (RApp f a) as
+
+>         mkNewName (UN n) i = UN ("W__"++ n ++ "__" ++ show i) -- MN (n, i)
+>         mkNewName (MN (n,j)) i = MN (n, (j + i + 255))
+
+>         mkNewTy [] (Ind t) = t
+>         mkNewTy ((x,b):ts) t = Bind x b (Sc (mkNewTy ts t))
+
+>         getNewPat proto i (RSch args ret) = do
+>             let pargs = rawApp (Var fn) (take (length args - i) args)
+>             (argv, argt, _) <- checkAndBind gam [] pargs Nothing
+>             getMatches argv proto
+
+>         newp proto newargs i (newps, RSch args ret) = do
+>             ret' <- newpRet ret
+>             return $ RSch ((getAuxPats (map fst newargs) newps)++(lastn i args)) ret'
+>                 where newpRet (RWith v schs) = 
+>                          do newpats <- mapM (getNewPat proto (i+1)) schs
+>                             newpdef <- mapM (newp proto newargs (i+1)) (zip newpats schs)
+>                             return (RWith v newpdef)
+>                       newpRet r = return r
+
+>         lastn i xs = reverse $ take i (reverse xs)
+
+>         getAuxPats [] n = []
+>         getAuxPats (x:xs) n = case lookup x n of
+>                                 (Just t) -> (forget t):(getAuxPats xs n)
+
 >         notGlobal gam n = case lookupval n gam of
 >                               Nothing -> True
 >                               _ -> False
->         checkAllBound r b rhs clause = do
+>         checkAllBound fl r b rhs clause rhsTy clauseTy = do
 >              let unbound = filter (\y -> not (elem y b)) r
 >              if (length unbound == 0)
 >                 then return ()
->                 else fail $ "Unbound names in clause for " ++ show clause ++ ":\n" ++ show rhs ++ "\n"
->                             ++ show unbound ++ "\n"
+>                 else ifail $ addContext fl (IUnbound (Ind clause) clauseTy rhs rhsTy unbound)
+>         addContext Nothing err = err
+>         addContext (Just (f,l)) err = IContext (f ++ ":" ++ show l ++ ":") err
 
 > mkScheme :: Gamma Name -> (Indexed Name, Indexed Name) -> PMDef Name
 > mkScheme gam (Ind pat, ret) = Sch (map mkpat (getPatArgs pat)) ret
@@ -245,31 +306,35 @@
 must match one of 'pats'.
 fails, reporting which case isn't matched, if patterns don't cover.
 
-> checkCoverage :: Monad m => [Indexed Name] -> [Indexed Name] -> m ()
+> checkCoverage :: [Indexed Name] -> [Indexed Name] -> IvorM ()
 > checkCoverage pats [] = return ()
 > checkCoverage pats (c:cs)
 >     | length (filter (matches c) pats) > 0 = checkCoverage pats cs
 >     | otherwise = fail $ "Missing clause: " ++ show c
 
-> matches (Ind p) (Ind t) = matches' p t
-> matches' (App f a) (App f' a') = matches' f f' && matches' a a'
-> matches' (Con _ x _) (Con _ y _) | x == y = True
-> matches' (TyCon x _) (TyCon y _) | x == y = True
-> matches' (P x) (P y) | x == y = True
-> matches' (P (MN ("INFER",_))) _ = True
-> matches' _ (P _) = True
-> matches' x y = x == y
+> matches p t = getMatches p t /= Nothing
 
+> getMatches (Ind p) (Ind t) = matches' p t
+> matches' (App f a) (App f' a') = do fm <- matches' f f'
+>                                     am <- matches' a a'
+>                                     return $ (fm ++ am)
+> matches' (Con _ x _) (Con _ y _) | x == y = return []
+> matches' (TyCon x _) (TyCon y _) | x == y = return []
+> matches' (P x) (P y) | x == y = return [(y, P x)]
+> matches' t (P n) = return [(n,t)]
+> matches' (P nm@(MN ("INFER",_))) t = return []
+> matches' x y = if x == y then return [] else fail "With pattern does not match parent"
 
-> expandClause :: Monad m => Gamma Name -> RawScheme -> m [RawScheme]
+
+> expandClause :: Gamma Name -> RawScheme -> IvorM [RawScheme]
 > expandClause gam (RSch ps ret) = do
 >   expanded <- mapM (expandCon gam) ps
 >   return $ map (\p -> RSch p ret) (combine expanded)
 
 Remove the clauses which can't possibly be type correct.
 
-> validClauses :: Monad m => Gamma Name -> Name -> Indexed Name ->
->                 [RawScheme] -> m [(Indexed Name, Indexed Name)]
+> validClauses :: Gamma Name -> Name -> Indexed Name ->
+>                 [RawScheme] -> IvorM [(Indexed Name, Indexed Name)]
 > validClauses gam fn ty cs = do
 >     -- add fn:ty to the context as an axiom
 >     checkValid gam [] cs
@@ -277,8 +342,8 @@
 >        checkValid gam acc ((RSch c r):cs)
 >           = do let app = mkapp (Var fn) c
 >                case typecheck gam app of
->                  Nothing -> checkValid gam acc cs
->                  Just (v,t) -> checkValid gam ((v,t):acc) cs
+>                  Right (v,t) -> checkValid gam ((v,t):acc) cs
+>                  _ -> checkValid gam acc cs
 
 
 Return true if the given pattern clause is the most specific in a list
@@ -310,7 +375,7 @@
 Given a raw term, recursively expand all of its arguments which are in
 constructor form
 
-> expandCon :: Monad m => Gamma Name -> Raw -> m [Raw]
+> expandCon :: Gamma Name -> Raw -> IvorM [Raw]
 > expandCon gam r = do
 >     let f = getappfun r
 >     let as = getappargs r
diff --git a/Ivor/Primitives.lhs b/Ivor/Primitives.lhs
--- a/Ivor/Primitives.lhs
+++ b/Ivor/Primitives.lhs
@@ -58,7 +58,7 @@
 > -- | Add primitive types for Int, Float and String, and some
 > -- primitive operations [add,sub,mult,div][int,float] and concat.
 
-> addPrimitives :: Monad m => Context -> m Context
+> addPrimitives :: Context -> TTM Context
 > addPrimitives c = do c <- addPrimitive c (name "Int")
 >                      c <- addPrimitive c (name "Float")
 >                      c <- addPrimitive c (name "String")
@@ -127,7 +127,7 @@
 > parseInt = lexeme $ fmap read (many1 digit)
 
 > -- | Parse a term including primitives
-> parsePrimTerm :: Monad m => String -> m ViewTerm
+> parsePrimTerm :: String -> TTM ViewTerm
 > parsePrimTerm str
 >     = case parse (do t <- pTerm (Just parsePrimitives) ; eof ; return t) 
 >                  "(input)" str of
diff --git a/Ivor/Shell.lhs b/Ivor/Shell.lhs
--- a/Ivor/Shell.lhs
+++ b/Ivor/Shell.lhs
@@ -50,9 +50,8 @@
 > newShell ctxt = Shell Nothing "> " False ctxt "" [] [] [] Nothing []
 
 > -- | Update the context in a shell
-> updateShell :: Monad m =>
->                (Context -> m Context) -- ^ Function to update context
->                -> ShellState -> m ShellState
+> updateShell :: (Context -> TTM Context) -- ^ Function to update context
+>                -> ShellState -> TTM ShellState
 > updateShell fctxt (Shell r p f c resp tacs coms imp ext path)
 >     = do ctxt <- fctxt c
 >          return (Shell r p f ctxt resp tacs coms imp ext path)
@@ -96,7 +95,7 @@
  output st = hPutStr (outputstream st)
  outputLn st x = output st (x++"\n")
 
-> runCommand :: (Monad m) => Command -> ShellState -> m ShellState
+> runCommand :: Command -> ShellState -> TTM ShellState
 > runCommand (Def nm tm) st = do let (_, tm') = addImplicit (context st) tm
 >                                ctxt <- addDef (context st) (name nm) tm'
 >                                return st { context = ctxt }
@@ -148,9 +147,9 @@
 >                       return (respondLn st (show (whnf (context st) tm)))
 > runCommand (Print n) st = do
 >     case (getDef (context st) (name n)) of
->       Just tm -> return (respondLn st (show (view tm)))
+>       Right tm -> return (respondLn st (show (view tm)))
 >       _ -> case (getPatternDef (context st) (name n)) of
->             Just (_,pats) -> return (respondLn st (printPats pats))
+>             Right (_,pats) -> return (respondLn st (printPats pats))
 >             _ -> do tm <- check (context st) n
 >                     case view tm of
 >                         (Name TypeCon _) -> return (respondLn st "Type constructor")
@@ -297,9 +296,10 @@
 >     (resp, ctxt) <- fn arg (context st)
 >     let st' = st { context = ctxt, response = resp }
 >     return st'
-> process x st = processInput x st
+> process x st = do let (Right r) = processInput x st
+>                   return r
 
-> processInput :: Monad m => Result Input -> ShellState -> m ShellState
+> processInput :: Result Input -> ShellState -> TTM ShellState
 > processInput (Failure err) st = return $ respondLn st err
 > processInput (Success (Command cmd)) st = runCommand cmd st
 > processInput (Success (Tactic goal tac)) st
@@ -324,7 +324,7 @@
 >  where
 >   ctxt = context st
 >   showGoalState :: Goal -> String
->   showGoalState g = let (Just gd) = goalData ctxt True g
+>   showGoalState g = let (Right gd) = goalData ctxt True g
 >                         env = bindings gd
 >                         ty = goalType gd
 >                         nm = goalName gd in
@@ -365,7 +365,7 @@
 >        return st
 
 > -- | Send a command directly to a shell
-> sendCommand :: Monad m => String -> ShellState -> m ShellState
+> sendCommand :: String -> ShellState -> TTM ShellState
 > sendCommand str st = processInput
 >                        (parseInput (extensions st)
 >                                    (gettacs (usertactics st))
@@ -383,7 +383,7 @@
 >                                    (map fst (usercommands st)) str) $
 >                          clearResponse st
 
-> gettacs :: [(String, String -> Goal -> Context -> IO Context)] -> [String]
+> gettacs :: [(String, String -> Goal -> Context -> TTM Context)] -> [String]
 > gettacs = map fst
 
 > -- | Get the install prefix of the library
diff --git a/Ivor/ShellParser.lhs b/Ivor/ShellParser.lhs
--- a/Ivor/ShellParser.lhs
+++ b/Ivor/ShellParser.lhs
@@ -126,9 +126,20 @@
 >     = do name <- identifier;
 >          when (name /= nm) $ fail $ show nm ++ " & " ++ show name ++ " do not match"
 >          args <- many (pNoApp ext)
->          lchar '=' ;
->          ret <- pTerm ext
->          return $ PClause args ret
+>          try (pclauseret args ext) <|> pclausewith nm args ext
+
+> pclauseret :: [ViewTerm] -> Maybe (Parser ViewTerm) -> Parser PClause
+> pclauseret args ext = do lchar '='
+>                          ret <- pTerm ext
+>                          return $ PClause args ret
+
+> pclausewith :: String -> [ViewTerm] -> Maybe (Parser ViewTerm) -> Parser PClause
+> pclausewith nm args ext = do lchar '|'
+>                              scr <- pTerm ext
+>                              lchar '{'
+>                              pats <- ppatterns nm ext
+>                              lchar '}'
+>                              return $ PWithClause args scr pats
 
 > ppatterns :: String -> Maybe (Parser ViewTerm) -> Parser Patterns
 > ppatterns name ext
diff --git a/Ivor/ShellState.lhs b/Ivor/ShellState.lhs
--- a/Ivor/ShellState.lhs
+++ b/Ivor/ShellState.lhs
@@ -23,7 +23,7 @@
 >                          context :: !Context,
 >                          -- | Get reply from last shell command
 >                          response :: String,
->                          usertactics :: forall m.Monad m => [(String, String -> Goal -> Context -> m Context)],
+>                          usertactics :: [(String, String -> Goal -> Context -> TTM Context)],
 >                          usercommands :: [(String, String -> Context -> IO (String, Context))],
 >                          imported :: [String],
 >                          extensions :: Maybe (Parser ViewTerm),
diff --git a/Ivor/State.lhs b/Ivor/State.lhs
--- a/Ivor/State.lhs
+++ b/Ivor/State.lhs
@@ -16,6 +16,7 @@
 > import Ivor.Tactics as Tactics
 > import Ivor.Display
 > import Ivor.Unify
+> import Ivor.Errors
 
 > import System.Environment
 > import Data.List
@@ -72,7 +73,7 @@
 
 Take a data type definition and add constructors and elim rule to the context.
 
-> doData :: Monad m => Bool -> IState -> Name -> RawDatatype -> m IState
+> doData :: Bool -> IState -> Name -> RawDatatype -> IvorM IState
 > doData elim st n r = do
 >            let ctxt = defs st
 >            dt <- if elim then checkType (defs st) r -- Make iota schemes
@@ -110,7 +111,7 @@
 >                               ctxt
 >            return newdefs
 
-> doMkData :: Monad m => Bool -> IState -> Datadecl -> m IState
+> doMkData :: Bool -> IState -> Datadecl -> IvorM IState
 > doMkData elim st (Datadecl n ps rawty cs) 
 >     = do (gty,_) <- checkIndices (defs st) ps [] rawty
 >          let ty = forget (normalise (defs st) gty)
@@ -129,7 +130,7 @@
 >        stripps 0 t = t
 >        stripps n (RBind _ _ sc) = stripps (n-1) sc
 
-> suspendProof :: Monad m => IState -> m IState
+> suspendProof :: IState -> IvorM IState
 > suspendProof st = do case proofstate st of
 >                        (Just prf) -> do
 >                          let olddefs = defs st
@@ -144,7 +145,7 @@
 >               return $ (x, G (Partial (Ind v) q) (finalise (Ind ty)) defplicit)
 > suspendFrom _ _ _ = fail "Not a suspendable proof"
 
-> resumeProof :: Monad m => IState -> Name -> m IState
+> resumeProof :: IState -> Name -> IvorM IState
 > resumeProof st n = case (proofstate st) of
 >      Nothing ->
 >          case glookup n (defs st) of
@@ -170,7 +171,7 @@
 e.g. adding z:C x to foo : (x:A)(y:B)Z = [x:A][y:B]H
  becomes foo : (x:A)(z:C x)(y:B) = [x:A][z:C x][y:B]H.
 
-> addArg :: Monad m => IState -> Name -> TT Name -> m IState
+> addArg :: IState -> Name -> TT Name -> IvorM IState
 > addArg st n ty =
 >     case proofstate st of
 >         Just (Ind (Bind n (B (Guess v) t) sc)) -> do
diff --git a/Ivor/TT.lhs b/Ivor/TT.lhs
--- a/Ivor/TT.lhs
+++ b/Ivor/TT.lhs
@@ -17,7 +17,9 @@
 >               checkCtxt,converts,
 >               Ivor.TT.compile,
 >               -- * Exported view of terms
->               module VTerm, IsTerm, IsData,
+>               module VTerm, IsTerm, IsData, 
+>               -- * Errors
+>               TTError(..), ttfail, getError, TTM,
 >               -- * Definitions and Theorems
 >               addDef,addTypedDef,addData,addDataNoElim,
 >               addAxiom,declare,declareData,
@@ -110,11 +112,13 @@
 > import Ivor.Compiler as Compiler
 > import Ivor.CodegenC
 > import Ivor.PatternDefs
+> import Ivor.Errors
 
 > import Data.List
 > import Debug.Trace
 > import Data.Typeable
 > import Control.Monad(when)
+> import Control.Monad.Error(Error,noMsg,strMsg)
 
 > -- | Abstract type representing state of the system.
 > newtype Context = Ctxt IState
@@ -135,7 +139,7 @@
 
 > -- |A tactic is any function which manipulates a term at the given goal
 > -- binding. Tactics may fail, hence the monad.
-> type Tactic = forall m.Monad m => Goal -> Context -> m Context
+> type Tactic = Goal -> Context -> TTM Context
 
 > -- | Initialise a context, with no data or definitions and an
 > -- empty proof state.
@@ -144,17 +148,17 @@
 
 > class IsTerm a where
 >     -- | Typecheck a term
->     check :: Monad m => Context -> a -> m Term
->     raw :: Monad m => a -> m Raw
+>     check :: Context -> a -> TTM Term
+>     raw :: a -> TTM Raw
 
 > class IsData a where
 >     -- Add a data type with case and elim rules an elimination rule
->     addData :: Monad m => Context -> a -> m Context
+>     addData :: Context -> a -> TTM Context
 >     addData ctxt x = addData' True ctxt x
 >     -- Add a data type without an elimination rule
->     addDataNoElim :: Monad m => Context -> a -> m Context
+>     addDataNoElim :: Context -> a -> TTM Context
 >     addDataNoElim ctxt x = addData' False ctxt x
->     addData' :: Monad m => Bool -> Context -> a -> m Context
+>     addData' :: Bool -> Context -> a -> TTM Context
 
 > instance IsTerm Term where
 >     check _ tm = return tm
@@ -175,10 +179,53 @@
 > instance IsTerm Raw where
 >     check (Ctxt st) t = do
 >        case (typecheck (defs st) t) of
->           (Success (t, ty)) -> return $ Term (t,ty)
->           (Failure err) -> fail err
+>           (Right (t, ty)) -> return $ Term (t,ty)
+>           (Left err) -> tt $ ifail err
 >     raw t = return t
 
+> data TTError = CantUnify ViewTerm ViewTerm
+>              | NotConvertible ViewTerm ViewTerm
+>              | Message String
+>              | Unbound ViewTerm ViewTerm ViewTerm ViewTerm [Name]
+>              | NoSuchVar Name
+>              | ErrContext String TTError
+
+> instance Show TTError where
+>     show (CantUnify t1 t2) = "Can't unify " ++ show t1 ++ " and " ++ show t2
+>     show (NotConvertible t1 t2) = show t1 ++ " and " ++ show t2 ++ " are not convertible"
+>     show (Message s) = s
+>     show (Unbound clause clty rhs rhsty ns) 
+>        = show ns ++ " unbound in clause " ++ show clause ++ " : " ++ show clty ++ 
+>                     " = " ++ show rhs
+>     show (NoSuchVar n) = "No such name as " ++ show n
+>     show (ErrContext c err) = c ++ show err
+
+> instance Error TTError where
+>     noMsg = Message "Ivor Error"
+>     strMsg s = Message s
+
+> type TTM = Either TTError
+
+> ttfail :: String -> TTM a
+> ttfail s = Left (Message s)
+
+> tt :: IvorM a -> TTM a
+> tt (Left err) = Left (getError err)
+> tt (Right v) = Right v
+
+> getError :: IError -> TTError
+> getError (ICantUnify l r) = CantUnify (view (Term (l, Ind TTCore.Star))) (view (Term (r, Ind TTCore.Star)))
+> getError (INotConvertible l r) = NotConvertible (view (Term (l, Ind TTCore.Star))) (view (Term (r, Ind TTCore.Star)))
+> getError (IMessage s) = Message s
+> getError (IUnbound clause clty rhs rhsty names) 
+>              = Unbound (view (Term (clause, Ind TTCore.Star)))
+>                        (view (Term (clty, Ind TTCore.Star)))
+>                        (view (Term (rhs, Ind TTCore.Star)))
+>                        (view (Term (rhsty, Ind TTCore.Star)))
+>                        names
+> getError (INoSuchVar n) = NoSuchVar n
+> getError (IContext s e) = ErrContext s (getError e)
+
 > -- | Quickly convert a 'ViewTerm' into a real 'Term'.
 > -- This is dangerous; you must know that typechecking will succeed,
 > -- and the resulting term won't have a valid type, but you will be
@@ -198,7 +245,7 @@
 >             Failure err -> fail err
 
 > instance IsData Inductive where
->     addData' elim (Ctxt st) ind = do st' <- doMkData elim st (datadecl ind)
+>     addData' elim (Ctxt st) ind = do st' <- tt $ doMkData elim st (datadecl ind)
 >                                      return (Ctxt st')
 >       where
 >         datadecl (Inductive n ps inds cty cons) =
@@ -218,6 +265,11 @@
 >                         arguments :: [ViewTerm],
 >                         returnval :: ViewTerm
 >                        }
+>              | PWithClause {
+>                         arguments :: [ViewTerm],
+>                         scrutinee :: ViewTerm,
+>                         patterns :: Patterns
+>                            }
 >    deriving Show
 
 > data Patterns = Patterns [PClause]
@@ -225,8 +277,9 @@
 
 > mkRawClause :: PClause -> RawScheme
 > mkRawClause (PClause args ret) =
->     RSch (map forget args) (forget ret)
-
+>     RSch (map forget args) (RWRet (forget ret))
+> mkRawClause (PWithClause args scr (Patterns rest)) = 
+>     RSch (map forget args) (RWith (forget scr) (map mkRawClause rest))
 
 > -- ^ Convert a term to matchable pattern form; i.e. the only names allowed
 > -- are variables and constructors. Any arbitrary function application is
@@ -239,6 +292,7 @@
 >     toPat gam (VTerm.App f a) = case toPat gam f of
 >                                   Placeholder -> Placeholder
 >                                   apptm -> VTerm.App f (toPat gam a)
+>     toPat gam (Annotation _ a) = toPat gam a
 >     toPat gam _ = Placeholder
 >     matchable gam n
 >        = case lookupval n gam of
@@ -257,18 +311,18 @@
 > -- but can be optionally partial or general recursive.
 > -- Returns the new context, and a list of names which need to be defined
 > -- to complete the definition.
-> addPatternDef :: (IsTerm ty, Monad m) =>
+> addPatternDef :: (IsTerm ty) =>
 >                Context -> Name -> ty -- ^ Type
 >                  -> Patterns -- ^ Definition
 >                -> [PattOpt] -- ^ Options to set which definitions will be accepted
->                -> m (Context, [(Name, ViewTerm)])
+>                -> TTM (Context, [(Name, ViewTerm)])
 > addPatternDef (Ctxt st) n ty pats opts = do
 >         checkNotExists n (defs st)
 >         let ndefs = defs st
 >         inty <- raw ty
 >         let (Patterns clauses) = pats
->         (pmdef, fty, newnames, tot) 
->                <- checkDef ndefs n inty (map mkRawClause clauses)
+>         (pmdefs, newnames, tot) 
+>               <- tt $ checkDef ndefs n inty (map mkRawClause clauses)
 >                            (not (elem Ivor.TT.Partial opts))
 >                            (not (elem GenRec opts))
 >         (ndefs',vnewnames) 
@@ -281,13 +335,17 @@
 >                                                  extend g (n, G Unreducible t 0))
 >                                               ndefs newnames
 >                              return (ngam, vnew)
->         newdefs <- gInsert n (G (PatternDef pmdef tot) fty defplicit) ndefs'
+>         newdefs <- insertAll pmdefs ndefs' tot
 >         return (Ctxt st { defs = newdefs }, vnewnames)
+>   where insertAll [] gam tot = return gam
+>         insertAll ((nm, def, ty):xs) gam tot = 
+>             do gam' <- gInsert nm (G (PatternDef def tot) ty defplicit) gam
+>                insertAll xs gam' tot
 
 > -- |Add a new definition, with its type to the global state.
 > -- These definitions can be recursive, so use with care.
-> addTypedDef :: (IsTerm term, IsTerm ty, Monad m) =>
->                Context -> Name -> term -> ty -> m Context
+> addTypedDef :: (IsTerm term, IsTerm ty) =>
+>                Context -> Name -> term -> ty -> TTM Context
 > addTypedDef (Ctxt st) n tm ty = do
 >         checkNotExists n (defs st)
 >         (Term (inty,_)) <- Ivor.TT.check (Ctxt st) ty
@@ -296,7 +354,7 @@
 >         let ctxt = defs st
 >         term <- raw tm
 >         case (checkAndBind tmp [] term (Just inty)) of
->              (Success (v,t@(Ind sc),_)) -> do
+>              (Right (v,t@(Ind sc),_)) -> do
 >                 if (convert (defs st) inty t)
 >                     then (do
 >                       checkBound (getNames (Sc sc)) t
@@ -304,31 +362,31 @@
 >                               -- = Gam ((n,G (Fun [] v) t):ctxt)
 >                       return $ Ctxt st { defs = newdefs })
 >                     else (fail $ "The given type and inferred type do not match, inferred " ++ show t)
->              (Failure err) -> fail err
+>              (Left err) -> tt $ ifail err
 
 
 > -- |Add a new definition to the global state.
-> addDef :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context
+> addDef :: (IsTerm a) => Context -> Name -> a -> TTM Context
 > addDef (Ctxt st) n tm = do
 >         checkNotExists n (defs st)
 >         v <- raw tm
 >         let ctxt = defs st
 >         case (typecheck ctxt v) of
->             (Success (v,t@(Ind sc))) -> do
+>             (Right (v,t@(Ind sc))) -> do
 >                 checkBound (getNames (Sc sc)) t
 >                 newdefs <- gInsert n (G (Fun [] v) t defplicit) ctxt
 >                 -- let newdefs = Gam ((n,G (Fun [] v) t):ctxt)
 >                 return $ Ctxt st { defs = newdefs }
->             (Failure err) -> fail err
+>             (Left err) -> tt $ ifail err
 
-> checkBound :: Monad m => [Name] -> (Indexed Name) -> m ()
+> checkBound :: [Name] -> (Indexed Name) -> TTM ()
 > checkBound [] t = return ()
 > checkBound (nm@(MN ("INFER",_)):ns) t
 >                = fail $ "Can't infer value for " ++ show nm ++ " in " ++ show t
 > checkBound (_:ns) t = checkBound ns t
 
 > -- |Forget a definition and all following definitions.
-> forgetDef :: Monad m => Context -> Name -> m Context
+> forgetDef :: Context -> Name -> TTM Context
 > forgetDef (Ctxt st) n = fail "Not any more..."
 
 do let olddefs = defs st
@@ -340,8 +398,8 @@
 
 > -- |Add the general recursion elimination rule, thus making all further
 > -- definitions untrustworthy :).
-> addGenRec :: Monad m => Context -> Name -- ^ Name to give recursion rule
->                      -> m Context
+> addGenRec :: Context -> Name -- ^ Name to give recursion rule
+>                      -> TTM Context
 > addGenRec (Ctxt st) n
 >     = do checkNotExists n (defs st)
 >          (Ctxt tmpctxt) <- addAxiom (Ctxt st) n
@@ -351,17 +409,17 @@
 >          general <- raw $ "[P:*][meth_general:(p:P)P](meth_general (" ++ 
 >                            show n ++ " P meth_general))"
 >          case (typecheck tmp general) of
->              (Success (v,t)) -> do
+>              (Right (v,t)) -> do
 >                 -- let newdefs = Gam ((n,G (Fun [] v) t):ctxt)
 >                 newdefs <- gInsert n (G (Fun [] v) t defplicit) ctxt
 >                 let scs = lift n (levelise (normalise (emptyGam) v))
 >                 return $ Ctxt st { defs = newdefs }
->              (Failure err) -> fail $ "Can't happen (general): "++err
+>              (Left err) -> ttfail $ "Can't happen (general): "++ show err
 
 > -- | Add the heterogenous (\"John Major\") equality rule and its reduction
-> addEquality :: Monad m => Context -> Name -- ^ Name to give equality type
+> addEquality :: Context -> Name -- ^ Name to give equality type
 >             -> Name -- ^ Name to give constructor
->             -> m Context
+>             -> TTM Context
 > addEquality ctxt@(Ctxt st) ty con = do
 >     checkNotExists ty (defs st)
 >     checkNotExists con (defs st)
@@ -371,7 +429,7 @@
 >     rcrule <- eqElimType (show ty) (show con) "Case"
 >     rischeme <- eqElimSch (show con)
 >     let rdata = (RData rtycon [rdatacon] 2 rerule rcrule [rischeme] [rischeme])
->     st <- doData True st ty rdata
+>     st <- tt $ doData True st ty rdata
 >     return $ Ctxt st
 
 > -- eqElim : (A:*)(a:A)(b:A)(q:JMEq A A a a)
@@ -400,21 +458,21 @@
 >                     mrefl <- raw "meth_refl"
 >                     arg <- raw $ refl ++ " A a"
 >                     ret <- raw "meth_refl"
->                     return $ RSch [aty,a,b,arg,phi,mrefl] ret
+>                     return $ RSch [aty,a,b,arg,phi,mrefl] (RWRet ret)
 
 > -- | Declare a name which is to be defined later
-> declare :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context
+> declare :: (IsTerm a) => Context -> Name -> a -> TTM Context
 > declare ctxt n tm = addUn Undefined ctxt n tm
 
 > -- | Declare a type constructor which is to be defined later
-> declareData :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context
+> declareData :: (IsTerm a) => Context -> Name -> a -> TTM Context
 > declareData ctxt@(Ctxt st) n tm = do
 >   let gamma = defs st
 >   Term (ty, _) <- Ivor.TT.check ctxt tm
 >   addUn (TCon (arity gamma ty) NoConstructorsYet) ctxt n tm
 
 > -- | Add a new axiom to the global state.
-> addAxiom :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context
+> addAxiom :: (IsTerm a) => Context -> Name -> a -> TTM Context
 > addAxiom ctxt n tm = addUn Unreducible ctxt n tm
 
 > addUn und (Ctxt st) n tm = do
@@ -422,18 +480,18 @@
 >        t <- raw tm
 >        let Gam ctxt = defs st
 >        case (typecheck (defs st) t) of
->           (Success (t, ty)) ->
->              do checkConv (defs st) ty (Ind TTCore.Star) "Not a type"
+>           (Right (t, ty)) ->
+>              do tt $ checkConv (defs st) ty (Ind TTCore.Star) (IMessage "Not a type")
 >                 -- let newdefs = Gam ((n, (G und (finalise t))):ctxt)
 >                 newdefs <- gInsert n (G und (finalise t) defplicit) (Gam ctxt)
 >                 return $ Ctxt st { defs = newdefs }
->           (Failure err) -> fail err
+>           (Left err) -> tt $ ifail err
 
 > -- | Add a new primitive type. This should be done in assocation with
 > -- creating an instance of 'ViewConst' for the type, and creating appropriate
 > -- primitive functions.
-> addPrimitive :: Monad m => Context -> Name -- ^ Type name
->                 -> m Context
+> addPrimitive :: Context -> Name -- ^ Type name
+>                 -> TTM Context
 > addPrimitive (Ctxt st) n = do
 >        checkNotExists n (defs st)
 >        let Gam ctxt = defs st
@@ -444,8 +502,8 @@
 
 > -- | Add a new binary operator on constants. Warning: The type you give
 > -- is not checked!
-> addBinOp :: (ViewConst a, ViewConst b, ViewConst c, IsTerm ty, Monad m) =>
->             Context -> Name -> (a->b->c) -> ty -> m Context
+> addBinOp :: (ViewConst a, ViewConst b, ViewConst c, IsTerm ty) =>
+>             Context -> Name -> (a->b->c) -> ty -> TTM Context
 > addBinOp (Ctxt st) n f tyin = do
 >        checkNotExists n (defs st)
 >        Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin
@@ -472,8 +530,8 @@
 
 > -- | Add a new binary function on constants. Warning: The type you give
 > -- is not checked!
-> addBinFn :: (ViewConst a, ViewConst b, IsTerm ty, Monad m) =>
->             Context -> Name -> (a->b->ViewTerm) -> ty -> m Context
+> addBinFn :: (ViewConst a, ViewConst b, IsTerm ty) =>
+>             Context -> Name -> (a->b->ViewTerm) -> ty -> TTM Context
 > addBinFn (Ctxt st) n f tyin = do
 >        checkNotExists n (defs st)
 >        Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin
@@ -487,7 +545,7 @@
 >              = case cast x of
 >                   Just x' -> case cast y of
 >                      Just y' -> case Ivor.TT.check (Ctxt st) $ f x' y' of
->                          Just (Term (Ind v,_)) ->
+>                          Right (Term (Ind v,_)) ->
 >                              Just $ nf (emptyGam) (VG []) [] False v
 >                      Nothing -> Nothing
 >                   Nothing -> Nothing
@@ -497,7 +555,7 @@
 >              = case cast x of
 >                   Just x' -> case cast y of
 >                      Just y' -> case Ivor.TT.check (Ctxt st) $ f x' y' of
->                          Just (Term (Ind v,_)) ->
+>                          Right (Term (Ind v,_)) ->
 >                              Just v
 >                      Nothing -> Nothing
 >                   Nothing -> Nothing
@@ -507,8 +565,8 @@
 > -- | Add a new primitive function on constants, usually used for converting
 > -- to some form which can be examined in the type theory itself.
 > -- Warning: The type you give is not checked!
-> addPrimFn :: (ViewConst a, IsTerm ty, Monad m) =>
->             Context -> Name -> (a->ViewTerm) -> ty -> m Context
+> addPrimFn :: (ViewConst a, IsTerm ty) =>
+>             Context -> Name -> (a->ViewTerm) -> ty -> TTM Context
 > addPrimFn (Ctxt st) n f tyin = do
 >        checkNotExists n (defs st)
 >        Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin
@@ -521,28 +579,28 @@
 >          mkfun (Snoc Empty (MR (RdConst x)))
 >              = case cast x of
 >                   Just x' -> case Ivor.TT.check (Ctxt st) $ f x' of
->                                  Just (Term (Ind v,_)) ->
+>                                  Right (Term (Ind v,_)) ->
 >                                      Just $ nf (emptyGam) (VG []) [] False v
->                                  Nothing -> Nothing
+>                                  _ -> Nothing
 >                   Nothing -> Nothing
 >          mkfun _ = Nothing
 >          mktt :: [TT Name] -> Maybe (TT Name)
 >          mktt [Const x]
 >               = case cast x of
 >                   Just x' -> case Ivor.TT.check (Ctxt st) $ f x' of
->                                  Just (Term (Ind v,_)) ->
+>                                  Right (Term (Ind v,_)) ->
 >                                      Just v
->                                  Nothing -> Nothing
+>                                  _ -> Nothing
 >                   Nothing -> Nothing
 >          mktt _ = Nothing
 
 > -- | Add a new externally defined function.
 > -- Warning: The type you give is not checked!
-> addExternalFn :: (IsTerm ty, Monad m) =>
+> addExternalFn :: (IsTerm ty) =>
 >                  Context -> Name -> Int -- ^ arity
 >                  -> ([ViewTerm] -> Maybe ViewTerm) -- ^ The function, which must
 >                     -- accept a list of the right length given by arity.
->                  -> ty -> m Context
+>                  -> ty -> TTM Context
 > addExternalFn (Ctxt st) n arity f tyin = do
 >        checkNotExists n (defs st)
 >        Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin
@@ -557,9 +615,9 @@
 >               else case runf xs of
 >                      Just res ->
 >                          case (Ivor.TT.check (Ctxt st) res) of
->                             Nothing -> Nothing
->                             Just (Term (Ind tm, _)) ->
+>                             Right (Term (Ind tm, _)) ->
 >                                 Just $ nf (emptyGam) (VG []) [] False tm
+>                             _ -> Nothing
 >                      Nothing -> Nothing
 >          mktt :: [TT Name] -> Maybe (TT Name)
 >          mktt xs
@@ -567,9 +625,9 @@
 >               else case f (map viewtt xs) of
 >                      Just res ->
 >                          case (Ivor.TT.check (Ctxt st) res) of
->                             Nothing -> Nothing
->                             Just (Term (Ind tm, _)) ->
+>                             Right (Term (Ind tm, _)) ->
 >                                 Just tm
+>                             _ -> Nothing
 >                      Nothing -> Nothing
 
 Using 'Star' here is a bit of a hack; I don't want to export vt from
@@ -597,11 +655,11 @@
 >                                           (Forall n Placeholder tm)
 
 > -- |Begin a new proof.
-> theorem :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context
+> theorem :: (IsTerm a) => Context -> Name -> a -> TTM Context
 > theorem (Ctxt st) n tm = do
 >        checkNotExists n (defs st)
 >        rawtm <- raw tm
->        (tv,tt) <- tcClaim (defs st) rawtm
+>        (tv,tt) <- tt $ tcClaim (defs st) rawtm
 >        case (proofstate st) of
 >            Nothing -> do
 >                       let thm = Tactics.theorem n tv
@@ -615,12 +673,12 @@
 > -- |Begin a new interactive definition.
 > -- Actually, just the same as 'theorem' but this version allows you to
 > -- make recursive calls, which should of course be done with care.
-> interactive :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context
+> interactive :: (IsTerm a) => Context -> Name -> a -> TTM Context
 > interactive (Ctxt st) n tm = do
 >        checkNotExists n (defs st)
 >        (Ctxt st') <- declare (Ctxt st) n tm
 >        rawtm <- raw tm
->        (tv,tt) <- tcClaim (defs st) rawtm
+>        (tv,tt) <- tt $ tcClaim (defs st) rawtm
 >        case (proofstate st) of
 >            Nothing -> do
 >                       let thm = Tactics.theorem n tv
@@ -635,19 +693,19 @@
 > -- to continue the proof.
 > suspend :: Context -> Context
 > suspend (Ctxt st) = case (suspendProof st) of
->                        (Just st') -> Ctxt st'
->                        Nothing -> Ctxt st
+>                        (Right st') -> Ctxt st'
+>                        _ -> Ctxt st
 
 > -- |Resume an unfinished proof, suspending the current one if necessary.
 > -- Fails if there is no such name. Can also be used to begin a
 > -- proof of an identifier previously claimed as an axiom.
 > -- Remember that you will need to 'attack' the goal if you are resuming an
 > -- axiom.
-> resume :: Monad m => Context -> Name -> m Context
+> resume :: Context -> Name -> TTM Context
 > resume ctxt@(Ctxt st) n =
 >     case glookup n (defs st) of
 >         Just ((Ivor.Nobby.Partial _ _),_) -> do let (Ctxt st) = suspend ctxt
->                                                 st' <- resumeProof st n
+>                                                 st' <- tt$ resumeProof st n
 >                                                 return (Ctxt st')
 >         Just (Unreducible,ty) ->
 >             do let st' = st { defs = remove n (defs st) }
@@ -659,7 +717,7 @@
 
 > -- | Freeze a name (i.e., set it so that it does not reduce)
 > -- Fails if the name does not exist.
-> freeze :: Monad m => Context -> Name -> m Context
+> freeze :: Context -> Name -> TTM Context
 > freeze (Ctxt st) n
 >      = case glookup n (defs st) of
 >           Nothing -> fail $ show n ++ " is not defined"
@@ -667,7 +725,7 @@
 
 > -- | Unfreeze a name (i.e., allow it to reduce).
 > -- Fails if the name does not exist.
-> thaw :: Monad m => Context -> Name -> m Context
+> thaw :: Context -> Name -> TTM Context
 > thaw (Ctxt st) n
 >      = case glookup n (defs st) of
 >           Nothing -> fail $ show n ++ " is not defined"
@@ -684,7 +742,7 @@
 > clearSaved (Ctxt st) = Ctxt st { undoState = Nothing }
 
 > -- | Restore a saved state; fails if none have been saved.
-> restore :: Monad m => Context -> m Context
+> restore :: Context -> TTM Context
 > restore (Ctxt st) = case undoState st of
 >                        Nothing -> fail "No saved state"
 >                        (Just st') -> return $ Ctxt st'
@@ -719,7 +777,7 @@
 >                                          eval_nf (defs st) ty)
 
 > -- |Check a term in the context of the given goal
-> checkCtxt :: (IsTerm a, Monad m) => Context -> Goal -> a -> m Term
+> checkCtxt :: (IsTerm a) => Context -> Goal -> a -> TTM Term
 > checkCtxt (Ctxt st) goal tm =
 >     do rawtm <- raw tm
 >        prf <- case proofstate st of
@@ -729,14 +787,14 @@
 >                (Goal x) -> x
 >                DefaultGoal -> head (holequeue st)
 >        case (Tactics.findhole (defs st) (Just h) prf holeenv) of
->          (Just env) -> do t <- Ivor.Typecheck.check (defs st) env rawtm Nothing
+>          (Just env) -> do t <- tt $ Ivor.Typecheck.check (defs st) env rawtm Nothing
 >                           return $ Term t
 >          Nothing -> fail "No such goal"
 >  where holeenv :: Gamma Name -> Env Name -> Indexed Name -> Env Name
 >        holeenv gam hs _ = Tactics.ptovenv hs
 
 > -- |Evaluate a term in the context of the given goal
-> evalCtxt :: (IsTerm a, Monad m) => Context -> Goal -> a -> m Term
+> evalCtxt :: (IsTerm a) => Context -> Goal -> a -> TTM Term
 > evalCtxt (Ctxt st) goal tm =
 >     do rawtm <- raw tm
 >        prf <- case proofstate st of
@@ -746,7 +804,7 @@
 >                (Goal x) -> x
 >                DefaultGoal -> head (holequeue st)
 >        case (Tactics.findhole (defs st) (Just h) prf holeenv) of
->          (Just env) -> do (tm, ty) <- Ivor.Typecheck.check (defs st) env rawtm Nothing
+>          (Just env) -> do (tm, ty) <- tt $ Ivor.Typecheck.check (defs st) env rawtm Nothing
 >                           let tnorm = normaliseEnv env (defs st) tm
 >                           return $ Term (tnorm, ty)
 >          Nothing -> fail "No such goal"
@@ -757,8 +815,8 @@
 > -- |Check whether the conversion relation holds between two terms, in the
 > -- context of the given goal
 
-> converts :: (Monad m, IsTerm a, IsTerm b) =>
->             Context -> Goal -> a -> b -> m Bool
+> converts :: (IsTerm a, IsTerm b) =>
+>             Context -> Goal -> a -> b -> TTM Bool
 > converts ctxt@(Ctxt st) goal a b
 >     = do atm <- checkCtxt ctxt goal a
 >          btm <- checkCtxt ctxt goal b
@@ -771,21 +829,21 @@
 >                (Goal x) -> x
 >                DefaultGoal -> head (holequeue st)
 >          case (Tactics.findhole (defs st) (Just h) prf holeenv) of
->                (Just env) -> case checkConvEnv env (defs st) av bv "" of
->                     Just _ -> return True
+>                (Just env) -> case checkConvEnv env (defs st) av bv (IMessage "") of
+>                     Right _ -> return True
 >                     _ -> return False
 >                Nothing -> fail "No such goal"
 >  where holeenv :: Gamma Name -> Env Name -> Indexed Name -> Env Name
 >        holeenv gam hs _ = Tactics.ptovenv hs
 
 > -- |Lookup a definition in the context.
-> getDef :: Monad m => Context -> Name -> m Term
+> getDef :: Context -> Name -> TTM Term
 > getDef (Ctxt st) n = case glookup n (defs st) of
 >                         Just ((Fun _ tm),ty) -> return $ Term (tm,ty)
 >                         _ -> fail "Not a function name"
 
 > -- |Get the type of a definition in the context.
-> getType :: Monad m => Context -> Name -> m Term
+> getType :: Context -> Name -> TTM Term
 > getType (Ctxt st) n = case glookup n (defs st) of
 >                         Just (_,ty) -> return $ Term (ty,Ind TTCore.Star)
 >                         _ -> fail "Not a defined name"
@@ -799,7 +857,7 @@
 > -- | Return the data type with the given name. Note that this knows nothing
 > -- about the difference between parameters and indices; that information
 > -- is discarded after the elimination rule is constructed.
-> getInductive :: Monad m => Context -> Name -> m Inductive
+> getInductive :: Context -> Name -> TTM Inductive
 > getInductive (Ctxt st) n 
 >     = case glookup n (defs st) of
 >         Just (TCon _ (Elims _ _ cons), ty) ->
@@ -812,11 +870,11 @@
 >         getTyType v = VTerm.getReturnType v
 >         getConTypes [] = []
 >         getConTypes (c:cs) = case getType (Ctxt st) c of
->                                Just ty -> (c,view ty):(getConTypes cs)
+>                                Right ty -> (c,view ty):(getConTypes cs)
 
 > -- |Lookup a pattern matching definition in the context. Return the
 > -- type and the pattern definition.
-> getPatternDef :: Monad m => Context -> Name -> m (ViewTerm, Patterns)
+> getPatternDef :: Context -> Name -> TTM (ViewTerm, Patterns)
 > getPatternDef (Ctxt st) n
 >     = case glookup n (defs st) of
 >           Just ((PatternDef pmf _),ty) ->
@@ -847,7 +905,7 @@
 >        = getPD (map fst (getAllTypes ctxt))
 >   where getPD [] = []
 >         getPD (x:xs) = case (getPatternDef ctxt x) of
->                          Just d -> (x,d):(getPD xs)
+>                          Right d -> (x,d):(getPD xs)
 >                          _ -> getPD xs
 
 > -- |Get all the inductive type definitions in the context.
@@ -856,22 +914,23 @@
 >        = getI (map fst (getAllTypes ctxt))
 >   where getI [] = []
 >         getI (x:xs) = case (getInductive ctxt x) of
->                          Just d -> (x,d):(getI xs)
+>                          Right d -> (x,d):(getI xs)
 >                          _ -> getI xs
 
 > getAllDefs :: Context -> [(Name, Term)]
 > getAllDefs ctxt = let names = map fst (getAllTypes ctxt) in
->                       map (\ x -> (x, unJust (getDef ctxt x))) names
+>                       map (\ x -> (x, unRight (getDef ctxt x))) names
+>   where unRight (Right r) = r
 
 > -- |Get the names of all of the constructors of an inductive family
-> getConstructors :: Monad m => Context -> Name -> m [Name]
+> getConstructors :: Context -> Name -> TTM [Name]
 > getConstructors (Ctxt st) n
 >      = case glookup n (defs st) of
 >           Just ((TCon _ (Elims _ _ cs)),ty) -> return cs
 >           _ -> fail "Not a type constructor"
 
 > -- |Find out what type of variable the given name is
-> nameType :: Monad m => Context -> Name -> m NameType
+> nameType :: Context -> Name -> TTM NameType
 > nameType (Ctxt st) n 
 >     = case glookup n (defs st) of
 >         Just ((DCon _ _), _) -> return DataCon
@@ -881,14 +940,14 @@
 
 > -- | Get an integer tag for a constructor. Each constructor has a tag
 > -- unique within the data type, which could be used by a compiler.
-> getConstructorTag :: Monad m => Context -> Name -> m Int
+> getConstructorTag :: Context -> Name -> TTM Int
 > getConstructorTag (Ctxt st) n
 >    = case glookup n (defs st) of
 >        Just ((DCon tag _), _) -> return tag
 >        _ -> fail "Not a constructor"
 
 > -- | Get the arity of the given constructor.
-> getConstructorArity :: Monad m => Context -> Name -> m Int
+> getConstructorArity :: Context -> Name -> TTM Int
 > getConstructorArity (Ctxt st) n
 >    = case glookup n (defs st) of
 >        Just ((DCon _ _), Ind ty) -> return (length (getExpected ty))
@@ -900,9 +959,9 @@
 > data Rule = Case | Elim
 
 > -- | Get the pattern matching elimination rule for a type
-> getElimRule :: Monad m => Context -> Name -- ^ Type
+> getElimRule :: Context -> Name -- ^ Type
 >                  -> Rule -- ^ Which rule to get patterns for (case or elim)
->                  -> m Patterns
+>                  -> TTM Patterns
 > getElimRule (Ctxt st) nm r =
 >     case (lookupval nm (defs st)) of
 >       Just (TCon _ (Elims erule crule cons)) ->
@@ -912,7 +971,7 @@
 >             elim <- lookupM rule (eliminators st)
 >             return $ Patterns $ map mkRed (fst $ snd elim)
 >       Nothing -> fail $ (show nm) ++ " is not a type constructor"
->  where mkRed (RSch pats ret) = PClause (map viewRaw pats) (viewRaw ret)
+>  where mkRed (RSch pats (RWRet ret)) = PClause (map viewRaw pats) (viewRaw ret)
 >         -- a reduction will only have variables and applications
 >        viewRaw (Var n) = Name Free n
 >        viewRaw (RApp f a) = VTerm.App (viewRaw f) (viewRaw a)
@@ -948,7 +1007,7 @@
 >                        _ -> True
 
 > -- |Get the current proof term, if we are in the middle of a proof.
-> proofterm :: Monad m => Context -> m Term
+> proofterm :: Context -> TTM Term
 > proofterm (Ctxt st) = case proofstate st of
 >                         Nothing -> fail "No proof in progress"
 >                         Just (Ind (Bind _ (B (Guess v) t) _)) ->
@@ -956,7 +1015,7 @@
 >                         Just t -> fail $ "Proof finished; " ++ show t
 
 > -- |Get the type and context of the given goal, if it exists
-> getGoal :: Monad m => Context -> Goal -> m ([(Name,Term)], Term)
+> getGoal :: Context -> Goal -> TTM ([(Name,Term)], Term)
 > getGoal (Ctxt st) goal =
 >     let h = case goal of
 >                   (Goal x) -> x
@@ -989,9 +1048,9 @@
 
 
 > -- |Get information about a subgoal.
-> goalData :: Monad m => Context -> Bool -- ^ Get all bindings (True), or
+> goalData :: Context -> Bool -- ^ Get all bindings (True), or
 >                                        -- just lambda bindings (False)
->          -> Goal -> m GoalData
+>          -> Goal -> TTM GoalData
 > goalData (Ctxt st) all goal = case proofstate st of
 >         Nothing -> fail "No proof in progress"
 >         (Just prf) ->
@@ -1015,7 +1074,7 @@
 >        getbs (_:xs) = getbs xs
 
 > -- | Get the names and types of all goals
-> subGoals :: Monad m => Context -> m [(Name,Term)]
+> subGoals :: Context -> TTM [(Name,Term)]
 > subGoals (Ctxt st) = case proofstate st of
 >         Nothing -> fail "No proof in progress"
 >         (Just prf) -> return $
@@ -1023,8 +1082,8 @@
 >                         $ Tactics.allholes (defs st) True prf
 
 > -- | Create a name unique in the proof state
-> uniqueName :: Monad m => Context -> Name -- ^ Suggested name
->            -> m Name -- ^ Unique name based on suggested name
+> uniqueName :: Context -> Name -- ^ Suggested name
+>            -> TTM Name -- ^ Unique name based on suggested name
 > uniqueName (Ctxt st) n = case proofstate st of
 >         Nothing -> fail "No proof in progress"
 >         (Just (Ind prf)) -> return $ uniqify n $ getBoundNames (Sc prf)
@@ -1049,7 +1108,7 @@
 
 
 > -- |Lift a finished proof into the context
-> qed :: Monad m => Context -> m Context
+> qed :: Context -> TTM Context
 > qed (Ctxt st)
 >     = do case proofstate st of
 >            Just prf -> do
@@ -1066,12 +1125,12 @@
 >                   Nothing -> False
 >                   _ -> True
 
-> qedLift :: Monad m => Gamma Name -> Bool -> Indexed Name ->
->                       m (Name, Gval Name)
+> qedLift :: Gamma Name -> Bool -> Indexed Name ->
+>                       TTM (Name, Gval Name)
 > qedLift gam freeze
 >             (Ind (Bind x (B (TTCore.Let v) ty) (Sc (P n)))) | n == x =
 >     do let (Ind vnorm) = convNormalise (emptyGam) (finalise (Ind v))
->        verify gam (Ind v)
+>        tt $ verify gam (Ind v)
 >        return $ (x, G (Fun opts (Ind vnorm)) (finalise (Ind ty)) defplicit)
 >   where opts = if freeze then [Frozen] else []
 > qedLift _ _ tm = fail $ "Not a complete proof " ++ show tm
@@ -1140,8 +1199,8 @@
 
 > -- | Apply a sequence of tactics to the default goal. Read the type
 > -- as ['Tactic'] -> 'Tactic'
-> tacs :: Monad m => [Goal -> Context -> m Context] ->
->         Goal -> Context -> m Context
+> tacs :: [Goal -> Context -> TTM Context] ->
+>         Goal -> Context -> TTM Context
 > tacs [] = idTac
 > tacs (t:ts) = \g ctxt -> do ctxt <- t g ctxt
 >                             tacs ts DefaultGoal ctxt
@@ -1157,8 +1216,8 @@
 >     -> Tactic
 > try tac success failure goal ctxt =
 >     case tac goal ctxt of
->         Just ctxt' -> success goal ctxt'
->         Nothing -> failure goal ctxt
+>         Right ctxt' -> success goal ctxt'
+>         _ -> failure goal ctxt
 
 > -- | Tries the left tactic, if that fails try the right one. Shorthand for
 > -- 'try' x 'idTac' y.
@@ -1174,7 +1233,7 @@
 >                     (Goal x) -> x
 >                     DefaultGoal -> head (holequeue st)
 >     let (Just prf) = proofstate st
->     (prf', act) <- Tactics.runtactic (defs st) hole prf tac
+>     (prf', act) <- tt $ Tactics.runtactic (defs st) hole prf tac
 >     let st' = addgoals act st
 >     return $ Ctxt st' { proofstate = Just prf',
 >                         --holequeue = jumpqueue hole
@@ -1233,17 +1292,17 @@
 > -- already have a guess attached after refinement, but the guess will not
 > -- be solved (via 'solve').
 > basicRefine :: IsTerm a => a -> Tactic
-> basicRefine tm = do rawtm <- raw tm
->                     runTac (Tactics.refine rawtm [])
+> basicRefine tm ctxt goal = do rawtm <- raw tm
+>                               runTac (Tactics.refine rawtm []) ctxt goal
 
 > -- | Solve a goal by applying a function with some arguments filled in.
 > -- See 'refine' for details.
 > refineWith :: IsTerm a => a -> [a] -> Tactic
 > refineWith tm args = (refineWith' tm args >=> trySolve) >+> keepSolving
 
-> refineWith' tm args = do rawtm <- raw tm
->                          rawargs <- mapM raw args
->                          runTac (Tactics.refine rawtm rawargs)
+> refineWith' tm args c g = do rawtm <- raw tm
+>                              rawargs <- mapM raw args
+>                              runTac (Tactics.refine rawtm rawargs) c g
 
 > -- | Finalise a goal's solution.
 > solve :: Tactic
@@ -1270,8 +1329,8 @@
 >    where trySolve [] ctxt = return ctxt
 >          trySolve (x:xs) ctxt
 >              = case solve x ctxt of
->                   Just ctxt' -> trySolve xs ctxt'
->                   Nothing -> trySolve xs ctxt
+>                   Right ctxt' -> trySolve xs ctxt'
+>                   _ -> trySolve xs ctxt
 
 -- > keepSolving goal ctxt
 -- >   | not (null (getGoals ctxt)) =
@@ -1284,8 +1343,8 @@
 > fill :: IsTerm a => a -> Tactic
 > fill guess = fill' guess >+> keepSolving
 
-> fill' guess = do rawguess <- raw guess
->                  runTac (Tactics.fill rawguess)
+> fill' guess c g = do rawguess <- raw guess
+>                      runTac (Tactics.fill rawguess) c g
 
 > -- | Remove a solution from a goal.
 > abandon :: Tactic
@@ -1343,15 +1402,15 @@
 > -- | Check that the goal is definitionally equal to the given term,
 > -- and rewrite the goal accordingly.
 > equiv :: IsTerm a => a -> Tactic
-> equiv ty = do rawty <- raw ty
->               runTac (Tactics.equiv rawty)
+> equiv ty c g = do rawty <- raw ty
+>                   runTac (Tactics.equiv rawty) c g
 
 > -- | Abstract over the given term in the goal.
 > generalise :: IsTerm a => a -> Tactic
 > generalise tm = generalise' tm >-> attack
 
-> generalise' tm = do rawtm <- raw tm
->                     runTac (Tactics.generalise rawtm)
+> generalise' tm c g = do rawtm <- raw tm
+>                         runTac (Tactics.generalise rawtm) c g
 
 > -- | Abstract over the given term in the goal, and also all variables
 > -- appearing in the goal whose types depend on it.
@@ -1379,7 +1438,7 @@
 > addArg n ty g ctxt@(Ctxt st)
 >     = do rawty <- raw ty
 >          Term (Ind tm, _) <- checkCtxt ctxt g rawty
->          st' <- Ivor.State.addArg st n tm
+>          st' <- tt $ Ivor.State.addArg st n tm
 >          return $ Ctxt st'
 
 > -- | Replace a term in the goal according to an equality premise. Any
@@ -1396,12 +1455,12 @@
 >         -> Bool -- ^ apply premise backwards (i.e. apply symmetry)
 >         -> Tactic
 > replace eq repl sym tm flip = replace' eq repl sym tm flip >+> attack
-> replace' eq repl sym tm flip =
+> replace' eq repl sym tm flip c g =
 >     do rawtm <- raw tm
 >        raweq <- raw eq
 >        rawrepl <- raw repl
 >        rawsym <- raw sym
->        runTac (Tactics.replace raweq rawrepl rawsym rawtm flip)
+>        runTac (Tactics.replace raweq rawrepl rawsym rawtm flip) c g
 
 > -- | Add an axiom to the global context which would solve the goal,
 > -- and apply it.
@@ -1444,24 +1503,24 @@
 >        -> Tactic
 > by rule = (by' rule >=> attack) >+> keepSolving
 
-> by' rule = do rawrule <- raw rule
->               runTac (Tactics.by rawrule)
+> by' rule c g = do rawrule <- raw rule
+>                   runTac (Tactics.by rawrule) c g
 
 > -- | Apply the appropriate induction rule to the term.
 > induction :: IsTerm a => a -- ^ target of the elimination
 >                -> Tactic
 > induction tm = (induction' tm >=> attack) >+> keepSolving
 
-> induction' tm = do rawtm <- raw tm
->                    runTac (Tactics.casetac True rawtm)
+> induction' tm c g = do rawtm <- raw tm
+>                        runTac (Tactics.casetac True rawtm) c g
 
 > -- | Apply the appropriate case analysis rule to the term.
 > -- Like 'induction', but no induction hypotheses generated.
 > cases :: IsTerm a => a -- ^ target of the case analysis
 >                -> Tactic
 > cases tm = (cases' tm >=> attack) >+> keepSolving
-> cases' tm = do rawtm <- raw tm
->                runTac (Tactics.casetac False rawtm)
+> cases' tm c g = do rawtm <- raw tm
+>                    runTac (Tactics.casetac False rawtm) c g
 
 > -- | Find a trivial solution to the goal by searching through the context
 > -- for a premise which solves it immediately by refinement
@@ -1489,7 +1548,7 @@
 >                       }
 >   deriving Show
 
-> allowedrec :: Monad m => Goal -> Context -> m [RecAllowed]
+> allowedrec :: Goal -> Context -> TTM [RecAllowed]
 > allowedrec g ctxt = do
 >     gd <- goalData ctxt False g
 >     return $ findRec $ bindings gd
@@ -1515,11 +1574,11 @@
 >                     rec <- {- trace (show allowed) $ -} findRec allowed tm
 >                     fill rec g ctxt
 >   where
->     findRec :: Monad m => [RecAllowed] -> Raw -> m ViewTerm
+>     findRec :: [RecAllowed] -> Raw -> TTM ViewTerm
 >     findRec [] tm = fail "This recursive call not allowed"
 >     findRec ((Rec fs nm args hyp):rs) tm =
 >         case mkRec fs nm args hyp tm of
->            Just x -> return x
+>            Right x -> return x
 >            _ -> findRec rs tm
 >     mkRec fs nm args hyp tm = do
 >          let (tmf,tmas) = getfa tm []
diff --git a/Ivor/TTCore.lhs b/Ivor/TTCore.lhs
--- a/Ivor/TTCore.lhs
+++ b/Ivor/TTCore.lhs
@@ -1,4 +1,4 @@
-> {-# OPTIONS_GHC -fglasgow-exts #-}
+> {-# OPTIONS_GHC -fglasgow-exts -XIncoherentInstances #-}
 
 > module Ivor.TTCore where
 
@@ -26,6 +26,7 @@
 >     | RCall RComputation Raw
 >     | RReturn Raw
 >     | RAnnot String -- Debugging hack
+>     | RFileLoc FilePath Int Raw -- For more helpful type error messages
 >     | RStage RStage
 
 > data RComputation = RComp Name [Raw]
@@ -143,19 +144,21 @@
 >     | MN (String,Int)
 >   deriving (Ord, Eq)
 
+> instance Typeable Name where
+>     typeOf n = mkTyConApp (mkTyCon "Name") []
+
 Data declarations and pattern matching
 
- data RawWith = RWith [Raw] 
-              | RWPatt [Raw]
-              | RWNone
-   deriving Show
+> data RawWith = RWith Raw [RawScheme] -- match with an extra arg, add new schemes
+>              | RWRet Raw
+>   deriving Show
 
  data With = With [Indexed n]
            | WPatt [Pattern n]
            | WNone
    deriving Show
 
-> data RawScheme = RSch [Raw] {- RawWith -} Raw
+> data RawScheme = RSch [Raw] RawWith
 >   deriving Show
 
 > data Scheme n = Sch [Pattern n] {- With -} (Indexed n)
@@ -309,6 +312,12 @@
 >                            --if (i<length ctx) then P (ctx!!i)
 >                              --           else V i) t'
 
+> makePsUniq :: TT Name -> TT Name
+> makePsUniq t = vapp (\ (ctx,i) -> P (traceIndex ctx i ("makePs " ++ 
+>                                                        debugTT t))) t
+>                            --if (i<length ctx) then P (ctx!!i)
+>                              --           else V i) t'
+
 > makePsEnv env t = let t' = evalState (uniqifyAllState t) env in
 >                       vapp (\ (ctx,i) -> P (traceIndex ctx i 
 >                                             ("makePsEnv" ++ debugTT t))) t'
@@ -565,6 +574,11 @@
 > getArgs (App f a) = getArgs f ++ [a]
 > getArgs _ = []
 
+> getRawArgs :: Raw -> [Raw]
+> getRawArgs (RApp f a) = getRawArgs f ++ [a]
+> getRawArgs (RFileLoc f l t) = getRawArgs t
+> getRawArgs _ = []
+
 Get the function being applied in an application
 
 > getFun :: TT Name -> TT Name
@@ -649,6 +663,7 @@
 >     (==) (RStage t) (RStage t') = t == t'
 >     (==) RInfer RInfer = True
 >     (==) (RMeta x) (RMeta x') = x == x'
+>     (==) (RFileLoc f l t) (RFileLoc _ _ t') = t == t'
 >     (==) _ _ = False
 
 > instance Eq n => Eq (TT n) where
@@ -726,7 +741,7 @@
 >       fPrec _ (RStar) = "*"
 >       fPrec _ (RInfer) = "_"
 >       fPrec _ (RMeta n) = "?"++forget n
->       fPrec _ (RAnnot t) = t
+>       fPrec p (RFileLoc f l t) = fPrec p t
 >       bracket outer inner str | inner>outer = "("++str++")"
 >                               | otherwise = str
 
@@ -746,11 +761,54 @@
 > instance Show n => Forget (Levelled n) Raw where
 >     forget (Lev t) = forget t
 
-> instance Show n => Forget (TT n) Raw where
+> instance (Show Name) => Forget (TT Name) Raw where
 >     forget t = forgetTT (vapp showV t)
 >      where
 >        showV (ctx,i) | i < length ctx = P (ctx!!i)
 >	               | otherwise = V i
+>        forgetTT (P x) = case (cast x) of
+>                           Just (MN ("INFER",i)) -> RInfer
+>                           _ -> Var $ UN (show x)
+>        forgetTT (V i) = RAnnot $ "v" ++ (show i)
+>        forgetTT (Con t x i) = Var $ UN (show x)
+>        forgetTT (TyCon x i) = Var $ UN (show x)
+>        forgetTT (Meta n i) = RMeta (UN (show n ++ " : " ++ show i))
+>        forgetTT (Elim x) = Var $ UN (show x)
+>        forgetTT (App f a) = RApp (forgetTT f) (forgetTT a)
+>        forgetTT (Bind n (B Lambda t) (Sc sc)) =
+>                    (RBind (UN (show n)) (B Lambda (forget t)) (forget sc))
+>        forgetTT (Bind n (B Pi t) (Sc sc)) =
+>                    (RBind (UN (show n)) (B Pi (forget t)) (forget sc))
+>        forgetTT (Bind n (B MatchAny t) (Sc sc)) =
+>                    (RBind (UN (show n)) (B MatchAny (forget t)) (forget sc))
+>        forgetTT (Bind n (B (Let v) t) (Sc sc)) =
+>                    (RBind (UN (show n)) (B (Let (forget v)) (forget t))
+>                      (forget sc))
+>        forgetTT (Bind n (B Hole t) (Sc sc)) =
+>                    (RBind (UN (show n)) (B Hole (forget t)) (forget sc))
+>        forgetTT (Bind n (B (Guess v) t) (Sc sc)) =
+>                    (RBind (UN (show n)) (B (Guess (forget v)) (forget t))
+>                      (forget sc))
+>        forgetTT (Bind n (B (Pattern v) t) (Sc sc)) =
+>                    (RBind (UN (show n)) (B (Pattern (forget v)) (forget t))
+>                      (forget sc))
+>        forgetTT (Proj n i t) = RAnnot $ (show t)++"!"++(show i)++":"++show n
+>        forgetTT (Label t (Comp n cs)) = RLabel (forgetTT t)
+>                                          (RComp (UN $ show n)
+>                                             (map forgetTT cs))
+>        forgetTT (Call (Comp n cs) t) = RCall (RComp (UN $ show n)
+>                                               (map forgetTT cs))
+>                                                 (forgetTT t)
+>        forgetTT (Return t) = RReturn (forgetTT t)
+>        forgetTT (Stage t) = RStage (forget t)
+>        forgetTT (Const x) = RConst x
+>        forgetTT Star = RStar
+
+> instance (Show n) => Forget (TT n) Raw where
+>     forget t = forgetTT (vapp showV t)
+>      where
+>        showV (ctx,i) | i < length ctx = P (ctx!!i)
+>	               | otherwise = V i
 >        forgetTT (P x) = Var $ UN (show x)
 >        forgetTT (V i) = RAnnot $ "v" ++ (show i)
 >        forgetTT (Con t x i) = Var $ UN (show x)
@@ -802,15 +860,19 @@
 > mkapp f (x:xs) = mkapp (RApp f x) xs
 
 > getargnames (RBind n _ sc) = n:(getargnames sc)
+> getargnames (RFileLoc _ _ t) = getargnames t
 > getargnames _ = []
 
 > getappargs (RApp f a) = getappargs f ++ [a]
+> getappargs (RFileLoc _ _ t) = getappargs t
 > getappargs _ = []
 
 > getappfun (RApp f a) = getappfun f
+> getappfun (RFileLoc _ _ t) = getappfun t
 > getappfun x = x
 
 > getrettype (RBind n (B Pi _) sc) = getrettype sc
+> getrettype (RFileLoc _ _ t) = getrettype t
 > getrettype x = x
 
 > nameOccurs x (Var n) | x == n = True
@@ -823,6 +885,7 @@
 > nameOccurs x (RCall comp r)  = nameOccurs x r || occComp x comp
 > nameOccurs x (RReturn r) = nameOccurs x r
 > nameOccurs x (RStage s) = occStage x s
+> nameOccurs x (RFileLoc f l t) = nameOccurs x t
 > nameOccurs x _ = False
 
 > occComp x (RComp _ rs) = or $ map (nameOccurs x) rs
@@ -833,6 +896,9 @@
 > occStage x (REval r) = nameOccurs x r
 > occStage x (REscape r) = nameOccurs x r
 
+> fileLine (RFileLoc f l t) = Just (f,l)
+> fileLine (RBind n b sc) = fileLine sc
+> fileLine _ = Nothing
 
 > debugTT t = show (forgetTT (vapp showV t))
 >      where
diff --git a/Ivor/Tactics.lhs b/Ivor/Tactics.lhs
--- a/Ivor/Tactics.lhs
+++ b/Ivor/Tactics.lhs
@@ -7,6 +7,7 @@
 > import Ivor.Nobby
 > import Ivor.Gadgets
 > import Ivor.Unify
+> import Ivor.Errors
 
 > import Data.List
 > import Data.Maybe
@@ -27,10 +28,8 @@
 >                   | HideGoal Name
 >    deriving (Show,Eq)
 
-> type Tactic = Monad m => Gamma Name ->
->                          Env Name ->
->                          Indexed Name ->
->                          m (Indexed Name, [TacticAction])
+> type Tactic = Gamma Name -> Env Name ->
+>               Indexed Name -> IvorM (Indexed Name, [TacticAction])
 
 > type HoleFn a = Gamma Name -> Env Name -> Indexed Name -> a
 
@@ -91,8 +90,8 @@
 
 Typecheck a term in the context of the given hole
 
-> holecheck :: Monad m => Name -> Gamma Name -> Indexed Name ->
->              Raw -> m (Indexed Name, Indexed Name)
+> holecheck :: Name -> Gamma Name -> Indexed Name ->
+>              Raw -> IvorM (Indexed Name, Indexed Name)
 > holecheck n gam state raw = case (findhole gam (Just n) state docheck) of
 >                                Nothing -> fail "No such hole binder"
 >                                (Just x) -> x
@@ -108,12 +107,12 @@
 
 FIXME: Why not use a state monad for the unified variables in rt?
 
-> runtactic :: Monad m => Gamma Name -> Name ->
->              Indexed Name -> Tactic -> m (Indexed Name, [TacticAction])
+> runtactic :: Gamma Name -> Name ->
+>              Indexed Name -> Tactic -> IvorM (Indexed Name, [TacticAction])
 > runtactic gam n t tac = runtacticEnv gam [] n t tac
 
-> runtacticEnv :: Monad m => Gamma Name -> Env Name -> Name ->
->                 Indexed Name -> Tactic -> m (Indexed Name, [TacticAction])
+> runtacticEnv :: Gamma Name -> Env Name -> Name ->
+>                 Indexed Name -> Tactic -> IvorM (Indexed Name, [TacticAction])
 > runtacticEnv gam env n (Ind s) tactic =
 >     do (tm, actions) <- (rt env s)
 >        return ((Ind (substNames (mapMaybe mkUnify actions) tm)), actions)
@@ -164,7 +163,7 @@
 
 Tactics by default don't need to return the other holes they solved.
 
-> tacret :: Monad m => Indexed Name -> m (Indexed Name, [TacticAction])
+> tacret :: Indexed Name -> IvorM (Indexed Name, [TacticAction])
 > tacret x = return (x,[])
 
 Sequence two tactics
@@ -179,8 +178,8 @@
 > attempt :: Tactic -> Tactic
 > attempt tac gam env tm =
 >     case tac gam env tm of
->        Just (tm',act) -> return (tm',act)
->        Nothing -> tacret tm
+>        Right (tm',act) -> return (tm',act)
+>        _ -> tacret tm
 
 Create a new theorem ?x:S. x
 
@@ -198,7 +197,7 @@
 > claim :: Name -> Raw -> Tactic -- ?Name:Type.
 > claim x s gam env (Ind t) =
 >     do (Ind sv, st) <- check gam (ptovenv env) s Nothing
->        checkConv gam st (Ind Star) "Type of claim must be *"
+>        checkConv gam st (Ind Star) (IMessage "Type of claim must be *")
 >        return $ (Ind (Bind x (B Hole (makePsEnv (map fst env) sv)) (Sc t)),
 >                      [NextGoal x])
 
@@ -238,8 +237,8 @@
 >        let fty = finalise (Ind ty)
 >        others <- -- trace ("unifying "++show gt++" and "++show ty') $
 >                  case unifyenv (emptyGam) (ptovenv env) fgt fty' of
->                     Nothing -> unifyenv gam (ptovenv env) fgt fty
->                     (Just x) -> return x
+>                     Left _ -> unifyenv gam (ptovenv env) fgt fty
+>                     (Right x) -> return x
 >        -- let newgt = substNames others gt
 >        -- let newgv = substNames others gv
 >        let newgv = gv
@@ -583,7 +582,7 @@
 >     do (Ind goalv,Ind goalt) <- check gam (ptovenv env) goal Nothing
 >        let goalvin = makePsEnv (map fst env) goalv
 >        checkConvEnv env gam (Ind goalv) (finalise (Ind ty))
->                         "Not equivalent to the Goal"
+>                         (IMessage "Not equivalent to the Goal")
 >        tacret $ Ind (Bind x (B Hole goalvin) sc)
 > equiv _ _ _ (Ind (Bind x _ _)) = fail $ "equiv: " ++ show x ++ " Not a hole"
 > equiv _ _ _ _ = fail "equiv: Not a binder, can't happen"
diff --git a/Ivor/Typecheck.lhs b/Ivor/Typecheck.lhs
--- a/Ivor/Typecheck.lhs
+++ b/Ivor/Typecheck.lhs
@@ -1,7 +1,7 @@
 > {-# OPTIONS_GHC -fglasgow-exts #-}
 
 > module Ivor.Typecheck(typecheck, tcClaim,
->                       check, checkAndBind, checkAndBindPair,
+>                       check, checkAndBind, checkAndBindWith, checkAndBindPair,
 >                       convert,
 >                       checkConv, checkConvEnv, pToV, pToV2,
 >                       verify, Gamma) where
@@ -11,6 +11,7 @@
 > import Ivor.Nobby
 > import Ivor.Unify
 > import Ivor.Constant
+> import Ivor.Errors
 
 > import Control.Monad.State
 > import Data.List
@@ -31,16 +32,14 @@
 
  convert g x y = trace ((show (normalise g x)) ++ " & " ++ (show (normalise g y))) $ (normalise g x)==(normalise g y)
 
-> checkConv :: Monad m => Gamma Name -> Indexed Name -> Indexed Name -> 
->              String -> m ()
+> checkConv :: Gamma Name -> Indexed Name -> Indexed Name -> IError -> IvorM ()
 > checkConv g x y err = if convert g x y then return ()
->	                 else fail err
+>	                 else ifail err
 
-> checkConvEnv :: Monad m => Env Name -> Gamma Name -> 
->                 Indexed Name -> Indexed Name -> 
->              String -> m ()
+> checkConvEnv :: Env Name -> Gamma Name -> Indexed Name -> Indexed Name -> 
+>                 IError -> IvorM ()
 > checkConvEnv env g x y err = if convertEnv env g x y then return ()
->                              else fail err
+>                              else ifail err
 
 
 *****
@@ -60,18 +59,18 @@
 Top level typechecking function - takes a context and a raw term,
 returning a pair of a term and its type
 
-> typecheck :: Monad m => Gamma Name -> Raw -> m (Indexed Name,Indexed Name)
+> typecheck :: Gamma Name -> Raw -> IvorM (Indexed Name,Indexed Name)
 > typecheck gamma term = do t <- check gamma [] term Nothing
 >			    return t
 
-> typecheckAndBind :: Monad m => Gamma Name -> Raw -> 
->                     m (Indexed Name,Indexed Name, Env Name)
+> typecheckAndBind :: Gamma Name -> Raw -> 
+>                     IvorM (Indexed Name,Indexed Name, Env Name)
 > typecheckAndBind gamma term = checkAndBind gamma [] term Nothing
 
 Check a term, and return well typed terms with explicit names (i.e. no
 de Bruijn indices)
 
-> tcClaim :: Monad m => Gamma Name -> Raw -> m (Indexed Name,Indexed Name)
+> tcClaim :: Gamma Name -> Raw -> IvorM (Indexed Name,Indexed Name)
 > tcClaim gamma term = do (Ind t, Ind v) <- check gamma [] term Nothing
 >			    {-trace (show t) $-}
 >                         return (Ind (makePs t), Ind (makePs v))
@@ -85,30 +84,39 @@
 >      Bool, -- Inferring types of names (if true)
 >      Env Name, -- Extra bindings, if above is true
 >      -- conversion constraints; remember the environment at the time we tried
->      -- also a string explaining where the constraint came from
->      [(Env Name, Indexed Name, Indexed Name, String)],
+>      -- also the context of where the constraint came from
+>      [(Env Name, Indexed Name, Indexed Name, Maybe FileContext)],
 >      -- Metavariables we've introduce to define later
->      [Name])
+>      [Name],
+>      Maybe FileContext)
 
 > type Level = Int
 
+> data FileContext = FC FilePath Int
+>   deriving Eq
+
+> errCtxt :: Maybe FileContext -> IError -> IError
+> errCtxt (Just (FC f l)) err = IContext (f ++ ":" ++ show l ++ ":") err
+> errCtxt _ err = err
+
+> errCtxtCS :: CheckState -> IError -> IError
+> errCtxtCS (_,_,_,_,_,fc) err = errCtxt fc err
+
 Finishes up type checking by making a substitution from all the conversion
 constraints and applying it to the term and type.
 
-> doConversion :: Monad m =>
->                 Raw -> Gamma Name ->
->                 [(Env Name, Indexed Name, Indexed Name,String)] ->
+> doConversion :: Raw -> Gamma Name ->
+>                 [(Env Name, Indexed Name, Indexed Name,Maybe FileContext)] ->
 >                 Indexed Name -> Indexed Name -> 
->                m (Indexed Name, Indexed Name)
+>                 IvorM (Indexed Name, Indexed Name)
 > doConversion raw gam constraints (Ind tm) (Ind ty) =
 >     -- trace ("Finishing checking " ++ show tm ++ " with " ++ show (length constraints) ++ " equations") $ 
 >           -- Unify twice; first time collect the substitutions, second
 >           -- time do them. Because we don't know what order we can solve
 >           -- constraints in and they might depend on each other...
 >       do let cs = nub constraints
->          (subst, nms) <- {-# SCC "name" #-}
->                          mkSubst $ (map (\x -> (True,x)) cs)
->                                    ++ (map (\x -> (False,x)) (reverse cs))
+>          (subst, nms) <- mkSubst $ (map (\x -> (True,x)) cs) ++
+>                                    (map (\x -> (False,x)) (reverse cs))
 >          let tm' = papp subst tm
 >          let ty' = papp subst ty
 >          return (Ind tm',Ind ty')
@@ -119,14 +127,14 @@
 >             = do acc' <- mkSubstQ acc q
 >                  mkSubst' acc' xs
 >
->          mkSubstQ (s',nms) (ok, (env,Ind x,Ind y,msg))
+>          mkSubstQ (s',nms) (ok, (env,Ind x,Ind y,fc))
 >             = do -- (s',nms) <- mkSubst xs
 >                  let x' = papp s' x
 >                  let (Ind y') = normalise gam (Ind (papp s' y))
->                  uns <- {-# SCC "substUnify" #-}
+>                  uns <- 
 >                         case unifyenvErr ok gam env (Ind x') (Ind y') of
->                           Success x' -> return x'
->                           Failure err -> fail err
+>                           Right x' -> return x'
+>                           Left err -> ifail (errCtxt fc err)
 
                          Failure err -> fail $ err ++"\n" ++ show nms ++"\n" ++ show constraints -- $ -} ++ " Can't convert "++show x'++" and "++show y' ++ "\n" ++ show constraints ++ "\n" ++ show nms
 
@@ -142,50 +150,83 @@
 >          delta n ty n' | n == n' = ty
 >                        | otherwise = P n'
 
-> check :: Monad m => Gamma Name -> Env Name -> Raw -> Maybe (Indexed Name) -> 
->          m (Indexed Name, Indexed Name)
+> check :: Gamma Name -> Env Name -> Raw -> Maybe (Indexed Name) -> 
+>          IvorM (Indexed Name, Indexed Name)
 > check gam env tm mty = do
->   ((tm', ty'), (_,_,_,convs,_)) <- lvlcheck 0 False 0 gam env tm mty
+>   ((tm', ty'), (_,_,_,convs,_,_)) <- lvlcheck 0 False 0 gam env tm mty
 >   tm'' <- doConversion tm gam convs tm' ty'
 >   return tm''
 
-> checkAndBind :: Monad m => Gamma Name -> Env Name -> Raw -> 
+> checkAndBind :: Gamma Name -> Env Name -> Raw -> 
 >                 Maybe (Indexed Name) -> 
->                 m (Indexed Name, Indexed Name, Env Name)
+>                 IvorM (Indexed Name, Indexed Name, Env Name)
 > checkAndBind gam env tm mty = do
->    ((v,t), (_,_,e,convs,_)) <- lvlcheck 0 True 0 gam env tm mty
->    (v',ty') <- doConversion tm gam convs v t
->    return (v',ty',e)
+>    ((v,t), (next,inf,e,convs,_,_)) <- lvlcheck 0 True 0 gam env tm mty
+>    (v'@(Ind vtm),t') <- doConversion tm gam convs v t -- (normalise gam t1') 
+>    return (v',t',e)
 
 
+Check a pattern and an intermediate computation together
+
+> checkAndBindWith :: Gamma Name -> Raw -> Raw -> Name ->
+>                     IvorM (Indexed Name, Indexed Name, Indexed Name, Indexed Name, Env Name)
+> checkAndBindWith gam tm1 tm2 root = do
+>    ((v1,t1), (next, inf, e, bs,_,_)) <- lvlcheck 0 True 0 gam [] tm1 Nothing
+>    -- rename all the 'inferred' things to another generated name,
+>    -- so that they actually get properly checked on the rhs
+>    let realNames = mkNames next
+>    e' <- renameB gam realNames (renameBinders e)
+>    (v1', t1') <- fixupGam gam realNames (v1, t1)
+>    (v1''@(Ind vtm),t1'') <- doConversion tm1 gam bs v1' t1' -- (normalise gam t1') 
+>    -- Drop names out of e' that don't appear in v1'' as a result of the
+>    -- unification.
+>    let namesbound = getNames (Sc vtm)
+>    let ein = orderEnv (filter (\ (n, ty) -> n `elem` namesbound) e')
+>    ((v2,t2), (_, _, e'', bs',metas,_)) <- lvlcheck 0 inf next gam ein tm2 Nothing
+>    (v2',t2') <- doConversion tm2 gam bs' v2 t2 -- (normalise gam t2) 
+>    let retEnv = reverse (ein ++ e'')
+>    if (null metas) 
+>       then return (v1',t1',v2',t2',retEnv)
+>       else fail "Can't have metavariables here"
+
+>  where mkNames 0 = []
+>        mkNames n
+>           = ([],Ind (P (MN ("INFER",n-1))), 
+>                 Ind (P (MN ("T",n-1))), "renaming"):(mkNames (n-1))
+>        renameBinders [] = []
+>        renameBinders (((MN ("INFER",n)),b):bs) 
+>                         = ((MN ("T",n),b):(renameBinders bs))
+>        renameBinders (b:bs) = b:renameBinders bs
+
 Check two things together, with the same environment and variable inference,
 and with the same expected type.
 We need this for checking pattern clauses...
 Return a list of the functions we need to define to complete the definition.
 
-> checkAndBindPair :: Monad m => Gamma Name -> Raw -> Raw -> 
->                     m (Indexed Name, Indexed Name, 
+> checkAndBindPair :: Gamma Name -> Raw -> Raw -> 
+>                     IvorM (Indexed Name, Indexed Name, 
 >                        Indexed Name, Indexed Name, Env Name,
 >                        [(Name, Indexed Name)])
 > checkAndBindPair gam tm1 tm2 = do
->    ((v1,t1), (next, inf, e, bs,_)) <- lvlcheck 0 True 0 gam [] tm1 Nothing
+>    ((v1,t1), (next, inf, e, bs,_,_)) <- lvlcheck 0 True 0 gam [] tm1 Nothing
 >    -- rename all the 'inferred' things to another generated name,
 >    -- so that they actually get properly checked on the rhs
 >    let realNames = mkNames next
 >    e' <- renameB gam realNames (renameBinders e)
 >    (v1', t1') <- fixupGam gam realNames (v1, t1)
->    (v1''@(Ind vtm),t1'') <- {-# SCC "convert1" #-}doConversion tm1 gam bs v1' t1' -- (normalise gam t1') 
+>    (v1''@(Ind vtm),t1'') <- doConversion tm1 gam bs v1' t1' -- (normalise gam t1') 
 >    -- Drop names out of e' that don't appear in v1'' as a result of the
 >    -- unification.
 >    let namesbound = getNames (Sc vtm)
 >    let ein = orderEnv (filter (\ (n, ty) -> n `elem` namesbound) e')
->    ((v2,t2), (_, _, e'', bs',metas)) <- {- trace ("Checking " ++ show tm2 ++ " has type " ++ show t1') $ -} {-# SCC "pairLvlCheck" #-} lvlcheck 0 inf next gam ein tm2 (Just t1')
->    (v2',t2') <- {-# SCC "convert2" #-} doConversion tm2 gam bs' v2 t2 -- (normalise gam t2) 
+>    ((v2,t2), (_, _, e'', bs',metas,_)) <- {- trace ("Checking " ++ show tm2 ++ " has type " ++ show t1') $ -} lvlcheck 0 inf next gam ein tm2 (Just t1')
+>    (v2',t2') <- doConversion tm2 gam bs' v2 t2 -- (normalise gam t2) 
+>    let retEnv = reverse (ein ++ e'')
 >    if (null metas) 
->       then return (v1',t1',v2',t2',e'', [])
+>       then return (v1',t1',v2',t2',retEnv, [])
 >       else do let (Ind v2tt) = v2' 
 >               let (v2'', newdefs) = updateMetas v2tt
->               return (v1',t1',Ind v2'',t2',e'', map (\ (x,y) -> (x, (normalise gam (Ind y)))) newdefs)
+>               return (v1',t1',Ind v2'',t2',retEnv, map (\ (x,y) -> (x, (normalise gam (Ind y)))) newdefs)
 
                if (null newdefs) then 
                   else trace (traceConstraints bs') $ return (v1',t1',Ind v2'',t2',e'', map (\ (x,y) -> (x, Ind y)) newdefs)
@@ -193,7 +234,7 @@
 >  where mkNames 0 = []
 >        mkNames n
 >           = ([],Ind (P (MN ("INFER",n-1))), 
->                 Ind (P (MN ("T",n-1))), "renaming"):(mkNames (n-1))
+>                 Ind (P (MN ("T",n-1))), IMessage "renaming"):(mkNames (n-1))
 >        renameBinders [] = []
 >        renameBinders (((MN ("INFER",n)),b):bs) 
 >                         = ((MN ("T",n),b):(renameBinders bs))
@@ -233,34 +274,32 @@
 
 > inferName n = (MN ("INFER", n))
 
-> lvlcheck :: Monad m => Level -> Bool -> Int -> 
+> lvlcheck :: Level -> Bool -> Int -> 
 >             Gamma Name -> Env Name -> Raw -> 
 >             Maybe (Indexed Name) -> 
->             m ((Indexed Name, Indexed Name), CheckState)
+>             IvorM ((Indexed Name, Indexed Name), CheckState)
 > lvlcheck lvl infer next gamma env tm exp 
->     = do runStateT (tcfixupTop env lvl tm exp) (next, infer, [], [], []) 
+>     = do runStateT (tcfixupTop env lvl tm exp) (next, infer, [], [], [], Nothing) 
 >  where
 
 Do the typechecking, then unify all the inferred terms.
 
 >  tcfixupTop env lvl t exp = do
 >     tm@(_,tmty) <- tc env lvl t exp
->     (next, infer, bindings, errs ,mvs) <- get
+>     (next, infer, bindings, errs ,mvs, fc) <- get
 >     -- First, insert inferred values into the term
 >     tm'@(_,tmty) <- fixup errs tm
 >     -- Then check the resulting type matches the expected type.
 >     if infer then (case exp of
 >              Nothing -> return ()
->              Just expty -> checkConvSt env gamma expty tmty 
->                               $ "Expected type and inferred type do not match: " 
->                               ++ show expty ++ " and " ++ show tmty)
+>              Just expty -> checkConvSt env gamma expty tmty )
 >       else return ()
 >     -- Then fill in any remained inferred values we got by knowing the
 >     -- expected type
->     (next, infer, bindings, errs, mvs) <- get
+>     (next, infer, bindings, errs, mvs, fc) <- get
 >     tm <- fixup errs tm
 >     -- bindings <- fixupB gamma errs bindings
->     put (next, infer, bindings, errs, mvs)
+>     put (next, infer, bindings, errs, mvs, fc)
 >     return tm'
 
 >  tcfixup env lvl t exp = do
@@ -268,10 +307,10 @@
 >     -- case exp of
 >     --   Nothing -> return ()
 >     --   Just expt -> checkConvSt env gamma expt tmty "Type error"
->     (next, infer, bindings, errs, mvs) <- get
+>     (next, infer, bindings, errs, mvs, fc) <- get
 >     tm' <- fixup errs tm
 >     bindings <- (fixupB gamma errs) $! bindings
->     put (next, infer, bindings, errs, mvs)
+>     put (next, infer, bindings, errs, mvs, fc)
 >     return tm'
 
 tc has state threaded through -- state is a tuple of the next name to
@@ -279,13 +318,13 @@
 will later be unified).  Needs an explicit type to help out ghc's
 typechecker...
 
->  tc :: Monad m => Env Name -> Level -> Raw -> Maybe (Indexed Name) ->
->                   StateT CheckState m (Indexed Name, Indexed Name)
+>  tc :: Env Name -> Level -> Raw -> Maybe (Indexed Name) ->
+>        StateT CheckState IvorM (Indexed Name, Indexed Name)
 >  tc env lvl (Var n) exp = do
 >        (rv, rt) <- mkTT (lookupi n env 0) (glookup n gamma)
 >        case exp of
 >           Nothing -> return (rv,rt)
->           Just expt -> do checkConvSt env gamma rt expt $ "Type error"
+>           Just expt -> do checkConvSt env gamma rt expt
 >                           return (rv,rt)
 
 >    where mkTT (Just (i, B _ t)) _ = return (Ind (P n), Ind t)
@@ -305,13 +344,13 @@
 >          lookupi x (_:xs) i = lookupi x xs (i+1)
 
 >          defaultResult = do
->              (next, infer, bindings, errs, mvs) <- get
+>              (next, infer, bindings, errs, mvs, fc) <- get
 >              if infer
 >                 then case exp of
->                        Nothing -> fail $ "No such name as " ++ show n
->                        Just (Ind t) -> do put (next, infer, (n, B Pi t):bindings, errs, mvs)
+>                        Nothing -> lift $ ifail (errCtxt fc (INoSuchVar n))
+>                        Just (Ind t) -> do put (next, infer, (n, B Pi t):bindings, errs, mvs, fc)
 >                                           return (Ind (P n), Ind t)
->                 else fail $ "No such name as " ++ show n
+>                 else lift $ ifail (errCtxt fc (INoSuchVar n))
 
 >  tc env lvl (RApp f a) exp = do
 >     (Ind fv, Ind ft) <- tcfixup env lvl f Nothing
@@ -324,11 +363,11 @@
 >          let sty = (normaliseEnv env emptyGam (Ind s))
 >          let tt = (Bind (MN ("x",0)) (B (Let av) at) (Sc t))
 >          let tmty = (normaliseEnv env emptyGam (Ind tt))
->          checkConvSt env gamma (Ind at) (Ind s) $ "Type error in application of " ++ show fv ++ " : " ++ show a ++ " : " ++ show at ++ ", expected type "++show sty ++ " " ++ show tmty
+>          checkConvSt env gamma (Ind at) (Ind s)
 >          return (Ind (App fv av), tmty)
 >        (_, (Ind (Bind _ (B Pi s) (Sc t)))) -> do
 >          (Ind av,Ind at) <- tcfixup env lvl a (Just (Ind s))
->          checkConvSt env gamma (Ind at) (Ind s) $ "Type error: " ++ show a ++ " : " ++ show at ++ ", expected type "++show s -- ++" "++show env
+>          checkConvSt env gamma (Ind at) (Ind s)
 >          let tt = (Bind (MN ("x",0)) (B (Let av) at) (Sc t))
 >          let tt' = (normaliseEnv env gamma (Ind tt))
 >          return (Ind (App fv av), (normaliseEnv env gamma (Ind tt)))
@@ -336,10 +375,14 @@
 >     return (rv,rt)
 >     case exp of
 >        Nothing -> return (rv,rt)
->        Just expt -> do checkConvSt env gamma rt expt $ "Type error"
+>        Just expt -> do checkConvSt env gamma rt expt
 >                        return (rv,rt)
->  tc env lvl (RConst x) _ = tcConst x
+>  tc env lvl (RConst x) _ = lift $ tcConst x
 >  tc env lvl RStar _ = return (Ind Star, Ind Star)
+>  tc env lvl (RFileLoc f l t) exp = 
+>     do (next, infer, bindings, errs, mvs, fc) <- get
+>        put (next, infer, bindings, errs, mvs, Just (FC f l))
+>        tc env lvl t exp
 
 Pattern bindings are a special case since they may bind several names,
 and we don't convert names to de Bruijn indices
@@ -382,8 +425,7 @@
 >     case expnf of
 >       (Ind (Label lt comp)) -> do
 >          (Ind tv, Ind tt) <- tcfixup env lvl t (Just (Ind lt))
->          checkConvSt env gamma (Ind lt) (Ind tt) $ 
->             "Type error: " ++ show tt ++", expected type " ++ show lt
+>          checkConvSt env gamma (Ind lt) (Ind tt)
 >          return (Ind (Return tv), Ind (Label tt comp))
 >       _ -> fail $ "return " ++ show t++ " should give a label, got " ++ show expnf
 >  tc env lvl (RReturn t) Nothing = fail $ "Need to know the type to return for "++show t
@@ -391,11 +433,11 @@
 >          (Ind sv, Ind st) <- tcStage env lvl s exp
 >          return (Ind sv, Ind st)
 >  tc env lvl RInfer (Just (Ind exp)) = do 
->                       (next, infer, bindings, errs, mvs) <- get
+>                       (next, infer, bindings, errs, mvs, fc) <- get
 >                       let bindings' = if infer 
 >                                        then (inferName next, B Pi exp):bindings
 >                                        else bindings
->                       put (next+1, infer, bindings', errs, mvs)
+>                       put (next+1, infer, bindings', errs, mvs, fc)
 >                       return (Ind (P (inferName next)), Ind exp)
 >  tc env lvl RInfer Nothing = fail "Can't infer a term for placeholder"
 
@@ -404,8 +446,8 @@
 the expected type.
 
 >  tc env lvl (RMeta n) (Just (Ind exp)) 
->     = do (next, infer, bindings, errs, mvs) <- get
->          put (next, infer, bindings, errs, n:mvs)
+>     = do (next, infer, bindings, errs, mvs, fc) <- get
+>          put (next, infer, bindings, errs, n:mvs, fc)
 >          -- Abstract it over the environment so that we have everything
 >          -- in scope we need.
 >          tm <- abstractOver (orderEnv env) n exp []
@@ -422,8 +464,8 @@
 
 >  tc env lvl (RMeta n) Nothing 
 >         -- just invent a name for it and see what inference gives us
->     = do (next, infer, bindings, errs, mvs) <- get
->          put (next+1, infer, bindings, errs, mvs)
+>     = do (next, infer, bindings, errs, mvs, fc) <- get
+>          put (next+1, infer, bindings, errs, mvs, fc)
 >          -- let guessty = Bind (MN ("X", 0)) (B Pi (P (inferName next)))
 >          --                 (Sc (P (inferName (next+1))))
 >          let guessty = (P (inferName next))
@@ -465,7 +507,7 @@
 
 >  fixup e tm = fixupGam gamma e tm
 
->  tcConst :: (Monad m, Constant c) => c -> m (Indexed Name, Indexed Name)
+>  tcConst :: (Constant c) => c -> IvorM (Indexed Name, Indexed Name)
 >  tcConst c = return (Ind (Const c), Ind (constType c))
 
  tcConst Star = return (Ind (Const Star), Ind (Const Star)) --- *:* is a bit dodgy...
@@ -498,10 +540,7 @@
 >     (Ind tv,Ind tt) <- tcfixup env lvl t (Just (Ind Star))
 >     (Ind vv,Ind vt) <- tcfixup env lvl v (Just (Ind tv))
 >     let ttnf = normaliseEnv env gamma (Ind tt)
->     checkConvEnv env gamma (Ind vt) (Ind tv) $ 
->        show vt ++ " and " ++ show tv ++ " are not convertible\n" ++ 
->             dbg (normaliseEnv env gamma (Ind vt)) ++ "\n" ++
->             dbg (normaliseEnv env gamma (Ind tv)) ++ "\n"
+>     lift $ checkConvEnv env gamma (Ind vt) (Ind tv) (INotConvertible (Ind vt) (Ind tv))
 >     case ttnf of
 >       (Ind Star) -> return (B (Let vv) tv)
 >       _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
@@ -517,8 +556,7 @@
 >     (Ind tv,Ind tt) <- tcfixup env lvl t Nothing
 >     (Ind vv,Ind vt) <- tcfixup env lvl v Nothing
 >     let ttnf = normaliseEnv env gamma (Ind tt)
->     checkConvEnv env gamma (Ind vt) (Ind tv) $ 
->        show vt ++ " and " ++ show tv ++ " are not convertible"
+>     lift $ checkConvEnv env gamma (Ind vt) (Ind tv) (INotConvertible (Ind vt) (Ind tv))
 >     case ttnf of
 >       (Ind Star) -> return (B (Guess vv) tv)
 >       _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
@@ -528,11 +566,11 @@
 >     return ((B MatchAny tv), env)
 >  checkpatt gamma env lvl n pat t = do
 >     (Ind tv,Ind tt) <- tcfixup env lvl t Nothing
->     (next, infer, bindings, err, mvs) <- get
->     put (next, True, bindings, err, mvs)
+>     (next, infer, bindings, err, mvs, fc) <- get
+>     put (next, True, bindings, err, mvs, fc)
 >     (Ind patv,Ind patt) <- tcfixup (bindings++env) lvl pat Nothing
->     (next, _ ,bindings, err, mvs) <- get
->     put (next, infer, bindings, err, mvs)
+>     (next, _ ,bindings, err, mvs, fc) <- get
+>     put (next, infer, bindings, err, mvs, fc)
 >     let ttnf = normaliseEnv env gamma (Ind tt)
 >     --checkConvEnv env gamma (Ind patt) (Ind tv) $ 
 >     --   show patt ++ " and " ++ show tv ++ " are not convertible"
@@ -578,16 +616,16 @@
 -- > checkPatt gam env acc RInfer ty = return (combinepats acc PTerm, env)
 -- > checkPatt gam env _ _ _ = fail "Invalid pattern"
 
-> checkConvSt env g x y msg
->                 = do (next, infer, bindings, err, mvs) <- get
->                      put (next, infer, bindings, (env,x,y,msg):err, mvs)
+> checkConvSt env g x y
+>                 = do (next, infer, bindings, err, mvs, fc) <- get
+>                      put (next, infer, bindings, (env,x,y,fc):err, mvs, fc)
 >                      return ()
 
 > fixupGam gamma [] tm = return tm
 > fixupGam gamma ((env,x,y,_):xs) (Ind tm, Ind ty) = do 
 >      uns <- case unifyenv gamma env y x of
->                 Success x' -> return x'
->                 Failure err -> return [] -- fail err -- $ "Can't convert "++show x++" and "++show y ++ " ("++show err++")"
+>                 Right x' -> return x'
+>                 Left err -> return [] -- fail err -- $ "Can't convert "++show x++" and "++show y ++ " ("++show err++")"
 >      let tm' = fixupNames gamma uns tm
 >      let ty' = fixupNames gamma uns ty
 >      fixupGam gamma xs (Ind tm', Ind ty')
@@ -621,18 +659,15 @@
 > combinepats (Just (PVar n)) x = error "can't apply things to a variable"
 > combinepats (Just (PCon tag n ty args)) x = PCon tag n ty (args++[x])
 
- discharge :: Monad m =>
-              Gamma Name -> Name -> Binder (TT Name) -> 
-	       (Scope (TT Name)) -> (Scope (TT Name)) ->
-	       m (Indexed Name, Indexed Name)
-
+> discharge :: Gamma Name -> Name -> Binder (TT Name) -> 
+>	       (Scope (TT Name)) -> (Scope (TT Name)) ->
+>	       StateT CheckState IvorM (Indexed Name, Indexed Name)
 > discharge gamma n (B Lambda t) scv sct = do
 >    let lt = Bind n (B Pi t) sct
 >    let lv = Bind n (B Lambda t) scv
 >    return (Ind lv,Ind lt)
 > discharge gamma n (B Pi t) scv (Sc sct) = do
->    checkConvSt [] gamma (Ind Star) (Ind sct) $ 
->       "The scope of a Pi binding must be a type"
+>    checkConvSt [] gamma (Ind Star) (Ind sct)
 >    let lt = Star
 >    let lv = Bind n (B Pi t) scv
 >    return (Ind lv,Ind lt)
@@ -644,26 +679,26 @@
 >    let lt = sct -- already checked sct and t are convertible
 >    let lv = Bind n (B Hole t) scv
 >    -- A hole can't appear in the type of its scope, however.
->    checkNotHoley 0 sct
+>    lift $ checkNotHoley 0 sct
 >    return (Ind lv,Ind lt)
 > discharge gamma n (B (Guess v) t) scv (Sc sct) = do
 >    let lt = sct -- already checked sct and t are convertible
 >    let lv = Bind n (B (Guess v) t) scv
 >    -- A hole can't appear in the type of its scope, however.
->    checkNotHoley 0 sct
+>    lift $ checkNotHoley 0 sct
 >    return (Ind lv,Ind lt)
 > discharge gamma n (B (Pattern v) t) scv (Sc sct) = do
 >    let lt = sct -- already checked sct and t are convertible
 >    let lv = Bind n (B (Pattern v) t) scv
 >    -- A hole can't appear in the type of its scope, however.
->    checkNotHoley 0 sct
+>    lift $ checkNotHoley 0 sct
 >    return (Ind lv,Ind lt)
 > discharge gamma n (B MatchAny t) scv (Sc sct) = do
 >    let lt = sct
 >    let lv = Bind n (B MatchAny t) scv
 >    return (Ind lv,Ind lt)
 
-> checkNotHoley :: Monad m => Int -> TT n -> m ()
+> checkNotHoley :: Int -> TT n -> IvorM ()
 > checkNotHoley i (V v) | v == i = fail "You can't put a hole where a hole don't belong."
 > checkNotHoley i (App f a) = do checkNotHoley i f
 >                                checkNotHoley i a
@@ -700,11 +735,11 @@
 > pToV2 v p (Const x) = Sc (Const x)
 > pToV2 v p Star = Sc Star
 
-> checkR g t = (typecheck g t):: (Result (Indexed Name, Indexed Name)) 
+ checkR g t = (typecheck g t):: (Result (Indexed Name, Indexed Name)) 
 
 If we're paranoid - recheck a supposedly well-typed term. Might want to
 do this after finishing a proof.
 
-> verify :: Monad m => Gamma Name -> Indexed Name -> m ()
+> verify :: Gamma Name -> Indexed Name -> IvorM ()
 > verify gam tm = do (_,_) <- typecheck gam (forget tm)
 >                    return ()
diff --git a/Ivor/Unify.lhs b/Ivor/Unify.lhs
--- a/Ivor/Unify.lhs
+++ b/Ivor/Unify.lhs
@@ -4,6 +4,7 @@
 
 > import Ivor.Nobby
 > import Ivor.TTCore
+> import Ivor.Errors
 
 > import Data.List
 
@@ -16,24 +17,20 @@
 Unify on named terms, but normalise using de Bruijn indices.
 (I hope this doesn't get too confusing...)
 
-> unify :: Monad m =>
->          Gamma Name -> Indexed Name -> Indexed Name -> m Unified
+> unify :: Gamma Name -> Indexed Name -> Indexed Name -> IvorM Unified
 > unify gam x y = unifyenv gam [] (finalise x) (finalise y)
 
-> unifyenv :: Monad m =>
->             Gamma Name -> Env Name ->
->             Indexed Name -> Indexed Name -> m Unified
+> unifyenv :: Gamma Name -> Env Name ->
+>             Indexed Name -> Indexed Name -> IvorM Unified
 > unifyenv = unifyenvErr False
 
-> unifyenvCollect :: Monad m =>
->                    Gamma Name -> Env Name ->
->                    Indexed Name -> Indexed Name -> m Unified
+> unifyenvCollect :: Gamma Name -> Env Name ->
+>                    Indexed Name -> Indexed Name -> IvorM Unified
 > unifyenvCollect = unifyenvErr True
 
-> unifyenvErr :: Monad m =>
->                Bool -> -- Ignore errors
+> unifyenvErr :: Bool -> -- Ignore errors
 >                Gamma Name -> Env Name ->
->                Indexed Name -> Indexed Name -> m Unified
+>                Indexed Name -> Indexed Name -> IvorM Unified
 > -- For the sake of readability of the results, first attempt to unify
 > -- without reducing, and reduce if that doesn't work.
 > -- Also, there is no point reducing if we don't have to, and not calling
@@ -45,9 +42,9 @@
 >                                    show (p (normalise (gam' gam) x))) $-}
 >     case unifynferr i env (p x)
 >                           (p y) of
->           (Just x) -> return x
->           Nothing -> unifynferr i env (p (normalise (gam' gam) x))
->                                       (p (normalise (gam' gam) y))
+>           (Right x) -> return x
+>           _ -> unifynferr i env (p (normalise (gam' gam) x))
+>                                 (p (normalise (gam' gam) y))
 >    where p (Ind t) = Ind (makePs t)
 >          gam' g = concatGam g (envToGamHACK env)
 
@@ -58,21 +55,18 @@
 >     = insertGam n (G (Fun [] (Ind v)) (Ind ty) defplicit) (envToGamHACK xs)
 > envToGamHACK (_:xs) = envToGamHACK xs
 
-> unifynf :: Monad m =>
->            Env Name -> Indexed Name -> Indexed Name -> m Unified
+> unifynf :: Env Name -> Indexed Name -> Indexed Name -> IvorM Unified
 > unifynf = unifynferr True
 
 Collect names which do unify, and ignore errors
 
-> unifyCollect :: Monad m =>
->            Env Name -> Indexed Name -> Indexed Name -> m Unified
+> unifyCollect :: Env Name -> Indexed Name -> Indexed Name -> IvorM Unified
 > unifyCollect = unifynferr False
 
 > sentinel = [(MN ("HACK!!",0), P (MN ("HACK!!",0)))]
 
-> unifynferr :: Monad m =>
->               Bool -> -- Ignore errors
->               Env Name -> Indexed Name -> Indexed Name -> m Unified
+> unifynferr :: Bool -> -- Ignore errors
+>               Env Name -> Indexed Name -> Indexed Name -> IvorM Unified
 > unifynferr ignore env topx@(Ind x) topy@(Ind y)
 >                = do acc <- un env env x y []
 >                     if ignore then return () else checkAcc acc
@@ -96,7 +90,7 @@
 >                   do acc' <- un envl envr f f' acc
 >                      un envl envr s s' acc'
 >              | otherwise = if ignore then return acc
->                               else fail $ "Can't unify "++show x++" and "++show y
+>                               else ifail $ ICantUnify (Ind x) (Ind y)
 >             where funify (P x) (P y)
 >                       | x==y = True
 >                       | otherwise = hole envl x || hole envl y
@@ -113,8 +107,7 @@
 >          un envl envr (Stage x) (Stage y) acc = unst envl envr x y acc
 >          un envl envr x y acc
 >                     | x == y || ignore = return acc
->                     | otherwise = fail $ "Can't unify " ++ show x ++
->                                          " and " ++ show y ++ " in " ++ show (topx,topy)
+>                     | otherwise = ifail $ ICantUnify (Ind x) (Ind y)
 >          unb envl envr (B b ty) (B b' ty') acc =
 >              do acc' <- unbb envl envr b b' acc
 >                 un envl envr ty ty' acc'
@@ -125,7 +118,7 @@
 >          unbb envl envr (Guess v) (Guess v') acc = un envl envr v v' acc
 >          unbb envl envr x y acc
 >                   = if ignore then return acc
->                        else fail $ "Can't unify "++show x++" and "++show y
+>                        else fail $ "Can't unify binders " ++ show x ++ " and " ++ show y
 
 >          unst envl envr (Quote x) (Quote y) acc = un envl envr x y acc
 >          unst envl envr (Code x) (Code y) acc = un envl envr x y acc
@@ -133,8 +126,7 @@
 >          unst envl envr (Escape x _) (Escape y _) acc = un envl envr x y acc
 >          unst envl envr x y acc =
 >                   if ignore then return acc
->                       else fail $ "Can't unify " ++ show (Stage x) ++
->                                " and " ++ show (Stage y)
+>                       else ifail $ ICantUnify (Ind (Stage x)) (Ind (Stage y))
 
 >          hole env x | (Just (B Hole ty)) <- lookup x env = True
 >                     | otherwise = isInferred x
@@ -146,8 +138,7 @@
 >              | (Just tm') <- lookup n xs
 >                  = if (ueq tm tm')  -- Take account of names! == no good.
 >                       then checkAcc xs
->                       else fail $ "Can't unify " ++ show tm ++
->                                   " and " ++ show tm'
+>                       else ifail $ ICantUnify (Ind tm) (Ind tm')
 >              | otherwise = checkAcc xs
 
 >          loc x xs = loc' 0 x xs
@@ -160,14 +151,14 @@
 
 >          ueq :: TT Name -> TT Name -> Bool
 >          ueq x y = case unifyenv emptyGam [] (Ind x) (Ind y) of
->                   Just _ -> True
+>                   Right _ -> True
 >                   _ -> False
 
 Grr!
 
 > ueq :: Gamma Name -> TT Name -> TT Name -> Bool
 > ueq gam x y = case unifyenv gam [] (Ind x) (Ind y) of
->                   Just _ -> True
+>                   Right _ -> True
 >                   _ -> False
 
 
diff --git a/Ivor/ViewTerm.lhs b/Ivor/ViewTerm.lhs
--- a/Ivor/ViewTerm.lhs
+++ b/Ivor/ViewTerm.lhs
@@ -15,7 +15,7 @@
 > module Ivor.ViewTerm(-- * Variable names
 >                        Name,name,displayName,NameType(..),mkVar,
 >                        -- * Terms
->                        Term(..), ViewTerm(..), apply,
+>                        Term(..), ViewTerm(..), Annot(..), apply,
 >                        view, viewType, ViewConst, typeof, 
 >                        freeIn, namesIn, occursIn, subst, getApp, 
 >                        Ivor.ViewTerm.getFnArgs,
@@ -75,8 +75,12 @@
 >     | Eval { evalterm :: ViewTerm } -- ^ Staging annotation
 >     | Escape { escapedterm :: ViewTerm } -- ^ Staging annotation
 >     | Placeholder
+>     | Annotation { annotation :: Annot,
+>                    term :: ViewTerm } -- ^ additional annotations
 >     | Metavar { var :: Name }
 
+> data Annot = FileLoc FilePath Int -- ^ source file, line number
+
 > instance Eq ViewTerm where
 >     (==) (Name _ x) (Name _ y) = x == y
 >     (==) (Ivor.ViewTerm.App f a) (Ivor.ViewTerm.App f' a') = f == f' && a == a'
@@ -97,6 +101,7 @@
 >     (==) (Ivor.ViewTerm.Code t) (Ivor.ViewTerm.Code t') = t==t'
 >     (==) (Ivor.ViewTerm.Eval t) (Ivor.ViewTerm.Eval t') = t==t'
 >     (==) (Ivor.ViewTerm.Escape t) (Ivor.ViewTerm.Escape t') = t==t'
+>     (==) (Annotation _ t) (Annotation _ t') = t == t'
 >     (==) _ _ = False
 
 > -- | Haskell types which can be used as constants
@@ -139,6 +144,7 @@
 >     forget (Ivor.ViewTerm.Code t) = RStage (RCode (forget t))
 >     forget (Ivor.ViewTerm.Eval t) = RStage (REval (forget t))
 >     forget (Ivor.ViewTerm.Escape t) = RStage (REscape (forget t))
+>     forget (Annotation (FileLoc f l) t) = RFileLoc f l (forget t)
 >     forget x = Var (var x)
 
 > instance Show ViewTerm where
@@ -220,6 +226,7 @@
 >    fi n (Ivor.ViewTerm.Code t) = fi n t
 >    fi n (Ivor.ViewTerm.Eval t) = fi n t
 >    fi n (Ivor.ViewTerm.Escape t) = fi n t
+>    fi n (Annotation _ t) = fi n t
 >    fi n _ = False
 
 > -- | Return the names occurring free in a term
@@ -238,6 +245,7 @@
 >    fi ns (Ivor.ViewTerm.Code t) = fi ns t
 >    fi ns (Ivor.ViewTerm.Eval t) = fi ns t
 >    fi ns (Ivor.ViewTerm.Escape t) = fi ns t
+>    fi ns (Annotation _ t) = fi ns t
 >    fi ns _ = []
 
 > -- | Return whether a subterm occurs in a (first order) term.
@@ -253,27 +261,32 @@
 >    fi n (Ivor.ViewTerm.Code t) = fi n t
 >    fi n (Ivor.ViewTerm.Eval t) = fi n t
 >    fi n (Ivor.ViewTerm.Escape t) = fi n t
+>    fi n (Annotation _ t) = fi n t
 >    fi n x = n == x
 
 > -- | Get the function from an application. If no application, returns the
 > -- entire term.
 > getApp :: ViewTerm -> ViewTerm
 > getApp (Ivor.ViewTerm.App f a) = getApp f
+> getApp (Annotation _ t) = getApp t
 > getApp x = x
 
 > -- | Get the arguments from a function application.
 > getFnArgs :: ViewTerm -> [ViewTerm]
 > getFnArgs (Ivor.ViewTerm.App f a) = Ivor.ViewTerm.getFnArgs f ++ [a]
+> getFnArgs (Annotation _ t) = getFnArgs t
 > getFnArgs x = []
 
 > -- | Get the argument names and types from a function type
 > getArgTypes :: ViewTerm -> [(Name, ViewTerm)]
 > getArgTypes (Ivor.ViewTerm.Forall n ty sc) = (n,ty):(getArgTypes sc)
+> getArgTypes (Annotation _ t) = getArgTypes t
 > getArgTypes x = []
 
 > -- | Get the return type from a function type
 > getReturnType :: ViewTerm -> ViewTerm
 > getReturnType (Ivor.ViewTerm.Forall n ty sc) = Ivor.ViewTerm.getReturnType sc
+> getReturnType (Annotation _ t) = Ivor.ViewTerm.getReturnType t
 > getReturnType x = x
 
 > dbgshow (UN n) = "UN " ++ show n
@@ -289,6 +302,8 @@
 >   m' (Ivor.ViewTerm.App f a) (Ivor.ViewTerm.App f' a') acc 
 >       = do acc' <- m' f f' acc
 >            m' a a' acc'
+>   m' (Annotation _ t) t' acc = m' t t' acc
+>   m' t (Annotation _ t') acc = m' t t' acc
 >   m' x y acc | x == y = return acc
 >              | otherwise = fail $"Mismatch " ++ show x ++ " and " ++ show y
 
@@ -328,5 +343,6 @@
 >           = Ivor.ViewTerm.Eval (subst n v r)
 > subst n v (Ivor.ViewTerm.Escape r) 
 >           = Ivor.ViewTerm.Escape (subst n v r)
+> subst n v (Annotation a t) = Annotation a (subst n v t)
 > subst n v t = t
 
diff --git a/emacs/ivor-mode.el b/emacs/ivor-mode.el
--- a/emacs/ivor-mode.el
+++ b/emacs/ivor-mode.el
@@ -211,4 +211,4 @@
              (comint-send-input))))
   (goto-char (point-min)))
 
-(provide 'ivor)
+(provide 'ivor-mode)
diff --git a/ivor.cabal b/ivor.cabal
--- a/ivor.cabal
+++ b/ivor.cabal
@@ -1,5 +1,5 @@
 Name:		ivor
-Version:	0.1.8
+Version:	0.1.9
 Author:		Edwin Brady
 License:	BSD3
 License-file:	LICENSE
@@ -58,7 +58,7 @@
 
 
 
-Build-depends:  base, parsec, mtl, directory
+Build-depends:  base >=3 && <5, parsec, mtl, directory
 Build-type:     Simple
 
 Extensions:     MultiParamTypeClasses, FunctionalDependencies,
@@ -76,5 +76,5 @@
 		Ivor.CodegenC, Ivor.Datatype, Ivor.Display,
 		Ivor.ICompile, Ivor.MakeData, Ivor.Unify,
 		Ivor.Grouper, Ivor.ShellParser, Ivor.Constant,
-		Ivor.RunTT, Ivor.Compiler, Ivor.Prefix,
+		Ivor.RunTT, Ivor.Compiler, Ivor.Prefix, Ivor.Errors,
 		Ivor.PatternDefs,  Ivor.ShellState, Ivor.Scopecheck