diff --git a/idris.cabal b/idris.cabal
--- a/idris.cabal
+++ b/idris.cabal
@@ -1,5 +1,5 @@
 Name:           idris
-Version:        0.9.2
+Version:        0.9.2.1
 License:        BSD3
 License-file:   LICENSE
 Author:         Edwin Brady
@@ -63,11 +63,13 @@
                               Idris.Coverage, Idris.IBC, Idris.Unlit,
                               Idris.DataOpts, Idris.Transforms, Idris.DSL, 
 
+                              Util.Pretty,
+
                               Paths_idris
 
                Build-depends:   base>=4 && <5, parsec, mtl, Cabal, haskeline,
                                 containers, process, transformers, filepath, directory,
-                                binary, bytestring, epic>=0.9.3
+                                binary, bytestring, epic>=0.9.3, pretty
                                 
                Extensions:      MultiParamTypeClasses, FunctionalDependencies,
                                 FlexibleInstances, TemplateHaskell
diff --git a/lib/builtins.idr b/lib/builtins.idr
--- a/lib/builtins.idr
+++ b/lib/builtins.idr
@@ -192,7 +192,7 @@
       else compare xr yr
 
 
-class Eq a => Num a where 
+class Num a where 
     (+) : a -> a -> a
     (-) : a -> a -> a
     (*) : a -> a -> a
diff --git a/lib/prelude/heap.idr b/lib/prelude/heap.idr
--- a/lib/prelude/heap.idr
+++ b/lib/prelude/heap.idr
@@ -30,6 +30,15 @@
 size Empty          = O
 size (Node s l e r) = s
 
