diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -7,50 +7,16 @@
 Idris (http://idris-lang.org/) is a general-purpose functional programming
 language with dependent types.
 
-## Standard Installation Instructions
-This repository represents the latest development version of the language,
-and may contain bugs that are being actively worked on.
-For those who wish to use a more stable version of Idris please consider
-installing the latest version that has been released on Hackage.
-Installation instructions for various platforms can be [found on the Idris Wiki](https://github.com/idris-lang/Idris-dev/wiki/Installation-Instructions).
-
-## Installing Development Versions
-
-If you like to work against the latest development version, please consider
-using Cabal Sandboxes to minimise disruption to your local Haskell setup.
-Instructions for installing Idris HEAD within a cabal sandbox are
-[available on the Idris Wiki](https://github.com/idris-lang/Idris-dev/wiki/Installing-an-Idris-Development-version-in-a-sandbox).
-
-To configure, edit config.mk. The default values should work for most people.
-
-Idris is built using a Makefile common targets include:
-
-* `make` This will install everything using cabal and
-typecheck the libraries.
-* `make test` This target execute the test suite.
-* `make relib` This target will typecheck and recompile the standard library.
-
-Idris has an optional buildtime dependency on the C library `libffi`. If you
-would like to use the features that it enables, make sure that it is compiled
-for the same architecture as your Haskell compiler (e.g. 64 bit libraries
-for 64 bit ghc). By default, Idris builds without it. To build with it, pass
-the flag `-f FFI`.
-
-To build with `libffi` by default, create a `custom.mk` file and add the
-following line to it:
-
-`CABALFLAGS += -f FFI`
-
-The file custom.mk-alldeps is a suitable example.
-
-The continuous integration builds on travis-ci.org are built using the
-ghc-flag -Werror. To enable this behaviour locally also, please compile
-using `make CI=true` or adding the following line into `custom.mk`:
+## Installation Guides.
 
-`CI = true`
+This repository represents the latest development version of the
+language, and may contain bugs that are being actively worked on.  For
+those who wish to use a more stable version of Idris please consider
+installing the latest version that has been released on Hackage.
+Installation instructions for various platforms can be
+[found on the Idris Wiki](https://github.com/idris-lang/Idris-dev/wiki/Installation-Instructions).
 
-If you are only compiling for installing the most current version, you can
-omit the CI flag, but please make sure you use it if you want to contribute.
+More information about building Idris from source has been detailed in the [Installation Guide](INSTALL.md)
 
 ## Code Generation
 
diff --git a/idris.cabal b/idris.cabal
--- a/idris.cabal
+++ b/idris.cabal
@@ -1,5 +1,5 @@
 Name:           idris
-Version:        0.9.20.1
+Version:        0.9.20.2
 License:        BSD3
 License-file:   LICENSE
 Author:         Edwin Brady
@@ -115,6 +115,7 @@
                        libs/base/Control/*.idr
                        libs/base/Control/Monad/*.idr
                        libs/base/Data/*.idr
+                       libs/base/Data/List/*.idr
                        libs/base/Data/Vect/*.idr
                        libs/base/Debug/*.idr
                        libs/base/Language/Reflection/*.idr
@@ -309,6 +310,9 @@
                        test/reg066/run
                        test/reg066/*.idr
                        test/reg066/expected
+                       test/reg067/run
+                       test/reg067/*.idr
+                       test/reg067/expected
 
                        test/basic001/run
                        test/basic001/*.idr
@@ -570,6 +574,9 @@
                        test/meta002/run
                        test/meta002/*.idr
                        test/meta002/expected
+                       test/meta004/run
+                       test/meta004/*.idr
+                       test/meta004/expected
 
                        test/primitives001/run
                        test/primitives001/*.idr
@@ -971,8 +978,11 @@
                 , vector < 0.12
                 , vector-binary-instances < 0.3
                 , zip-archive > 0.2.3.5 && < 0.2.4
-                , zlib < 0.6
                 , safe
+  -- zlib >= 0.6.1 is broken with GHC < 7.10.3
+  if impl(ghc < 7.10.3)
+     build-depends: zlib < 0.6.1
+
   Extensions:     MultiParamTypeClasses
                 , DeriveFoldable
                 , DeriveTraversable
diff --git a/libs/base/Data/Complex.idr b/libs/base/Data/Complex.idr
--- a/libs/base/Data/Complex.idr
+++ b/libs/base/Data/Complex.idr
@@ -25,7 +25,7 @@
             plus_i = User 6
 
 
--- when we have a type class 'Fractional' (which contains Float and Double),
+-- when we have a type class 'Fractional' (which contains Double),
 -- we can do:
 {-
 instance Fractional a => Fractional (Complex a) where
@@ -40,16 +40,16 @@
 
 ------------------------------ Polarform
 
-mkPolar : Float -> Float -> Complex Float
+mkPolar : Double -> Double -> Complex Double
 mkPolar radius angle = radius * cos angle :+ radius * sin angle
 
-cis : Float -> Complex Float
+cis : Double -> Complex Double
 cis angle = cos angle :+ sin angle
 
-magnitude : Complex Float -> Float
+magnitude : Complex Double -> Double
 magnitude (r:+i) = sqrt (r*r+i*i)
 
-phase : Complex Float -> Float
+phase : Complex Double -> Double
 phase (x:+y) = atan2 y x
 
 
@@ -62,13 +62,13 @@
     map f (r :+ i) = f r :+ f i
 
 -- We can't do "instance Num a => Num (Complex a)" because
--- we need "abs" which needs "magnitude" which needs "sqrt" which needs Float
-instance Num (Complex Float) where
+-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Double
+instance Num (Complex Double) where
     (+) (a:+b) (c:+d) = ((a+c):+(b+d))
     (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))
     fromInteger x = (fromInteger x:+0)
 
-instance Neg (Complex Float) where
+instance Neg (Complex Double) where
     negate = map negate
     (-) (a:+b) (c:+d) = ((a-c):+(b-d))
     abs (a:+b) = (magnitude (a:+b):+0)
diff --git a/libs/base/Data/List/Quantifiers.idr b/libs/base/Data/List/Quantifiers.idr
new file mode 100644
--- /dev/null
+++ b/libs/base/Data/List/Quantifiers.idr
@@ -0,0 +1,75 @@
+module Data.List.Quantifiers
+
+import Data.List
+
+||| A proof that some element of a list satisfies some property
+|||
+||| @ P the property to be satsified
+data Any : (P : a -> Type) -> List a -> Type where
+  ||| A proof that the satisfying element is the first one in the `List`
+  Here  : {P : a -> Type} -> {xs : List a} -> P x -> Any P (x :: xs)
+  ||| A proof that the satsifying element is in the tail of the `List`
+  There : {P : a -> Type} -> {xs : List a} -> Any P xs -> Any P (x :: xs)
+
+||| No element of an empty list satisfies any property
+anyNilAbsurd : {P : a -> Type} -> Any P Nil -> Void
+anyNilAbsurd (Here _) impossible
+anyNilAbsurd (There _) impossible
+
+instance Uninhabited (Any p Nil) where
+  uninhabited = anyNilAbsurd
+
+||| Eliminator for `Any`
+anyElim : {xs : List a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
+anyElim _ f (Here p) = f p
+anyElim f _ (There p) = f p
+
+||| Given a decision procedure for a property, determine if an element of a
+||| list satisfies it.
+|||
+||| @ P the property to be satisfied
+||| @ dec the decision procedure
+||| @ xs the list to examine
+any : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : List a) -> Dec (Any P xs)
+any _ Nil = No anyNilAbsurd
+any p (x::xs) with (p x)
+  | Yes prf = Yes (Here prf)
+  | No prf =
+    case any p xs of
+      Yes prf' => Yes (There prf')
+      No prf' => No (anyElim prf' prf)
+
+||| A proof that all elements of a list satisfy a property. It is a list of
+||| proofs, corresponding element-wise to the `List`.
+data All : (P : a -> Type) -> List a -> Type where
+  Nil : {P : a -> Type} -> All P Nil
+  (::) : {P : a -> Type} -> {xs : List a} -> P x -> All P xs -> All P (x :: xs)
+
+||| If there does not exist an element that satifies the property, then it is
+||| the case that all elements do not satisfy.
+negAnyAll : {P : a -> Type} -> {xs : List a} -> Not (Any P xs) -> All (\x => Not (P x)) xs
+negAnyAll {xs=Nil} _ = Nil
+negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x))
+
+notAllHere : {P : a -> Type} -> {xs : List a} -> Not (P x) -> All P (x :: xs) -> Void
+notAllHere _ Nil impossible
+notAllHere np (p :: _) = np p
+
+notAllThere : {P : a -> Type} -> {xs : List a} -> Not (All P xs) -> All P (x :: xs) -> Void
+notAllThere _ Nil impossible
+notAllThere np (_ :: ps) = np ps
+
+||| Given a decision procedure for a property, decide whether all elements of
+||| a list satisfy it.
+|||
+||| @ P the property
+||| @ dec the decision procedure
+||| @ xs the list to examine
+all : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : List a) -> Dec (All P xs)
+all _ Nil = Yes Nil
+all d (x::xs) with (d x)
+  | No prf = No (notAllHere prf)
+  | Yes prf =
+    case all d xs of
+      Yes prf' => Yes (prf :: prf')
+      No prf' => No (notAllThere prf')
diff --git a/libs/base/Data/String.idr b/libs/base/Data/String.idr
--- a/libs/base/Data/String.idr
+++ b/libs/base/Data/String.idr
@@ -1,5 +1,14 @@
 module Data.String
 
+private
+parseNumWithoutSign : List Char -> Integer -> Maybe Integer
+parseNumWithoutSign []        acc = Just acc
+parseNumWithoutSign (c :: cs) acc = 
+  if (c >= '0' && c <= '9') 
+  then parseNumWithoutSign cs ((acc * 10) + (cast ((ord c) - (ord '0'))))
+  else Nothing
+         
+
 ||| Convert a positive number string to a Num.
 |||
 ||| ```idris example
@@ -15,15 +24,8 @@
       parsePosTrimmed ""             | StrNil         = Nothing
       parsePosTrimmed (strCons x xs) | (StrCons x xs) = 
         if (x == '+') 
-          then map fromInteger (parsePosAux (unpack xs) 0)
-          else map fromInteger (parsePosAux (unpack xs)  (cast (ord x - ord '0')))
-            where
-              parsePosAux : List Char -> Integer -> Maybe Integer
-              parsePosAux []        acc = Just acc
-              parsePosAux (c :: cs) acc = 
-                if (c >= '0' && c <= '9') 
-                  then parsePosAux cs ((acc * 10) + (cast ((ord c) - (ord '0'))))
-                  else Nothing
+          then map fromInteger (parseNumWithoutSign (unpack xs) 0)
+          else map fromInteger (parseNumWithoutSign (unpack xs)  (cast (ord x - ord '0')))
 
 
 ||| Convert a number string to a Num.
@@ -41,14 +43,68 @@
       parseIntTrimmed ""             | StrNil         = Nothing
       parseIntTrimmed (strCons x xs) | (StrCons x xs) = 
         if (x == '-') 
-          then map (\y => negate (fromInteger y)) (parseIntegerAux (unpack xs) 0)
+          then map (\y => negate (fromInteger y)) (parseNumWithoutSign (unpack xs) 0)
           else if (x == '+') 
-            then map fromInteger (parseIntegerAux (unpack xs) (cast {from=Int} 0))
-            else map fromInteger (parseIntegerAux (unpack xs) (cast (ord x - ord '0')))
-              where
-                parseIntegerAux : List Char -> Integer -> Maybe Integer
-                parseIntegerAux []        acc = Just acc
-                parseIntegerAux (c :: cs) acc = 
-                  if (c >= '0' && c <= '9') 
-                    then parseIntegerAux cs ((acc * 10) + (cast ((ord c) - (ord '0'))))
-                    else Nothing
+            then map fromInteger (parseNumWithoutSign (unpack xs) (cast {from=Int} 0))
+            else map fromInteger (parseNumWithoutSign (unpack xs) (cast (ord x - ord '0')))
+
+
+||| Convert a number string to a Double.
+|||
+||| ```idris example
+||| parseDouble "+123.123e-2"
+||| ```
+||| ```idris example
+||| parseDouble {a=Int} " -123.123E+2"
+||| ```
+||| ```idris example
+||| parseDouble {a=Int} " +123.123"
+||| ```
+parseDouble : String -> Maybe Double
+parseDouble = mkDouble . wfe . trim
+  where
+    mkDouble (Just (w, f, e)) = let ex = intPow 10 e in
+                                Just $ (w * ex + f * ex)
+    mkDouble Nothing = Nothing
+    
+    %assert_total
+    intPow : Integer -> Integer -> Double
+    intPow base exp = if exp > 0 then (num base exp) else 1 / (num base exp)
+      where
+        num base 0 = 1
+        num base e = if e < 0 
+                     then cast base * num base (e + 1)
+                     else cast base * num base (e - 1)
+
+    wfe : String -> Maybe (Double, Double, Integer)
+    wfe cs = case split (== '.') cs of
+               (wholeAndExp :: []) => 
+                 case split (\c => c == 'e' || c == 'E') wholeAndExp of
+                   (whole::exp::[]) =>  
+                     do
+                       w <- cast <$> parseInteger whole
+                       e <- parseInteger exp
+                       return (w, 0, e)
+                   (whole::[]) =>      
+                     do
+                       w <- cast <$> parseInteger whole
+                       return (w, 0, 0)
+                   _ => Nothing
+               (whole::fracAndExp::[]) =>
+                 case split (\c => c == 'e' || c == 'E') fracAndExp of
+                   (""::exp::[]) => Nothing
+                   (frac::exp::[]) =>  
+                     do
+                       w <- cast <$> parseInteger whole
+                       f <- (/ (pow 10 (length frac))) <$> 
+                            (cast <$> parseNumWithoutSign (unpack frac) 0)
+                       e <- parseInteger exp
+                       return (w, if w < 0 then (-f) else f, e)
+                   (frac::[]) =>      
+                     do
+                       w <- cast <$> parseInteger whole
+                       f <- (/ (pow 10 (length frac))) <$> 
+                            (cast <$> parseNumWithoutSign (unpack frac) 0)
+                       return (w, if w < 0 then (-f) else f, 0)
+                   _ => Nothing
+               _ => Nothing
diff --git a/libs/base/Data/Vect/Quantifiers.idr b/libs/base/Data/Vect/Quantifiers.idr
--- a/libs/base/Data/Vect/Quantifiers.idr
+++ b/libs/base/Data/Vect/Quantifiers.idr
@@ -19,6 +19,7 @@
 instance Uninhabited (Any p Nil) where
   uninhabited = anyNilAbsurd
 
+||| Eliminator for `Any`
 anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) -> Any P (x :: xs) -> b
 anyElim _ f (Here p) = f p
 anyElim f _ (There p) = f p
diff --git a/libs/base/Language/Reflection/Utils.idr b/libs/base/Language/Reflection/Utils.idr
--- a/libs/base/Language/Reflection/Utils.idr
+++ b/libs/base/Language/Reflection/Utils.idr
@@ -129,7 +129,7 @@
 
 instance Show ArithTy where
   showPrec d (ATInt t) = showCon d "ATInt" $ showArg t
-  showPrec d ATFloat   = "ATFloat"
+  showPrec d ATDouble   = "ATDouble"
 
 instance Show Const where
   showPrec d (I i)      = showCon d "I" $ showArg i
@@ -162,7 +162,7 @@
 
 instance Eq ArithTy where
   (ATInt x) == (ATInt y) = x == y
-  ATFloat   == ATFloat   = True
+  ATDouble  == ATDouble   = True
   _         == _         = False
 
 instance Eq Const where
@@ -349,3 +349,9 @@
 instance Show TyDecl where
   showPrec d (Declare fn args ret) = showCon d "Declare" $ showArg fn ++
                                      showArg args ++ showArg ret
+
+instance Show tm => Show (FunClause tm) where
+  showPrec d (MkFunClause lhs rhs) =
+      showCon d "MkFunClause" $ showArg lhs ++ showArg rhs
+  showPrec d (MkImpossibleClause lhs) =
+      showCon d "MkImpossibleClause" $ showArg lhs
diff --git a/libs/base/System.idr b/libs/base/System.idr
--- a/libs/base/System.idr
+++ b/libs/base/System.idr
@@ -56,7 +56,7 @@
 exit : Int -> IO ()
 exit code = foreign FFI_C "exit" (Int -> IO ()) code
 
-||| Get the Unix time
+||| Get the numbers of sections since 1st January 1970, 00:00 UTC 
 time : IO Integer
 time = do MkRaw t <- foreign FFI_C "idris_time" (IO (Raw Integer))
           return t
diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg
--- a/libs/base/base.ipkg
+++ b/libs/base/base.ipkg
@@ -17,6 +17,7 @@
           Data.HVect, Data.Vect.Quantifiers,
           Data.Complex,
           Data.Erased, Data.List,
+          Data.List.Quantifiers,
           Data.So, Data.String,
 
           Control.Isomorphism,
diff --git a/libs/contrib/Control/Algebra/NumericInstances.idr b/libs/contrib/Control/Algebra/NumericInstances.idr
--- a/libs/contrib/Control/Algebra/NumericInstances.idr
+++ b/libs/contrib/Control/Algebra/NumericInstances.idr
@@ -44,24 +44,24 @@
   unity = 1
 
 
-instance Semigroup Float where
+instance Semigroup Double where
   (<+>) = (+)
 
-instance Monoid Float where
+instance Monoid Double where
   neutral = 0
 
-instance Group Float where
+instance Group Double where
   inverse = (* -1)
 
-instance AbelianGroup Float
+instance AbelianGroup Double
 
-instance Ring Float where
+instance Ring Double where
   (<.>) = (*)
 
-instance RingWithUnity Float where
+instance RingWithUnity Double where
   unity = 1
 
-instance Field Float where
+instance Field Double where
   inverseM f _ = 1 / f
 
 
diff --git a/libs/effects/Effect/Default.idr b/libs/effects/Effect/Default.idr
--- a/libs/effects/Effect/Default.idr
+++ b/libs/effects/Effect/Default.idr
@@ -11,7 +11,7 @@
 instance Default Integer where
     default = 0
 
-instance Default Float where
+instance Default Double where
     default = 0
 
 instance Default Nat where
diff --git a/libs/effects/Effect/File.idr b/libs/effects/Effect/File.idr
--- a/libs/effects/Effect/File.idr
+++ b/libs/effects/Effect/File.idr
@@ -79,14 +79,14 @@
                                     k True (FH h)
     handle (FH h) Close      k = do closeFile h
                                     k () ()
-    handle (FH h) ReadLine        k = do Right str <- fread h
+    handle (FH h) ReadLine        k = do Right str <- fGetLine h
                                          -- Need proper error handling!
                                              | Left err => k "" (FH h)
                                          k str (FH h)
-    handle (FH h) (WriteString str) k = do Right () <- fwrite h str
+    handle (FH h) (WriteString str) k = do Right () <- fPutStr h str
                                              | Left err => k () (FH h)
                                            k () (FH h)
-    handle (FH h) EOF             k = do e <- feof h
+    handle (FH h) EOF             k = do e <- fEOF h
                                          k e (FH h)
 
 instance Handler FileIO (IOExcept a) where
@@ -95,14 +95,14 @@
                                     k True (FH h)
     handle (FH h) Close      k = do ioe_lift $ closeFile h
                                     k () ()
-    handle (FH h) ReadLine        k = do Right str <- ioe_lift $ fread h
+    handle (FH h) ReadLine        k = do Right str <- ioe_lift $ fGetLine h
                                          -- Need proper error handling!
                                              | Left err => k "" (FH h)
                                          k str (FH h)
-    handle (FH h) (WriteString str) k = do Right () <- ioe_lift $ fwrite h str
+    handle (FH h) (WriteString str) k = do Right () <- ioe_lift $ fPutStr h str
                                              | Left err => k () (FH h)
                                            k () (FH h)
-    handle (FH h) EOF             k = do e <- ioe_lift $ feof h
+    handle (FH h) EOF             k = do e <- ioe_lift $ fEOF h
                                          k e (FH h)
 
 -- -------------------------------------------------------------- [ The Effect ]
diff --git a/libs/prelude/Builtins.idr b/libs/prelude/Builtins.idr
--- a/libs/prelude/Builtins.idr
+++ b/libs/prelude/Builtins.idr
@@ -19,6 +19,10 @@
      ||| @b the right element of the pair
      MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
 
+  -- Usage hints for erasure analysis
+  %used MkPair a
+  %used MkPair b
+
   ||| The non-dependent pair type, also known as conjunction, usable with
   ||| UniqueTypes.
   ||| @A the type of the left elements in the pair
@@ -29,6 +33,10 @@
      ||| @b the right element of the pair
      MkUPair : {A, B : AnyType} -> (a : A) -> (b : B) -> UPair A B
 
+  -- Usage hints for erasure analysis
+  %used MkUPair a
+  %used MkUPair b
+
   ||| Dependent pairs
   |||
   ||| Dependent pairs represent existential quantification - they consist of a
@@ -48,7 +56,12 @@
     
 ||| The eliminator for the `Void` type.
 void : Void -> a
-void {a} v = elim_for Void (\_ => a) v
+-- We can't define void yet. We can't define a function with no clauses without
+-- elaborator reflection, and we can't do elaborator reflection without
+-- Language.Reflection.Elab, and Language.Reflection.Elab depends on Builtins.
+-- We can't delay the declaration of void, because Prelude.Uninhabited depends on
+-- it, Prelude.Nat depends on Prelude.Uninhabited, and Language.Reflection.Elab
+-- depends on Prelude.Nat. Instead, void is defined in Prelude.idr
 
 ||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
 data Symbol_ : String -> Type where
@@ -152,9 +165,11 @@
 really_believe_me : a -> b
 really_believe_me x = prim__believe_me _ _ x
 
--- Deprecated - for backward compatibility
+||| Deprecated alias for `Double`, for the purpose of backwards
+||| compatibility. Idris does not support 32 bit floats at present.
 Float : Type
 Float = Double
+%deprecate Float
 
 -- Pointers as external primitive; there's no literals for these, so no
 -- need for them to be part of the compiler.
diff --git a/libs/prelude/Decidable/Equality.idr b/libs/prelude/Decidable/Equality.idr
--- a/libs/prelude/Decidable/Equality.idr
+++ b/libs/prelude/Decidable/Equality.idr
@@ -178,7 +178,7 @@
 instance DecEq Integer where
     decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq
        where primitiveEq : x = y
-             primitiveEq = believe_me (Refl {x})
+             primitiveEq = really_believe_me (Refl {x})
              postulate primitiveNotEq : x = y -> Void
 
 
diff --git a/libs/prelude/IO.idr b/libs/prelude/IO.idr
--- a/libs/prelude/IO.idr
+++ b/libs/prelude/IO.idr
@@ -162,7 +162,7 @@
   ||| Supported C foreign types
   data C_Types : Type -> Type where
        C_Str   : C_Types String
-       C_Float : C_Types Float
+       C_Float : C_Types Double
        C_Ptr   : C_Types Ptr
        C_MPtr  : C_Types ManagedPtr
        C_Unit  : C_Types ()
@@ -221,7 +221,7 @@
 
   data JS_Types : Type -> Type where
        JS_Str   : JS_Types String
-       JS_Float : JS_Types Float
+       JS_Float : JS_Types Double
        JS_Ptr   : JS_Types Ptr
        JS_Unit  : JS_Types ()
        JS_FnT   : JS_FnTypes a -> JS_Types (JsFn a)
diff --git a/libs/prelude/Language/Reflection.idr b/libs/prelude/Language/Reflection.idr
--- a/libs/prelude/Language/Reflection.idr
+++ b/libs/prelude/Language/Reflection.idr
@@ -70,10 +70,10 @@
 
 data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar
 
-data ArithTy = ATInt Language.Reflection.IntTy | ATFloat
+data ArithTy = ATInt Language.Reflection.IntTy | ATDouble
 
 ||| Primitive constants
-data Const = I Int | BI Integer | Fl Float | Ch Char | Str String
+data Const = I Int | BI Integer | Fl Double | Ch Char | Str String
            | B8 Bits8 | B16 Bits16 | B32 Bits32 | B64 Bits64
            | AType ArithTy | StrType
            | VoidType | Forgot
@@ -89,7 +89,7 @@
 instance ReflConst Integer where
    toConst = BI
 
-instance ReflConst Float where
+instance ReflConst Double where
    toConst = Fl
 
 instance ReflConst Char where
@@ -366,12 +366,12 @@
   quotedTy = `(Int)
   quote x = RConstant (I x)
 
-instance Quotable Float TT where
-  quotedTy = `(Float)
+instance Quotable Double TT where
+  quotedTy = `(Double)
   quote x = TConst (Fl x)
 
-instance Quotable Float Raw where
-  quotedTy = `(Float)
+instance Quotable Double Raw where
+  quotedTy = `(Double)
   quote x = RConstant (Fl x)
 
 instance Quotable Char TT where
@@ -541,12 +541,12 @@
 instance Quotable ArithTy TT where
   quotedTy = `(ArithTy)
   quote (ATInt x) = `(ATInt ~(quote x))
-  quote ATFloat = `(ATFloat)
+  quote ATDouble = `(ATDouble)
 
 instance Quotable ArithTy Raw where
   quotedTy = `(ArithTy)
   quote (ATInt x) = `(ATInt ~(quote {t=Raw} x))
-  quote ATFloat = `(ATFloat)
+  quote ATDouble = `(ATDouble)
 
 instance Quotable Const TT where
   quotedTy = `(Const)
diff --git a/libs/prelude/Language/Reflection/Elab.idr b/libs/prelude/Language/Reflection/Elab.idr
--- a/libs/prelude/Language/Reflection/Elab.idr
+++ b/libs/prelude/Language/Reflection/Elab.idr
@@ -69,17 +69,16 @@
   returnType : Raw
 
 
--- Note: FunClause is not a record because impossible clauses may be
--- added at some point.
 ||| A single pattern-matching clause
-data FunClause : Type where
-  MkFunClause : (lhs, rhs : Raw) -> FunClause
+data FunClause : Type -> Type where
+  MkFunClause : (lhs, rhs : a) -> FunClause a
+  MkImpossibleClause : (lhs : a) -> FunClause a
 
 ||| A reflected function definition.
-record FunDefn where
+record FunDefn a where
   constructor DefineFun
   name : TTName
-  clauses : List FunClause
+  clauses : List (FunClause a)
 
 
 data CtorArg = CtorParameter FunArg | CtorField FunArg
@@ -116,6 +115,7 @@
   Prim__Guess : Elab TT
   Prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))
   Prim__LookupDatatype : TTName -> Elab (List Datatype)
+  Prim__LookupFunDefn : TTName -> Elab (List (FunDefn TT))
   Prim__LookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
 
   Prim__Check : List (TTName, Binder TT) -> Raw -> Elab (TT, TT)
@@ -148,7 +148,7 @@
   Prim__Converts : (List (TTName, Binder TT)) -> TT -> TT -> Elab ()
 
   Prim__DeclareType : TyDecl -> Elab ()
-  Prim__DefineFunction : FunDefn -> Elab ()
+  Prim__DefineFunction : FunDefn Raw -> Elab ()
   Prim__AddInstance : TTName -> TTName -> Elab ()
   Prim__IsTCName : TTName -> Elab Bool
 
@@ -231,7 +231,20 @@
                             []    => fail [TextPart "No datatype named", NamePart n]
                             xs    => fail [TextPart "More than one datatype named", NamePart n]
 
+  ||| Find the reflected function definition of all functions whose names
+  ||| are overloadings of some name.
+  lookupFunDefn : TTName -> Elab (List (FunDefn TT))
+  lookupFunDefn n = Prim__LookupFunDefn n
 
+  ||| Find the reflected function definition of a function, given its
+  ||| fully-qualified name. Fail if the name does not uniquely resolve
+  ||| to a function.
+  lookupFunDefnExact : TTName -> Elab (FunDefn TT)
+  lookupFunDefnExact n = case !(lookupFunDefn n) of
+                           [res] => return res
+                           []    => fail [TextPart "No function named", NamePart n]
+                           xs    => fail [TextPart "More than one function named", NamePart n]
+
   ||| Get the argument specification for each overloading of a name.
   lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))
   lookupArgs n = Prim__LookupArgs n
@@ -452,7 +465,7 @@
   ||| Define a function in the global context. The function must have
   ||| already been declared, either in ordinary Idris code or using
   ||| `declareType`.
-  defineFunction : FunDefn -> Elab ()
+  defineFunction : FunDefn Raw -> Elab ()
   defineFunction defun = Prim__DefineFunction defun
 
   ||| Register a new instance for type class resolution.
diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr
--- a/libs/prelude/Prelude.idr
+++ b/libs/prelude/Prelude.idr
@@ -37,6 +37,10 @@
 %default total
 
 -- Things that can't be elsewhere for import cycle reasons
+-- See comment after declaration of void in Builtins.idr
+-- for explanation of this definition's location
+%runElab (defineFunction $ DefineFun `{void} [])
+
 decAsBool : Dec p -> Bool
 decAsBool (Yes _) = True
 decAsBool (No _)  = False
@@ -202,6 +206,12 @@
     where go : List Nat -> List Int
           go [] = []
           go (x :: xs) = n + (cast x * inc) :: go xs
+
+instance Enum Char where
+  toNat c   = toNat (ord c)
+  fromNat n = chr (fromNat n)
+  
+  pred c = fromNat (pred (toNat c))
 
 syntax "[" [start] ".." [end] "]"
      = enumFromTo start end
diff --git a/libs/prelude/Prelude/Classes.idr b/libs/prelude/Prelude/Classes.idr
--- a/libs/prelude/Prelude/Classes.idr
+++ b/libs/prelude/Prelude/Classes.idr
@@ -37,7 +37,7 @@
 instance Eq Integer where
     (==) = boolOp prim__eqBigInt
 
-instance Eq Float where
+instance Eq Double where
     (==) = boolOp prim__eqFloat
 
 instance Eq Char where
@@ -118,7 +118,7 @@
                   GT
 
 
-instance Ord Float where
+instance Ord Double where
     compare x y = if (x == y) then EQ else
                   if (boolOp prim__sltFloat x y) then LT else
                   GT
@@ -170,7 +170,7 @@
     fromInteger = prim__truncBigInt_Int
 
 
-instance Num Float where
+instance Num Double where
     (+) = prim__addFloat
     (*) = prim__mulFloat
 
@@ -215,7 +215,7 @@
     (-) = prim__subInt
     abs x = if x < (prim__truncBigInt_Int 0) then -x else x
 
-instance Neg Float where
+instance Neg Double where
     negate x = prim__negFloat x
     (-) = prim__subFloat
     abs x = if x < (prim__toFloatBigInt 0) then -x else x
@@ -306,8 +306,8 @@
 
 -- ------------------------------------------------------------- [ Fractionals ]
 
-||| Fractional division of two Floats.
-(/) : Float -> Float -> Float
+||| Fractional division of two Doubles.
+(/) : Double -> Double -> Double
 (/) = prim__divFloat
 
 
diff --git a/libs/prelude/Prelude/Either.idr b/libs/prelude/Prelude/Either.idr
--- a/libs/prelude/Prelude/Either.idr
+++ b/libs/prelude/Prelude/Either.idr
@@ -9,11 +9,15 @@
 import Prelude.List
 
 ||| A sum type
-%elim data Either a b =
+%elim data Either : (a, b : Type) -> Type where
   ||| One possibility of the sum, conventionally used to represent errors
-  Left a |
+  Left : (l : a) -> Either a b
   ||| The other possibility, conventionally used to represent success
-  Right b
+  Right : (r : b) -> Either a b
+
+-- Usage hints for erasure analysis
+%used Left l
+%used Right r
 
 --------------------------------------------------------------------------------
 -- Syntactic tests
diff --git a/libs/prelude/Prelude/File.idr b/libs/prelude/Prelude/File.idr
--- a/libs/prelude/Prelude/File.idr
+++ b/libs/prelude/Prelude/File.idr
@@ -18,8 +18,12 @@
 
 ||| A file handle
 abstract
-data File = FHandle Ptr
+data File : Type where
+  FHandle : (p : Ptr) -> File
 
+-- Usage hints for erasure analysis
+%used FHandle p
+
 ||| An error from a file operation
 -- This is built in idris_mkFileError() in rts/idris_stdfgn.c. Make sure
 -- the values correspond!
@@ -88,7 +92,7 @@
 
 ||| Open a file
 ||| @ f the filename
-||| @ m the mode
+||| @ m the mode; either Read, Write, or ReadWrite
 openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
 openFile f m = fopen f (modeStr m) where
   modeStr Read  = "r"
@@ -139,6 +143,13 @@
                           then return (Left FileReadError)
                           else return (Right str)
 
+||| Read a line from a file
+||| @h a file handle which must be open for reading
+fGetLine : (h : File) -> IO (Either FileError String)
+fGetLine = fread
+
+%deprecate fread "Use fGetLine instead"
+
 do_fwrite : Ptr -> String -> IO (Either FileError ())
 do_fwrite h s = do res <- prim_fwrite h s
                    if (res /= 0)
@@ -152,14 +163,31 @@
 fwrite : File -> String -> IO (Either FileError ())
 fwrite (FHandle h) s = do_fwrite h s
 
+||| Write a line to a file
+||| @h a file handle which must be open for writing
+||| @str the line to write to the file
+fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())
+fPutStr (FHandle h) s = do_fwrite h s
+
+fPutStrLn : File -> String -> IO (Either FileError ())
+fPutStrLn (FHandle h) s = do_fwrite h (s ++ "\n")
+
+%deprecate fwrite "Use fPutStr instead"
+
 do_feof : Ptr -> IO Int
 do_feof h = foreign FFI_C "fileEOF" (Ptr -> IO Int) h
 
 ||| Check if a file handle has reached the end
-feof : File -> IO Bool
-feof (FHandle h) = do eof <- do_feof h
+fEOF : File -> IO Bool
+fEOF (FHandle h) = do eof <- do_feof h
                       return (not (eof == 0))
 
+||| Check if a file handle has reached the end
+feof : File -> IO Bool
+feof = fEOF
+
+%deprecate feof "Use fEOF instead"
+
 fpoll : File -> IO Bool
 fpoll (FHandle h) = do p <- foreign FFI_C "fpoll" (Ptr -> IO Int) h
                        return (p > 0)
@@ -177,8 +205,8 @@
     partial
     readFile' : File -> String -> IO (Either FileError String)
     readFile' h contents =
-       do x <- feof h
-          if not x then do Right l <- fread h
+       do x <- fEOF h
+          if not x then do Right l <- fGetLine h
                                | Left err => return (Left err)
                            readFile' h (contents ++ l)
                    else return (Right contents)
@@ -188,6 +216,6 @@
             IO (Either FileError ())
 writeFile fn contents = do
      Right h <- openFile fn Write | Left err => return (Left err)
-     Right () <- fwrite h contents | Left err => return (Left err)
+     Right () <- fPutStr h contents | Left err => return (Left err)
      closeFile h
      return (Right ())
diff --git a/libs/prelude/Prelude/Interactive.idr b/libs/prelude/Prelude/Interactive.idr
--- a/libs/prelude/Prelude/Interactive.idr
+++ b/libs/prelude/Prelude/Interactive.idr
@@ -121,9 +121,9 @@
                 (onEOF : a -> String) -> 
                 IO ()
 processHandle h acc onRead onEOF 
-   = if !(feof h)
+   = if !(fEOF h)
         then putStr (onEOF acc)
-        else do Right x <- fread h
+        else do Right x <- fGetLine h
                     | Left err => putStr (onEOF acc)
                 let (out, acc') = onRead acc x
                 putStr out
diff --git a/libs/prelude/Prelude/List.idr b/libs/prelude/Prelude/List.idr
--- a/libs/prelude/Prelude/List.idr
+++ b/libs/prelude/Prelude/List.idr
@@ -19,15 +19,19 @@
 infixr 7 ::,++
 
 ||| Generic lists
-%elim data List elem =
+%elim data List : (elem : Type) -> Type where
   ||| Empty list
-  Nil |
+  Nil : List elem
   ||| A non-empty list, consisting of a head element and the rest of
   ||| the list.
-  (::) elem (List elem)
+  (::) : (x : elem) -> (xs : List elem) -> List elem
 
 -- Name hints for interactive editing
 %name List xs, ys, zs, ws
+
+-- Usage hints for erasure analysis
+%used List.(::) x
+%used List.(::) xs
 
 --------------------------------------------------------------------------------
 -- Syntactic tests
diff --git a/libs/prelude/Prelude/Maybe.idr b/libs/prelude/Prelude/Maybe.idr
--- a/libs/prelude/Prelude/Maybe.idr
+++ b/libs/prelude/Prelude/Maybe.idr
@@ -13,11 +13,14 @@
 
 ||| An optional value. This can be used to represent the possibility of
 ||| failure, where a function may return a value, or not.
-data Maybe a
-    = ||| No value stored
-      Nothing
-    | ||| A value of type `a` is stored
-      Just a
+data Maybe : (a : Type) -> Type where
+    ||| No value stored
+    Nothing : Maybe a
+    ||| A value of type `a` is stored
+    Just : (x : a) -> Maybe a
+
+-- Used hints for erasure analysis
+%used Just x
 
 --------------------------------------------------------------------------------
 -- Syntactic tests
diff --git a/libs/prelude/Prelude/Nat.idr b/libs/prelude/Prelude/Nat.idr
--- a/libs/prelude/Prelude/Nat.idr
+++ b/libs/prelude/Prelude/Nat.idr
@@ -214,6 +214,9 @@
 instance Cast Integer Nat where
   cast = fromInteger
 
+instance Cast String Nat where
+    cast str = cast (the Integer (cast str))
+
 ||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)
 record Multiplicative where
   constructor GetMultiplicative
diff --git a/libs/prelude/Prelude/Stream.idr b/libs/prelude/Prelude/Stream.idr
--- a/libs/prelude/Prelude/Stream.idr
+++ b/libs/prelude/Prelude/Stream.idr
@@ -14,10 +14,13 @@
 
 ||| An infinite stream
 codata Stream : Type -> Type where
-  (::) : a -> Stream a -> Stream a
+  (::) : (e : a) -> Stream a -> Stream a
 
 -- Hints for interactive editing
 %name Stream xs,ys,zs,ws
+
+-- Usage hints for erasure analysis
+%used Stream.(::) e
 
 instance Functor Stream where
     map f (x::xs) = f x :: map f xs
diff --git a/libs/pruviloj/Pruviloj/Core.idr b/libs/pruviloj/Pruviloj/Core.idr
--- a/libs/pruviloj/Pruviloj/Core.idr
+++ b/libs/pruviloj/Pruviloj/Core.idr
@@ -91,7 +91,7 @@
 |||
 ||| @ tm the term that has the right type for the hole
 exact : (tm : Raw) -> Elab ()
-exact tm = do apply tm []
+exact tm = do fill tm
               solve
 
 ||| Introduce as many names as possible, returning them.
@@ -178,7 +178,7 @@
 total
 inferType : (tac : Elab ()) -> Elab (TT, TT)
 inferType tac =
-    case fst !(runElab `(Infer) (startInfer *> tac)) of
+    case fst !(runElab `(Infer) (do startInfer; tac)) of
         `(MkInfer ~ty ~tm) => return (tm, ty)
         _ => fail [TextPart "Not infer"]
   where
diff --git a/libs/pruviloj/Pruviloj/Derive/DecEq.idr b/libs/pruviloj/Pruviloj/Derive/DecEq.idr
--- a/libs/pruviloj/Pruviloj/Derive/DecEq.idr
+++ b/libs/pruviloj/Pruviloj/Derive/DecEq.idr
@@ -44,9 +44,7 @@
 matchCase : List Raw -> Elab ()
 matchCase []          = search
 matchCase (tm :: tms) =
-    do hs <- induction tm
-       y <- unsafeNth 0 hs
-       n <- unsafeNth 1 hs
+    do (y :: n :: _)  <- induction tm
 
        focus n; compute
        contra <- gensym "contra"
@@ -183,7 +181,7 @@
                     Nothing => return False
 
     partial -- mkRhs
-    mkCase : Nat -> TTName -> (x, y : (TTName, List CtorArg, Raw)) -> Elab (Maybe FunClause)
+    mkCase : Nat -> TTName -> (x, y : (TTName, List CtorArg, Raw)) -> Elab (Maybe (FunClause Raw))
     mkCase k fam (cn1, args1, _) (cn2, args2, _) =
         perhaps $ elabPatternClause
           (do (h2 :: h1 :: _) <- reverse <$>
diff --git a/libs/pruviloj/Pruviloj/Derive/Eliminators.idr b/libs/pruviloj/Pruviloj/Derive/Eliminators.idr
--- a/libs/pruviloj/Pruviloj/Derive/Eliminators.idr
+++ b/libs/pruviloj/Pruviloj/Derive/Eliminators.idr
@@ -134,7 +134,7 @@
   show (NormalArgument x) = "NormalArgument " ++ show x
 
 getElimClause : TyConInfo -> (elimn : TTName) -> (methCount : Nat) ->
-                (TTName, List CtorArg, Raw) -> Nat -> Elab FunClause
+                (TTName, List CtorArg, Raw) -> Nat -> Elab (FunClause Raw)
 getElimClause info elimn methCount (cn, args, resTy) whichCon =
   elabPatternClause
     (do -- Establish a hole for each parameter
@@ -242,14 +242,11 @@
         bindLam ((n, b)::rest) x = RBind n (Lam (getBinderTy b)) $ bindLam rest x
 
 getElimClauses : TyConInfo -> (elimn : TTName) ->
-                 List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
+                 List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
 getElimClauses info elimn ctors =
   let methodCount = length ctors
   in traverse (\(i, con) => getElimClause info elimn methodCount con i)
               (enumerate ctors)
-
-instance Show FunClause where
-  show (MkFunClause x y) = "(MkFunClause " ++ show x ++ " " ++ show y ++ ")"
 
 abstract
 deriveElim : (tyn, elimn : TTName) -> Elab ()
diff --git a/libs/pruviloj/Pruviloj/Internals.idr b/libs/pruviloj/Pruviloj/Internals.idr
--- a/libs/pruviloj/Pruviloj/Internals.idr
+++ b/libs/pruviloj/Pruviloj/Internals.idr
@@ -101,7 +101,7 @@
 |||       It will be run in a context where the pattern variables are
 |||       already bound, and should leave behind no holes.
 partial
-elabPatternClause : (lhs, rhs : Elab ()) -> Elab FunClause
+elabPatternClause : (lhs, rhs : Elab ()) -> Elab (FunClause Raw)
 elabPatternClause lhs rhs =
   do -- Elaborate the LHS in a context where its type will be solved via unification
      (pat, _) <- runElab `(Infer) $
diff --git a/rts/idris_gmp.c b/rts/idris_gmp.c
--- a/rts/idris_gmp.c
+++ b/rts/idris_gmp.c
@@ -196,6 +196,88 @@
     return cl;
 }
 
+VAL bigAnd(VM* vm, VAL x, VAL y) {
+    idris_requireAlloc(IDRIS_MAXGMP);
+
+    mpz_t* bigint;
+    VAL cl = allocate(sizeof(Closure) + sizeof(mpz_t), 0);
+    idris_doneAlloc();
+    bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
+    mpz_and(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));
+    SETTY(cl, BIGINT);
+    cl -> info.ptr = (void*)bigint;
+    return cl;
+}
+
+VAL bigOr(VM* vm, VAL x, VAL y) {
+    idris_requireAlloc(IDRIS_MAXGMP);
+
+    mpz_t* bigint;
+    VAL cl = allocate(sizeof(Closure) + sizeof(mpz_t), 0);
+    idris_doneAlloc();
+    bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
+    mpz_ior(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));
+    SETTY(cl, BIGINT);
+    cl -> info.ptr = (void*)bigint;
+    return cl;
+}
+
+VAL bigShiftLeft(VM* vm, VAL x, VAL y) {
+    idris_requireAlloc(IDRIS_MAXGMP);
+
+    mpz_t* bigint;
+    VAL cl = allocate(sizeof(Closure) + sizeof(mpz_t), 0);
+    idris_doneAlloc();
+    bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
+    mpz_mul_2exp(*bigint, GETMPZ(GETBIG(vm,x)), GETINT(y));
+    SETTY(cl, BIGINT);
+    cl -> info.ptr = (void*)bigint;
+    return cl;
+}
+
+
+VAL bigLShiftRight(VM* vm, VAL x, VAL y) {
+    idris_requireAlloc(IDRIS_MAXGMP);
+
+    mpz_t* bigint;
+    VAL cl = allocate(sizeof(Closure) + sizeof(mpz_t), 0);
+    idris_doneAlloc();
+    bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
+    mpz_fdiv_q_2exp(*bigint, GETMPZ(GETBIG(vm,x)), GETINT(y));
+    SETTY(cl, BIGINT);
+    cl -> info.ptr = (void*)bigint;
+    return cl;
+}
+
+VAL bigAShiftRight(VM* vm, VAL x, VAL y) {
+    idris_requireAlloc(IDRIS_MAXGMP);
+
+    mpz_t* bigint;
+    VAL cl = allocate(sizeof(Closure) + sizeof(mpz_t), 0);
+    idris_doneAlloc();
+    bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
+    mpz_fdiv_q_2exp(*bigint, GETMPZ(GETBIG(vm,x)), GETINT(y));
+    SETTY(cl, BIGINT);
+    cl -> info.ptr = (void*)bigint;
+    return cl;
+}
+
+VAL idris_bigAnd(VM* vm, VAL x, VAL y) {
+    if (ISINT(x) && ISINT(y)) {
+        return INTOP(&, x, y);
+    } else {
+        return bigAnd(vm, GETBIG(vm, x), GETBIG(vm, y));
+    }
+}
+
+VAL idris_bigOr(VM* vm, VAL x, VAL y) {
+    if (ISINT(x) && ISINT(y)) {
+        return INTOP(|, x, y);
+    } else {
+        return bigOr(vm, GETBIG(vm, x), GETBIG(vm, y));
+    }
+}
+
 VAL idris_bigPlus(VM* vm, VAL x, VAL y) {
     if (ISINT(x) && ISINT(y)) {
         i_int vx = GETINT(x);
@@ -250,6 +332,30 @@
         }
     } else {
         return bigMul(vm, GETBIG(vm, x), GETBIG(vm, y));
+    }
+}
+
+VAL idris_bigShiftLeft(VM* vm, VAL x, VAL y) {
+    if (ISINT(x) && ISINT(y)) {
+        return INTOP(<<, x, y);
+    } else {
+        return bigShiftLeft(vm, GETBIG(vm, x), GETBIG(vm, y));
+    }
+}
+
+VAL idris_bigAShiftRight(VM* vm, VAL x, VAL y) {
+    if (ISINT(x) && ISINT(y)) {
+        return INTOP(>>, x, y);
+    } else {
+        return bigAShiftRight(vm, GETBIG(vm, x), GETBIG(vm, y));
+    }
+}
+
+VAL idris_bigLShiftRight(VM* vm, VAL x, VAL y) {
+    if (ISINT(x) && ISINT(y)) {
+        return INTOP(>>, x, y);
+    } else {
+        return bigLShiftRight(vm, GETBIG(vm, x), GETBIG(vm, y));
     }
 }
 
diff --git a/rts/idris_gmp.h b/rts/idris_gmp.h
--- a/rts/idris_gmp.h
+++ b/rts/idris_gmp.h
@@ -38,6 +38,11 @@
 VAL idris_castStrBig(VM* vm, VAL i);
 VAL idris_castBigStr(VM* vm, VAL i);
 
+VAL idris_bigAnd(VM* vm, VAL x, VAL y);
+VAL idris_bigOr(VM* vm, VAL x, VAL y);
+VAL idris_bigShiftLeft(VM* vm, VAL x, VAL y);
+VAL idris_bigShiftRight(VM* vm, VAL x, VAL y);
+
 #define GETMPZ(x) *((mpz_t*)((x)->info.ptr))
 
 #endif
diff --git a/src/IRTS/CodegenC.hs b/src/IRTS/CodegenC.hs
--- a/src/IRTS/CodegenC.hs
+++ b/src/IRTS/CodegenC.hs
@@ -444,6 +444,11 @@
 doOp v (LTimes (ATInt ITBig)) [l, r] = v ++ "idris_bigTimes(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
 doOp v (LSDiv (ATInt ITBig)) [l, r] = v ++ "idris_bigDivide(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
 doOp v (LSRem (ATInt ITBig)) [l, r] = v ++ "idris_bigMod(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LAnd ITBig) [l, r] = v ++ "idris_bigAnd(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LOr ITBig) [l, r] = v ++ "idris_bigOr(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LSHL ITBig) [l, r] = v ++ "idris_bigShiftLeft(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LLSHR ITBig) [l, r] = v ++ "idris_bigLShiftRight(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
+doOp v (LASHR ITBig) [l, r] = v ++ "idris_bigAShiftRight(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
 doOp v (LEq (ATInt ITBig)) [l, r] = v ++ "idris_bigEq(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
 doOp v (LSLt (ATInt ITBig)) [l, r] = v ++ "idris_bigLt(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
 doOp v (LSLe (ATInt ITBig)) [l, r] = v ++ "idris_bigLe(vm, " ++ creg l ++ ", " ++ creg r ++ ")"
diff --git a/src/IRTS/CodegenJavaScript.hs b/src/IRTS/CodegenJavaScript.hs
--- a/src/IRTS/CodegenJavaScript.hs
+++ b/src/IRTS/CodegenJavaScript.hs
@@ -604,7 +604,7 @@
 jsBASETOP _ n = JSAssign jsSTACKBASE (JSBinOp "+" jsSTACKTOP (JSNum (JSInt n)))
 
 jsNULL :: CompileInfo -> Reg -> JS
-jsNULL _ r = JSDelete (translateReg r)
+jsNULL _ r = JSClear (translateReg r)
 
 jsERROR :: CompileInfo -> String -> JS
 jsERROR _ = JSError
@@ -1277,4 +1277,3 @@
 toFType (FApp c [_,fty])
     | c == sUN "JS_FnT" = toFnType fty
 toFType t = error (show t ++ " not yet defined in toFType")
-
diff --git a/src/IRTS/JavaScript/AST.hs b/src/IRTS/JavaScript/AST.hs
--- a/src/IRTS/JavaScript/AST.hs
+++ b/src/IRTS/JavaScript/AST.hs
@@ -77,6 +77,7 @@
         | JSFFI String [JS]
         | JSAnnotation JSAnnotation JS
         | JSDelete JS
+        | JSClear JS
         | JSNoop
         deriving Eq
 
@@ -133,6 +134,9 @@
 compileJS' indent (JSDelete js) =
   "delete " `T.append` compileJS' 0 js
 
+compileJS' indent (JSClear js) =
+   compileJS' 0 js `T.append` " = undefined"
+
 compileJS' indent (JSFFI raw args) =
   ffi raw (map (T.unpack . compileJS' indent) args)
 
@@ -398,4 +402,3 @@
 
 jsPackSBits32 :: JS -> JS
 jsPackSBits32 js = JSNew "Int32Array" [JSArray [js]]
-
diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs
--- a/src/Idris/AbsSyntaxTree.hs
+++ b/src/Idris/AbsSyntaxTree.hs
@@ -188,7 +188,7 @@
     idris_optimisation :: Ctxt OptInfo,
     idris_datatypes :: Ctxt TypeInfo,
     idris_namehints :: Ctxt [Name],
-    idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported
+    idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm]), -- not exported
       -- ^ list of lhs/rhs, and a list of missing clauses
     idris_flags :: Ctxt [FnOpt],
     idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
@@ -717,7 +717,7 @@
 -- | A set of instructions for things that need to happen in IState
 -- after a term elaboration when there's been reflected elaboration.
 data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
-                       | RClausesInstrs Name [([Name], Term, Term)]
+                       | RClausesInstrs Name [([(Name, Term)], Term, Term)]
                        | RAddInstance Name Name
 
 -- | For elaborator state
diff --git a/src/Idris/Coverage.hs b/src/Idris/Coverage.hs
--- a/src/Idris/Coverage.hs
+++ b/src/Idris/Coverage.hs
@@ -351,56 +351,6 @@
     noRec arg = all (\x -> x `notElem` mut_ns) (allTTNames arg)
 
 
-calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> Idris Totality
-calcProd i fc topn pats
-    = cp topn pats []
-   where
-     -- every application of n must be in an argument of a coinductive
-     -- constructor, in every function reachable from here in the
-     -- call graph.
-     cp n pats done = do patsprod <- mapM (prodRec n done) pats
-                         if (and patsprod)
-                            then return Productive
-                            else return (Partial NotProductive)
-
-     prodRec :: Name -> [Name] -> ([Name], Term, Term) -> Idris Bool
-     prodRec n done _ | n `elem` done = return True
-     prodRec n done (_, _, tm) = prod n done False (delazy' True tm)
-
-     prod :: Name -> [Name] -> Bool -> Term -> Idris Bool
-     prod n done ok ap@(App _ _ _)
-        | (P nt f _, args) <- unApply ap
-            = do recOK <- checkProdRec (n:done) f
-                 let ctxt = tt_ctxt i
-                 let [ty] = lookupTy f ctxt -- must exist!
-                 let co = cotype nt f ty in
-                     if (not recOK) then return False else
-                       if f == topn
-                         then do argsprod <- mapM (prod n done co) args
-                                 return (and (ok : argsprod) )
-                         else do argsprod <- mapM (prod n done co) args
-                                 return (and argsprod)
-     prod n done ok (App _ f a) = liftM2 (&&) (prod n done False f)
-                                              (prod n done False a)
-     prod n done ok (Bind _ (Let t v) sc)
-         = liftM2 (&&) (prod n done False v) (prod n done False v)
-     prod n done ok (Bind _ b sc) = prod n done ok sc
-     prod n done ok t = return True
-
-     checkProdRec :: [Name] -> Name -> Idris Bool
-     checkProdRec done f
-        = case lookupCtxt f (idris_patdefs i) of
-               [(def, _)] -> do ok <- mapM (prodRec f done) def
-                                return (and ok)
-               _ -> return True -- defined elsewhere, can't call topn
-
-     cotype (DCon _ _ _) n ty
-        | (P _ t _, _) <- unApply (getRetTy ty)
-            = case lookupCtxt t (idris_datatypes i) of
-                   [TI _ True _ _ _] -> True
-                   _ -> False
-     cotype nt n ty = False
-
 -- | Calculate the totality of a function from its patterns.
 -- Either follow the size change graph (if inductive) or check for
 -- productivity (if coinductive)
diff --git a/src/Idris/DSL.hs b/src/Idris/DSL.hs
--- a/src/Idris/DSL.hs
+++ b/src/Idris/DSL.hs
@@ -98,8 +98,8 @@
     block b (DoBind fc n nfc tm : rest)
         = PApp fc b [pexp tm, pexp (PLam fc n nfc Placeholder (block b rest))]
     block b (DoBindP fc p tm alts : rest)
-        = PApp fc b [pexp tm, pexp (PLam fc (sMN 0 "bpat") NoFC Placeholder
-                                   (PCase fc (PRef fc [] (sMN 0 "bpat"))
+        = PApp fc b [pexp tm, pexp (PLam fc (sMN 0 "__bpat") NoFC Placeholder
+                                   (PCase fc (PRef fc [] (sMN 0 "__bpat"))
                                              ((p, block b rest) : alts)))]
     block b (DoLet fc n nfc ty tm : rest)
         = PLet fc n nfc ty tm (block b rest)
@@ -108,7 +108,7 @@
     block b (DoExp fc tm : rest)
         = PApp fc b
             [pexp tm,
-             pexp (PLam fc (sMN 0 "bindx") NoFC (mkTy tm) (block b rest))]
+             pexp (PLam fc (sMN 0 "__bindx") NoFC (mkTy tm) (block b rest))]
         where mkTy (PCase _ _ _) = PRef fc [] unitTy
               mkTy (PMetavar _ _) = PRef fc [] unitTy
               mkTy _ = Placeholder
diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs
--- a/src/Idris/Delaborate.hs
+++ b/src/Idris/Delaborate.hs
@@ -204,8 +204,8 @@
                     [(cases, _)] -> return cases
                     _ -> Nothing
          return $ PCase un (de env imps scrutinee)
-                    [ (de (env ++ map (\n -> (n, n)) vars) imps (splitArg lhs),
-                       de (env ++ map (\n -> (n, n)) vars) imps rhs)
+                    [ (de (env ++ map (\(n, _) -> (n, n)) vars) imps (splitArg lhs),
+                       de (env ++ map (\(n, _) -> (n, n)) vars) imps rhs)
                     | (vars, lhs, rhs) <- cases
                     ]
       where splitArg tm | (_, args) <- unApply tm = nonVar (reverse args)
diff --git a/src/Idris/Elab/Clause.hs b/src/Idris/Elab/Clause.hs
--- a/src/Idris/Elab/Clause.hs
+++ b/src/Idris/Elab/Clause.hs
@@ -133,7 +133,7 @@
 
            -- pdef is the compile-time pattern definition.
            -- This will get further inlined to help with totality checking.
-           let pdef = map debind pats_raw
+           let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $ map debind pats_raw
            -- pdef_pe is the one which will get further optimised 
            -- for run-time, and, partially evaluated
            let pdef_pe = map debind pats_transformed
@@ -182,7 +182,7 @@
 
            -- pdef' is the version that gets compiled for run-time,
            -- so we start from the partially evaluated version
-           pdef_in' <- applyOpts pdef_pe
+           pdef_in' <- applyOpts $ map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) pdef_pe
            let pdef' = map (simple_rt (tt_ctxt ist)) pdef_in'
 
            logLvl 5 $ "After data structure transformations:\n" ++ show pdef'
@@ -289,7 +289,7 @@
     debind (Left x)       = let (vs, x') = depat [] x in
                                 (vs, x', Impossible)
 
-    depat acc (Bind n (PVar t) sc) = depat (n : acc) (instantiate (P Bound n t) sc)
+    depat acc (Bind n (PVar t) sc) = depat ((n, t) : acc) (instantiate (P Bound n t) sc)
     depat acc x = (acc, x)
 
 
diff --git a/src/Idris/Elab/Term.hs b/src/Idris/Elab/Term.hs
--- a/src/Idris/Elab/Term.hs
+++ b/src/Idris/Elab/Term.hs
@@ -1775,14 +1775,33 @@
 
     returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased)
 
-    patvars :: [Name] -> Term -> ([Name], Term)
-    patvars ns (Bind n (PVar t) sc) = patvars (n : ns) (instantiate (P Bound n t) sc)
+    patvars :: [(Name, Term)] -> Term -> ([(Name, Term)], Term)
+    patvars ns (Bind n (PVar t) sc) = patvars ((n, t) : ns) (instantiate (P Bound n t) sc)
     patvars ns tm                   = (ns, tm)
 
-    pullVars :: (Term, Term) -> ([Name], Term, Term)
+    pullVars :: (Term, Term) -> ([(Name, Term)], Term, Term)
     pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs
 
-    defineFunction :: RFunDefn -> ElabD ()
+    requireError :: Err -> ElabD a -> ElabD ()
+    requireError orErr elab =
+      do state <- get
+         case runStateT elab state of
+           OK (_, state') -> lift (tfail orErr)
+           Error e -> return ()
+
+    -- create a fake TT term for the LHS of an impossible case
+    fakeTT :: Raw -> Term
+    fakeTT (Var n) =
+      case lookupNameDef n (tt_ctxt ist) of
+        [(n', TyDecl nt _)] -> P nt n' Erased
+        _ -> P Ref n Erased
+    fakeTT (RBind n b body) = Bind n (fmap fakeTT b) (fakeTT body)
+    fakeTT (RApp f a) = App Complete (fakeTT f) (fakeTT a)
+    fakeTT RType = TType (UVar (-1))
+    fakeTT (RUType u) = UType u
+    fakeTT (RConstant c) = Constant c
+
+    defineFunction :: RFunDefn Raw -> ElabD ()
     defineFunction (RDefineFun n clauses) =
       do ctxt <- get_context
          ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt
@@ -1794,22 +1813,24 @@
                                            lift $ converts ctxt [] lty rty
                                            return $ Right (lhs', rhs')
                                       RMkImpossibleClause lhs ->
-                                        do lhs' <- fmap fst . lift $ check ctxt [] lhs
-                                           return $ Left lhs')
+                                        do requireError (Msg "Not an impossible case") . lift $
+                                             check ctxt [] lhs
+                                           return $ Left (fakeTT lhs))
          let clauses'' = map (\case Right c -> pullVars c
-                                    Left lhs -> let (ns, lhs') = patvars [] lhs'
+                                    Left lhs -> let (ns, lhs') = patvars [] lhs
                                                 in (ns, lhs', Impossible))
                             clauses'
+         let clauses''' = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses''
          ctxt'<- lift $
                   addCasedef n (const [])
                              info False (STerm Erased)
                              True False -- TODO what are these?
                              (map snd $ getArgTys ty) [] -- TODO inaccessible types
                              clauses'
-                             clauses''
-                             clauses''
-                             clauses''
-                             clauses''
+                             clauses'''
+                             clauses'''
+                             clauses'''
+                             clauses'''
                              ty
                              ctxt
          set_context ctxt'
@@ -1874,6 +1895,11 @@
            fmap fst . checkClosed $
              rawList (Var (tacN "Datatype"))
                      (map reflectDatatype (buildDatatypes ist n'))
+      | n == tacN "Prim__LookupFunDefn", [name] <- args
+      = do n' <- reifyTTName name
+           fmap fst . checkClosed $
+             rawList (RApp (Var $ tacN "FunDefn") (Var $ reflm "TT"))
+               (map reflectFunDefn (buildFunDefns ist n'))
       | n == tacN "Prim__LookupArgs", [name] <- args
       = do n' <- reifyTTName name
            let listTy = Var (sNS (sUN "List") ["List", "Prelude"])
diff --git a/src/Idris/Erasure.hs b/src/Idris/Erasure.hs
--- a/src/Idris/Erasure.hs
+++ b/src/Idris/Erasure.hs
@@ -414,7 +414,7 @@
             V i -> snd (bs !! i) cd `union` unconditionalDeps args
 
             -- we interpret applied lambdas as lets in order to reuse code here
-            Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)
+            Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet app)
 
             -- and we interpret applied lets as lambdas
             Bind n ( Let ty t') t -> getDepsTerm vs bs cd (App Complete (Bind n (Lam ty) t) t')
@@ -491,11 +491,8 @@
 
     -- convert applications of lambdas to lets
     -- Note that this transformation preserves de bruijn numbering
-    lamToLet :: [Term] -> Term -> Term
-    lamToLet    xs  (App _ f x)         = lamToLet (x:xs) f
-    lamToLet (x:xs) (Bind n (Lam ty) t) = Bind n (Let ty x) (lamToLet xs t)
-    lamToLet (x:xs)  t                  = App Complete (lamToLet xs t) x
-    lamToLet    []   t                  = t
+    lamToLet :: Term -> Term
+    lamToLet (App _ (Bind n (Lam ty) tm) val) = Bind n (Let ty val) tm
 
     -- split "\x_i -> T(x_i)" into [x_i] and T
     unfoldLams :: Term -> ([Name], Term)
diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs
--- a/src/Idris/IBC.hs
+++ b/src/Idris/IBC.hs
@@ -40,7 +40,7 @@
 import Codec.Archive.Zip
 
 ibcVersion :: Word16
-ibcVersion = 127
+ibcVersion = 128
 
 data IBCFile = IBCFile { ver :: Word16,
                          sourcefile :: FilePath,
@@ -80,7 +80,7 @@
                          ibc_errorhandlers :: ![Name],
                          ibc_function_errorhandlers :: ![(Name, Name, Name)], -- fn, arg, handler
                          ibc_metavars :: ![(Name, (Maybe Name, Int, [Name], Bool))],
-                         ibc_patdefs :: ![(Name, ([([Name], Term, Term)], [PTerm]))],
+                         ibc_patdefs :: ![(Name, ([([(Name, Term)], Term, Term)], [PTerm]))],
                          ibc_postulates :: ![Name],
                          ibc_externs :: ![(Name, Int)],
                          ibc_parsedSpan :: !(Maybe FC),
@@ -505,7 +505,7 @@
 pHdrs :: [(Codegen, String)] -> Idris ()
 pHdrs hs = mapM_ (uncurry addHdr) hs
 
-pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()
+pPatdefs :: [(Name, ([([(Name, Term)], Term, Term)], [PTerm]))] -> Idris ()
 pPatdefs ds = mapM_ (\ (n, d) -> updateIState (\i ->
             i { idris_patdefs = addDef n (force d) (idris_patdefs i) })) ds
 
diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs
--- a/src/Idris/REPL.hs
+++ b/src/Idris/REPL.hs
@@ -1450,11 +1450,11 @@
      return $ map (ppDef ambiguous ist) (lookupCtxtName n patdefs) ++
               map (ppTy ambiguous ist) (lookupCtxtName n tyinfo) ++
               map (ppCon ambiguous ist) (filter (flip isDConName ctxt) (lookupNames n ctxt))
-  where ppDef :: Bool -> IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation
+  where ppDef :: Bool -> IState -> (Name, ([([(Name, Term)], Term, Term)], [PTerm])) -> Doc OutputAnnotation
         ppDef amb ist (n, (clauses, missing)) =
           prettyName True amb [] n <+> colon <+>
           align (pprintDelabTy ist n) <$>
-          ppClauses ist clauses <> ppMissing missing
+          ppClauses ist (map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses) <> ppMissing missing
         ppClauses ist [] = text "No clauses."
         ppClauses ist cs = vsep (map pp cs)
           where pp (vars, lhs, rhs) =
diff --git a/src/Idris/Reflection.hs b/src/Idris/Reflection.hs
--- a/src/Idris/Reflection.hs
+++ b/src/Idris/Reflection.hs
@@ -7,6 +7,8 @@
 
 #if __GLASGOW_HASKELL__ < 710
 import Control.Applicative ((<$>), (<*>), pure)
+import Prelude hiding (mapM)
+import Data.Traversable (mapM)
 #endif
 import Control.Monad (liftM, liftM2, liftM4)
 import Control.Monad.State.Strict (lift)
@@ -19,7 +21,7 @@
 import Idris.Core.Evaluate (Def(TyDecl), initContext, lookupDefExact, lookupTyExact)
 import Idris.Core.TT
 
-import Idris.AbsSyntaxTree (ArgOpt(..),ElabD, IState(tt_ctxt, idris_implicits,idris_datatypes),
+import Idris.AbsSyntaxTree (ArgOpt(..),ElabD, IState(tt_ctxt, idris_implicits,idris_datatypes, idris_patdefs),
                             PArg'(..), PArg, PTactic, PTactic'(..), PTerm(..), Fixity (..),
                             initEState, pairCon, pairTy)
 import Idris.Delaborate (delab)
@@ -55,11 +57,11 @@
 rFunArgToPArg (RFunArg n _ RImplicit e) = PImp 0 False (rArgOpts e) n Placeholder
 rFunArgToPArg (RFunArg n _ RConstraint e) = PConstraint 0 (rArgOpts e) n Placeholder
 
-data RFunClause = RMkFunClause Raw Raw
-                | RMkImpossibleClause Raw
-                deriving Show
+data RFunClause a = RMkFunClause a a
+                  | RMkImpossibleClause a
+                  deriving Show
 
-data RFunDefn = RDefineFun Name [RFunClause] deriving Show
+data RFunDefn a = RDefineFun Name [RFunClause a] deriving Show
 
 -- | Prefix a name with the "Language.Reflection" namespace
 reflm :: String -> Name
@@ -357,8 +359,8 @@
 reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
 
 reifyArithTy :: Term -> ElabD ArithTy
-reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt"   = fmap ATInt (reifyIntTy intTy)
-reifyArithTy (P _ n _)             | n == reflm "ATFloat" = return ATFloat
+reifyArithTy (App _ (P _ n _) intTy) | n == reflm "ATInt"    = fmap ATInt (reifyIntTy intTy)
+reifyArithTy (P _ n _)               | n == reflm "ATDouble" = return ATFloat
 reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)
 
 reifyNativeTy :: Term -> ElabD NativeTy
@@ -768,7 +770,7 @@
 reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
 reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]
 reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]
-reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]
+reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATDouble")]
 reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]
 reflectConstant StrType = Var (reflm "StrType")
 reflectConstant (AType (ATInt (ITFixed IT8)))  = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]
@@ -1023,21 +1025,21 @@
      return $ RDeclare tyN' args' ret'
 reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."
 
-reifyFunDefn :: Term -> ElabD RFunDefn
-reifyFunDefn (App _ (App _ (P _ n _) fnN) clauses)
-  | n == tacN "DefineFun" =
+reifyFunDefn :: Term -> ElabD (RFunDefn Raw)
+reifyFunDefn (App _ (App _ (App _ (P _ n _) (P _ t _)) fnN) clauses)
+  | n == tacN "DefineFun" && t == reflm "Raw" =
   do fnN' <- reifyTTName fnN
      clauses' <- case unList clauses of
                    Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"
                    Just cs -> mapM reifyC cs
      return $ RDefineFun fnN' clauses'
-  where reifyC :: Term -> ElabD RFunClause
-        reifyC (App _ (App _ (P (DCon _ _ _) n _) lhs) rhs)
-          | n == tacN "MkFunClause" = liftM2 RMkFunClause
+  where reifyC :: Term -> ElabD (RFunClause Raw)
+        reifyC (App _ (App _ (App _ (P (DCon _ _ _) n _) (P _ t _)) lhs) rhs)
+          | n == tacN "MkFunClause" && t == reflm "Raw" = liftM2 RMkFunClause
                                              (reifyRaw lhs)
                                              (reifyRaw rhs)
-        reifyC (App _ (P (DCon _ _ _) n _) lhs)
-          | n == tacN "MkImpossibleClause" = fmap RMkImpossibleClause $ reifyRaw lhs
+        reifyC (App _ (App _ (P (DCon _ _ _) n _) (P _ t _)) lhs)
+          | n == tacN "MkImpossibleClause" && t == reflm "Raw" = fmap RMkImpossibleClause $ reifyRaw lhs
         reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."
 reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."
 
@@ -1074,6 +1076,22 @@
     ua args (RApp f a) = ua (a:args) f
     ua args t         = (t, args)
 
+-- | Build the reflected function definition(s) that correspond(s) to
+-- a provided unqualifed name
+buildFunDefns :: IState -> Name -> [RFunDefn Term]
+buildFunDefns ist n =
+  [ mkFunDefn name clauses
+  | (name, (clauses, _)) <- lookupCtxtName n $ idris_patdefs ist
+  ]
+
+  where mkFunDefn name clauses = RDefineFun name (map mkFunClause clauses)
+
+        mkFunClause ([], lhs, Impossible) = RMkImpossibleClause lhs
+        mkFunClause ([], lhs, rhs) = RMkFunClause lhs rhs
+        mkFunClause (((n, ty) : ns), lhs, rhs) = mkFunClause (ns, bind lhs, bind rhs) where
+          bind Impossible = Impossible
+          bind tm = Bind n (PVar ty) tm
+
 -- | Build the reflected datatype definition(s) that correspond(s) to
 -- a provided unqualified name
 buildDatatypes :: IState -> Name -> [RDatatype]
@@ -1163,3 +1181,13 @@
           RApp (Var $ tacN "TyConParameter") (reflectArg a)
         reflectConArg (RIndex a) =
           RApp (Var $ tacN "TyConIndex") (reflectArg a)
+
+reflectFunClause :: RFunClause Term -> Raw
+reflectFunClause (RMkFunClause lhs rhs) = raw_apply (Var $ tacN "MkFunClause") $ (Var $ reflm "TT") : map reflect [ lhs, rhs ]
+reflectFunClause (RMkImpossibleClause lhs) = raw_apply (Var $ tacN "MkImpossibleClause") $ [ Var $ reflm "TT", reflect lhs ]
+
+reflectFunDefn :: RFunDefn Term -> Raw
+reflectFunDefn (RDefineFun name clauses) = raw_apply (Var $ tacN "DefineFun") [ Var $ reflm "TT"
+                                                                              , reflectName name
+                                                                              , rawList (RApp (Var $ tacN "FunClause") (Var $ reflm "TT")) (map reflectFunClause clauses)
+                                                                              ]
diff --git a/src/Util/System.hs b/src/Util/System.hs
--- a/src/Util/System.hs
+++ b/src/Util/System.hs
@@ -16,9 +16,8 @@
                         , removeFile
                         , removeDirectoryRecursive
                         , createDirectoryIfMissing
-                        , doesDirectoryExist
                         )
-import System.FilePath ((</>), normalise, isAbsolute, dropFileName)
+import System.FilePath ((</>), normalise)
 import System.IO
 import System.Info
 import System.IO.Error
@@ -66,7 +65,7 @@
 withTempdir :: String -> (FilePath -> IO a) -> IO a
 withTempdir subdir callback
   = do dir <- getTemporaryDirectory
-       let tmpDir = (normalise dir) </> subdir
+       let tmpDir = normalise dir </> subdir
        removeLater <- catchIO (createDirectoryIfMissing True tmpDir >> return True)
                               (\ ioError -> if isAlreadyExistsError ioError then return False
                                             else throw ioError
@@ -76,10 +75,15 @@
        return result
 
 rmFile :: FilePath -> IO ()
-rmFile f = do putStrLn $ "Removing " ++ f
-              catchIO (removeFile f)
-                      (\ioerr -> putStrLn $ "WARNING: Cannot remove file "
-                                 ++ f ++ ", Error msg:" ++ show ioerr)
+rmFile f = do
+  result <- try (removeFile f)
+  case result of
+    Right _ -> putStrLn $ "Removed: " ++ f
+    Left err -> handleExists err
+     where handleExists e
+            | isDoesNotExistError e = return ()
+            | otherwise = putStrLn $ "WARNING: Cannot remove file "
+                          ++ f ++ ", Error msg:" ++ show e
 
 setupBundledCC :: IO()
 #ifdef FREESTANDING
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,6 +1,13 @@
-flags: {}
+resolver: lts-3.16
 packages:
 - '.'
+flags:
+  # idris:
+  #   FFI: true
+  #   GMP: True
+  #   curses: True
 extra-deps: 
+- annotated-wl-pprint-0.7.0
 - cheapskate-0.1.0.4
-resolver: nightly-2015-07-24
+# - hscurses-1.4.2.0
+# - libffi-0.1
diff --git a/test/dsl002/test014.idr b/test/dsl002/test014.idr
--- a/test/dsl002/test014.idr
+++ b/test/dsl002/test014.idr
@@ -23,12 +23,12 @@
 close (OpenH h) = iou (closeFile h)
 
 readLine : FILE Reading -> Reader String
-readLine (OpenH h) = ior (do Right str <- fread h
+readLine (OpenH h) = ior (do Right str <- fGetLine h
                                    | return ""
                              return str)
 
 eof : FILE Reading -> Reader Bool
-eof (OpenH h) = ior (feof h)
+eof (OpenH h) = ior (fEOF h)
 
 syntax rclose [h]    = Update close h
 syntax rreadLine [h] = Use readLine h
diff --git a/test/ffi001/test022.idr b/test/ffi001/test022.idr
--- a/test/ffi001/test022.idr
+++ b/test/ffi001/test022.idr
@@ -2,8 +2,8 @@
 
 %dynamic "dummy", "libm", "msvcrt"
 
-x : Float
-x = unsafePerformIO (foreign FFI_C "sin" (Float -> IO Float) 1.6)
+x : Double
+x = unsafePerformIO (foreign FFI_C "sin" (Double -> IO Double) 1.6)
 
 main : IO ()
 main = putStrLn (show x)
diff --git a/test/interactive010/expected b/test/interactive010/expected
--- a/test/interactive010/expected
+++ b/test/interactive010/expected
@@ -1,14 +1,14 @@
 Prelude.List.(++) : List a -> List a -> List a
 Prelude.Strings.(++) : String -> String -> String
-Prelude.Classes./ : (__pi_arg : Float) →
-                    (__pi_arg1 : Float) → Float
+Prelude.Classes./ : (__pi_arg : Double) →
+                    (__pi_arg1 : Double) → Double
 Usage is :doc <functionname>
 Usage is :wc <functionname>
 Usage is :printdef <functionname>
 prim__divFloat
 Prelude.Classes./
 
- : Float -> Float -> Float
+ : Double -> Double -> Double
 (input):1:1: error: expected: ":",
     dependent type signature,
     end of input
diff --git a/test/interactive012/run b/test/interactive012/run
--- a/test/interactive012/run
+++ b/test/interactive012/run
@@ -1,3 +1,3 @@
 #!/usr/bin/env bash
-idris --quiet interactive012.idr < input
+idris --nocolour --consolewidth 70 --quiet interactive012.idr < input
 rm -f *.ibc
diff --git a/test/io001/test004.idr b/test/io001/test004.idr
--- a/test/io001/test004.idr
+++ b/test/io001/test004.idr
@@ -10,15 +10,15 @@
 dumpFile : String -> IO ()
 dumpFile fn = do { Right h <- openFile fn Read
                    mwhile (do { -- putStrLn "TEST"
-                                x <- feof h
+                                x <- fEOF h
                                 return (not x) })
-                          (do { Right l <- fread h
+                          (do { Right l <- fGetLine h
                                 putStr l })
                    closeFile h }
 
 main : IO ()
 main = do { Right h <- openFile "testfile" Write
-            fwrite h "Hello!\nWorld!\n...\n3\n4\nLast line\n"
+            fPutStr h "Hello!\nWorld!\n...\n3\n4\nLast line\n"
             closeFile h
             putStrLn "Reading testfile"
             Right f <- readFile "testfile"
diff --git a/test/meta001/Finite.idr b/test/meta001/Finite.idr
--- a/test/meta001/Finite.idr
+++ b/test/meta001/Finite.idr
@@ -29,7 +29,7 @@
 
 mkToClause : TTName -> (size, i : Nat) ->
              (constr : (TTName, List CtorArg, Raw)) ->
-             Elab FunClause
+             Elab (FunClause Raw)
 mkToClause fn size i (n, [], Var ty) =
   MkFunClause (RApp (Var fn) (Var n)) <$> mkFin size i
 mkToClause fn size i (n, _, ty) =
@@ -38,14 +38,14 @@
 
 mkFromClause : TTName -> (size, i : Nat) ->
                (constr : (TTName, List CtorArg, Raw)) ->
-               Elab FunClause
+               Elab (FunClause Raw)
 mkFromClause fn size i (n, [], Var ty) =
   return $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n)
 mkFromClause fn size i (n, _, ty) =
   fail [TextPart "unsupported constructor", NamePart n]
 
 
-mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab FunClause
+mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab (FunClause Raw)
 mkOk1Clause fn size i (n, [], Var ty) =
   return $ MkFunClause (RApp (Var fn) (Var n))
                        [| (Var (UN "Refl")) (Var ty) (Var n) |]
@@ -53,7 +53,7 @@
   fail [TextPart "unsupported constructor", NamePart n]
 
 
-mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab FunClause
+mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab (FunClause Raw)
 mkOk2Clause fn size i (n, [], Var ty) =
   return $ MkFunClause (RApp (Var fn) !(mkFin size i))
                        [| (Var "Refl") `(Fin ~(quote size))
@@ -62,9 +62,9 @@
   fail [TextPart "unsupported constructor", NamePart n]
 
 
-mkToClauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
+mkToClauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
 mkToClauses fn size xs = mkToClauses' Z xs
-  where mkToClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
+  where mkToClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
         mkToClauses' k []        = return []
         mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs
                                       clause <- mkToClause fn size k x
@@ -76,7 +76,7 @@
 ||| This is to satisfy the totality checker, because `impossible`
 ||| clauses are still
 mkAbsurdFinClause : (fn : TTName) -> (goal : Raw -> Raw) -> (size : Nat) ->
-                    Elab FunClause
+                    Elab (FunClause Raw)
 mkAbsurdFinClause fn goal size =
   do pv <- gensym "badfin"
      lhsArg <- lhsBody pv size
@@ -92,26 +92,26 @@
 
 
 mkFromClauses : TTName -> TTName -> Nat ->
-                List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
+                List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
 mkFromClauses fn ty size xs = mkFromClauses' Z xs
-  where mkFromClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
+  where mkFromClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
         mkFromClauses' k []        =
              return [!(mkAbsurdFinClause fn (const (Var ty)) size)]
         mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs
                                         clause <- mkFromClause fn size k x
                                         return $ clause :: rest
 
-mkOk1Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
+mkOk1Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
 mkOk1Clauses fn size xs = mkOk1Clauses' Z xs
-  where mkOk1Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
+  where mkOk1Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
         mkOk1Clauses' k []        = return []
         mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs
                                        clause <- mkOk1Clause fn size k x
                                        return $ clause :: rest
 
-mkOk2Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> (Raw -> Raw) -> Elab (List FunClause)
+mkOk2Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> (Raw -> Raw) -> Elab (List (FunClause Raw))
 mkOk2Clauses fn size xs resTy = mkOk2Clauses' Z xs
-  where mkOk2Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
+  where mkOk2Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))
         mkOk2Clauses' k []        = return [!(mkAbsurdFinClause fn resTy size)]
         mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs
                                        clause <- mkOk2Clause fn size k x
diff --git a/test/meta002/Deriving.idr b/test/meta002/Deriving.idr
--- a/test/meta002/Deriving.idr
+++ b/test/meta002/Deriving.idr
@@ -1,6 +1,8 @@
 ||| Test some deriving features
 module Deriving
 
+-- NB: test disabled due to excess memory consumption
+
 import Pruviloj
 import Pruviloj.Derive.DecEq
 
diff --git a/test/meta002/run b/test/meta002/run
--- a/test/meta002/run
+++ b/test/meta002/run
@@ -1,5 +1,6 @@
 #!/usr/bin/env bash
 idris $@ -p pruviloj --nocolour --check --consolewidth 70 Tacs.idr
 idris $@ -p pruviloj --nocolour --check --consolewidth 70 AgdaStyleReflection.idr
-idris $@ -p pruviloj --nocolour --check --consolewidth 70 Deriving.idr
+# Disabled due to excess memory consumption
+# idris $@ -p pruviloj --nocolour --check --consolewidth 70 Deriving.idr
 rm -f *.ibc
diff --git a/test/meta004/expected b/test/meta004/expected
new file mode 100644
--- /dev/null
+++ b/test/meta004/expected
@@ -0,0 +1,3 @@
+meta004.idr:48:1-9:
+While running an elaboration script, the following error occurred:
+Not an impossible case
diff --git a/test/meta004/meta004.idr b/test/meta004/meta004.idr
new file mode 100644
--- /dev/null
+++ b/test/meta004/meta004.idr
@@ -0,0 +1,48 @@
+import Data.Fin
+import Language.Reflection.Utils
+import Pruviloj.Core
+
+rename : TTName -> TTName -> Raw -> Raw
+rename old new (RBind name b body) = RBind name (map (rename old new) b) (rename old new body)
+rename old new (RApp f arg) = RApp (rename old new f) (rename old new arg)
+rename old new (Var n) = if n == old then Var new else Var n
+rename old new tm = tm
+
+roundtrip : TTName -> TTName -> Elab ()
+roundtrip old new = do
+  DefineFun _ clauses <- lookupFunDefnExact old
+  clauses' <- for clauses (\(MkFunClause lhs rhs) => do
+    lhs' <- rename old new <$> forget lhs
+    rhs' <- rename old new <$> forget rhs
+    pure $ MkFunClause lhs' rhs')
+  defineFunction (DefineFun new clauses')
+
+plus' : Nat -> Nat -> Nat
+%runElab (roundtrip `{plus} `{plus'})
+
+total
+p : (a : Nat) -> (b : Nat) -> plus a b = plus' a b
+p Z right = Refl
+p (S left) right = Refl
+
+
+-- Test handling of impossible clauses in function definitions
+foo : Fin Z -> Nat
+bar : Nat -> Fin Z
+
+doit : Elab ()
+doit = defineFunction $
+          DefineFun `{foo} [MkImpossibleClause
+                             (RBind `{{n}}
+                               (PVar (Var `{Nat}))
+                               (RApp (Var `{foo})
+                                 (RApp (Var `{FZ}) (Var `{{n}}))))]
+
+domore : Elab ()
+domore = defineFunction $
+            DefineFun `{foo} [MkImpossibleClause $
+                                RBind `{{k}} (PVar `(Nat)) $
+                                  RApp (Var `{bar}) (Var `{{k}})]
+
+%runElab doit
+%runElab domore
diff --git a/test/meta004/run b/test/meta004/run
new file mode 100644
--- /dev/null
+++ b/test/meta004/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+idris $@ -p pruviloj --nocolour --check --consolewidth 70 meta004.idr
+rm -f *.ibc
diff --git a/test/proofsearch002/proofsearch002.idr b/test/proofsearch002/proofsearch002.idr
--- a/test/proofsearch002/proofsearch002.idr
+++ b/test/proofsearch002/proofsearch002.idr
@@ -24,9 +24,6 @@
                                                         Pure (fact k, ()))
                  Loop mathsServer
 
-instance Cast String Nat where
-    cast orig = cast (the Integer (cast orig))
-
 -- Start up a couple of servers, send them requests
 testProg1 : Program () (const Void)
 testProg1 = do -- with Process do 
diff --git a/test/quasiquote001/expected b/test/quasiquote001/expected
--- a/test/quasiquote001/expected
+++ b/test/quasiquote001/expected
@@ -1,5 +1,5 @@
-App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar (-1)))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar (-1)))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))))
+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))) (P (DCon 0 0) (UN "MkUnit") (P (TCon 0 0) (UN "Unit") Erased))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN "Unit") (TType (UVar (-1))))))
 --------------
-App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar (-1)))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (MN 0 "_t") (Pi (V 0) (TType (UVar (-1)))) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1))))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1)))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27))))
+App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 24))) (TType (UVar 25))) (App (App (App (P (DCon 1 3) (NS (UN "::") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "x") (Pi (V 0) (TType (UVar (-1)))) (Bind (UN "xs") (Pi (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 1)) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 26))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1))))) (P (TCon 8 0) (NS (UN "Nat") ["Nat", "Prelude"]) (TType (UVar (-1)))))) (App (P (DCon 0 1) (NS (UN "Nil") ["List", "Prelude"]) (Bind (UN "elem") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (App (P (TCon 0 0) (NS (UN "List") ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 27))))
 --------------
 App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))) (App (App (App (App (P (DCon 0 4) (NS (UN "MkPair") ["Builtins"]) (Bind (UN "A") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "B") (Pi (TType (UVar (-1))) (TType (UVar (-1)))) (Bind (UN "a") (Pi (V 1) (TType (UVar (-1)))) (Bind (UN "b") (Pi (V 1) (TType (UVar (-1)))) (App (App (P (TCon 0 0) (NS (UN "Pair") ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 22))) (TType (UVar 23))) (TType (UVar 24))) (TType (UVar 24)))
diff --git a/test/reg067/expected b/test/reg067/expected
new file mode 100644
--- /dev/null
+++ b/test/reg067/expected
@@ -0,0 +1,1 @@
+tst2["as"]
diff --git a/test/reg067/reg067.idr b/test/reg067/reg067.idr
new file mode 100644
--- /dev/null
+++ b/test/reg067/reg067.idr
@@ -0,0 +1,23 @@
+module Main
+
+-- https://github.com/idris-lang/Idris-dev/issues/2844
+main_2844 : IO ()
+main_2844 =
+  let
+    f =
+      the
+        ((String,String) -> String -> (String, Maybe String ))
+        (\(_,s),y => (s, Just s))
+  in
+    case snd $ f ("tst","tst2") "cenas" of
+      Just z => putStr z
+
+-- https://github.com/idris-lang/Idris-dev/issues/2493
+main_2493 : IO ()
+main_2493 = printLn $ doThing [1,2,3] [("as",1),("asasasas",4)]
+  where
+    doThing : List Nat -> List (v,Nat) -> List v
+    doThing is g = foldr (\(v,i),res => if elem i is then v::res else res) List.Nil g
+
+main : IO ()
+main = main_2844 *> main_2493
diff --git a/test/reg067/run b/test/reg067/run
new file mode 100644
--- /dev/null
+++ b/test/reg067/run
@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+rm -f *.ibc reg067
+idris $@ reg067.idr -o reg067 --warnreach
+./reg067
+rm -f *.ibc reg067
diff --git a/test/runtest.pl b/test/runtest.pl
--- a/test/runtest.pl
+++ b/test/runtest.pl
@@ -8,18 +8,46 @@
 my $exitstatus = 0;
 my @idrOpts    = ();
 
+
+# Determines how idris was built locally, returning a PATH modifier.
+#
+# Order of checking is:
+#
+#  1. Cabal Sandboxing
+#  2. Stack
+#  3. Pure cabal.
+#
 sub sandbox_path {
     my ($test_dir,) = @_;
     my $sandbox = "$test_dir/../../.cabal-sandbox/bin";
 
+    my $stack_bin_path = `stack path --dist-dir`;
+    $stack_bin_path =~ s/\n//g;
+    my $stack_work_dir = "$test_dir/../../$stack_bin_path/build/idris";
+
     if ( -d $sandbox ) {
+
         my $sandbox_abs = abs_path($sandbox);
+        print "Using Cabal Sandbox\n";
+        printf("Sandbox located at: %s\n", $sandbox_abs);
         return "PATH=\"$sandbox_abs:$PATH\"";
+
+    } elsif ( -d $stack_work_dir ) {
+
+        my $stack_work_abs = abs_path($stack_work_dir);
+        print "Using Stack Work\n";
+        printf("Stack work located at: %s\n", $stack_work_abs);
+        return "PATH=\"$stack_work_abs:$PATH\"";
+
     } else {
+        print "Using Default Cabal.\n";
         return "";
     }
 }
 
+# Run an individual test, and compare expected output with given
+# output and report results.
+#
 sub runtest {
     my ($test, $update) = @_;
 
@@ -73,8 +101,13 @@
     chdir "..";
 }
 
+# Main test running program to sort test input, and execute individual
+# tests.
+#
+
 my ( @without, @args, @tests, @opts );
 
+# Deal with the Args.
 if ($#ARGV>=0) {
     my $test = shift @ARGV;
     if ($test eq "all") {
@@ -119,6 +152,8 @@
     print "Give a test name, or 'all' to run all.\n";
     exit;
 }
+
+# Run the tests.
 
 my $update  = 0;
 my $diff    = 0;