diff --git a/Ivor/Datatype.lhs b/Ivor/Datatype.lhs
--- a/Ivor/Datatype.lhs
+++ b/Ivor/Datatype.lhs
@@ -63,8 +63,8 @@
 >	 (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 Nothing
+>        ([(_, csch, _)], _, _) <- checkDef gamma'' cr crty cschemes False False Nothing
 >	 return (Data (ty,G (TCon (arity gamma kv) erdata) kv defplicit) consv numps
 >                    (er,ev) (cr,cv) (Just esch) (Just csch) eschemes cschemes)
 
diff --git a/Ivor/Errors.lhs b/Ivor/Errors.lhs
--- a/Ivor/Errors.lhs
+++ b/Ivor/Errors.lhs
@@ -12,6 +12,7 @@
 >             | INoSuchVar Name
 >             | ICantInfer Name (Indexed Name)
 >             | IContext String IError
+>             | IAmbiguousName [Name]
 >   deriving (Show, Eq)
 
 > instance Error IError where
diff --git a/Ivor/Evaluator.lhs b/Ivor/Evaluator.lhs
--- a/Ivor/Evaluator.lhs
+++ b/Ivor/Evaluator.lhs
@@ -1,6 +1,7 @@
 > {-# OPTIONS_GHC -fglasgow-exts #-}
 
-> module Ivor.Evaluator(eval_whnf, eval_nf, eval_nf_without, eval_nf_limit,
+> module Ivor.Evaluator(eval_whnf, eval_nf, eval_nf_env,
+>                       eval_nf_without, eval_nf_limit,
 >                       eval_nfEnv, tidyNames) where
 
 > import Ivor.TTCore
@@ -25,6 +26,14 @@
 > eval_nf :: Gamma Name -> Indexed Name -> Indexed Name
 > eval_nf gam (Ind tm) = let res = makePs (evaluate True gam tm Nothing Nothing)
 >                            in finalise (Ind res)
+
+> eval_nf_env :: Env Name -> Gamma Name -> Indexed Name -> Indexed Name
+> eval_nf_env env g t
+>     = eval_nf (addenv env g) t
+>   where addenv [] g = g
+>         addenv ((n,B (Let v) ty):xs) (Gam g)
+>             = addenv xs (Gam (Map.insert n (G (Fun [] (Ind v)) (Ind ty) defplicit) g))
+>         addenv (_:xs) g = addenv xs g
 
 > eval_nf_without :: Gamma Name -> Indexed Name -> [Name] -> Indexed Name
 > eval_nf_without gam tm [] = eval_nf gam tm
diff --git a/Ivor/Nobby.lhs b/Ivor/Nobby.lhs
--- a/Ivor/Nobby.lhs
+++ b/Ivor/Nobby.lhs
@@ -70,6 +70,8 @@
 >  eval stage gamma g (Con tag n i) = (MB (BCon tag n i, pty n) Empty)
 >  eval stage gamma g (TyCon n 0) = (MR (RTyCon n Empty))
 >  eval stage gamma g (TyCon n i) = (MB (BTyCon n i, pty n) Empty)
+>  eval stage gamma g (Meta n ty) = (MB (BMeta n bty, bty) Empty)
+>     where bty = eval stage gamma g ty
 >  eval stage gamma g (Const x) = (MR (RdConst x))
 >  eval stage gamma g Star = MR RdStar
 >  eval stage gamma (VG g) (Bind n (B Lambda ty) (Sc sc)) =
@@ -99,6 +101,7 @@
 >          getelim y = error $ show n ++
 >            " is not an elimination rule. Something went wrong." ++ show y
 >  eval stage gamma g (Stage s) = evalStage stage gamma g s
+>  eval stage gamma g x = error $ "eval, can't happen: " ++ show x
 
 >  evalcomp stage gamma g (Comp n ts) = MComp n (map (eval stage gamma g) ts)
 
@@ -261,6 +264,7 @@
 >     weakenp i (BPatDef p n) = BPatDef p n
 >     weakenp i (BRec n v) = BRec n v
 >     weakenp i (BPrimOp e n) = BPrimOp e n
+>     weakenp i (BMeta n ty) = BMeta n (weakenp i ty)
 >     weakenp i (BP n) = BP n
 >     weakenp i (BV j) = BV (weakenp i j)
 >     weakenp i (BEval t ty) = BEval (weakenp i t) (weakenp i ty)
@@ -309,6 +313,7 @@
 > instance Quote (Blocked Kripke) (Blocked Scope) where
 >     quote' ns (BCon t n j) = BCon t n j
 >     quote' ns (BTyCon n j) = BTyCon n j
+>     quote' ns (BMeta n t) = BMeta n (quote' ns t)
 >     quote' ns (BElim e n) = BElim e n
 >     quote' ns (BPatDef p n) = BPatDef p n
 >     quote' ns (BRec n v) = BRec n v
@@ -372,6 +377,7 @@
 >     forget (BPatDef p n) = P n
 >     forget (BRec n v) = P n
 >     forget (BPrimOp f n) = P n
+>     forget (BMeta n t) = Meta n (forget t)
 >     forget (BP n) = P n
 >     forget (BV i) = V i
 >     forget (BEval t ty) = Stage (Eval (forget t) (forget ty))
diff --git a/Ivor/Overloading.lhs b/Ivor/Overloading.lhs
new file mode 100644
--- /dev/null
+++ b/Ivor/Overloading.lhs
@@ -0,0 +1,35 @@
+Facilities for handling overloading. This is currently a bodge - terms
+contain 'ROpts' which are variables which could be one of several things.
+We convert such terms to a list of terms which contain all the possible 
+combinations of 'Var', typecheck them all, and if only one succeeds, that's
+the right overloading. If more than one succeeds, there is an ambiguous name.
+
+> module Ivor.Overloading where
+
+> import Ivor.TTCore
+
+> getTerms :: Raw -> [Raw]
+> getTerms (Var n) = return $ Var n
+> getTerms (ROpts ns) = do n <- ns
+>                          return $ Var n
+> getTerms (RApp f a) = do f' <- getTerms f
+>                          a' <- getTerms a
+>                          return $ RApp f' a'
+> getTerms (RBind n (B b t) sc)
+>                     = do b' <- gtb b
+>                          t' <- getTerms t
+>                          sc' <- getTerms sc
+>                          return $ RBind n (B b' t') sc'
+>    where gtb Lambda = return Lambda
+>          gtb Pi = return Pi
+>          gtb (Let t) = do t' <- getTerms t
+>                           return $ Let t'
+>          gtb Hole = return Hole
+>          gtb (Guess t) = do t' <- getTerms t
+>                             return $ Guess t'
+>          gtb (Pattern t) = do t' <- getTerms t
+>                               return $ Guess t'
+>          gtb MatchAny = return MatchAny
+> getTerms (RFileLoc f l t) = do t' <- getTerms t
+>                                return (RFileLoc f l t')
+> getTerms t = return t
diff --git a/Ivor/PatternDefs.lhs b/Ivor/PatternDefs.lhs
--- a/Ivor/PatternDefs.lhs
+++ b/Ivor/PatternDefs.lhs
@@ -9,6 +9,7 @@
 > import Ivor.Unify
 > import Ivor.Errors
 > import Ivor.Values
+> import Ivor.Evaluator
 
 > import Debug.Trace
 > import Data.List
@@ -24,8 +25,9 @@
 > checkDef :: Gamma Name -> Name -> Raw -> [PMRaw] -> 
 >             Bool -> -- Check for coverage
 >             Bool -> -- Check for well-foundedness
+>             Maybe [(Name, Int)] -> -- Names to specialise
 >             IvorM ([(Name, PMFun Name, Indexed Name)], [(Name, Indexed Name)], Bool)
-> checkDef gam fn tyin pats cover wellfounded = do
+> checkDef gam fn tyin pats cover wellfounded spec = 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")]])
 >   clausesIn <- mapM (expandClause gam) pats
@@ -37,7 +39,7 @@
 >   checkNotExists fn gam
 >   gam' <- gInsert fn (G Undefined ty defplicit) gam
 >   clauses' <- validClauses gam' fn ty clauses'
->   (pmdefs, newdefs, covers) <- matchClauses gam' fn pats tyin ty cover clauses'
+>   (pmdefs, newdefs, covers) <- matchClauses gam' fn pats tyin ty cover clauses' spec
 >   wf <- return True 
 >         {- if wellfounded then
 >             do checkWellFounded gam fn [0..arity-1] pmdef
@@ -175,13 +177,14 @@
 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.
 
-Each clause may generate auxiliary definitions, so return all definitons created.
+Each clause may generate auxiliary definitions, so return all definitions created.
 
 > matchClauses :: Gamma Name -> Name -> [PMRaw] -> Raw -> Indexed Name -> 
 >                 Bool -> -- Check coverage
 >                 [(Indexed Name, Indexed Name)] -> 
+>                 Maybe [(Name, Int)] ->
 >                 IvorM ([(Name, PMFun Name, Indexed Name)], [(Name, Indexed Name)], Bool)
-> matchClauses gam fn pats tyin ty@(Ind ty') cover gen = do
+> matchClauses gam fn pats tyin ty@(Ind ty') cover gen spec = do
 >    let raws = zip (map mkRaw pats) (map getRet pats)
 >    (checkpats, newdefs, aux, covers) <- mytypechecks gam raws [] [] [] True
 >    cv <- if cover then 
@@ -217,7 +220,11 @@
 >                let namesbound = getNames (Sc tmtt)
 >                checkAllBound (fileLine ret) namesret namesbound (Ind rtmtt') tmtt rty pty
 >                -- trace (show env) $
->                return ((tm, Ind rtmtt', env), [], newdefs, True)
+>                let specrtm = case spec of
+>                                Nothing -> Ind rtmtt'
+>                                Just [] -> eval_nf gam (Ind rtmtt')
+>                                Just ns -> eval_nf_limit gam (Ind rtmtt') ns
+>                return ((tm, specrtm, env), [], newdefs, True)
 >         mytypecheck gam (clause, (RWith addprf 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
@@ -244,7 +251,7 @@
 >                let gam' = insertGam newname (G Undefined newfnTy 0) gam
 >                newpdef <- mapM (newp tm newargs 1 addprf) (zip newpats pats)
 >                (chk, auxdefs, _, _) <- mytypecheck gam' (clause, (RWRet ret)) i
->                (auxdefs', newdefs, covers) <- checkDef gam' newname (forget newfnTy) newpdef False cover
+>                (auxdefs', newdefs, covers) <- checkDef gam' newname (forget newfnTy) newpdef False cover spec
 >                return (chk, auxdefs++auxdefs', newdefs, covers)
 
 >         addLastArg (RBind n (B Pi arg) x) ty scr addprf 
diff --git a/Ivor/Prefix.hs b/Ivor/Prefix.hs
deleted file mode 100644
--- a/Ivor/Prefix.hs
+++ /dev/null
@@ -1,1 +0,0 @@
-module Ivor.Prefix where prefix = "/Users/edwin"
diff --git a/Ivor/Shell.lhs b/Ivor/Shell.lhs
--- a/Ivor/Shell.lhs
+++ b/Ivor/Shell.lhs
@@ -26,13 +26,14 @@
 > import Ivor.Equality
 > import Ivor.Gadgets
 > import Ivor.Primitives
-> import qualified Ivor.Prefix
 > import Ivor.Plugin
+> import Paths_ivor
 
 > import System.Exit
 > import System.Environment
 > import System.Directory
 > import System.IO
+> import System.IO.Unsafe
 > import Data.Char
 > import Debug.Trace
 
@@ -388,7 +389,7 @@
 
 > -- | Get the install prefix of the library
 > prefix :: FilePath
-> prefix = Ivor.Prefix.prefix
+> prefix = unsafePerformIO getDataDir -- Yes, yes, I know.
 
 If the given file is already loaded, do nothing.
 
diff --git a/Ivor/TT.lhs b/Ivor/TT.lhs
--- a/Ivor/TT.lhs
+++ b/Ivor/TT.lhs
@@ -189,6 +189,7 @@
 >              | NoSuchVar Name
 >              | CantInfer Name ViewTerm
 >              | ErrContext String TTError
+>              | AmbiguousName [Name]
 
 > instance Show TTError where
 >     show (CantUnify t1 t2) = "Can't unify " ++ show t1 ++ " and " ++ show t2
@@ -199,6 +200,7 @@
 >                     " = " ++ show rhs
 >     show (CantInfer  n tm) = "Can't infer value for " ++ show n ++ " in " ++ show tm
 >     show (NoSuchVar n) = "No such name as " ++ show n
+>     show (AmbiguousName ns) = "Ambiguous name " ++ show ns
 >     show (ErrContext c err) = c ++ show err
 
 > instance Error TTError where
@@ -226,6 +228,7 @@
 >                        names
 > getError (ICantInfer nm tm) = CantInfer nm (view (Term (tm, Ind TTCore.Star)))
 > getError (INoSuchVar n) = NoSuchVar n
+> getError (IAmbiguousName ns) = AmbiguousName ns
 > getError (IContext s e) = ErrContext s (getError e)
 
 > -- | Quickly convert a 'ViewTerm' into a real 'Term'.
@@ -308,6 +311,7 @@
 > data PattOpt = Partial -- ^ No need to cover all cases
 >              | GenRec -- ^ No termination checking
 >              | Holey -- ^ Allow metavariables in the definition, which will become theorems which need to be proved.
+>              | Specialise [(Name, Int)] -- ^ Specialise the right hand side
 >   deriving Eq
 
 > -- |Add a new definition to the global state.
@@ -329,6 +333,7 @@
 >               <- tt $ checkDef ndefs n inty (map mkRawClause clauses)
 >                            (not (elem Ivor.TT.Partial opts))
 >                            (not (elem GenRec opts))
+>                            (getSpec opts)
 >         (ndefs',vnewnames) 
 >                <- if (null newnames) then return (ndefs, [])
 >                      else do when (not (Holey `elem` opts)) $ 
@@ -346,6 +351,10 @@
 >             do gam' <- gInsert nm (G (PatternDef def tot (gen nm)) ty defplicit) gam
 >                insertAll xs gam' tot
 >         gen nm = nm /= n -- generated if it's not the provided name.
+
+>         getSpec [] = Nothing
+>         getSpec (Specialise fns:_) = Just fns
+>         getSpec (_:xs) = getSpec xs
 
 > -- |Add a new definition, with its type to the global state.
 > -- These definitions can be recursive, so use with care.
diff --git a/Ivor/TTCore.lhs b/Ivor/TTCore.lhs
--- a/Ivor/TTCore.lhs
+++ b/Ivor/TTCore.lhs
@@ -17,6 +17,7 @@
 
 > data Raw
 >     = Var Name
+>     | ROpts [Name]
 >     | RApp Raw Raw
 >     | RBind Name (Binder Raw) Raw
 >     | forall c.(Constant c) => RConst !c
@@ -676,6 +677,12 @@
 >     (==) (Elim x) (Elim y) = x==y
 >     (==) (App f a) (App f' a') = f==f' && a==a'
 >     (==) (Bind _ b sc) (Bind _ b' sc') = b==b' && sc==sc'
+
+Eta equality:
+
+>     (==) (Bind x (B Lambda ty) (Sc (App t (V 0)))) t' = t == t'
+>     (==) t' (Bind x (B Lambda ty) (Sc (App t (V 0)))) = t == t'
+
 >     (==) (Proj _ i x) (Proj _ j y) = i==j && x==y
 >     (==) (Const x) (Const y) = case cast x of
 >                                   Just x' -> x'==y
@@ -708,6 +715,7 @@
 >     forget x = fPrec 10 x where
 >       fPrec :: Int -> Raw -> String
 >       fPrec _ (Var n) = forget n
+>       fPrec _ (ROpts n) = show n
 >       fPrec x (RApp f a) = bracket x 1 $ fPrec 1 f ++ " " ++ fPrec 0 a
 >       fPrec x (RBind n (B Lambda t) sc) = bracket x 2 $
 >           "["++forget n ++":"++fPrec 10 t++"]" ++ fPrec 10 sc
diff --git a/Ivor/Tactics.lhs b/Ivor/Tactics.lhs
--- a/Ivor/Tactics.lhs
+++ b/Ivor/Tactics.lhs
@@ -3,6 +3,7 @@
 > import Ivor.TTCore
 > import Ivor.Typecheck
 > import Ivor.Nobby
+> import Ivor.Evaluator
 > import Ivor.Gadgets
 > import Ivor.Unify
 > import Ivor.Errors
@@ -263,19 +264,32 @@
 >        let (Ind nty) = normaliseEnv (ptovenv env) gam (Ind ntyin)
 >        let bvin = makePsEnv (map fst env) bv
 >        -- let (Just (Ind nty)) = lookuptype n gam
+
+Get the names and types of the arguments to be passed to the thing 
+we're refining by.
+
 >        let claimTypes = getClaims (makePsEnv (map fst env) nty)
 >        let rawapp = mkapp rtm (map (\_ -> RInfer) claimTypes)
+
+Normalise the goal.
+
 >        let (Ind tyin') = finalise (normaliseEnv (ptovenv env) gam (Ind ty))
+
+Type check the application we've just built, with the placeholders, some of 
+which may have been solved.
+
 >        (Ind rtch, rtych, ev) <- checkAndBind gam (ptovenv env) rawapp (Just (Ind tyin'))
->        let argguesses = getArgs rtch
->        -- So we'll have an application, some of the arguments with inferred
->        -- names. Let's record which ones...
+>        let argguesses = -- trace (show rawapp ++ "\n" ++ show tyin' ++ "\n" ++ show rtch ++ "\n" ++ show rtych ++ "\nNew env: " ++ show ev) $ 
+>                         getArgs rtch
+
+So we'll have an application, some of the arguments with inferred
+names. Let's record which ones...
+
 >        let claims = uniqifyClaims x env claimTypes
 >        let claimGuesses = zip claims (map appVar argguesses)
->        (tm',_) <- {- trace (show claimGuesses) $ -} doClaims x claimGuesses gam env tm
+>        (tm',_) <- doClaims x claimGuesses gam env tm
 >        let guess = (mkGuess claimGuesses [] (forget bvin))
->        (filled, unified) <- runtacticEnv gam env x tm'
->                  (fill guess)
+>        (filled, unified) <- runtacticEnv gam env x tm' (fill guess)
 >        -- (filled, solved) <- solveUnified [] unified filled
 >        -- filled <- tryDefaults defaults claims filled
 >        -- (tm', _) <- trace (show claims) $ tidy gam env filled
@@ -386,7 +400,7 @@
 
 > evalGoal :: Tactic
 > evalGoal gam env (Ind (Bind x (B Hole ty) sc)) =
->    do let (Ind nty) = normaliseEnv (ptovenv env) gam (finalise (Ind ty))
+>    do let (Ind nty) = eval_nf_env (ptovenv env) gam (finalise (Ind ty))
 >       tacret $ Ind (Bind x (B Hole nty) sc)
 > evalGoal _ _ (Ind (Bind x _ _)) = fail $ "evalGoal: " ++ show x ++ " Not a hole"
 > evalGoal _ _ _ = fail "evalGoal: Can't happen"
diff --git a/Ivor/Typecheck.lhs b/Ivor/Typecheck.lhs
--- a/Ivor/Typecheck.lhs
+++ b/Ivor/Typecheck.lhs
@@ -14,6 +14,7 @@
 > import Ivor.Errors
 > import Ivor.Evaluator
 > import Ivor.Values
+> import Ivor.Overloading
 
 > import Control.Monad.State
 > import Data.List
@@ -112,13 +113,13 @@
 >                 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") $ 
+>      -- trace ("Finishing checking " ++ show tm ++ " with " ++ show (length constraints) ++ " equations\n" ++ showeqn (map (\x -> (True,x)) constraints)) $ 
 >           -- 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) <- mkSubst $ (map (\x -> (True,x)) cs) ++
->                                    (map (\x -> (False,x)) (reverse cs))
+>                                    (map (\x -> (False,x)) cs)
 >          let tm' = papp subst tm
 >          let ty' = papp subst ty
 >          return (Ind tm',Ind ty')
@@ -139,7 +140,7 @@
 >                  let x' = papp s' x
 >                  let (Ind y') = eval_nf gam (Ind (papp s' y))
 >                  uns <- case unifyenvErr ok gam env (Ind y') (Ind x') of
->                           Right uns -> {- trace (show (y', x', uns)) $ -} return uns
+>                           Right uns -> return uns
 >                           Left err -> {- trace (showeqn all) $ -} 
 >                                       ifail (errCtxt fc (ICantUnify (Ind y') (Ind x')))
 
@@ -178,6 +179,7 @@
 >                 IvorM (Indexed Name, Indexed Name, Env Name)
 > checkAndBind gam env tm mty = do
 >    ((v,t), (next,inf,e,convs,_,_)) <- lvlcheck 0 True 0 gam env tm mty
+>    e <- convertAllEnv gam convs e
 >    (v'@(Ind vtm),t') <- doConversion tm gam convs v t -- (normalise gam t1') 
 >    return (v',t',e)
 
@@ -303,7 +305,8 @@
 >             Maybe (Indexed Name) -> 
 >             IvorM ((Indexed Name, Indexed Name), CheckState)
 > lvlcheck lvl infer next gamma env tm exp 
->     = do runStateT (tcfixupTop env lvl tm exp) (next, infer, [], [], [], Nothing) 
+>     = -- let tms = getTerms tm in
+>           runStateT (tcfixupTop env lvl tm exp) (next, infer, [], [], [], Nothing)
 >  where
 
 Do the typechecking, then unify all the inferred terms.
@@ -378,6 +381,8 @@
 >                          else lift $ ifail (errCtxt fc (INoSuchVar n))
 >                Just (B Pi t) -> return (Ind (P n), Ind t)
 
+>  tc env lvl (ROpts ns) Nothing = fail $ "Need a type for overloaded names"
+>  tc env lvl (ROpts ns) (Just exp) = fail $ "Overloading not implemented (" ++ show ns ++ " : " ++ show exp ++ ")"
 >  tc env lvl (RApp f a) exp = do
 >     (Ind fv, Ind ft) <- tcfixup env lvl f Nothing
 >     let fnfng = normaliseEnv env emptyGam (Ind ft)
@@ -398,11 +403,12 @@
 >          let tt' = (normaliseEnv env gamma (Ind tt))
 >          return (Ind (App fv av), (normaliseEnv env gamma (Ind tt)))
 >        _ -> fail $ "Cannot apply a non function type " ++ show ft ++ " to " ++ show a
->     return (rv,rt)
+>     -- return (rv,rt)
 >     case exp of
 >        Nothing -> return (rv,rt)
->        Just expt -> do checkConvSt env gamma rt expt
->                        return (rv,rt)
+>        Just expt -> -- trace ("Checking " ++ show (rv, rt, expt)) $
+>                      do checkConvSt env gamma rt expt
+>                         return (rv,rt)
 >  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 = 
diff --git a/Ivor/Unify.lhs b/Ivor/Unify.lhs
--- a/Ivor/Unify.lhs
+++ b/Ivor/Unify.lhs
@@ -42,8 +42,8 @@
 > {- trace (show (x,y) ++ "\n" ++
 >                                    show (p (normalise (gam' gam) x)) ++ "\n" ++
 >                                    show (p (normalise (gam' gam) x))) $-}
->     case unifynferr i env (p x)
->                           (p y) of
+>     case unifynferr False env (p x)
+>                               (p y) of
 >           (Right x) -> return x
 
 >           _ -> {- trace (dbgtt x ++ ", " ++ dbgtt y ++"\n") $ -}
@@ -115,11 +115,13 @@
 >                               else ifail $ ICantUnify (Ind x) (Ind y)
 >             where funify (P x) (P y)
 >                       | x==y = True
->                       | otherwise = hole envl x || hole envl y
->                   funify (Con _ _ _) (P x) = hole envr x
->                   funify (P x) (Con _ _ _) = hole envl x
->                   funify (TyCon _ _) (P x) = hole envr x
->                   funify (P x) (TyCon _ _) = hole envl x
+>                       | otherwise = False -- hole envl x || hole envl y
+>                   funify (Con _ _ _) (P x) = False -- hole envr x
+>                   funify (P x) (Con _ _ _) = False -- hole envl x
+>                   funify (TyCon _ _) (P x) = False -- hole envr x
+>                   funify (P x) (TyCon _ _) = False -- hole envl x
+>                   funify (P x) (App _ _) = False
+>                   funify (App _ _) (P x) = False
 >                   funify _ _ = True -- unify normally
 >          un envl envr (Proj _ i t) (Proj _ i' t') acc
 >             | i == i' = un envl envr t t' acc
diff --git a/Ivor/Values.lhs b/Ivor/Values.lhs
--- a/Ivor/Values.lhs
+++ b/Ivor/Values.lhs
@@ -195,6 +195,7 @@
 >     | BPrimOp PrimOp Name
 >     | BRec Name Value
 >     | BP Name
+>     | BMeta Name (Model s)
 >     | BV Int
 >     | BEval (Model s) (Model s)
 >     | BEscape (Model s) (Model s)
diff --git a/Ivor/ViewTerm.lhs b/Ivor/ViewTerm.lhs
--- a/Ivor/ViewTerm.lhs
+++ b/Ivor/ViewTerm.lhs
@@ -63,6 +63,7 @@
 
 > data ViewTerm 
 >     = Name { nametype :: NameType, var :: Name }
+>     | Overloaded { vars :: [Name] } -- ^ on input only, list of possible names, to be resolved to one by the type checker.
 >     | App { fun :: ViewTerm, arg :: ViewTerm }
 >     | Lambda { var :: Name, vartype :: ViewTerm, scope :: ViewTerm }
 >     | Forall { var :: Name, vartype :: ViewTerm, scope :: ViewTerm }
@@ -131,6 +132,7 @@
 >                   constructors :: [(Name,ViewTerm)] }
 
 > instance Forget ViewTerm Raw where
+>     forget (Overloaded vs) = ROpts vs
 >     forget (Ivor.ViewTerm.App f a) = RApp (forget f) (forget a)
 >     forget (Ivor.ViewTerm.Lambda v ty sc) = RBind v 
 >                                            (B TTCore.Lambda (forget ty)) 
diff --git a/ivor.cabal b/ivor.cabal
--- a/ivor.cabal
+++ b/ivor.cabal
@@ -1,5 +1,5 @@
 Name:		ivor
-Version:	0.1.11
+Version:	0.1.12
 Author:		Edwin Brady
 License:	BSD3
 License-file:	LICENSE
@@ -45,16 +45,17 @@
                 papers/ivor/ivor.tex, papers/ivor/corett.tex, papers/ivor/conclusions.tex,
                 papers/ivor/intro.tex, papers/ivor/llncs.cls, papers/ivor/tactics.tex,
                 papers/ivor/library.ltx, papers/ivor/dtp.bib, papers/ivor/alink.bib,
-                papers/ivor/Makefile, papers/ivor/embounded.bib
+                papers/ivor/Makefile, papers/ivor/embounded.bib,
+                lib/nat.tt, lib/lt.tt, lib/list.tt, lib/eq.tt,
+                lib/basics.tt, lib/logic.tt, lib/vect.tt, lib/fin.tt
+                
 
 Extra-source-files: emacs/ivor-mode.el, examplett/staged.tt, examplett/test.c, examplett/partial.tt, examplett/nat.tt,
                     examplett/vec.tt, examplett/lt.tt, examplett/Test.hs, examplett/plus.tt,
                     examplett/jmeq.tt, examplett/eq.tt, examplett/logic.tt, examplett/interp.tt,
                     examplett/stageplus.tt, examplett/Nat.hs, examplett/general.tt, examplett/natsimpl.tt,
                     examplett/test.tt, examplett/vect.tt, examplett/fin.tt, examplett/ack.tt,
-                    IOvor/IOPrims.lhs, IOvor/Main.lhs, IOvor/iobasics.tt, Jones/Main.lhs,
-                    lib/nat.tt, lib/lt.tt, lib/list.tt, lib/eq.tt,
-                    lib/basics.tt, lib/logic.tt, lib/vect.tt, lib/fin.tt
+                    IOvor/IOPrims.lhs, IOvor/Main.lhs, IOvor/iobasics.tt, Jones/Main.lhs
 
 
 
@@ -77,5 +78,7 @@
 		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.Errors,
-		Ivor.PatternDefs,  Ivor.ShellState, Ivor.Scopecheck
+		Ivor.RunTT, Ivor.Compiler, Ivor.Errors,
+		Ivor.PatternDefs,  Ivor.ShellState, Ivor.Scopecheck,
+		Ivor.Overloading,
+                Paths_ivor