+isValidHeap : Ord a => MaxiphobicHeap a -> Bool
+isValidHeap Empty          = True
+isValidHeap (Node s l e r) =
+  dominates e l && dominates e r && s == S (size l + size r)
+  where
+    dominates : Ord a => a -> MaxiphobicHeap a -> Bool
+    dominates e Empty           = True
+    dominates e (Node s l e' r) = e' <= e
+
 --------------------------------------------------------------------------------
 -- Basic heaps
 --------------------------------------------------------------------------------
@@ -140,6 +149,23 @@
 total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = O
 isEmptySizeZero Empty          p = refl
 isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd
+
+total emptyHeapValid : Ord a => isValidHeap empty = True
+emptyHeapValid = refl
+
+total singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True
+singletonHeapValid e = refl
+
+{-
+total mergePreservesValidHeaps : Ord a => (left : MaxiphobicHeap a) ->
+  (right : MaxiphobicHeap a) -> (leftValid : isValidHeap left = True) ->
+  (rightValid : isValidHeap right = True) -> isValidHeap $ merge left right = True
+mergePreservesValidHeaps Empty              Empty              lp rp = refl
+mergePreservesValidHeaps Empty              (Node rs rl re rr) lp rp = rp
+mergePreservesValidHeaps (Node ls ll le lr) Empty              lp rp = lp
+mergePreservesValidHeaps (Node ls ll le lr) (Node rs rl re rr) lp rp =
+  ?mergePreservesValidHeapsBody
+-}
 
 --------------------------------------------------------------------------------
 -- Proofs
diff --git a/lib/prelude/list.idr b/lib/prelude/list.idr
--- a/lib/prelude/list.idr
+++ b/lib/prelude/list.idr
@@ -8,7 +8,7 @@
 
 %access public
 
-infixr 10 :: 
+infixr 7 :: 
 
 data List a
   = Nil
diff --git a/lib/prelude/vect.idr b/lib/prelude/vect.idr
--- a/lib/prelude/vect.idr
+++ b/lib/prelude/vect.idr
@@ -6,7 +6,7 @@
 
 %access public
 
-infixr 10 :: 
+infixr 7 :: 
 
 data Vect : Set -> Nat -> Set where
   Nil  : Vect a O
@@ -67,6 +67,7 @@
 -- Building bigger vectors
 --------------------------------------------------------------------------------
 
+total
 (++) : Vect a m -> Vect a n -> Vect a (m + n)
 (++) []      ys = ys
 (++) (x::xs) ys = x :: xs ++ ys
diff --git a/src/Core/Elaborate.hs b/src/Core/Elaborate.hs
--- a/src/Core/Elaborate.hs
+++ b/src/Core/Elaborate.hs
@@ -21,6 +21,8 @@
 import Data.List
 import Debug.Trace
 
+import Util.Pretty
+
 -- I don't really want this here, but it's useful for the test shell
 data Command = Theorem Name Raw
              | Eval Raw
@@ -30,6 +32,7 @@
 
 data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
   deriving Show
+
 type Elab' aux a = StateT (ElabState aux) TC a
 type Elab a = Elab' () a
 
diff --git a/src/Core/Evaluate.hs b/src/Core/Evaluate.hs
--- a/src/Core/Evaluate.hs
+++ b/src/Core/Evaluate.hs
@@ -80,6 +80,7 @@
 threshold = 1000 -- boredom threshold for evaluation, to prevent infinite typechecking
                  -- in fact it's a maximum recursion depth
 
+-- Normalise fully type checked terms (so, assume all names/let bindings resolved)
 normaliseC :: Context -> Env -> TT Name -> TT Name
 normaliseC ctxt env t 
    = evalState (do val <- eval ctxt threshold [] env t []
diff --git a/src/Core/ProofShell.hs b/src/Core/ProofShell.hs
--- a/src/Core/ProofShell.hs
+++ b/src/Core/ProofShell.hs
@@ -11,6 +11,8 @@
 import Control.Monad.State
 import System.Console.Haskeline
 
+import Util.Pretty
+
 data ShellState = ShellState 
                         { ctxt     :: Context,
                           prf      :: Maybe ProofState,
@@ -56,7 +58,7 @@
 runShell :: ShellState -> InputT IO ShellState
 runShell st = do (prompt, parser) <- 
                            maybe (return ("TT# ", parseCommand)) 
-                                 (\st -> do outputStrLn (show st)
+                                 (\st -> do outputStrLn . render . pretty $ st
                                             return (show (thname st) ++ "# ", parseTactic)) 
                                  (prf st)
                  x <- getInputLine prompt
diff --git a/src/Core/ProofState.hs b/src/Core/ProofState.hs
--- a/src/Core/ProofState.hs
+++ b/src/Core/ProofState.hs
@@ -13,10 +13,12 @@
 import Core.Unify
 
 import Control.Monad.State
-import Control.Applicative
+import Control.Applicative hiding (empty)
 import Data.List
 import Debug.Trace
 
+import Util.Pretty
+
 data ProofState = PS { thname   :: Name,
                        holes    :: [Name], -- holes still to be solved
                        nextname :: Int,    -- name supply
@@ -93,6 +95,45 @@
                showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++ 
                                          " =?= " ++ showEnv ps v
                showG ps b = showEnv ps (binderTy b)
+
+instance Pretty ProofState where
+  pretty (PS nm [] _ trm _ _ _ _ _ _ _ _ _ _ _) =
+    if size nm > breakingSize then
+      pretty nm <> colon $$ nest nestingSize (text " no more goals.")
+    else
+      pretty nm <> colon <+> text " no more goals."
+  pretty p@(PS nm (h:hs) _ tm _ _ _ _ _ i _ _ ctxt _ _) =
+    let OK g  = goal (Just h) tm in
+    let wkEnv = premises g in
+      text "Other goals" <+> colon <+> pretty hs $$
+      prettyPs wkEnv (reverse wkEnv) $$
+      text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$
+      pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
+    where
+      prettyGoal ps (Guess t v) =
+        if size v > breakingSize then
+          prettyEnv ps t <+> text "=?=" $$
+            nest nestingSize (prettyEnv ps v)
+        else 
+          prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
+      prettyGoal ps b = prettyEnv ps $ binderTy b
+
+      prettyPs env [] = empty
+      prettyPs env ((n, Let t v):bs) =
+        nest nestingSize (pretty n <+> colon <+>
+          if size v > breakingSize then
+            prettyEnv env t <+> text "=" $$
+              nest nestingSize (prettyEnv env v) $$
+                nest nestingSize (prettyPs env bs)
+          else
+            prettyEnv env t <+> text "=" <+> prettyEnv env v $$
+              nest nestingSize (prettyPs env bs))
+      prettyPs env ((n, b):bs) =
+        if size (binderTy b) > breakingSize then
+          nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)
+        else
+          nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$
+            nest nestingSize (prettyPs env bs))
 
 same Nothing n  = True
 same (Just x) n = x == n
diff --git a/src/Core/TT.hs b/src/Core/TT.hs
--- a/src/Core/TT.hs
+++ b/src/Core/TT.hs
@@ -10,6 +10,8 @@
 import qualified Data.Binary as B
 import Data.Binary hiding (get, put)
 
+import Util.Pretty hiding (Str)
+
 {- The language has:
    * Full dependent types
    * A hierarchy of universes, with cumulativity: Set : Set1, Set1 : Set2, ...
@@ -34,6 +36,9 @@
 deriving instance Binary FC 
 !-}
 
+instance Sized FC where
+  size (FC f l) = 1 + length f
+
 instance Show FC where
     show (FC f l) = f ++ ":" ++ show l
 
@@ -48,6 +53,17 @@
          | At FC Err
   deriving Eq
 
+instance Sized Err where
+  size (Msg msg) = length msg
+  size (CantUnify left right err score) = size left + size right + size err
+  size (NoSuchVariable name) = size name
+  size (NotInjective l c r) = size l + size c + size r
+  size (CantResolve trm) = size trm
+  size (IncompleteTerm trm) = size trm
+  size UniverseError = 1
+  size ProgramLineComment = 1
+  size (At fc err) = size fc + size err
+
 score :: Err -> Int
 score (CantUnify _ _ m s) = s + score m
 score (CantResolve _) = 20
@@ -60,10 +76,30 @@
                                ++ show e ++ " " ++ show i
     show _ = "Error"
 
+instance Pretty Err where
+  pretty (Msg m) = text m
+  pretty (CantUnify l r e i) =
+    if size l + size r > breakingSize then
+      text "Cannot unify" <+> colon $$
+        nest nestingSize (pretty l <+> text "and" <+> pretty r) $$
+        nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
+    else
+      text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r $$
+        nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
+  pretty _ = text "Error"
+
 data TC a = OK a
           | Error Err
   deriving (Eq, Functor)
 
+instance Pretty a => Pretty (TC a) where
+  pretty (OK ok) = pretty ok
+  pretty (Error err) =
+    if size err > breakingSize then
+      text "Error" <+> colon $$ (nest nestingSize $ pretty err)
+    else
+      text "Error" <+> colon <+> pretty err
+
 instance Show a => Show (TC a) where
     show (OK x) = show x
     show (Error str) = "Error: " ++ show str
@@ -118,6 +154,16 @@
 deriving instance Binary Name 
 !-}
 
+instance Sized Name where
+  size (UN n)     = 1
+  size (NS n els) = 1 + length els
+  size (MN i n) = 1
+
+instance Pretty Name where
+  pretty (UN n) = text n
+  pretty (NS n s) = pretty n
+  pretty (MN i s) = lbrace <+> text s <+> (text . show $ i) <+> rbrace
+
 instance Show Name where
     show (UN n) = n
     show (NS n s) = showSep "." (reverse s) ++ "." ++ show n
@@ -190,6 +236,23 @@
 deriving instance Binary Const 
 !-}
 
+instance Sized Const where
+  size _ = 1
+
+instance Pretty Const where
+  pretty (I i) = text . show $ i
+  pretty (BI i) = text . show $ i
+  pretty (Fl f) = text . show $ f
+  pretty (Ch c) = text . show $ c
+  pretty (Str s) = text s
+  pretty IType = text "Int"
+  pretty BIType = text "BigInt"
+  pretty FlType = text "Float"
+  pretty ChType = text "Char"
+  pretty StrType = text "String"
+  pretty PtrType = text "Ptr"
+  pretty Forgot = text "Forgot"
+
 data Raw = Var Name
          | RBind Name (Binder Raw) Raw
          | RApp Raw Raw
@@ -197,6 +260,18 @@
          | RForce Raw
          | RConstant Const
   deriving (Show, Eq)
+
+instance Sized Raw where
+  size (Var name) = 1
+  size (RBind name bind right) = 1 + size bind + size right
+  size (RApp left right) = 1 + size left + size right
+  size RSet = 1
+  size (RForce raw) = 1 + size raw
+  size (RConstant const) = size const
+
+instance Pretty Raw where
+  pretty = text . show
+
 {-! 
 deriving instance Binary Raw 
 !-}
@@ -218,6 +293,17 @@
 deriving instance Binary Binder 
 !-}
 
+instance Sized a => Sized (Binder a) where
+  size (Lam ty) = 1 + size ty
+  size (Pi ty) = 1 + size ty
+  size (Let ty val) = 1 + size ty + size val
+  size (NLet ty val) = 1 + size ty + size val
+  size (Hole ty) = 1 + size ty
+  size (GHole ty) = 1 + size ty
+  size (Guess ty val) = 1 + size ty + size val
+  size (PVar ty) = 1 + size ty
+  size (PVTy ty) = 1 + size ty
+
 fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)
 fmapMB f (Let t v)   = liftM2 Let (f t) (f v)
 fmapMB f (NLet t v)  = liftM2 NLet (f t) (f v)
@@ -259,6 +345,9 @@
           | UVal Int -- explicit universe level
   deriving (Eq, Ord)
 
+instance Sized UExp where
+  size _ = 1
+
 -- We assume that universe levels have been checked, so anything external
 -- can just have the same universe variable and we won't get any new
 -- cycles.
@@ -289,6 +378,12 @@
 deriving instance Binary NameType 
 !-}
 
+instance Sized NameType where
+  size _ = 1
+
+instance Pretty NameType where
+  pretty = text . show
+
 instance Eq NameType where
     Bound    == Bound    = True
     Ref      == Ref      = True
@@ -308,6 +403,18 @@
 deriving instance Binary TT 
 !-}
 
+instance Sized a => Sized (TT a) where
+  size (P name n trm) = 1 + size name + size n + size trm
+  size (V v) = 1
+  size (Bind nm binder bdy) = 1 + size nm + size binder + size bdy
+  size (App l r) = 1 + size l + size r
+  size (Constant c) = size c
+  size Erased = 1
+  size (Set u) = 1 + size u
+
+instance Pretty a => Pretty (TT a) where
+  pretty _ = text "test"
+
 type EnvTT n = [(n, Binder (TT n))]
 
 data Datatype n = Data { d_typename :: n,
@@ -495,6 +602,54 @@
 
 showEnv env t = showEnv' env t False
 showEnvDbg env t = showEnv' env t True
+
+prettyEnv env t = prettyEnv' env t False
+  where
+    prettyEnv' env t dbg = prettySe 10 env t dbg
+
+    bracket outer inner p
+      | inner > outer = lparen <> p <> rparen
+      | otherwise     = p
+
+    prettySe p env (P nt n t) debug =
+      pretty n <+> 
+        if debug then
+          lbrack <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbrack
+        else
+          empty
+    prettySe p env (V i) debug
+      | i < length env =
+        if debug then
+          text . show . fst $ env!!i
+        else
+          lbrack <+> text (show i) <+> rbrack
+      | otherwise      = text "unbound" <+> text (show i) <+> text "!"
+    prettySe p env (Bind n b@(Pi t) sc) debug
+      | noOccurrence n sc && not debug =
+          bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug
+    prettySe p env (Bind n b sc) debug =
+      bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug
+    prettySe p env (App f a) debug =
+      bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug
+    prettySe p env (Constant c) debug = pretty c
+    prettySe p env Erased debug = text "[_]"
+    prettySe p env (Set i) debug = text "Set" <+> (text . show $ i)
+
+    prettySb env n (Lam t) = prettyB env "λ" "=>" n t
+    prettySb env n (Hole t) = prettyB env "?defer" "." n t
+    prettySb env n (Pi t) = prettyB env "(" ") ->" n t
+    prettySb env n (PVar t) = prettyB env "pat" "." n t
+    prettySb env n (PVTy t) = prettyB env "pty" "." n t
+    prettySb env n (Let t v) = prettyBv env "let" "in" n t v
+    prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
+
+    prettyB env op sc n t debug =
+      text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc
+
+    prettyBv env op sc n t v debug =
+      text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>
+        prettySe 10 env v debug <> text sc
+          
 
 showEnv' env t dbg = se 10 env t where
     se p env (P nt n t) = show n 
diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs
--- a/src/Idris/AbsSyntax.hs
+++ b/src/Idris/AbsSyntax.hs
@@ -5,18 +5,23 @@
 
 import Core.TT
 import Core.Evaluate
-import Core.Elaborate
+import Core.Elaborate hiding (Tactic(..))
 import Core.Typecheck
 
 import System.Console.Haskeline
+
 import Control.Monad.State
+
 import Data.List
 import Data.Char
 import Data.Either
+
 import Debug.Trace
 
 import qualified Epic.Epic as E
 
+import Util.Pretty
+
 data IOption = IOption { opt_logLevel :: Int,
                          opt_typecase :: Bool,
                          opt_typeintype :: Bool,
@@ -571,6 +576,26 @@
 deriving instance Binary PTactic' 
 !-}
 
+instance Sized a => Sized (PTactic' a) where
+  size (Intro nms) = 1 + size nms
+  size Intros = 1
+  size (Focus nm) = 1 + size nm
+  size (Refine nm bs) = 1 + size nm + length bs
+  size (Rewrite t) = 1 + size t
+  size (LetTac nm t) = 1 + size nm + size t
+  size (Exact t) = 1 + size t
+  size Compute = 1
+  size Trivial = 1
+  size Solve = 1
+  size Attack = 1
+  size ProofState = 1
+  size ProofTerm = 1
+  size Undo = 1
+  size (Try l r) = 1 + size l + size r
+  size (TSeq l r) = 1 + size l + size r
+  size Qed = 1
+  size Abandon = 1
+
 type PTactic = PTactic' PTerm
 
 data PDo' t = DoExp  FC t
@@ -583,6 +608,13 @@
 deriving instance Binary PDo' 
 !-}
 
+instance Sized a => Sized (PDo' a) where
+  size (DoExp fc t) = 1 + size fc + size t
+  size (DoBind fc nm t) = 1 + size fc + size nm + size t
+  size (DoBindP fc l r) = 1 + size fc + size l + size r
+  size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
+  size (DoLetP fc l r) = 1 + size fc + size l + size r
+
 type PDo = PDo' PTerm
 
 -- The priority gives a hint as to elaboration order. Best to elaborate
@@ -600,6 +632,13 @@
                               getScript :: t,
                               getTm :: t }
     deriving (Show, Eq, Functor)
+
+instance Sized a => Sized (PArg' a) where
+  size (PImp p l nm trm) = 1 + size nm + size trm
+  size (PExp p l trm) = 1 + size trm
+  size (PConstraint p l trm) = 1 + size trm
+  size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
+
 {-! 
 deriving instance Binary PArg' 
 !-}
@@ -712,6 +751,9 @@
 instance Show PTerm where
     show tm = showImp False tm
 
+instance Pretty PTerm where
+  pretty = prettyImp False
+
 instance Show PDecl where
     show d = showDeclImp False d
 
@@ -765,6 +807,186 @@
 getAll :: [PArg] -> [PTerm]
 getAll = map getTm 
 
+prettyImp :: Bool -> PTerm -> Doc
+prettyImp impl = prettySe 10
+  where
+    prettySe p (PQuote r) =
+      if size r > breakingSize then
+        text "![" $$ pretty r <> text "]"
+      else
+        text "![" <> pretty r <> text "]"
+    prettySe p (PRef fc n) =
+      if impl then
+        pretty n
+      else
+        prettyBasic n
+      where
+        prettyBasic n@(UN _) = pretty n
+        prettyBasic (MN _ s) = text s
+        prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map text $ reverse s))) <> prettyBasic n
+    prettySe p (PLam n ty sc) =
+      bracket p 2 $
+        if size sc > breakingSize then
+          text "λ" <> pretty n <+> text "=>" $+$ pretty sc
+        else
+          text "λ" <> pretty n <+> text "=>" <+> pretty sc
+    prettySe p (PLet n ty v sc) =
+      bracket p 2 $
+        if size sc > breakingSize then
+          text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$
+            nest nestingSize (prettySe 10 sc)
+        else
+          text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>
+            prettySe 10 sc
+    prettySe p (PPi (Exp l s) n ty sc)
+      | n `elem` allNamesIn sc || impl =
+          let open = if l then text "|" <> lparen else lparen in
+            bracket p 2 $
+              if size sc > breakingSize then
+                open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
+                  st <+> text "->" $+$ prettySe 10 sc
+              else
+                open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
+                  st <+> text "->" <+> prettySe 10 sc
+      | otherwise                      =
+          bracket p 2 $
+            if size sc > breakingSize then
+              prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc
+            else
+              prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc
+      where
+        st =
+          case s of
+            Static -> text "[static]"
+            _      -> empty
+    prettySe p (PPi (Imp l s) n ty sc)
+      | impl =
+          let open = if l then text "|" <> lbrace else lbrace in
+            bracket p 2 $
+              if size sc > breakingSize then
+                open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
+                  st <+> text "->" <+> prettySe 10 sc
+              else
+                open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
+                  st <+> text "->" <+> prettySe 10 sc
+      | otherwise = prettySe 10 sc
+      where
+        st =
+          case s of
+            Static -> text $ "[static]"
+            _      -> empty
+    prettySe p (PPi (Constraint _ _) n ty sc) =
+      bracket p 2 $
+        if size sc > breakingSize then
+          prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
+        else
+          prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc
+    prettySe p (PPi (TacImp _ _ s) n ty sc) =
+      bracket p 2 $
+        if size sc > breakingSize then
+          lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
+            rbrace <+> text "->" $+$ prettySe 10 sc
+        else
+          lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
+            rbrace <+> text "->" <+> prettySe 10 sc
+    prettySe p (PApp _ (PRef _ f) [])
+      | not impl = pretty f
+    prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)
+      | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =
+          let [l, r] = getExps args in
+            bracket p 1 $
+              if size r > breakingSize then
+                prettySe 1 l <+> pretty op $+$ prettySe 0 r
+              else
+                prettySe 1 l <+> pretty op <+> prettySe 0 r
+    prettySe p (PApp _ f as) =
+      let args = getExps as in
+        bracket p 1 $
+          prettySe 1 f <+>
+            if impl then
+              foldl fS empty as
+              -- foldr (<+>) empty $ map prettyArgS as
+            else
+              foldl fSe empty args
+              -- foldr (<+>) empty $ map prettyArgSe args
+      where
+        fS l r =
+          if size r > breakingSize then
+            l $+$ nest nestingSize (prettyArgS r)
+          else
+            l <+> prettyArgS r
+
+        fSe l r =
+          if size r > breakingSize then
+            l $+$ nest nestingSize (prettyArgSe r)
+          else
+            l <+> prettyArgSe r
+    prettySe p (PCase _ scr opts) =
+      text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody
+      where
+        prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts
+
+        sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r
+    prettySe p (PHidden tm) = text "." <> prettySe 0 tm
+    prettySe p (PRefl _) = text "refl"
+    prettySe p (PResolveTC _) = text "resolvetc"
+    prettySe p (PTrue _) = text "()"
+    prettySe p (PFalse _) = text "_|_"
+    prettySe p (PEq _ l r) =
+      bracket p 2 $
+        if size r > breakingSize then
+          prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)
+        else
+          prettySe 10 l <+> text "=" <+> prettySe 10 r
+    prettySe p (PTyped l r) =
+      lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
+    prettySe p (PPair _ l r) =
+      if size r > breakingSize then
+        lparen <> prettySe 10 l <> text "," $+$
+          prettySe 10 r <> rparen
+      else
+        lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen
+    prettySe p (PDPair _ l t r) =
+      if size r > breakingSize then
+        lparen <> prettySe 10 l <+> text "**" $+$
+          prettySe 10 r <> rparen
+      else
+        lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen
+    prettySe p (PAlternative as) =
+      lparen <> text "|" <> prettyAs <> text "|" <> rparen
+        where
+          prettyAs =
+            foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
+    prettySe p PSet = text "Set"
+    prettySe p (PConstant c) = pretty c
+    -- XXX: add pretty for tactics
+    prettySe p (PProof ts) =
+      text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
+    prettySe p (PTactics ts) =
+      text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
+    prettySe p (PMetavar n) = text "?" <> pretty n
+    prettySe p (PReturn f) = text "return"
+    prettySe p PImpossible = text "impossible"
+    prettySe p Placeholder = text "_"
+    prettySe p (PDoBlock _) = text "do block pretty not implemented"
+    prettySe p (PElabError s) = pretty s
+
+    prettySe p _ = text "test"
+
+    prettyArgS (PImp _ _ n tm) = prettyArgSi (n, tm)
+    prettyArgS (PExp _ _ tm)   = prettyArgSe tm
+    prettyArgS (PConstraint _ _ tm) = prettyArgSc tm
+    prettyArgS (PTacImplicit _ _ n _ tm) = prettyArgSti (n, tm)
+
+    prettyArgSe arg = prettySe 0 arg
+    prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
+    prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace
+    prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
+
+    bracket outer inner doc
+      | inner > outer = lparen <> doc <> rparen
+      | otherwise     = doc
+        
 showImp :: Bool -> PTerm -> String
 showImp impl tm = se 10 tm where
     se p (PQuote r) = "![" ++ show r ++ "]"
@@ -773,7 +995,9 @@
       where showbasic n@(UN _) = show n
             showbasic (MN _ s) = s
             showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
-    se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc
+    se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ 
+                            (if impl then " : " ++ se 10 ty else "") ++ " => " 
+                            ++ se 10 sc
     se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
                             " in " ++ se 10 sc 
     se p (PPi (Exp l s) n ty sc)
@@ -845,6 +1069,66 @@
 
     bracket outer inner str | inner > outer = "(" ++ str ++ ")"
                             | otherwise = str
+
+{-
+ PQuote Raw
+           | PRef FC Name
+           | PLam Name PTerm PTerm
+           | PPi  Plicity Name PTerm PTerm
+           | PLet Name PTerm PTerm PTerm 
+           | PTyped PTerm PTerm -- term with explicit type
+           | PApp FC PTerm [PArg]
+           | PCase FC PTerm [(PTerm, PTerm)]
+           | PTrue FC
+           | PFalse FC
+           | PRefl FC
+           | PResolveTC FC
+           | PEq FC PTerm PTerm
+           | PPair FC PTerm PTerm
+           | PDPair FC PTerm PTerm PTerm
+           | PAlternative [PTerm]
+           | PHidden PTerm -- irrelevant or hidden pattern
+           | PSet
+           | PConstant Const
+           | Placeholder
+           | PDoBlock [PDo]
+           | PIdiom FC PTerm
+           | PReturn FC
+           | PMetavar Name
+           | PProof [PTactic]
+           | PTactics [PTactic] -- as PProof, but no auto solving
+           | PElabError Err -- error to report on elaboration
+           | PImpossible -- special case for declaring when an LHS can't typecheck
+-}
+
+instance Sized PTerm where
+  size (PQuote rawTerm) = size rawTerm
+  size (PRef fc name) = size name
+  size (PLam name ty bdy) = 1 + size ty + size bdy
+  size (PPi plicity name ty bdy) = 1 + size ty + size bdy
+  size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
+  size (PTyped trm ty) = 1 + size trm + size ty
+  size (PApp fc name args) = 1 + size args
+  size (PCase fc trm bdy) = 1 + size trm + size bdy
+  size (PTrue fc) = 1
+  size (PFalse fc) = 1
+  size (PRefl fc) = 1
+  size (PResolveTC fc) = 1
+  size (PEq fc left right) = 1 + size left + size right
+  size (PPair fc left right) = 1 + size left + size right
+  size (PDPair fs left ty right) = 1 + size left + size ty + size right
+  size (PAlternative alts) = 1 + size alts
+  size (PHidden hidden) = size hidden
+  size PSet = 1
+  size (PConstant const) = 1 + size const
+  size Placeholder = 1
+  size (PDoBlock dos) = 1 + size dos
+  size (PIdiom fc term) = 1 + size term
+  size (PReturn fc) = 1
+  size (PMetavar name) = 1
+  size (PProof tactics) = size tactics
+  size (PElabError err) = size err
+  size PImpossible = 1
 
 allNamesIn :: PTerm -> [Name]
 allNamesIn tm = nub $ ni [] tm 
diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs
--- a/src/Idris/Delaborate.hs
+++ b/src/Idris/Delaborate.hs
@@ -47,8 +47,10 @@
     deFn env (P _ n _) [l,r]     | n == pairTy  = PPair un (de env l) (de env r)
                                  | n == eqCon   = PRefl un
                                  | n == UN "lazy" = de env r
-                                 | n == UN "Exists" = PDPair un (de env l) Placeholder
-                                                                (de env r)
+    deFn env (P _ n _) [ty, Bind x (Lam _) r]
+                                 | n == UN "Exists" 
+                                       = PDPair un (PRef un x) (de env ty)
+                                                   (de env (instantiate (P Bound x ty) r))
     deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair un (de env l) (de env r)
                                  | n == eqTy    = PEq un (de env l) (de env r)
                                  | n == UN "Ex_intro" = PDPair un (de env l) Placeholder
@@ -71,6 +73,7 @@
 pshow i (CantUnify x y e s) 
     = "Can't unify " ++ show (delab i x)
         ++ " with " ++ show (delab i y) ++
+--         " (" ++ show x ++ " and " ++ show y ++ ") " ++
         case e of
             Msg "" -> ""
             _ -> "\n\nSpecifically:\n\t " ++ pshow i e 
diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs
--- a/src/Idris/ElabDecls.hs
+++ b/src/Idris/ElabDecls.hs
@@ -207,11 +207,12 @@
          mapM_ (elabCaseBlock info) is
          ctxt <- getContext
          (cty, _)  <- recheckC fc [] t'
-         tyIs cty
-         logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty
+         let cty' = normaliseC ctxt [] cty
+         tyIs cty'
+         logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'
          addIBC (IBCDef n)
-         forceArgs n cty
-         return (n, cty)
+         forceArgs n cty'
+         return (n, cty')
   where
     tyIs (Bind n b sc) = tyIs sc
     tyIs t | (P _ n' _, _) <- unApply t 
@@ -801,6 +802,7 @@
           dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as
           dappname t = t
 
+
 pbinds (Bind n (PVar t) sc) = do attack; patbind n 
                                  pbinds sc
 pbinds tm = return ()
@@ -862,7 +864,6 @@
     = do i <- get
          put (i { idris_dsls = addDef n dsl (idris_dsls i) }) 
          addIBC (IBCDSL n)
-
 elabDecl' info (PDirective i) = i
 
 elabCaseBlock info d@(PClauses f o n ps) 
diff --git a/src/Idris/ElabTerm.hs b/src/Idris/ElabTerm.hs
--- a/src/Idris/ElabTerm.hs
+++ b/src/Idris/ElabTerm.hs
@@ -102,8 +102,12 @@
     elab' ina (PFalse fc)    = elab' ina (PRef fc falseTy)
     elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes
        = resolveTC 5 fn ist
-    elab' ina (PResolveTC fc) = do c <- unique_hole (MN 0 "c")
-                                   instanceArg c
+    elab' ina (PResolveTC fc) 
+        | pattern = do c <- unique_hole (MN 0 "c")
+                       instanceArg c
+        | otherwise = try (resolveTC 2 fn ist)
+                          (do c <- unique_hole (MN 0 "c")
+                              instanceArg c)
     elab' ina (PRefl fc)     = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,
                                                            pimp (MN 0 "x") Placeholder])
     elab' ina (PEq fc l r)   = elab' ina (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,
diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs
--- a/src/Idris/Parser.hs
+++ b/src/Idris/Parser.hs
@@ -1261,8 +1261,8 @@
          <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'
                      return [PDirective (do i <- getIState
                                             putIState (i { default_access = acc }))])
-         <|> do lchar '%'; reserved "logging"; i <- natural;
-                return [PDirective (setLogLevel (fromInteger i))] 
+         <|> try (do lchar '%'; reserved "logging"; i <- natural;
+                     return [PDirective (setLogLevel (fromInteger i))])
 
 pTactic :: SyntaxInfo -> IParser PTactic
 pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
diff --git a/src/Idris/Prover.hs b/src/Idris/Prover.hs
--- a/src/Idris/Prover.hs
+++ b/src/Idris/Prover.hs
@@ -17,6 +17,8 @@
 import System.Console.Haskeline
 import Control.Monad.State
 
+import Util.Pretty
+
 prover :: Bool -> Name -> Idris ()
 prover lit x =
            do ctxt <- getContext
@@ -55,31 +57,49 @@
                      OK (a, st') -> return (a, st')
                      Error a -> do i <- get
                                    fail (pshow i a)
-                  
+
 dumpState :: IState -> ProofState -> IO ()
-dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"
-dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _)
-   = do let OK ty = goalAtFocus ps
-        let OK env = envAtFocus ps
---         putStrLn $ "Other goals: " ++ show hs ++ "\n"
-        putStr $ "\n" ++ showPs (reverse env)
-        putStrLn $ "---------------------------------- (" ++ show nm
-                     ++ ") --------"
-        putStrLn $ show h ++ " : " ++ showG ty ++ "\n"
+dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) =
+  putStrLn . render $ pretty nm <> colon <+> text "No more goals."
+dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _) = do
+  let OK ty  = goalAtFocus ps
+  let OK env = envAtFocus ps
+  putStrLn . render $
+    prettyOtherGoals hs $$
+    prettyAssumptions env $$
+    prettyGoal ty
   where
-    tshow t = show (delab ist t)
+    -- XXX
+    tPretty t = pretty $ delab ist t
 
-    showPs [] = ""
-    showPs ((MN _ "rewrite_rule", _) : bs) = showPs bs
-    showPs ((n, Let t v) : bs)
-        = "  " ++ show n ++ " = " ++ tshow v ++ " : " ++
-            tshow t ++ "\n" ++ showPs bs
-    showPs ((n, b) : bs)
-        = "  " ++ show n ++ " : " ++
-            tshow (binderTy b) ++ "\n" ++ showPs bs
+    prettyPs [] = empty
+    prettyPs ((MN _ "rewrite_rule", _) : bs) = prettyPs bs
+    prettyPs ((n, Let t v) : bs) =
+      nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>
+        tPretty t $$ prettyPs bs)
+    prettyPs ((n, b) : bs) = 
+      pretty n <+> colon <+> tPretty (binderTy b) $$ prettyPs bs
 
-    showG (Guess t v) = tshow t ++ " =?= " ++ tshow v
-    showG b = tshow (binderTy b)
+    prettyG (Guess t v) = tPretty t <+> text "=?=" <+> tPretty v
+    prettyG b = tPretty $ binderTy b
+
+    prettyGoal ty =
+      text "----------                 Goal:                  ----------" $$
+      pretty h <> colon $$ nest nestingSize (prettyG ty)
+
+    prettyAssumptions env =
+      if length env == 0 then
+        empty
+      else
+        text "----------              Assumptions:              ----------" $$
+        nest nestingSize (prettyPs $ reverse env)
+
+    prettyOtherGoals hs =
+      if length hs == 0 then
+        empty
+      else
+        text "----------              Other goals:              ----------" $$
+        pretty hs
 
 lifte :: ElabState [PDecl] -> ElabD a -> Idris a
 lifte st e = do (v, _) <- elabStep st e
diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs
--- a/src/Idris/REPL.hs
+++ b/src/Idris/REPL.hs
@@ -151,9 +151,9 @@
                        ist <- get
                        imp <- impShow
                        case lookupTy Nothing n ctxt of
-                        [t] -> iputStrLn $ show n ++ " : " ++
-                                  showImp imp (delab ist t)
-                        _ -> iputStrLn $ "No such variable " ++ show n
+                        ts@(_:_) -> mapM_ (\t -> iputStrLn $ show n ++ " : " ++
+                                                       showImp imp (delab ist t)) ts
+                        [] -> iputStrLn $ "No such variable " ++ show n
 process fn (Check t) = do (tm, ty) <- elabVal toplevel False t
                           ctxt <- getContext
                           ist <- get 
@@ -188,7 +188,7 @@
                                 [t] -> iputStrLn (showTotal t i)
                                 _ -> return ()
 process fn (Info n) = do i <- get
-                         let oi = lookupCtxt Nothing n (idris_optimisation i)
+                         let oi = lookupCtxtName Nothing n (idris_optimisation i)
                          when (not (null oi)) $ iputStrLn (show oi)
                          let si = lookupCtxt Nothing n (idris_statics i)
                          when (not (null si)) $ iputStrLn (show si)
diff --git a/src/Util/Pretty.hs b/src/Util/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Util/Pretty.hs
@@ -0,0 +1,33 @@
+module Util.Pretty (
+  module Text.PrettyPrint.HughesPJ,
+  Sized(..), breakingSize, nestingSize,
+  Pretty(..)
+) where
+
+import Text.PrettyPrint.HughesPJ
+
+-- A rough notion of size for pretty printing various types.
+class Sized a where
+  size :: a -> Int
+
+instance (Sized a, Sized b) => Sized (a, b) where
+  size (left, right) = 1 + size left + size right
+
+instance Sized a => Sized [a] where
+  size = sum . map size
+
+-- The maximum size before we break on to another line.
+breakingSize :: Int
+breakingSize = 15
+
+nestingSize :: Int
+nestingSize = 1
+
+class Pretty a where
+  pretty :: a -> Doc
+
+instance Pretty () where
+  pretty () = text "()"
+
+instance Pretty a => Pretty [a] where
+  pretty l = foldr ($$) empty $ map pretty l