diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -23,6 +23,22 @@
 * C function pointers can be called.
 * Idris can access pointers to C globals.
 
+Effects
+-------
+
+* Effects can now be given in any order in effect lists (there is no need
+for the ordering to be preserved in sub lists of effects)
+
+Elaborator reflection updates
+-----------------------------
+
+* Datatypes can now be defined from elaborator reflection:
+  - declareDatatype adds the type constructor declaration to the context
+  - defineDatatype adds the constructors to the datatype
+  - To declare an inductive-recursive family, declare the types of the
+    function and the type constructor before defining the pattern-match
+    cases and constructors.
+
 Minor language changes
 ----------------------
 
diff --git a/idris.cabal b/idris.cabal
--- a/idris.cabal
+++ b/idris.cabal
@@ -1,5 +1,5 @@
 Name:           idris
-Version:        0.10.2
+Version:        0.10.3
 License:        BSD3
 License-file:   LICENSE
 Author:         Edwin Brady
@@ -124,6 +124,8 @@
 
                        libs/contrib/contrib.ipkg
                        libs/contrib/Makefile
+                       libs/contrib/*.idr
+                       libs/contrib/CFFI/*.idr
                        libs/contrib/Classes/*.idr
                        libs/contrib/Control/*.idr
                        libs/contrib/Control/Isomorphism/*.idr
@@ -482,6 +484,11 @@
                        test/ffi007/*.h
                        test/ffi007/run
                        test/ffi007/expected
+                       test/ffi008/*.idr
+                       test/ffi008/*.c
+                       test/ffi008/*.h
+                       test/ffi008/run
+                       test/ffi008/expected
 
                        test/folding001/*.idr
                        test/folding001/run
@@ -609,6 +616,14 @@
                        test/primitives005/*.idr
                        test/primitives005/expected
 
+                       test/primitives006/run
+                       test/primitives006/array.c
+                       test/primitives006/array.h
+                       test/primitives006/load-test.idr
+                       test/primitives006/Data/Bytes.idr
+                       test/primitives006/Data/ByteArray.idr
+                       test/primitives006/expected
+
                        test/pkg001/run
                        test/pkg001/test.ipkg
                        test/pkg001/*.idr
@@ -831,11 +846,6 @@
   Default:      False
   manual:       True
 
-Flag curses
-  Description:  Use Curses to get the screen width
-  Default:      False
-  manual:       True
-
 -- This flag determines whether to show Git hashes in version strings
 -- Defaults to True because Hackage is a source release
 Flag release
@@ -994,6 +1004,7 @@
                 , pretty < 1.2
                 , process < 1.3
                 , split < 0.3
+                , terminal-size < 0.4
                 , text >=1.2.1.0 && < 1.3
                 , time >= 1.4 && < 1.6
                 , transformers < 0.5
@@ -1045,9 +1056,6 @@
      build-depends: libffi < 0.2
      extra-libraries: gmp
      cpp-options:   -DIDRIS_GMP
-  if flag(curses)
-     build-depends: hscurses < 1.5
-     cpp-options:   -DCURSES
   if flag(freestanding)
      other-modules: Target_idris
      cpp-options:   -DFREESTANDING
diff --git a/libs/base/Control/Monad/State.idr b/libs/base/Control/Monad/State.idr
--- a/libs/base/Control/Monad/State.idr
+++ b/libs/base/Control/Monad/State.idr
@@ -54,7 +54,7 @@
 
 ||| The State monad. See the MonadState interface
 State : Type -> Type -> Type
-State s a = StateT s Identity a
+State = \s, a => StateT s Identity a
 
 ||| Unwrap a State monad computation.
 runState : StateT s Identity a -> s -> (a, s)
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
@@ -40,17 +40,30 @@
 getUName (NS n ns) = getUName n
 getUName _         = Nothing
 
-total
-unApply : TT -> (TT, List TT)
-unApply t = unA t []
-  where unA : TT -> List TT -> (TT, List TT)
-        unA (App fn arg) args = unA fn (arg::args)
-        unA tm           args = (tm, args)
+namespace TT
+  total
+  unApply : TT -> (TT, List TT)
+  unApply t = unA t []
+    where unA : TT -> List TT -> (TT, List TT)
+          unA (App fn arg) args = unA fn (arg::args)
+          unA tm           args = (tm, args)
 
-total
-mkApp : TT -> List TT -> TT
-mkApp tm []      = tm
-mkApp tm (a::as) = mkApp (App tm a) as
+  total
+  mkApp : Foldable f => TT -> f TT -> TT
+  mkApp f args = foldl App f args
+
+namespace Raw
+  total
+  unApply : Raw -> (Raw, List Raw)
+  unApply tm = unApply' tm []
+    where unApply' : Raw -> List Raw -> (Raw, List Raw)
+          unApply' (RApp f x) xs = unApply' f (x::xs)
+          unApply' notApp xs = (notApp, xs)
+
+  total
+  mkApp : Foldable f => Raw -> f Raw -> Raw
+  mkApp f args = foldl RApp f args
+
 
 total
 binderTy : Binder t -> t
diff --git a/libs/contrib/CFFI.idr b/libs/contrib/CFFI.idr
new file mode 100644
--- /dev/null
+++ b/libs/contrib/CFFI.idr
@@ -0,0 +1,4 @@
+module CFFI
+
+import public CFFI.Types
+import public CFFI.Memory
diff --git a/libs/contrib/CFFI/Memory.idr b/libs/contrib/CFFI/Memory.idr
new file mode 100644
--- /dev/null
+++ b/libs/contrib/CFFI/Memory.idr
@@ -0,0 +1,94 @@
+||| Machinery for interfacing with C.
+module CFFI.Memory
+
+import CFFI.Types
+import Data.Vect
+
+%include C "memory.h"
+
+%access public export
+%default partial
+
+
+data CPtr = CPt Ptr Int
+
+implicit toCPtr : Ptr -> CPtr
+toCPtr p = CPt p 0
+
+implicit toPtr : CPtr -> Ptr
+toPtr (CPt p 0) = p
+toPtr (CPt p o) = prim__ptrOffset p o
+
+||| Import of malloc from the C standard library.
+malloc : Int -> IO Ptr
+malloc size = foreign FFI_C "malloc" (Int -> IO Ptr) size
+
+||| Import of free from the C standard library.
+mfree : Ptr -> IO ()
+mfree ptr = foreign FFI_C "free" (Ptr -> IO ()) ptr
+
+||| Allocate enough memory to hold an instance of a C typr
+alloc : Composite -> IO CPtr
+alloc t = return $ CPt !(malloc (sizeOf t)) 0
+
+||| Free memory allocated with alloc
+free : CPtr -> IO ()
+free (CPt p _ ) = mfree p
+
+||| Perform an IO action with memory that is freed afterwards
+withAlloc : Composite -> (CPtr -> IO ()) -> IO ()
+withAlloc t f = do m <- alloc t
+                   f m
+                   free m
+
+infixl 1 ~~>
+||| Perform an IO action with memory that is freed afterwards
+(~~>) :  Composite-> (CPtr -> IO ()) -> IO ()
+(~~>) = withAlloc
+
+||| Read from memory
+peek : (t: CType) -> CPtr -> IO (translate t)
+peek I8 (CPt p o) = prim_peek8 p o
+peek I16 (CPt p o) = prim_peek16 p o
+peek I32 (CPt p o) = prim_peek32 p o
+peek I64 (CPt p o) = prim_peek64 p o
+peek FLOAT (CPt p o) = prim_peekSingle p o
+peek DOUBLE (CPt p o) = prim_peekDouble p o
+peek PTR (CPt p o) = prim_peekPtr p o
+
+||| Write to memory
+poke : (t : CType) -> CPtr -> translate t -> IO ()
+poke I8 (CPt p o) x = do _ <- prim_poke8 p o x
+                         return ()
+poke I16 (CPt p o) x = do _ <- prim_poke16 p o x
+                          return ()
+poke I32 (CPt p o) x = do _ <- prim_poke32 p o x
+                          return ()
+poke I64 (CPt p o) x = do _ <- prim_poke64 p o x
+                          return ()
+poke PTR (CPt p o) x = do _ <- prim_pokePtr p o x
+                          return ()
+poke FLOAT (CPt p o) x = do _ <- prim_pokeSingle p o x
+                            return ()
+poke DOUBLE (CPt p o) x = do _ <- prim_pokeDouble p o x
+                             return ()
+
+||| Update memory with a function.
+update : (t: CType) -> CPtr -> (translate t -> translate t) -> IO ()
+update ty cp f = do val <- peek ty cp
+                    out <- return $ f val
+                    poke ty cp out
+
+||| Get a pointer to a field in a composite value
+field : Composite -> Nat ->  CPtr -> CPtr
+field arr@(ARRAY n t) i (CPt p o) = CPt p (o + offset arr i)
+field un@(UNION xs) i (CPt p o) = CPt p o
+field st@(STRUCT xs) i (CPt p o) = CPt p (o + offset st i)
+field ps@(PACKEDSTRUCT xs) i (CPt p o) = CPt p (o + offset ps i)
+field (T t) Z p = p
+
+infixl 10 #
+
+||| Get a pointer to a field in a composite value
+(#) : Composite -> Nat -> CPtr -> CPtr
+(#) = field
diff --git a/libs/contrib/CFFI/Types.idr b/libs/contrib/CFFI/Types.idr
new file mode 100644
--- /dev/null
+++ b/libs/contrib/CFFI/Types.idr
@@ -0,0 +1,159 @@
+||| Types for interfacing with C.
+||| This file should be kept free from IO.
+module CFFI.Types
+
+import Data.Vect
+import Debug.Error
+
+%access public export
+%default partial
+
+||| An universe of C types.
+data CType = I8 | I16 | I32 | I64 | FLOAT | DOUBLE | PTR
+
+||| Composites of C types
+data Composite = T CType | ARRAY Int Composite | STRUCT (List Composite) | UNION (List Composite)
+                | PACKEDSTRUCT (List Composite)
+
+||| Implicit conversion of primitive C types to composites
+implicit mkComposite : CType -> Composite
+mkComposite x = T x
+
+Show CType where
+    show I8 = "I8"
+    show I16 = "I16"
+    show I32 = "I32"
+    show I64 = "I64"
+    show FLOAT = "FLOAT"
+    show DOUBLE = "DOUBLE"
+    show PTR = "PTR"
+
+Show Composite where
+    show (T ct) = show ct
+    show (ARRAY n t) = "ARRAY " ++ show n ++ " " ++ show t
+    show (STRUCT xs) = "STRUCT " ++ show xs
+    show (UNION xs) = "UNION " ++ show xs
+    show (PACKEDSTRUCT xs) = "PACKEDSTRUCT " ++ show xs
+
+||| What Idris type the C type is marshalled to
+translate : CType -> Type
+translate I8 = Bits8
+translate I16 = Bits16
+translate I32 = Bits32
+translate I64 = Bits64
+translate FLOAT = Double
+translate DOUBLE = Double
+translate PTR = Ptr
+
+mutual
+    private
+    sizeOfCT : CType -> Int
+    sizeOfCT I8 = 1
+    sizeOfCT I16 = 2
+    sizeOfCT I32 = 4
+    sizeOfCT I64 = 8
+    sizeOfCT FLOAT = 4
+    sizeOfCT DOUBLE = 8
+    sizeOfCT PTR = prim__sizeofPtr
+
+    ||| Size of value of the type in bytes
+    export
+    sizeOf : Composite -> Int
+    sizeOf (T ct) = sizeOfCT ct
+    sizeOf (ARRAY n t) = n * sizeOf t
+    sizeOf (STRUCT xs) = sizeOfStruct xs
+    sizeOf (UNION xs) = foldl (\acc, x =>max acc $ sizeOf x) 0 xs
+    sizeOf (PACKEDSTRUCT xs) = foldl (\acc, x => acc + sizeOf x) 0 xs
+
+    private
+    alignOfCT : CType -> Int
+    alignOfCT I8 = 1
+    alignOfCT I16 = 2
+    alignOfCT I32 = 4
+    alignOfCT I64 = prim__sizeofPtr
+    alignOfCT FLOAT = 4
+    alignOfCT DOUBLE = prim__sizeofPtr
+    alignOfCT PTR = prim__sizeofPtr
+
+    ||| Alignment requirement of the type
+    export
+    alignOf : Composite -> Int
+    alignOf (T t) = alignOfCT t
+    alignOf (ARRAY n t) = alignOf t
+    alignOf (STRUCT xs) = foldl (\acc, x => max acc $ alignOf x) 0 xs
+    alignOf (UNION xs) = foldl (\acc, x => max acc $ alignOf x) 0 xs
+    alignOf (PACKEDSTRUCT xs) = 1
+
+    private
+    pad : Int -> Int -> Int
+    pad pos align = let c = pos `mod` align in if c == 0 then 0 else align - c
+
+    private
+    nextOffset : Composite -> Int -> Int
+    nextOffset ty pos = pos + pad pos (alignOf ty)
+
+    private
+    offsetsStruct : List Composite -> List Int
+    offsetsStruct xs = offsets' xs 0
+        where
+            offsets' : List Composite -> Int -> List Int
+            offsets' [] _ = []
+            offsets' (x::xs) pos = (nextOffset x pos)::(offsets' xs (nextOffset x pos + sizeOf x))
+
+    private
+    sizeOfStruct : List Composite -> Int
+    sizeOfStruct xs = sizeStruct' xs 0 1
+        where
+            sizeStruct' : List Composite -> Int -> Int -> Int
+            sizeStruct' [] pos maxAlign = pos + (pad pos maxAlign)
+            sizeStruct' (x::xs) pos maxAlign = sizeStruct' xs (nextOffset x pos + sizeOf x)
+                                                        (max maxAlign (alignOf x))
+
+||| Number of fields in a composite type
+export
+fields : Composite -> Nat
+fields (STRUCT xs) = length xs
+fields (PACKEDSTRUCT xs) = length xs
+fields (UNION xs) = length xs
+fields (ARRAY n _) = toNat n
+fields (T _) = 1
+
+private
+offsetsPacked : List Composite -> List Int
+offsetsPacked xs = offsets' xs [] 0
+    where
+        offsets' : List Composite -> List Int -> Int -> List Int
+        offsets' [] acc _ = reverse acc
+        offsets' (x::xs) acc pos = offsets' xs (pos::acc) (sizeOf x)
+
+private
+indexOrFail : Nat -> List a -> a
+indexOrFail i xs = case index' i xs of
+                        Just x => x
+                        Nothing => error "Out of bounds access"
+
+||| The offset of a firld in a composite type
+export
+offset : Composite -> Nat -> Int
+offset (STRUCT xs) i = indexOrFail i (offsetsStruct xs)
+offset (PACKEDSTRUCT xs) i = indexOrFail i (offsetsPacked xs)
+offset (ARRAY _ t) i = sizeOf t * toIntNat i
+offset (T _) _ = 0
+
+||| All offsets of a composite type
+export
+offsets : Composite -> List Int
+offsets (STRUCT xs) = offsetsStruct xs
+offsets (PACKEDSTRUCT xs) = offsetsPacked xs
+offsets (UNION xs) = replicate (length xs) 0
+offsets (ARRAY n t) = [ x*sizeOf t | x <- [0..n-1]]
+offsets (T _) = [0]
+
+||| The type of a field in a composite type.
+export
+fieldType : Composite -> Nat -> Composite
+fieldType (STRUCT xs@(y::_)) i = indexOrFail i xs
+fieldType (PACKEDSTRUCT xs@(y::_)) i = indexOrFail i xs
+fieldType (UNION xs@(y::_)) i = indexOrFail i xs
+fieldType (ARRAY n t) _ = t
+fieldType t _ = t
diff --git a/libs/contrib/Classes/Verified.idr b/libs/contrib/Classes/Verified.idr
--- a/libs/contrib/Classes/Verified.idr
+++ b/libs/contrib/Classes/Verified.idr
@@ -14,7 +14,7 @@
 -- and Monoid).
 
 interface Functor f => VerifiedFunctor (f : Type -> Type) where
-  functorIdentity : {a : Type} -> (x : f a) -> map id x = id x
+  functorIdentity : {a : Type} -> (x : f a) -> map Basics.id x = Basics.id x
   functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->
                        (g1 : a -> b) -> (g2 : b -> c) ->
                        map (g2 . g1) x = (map g2 . map g1) x
diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg
--- a/libs/contrib/contrib.ipkg
+++ b/libs/contrib/contrib.ipkg
@@ -1,7 +1,9 @@
 package contrib
 
 opts = "--nobasepkgs --total -i ../prelude -i ../base"
-modules = Control.Algebra,
+modules = CFFI, CFFI.Types, CFFI.Memory,
+
+          Control.Algebra,
           Control.Algebra.Lattice, Control.Algebra.VectorSpace,
           Control.Algebra.NumericInstances,
           Control.Isomorphism.Primitives,
diff --git a/libs/effects/Effects.idr b/libs/effects/Effects.idr
--- a/libs/effects/Effects.idr
+++ b/libs/effects/Effects.idr
@@ -84,60 +84,119 @@
 syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
 
 -- --------------------------------------- [ Properties and Proof Construction ]
+
 public export
+data SubElem : a -> List a -> Type where
+  Z : SubElem a (a :: as)
+  S : SubElem a as -> SubElem a (b :: as)
+  
+public export
 data SubList : List a -> List a -> Type where
-     SubNil : SubList [] []
-     Keep   : SubList xs ys -> SubList (x :: xs) (x :: ys)
-     Drop   : SubList xs ys -> SubList xs (x :: ys)
+  SubNil : SubList [] xs
+  InList : SubElem x ys -> SubList xs ys -> SubList (x :: xs) ys
 
+Uninhabited (SubElem x []) where
+  uninhabited Z impossible
+  uninhabited (S _) impossible
+
+-- Some useful hints for proof construction in polymorphic programs
 %hint
-subListId : SubList xs xs
-subListId {xs = Nil} = SubNil
-subListId {xs = x :: xs} = Keep subListId
+public export total
+dropFirst : SubList xs ys -> SubList xs (x :: ys)
+dropFirst SubNil = SubNil
+dropFirst (InList el sub) = InList (S el) (dropFirst sub)
 
+%hint
+public export total
+subListId : (xs : List a) -> SubList xs xs
+subListId [] = SubNil
+subListId (x :: xs) = InList Z (dropFirst (subListId xs))
+
+public export total
+inSuffix : SubElem x ys -> SubList xs ys -> SubElem x (zs ++ ys)
+inSuffix {zs = []} el sub = el
+inSuffix {zs = (x :: xs)} el sub = S (inSuffix el sub)
+
+%hint
+public export total
+dropPrefix : SubList xs ys -> SubList xs (zs ++ ys)
+dropPrefix SubNil = SubNil
+dropPrefix (InList el sub) = InList (inSuffix el sub) (dropPrefix sub)
+
+public export total
+inPrefix : SubElem x ys -> SubList xs ys -> SubElem x (ys ++ zs)
+inPrefix {zs = []} {ys} el sub
+    = rewrite appendNilRightNeutral ys in el
+inPrefix {zs = (x :: xs)} Z sub = Z
+inPrefix {zs = (x :: xs)} (S y) sub = S (inPrefix y SubNil)
+
+%hint
+public export total
+dropSuffix : SubList xs ys -> SubList xs (ys ++ zs)
+dropSuffix SubNil = SubNil
+dropSuffix (InList el sub) = InList (inPrefix el sub) (dropSuffix sub)
+
 namespace Env
   public export
   data Env  : (m : Type -> Type) -> List EFFECT -> Type where
-       Nil  : Env m Nil
-       (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
+    Nil  : Env m Nil
+    (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
 
-public export
-data EffElem : Effect -> Type ->
-               List EFFECT -> Type where
-     Here : EffElem x a (MkEff a x :: xs)
-     There : EffElem x a xs -> EffElem x a (y :: xs)
+namespace EffElem
+  public export
+  data EffElem : Effect -> Type ->
+                 List EFFECT -> Type where
+    Here : EffElem x a (MkEff a x :: xs)
+    There : EffElem x a xs -> EffElem x a (y :: xs)
+    
+total envElem : SubElem x xs -> Env m xs -> Env m [x]
+envElem Z (x :: xs) = [x]
+envElem (S k) (x :: xs) = envElem k xs
 
 ||| make an environment corresponding to a sub-list
-private
-dropEnv : Env m ys -> SubList xs ys -> Env m xs
+total dropEnv : Env m ys -> SubList xs ys -> Env m xs
 dropEnv [] SubNil = []
-dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
-dropEnv (v :: vs) (Drop rest) = dropEnv vs rest
+dropEnv [] (InList idx rest) = absurd idx
+dropEnv (y::ys) SubNil = []
+dropEnv e@(y::ys) (InList idx rest) = 
+  let [x] = envElem idx e
+  in x :: dropEnv e rest
 
 public export
-updateWith : (ys' : List a) -> (xs : List a) ->
-             SubList ys xs -> List a
-updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
-updateWith ys        (x :: xs) (Drop rest) = x :: updateWith ys xs rest
-updateWith []        []        SubNil      = []
-updateWith (y :: ys) []        SubNil      = y :: ys
-updateWith []        (x :: xs) (Keep rest) = []
+total updateAt : (idx : SubElem x' xs) -> (a:Type) -> List EFFECT -> List EFFECT
+updateAt Z a [] = []
+updateAt Z a ((MkEff b eff) :: xs) = (MkEff a eff) :: xs
+updateAt (S k) a [] = []
+updateAt (S k) a (x :: xs) = x :: updateAt k a xs
 
+public export
+total updateWith : (ys' : List EFFECT) -> (xs : List EFFECT) ->
+             SubList ys xs -> List EFFECT
+updateWith [] xs sl = xs
+updateWith (y :: ys) xs SubNil = xs
+updateWith ((MkEff a f) :: ys) xs (InList idx rest) = updateAt idx a (updateWith ys xs rest)
+
+public export
+total replaceEnvAt : (x : a) -> (idx : SubElem x' xs) -> Env m ys ->
+               Env m (updateAt idx a ys)
+replaceEnvAt x Z [] = []
+replaceEnvAt x Z (y :: ys) = x :: ys
+replaceEnvAt x (S k) [] = []
+replaceEnvAt x (S k) (y :: ys) = y :: replaceEnvAt x k ys
+
 ||| Put things back, replacing old with new in the sub-environment
-private
-rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
+public export
+total rebuildEnv : {ys':List EFFECT} -> Env m ys' -> (prf : SubList ys xs) ->
              Env m xs -> Env m (updateWith ys' xs prf)
-rebuildEnv []        SubNil      env = env
-rebuildEnv (x :: xs) SubNil      env = x :: xs
-rebuildEnv []        (Keep rest) (y :: env) = []
-rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
-rebuildEnv xs        (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
-
+rebuildEnv [] SubNil env = env
+rebuildEnv (x :: xs) SubNil env = env
+rebuildEnv [] (InList w s) env = env
+rebuildEnv (x :: xs) (InList idx rest) env = replaceEnvAt x idx (rebuildEnv xs rest env) 
 
 -- -------------------------------------------------- [ The Effect EDSL itself ]
 
 public export
-updateResTy : (val : t) ->
+total updateResTy : (val : t) ->
               (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
               List EFFECT
 updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
diff --git a/libs/prelude/Builtins.idr b/libs/prelude/Builtins.idr
--- a/libs/prelude/Builtins.idr
+++ b/libs/prelude/Builtins.idr
@@ -184,6 +184,7 @@
 
 export data Ptr : Type
 export data ManagedPtr : Type
+export data CData : Type
 
 %extern prim__readFile : prim__WorldType -> Ptr -> String
 %extern prim__writeFile : prim__WorldType -> Ptr -> String -> Int
@@ -201,6 +202,7 @@
 -- primitives for accessing memory.
 %extern prim__asPtr : ManagedPtr -> Ptr
 %extern prim__sizeofPtr : Int
+%extern prim__ptrOffset : Ptr -> Int -> Ptr
 %extern prim__peek8 : prim__WorldType -> Ptr -> Int -> Bits8
 %extern prim__peek16 : prim__WorldType -> Ptr -> Int -> Bits16
 %extern prim__peek32 : prim__WorldType -> Ptr -> Int -> Bits32
@@ -213,3 +215,8 @@
 
 %extern prim__peekPtr : prim__WorldType -> Ptr -> Int -> Ptr
 %extern prim__pokePtr : prim__WorldType -> Ptr -> Int -> Ptr -> Int
+
+%extern prim__peekDouble : prim__WorldType -> Ptr -> Int -> Double
+%extern prim__pokeDouble : prim__WorldType -> Ptr -> Int -> Double -> Int
+%extern prim__peekSingle : prim__WorldType -> Ptr -> Int -> Double
+%extern prim__pokeSingle : prim__WorldType -> Ptr -> Int -> Double -> Int
diff --git a/libs/prelude/IO.idr b/libs/prelude/IO.idr
--- a/libs/prelude/IO.idr
+++ b/libs/prelude/IO.idr
@@ -178,6 +178,7 @@
        C_Any   : C_Types (Raw a)
        C_FnT   : C_FnTypes t -> C_Types (CFnPtr t)
        C_IntT  : C_IntTypes i -> C_Types i
+       C_CData : C_Types CData
 
     ||| A descriptor for the C FFI. See the constructors of `C_Types`
     ||| and `C_IntTypes` for the concrete types that are available.
@@ -348,3 +349,19 @@
 prim_pokePtr : Ptr -> Int -> Ptr -> IO Int
 prim_pokePtr ptr offset val = MkIO (\w =>  prim_io_return (
     prim__pokePtr (world w) ptr offset val))
+
+prim_peekDouble : Ptr -> Int -> IO Double
+prim_peekDouble ptr offset = MkIO (\w => prim_io_return (prim__peekDouble (world w) ptr offset))
+
+prim_pokeDouble : Ptr -> Int -> Double -> IO Int
+prim_pokeDouble ptr offset val = MkIO (\w =>  prim_io_return (
+    prim__pokeDouble (world w) ptr offset val))
+
+||| Single precision floats are marshalled to Doubles
+prim_peekSingle : Ptr -> Int -> IO Double
+prim_peekSingle ptr offset = MkIO (\w => prim_io_return (prim__peekSingle (world w) ptr offset))
+
+||| Single precision floats are marshalled to Doubles
+prim_pokeSingle : Ptr -> Int -> Double -> IO Int
+prim_pokeSingle ptr offset val = MkIO (\w =>  prim_io_return (
+    prim__pokeSingle (world w) ptr offset val))
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
@@ -57,11 +57,11 @@
   ||| Indices are not uniform
   TyConIndex FunArg
 
-||| A type declaration
+||| A type declaration for a function or datatype
 record TyDecl where
   constructor Declare
 
-  ||| The name of the function being declared.
+  ||| The fully-qualified name of the function or datatype being declared.
   name : TTName
 
   ||| Each argument is in the scope of the names of previous arguments.
@@ -83,6 +83,34 @@
   clauses : List (FunClause a)
 
 
+||| A constructor to be associated with a new datatype.
+record ConstructorDefn where
+  constructor Constructor
+
+  ||| The name of the constructor. The name must _not_ be qualified -
+  ||| that is, it should begin with the `UN` or `MN` constructors.
+  name : TTName
+
+  ||| The constructor arguments. Idris will infer which arguments are
+  ||| datatype parameters.
+  arguments : List FunArg
+
+  ||| The specific type constructed by the constructor.
+  returnType : Raw
+
+
+||| A definition of a datatype to be added during an elaboration script.
+record DataDefn where
+  constructor DefineDatatype
+  ||| The name of the datatype being defined. It must be
+  ||| fully-qualified, and it must have been previously declared as a
+  ||| datatype.
+  name : TTName
+
+  ||| A list of constructors for the datatype.
+  constructors : List ConstructorDefn
+
+
 data CtorArg = CtorParameter FunArg | CtorField FunArg
 
 ||| A reflected datatype definition
@@ -151,6 +179,8 @@
 
   Prim__DeclareType : TyDecl -> Elab ()
   Prim__DefineFunction : FunDefn Raw -> Elab ()
+  Prim__DeclareDatatype : TyDecl -> Elab ()
+  Prim__DefineDatatype : DataDefn -> Elab ()
   Prim__AddInstance : TTName -> TTName -> Elab ()
   Prim__IsTCName : TTName -> Elab Bool
 
@@ -335,7 +365,7 @@
 
   export
   matchApply : (op : Raw) -> (argSpec : List Bool) -> Elab (List TTName)
-  matchApply tm argSpec = map snd <$> Prim__Apply tm argSpec
+  matchApply tm argSpec = map snd <$> Prim__MatchApply tm argSpec
 
   ||| Move the focus to the specified hole. Fails if the hole does not
   ||| exist.
@@ -509,6 +539,17 @@
   export
   defineFunction : FunDefn Raw -> Elab ()
   defineFunction defun = Prim__DefineFunction defun
+
+  ||| Declare a datatype in the global context. This step only
+  ||| establishes the type constructor; use `defineDatatype` to give
+  ||| it constructors.
+  export
+  declareDatatype : TyDecl -> Elab ()
+  declareDatatype decl = Prim__DeclareDatatype decl
+
+  export
+  defineDatatype : DataDefn -> Elab ()
+  defineDatatype defn = Prim__DefineDatatype defn
 
   ||| Register a new implementation for interface resolution.
   |||
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
@@ -26,16 +26,6 @@
 updateTyConArgTy f (TyConIndex a) =
     TyConIndex (record {type = f (type a) } a)
 
-unApply : Raw -> (Raw, List Raw)
-unApply tm = unApply' tm []
-  where unApply' : Raw -> List Raw -> (Raw, List Raw)
-        unApply' (RApp f x) xs = unApply' f (x::xs)
-        unApply' notApp xs = (notApp, xs)
-
-mkApp : Raw -> List Raw -> Raw
-mkApp f [] = f
-mkApp f (x :: xs) = mkApp (RApp f x) xs
-
 ||| Grab the binders from around a term, alpha-converting to make
 ||| their names unique
 partial
diff --git a/rts/getline.c b/rts/getline.c
--- a/rts/getline.c
+++ b/rts/getline.c
@@ -38,40 +38,41 @@
 ssize_t
 getdelim(char **buf, size_t *bufsiz, int delimiter, FILE *fp)
 {
-  char *ptr, *eptr;
-
-
-  if (*buf == NULL || *bufsiz == 0) {
-    *bufsiz = BUFSIZ;
-    if ((*buf = malloc(*bufsiz)) == NULL)
-      return -1;
-  }
+    char *ptr, *eptr;
 
-  for (ptr = *buf, eptr = *buf + *bufsiz;;) {
-    int c = fgetc(fp);
-    if (c == -1) {
-      if (feof(fp))
-        return ptr == *buf ? -1 : ptr - *buf;
-      else
-        return -1;
-    }
-    *ptr++ = c;
-    if (c == delimiter) {
-      *ptr = '\0';
-      return ptr - *buf;
+    if (*buf == NULL || *bufsiz == 0) {
+        *bufsiz = BUFSIZ;
+        if ((*buf = malloc(*bufsiz)) == NULL)
+            return -1;
     }
-    if (ptr + 2 >= eptr) {
-      char *nbuf;
-      size_t nbufsiz = *bufsiz * 2;
-      ssize_t d = ptr - *buf;
-      if ((nbuf = realloc(*buf, nbufsiz)) == NULL)
-        return -1;
-      *buf = nbuf;
-      *bufsiz = nbufsiz;
-      eptr = nbuf + nbufsiz;
-      ptr = nbuf + d;
+
+    for (ptr = *buf, eptr = *buf + *bufsiz;;) {
+        int c = fgetc(fp);
+        if (c == -1) {
+            if (feof(fp)) {
+                *ptr = '\0';
+                return ptr - *buf;
+            } else {
+                return -1;
+            }
+        }
+        *ptr++ = c;
+        if (c == delimiter) {
+            *ptr = '\0';
+            return ptr - *buf;
+        }
+        if (ptr + 2 >= eptr) {
+            char *nbuf;
+            size_t nbufsiz = *bufsiz * 2;
+            ssize_t d = ptr - *buf;
+            if ((nbuf = realloc(*buf, nbufsiz)) == NULL)
+                return -1;
+            *buf = nbuf;
+            *bufsiz = nbufsiz;
+            eptr = nbuf + nbufsiz;
+            ptr = nbuf + d;
+        }
     }
-  }
 }
 
 ssize_t
diff --git a/rts/idris_bitstring.c b/rts/idris_bitstring.c
--- a/rts/idris_bitstring.c
+++ b/rts/idris_bitstring.c
@@ -5,7 +5,7 @@
 VAL idris_b8CopyForGC(VM *vm, VAL a) {
     uint8_t A = a->info.bits8;
     VAL cl = allocate(sizeof(Closure), 1);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = A;
     return cl;
 }
@@ -13,7 +13,7 @@
 VAL idris_b16CopyForGC(VM *vm, VAL a) {
     uint16_t A = a->info.bits16;
     VAL cl = allocate(sizeof(Closure), 1);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = A;
     return cl;
 }
@@ -21,7 +21,7 @@
 VAL idris_b32CopyForGC(VM *vm, VAL a) {
     uint32_t A = a->info.bits32;
     VAL cl = allocate(sizeof(Closure), 1);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = A;
     return cl;
 }
@@ -29,7 +29,7 @@
 VAL idris_b64CopyForGC(VM *vm, VAL a) {
     uint64_t A = a->info.bits64;
     VAL cl = allocate(sizeof(Closure), 1);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = A;
     return cl;
 }
@@ -37,7 +37,7 @@
 VAL idris_b8(VM *vm, VAL a) {
     uint8_t A = GETINT(a);
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = (uint8_t) A;
     return cl;
 }
@@ -45,7 +45,7 @@
 VAL idris_b16(VM *vm, VAL a) {
     uint16_t A = GETINT(a);
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = (uint16_t) A;
     return cl;
 }
@@ -53,7 +53,7 @@
 VAL idris_b32(VM *vm, VAL a) {
     uint32_t A = GETINT(a);
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = (uint32_t) A;
     return cl;
 }
@@ -61,7 +61,7 @@
 VAL idris_b64(VM *vm, VAL a) {
     uint64_t A = GETINT(a);
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = (uint64_t) A;
     return cl;
 }
@@ -72,28 +72,28 @@
 
 VAL idris_b8const(VM *vm, uint8_t a) {
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = a;
     return cl;
 }
 
 VAL idris_b16const(VM *vm, uint16_t a) {
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = a;
     return cl;
 }
 
 VAL idris_b32const(VM *vm, uint32_t a) {
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = a;
     return cl;
 }
 
 VAL idris_b64const(VM *vm, uint64_t a) {
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = a;
     return cl;
 }
@@ -102,7 +102,7 @@
     uint8_t A = a->info.bits8;
     uint8_t B = b->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = A + B;
     return cl;
 }
@@ -111,7 +111,7 @@
     uint8_t A = a->info.bits8;
     uint8_t B = b->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = A - B;
     return cl;
 }
@@ -120,7 +120,7 @@
     uint8_t A = a->info.bits8;
     uint8_t B = b->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = A * B;
     return cl;
 }
@@ -129,7 +129,7 @@
     uint8_t A = a->info.bits8;
     uint8_t B = b->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = A / B;
     return cl;
 }
@@ -138,7 +138,7 @@
     uint8_t A = a->info.bits8;
     uint8_t B = b->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = (uint8_t) (((int8_t) A) / ((int8_t) B));
     return cl;
 }
@@ -147,7 +147,7 @@
     uint8_t A = a->info.bits8;
     uint8_t B = b->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = A % B;
     return cl;
 }
@@ -156,7 +156,7 @@
     uint8_t A = a->info.bits8;
     uint8_t B = b->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = (uint8_t) (((int8_t) A) % ((int8_t) B));
     return cl;
 }
@@ -184,7 +184,7 @@
 VAL idris_b8Compl(VM *vm, VAL a) {
     uint8_t A = a->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = ~ A;
     return cl;
 }
@@ -193,7 +193,7 @@
     uint8_t A = a->info.bits8;
     uint8_t B = b->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = A & B;
     return cl;
 }
@@ -202,7 +202,7 @@
     uint8_t A = a->info.bits8;
     uint8_t B = b->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = A | B;
     return cl;
 }
@@ -211,7 +211,7 @@
     uint8_t A = a->info.bits8;
     uint8_t B = b->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = A ^ B;
     return cl;
 }
@@ -220,7 +220,7 @@
     uint8_t A = a->info.bits8;
     uint8_t B = b->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = A << B;
     return cl;
 }
@@ -229,7 +229,7 @@
     uint8_t A = a->info.bits8;
     uint8_t B = b->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = A >> B;
     return cl;
 }
@@ -238,7 +238,7 @@
     uint8_t A = a->info.bits8;
     uint8_t B = b->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = (uint8_t) (((int8_t) A) >> ((int8_t) B));
     return cl;
 }
@@ -247,7 +247,7 @@
     uint16_t A = a->info.bits16;
     uint16_t B = b->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = A + B;
     return cl;
 }
@@ -256,7 +256,7 @@
     uint16_t A = a->info.bits16;
     uint16_t B = b->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = A - B;
     return cl;
 }
@@ -265,7 +265,7 @@
     uint16_t A = a->info.bits16;
     uint16_t B = b->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = A * B;
     return cl;
 }
@@ -274,7 +274,7 @@
     uint16_t A = a->info.bits16;
     uint16_t B = b->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = A / B;
     return cl;
 }
@@ -283,7 +283,7 @@
     uint16_t A = a->info.bits16;
     uint16_t B = b->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = (uint16_t) (((int16_t) A) / ((int16_t) B));
     return cl;
 }
@@ -292,7 +292,7 @@
     uint16_t A = a->info.bits16;
     uint16_t B = b->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = A % B;
     return cl;
 }
@@ -301,7 +301,7 @@
     uint16_t A = a->info.bits16;
     uint16_t B = b->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = (uint16_t) (((int16_t) A) % ((int16_t) B));
     return cl;
 }
@@ -329,7 +329,7 @@
 VAL idris_b16Compl(VM *vm, VAL a) {
     uint16_t A = a->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = ~ A;
     return cl;
 }
@@ -338,7 +338,7 @@
     uint16_t A = a->info.bits16;
     uint16_t B = b->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = A & B;
     return cl;
 }
@@ -347,7 +347,7 @@
     uint16_t A = a->info.bits16;
     uint16_t B = b->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = A | B;
     return cl;
 }
@@ -356,7 +356,7 @@
     uint16_t A = a->info.bits16;
     uint16_t B = b->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = A ^ B;
     return cl;
 }
@@ -365,7 +365,7 @@
     uint16_t A = a->info.bits16;
     uint16_t B = b->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = A << B;
     return cl;
 }
@@ -374,7 +374,7 @@
     uint16_t A = a->info.bits16;
     uint16_t B = b->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = A >> B;
     return cl;
 }
@@ -383,7 +383,7 @@
     uint16_t A = a->info.bits16;
     uint16_t B = b->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = (uint16_t) (((int16_t) A) >> ((int16_t) B));
     return cl;
 }
@@ -392,7 +392,7 @@
     uint32_t A = a->info.bits32;
     uint32_t B = b->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = A + B;
     return cl;
 }
@@ -401,7 +401,7 @@
     uint32_t A = a->info.bits32;
     uint32_t B = b->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = A - B;
     return cl;
 }
@@ -410,7 +410,7 @@
     uint32_t A = a->info.bits32;
     uint32_t B = b->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = A * B;
     return cl;
 }
@@ -419,7 +419,7 @@
     uint32_t A = a->info.bits32;
     uint32_t B = b->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = A / B;
     return cl;
 }
@@ -428,7 +428,7 @@
     uint32_t A = a->info.bits32;
     uint32_t B = b->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = (uint32_t) (((int32_t) A) / ((int32_t) B));
     return cl;
 }
@@ -437,7 +437,7 @@
     uint32_t A = a->info.bits32;
     uint32_t B = b->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = A % B;
     return cl;
 }
@@ -446,7 +446,7 @@
     uint32_t A = a->info.bits32;
     uint32_t B = b->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = (uint32_t) (((int32_t) A) % ((int32_t) B));
     return cl;
 }
@@ -474,7 +474,7 @@
 VAL idris_b32Compl(VM *vm, VAL a) {
     uint32_t A = a->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = ~ A;
     return cl;
 }
@@ -483,7 +483,7 @@
     uint32_t A = a->info.bits32;
     uint32_t B = b->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = A & B;
     return cl;
 }
@@ -492,7 +492,7 @@
     uint32_t A = a->info.bits32;
     uint32_t B = b->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = A | B;
     return cl;
 }
@@ -501,7 +501,7 @@
     uint32_t A = a->info.bits32;
     uint32_t B = b->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = A ^ B;
     return cl;
 }
@@ -510,7 +510,7 @@
     uint32_t A = a->info.bits32;
     uint32_t B = b->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = A << B;
     return cl;
 }
@@ -519,7 +519,7 @@
     uint32_t A = a->info.bits32;
     uint32_t B = b->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = A >> B;
     return cl;
 }
@@ -528,7 +528,7 @@
     uint32_t A = a->info.bits32;
     uint32_t B = b->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = (uint32_t) (((int32_t)A) >> ((int32_t)B));
     return cl;
 }
@@ -537,7 +537,7 @@
     uint64_t A = a->info.bits64;
     uint64_t B = b->info.bits64;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = A + B;
     return cl;
 }
@@ -546,7 +546,7 @@
     uint64_t A = a->info.bits64;
     uint64_t B = b->info.bits64;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = A - B;
     return cl;
 }
@@ -555,7 +555,7 @@
     uint64_t A = a->info.bits64;
     uint64_t B = b->info.bits64;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = A * B;
     return cl;
 }
@@ -564,7 +564,7 @@
     uint64_t A = a->info.bits64;
     uint64_t B = b->info.bits64;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = A / B;
     return cl;
 }
@@ -573,7 +573,7 @@
     uint64_t A = a->info.bits64;
     uint64_t B = b->info.bits64;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = (uint64_t) (((int64_t) A) / ((int64_t) B));
     return cl;
 }
@@ -582,7 +582,7 @@
     uint64_t A = a->info.bits64;
     uint64_t B = b->info.bits64;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = A % B;
     return cl;
 }
@@ -591,7 +591,7 @@
     uint64_t A = a->info.bits64;
     uint64_t B = b->info.bits64;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = (uint64_t) (((int64_t) A) % ((int64_t) B));
     return cl;
 }
@@ -619,7 +619,7 @@
 VAL idris_b64Compl(VM *vm, VAL a) {
     uint64_t A = a->info.bits64;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = ~ A;
     return cl;
 }
@@ -628,7 +628,7 @@
     uint64_t A = a->info.bits64;
     uint64_t B = b->info.bits64;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = A & B;
     return cl;
 }
@@ -637,7 +637,7 @@
     uint64_t A = a->info.bits64;
     uint64_t B = b->info.bits64;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = A | B;
     return cl;
 }
@@ -646,7 +646,7 @@
     uint64_t A = a->info.bits64;
     uint64_t B = b->info.bits64;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = A ^ B;
     return cl;
 }
@@ -655,7 +655,7 @@
     uint64_t A = a->info.bits64;
     uint64_t B = b->info.bits64;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = A << B;
     return cl;
 }
@@ -664,7 +664,7 @@
     uint64_t A = a->info.bits64;
     uint64_t B = b->info.bits64;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = A >> B;
     return cl;
 }
@@ -673,7 +673,7 @@
     uint64_t A = a->info.bits64;
     uint64_t B = b->info.bits64;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = (uint64_t) (((int64_t) A) >> ((int64_t) B));
     return cl;
 }
@@ -681,7 +681,7 @@
 VAL idris_b8Z16(VM *vm, VAL a) {
     uint8_t A = a->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = (uint16_t) A;
     return cl;
 }
@@ -689,7 +689,7 @@
 VAL idris_b8Z32(VM *vm, VAL a) {
     uint8_t A = a->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = (uint32_t) A;
     return cl;
 }
@@ -697,7 +697,7 @@
 VAL idris_b8Z64(VM *vm, VAL a) {
     uint8_t A = a->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = (uint64_t) A;
     return cl;
 }
@@ -705,7 +705,7 @@
 VAL idris_b8S16(VM *vm, VAL a) {
     uint8_t A = a->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = (uint16_t) (int16_t) (int8_t) A;
     return cl;
 }
@@ -713,7 +713,7 @@
 VAL idris_b8S32(VM *vm, VAL a) {
     uint8_t A = a->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = (uint32_t) (int32_t) (int8_t) A;
     return cl;
 }
@@ -721,7 +721,7 @@
 VAL idris_b8S64(VM *vm, VAL a) {
     uint8_t A = a->info.bits8;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = (uint64_t) (int64_t) (int8_t) A;
     return cl;
 }
@@ -729,7 +729,7 @@
 VAL idris_b16Z32(VM *vm, VAL a) {
     uint16_t A = a->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = (uint32_t) A;
     return cl;
 }
@@ -737,7 +737,7 @@
 VAL idris_b16Z64(VM *vm, VAL a) {
     uint16_t A = a->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = (uint64_t) A;
     return cl;
 }
@@ -745,7 +745,7 @@
 VAL idris_b16S32(VM *vm, VAL a) {
     uint16_t A = a->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = (uint32_t) (int32_t) (int16_t) A;
     return cl;
 }
@@ -753,7 +753,7 @@
 VAL idris_b16S64(VM *vm, VAL a) {
     uint16_t A = a->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = (uint64_t) (int64_t) (int16_t) A;
     return cl;
 }
@@ -761,7 +761,7 @@
 VAL idris_b16T8(VM *vm, VAL a) {
     uint16_t A = a->info.bits16;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = (uint8_t) A;
     return cl;
 }
@@ -769,7 +769,7 @@
 VAL idris_b32Z64(VM *vm, VAL a) {
     uint32_t A = a->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = (uint64_t) A;
     return cl;
 }
@@ -777,7 +777,7 @@
 VAL idris_b32S64(VM *vm, VAL a) {
     uint32_t A = a->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl->info.bits64 = (uint64_t) (int64_t) (int32_t) A;
     return cl;
 }
@@ -785,7 +785,7 @@
 VAL idris_b32T8(VM *vm, VAL a) {
     uint32_t A = a->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = (uint8_t) A;
     return cl;
 }
@@ -793,7 +793,7 @@
 VAL idris_b32T16(VM *vm, VAL a) {
     uint32_t A = a->info.bits32;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = (uint16_t) A;
     return cl;
 }
@@ -801,7 +801,7 @@
 VAL idris_b64T8(VM *vm, VAL a) {
     uint64_t A = a->info.bits64;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl->info.bits8 = (uint8_t) A;
     return cl;
 }
@@ -809,7 +809,7 @@
 VAL idris_b64T16(VM *vm, VAL a) {
     uint64_t A = a->info.bits64;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl->info.bits16 = (uint16_t) A;
     return cl;
 }
@@ -817,7 +817,7 @@
 VAL idris_b64T32(VM *vm, VAL a) {
     uint64_t A = a->info.bits64;
     VAL cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl->info.bits32 = (uint32_t) A;
     return cl;
 }
diff --git a/rts/idris_gc.c b/rts/idris_gc.c
--- a/rts/idris_gc.c
+++ b/rts/idris_gc.c
@@ -10,7 +10,7 @@
         return x;
     }
     switch(GETTY(x)) {
-    case CON:
+    case CT_CON:
         ar = CARITY(x);
         if (ar == 0 && CTAG(x) < 256) {
             return x;
@@ -21,49 +21,53 @@
             }
         }
         break;
-    case FLOAT:
+    case CT_FLOAT:
         cl = MKFLOATc(vm, x->info.f);
         break;
-    case STRING:
+    case CT_STRING:
         cl = MKSTRc(vm, x->info.str);
         break;
-    case STROFFSET:
+    case CT_STROFFSET:
         cl = MKSTROFFc(vm, x->info.str_offset);
         break;
-    case BIGINT:
+    case CT_BIGINT:
         cl = MKBIGMc(vm, x->info.ptr);
         break;
-    case PTR:
+    case CT_PTR:
         cl = MKPTRc(vm, x->info.ptr);
         break;
-    case MANAGEDPTR:
+    case CT_MANAGEDPTR:
         cl = MKMPTRc(vm, x->info.mptr->data, x->info.mptr->size);
         break;
-    case BITS8:
+    case CT_BITS8:
         cl = idris_b8CopyForGC(vm, x);
         break;
-    case BITS16:
+    case CT_BITS16:
         cl = idris_b16CopyForGC(vm, x);
         break;
-    case BITS32:
+    case CT_BITS32:
         cl = idris_b32CopyForGC(vm, x);
         break;
-    case BITS64:
+    case CT_BITS64:
         cl = idris_b64CopyForGC(vm, x);
         break;
-    case FWD:
+    case CT_FWD:
         return x->info.ptr;
-    case RAWDATA:
+    case CT_RAWDATA:
         {
             size_t size = x->info.size + sizeof(Closure);
             cl = allocate(size, 0);
             memcpy(cl, x, size);
         }
         break;
+    case CT_CDATA:
+        cl = MKCDATAc(vm, x->info.c_heap_item);
+        c_heap_mark_item(x->info.c_heap_item);
+        break;
     default:
         break;
     }
-    SETTY(x, FWD);
+    SETTY(x, CT_FWD);
     x->info.ptr = cl;
     return cl;
 }
@@ -76,16 +80,16 @@
     while(scan < vm->heap.next) {
        size_t inc = *((size_t*)scan);
        VAL heap_item = (VAL)(scan+sizeof(size_t));
-       // If it's a CON or STROFFSET, copy its arguments
+       // If it's a CT_CON or CT_STROFFSET, copy its arguments
        switch(GETTY(heap_item)) {
-       case CON:
+       case CT_CON:
            ar = ARITY(heap_item);
            for(i = 0; i < ar; ++i) {
                VAL newptr = copy(vm, heap_item->info.c.args[i]);
                heap_item->info.c.args[i] = newptr;
            }
            break;
-       case STROFFSET:
+       case CT_STROFFSET:
            heap_item->info.str_offset->str
                = copy(vm, heap_item->info.str_offset->str);
            break;
@@ -132,6 +136,9 @@
     if ((vm->heap.next - vm->heap.heap) > vm->heap.size >> 1) {
         vm->heap.size += vm->heap.growth;
     }
+
+    // finally, sweep the C heap
+    c_heap_sweep(&vm->c_heap);
 
     STATS_LEAVE_GC(vm->stats, vm->heap.size, vm->heap.next - vm->heap.heap)
     HEAP_CHECK(vm)
diff --git a/rts/idris_gmp.c b/rts/idris_gmp.c
--- a/rts/idris_gmp.c
+++ b/rts/idris_gmp.c
@@ -33,7 +33,7 @@
     mpz_init(*bigint);
     mpz_set_str(*bigint, val, 10);
 
-    SETTY(cl, BIGINT);
+    SETTY(cl, CT_BIGINT);
     cl -> info.ptr = (void*)bigint;
 
     return cl;
@@ -50,7 +50,7 @@
     mpz_init(*bigint);
     mpz_set(*bigint, *((mpz_t*)big));
 
-    SETTY(cl, BIGINT);
+    SETTY(cl, CT_BIGINT);
     cl -> info.ptr = (void*)bigint;
 
     return cl;
@@ -66,7 +66,7 @@
 
     mpz_init_set(*bigint, *((mpz_t*)big));
 
-    SETTY(cl, BIGINT);
+    SETTY(cl, CT_BIGINT);
     cl -> info.ptr = (void*)bigint;
 
     return cl;
@@ -82,7 +82,7 @@
 
     mpz_init_set_ui(*bigint, val);
 
-    SETTY(cl, BIGINT);
+    SETTY(cl, CT_BIGINT);
     cl -> info.ptr = (void*)bigint;
 
     return cl;
@@ -98,7 +98,7 @@
 
     mpz_init_set_si(*bigint, val);
 
-    SETTY(cl, BIGINT);
+    SETTY(cl, CT_BIGINT);
     cl -> info.ptr = (void*)bigint;
 
     return cl;
@@ -116,14 +116,14 @@
         mpz_init(*bigint);
         mpz_set_si(*bigint, GETINT(x));
 
-        SETTY(cl, BIGINT);
+        SETTY(cl, CT_BIGINT);
         cl -> info.ptr = (void*)bigint;
 
         return cl;
     } else {
         idris_doneAlloc();
         switch(GETTY(x)) {
-        case FWD:
+        case CT_FWD:
             return GETBIG(vm, x->info.ptr);
         default:
             return x;
@@ -139,7 +139,7 @@
     idris_doneAlloc();
     bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
     mpz_add(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));
-    SETTY(cl, BIGINT);
+    SETTY(cl, CT_BIGINT);
     cl -> info.ptr = (void*)bigint;
     return cl;
 }
@@ -152,7 +152,7 @@
     idris_doneAlloc();
     bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
     mpz_sub(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));
-    SETTY(cl, BIGINT);
+    SETTY(cl, CT_BIGINT);
     cl -> info.ptr = (void*)bigint;
     return cl;
 }
@@ -165,7 +165,7 @@
     idris_doneAlloc();
     bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
     mpz_mul(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));
-    SETTY(cl, BIGINT);
+    SETTY(cl, CT_BIGINT);
     cl -> info.ptr = (void*)bigint;
     return cl;
 }
@@ -178,7 +178,7 @@
     idris_doneAlloc();
     bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
     mpz_tdiv_q(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));
-    SETTY(cl, BIGINT);
+    SETTY(cl, CT_BIGINT);
     cl -> info.ptr = (void*)bigint;
     return cl;
 }
@@ -191,7 +191,7 @@
     idris_doneAlloc();
     bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
     mpz_mod(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));
-    SETTY(cl, BIGINT);
+    SETTY(cl, CT_BIGINT);
     cl -> info.ptr = (void*)bigint;
     return cl;
 }
@@ -204,7 +204,7 @@
     idris_doneAlloc();
     bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
     mpz_and(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));
-    SETTY(cl, BIGINT);
+    SETTY(cl, CT_BIGINT);
     cl -> info.ptr = (void*)bigint;
     return cl;
 }
@@ -217,7 +217,7 @@
     idris_doneAlloc();
     bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
     mpz_ior(*bigint, GETMPZ(GETBIG(vm,x)), GETMPZ(GETBIG(vm,y)));
-    SETTY(cl, BIGINT);
+    SETTY(cl, CT_BIGINT);
     cl -> info.ptr = (void*)bigint;
     return cl;
 }
@@ -230,7 +230,7 @@
     idris_doneAlloc();
     bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
     mpz_mul_2exp(*bigint, GETMPZ(GETBIG(vm,x)), GETINT(y));
-    SETTY(cl, BIGINT);
+    SETTY(cl, CT_BIGINT);
     cl -> info.ptr = (void*)bigint;
     return cl;
 }
@@ -244,7 +244,7 @@
     idris_doneAlloc();
     bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
     mpz_fdiv_q_2exp(*bigint, GETMPZ(GETBIG(vm,x)), GETINT(y));
-    SETTY(cl, BIGINT);
+    SETTY(cl, CT_BIGINT);
     cl -> info.ptr = (void*)bigint;
     return cl;
 }
@@ -257,7 +257,7 @@
     idris_doneAlloc();
     bigint = (mpz_t*)(((char*)cl) + sizeof(Closure));
     mpz_fdiv_q_2exp(*bigint, GETMPZ(GETBIG(vm,x)), GETINT(y));
-    SETTY(cl, BIGINT);
+    SETTY(cl, CT_BIGINT);
     cl -> info.ptr = (void*)bigint;
     return cl;
 }
@@ -473,7 +473,7 @@
 
     mpz_init_set_d(*bigint, val);
 
-    SETTY(cl, BIGINT);
+    SETTY(cl, CT_BIGINT);
     cl -> info.ptr = (void*)bigint;
 
     return cl;
diff --git a/rts/idris_heap.c b/rts/idris_heap.c
--- a/rts/idris_heap.c
+++ b/rts/idris_heap.c
@@ -1,12 +1,112 @@
 #include "idris_heap.h"
 #include "idris_rts.h"
+#include "idris_gc.h"
 
 #include <stdlib.h>
 #include <stddef.h>
 #include <stdio.h>
+#include <assert.h>
 
+static void c_heap_free_item(CHeap * heap, CHeapItem * item)
+{
+    assert(item->size <= heap->size);
+    heap->size -= item->size;
 
-/* Used for initializing the heap. */
+    // fix links
+    if (item->next != NULL)
+    {
+        item->next->prev_next = item->prev_next;
+    }
+    *(item->prev_next) = item->next;
+
+    // free payload
+    item->finalizer(item->data);
+
+    // free item struct
+    free(item);
+}
+
+CHeapItem * c_heap_create_item(void * data, size_t size, CDataFinalizer * finalizer)
+{
+    CHeapItem * item = (CHeapItem *) malloc(sizeof(CHeapItem));
+
+    item->data = data;
+    item->size = size;
+    item->finalizer = finalizer;
+    item->is_used = false;
+    item->next = NULL;
+    item->prev_next = NULL;
+
+    return item;
+}
+
+void c_heap_insert_if_needed(VM * vm, CHeap * heap, CHeapItem * item)
+{
+    if (item->prev_next != NULL) return;  // already inserted
+
+    if (heap->first != NULL)
+    {
+        heap->first->prev_next = &item->next;
+    }
+
+    item->prev_next = &heap->first;
+    item->next = heap->first;
+
+    heap->first = item;
+
+    // at this point, links are done; let's calculate sizes
+    
+    heap->size += item->size;
+    if (heap->size >= heap->gc_trigger_size)
+    {
+        item->is_used = true;  // don't collect what we're inserting
+        idris_gc(vm);
+    }
+}
+
+void c_heap_mark_item(CHeapItem * item)
+{
+    item->is_used = true;
+}
+
+void c_heap_sweep(CHeap * heap)
+{
+    CHeapItem * p = heap->first;
+    while (p != NULL)
+    {
+        if (p->is_used)
+        {
+            p->is_used = false;
+            p = p->next;
+        }
+        else
+        {
+            CHeapItem * unused_item = p;
+            p = p->next;
+
+            c_heap_free_item(heap, unused_item);
+        }
+    }
+
+    heap->gc_trigger_size = C_HEAP_GC_TRIGGER_SIZE(heap->size);
+}
+
+void c_heap_init(CHeap * heap)
+{
+    heap->first = NULL;
+    heap->size = 0;
+    heap->gc_trigger_size = C_HEAP_GC_TRIGGER_SIZE(heap->size);
+}
+
+void c_heap_destroy(CHeap * heap)
+{
+    while (heap->first != NULL)
+    {
+        c_heap_free_item(heap, heap->first);  // will update heap->first via the backward link
+    }
+}
+
+/* Used for initializing the FP heap. */
 void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old)
 {
     char * mem = malloc(heap_size);
@@ -86,7 +186,7 @@
        VAL heap_item = (VAL)(scan + sizeof(size_t));
 
        switch(GETTY(heap_item)) {
-       case CON:
+       case CT_CON:
            {
              int ar = ARITY(heap_item);
              int i = 0;
@@ -107,7 +207,7 @@
                      if (!(ptr < heap_item)) {
                          fprintf(stderr,
                                  "RTS ERROR: heap unidirectionality broken:" \
-                                 "<CON %p> <FIELD %p>\n",
+                                 "<CT_CON %p> <FIELD %p>\n",
                                  heap_item, ptr);
                          exit(EXIT_FAILURE);
                      }
@@ -116,9 +216,9 @@
              }
              break;
            }
-       case FWD:
+       case CT_FWD:
            // Check for artifacts after cheney gc.
-           fprintf(stderr, "RTS ERROR: FWD in working heap.\n");
+           fprintf(stderr, "RTS ERROR: CT_FWD in working heap.\n");
            exit(EXIT_FAILURE);
            break;
        default:
diff --git a/rts/idris_heap.h b/rts/idris_heap.h
--- a/rts/idris_heap.h
+++ b/rts/idris_heap.h
@@ -1,7 +1,89 @@
 #ifndef _IDRIS_HEAP_H
 #define _IDRIS_HEAP_H
 
+#include <stdbool.h>
 #include <stddef.h>
+
+/* *** C heap ***
+ * Objects with finalizers. Mark&sweep-collected.
+ *
+ * The C heap is implemented as a doubly linked list
+ * of pointers coupled with their finalizers.
+ */
+
+struct VM;
+
+#define C_HEAP_GC_TRIGGER_SIZE(heap_size) \
+    (heap_size < 2048    \
+        ? 4096           \
+        : 2 * heap_size  \
+    )
+
+typedef void CDataFinalizer(void *);
+
+typedef struct CHeapItem {
+    /// Payload.
+    void * data;
+
+    /// Size of the item, in bytes.
+    /// This does not have to be a precise size. It is used to assess
+    /// whether the heap needs garbage collection.
+    size_t size;
+
+    /// Finalizer that will be called on the payload pointer.
+    /// Its job is to deallocate all associated resources,
+    /// including the memory pointed to by `data` (if any).
+    CDataFinalizer * finalizer;
+
+    /// The mark bit set by the FP heap traversal,
+    /// cleared by C heap sweep.
+    bool is_used;
+
+    /// Next item in the C heap.
+    struct CHeapItem * next;
+
+    /// Pointer to the previous next-pointer.
+    struct CHeapItem ** prev_next;
+} CHeapItem;
+
+typedef struct CHeap {
+    /// The first item in the heap. NULL if the heap is empty.
+    CHeapItem * first;
+
+    /// Total size of the heap. (Sum of sizes of items.)
+    /// This may not be a precise size since individual items'
+    /// sizes may be just estimates.
+    size_t size;
+
+    /// When heap reaches this size, GC will be triggered.
+    size_t gc_trigger_size;
+} CHeap;
+
+/// Create a C heap.
+void c_heap_init(CHeap * c_heap);
+
+/// Destroy the given C heap. Will not deallocate the given pointer.
+/// Will call finalizers & deallocate all blocks in the heap.
+void c_heap_destroy(CHeap * c_heap);
+
+/// Insert the given item into the heap if it's not there yet.
+/// The VM pointer is needed because this operation may trigger GC.
+void c_heap_insert_if_needed(struct VM * vm, CHeap * c_heap, CHeapItem * item);
+
+/// Mark the given item as used.
+void c_heap_mark_item(CHeapItem * item);
+
+/// Sweep the C heap, finalizing and freeing unused blocks.
+void c_heap_sweep(CHeap * c_heap);
+
+/// Create a C heap item from its payload, size estimate, and finalizer.
+/// The size does not have to be precise but it should roughly reflect
+/// how big the item is for GC to work effectively.
+CHeapItem * c_heap_create_item(void * data, size_t size, CDataFinalizer * finalizer);
+
+/* *** Idris heap **
+ * Objects without finalizers. Cheney-collected.
+ */
 
 typedef struct {
     char*  next;   // Next allocated chunk. Should always (heap <= next < end).
diff --git a/rts/idris_rts.c b/rts/idris_rts.c
--- a/rts/idris_rts.c
+++ b/rts/idris_rts.c
@@ -35,6 +35,8 @@
 
     alloc_heap(&(vm->heap), heap_size, heap_size, NULL);
 
+    c_heap_init(&vm->c_heap);
+
     vm->ret = NULL;
     vm->reg1 = NULL;
 #ifdef HAS_PTHREAD
@@ -80,6 +82,7 @@
 
 VM* get_vm(void) {
 #ifdef HAS_PTHREAD
+    init_threadkeys();
     return pthread_getspecific(vm_key);
 #else
     return global_vm;
@@ -90,10 +93,17 @@
     terminate(vm);
 }
 
-void init_threadkeys() {
 #ifdef HAS_PTHREAD
+void create_key() {
     pthread_key_create(&vm_key, (void*)free_key);
+}
 #endif
+
+void init_threadkeys() {
+#ifdef HAS_PTHREAD
+    static pthread_once_t key_once = PTHREAD_ONCE_INIT;
+    pthread_once(&key_once, create_key);
+#endif
 }
 
 void init_threaddata(VM *vm) {
@@ -116,6 +126,7 @@
 #endif
     free(vm->valstack);
     free_heap(&(vm->heap));
+    c_heap_destroy(&(vm->c_heap));
 #ifdef HAS_PTHREAD
     pthread_mutex_destroy(&(vm -> inbox_lock));
     pthread_mutex_destroy(&(vm -> inbox_block));
@@ -132,6 +143,17 @@
     return stats;
 }
 
+CData cdata_allocate(size_t size, CDataFinalizer finalizer)
+{
+    void * data = (void *) malloc(size);
+    return cdata_manage(data, size, finalizer);
+}
+
+CData cdata_manage(void * data, size_t size, CDataFinalizer finalizer)
+{
+    return c_heap_create_item(data, size, finalizer);
+}
+
 void idris_requireAlloc(size_t size) {
 #ifdef HAS_PTHREAD
     VM* vm = pthread_getspecific(vm_key);
@@ -166,7 +188,7 @@
 
 void* idris_alloc(size_t size) {
     Closure* cl = (Closure*) allocate(sizeof(Closure)+size, 0);
-    SETTY(cl, RAWDATA);
+    SETTY(cl, CT_RAWDATA);
     cl->info.size = size;
     return (void*)cl+sizeof(Closure);
 }
@@ -231,7 +253,7 @@
 void* allocCon(VM* vm, int arity, int outer) {
     Closure* cl = allocate(vm, sizeof(Closure) + sizeof(VAL)*arity,
                                outer);
-    SETTY(cl, CON);
+    SETTY(cl, CT_CON);
 
     cl -> info.c.arity = arity;
 //    cl -> info.c.tag = 42424242;
@@ -242,7 +264,7 @@
 
 VAL MKFLOAT(VM* vm, double val) {
     Closure* cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, FLOAT);
+    SETTY(cl, CT_FLOAT);
     cl -> info.f = val;
     return cl;
 }
@@ -256,7 +278,7 @@
     }
     Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) +
                            sizeof(char)*len, 0);
-    SETTY(cl, STRING);
+    SETTY(cl, CT_STRING);
     cl -> info.str = (char*)cl + sizeof(Closure);
     if (str == NULL) {
         cl->info.str = NULL;
@@ -272,9 +294,25 @@
     return (root->str->info.str + root->offset);
 }
 
+VAL MKCDATA(VM* vm, CHeapItem * item) {
+    c_heap_insert_if_needed(vm, &vm->c_heap, item);
+    Closure* cl = allocate(sizeof(Closure), 0);
+    SETTY(cl, CT_CDATA);
+    cl->info.c_heap_item = item;
+    return cl;
+}
+
+VAL MKCDATAc(VM* vm, CHeapItem * item) {
+    c_heap_insert_if_needed(vm, &vm->c_heap, item);
+    Closure* cl = allocate(sizeof(Closure), 1);
+    SETTY(cl, CT_CDATA);
+    cl->info.c_heap_item = item;
+    return cl;
+}
+
 VAL MKPTR(VM* vm, void* ptr) {
     Closure* cl = allocate(sizeof(Closure), 0);
-    SETTY(cl, PTR);
+    SETTY(cl, CT_PTR);
     cl -> info.ptr = ptr;
     return cl;
 }
@@ -282,7 +320,7 @@
 VAL MKMPTR(VM* vm, void* ptr, size_t size) {
     Closure* cl = allocate(sizeof(Closure) +
                            sizeof(ManagedPtr) + size, 0);
-    SETTY(cl, MANAGEDPTR);
+    SETTY(cl, CT_MANAGEDPTR);
     cl->info.mptr = (ManagedPtr*)((char*)cl + sizeof(Closure));
     cl->info.mptr->data = (char*)cl + sizeof(Closure) + sizeof(ManagedPtr);
     memcpy(cl->info.mptr->data, ptr, size);
@@ -292,7 +330,7 @@
 
 VAL MKFLOATc(VM* vm, double val) {
     Closure* cl = allocate(sizeof(Closure), 1);
-    SETTY(cl, FLOAT);
+    SETTY(cl, CT_FLOAT);
     cl -> info.f = val;
     return cl;
 }
@@ -300,7 +338,7 @@
 VAL MKSTRc(VM* vm, char* str) {
     Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) +
                            sizeof(char)*strlen(str)+1, 1);
-    SETTY(cl, STRING);
+    SETTY(cl, CT_STRING);
     cl -> info.str = (char*)cl + sizeof(Closure);
 
     strcpy(cl -> info.str, str);
@@ -309,7 +347,7 @@
 
 VAL MKPTRc(VM* vm, void* ptr) {
     Closure* cl = allocate(sizeof(Closure), 1);
-    SETTY(cl, PTR);
+    SETTY(cl, CT_PTR);
     cl -> info.ptr = ptr;
     return cl;
 }
@@ -317,7 +355,7 @@
 VAL MKMPTRc(VM* vm, void* ptr, size_t size) {
     Closure* cl = allocate(sizeof(Closure) +
                            sizeof(ManagedPtr) + size, 1);
-    SETTY(cl, MANAGEDPTR);
+    SETTY(cl, CT_MANAGEDPTR);
     cl->info.mptr = (ManagedPtr*)((char*)cl + sizeof(Closure));
     cl->info.mptr->data = (char*)cl + sizeof(Closure) + sizeof(ManagedPtr);
     memcpy(cl->info.mptr->data, ptr, size);
@@ -327,28 +365,28 @@
 
 VAL MKB8(VM* vm, uint8_t bits8) {
     Closure* cl = allocate(sizeof(Closure), 1);
-    SETTY(cl, BITS8);
+    SETTY(cl, CT_BITS8);
     cl -> info.bits8 = bits8;
     return cl;
 }
 
 VAL MKB16(VM* vm, uint16_t bits16) {
     Closure* cl = allocate(sizeof(Closure), 1);
-    SETTY(cl, BITS16);
+    SETTY(cl, CT_BITS16);
     cl -> info.bits16 = bits16;
     return cl;
 }
 
 VAL MKB32(VM* vm, uint32_t bits32) {
     Closure* cl = allocate(sizeof(Closure), 1);
-    SETTY(cl, BITS32);
+    SETTY(cl, CT_BITS32);
     cl -> info.bits32 = bits32;
     return cl;
 }
 
 VAL MKB64(VM* vm, uint64_t bits64) {
     Closure* cl = allocate(sizeof(Closure), 1);
-    SETTY(cl, BITS64);
+    SETTY(cl, CT_BITS64);
     cl -> info.bits64 = bits64;
     return cl;
 }
@@ -390,18 +428,18 @@
         return;
     }
     switch(GETTY(v)) {
-    case CON:
+    case CT_CON:
         printf("%d[", TAG(v));
         for(i = 0; i < ARITY(v); ++i) {
             dumpVal(v->info.c.args[i]);
         }
         printf("] ");
         break;
-    case STRING:
+    case CT_STRING:
         printf("STR[%s]", v->info.str);
         break;
-    case FWD:
-        printf("FWD ");
+    case CT_FWD:
+        printf("CT_FWD ");
         dumpVal((VAL)(v->info.ptr));
         break;
     default:
@@ -434,6 +472,24 @@
     return MKINT(0);
 }
 
+VAL idris_peekDouble(VM* vm, VAL ptr, VAL offset) {
+    return MKFLOAT(vm, *(double*)(GETPTR(ptr) + GETINT(offset)));
+}
+
+VAL idris_pokeDouble(VAL ptr, VAL offset, VAL data) {
+    *(double*)(GETPTR(ptr) + GETINT(offset)) = GETFLOAT(data);
+    return MKINT(0);
+}
+
+VAL idris_peekSingle(VM* vm, VAL ptr, VAL offset) {
+    return MKFLOAT(vm, *(float*)(GETPTR(ptr) + GETINT(offset)));
+}
+
+VAL idris_pokeSingle(VAL ptr, VAL offset, VAL data) {
+    *(float*)(GETPTR(ptr) + GETINT(offset)) = GETFLOAT(data);
+    return MKINT(0);
+}
+
 void idris_memmove(void* dest, void* src, i_int dest_offset, i_int src_offset, i_int size) {
     memmove(dest + dest_offset, src + src_offset, size);
 }
@@ -441,7 +497,7 @@
 VAL idris_castIntStr(VM* vm, VAL i) {
     int x = (int) GETINT(i);
     Closure* cl = allocate(sizeof(Closure) + sizeof(char)*16, 0);
-    SETTY(cl, STRING);
+    SETTY(cl, CT_STRING);
     cl -> info.str = (char*)cl + sizeof(Closure);
     sprintf(cl -> info.str, "%d", x);
     return cl;
@@ -452,25 +508,25 @@
     ClosureType ty = i->ty;
 
     switch (ty) {
-    case BITS8:
+    case CT_BITS8:
         // max length 8 bit unsigned int str 3 chars (256)
         cl = allocate(sizeof(Closure) + sizeof(char)*4, 0);
         cl->info.str = (char*)cl + sizeof(Closure);
         sprintf(cl->info.str, "%" PRIu8, (uint8_t)i->info.bits8);
         break;
-    case BITS16:
+    case CT_BITS16:
         // max length 16 bit unsigned int str 5 chars (65,535)
         cl = allocate(sizeof(Closure) + sizeof(char)*6, 0);
         cl->info.str = (char*)cl + sizeof(Closure);
         sprintf(cl->info.str, "%" PRIu16, (uint16_t)i->info.bits16);
         break;
-    case BITS32:
+    case CT_BITS32:
         // max length 32 bit unsigned int str 10 chars (4,294,967,295)
         cl = allocate(sizeof(Closure) + sizeof(char)*11, 0);
         cl->info.str = (char*)cl + sizeof(Closure);
         sprintf(cl->info.str, "%" PRIu32, (uint32_t)i->info.bits32);
         break;
-    case BITS64:
+    case CT_BITS64:
         // max length 64 bit unsigned int str 20 chars (18,446,744,073,709,551,615)
         cl = allocate(sizeof(Closure) + sizeof(char)*21, 0);
         cl->info.str = (char*)cl + sizeof(Closure);
@@ -481,7 +537,7 @@
         exit(EXIT_FAILURE);
     }
 
-    SETTY(cl, STRING);
+    SETTY(cl, CT_STRING);
     return cl;
 }
 
@@ -496,7 +552,7 @@
 
 VAL idris_castFloatStr(VM* vm, VAL i) {
     Closure* cl = allocate(sizeof(Closure) + sizeof(char)*32, 0);
-    SETTY(cl, STRING);
+    SETTY(cl, CT_STRING);
     cl -> info.str = (char*)cl + sizeof(Closure);
     snprintf(cl -> info.str, 32, "%.16g", GETFLOAT(i));
     return cl;
@@ -512,7 +568,7 @@
     // dumpVal(l);
     // printf("\n");
     Closure* cl = allocate(sizeof(Closure) + strlen(ls) + strlen(rs) + 1, 0);
-    SETTY(cl, STRING);
+    SETTY(cl, CT_STRING);
     cl -> info.str = (char*)cl + sizeof(Closure);
     strcpy(cl -> info.str, ls);
     strcat(cl -> info.str, rs);
@@ -558,7 +614,7 @@
 
 VAL MKSTROFFc(VM* vm, StrOffset* off) {
     Closure* cl = allocate(sizeof(Closure) + sizeof(StrOffset), 1);
-    SETTY(cl, STROFFSET);
+    SETTY(cl, CT_STROFFSET);
     cl->info.str_offset = (StrOffset*)((char*)cl + sizeof(Closure));
 
     cl->info.str_offset->str = off->str;
@@ -572,7 +628,7 @@
     // gc moves str
     if (space(vm, sizeof(Closure) + sizeof(StrOffset))) {
         Closure* cl = allocate(sizeof(Closure) + sizeof(StrOffset), 0);
-        SETTY(cl, STROFFSET);
+        SETTY(cl, CT_STROFFSET);
         cl->info.str_offset = (StrOffset*)((char*)cl + sizeof(Closure));
 
         int offset = 0;
@@ -600,7 +656,7 @@
     if ((xval & 0x80) == 0) { // ASCII char
         Closure* cl = allocate(sizeof(Closure) +
                                strlen(xstr) + 2, 0);
-        SETTY(cl, STRING);
+        SETTY(cl, CT_STRING);
         cl -> info.str = (char*)cl + sizeof(Closure);
         cl -> info.str[0] = (char)(GETINT(x));
         strcpy(cl -> info.str+1, xstr);
@@ -608,7 +664,7 @@
     } else {
         char *init = idris_utf8_fromChar(xval);
         Closure* cl = allocate(sizeof(Closure) + strlen(init) + strlen(xstr) + 1, 0);
-        SETTY(cl, STRING);
+        SETTY(cl, CT_STRING);
         cl -> info.str = (char*)cl + sizeof(Closure);
         strcpy(cl -> info.str, init);
         strcat(cl -> info.str, xstr);
@@ -626,7 +682,7 @@
     char *start = idris_utf8_advance(GETSTR(str), GETINT(offset));
     char *end = idris_utf8_advance(start, GETINT(length));
     Closure* newstr = allocate(sizeof(Closure) + (end - start) +1, 0);
-    SETTY(newstr, STRING);
+    SETTY(newstr, CT_STRING);
     newstr -> info.str = (char*)newstr + sizeof(Closure);
     memcpy(newstr -> info.str, start, end - start);
     *(newstr -> info.str + (end - start) + 1) = '\0';
@@ -637,7 +693,7 @@
     char *xstr = GETSTR(str);
     Closure* cl = allocate(sizeof(Closure) +
                            strlen(xstr) + 1, 0);
-    SETTY(cl, STRING);
+    SETTY(cl, CT_STRING);
     cl->info.str = (char*)cl + sizeof(Closure);
     idris_utf8_rev(xstr, cl->info.str);
     return cl;
@@ -720,7 +776,7 @@
         return x;
     }
     switch(GETTY(x)) {
-    case CON:
+    case CT_CON:
         ar = CARITY(x);
         if (ar == 0 && CTAG(x) < 256) { // globally allocated
             cl = x;
@@ -734,34 +790,34 @@
             }
         }
         break;
-    case FLOAT:
+    case CT_FLOAT:
         cl = MKFLOATc(vm, x->info.f);
         break;
-    case STRING:
+    case CT_STRING:
         cl = MKSTRc(vm, x->info.str);
         break;
-    case BIGINT:
+    case CT_BIGINT:
         cl = MKBIGMc(vm, x->info.ptr);
         break;
-    case PTR:
+    case CT_PTR:
         cl = MKPTRc(vm, x->info.ptr);
         break;
-    case MANAGEDPTR:
+    case CT_MANAGEDPTR:
         cl = MKMPTRc(vm, x->info.mptr->data, x->info.mptr->size);
         break;
-    case BITS8:
+    case CT_BITS8:
         cl = idris_b8CopyForGC(vm, x);
         break;
-    case BITS16:
+    case CT_BITS16:
         cl = idris_b16CopyForGC(vm, x);
         break;
-    case BITS32:
+    case CT_BITS32:
         cl = idris_b32CopyForGC(vm, x);
         break;
-    case BITS64:
+    case CT_BITS64:
         cl = idris_b64CopyForGC(vm, x);
         break;
-    case RAWDATA:
+    case CT_RAWDATA:
         {
             size_t size = x->info.size + sizeof(Closure);
             cl = allocate(size, 0);
@@ -971,7 +1027,7 @@
     nullary_cons = malloc(256 * sizeof(VAL));
     for(i = 0; i < 256; ++i) {
         cl = malloc(sizeof(Closure));
-        SETTY(cl, CON);
+        SETTY(cl, CT_CON);
         cl->info.c.tag_arity = i << 8;
         nullary_cons[i] = cl;
     }
diff --git a/rts/idris_rts.h b/rts/idris_rts.h
--- a/rts/idris_rts.h
+++ b/rts/idris_rts.h
@@ -25,9 +25,9 @@
 
 // Closures
 typedef enum {
-    CON, INT, BIGINT, FLOAT, STRING, STROFFSET,
-    BITS8, BITS16, BITS32, BITS64, UNIT, PTR, FWD,
-    MANAGEDPTR, RAWDATA
+    CT_CON, CT_INT, CT_BIGINT, CT_FLOAT, CT_STRING, CT_STROFFSET,
+    CT_BITS8, CT_BITS16, CT_BITS32, CT_BITS64, CT_UNIT, CT_PTR, CT_FWD,
+    CT_MANAGEDPTR, CT_RAWDATA, CT_CDATA
 } ClosureType;
 
 typedef struct Closure *VAL;
@@ -67,20 +67,21 @@
         uint32_t bits32;
         uint64_t bits64;
         ManagedPtr* mptr;
+        CHeapItem* c_heap_item;
         size_t size;
     } info;
 } Closure;
 
-struct VM_t;
+struct VM;
 
 struct Msg_t {
-    struct VM_t* sender;
+    struct VM* sender;
     VAL msg;
 };
 
 typedef struct Msg_t Msg;
 
-struct VM_t {
+struct VM {
     int active; // 0 if no longer running; keep for message passing
                 // TODO: If we're going to have lots of concurrent threads,
                 // we really need to be cleverer than this!
@@ -90,6 +91,7 @@
     VAL* valstack_base;
     VAL* stack_max;
 
+    CHeap c_heap;
     Heap heap;
 #ifdef HAS_PTHREAD
     pthread_mutex_t inbox_lock;
@@ -110,8 +112,38 @@
     VAL reg1;
 };
 
-typedef struct VM_t VM;
+typedef struct VM VM;
 
+
+/* C data interface: allocation on the C heap.
+ *
+ * Although not enforced in code, CData is meant to be opaque
+ * and non-RTS code (such as libraries or C bindings) should
+ * access only its (void *) field called "data".
+ *
+ * Feel free to mutate cd->data; the heap does not care
+ * about its particular value. However, keep in mind
+ * that it must not break Idris's referential transparency.
+ *
+ * If you call cdata_allocate or cdata_manage, the resulting
+ * CData object *must* be returned from your FFI function so
+ * that it is inserted in the C heap. Otherwise the memory
+ * will be leaked.
+ */
+
+/// C data block. Contains (void * data).
+typedef CHeapItem * CData;
+
+/// Allocate memory, returning the corresponding C data block.
+CData cdata_allocate(size_t size, CDataFinalizer * finalizer);
+
+/// Wrap a pointer as a C data block.
+/// The size should be an estimate of how much memory, in bytes,
+/// is associated with the pointer. This estimate need not be absolutely precise
+/// but it is necessary for GC to work effectively.
+CData cdata_manage(void * data, size_t size, CDataFinalizer * finalizer);
+
+
 // Create a new VM
 VM* init_vm(int stack_size, size_t heap_size,
             int max_threads);
@@ -150,16 +182,17 @@
 #define GETPTR(x) (((VAL)(x))->info.ptr)
 #define GETMPTR(x) (((VAL)(x))->info.mptr->data)
 #define GETFLOAT(x) (((VAL)(x))->info.f)
+#define GETCDATA(x) (((VAL)(x))->info.c_heap_item)
 
 #define GETBITS8(x) (((VAL)(x))->info.bits8)
 #define GETBITS16(x) (((VAL)(x))->info.bits16)
 #define GETBITS32(x) (((VAL)(x))->info.bits32)
 #define GETBITS64(x) (((VAL)(x))->info.bits64)
 
-#define TAG(x) (ISINT(x) || x == NULL ? (-1) : ( GETTY(x) == CON ? (x)->info.c.tag_arity >> 8 : (-1)) )
-#define ARITY(x) (ISINT(x) || x == NULL ? (-1) : ( GETTY(x) == CON ? (x)->info.c.tag_arity & 0x000000ff : (-1)) )
+#define TAG(x) (ISINT(x) || x == NULL ? (-1) : ( GETTY(x) == CT_CON ? (x)->info.c.tag_arity >> 8 : (-1)) )
+#define ARITY(x) (ISINT(x) || x == NULL ? (-1) : ( GETTY(x) == CT_CON ? (x)->info.c.tag_arity & 0x000000ff : (-1)) )
 
-// Already checked it's a CON
+// Already checked it's a CT_CON
 #define CTAG(x) (((x)->info.c.tag_arity) >> 8)
 #define CARITY(x) ((x)->info.c.tag_arity & 0x000000ff)
 
@@ -179,7 +212,7 @@
 #define MKINT(x) ((void*)((x)<<1)+1)
 #define GETINT(x) ((i_int)(x)>>1)
 #define ISINT(x) ((((i_int)x)&1) == 1)
-#define ISSTR(x) (GETTY(x) == STRING)
+#define ISSTR(x) (GETTY(x) == CT_STRING)
 
 #define INTOP(op,x,y) MKINT((i_int)((((i_int)x)>>1) op (((i_int)y)>>1)))
 #define UINTOP(op,x,y) MKINT((i_int)((((uintptr_t)x)>>1) op (((uintptr_t)y)>>1)))
@@ -210,6 +243,7 @@
 VAL MKB16(VM* vm, uint16_t b);
 VAL MKB32(VM* vm, uint32_t b);
 VAL MKB64(VM* vm, uint64_t b);
+VAL MKCDATA(VM* vm, CHeapItem * item);
 
 // following versions don't take a lock when allocating
 VAL MKFLOATc(VM* vm, double val);
@@ -217,6 +251,7 @@
 VAL MKSTRc(VM* vm, char* str);
 VAL MKPTRc(VM* vm, void* ptr);
 VAL MKMPTRc(VM* vm, void* ptr, size_t size);
+VAL MKCDATAc(VM* vm, CHeapItem * item);
 
 char* GETSTROFF(VAL stroff);
 
@@ -248,12 +283,12 @@
 
 #define allocCon(cl, vm, t, a, o) \
   cl = allocate(sizeof(Closure) + sizeof(VAL)*a, o); \
-  SETTY(cl, CON); \
+  SETTY(cl, CT_CON); \
   cl->info.c.tag_arity = ((t) << 8) | (a);
 
 #define updateCon(cl, old, t, a) \
   cl = old; \
-  SETTY(cl, CON); \
+  SETTY(cl, CT_CON); \
   cl->info.c.tag_arity = ((t) << 8) | (a);
 
 #define NULL_CON(x) nullary_cons[x]
@@ -313,6 +348,10 @@
 
 VAL idris_peekPtr(VM* vm, VAL ptr, VAL offset);
 VAL idris_pokePtr(VAL ptr, VAL offset, VAL data);
+VAL idris_peekDouble(VM* vm, VAL ptr, VAL offset);
+VAL idris_pokeDouble(VAL ptr, VAL offset, VAL data);
+VAL idris_peekSingle(VM* vm, VAL ptr, VAL offset);
+VAL idris_pokeSingle(VAL ptr, VAL offset, VAL data);
 
 // String primitives
 VAL idris_concat(VM* vm, VAL l, VAL r);
diff --git a/src/IRTS/CodegenC.hs b/src/IRTS/CodegenC.hs
--- a/src/IRTS/CodegenC.hs
+++ b/src/IRTS/CodegenC.hs
@@ -75,6 +75,7 @@
              libFlags <- getLibFlags
              incFlags <- getIncFlags
              envFlags <- getEnvFlags
+             let stackFlag = if isWindows then ["-Wl,--stack,16777216"] else []
              let args = [gccDbg dbg] ++
                         gccFlags iface ++
                         -- # Any flags defined here which alter the RTS API must also be added to config.mk
@@ -85,7 +86,7 @@
                         (if not iface then libFlags else []) ++
                         incFlags ++
                         (if not iface then libs else []) ++
-                        flags ++
+                        flags ++ stackFlag ++
                         ["-o", out]
 --              putStrLn (show args)
              exit <- rawSystem comp args
@@ -354,6 +355,7 @@
     | c == sUN "C_Float" = FArith ATFloat
     | c == sUN "C_Ptr" = FPtr
     | c == sUN "C_MPtr" = FManagedPtr
+    | c == sUN "C_CData" = FCData
     | c == sUN "C_Unit" = FUnit
 toFType (FApp c [_,ity])
     | c == sUN "C_IntT" = FArith (toAType ity)
@@ -378,6 +380,7 @@
 c_irts FPtr l x = l ++ "MKPTR(vm, " ++ x ++ ")"
 c_irts FManagedPtr l x = l ++ "MKMPTR(vm, " ++ x ++ ")"
 c_irts (FArith ATFloat) l x = l ++ "MKFLOAT(vm, " ++ x ++ ")"
+c_irts FCData l x = l ++ "MKCDATA(vm, " ++ x ++ ")"
 c_irts FAny l x = l ++ x
 c_irts FFunction l x = error "Return of function from foreign call is not supported"
 c_irts FFunctionIO l x = error "Return of function from foreign call is not supported"
@@ -391,6 +394,7 @@
 irts_c FPtr x = "GETPTR(" ++ x ++ ")"
 irts_c FManagedPtr x = "GETMPTR(" ++ x ++ ")"
 irts_c (FArith ATFloat) x = "GETFLOAT(" ++ x ++ ")"
+irts_c FCData x = "GETCDATA(" ++ x ++ ")"
 irts_c FAny x = x
 irts_c FFunctionIO x = wrapped x
 irts_c FFunction x = wrapped x
@@ -649,9 +653,20 @@
     = v ++ "idris_peekPtr(vm," ++ creg p ++ "," ++ creg o ++")"
 doOp v (LExternal pk) [_, p, o, x] | pk == sUN "prim__pokePtr"
     = v ++ "idris_pokePtr(" ++ creg p ++ "," ++ creg o ++ "," ++ creg x ++ ")"
+doOp v (LExternal pk) [_, p, o, x] | pk == sUN "prim__pokeDouble"
+    = v ++ "idris_pokeDouble(" ++ creg p ++ "," ++ creg o ++ "," ++ creg x ++ ")"
+doOp v (LExternal pk) [_, p, o] | pk == sUN "prim__peekDouble"
+    = v ++ "idris_peekDouble(vm," ++ creg p ++ "," ++ creg o ++")"
+doOp v (LExternal pk) [_, p, o, x] | pk == sUN "prim__pokeSingle"
+    = v ++ "idris_pokeSingle(" ++ creg p ++ "," ++ creg o ++ "," ++ creg x ++ ")"
+doOp v (LExternal pk) [_, p, o] | pk == sUN "prim__peekSingle"
+    = v ++ "idris_peekSingle(vm," ++ creg p ++ "," ++ creg o ++")"
 doOp v (LExternal pk) [] | pk == sUN "prim__sizeofPtr"
     = v ++ "MKINT(sizeof(void*))"
-doOp v (LExternal mpt) [p] | mpt == sUN "prim__asPtr" = v ++ "MKPTR(vm, GETMPTR("++ creg p ++"))"
+doOp v (LExternal mpt) [p] | mpt == sUN "prim__asPtr"
+    = v ++ "MKPTR(vm, GETMPTR("++ creg p ++"))"
+doOp v (LExternal offs) [p, n] | offs == sUN "prim__ptrOffset"
+    = v ++ "MKPTR(vm, GETPTR(" ++ creg p ++ ") + GETINT(" ++ creg n ++ "))"
 doOp _ op args = error $ "doOp not implemented (" ++ show (op, args) ++ ")"
 
 
@@ -790,19 +805,13 @@
                           (if ret /= "void" then indent 1 ++ ret ++ " ret;\n" else "") ++
                           indent 1 ++ "VM* vm = get_vm();\n" ++
                           indent 1 ++ "if (vm == NULL) {\n" ++
-                          indent 2 ++ "fprintf(stderr, \"No vm available in callback.\");\n" ++
-                          indent 2 ++ "exit(-1);\n" ++
+                          indent 2 ++ "vm = idris_vm();\n" ++
                           indent 1 ++ "}\n" ++
                           indent 1 ++ "INITFRAME;\n" ++
                           indent 1 ++ "RESERVE(" ++ show (len + 1) ++ ");\n" ++
                           indent 1 ++ "allocCon(REG1, vm, " ++ show tag ++ ",0 , 0);\n" ++
                           indent 1 ++ "TOP(0) = REG1;\n" ++
-
-                          push 1 argList ++
-                          indent 1 ++ "STOREOLD;\n" ++
-                          indent 1 ++ "BASETOP(0);\n" ++
-                          indent 1 ++ "ADDTOP(" ++ show (len + 1) ++ ");\n" ++
-                          indent 1 ++ "CALL(_idris__123_APPLY0_125_);\n" ++
+                          applyArgs argList ++
                           if ret /= "void"
                             then indent 1 ++ "ret = " ++ irts_c (toFType ft) "RVAL" ++ ";\n"
                                           ++ indent 1 ++ "return ret;\n}\n\n"
@@ -811,6 +820,19 @@
                         (ret, ft) = rty desc
                         argList = zip (args desc) [0..]
                         len = length argList
+
+                        applyArgs (x:y:xs) = push 1 [x] ++
+                                            indent 1 ++ "STOREOLD;\n" ++
+                                            indent 1 ++ "BASETOP(0);\n" ++
+                                            indent 1 ++ "ADDTOP(2);\n" ++
+                                            indent 1 ++ "CALL(_idris__123_APPLY0_125_);\n" ++
+                                            indent 1 ++ "TOP(0)=REG1;\n" ++
+                                            applyArgs (y:xs)
+                        applyArgs x = push 1 x ++
+                                      indent 1 ++ "STOREOLD;\n" ++
+                                      indent 1 ++ "BASETOP(0);\n" ++
+                                      indent 1 ++ "ADDTOP(" ++ show (length x + 1) ++ ");\n" ++
+                                      indent 1 ++ "CALL(_idris__123_APPLY0_125_);\n"
                         renderArgs [] = "void"
                         renderArgs [((s, _), n)] = s ++ " a" ++ (show n)
                         renderArgs (((s, _), n):xs) = s ++ " a" ++ (show n) ++ ", " ++
diff --git a/src/IRTS/Lang.hs b/src/IRTS/Lang.hs
--- a/src/IRTS/Lang.hs
+++ b/src/IRTS/Lang.hs
@@ -17,10 +17,11 @@
   deriving (Show, Eq)
 
 -- ASSUMPTION: All variable bindings have unique names here
+-- Constructors commented as lifted are not present in the LIR provided to the different backends.
 data LExp = LV LVar
           | LApp Bool LExp [LExp] -- True = tail call
           | LLazyApp Name [LExp] -- True = tail call
-          | LLazyExp LExp
+          | LLazyExp LExp -- lifted out before compiling
           | LForce LExp -- make sure Exp is evaluted
           | LLet Name LExp LExp -- name just for pretty printing
           | LLam [Name] LExp -- lambda, lifted out before compiling
@@ -99,6 +100,7 @@
            | FUnit
            | FPtr
            | FManagedPtr
+           | FCData
            | FAny
   deriving (Show, Eq)
 
@@ -132,7 +134,7 @@
 
 lname (NS n x) i = NS (lname n i) x
 lname (UN n) i = MN i n
-lname x i = sMN i (show x ++ "_lam")
+lname x i = sMN i (showCG x ++ "_lam")
 
 liftAll :: [(Name, LDecl)] -> [(Name, LDecl)]
 liftAll xs = concatMap (\ (x, d) -> lambdaLift x d) xs
@@ -215,7 +217,7 @@
     -- Keep track of 'updatable' names in the state, i.e. names whose heap
     -- entry may be reused, along with the arity which was there
     findUp :: LExp -> State [(Name, Int)] LExp
-    findUp (LApp t (LV (Glob n)) as) 
+    findUp (LApp t (LV (Glob n)) as)
        | Just (LConstructor _ i ar) <- lookupCtxtExact n defs,
          ar == length as
           = findUp (LCon Nothing i n as)
@@ -241,7 +243,7 @@
     findUp (LOp o es) = LOp o <$> mapM findUp es
     findUp (LCase Updatable e@(LV (Glob n)) as)
            = LCase Updatable e <$> mapM (doUpAlt n) as
-    findUp (LCase t e as) 
+    findUp (LCase t e as)
            = LCase t <$> findUp e <*> mapM findUpAlt as
     findUp t = return t
 
@@ -252,7 +254,7 @@
     findUpAlt (LConstCase i rhs) = LConstCase i <$> findUp rhs
     findUpAlt (LDefaultCase rhs) = LDefaultCase <$> findUp rhs
 
-    doUpAlt n (LConCase i t args rhs) 
+    doUpAlt n (LConCase i t args rhs)
            = do avail <- get
                 put ((n, length args) : avail)
                 rhs' <- findUp rhs
@@ -282,7 +284,7 @@
 usedIn env (LLam ns e) = usedIn (env \\ ns) e
 usedIn env (LCon v i n args) = let rest = concatMap (usedIn env) args in
                                    case v of
-                                      Nothing -> rest 
+                                      Nothing -> rest
                                       Just (Glob n) -> usedArg env n ++ rest
 usedIn env (LProj t i) = usedIn env t
 usedIn env (LCase up e alts) = usedIn env e ++ concatMap (usedInA env) alts
@@ -329,7 +331,7 @@
                        Updatable -> "! "
          fmt [] = ""
          fmt [alt]
-            = "\t" ++ ind ++ "| " ++ showAlt env (ind ++ "    ") alt 
+            = "\t" ++ ind ++ "| " ++ showAlt env (ind ++ "    ") alt
          fmt (alt:as)
             = "\t" ++ ind ++ "| " ++ showAlt env (ind ++ ".   ") alt
                 ++ "\n" ++ fmt as
diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs
--- a/src/Idris/AbsSyntax.hs
+++ b/src/Idris/AbsSyntax.hs
@@ -1593,7 +1593,7 @@
     -- binding
     -- Not the function position, but do everything else...
     implNamesIn uv (PApp fc f args) = concatMap (implNamesIn uv . getTm) args
-    implNamesIn uv t = namesIn uv ist t
+    implNamesIn uv t = implicitNamesIn (map fst uv) ist t
 
     imps top env ty@(PApp _ f as)
        = do (decls, ns) <- get
diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs
--- a/src/Idris/AbsSyntaxTree.hs
+++ b/src/Idris/AbsSyntaxTree.hs
@@ -775,6 +775,9 @@
 data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
                        | RClausesInstrs Name [([(Name, Term)], Term, Term)]
                        | RAddInstance Name Name
+                       | RDatatypeDeclInstrs Name [PArg]
+                       | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
+                         -- ^ Datatype, constructors
 
 -- | For elaborator state
 data EState = EState {
diff --git a/src/Idris/Core/Elaborate.hs b/src/Idris/Core/Elaborate.hs
--- a/src/Idris/Core/Elaborate.hs
+++ b/src/Idris/Core/Elaborate.hs
@@ -139,13 +139,19 @@
 execElab :: aux -> Elab' aux a -> ProofState -> TC (ElabState aux)
 execElab a e ps = execStateT e (ES (ps, a) "" Nothing)
 
-initElaborator :: Name -> Context -> Ctxt TypeInfo -> Type -> ProofState
+initElaborator :: Name -- ^ the name of what's to be elaborated
+               -> Context -- ^ the current global context
+               -> Ctxt TypeInfo -- ^ the value of the idris_datatypes field of IState
+               -> Int -- ^ the value of the idris_name field of IState
+               -> Type -- ^ the goal type
+               -> ProofState
 initElaborator = newProof
 
-elaborate :: Context -> Ctxt TypeInfo -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)
-elaborate ctxt datatypes n ty d elab = do let ps = initElaborator n ctxt datatypes ty
-                                          (a, ES ps' str _) <- runElab d elab ps
-                                          return $! (a, str)
+elaborate :: Context -> Ctxt TypeInfo -> Int -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)
+elaborate ctxt datatypes globalNames n ty d elab =
+  do let ps = initElaborator n ctxt datatypes globalNames ty
+     (a, ES ps' str _) <- runElab d elab ps
+     return $! (a, str)
 
 -- | Modify the auxiliary state
 updateAux :: (aux -> aux) -> Elab' aux ()
@@ -209,6 +215,14 @@
 set_datatypes :: Ctxt TypeInfo -> Elab' aux ()
 set_datatypes ds = do ES (p, a) logs prev <- get
                       put (ES (p { datatypes = ds }, a) logs prev)
+
+get_global_nextname :: Elab' aux Int
+get_global_nextname = do ES (ps, _) _ _ <- get
+                         return (global_nextname ps)
+
+set_global_nextname :: Int -> Elab' aux ()
+set_global_nextname i = do ES (ps, a) logs prev <- get
+                           put $ ES (ps { global_nextname = i}, a) logs prev
 
 -- | get the proof term
 get_term :: Elab' aux Term
diff --git a/src/Idris/Core/Evaluate.hs b/src/Idris/Core/Evaluate.hs
--- a/src/Idris/Core/Evaluate.hs
+++ b/src/Idris/Core/Evaluate.hs
@@ -13,7 +13,7 @@
                 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
                 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
                 mapDefCtxt, 
-                lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
+                lookupTotal, lookupTotalExact, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
                 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
                 isUniverse) where
 
@@ -1082,6 +1082,10 @@
 
 lookupTotal :: Name -> Context -> [Totality]
 lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)
+  where mkt (d, a, t, m) = t
+
+lookupTotalExact :: Name -> Context -> Maybe Totality
+lookupTotalExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)
   where mkt (d, a, t, m) = t
 
 lookupMetaInformation :: Name -> Context -> [MetaInformation]
diff --git a/src/Idris/Core/ProofState.hs b/src/Idris/Core/ProofState.hs
--- a/src/Idris/Core/ProofState.hs
+++ b/src/Idris/Core/ProofState.hs
@@ -25,7 +25,10 @@
 data ProofState = PS { thname   :: Name,
                        holes    :: [Name], -- ^ holes still to be solved
                        usedns   :: [Name], -- ^ used names, don't use again
-                       nextname :: Int,    -- ^ name supply
+                       nextname :: Int,    -- ^ name supply, for locally unique names
+                       global_nextname :: Int, -- ^ a mirror of the global name supply,
+                                               --   for generating things like type tags
+                                               --   in reflection
                        pterm    :: ProofTerm,   -- ^ current proof term
                        ptype    :: Type,   -- ^ original goal
                        dontunify :: [Name], -- ^ explicitly given by programmer, leave it
@@ -305,11 +308,16 @@
 addLog :: Monad m => String -> StateT TState m ()
 addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
 
-newProof :: Name -> Context -> Ctxt TypeInfo -> Type -> ProofState
-newProof n ctxt datatypes ty =
+newProof :: Name -- ^ the name of what's to be elaborated
+         -> Context -- ^ the current global context
+         -> Ctxt TypeInfo -- ^ the value of the idris_datatypes field of IState
+         -> Int -- ^ the value of the idris_name field of IState
+         -> Type -- ^ the goal type
+         -> ProofState
+newProof n ctxt datatypes globalNames ty =
   let h = holeName 0
       ty' = vToP ty
-  in PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')
+  in PS n [h] [] 1 globalNames (mkProofTerm (Bind h (Hole ty')
         (P Bound h ty'))) ty [] (h, []) [] []
         Nothing [] []
         [] [] [] []
diff --git a/src/Idris/Coverage.hs b/src/Idris/Coverage.hs
--- a/src/Idris/Coverage.hs
+++ b/src/Idris/Coverage.hs
@@ -334,11 +334,12 @@
              x -> return () -- stop if total
 checkAllCovering _ _ _ _ = return ()
 
--- Check if, in a given group of type declarations mut_ns,
+-- | Check if, in a given group of type declarations mut_ns,
 -- the constructor cn : ty is strictly positive,
 -- and update the context accordingly
-
-checkPositive :: [Name] -> (Name, Type) -> Idris Totality
+checkPositive :: [Name] -- ^ the group of type declarations
+              -> (Name, Type) -- ^ the constructor
+              -> Idris Totality
 checkPositive mut_ns (cn, ty')
     = do i <- getIState
          let ty = delazy' True (normalise (tt_ctxt i) [] ty')
@@ -381,8 +382,8 @@
             _ -> checkSizeChange n
   where
     checkLHS i (P _ fn _)
-        = case lookupTotal fn (tt_ctxt i) of
-               [Partial _] -> return (Partial (Other [fn]))
+        = case lookupTotalExact fn (tt_ctxt i) of
+               Just (Partial _) -> return (Partial (Other [fn]))
                _ -> Nothing
     checkLHS i (App _ f a) = mplus (checkLHS i f) (checkLHS i a)
     checkLHS _ _ = Nothing
@@ -596,8 +597,8 @@
 
       toJust (n, t) = Just t
 
-      getType n = case lookupTy n (tt_ctxt ist) of
-                       [ty] -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist
+      getType n = case lookupTyExact n (tt_ctxt ist) of
+                       Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist
 
       isInductive (P _ nty _) (P _ nty' _) =
           let co = case lookupCtxt nty (idris_datatypes ist) of
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
@@ -486,14 +486,15 @@
         i <- getIState
         let lhs = addImplPat i lhs_in
         -- if the LHS type checks, it is possible
-        case elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState
+        case elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState
                             (erun fc (buildTC i info ELHS [] fname
                                                 (allNamesIn lhs_in)
                                                 (infTerm lhs))) of
-            OK (ElabResult lhs' _ _ ctxt' newDecls highlights, _) ->
+            OK (ElabResult lhs' _ _ ctxt' newDecls highlights newGName, _) ->
                do setContext ctxt'
                   processTacticDecls info newDecls
                   sendHighlighting highlights
+                  updateIState $ \i -> i { idris_name = newGName }
                   let lhs_tm = orderPats (getInferTerm lhs')
                   case recheck ctxt' [] (forget lhs_tm) lhs_tm of
                        OK _ -> return True
@@ -587,8 +588,8 @@
         logElab 4 ("Fixed parameters: " ++ show params ++ " from " ++ showTmImpls lhs_in ++
                   "\n" ++ show (fn_ty, fn_is))
 
-        ((ElabResult lhs' dlhs [] ctxt' newDecls highlights, probs, inj), _) <-
-           tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState
+        ((ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, probs, inj), _) <-
+           tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState
                     (do res <- errAt "left hand side of " fname Nothing
                                  (erun fc (buildTC i info ELHS opts fname
                                           (allNamesIn lhs_in)
@@ -599,6 +600,7 @@
         setContext ctxt'
         processTacticDecls info newDecls
         sendHighlighting highlights
+        updateIState $ \i -> i { idris_name = newGName }
 
         when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)
 
@@ -670,14 +672,14 @@
         logElab 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs
         ctxt <- getContext -- new context with where block added
         logElab 5 "STARTING CHECK"
-        ((rhs', defer, holes, is, probs, ctxt', newDecls, highlights), _) <-
-           tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patRHS") clhsty initEState
+        ((rhs', defer, holes, is, probs, ctxt', newDecls, highlights, newGName), _) <-
+           tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patRHS") clhsty initEState
                     (do pbinds ist lhs_tm
                         -- proof search can use explicitly written names
                         mapM_ addPSname (allNamesIn lhs_in)
                         mapM_ setinj (nub (tcparams ++ inj))
                         setNextName
-                        (ElabResult _ _ is ctxt' newDecls highlights) <-
+                        (ElabResult _ _ is ctxt' newDecls highlights newGName) <-
                           errAt "right hand side of " fname (Just clhsty)
                                 (erun fc (build i winfo ERHS opts fname rhs))
                         errAt "right hand side of " fname (Just clhsty)
@@ -688,10 +690,11 @@
                                                      (map fst $ case_decls aux) ctxt tt) []
                         probs <- get_probs
                         hs <- get_holes
-                        return (tm, ds, hs, is, probs, ctxt', newDecls, highlights))
+                        return (tm, ds, hs, is, probs, ctxt', newDecls, highlights, newGName))
         setContext ctxt'
         processTacticDecls info newDecls
         sendHighlighting highlights
+        updateIState $ \i -> i { idris_name = newGName }
 
         when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)
 
@@ -838,8 +841,8 @@
                    propagateParams i params fn_ty (allNamesIn lhs_in)
                     (addImplPat i lhs_in)
         logElab 2 ("LHS: " ++ show lhs)
-        (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-
-            tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState
+        (ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, _) <-
+            tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState
               (errAt "left hand side of with in " fname Nothing
                 (erun fc (buildTC i info ELHS opts fname
                                   (allNamesIn lhs_in)
@@ -847,6 +850,7 @@
         setContext ctxt'
         processTacticDecls info newDecls
         sendHighlighting highlights
+        updateIState $ \i -> i { idris_name = newGName }
 
         ctxt <- getContext
         let lhs_tm = orderPats (getInferTerm lhs')
@@ -860,22 +864,23 @@
         let wval = addImplBound i (map fst bargs) wval_in
         logElab 5 ("Checking " ++ showTmImpls wval)
         -- Elaborate wval in this context
-        ((wval', defer, is, ctxt', newDecls, highlights), _) <-
-            tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "withRHS")
+        ((wval', defer, is, ctxt', newDecls, highlights, newGName), _) <-
+            tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "withRHS")
                         (bindTyArgs PVTy bargs infP) initEState
                         (do pbinds i lhs_tm
                             -- proof search can use explicitly written names
                             mapM_ addPSname (allNamesIn lhs_in)
                             setNextName
                             -- TODO: may want where here - see winfo abpve
-                            (ElabResult _ d is ctxt' newDecls highlights) <- errAt "with value in " fname Nothing
+                            (ElabResult _ d is ctxt' newDecls highlights newGName) <- errAt "with value in " fname Nothing
                               (erun fc (build i info ERHS opts fname (infTerm wval)))
                             erun fc $ psolve lhs_tm
                             tt <- get_term
-                            return (tt, d, is, ctxt', newDecls, highlights))
+                            return (tt, d, is, ctxt', newDecls, highlights, newGName))
         setContext ctxt'
         processTacticDecls info newDecls
         sendHighlighting highlights
+        updateIState $ \i -> i { idris_name = newGName }
 
         def' <- checkDef fc iderr True defer
         let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'
@@ -970,18 +975,19 @@
         logElab 5 ("New RHS " ++ showTmImpls rhs)
         ctxt <- getContext -- New context with block added
         i <- getIState
-        ((rhs', defer, is, ctxt', newDecls, highlights), _) <-
-           tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "wpatRHS") clhsty initEState
+        ((rhs', defer, is, ctxt', newDecls, highlights, newGName), _) <-
+           tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "wpatRHS") clhsty initEState
                     (do pbinds i lhs_tm
                         setNextName
-                        (ElabResult _ d is ctxt' newDecls highlights) <-
+                        (ElabResult _ d is ctxt' newDecls highlights newGName) <-
                            erun fc (build i info ERHS opts fname rhs)
                         psolve lhs_tm
                         tt <- get_term
-                        return (tt, d, is, ctxt', newDecls, highlights))
+                        return (tt, d, is, ctxt', newDecls, highlights, newGName))
         setContext ctxt'
         processTacticDecls info newDecls
         sendHighlighting highlights
+        updateIState $ \i -> i { idris_name = newGName }
 
         def' <- checkDef fc iderr True defer
         let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'
diff --git a/src/Idris/Elab/Data.hs b/src/Idris/Elab/Data.hs
--- a/src/Idris/Elab/Data.hs
+++ b/src/Idris/Elab/Data.hs
@@ -90,7 +90,7 @@
          ttag <- getName
          i <- getIState
          let as = map (const (Left (Msg ""))) (getArgTys cty)
-         let params = findParams  (map snd cons)
+         let params = findParams n (map snd cons)
          logElab 2 $ "Parameters : " ++ show params
          -- TI contains information about mutually declared types - this will
          -- be updated when the mutual block is complete
@@ -132,13 +132,6 @@
                  (nfc, AnnName n Nothing Nothing Nothing))
                dcons
   where
-        setDetaggable :: Name -> Idris ()
-        setDetaggable n = do
-            ist <- getIState
-            let opt = idris_optimisation ist
-            case lookupCtxt n opt of
-                [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }
-                _    -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }
 
         checkDefinedAs fc n t i
             = let defined = tclift $ tfail (At fc (AlreadyDefined n))
@@ -152,63 +145,8 @@
                                          _ -> defined
                            _ -> defined
                    _ -> defined
-        -- parameters are names which are unchanged across the structure,
-        -- which appear exactly once in the return type of a constructor
 
-        -- First, find all applications of the constructor, then check over
-        -- them for repeated arguments
 
-        findParams :: [Type] -> [Int]
-        findParams ts = let allapps = map getDataApp ts
-           -- do each constructor separately, then merge the results (names
-           -- may change between constructors)
-                            conParams = map paramPos allapps in
-                            inAll conParams
-
-        inAll :: [[Int]] -> [Int]
-        inAll [] = []
-        inAll (x : xs) = filter (\p -> all (\ps -> p `elem` ps) xs) x
-
-        paramPos [] = []
-        paramPos (args : rest)
-              = dropNothing $ keepSame (zip [0..] args) rest
-
-        dropNothing [] = []
-        dropNothing ((x, Nothing) : ts) = dropNothing ts
-        dropNothing ((x, _) : ts) = x : dropNothing ts
-
-        keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->
-                    [(Int, Maybe Name)]
-        keepSame as [] = as
-        keepSame as (args : rest) = keepSame (update as args) rest
-          where
-            update [] _ = []
-            update _ [] = []
-            update ((n, Just x) : as) (Just x' : args)
-                | x == x' = (n, Just x) : update as args
-            update ((n, _) : as) (_ : args) = (n, Nothing) : update as args
-
-        getDataApp :: Type -> [[Maybe Name]]
-        getDataApp f@(App _ _ _)
-            | (P _ d _, args) <- unApply f
-                   = if (d == n) then [mParam args args] else []
-        getDataApp (Bind n (Pi _ t _) sc)
-            = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)
-        getDataApp _ = []
-
-        -- keep the arguments which are single names, which don't appear
-        -- elsewhere
-
-        mParam args [] = []
-        mParam args (P Bound n _ : rest)
-               | count n args == 1
-                  = Just n : mParam args rest
-            where count n [] = 0
-                  count n (t : ts)
-                       | n `elem` freeNames t = 1 + count n ts
-                       | otherwise = count n ts
-        mParam args (_ : rest) = Nothing : mParam args rest
-
         cname (_, _, n, _, _, _, _) = n
 
         -- Abuse of ElabInfo.
@@ -263,7 +201,7 @@
   where
     tyIs con (Bind n b sc) = tyIs con (substV (P Bound n Erased) sc)
     tyIs con t | (P Bound n' _, _) <- unApply t
-        = if n' /= tn then 
+        = if n' /= tn then
                tclift $ tfail (At fc (Elaborating "constructor " con Nothing 
                          (Msg ("Type level variable " ++ show n' ++ " is not " ++ show tn))))
              else return ()
diff --git a/src/Idris/Elab/Instance.hs b/src/Idris/Elab/Instance.hs
--- a/src/Idris/Elab/Instance.hs
+++ b/src/Idris/Elab/Instance.hs
@@ -186,12 +186,14 @@
              ty' <- implicit info syn iname ty'
              let ty = addImpl [] i ty'
              ctxt <- getContext
-             (ElabResult tyT _ _ ctxt' newDecls highlights, _) <-
-                tclift $ elaborate ctxt (idris_datatypes i) iname (TType (UVal 0)) initEState
+             (ElabResult tyT _ _ ctxt' newDecls highlights newGName, _) <-
+                tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) iname (TType (UVal 0)) initEState
                          (errAt "type of " iname Nothing (erun fc (build i info ERHS [] iname ty)))
              setContext ctxt'
              processTacticDecls info newDecls
              sendHighlighting highlights
+             updateIState $ \i -> i { idris_name = newGName }
+
              ctxt <- getContext
              (cty, _) <- recheckC fc id [] tyT
              let nty = normalise ctxt [] cty
diff --git a/src/Idris/Elab/RunElab.hs b/src/Idris/Elab/RunElab.hs
--- a/src/Idris/Elab/RunElab.hs
+++ b/src/Idris/Elab/RunElab.hs
@@ -32,18 +32,20 @@
      mustBeElabScript scriptTy
      ist <- getIState
      ctxt <- getContext
-     (ElabResult tyT' defer is ctxt' newDecls highlights, log) <-
-        tclift $ elaborate ctxt (idris_datatypes ist) (sMN 0 "toplLevelElab") elabScriptTy initEState
+     (ElabResult tyT' defer is ctxt' newDecls highlights newGName, log) <-
+        tclift $ elaborate ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "toplLevelElab") elabScriptTy initEState
                  (transformErr RunningElabScript
                    (erun fc (do tm <- runElabAction ist fc [] script ns
                                 EState is _ impls highlights <- getAux
                                 ctxt <- get_context
                                 let ds = [] -- todo
                                 log <- getLog
-                                return (ElabResult tm ds (map snd is) ctxt impls highlights))))
+                                newGName <- get_global_nextname
+                                return (ElabResult tm ds (map snd is) ctxt impls highlights newGName))))
 
 
 
      setContext ctxt'
      processTacticDecls info newDecls
      sendHighlighting highlights
+     updateIState $ \i -> i { idris_name = newGName }
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
@@ -18,7 +18,7 @@
 import Idris.Core.ProofTerm (getProofTerm)
 import Idris.Core.Typecheck (check, recheck, converts, isType)
 import Idris.Core.WHNF (whnf)
-import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)
+import Idris.Coverage (buildSCG, checkDeclTotality, checkPositive, genClauses, recoverableCoverage, validCoverageCase)
 import Idris.ErrReverse (errReverse)
 import Idris.Elab.Quasiquote (extractUnquotes)
 import Idris.Elab.Utils
@@ -52,6 +52,9 @@
              , resultTyDecls :: [RDeclInstructions]
                -- ^ Meta-info about the new type declarations
              , resultHighlighting :: [(FC, OutputAnnotation)]
+               -- ^ Saved highlights from elaboration
+             , resultName :: Int
+               -- ^ The new global name counter
              }
 
 
@@ -122,9 +125,10 @@
          ctxt <- get_context
          let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []
          log <- getLog
+         g_nextname <- get_global_nextname
          if log /= ""
-            then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights)
-            else return (ElabResult tm ds (map snd is) ctxt impls highlights)
+            then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
+            else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
   where pattern = emode == ELHS
         tydecl = emode == ETyDecl
 
@@ -166,9 +170,10 @@
          ctxt <- get_context
          let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []
          log <- getLog
+         g_nextname <- get_global_nextname
          if (log /= "")
-            then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights)
-            else return (ElabResult tm ds (map snd is) ctxt impls highlights)
+            then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
+            else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
   where pattern = emode == ELHS
 
 -- return whether arguments of the given constructor name can be
@@ -1158,9 +1163,10 @@
              -- capturing lexically available variables in the quoted term.
              ctxt <- get_context
              datatypes <- get_datatypes
+             g_nextname <- get_global_nextname
              saveState
              updatePS (const .
-                       newProof (sMN 0 "q") ctxt datatypes $
+                       newProof (sMN 0 "q") ctxt datatypes g_nextname $
                        P Ref (reflm "TT") Erased)
 
              -- Re-add the unquotes, letting Idris infer the (fictional)
@@ -1839,11 +1845,74 @@
          updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}
          return ()
 
+
     checkClosed :: Raw -> Elab' aux (Term, Type)
     checkClosed tm = do ctxt <- get_context
                         (val, ty) <- lift $ check ctxt [] tm
                         return $! (finalise val, finalise ty)
 
+    -- | Add another argument to a Pi
+    mkPi :: RFunArg -> Raw -> Raw
+    mkPi arg rTy = RBind (argName arg) (Pi Nothing (argTy arg) (RUType AllTypes)) rTy
+
+    mustBeType ctxt tm ty =
+      case normaliseAll ctxt [] (finalise ty) of
+        UType _ -> return ()
+        TType _ -> return ()
+        ty'    -> lift . tfail . InternalMsg $
+                     show tm ++ " is not a type: it's " ++ show ty'
+
+    mustNotBeDefined ctxt n =
+      case lookupDefExact n ctxt of
+        Just _ -> lift . tfail . InternalMsg $
+                    show n ++ " is already defined."
+        Nothing -> return ()
+
+    -- | Prepare a constructor to be added to a datatype being defined here
+    prepareConstructor :: Name -> RConstructorDefn -> ElabD (Name, [PArg], Type)
+    prepareConstructor tyn (RConstructor cn args resTy) =
+      do ctxt <- get_context
+         -- ensure the constructor name is not qualified, and
+         -- construct a qualified one
+         notQualified cn
+         let qcn = qualify cn
+
+         -- ensure that the constructor name is not defined already
+         mustNotBeDefined ctxt qcn
+
+         -- construct the actual type for the constructor
+         let cty = foldr mkPi resTy args
+         (checkedTy, ctyTy) <- lift $ check ctxt [] cty
+         mustBeType ctxt checkedTy ctyTy
+
+         -- ensure that the constructor builds the right family
+         case unApply (getRetTy (normaliseAll ctxt [] (finalise checkedTy))) of
+           (P _ n _, _) | n == tyn -> return ()
+           t -> lift . tfail . Msg $ "The constructor " ++ show cn ++
+                                     " doesn't construct " ++ show tyn ++
+                                     " (return type is " ++ show t ++ ")"
+
+         -- add temporary type declaration for constructor (so it can
+         -- occur in later constructor types)
+         set_context (addTyDecl qcn (DCon 0 0 False) checkedTy ctxt)
+
+         -- Save the implicits for high-level Idris
+         let impls = map rFunArgToPArg args
+
+         return (qcn, impls, checkedTy)
+
+      where
+        notQualified (NS _ _) = lift . tfail . Msg $ "Constructor names may not be qualified"
+        notQualified _ = return ()
+
+        qualify n = case tyn of
+                      (NS _ ns) -> NS n ns
+                      _ -> n
+
+        getRetTy :: Type -> Type
+        getRetTy (Bind _ (Pi _ _ _) sc) = getRetTy sc
+        getRetTy ty = ty
+
     -- | Do a step in the reflected elaborator monad. The input is the
     -- step, the output is the (reflected) term returned.
     runTacTm :: Term -> ElabD Term
@@ -2052,20 +2121,10 @@
       | n == tacN "Prim__DeclareType", [decl] <- args
       = do (RDeclare n args res) <- reifyTyDecl decl
            ctxt <- get_context
-           let mkPi arg res = RBind (argName arg)
-                                    (Pi Nothing (argTy arg) (RUType AllTypes))
-                                    res
-               rty = foldr mkPi res args
+           let rty = foldr mkPi res args
            (checked, ty') <- lift $ check ctxt [] rty
-           case normaliseAll ctxt [] (finalise ty') of
-             UType _ -> return ()
-             TType _ -> return ()
-             ty''    -> lift . tfail . InternalMsg $
-                          show checked ++ " is not a type: it's " ++ show ty''
-           case lookupDefExact n ctxt of
-             Just _ -> lift . tfail . InternalMsg $
-                         show n ++ " is already defined."
-             Nothing -> return ()
+           mustBeType ctxt checked ty'
+           mustNotBeDefined ctxt n
            let decl = TyDecl Ref checked
                ctxt' = addCtxtDef n decl ctxt
            set_context ctxt'
@@ -2076,11 +2135,46 @@
       = do defn <- reifyFunDefn decl
            defineFunction defn
            returnUnit
+      | n == tacN "Prim__DeclareDatatype", [decl] <- args
+      = do RDeclare n args resTy <- reifyTyDecl decl
+           ctxt <- get_context
+           let tcTy = foldr mkPi resTy args
+           (checked, ty') <- lift $ check ctxt [] tcTy
+           mustBeType ctxt checked ty'
+           mustNotBeDefined ctxt n
+           let ctxt' = addTyDecl n (TCon 0 0) checked ctxt
+           set_context ctxt'
+           updateAux $ \e -> e { new_tyDecls = RDatatypeDeclInstrs n (map rFunArgToPArg args) : new_tyDecls e }
+           returnUnit
+      | n == tacN "Prim__DefineDatatype", [defn] <- args
+      = do RDefineDatatype n ctors <- reifyRDataDefn defn
+           ctxt <- get_context
+           tyconTy <- case lookupTyExact n ctxt of
+                        Just t -> return t
+                        Nothing -> lift . tfail . Msg $ "Type not previously declared"
+           datatypes <- get_datatypes
+           case lookupCtxtName n datatypes of
+             [] -> return ()
+             _  -> lift . tfail . Msg $ show n ++ " is already defined as a datatype."
+           -- Prepare the constructors
+           ctors' <- mapM (prepareConstructor n) ctors
+           ttag <- do ES (ps, aux) str prev <- get
+                      let i = global_nextname ps
+                      put $ ES (ps { global_nextname = global_nextname ps + 1 },
+                                aux)
+                               str
+                               prev
+                      return i
+           let ctxt' = addDatatype (Data n ttag tyconTy False (map (\(cn, _, cty) -> (cn, cty)) ctors')) ctxt
+           set_context ctxt'
+           -- the rest happens in a bit
+           updateAux $ \e -> e { new_tyDecls = RDatatypeDefnInstrs n tyconTy ctors' : new_tyDecls e }
+           returnUnit
       | n == tacN "Prim__AddInstance", [cls, inst] <- args
       = do className <- reifyTTName cls
            instName <- reifyTTName inst
            updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
-                                               new_tyDecls e}
+                                               new_tyDecls e }
            returnUnit
       | n == tacN "Prim__IsTCName", [n] <- args
       = do n' <- reifyTTName n
@@ -2115,6 +2209,7 @@
            aux <- getAux
            datatypes <- get_datatypes
            env <- get_env
+           g_next <- get_global_nextname
 
            (ctxt', ES (p, aux') _ _) <-
               do (ES (current_p, _) _ _) <- get
@@ -2122,13 +2217,15 @@
                              (do runElabAction ist fc [] script ns
                                  ctxt' <- get_context
                                  return ctxt')
-                             ((newProof recH ctxt datatypes goalTT)
+                             ((newProof recH ctxt datatypes g_next goalTT)
                               { nextname = nextname current_p })
            set_context ctxt'
 
            let tm_out = getProofTerm (pterm p)
            do (ES (prf, _) s e) <- get
-              let p' = prf { nextname = nextname p }
+              let p' = prf { nextname = nextname p
+                           , global_nextname = global_nextname p
+                           }
               put (ES (p', aux') s e)
            env' <- get_env
            (tm, ty, _) <- lift $ recheck ctxt' env (forget tm_out) tm_out
@@ -2520,6 +2617,50 @@
              let ds' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True, True))) ds
              in addDeferred ds'
            _ -> return ()
+    RDatatypeDeclInstrs n impls ->
+      do addIBC (IBCDef n)
+         updateIState $ \i -> i { idris_implicits = addDef n impls (idris_implicits i) }
+         addIBC (IBCImp n)
+
+    RDatatypeDefnInstrs tyn tyconTy ctors ->
+      do let cn (n, _, _) = n
+             cimpls (_, impls, _) = impls
+             cty (_, _, t) = t
+         addIBC (IBCDef tyn)
+         mapM_ (addIBC . IBCDef . cn) ctors
+         let params = findParams tyn (map cty ctors)
+         let typeInfo = TI (map cn ctors) False [] params []
+         -- implicit precondition to IBCData is that idris_datatypes on the IState is populated.
+         -- otherwise writing the IBC just fails silently!
+         updateIState $ \i -> i { idris_datatypes =
+                                    addDef tyn typeInfo (idris_datatypes i) }
+         addIBC (IBCData tyn)
+
+
+         ttag <- getName -- from AbsSyntax.hs, really returns a disambiguating Int
+
+         let metainf = DataMI params
+         addIBC (IBCMetaInformation tyn metainf)
+         updateContext (setMetaInformation tyn metainf)
+
+         for_ ctors $ \(cn, impls, _) ->
+           do updateIState $ \i -> i { idris_implicits = addDef cn impls (idris_implicits i) }
+              addIBC (IBCImp cn)
+
+         for_ ctors $ \(ctorN, _, _) ->
+           do totcheck (NoFC, ctorN)
+              ctxt <- tt_ctxt <$> getIState
+              case lookupTyExact ctorN ctxt of
+                Just cty -> do checkPositive (tyn : map cn ctors) (ctorN, cty)
+                               return ()
+                Nothing -> return ()
+
+         case ctors of
+            [ctor] -> do setDetaggable (cn ctor); setDetaggable tyn
+                         addIBC (IBCOpt (cn ctor)); addIBC (IBCOpt tyn)
+            _ -> return ()
+         -- TODO: inaccessible
+
     RAddInstance className instName ->
       do -- The type class resolution machinery relies on a special
          logElab 2 $ "Adding elab script instance " ++ show instName ++
@@ -2581,13 +2722,14 @@
           let lhs = addImplPat ist lhs_in
           let fc = fileFC "elab_reflected_totality"
           let tcgen = False -- TODO: later we may support dictionary generation
-          case elaborate ctxt (idris_datatypes ist) (sMN 0 "refPatLHS") infP initEState
+          case elaborate ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "refPatLHS") infP initEState
                 (erun fc (buildTC ist info ELHS [] fname (allNamesIn lhs_in)
                                                          (infTerm lhs))) of
-            OK (ElabResult lhs' _ _ _ _ _, _) ->
+            OK (ElabResult lhs' _ _ _ _ _ name', _) ->
               do -- not recursively calling here, because we don't
                  -- want to run infinitely many times
                  let lhs_tm = orderPats (getInferTerm lhs')
+                 updateIState $ \i -> i { idris_name = name' }
                  case recheck ctxt [] (forget lhs_tm) lhs_tm of
                       OK _ -> return True
                       err -> return False
diff --git a/src/Idris/Elab/Transform.hs b/src/Idris/Elab/Transform.hs
--- a/src/Idris/Elab/Transform.hs
+++ b/src/Idris/Elab/Transform.hs
@@ -54,13 +54,14 @@
          i <- getIState
          let lhs = addImplPat i lhs_in
          logElab 5 ("Transform LHS input: " ++ showTmImpls lhs)
-         (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-
-              tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transLHS") infP initEState
+         (ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, _) <-
+              tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "transLHS") infP initEState
                        (erun fc (buildTC i info ETransLHS [] (sUN "transform")
                                    (allNamesIn lhs_in) (infTerm lhs)))
          setContext ctxt'
          processTacticDecls info newDecls
          sendHighlighting highlights
+         updateIState $ \i -> i { idris_name = newGName }
          let lhs_tm = orderPats (getInferTerm lhs')
          let lhs_ty = getInferType lhs'
          let newargs = pvars i lhs_tm
@@ -73,18 +74,21 @@
          let rhs = addImplBound i (map fst newargs) rhs_in
          logElab 5 ("Transform RHS input: " ++ showTmImpls rhs)
 
-         ((rhs', defer, ctxt', newDecls), _) <-
-              tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transRHS") clhs_ty initEState
+         ((rhs', defer, ctxt', newDecls, newGName), _) <-
+              tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "transRHS") clhs_ty initEState
                        (do pbinds i lhs_tm
                            setNextName
-                           (ElabResult _ _ _ ctxt' newDecls highlights) <- erun fc (build i info ERHS [] (sUN "transform") rhs)
+                           (ElabResult _ _ _ ctxt' newDecls highlights newGName) <- erun fc (build i info ERHS [] (sUN "transform") rhs)
+                           set_global_nextname newGName
                            erun fc $ psolve lhs_tm
                            tt <- get_term
                            let (rhs', defer) = runState (collectDeferred Nothing [] ctxt tt) []
-                           return (rhs', defer, ctxt', newDecls))
+                           newGName <- get_global_nextname
+                           return (rhs', defer, ctxt', newDecls, newGName))
          setContext ctxt'
          processTacticDecls info newDecls
          sendHighlighting highlights
+         updateIState $ \i -> i { idris_name = newGName }
 
          (crhs_tm_in, crhs_ty) <- recheckC_borrowing False False [] fc id [] rhs'
          let crhs_tm = renamepats pnames crhs_tm_in
diff --git a/src/Idris/Elab/Type.hs b/src/Idris/Elab/Type.hs
--- a/src/Idris/Elab/Type.hs
+++ b/src/Idris/Elab/Type.hs
@@ -67,12 +67,13 @@
          logElab 5 $ show "with methods " ++ show (imp_methods syn)
          logElab 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty
 
-         (ElabResult tyT' defer is ctxt' newDecls highlights, log) <-
-            tclift $ elaborate ctxt (idris_datatypes i) n (TType (UVal 0)) initEState
+         (ElabResult tyT' defer is ctxt' newDecls highlights newGName, log) <-
+            tclift $ elaborate ctxt (idris_datatypes i) (idris_name i) n (TType (UVal 0)) initEState
                      (errAt "type of " n Nothing (erun fc (build i info ETyDecl [] n ty)))
          setContext ctxt'
          processTacticDecls info newDecls
-         sendHighlighting highlights
+         sendHighlighting highlights 
+         updateIState $ \i -> i { idris_name = newGName }
 
          let tyT = patToImp tyT'
 
diff --git a/src/Idris/Elab/Utils.hs b/src/Idris/Elab/Utils.hs
--- a/src/Idris/Elab/Utils.hs
+++ b/src/Idris/Elab/Utils.hs
@@ -331,4 +331,67 @@
                               else return ()
 
 
+-- | Find the type constructor arguments that are parameters, given a list of constructor types.
+--   Parameters are names which are unchanged across the structure,
+--   which appear exactly once in the return type of a constructor
+--   First, find all applications of the constructor, then check over
+--   them for repeated arguments
+findParams :: Name -- ^ the name of the family that we are finding parameters for
+           -> [Type] -- ^ the declared constructor types
+           -> [Int]
+findParams tyn ts =
+    let allapps = map getDataApp ts
+        -- do each constructor separately, then merge the results (names
+        -- may change between constructors)
+        conParams = map paramPos allapps
+    in inAll conParams
 
+  where
+    inAll :: [[Int]] -> [Int]
+    inAll [] = []
+    inAll (x : xs) = filter (\p -> all (\ps -> p `elem` ps) xs) x
+
+    paramPos [] = []
+    paramPos (args : rest)
+          = dropNothing $ keepSame (zip [0..] args) rest
+    dropNothing [] = []
+    dropNothing ((x, Nothing) : ts) = dropNothing ts
+    dropNothing ((x, _) : ts) = x : dropNothing ts
+    keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->
+                [(Int, Maybe Name)]
+    keepSame as [] = as
+    keepSame as (args : rest) = keepSame (update as args) rest
+      where
+        update [] _ = []
+        update _ [] = []
+        update ((n, Just x) : as) (Just x' : args)
+            | x == x' = (n, Just x) : update as args
+        update ((n, _) : as) (_ : args) = (n, Nothing) : update as args
+    getDataApp :: Type -> [[Maybe Name]]
+    getDataApp f@(App _ _ _)
+        | (P _ d _, args) <- unApply f
+               = if (d == tyn) then [mParam args args] else []
+    getDataApp (Bind n (Pi _ t _) sc)
+        = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)
+    getDataApp _ = []
+    -- keep the arguments which are single names, which don't appear
+    -- elsewhere
+    mParam args [] = []
+    mParam args (P Bound n _ : rest)
+           | count n args == 1
+              = Just n : mParam args rest
+        where count n [] = 0
+              count n (t : ts)
+                   | n `elem` freeNames t = 1 + count n ts
+                   | otherwise = count n ts
+    mParam args (_ : rest) = Nothing : mParam args rest
+
+-- | Mark a name as detaggable in the global state (should be called
+-- for type and constructor names of single-constructor datatypes)
+setDetaggable :: Name -> Idris ()
+setDetaggable n = do
+    ist <- getIState
+    let opt = idris_optimisation ist
+    case lookupCtxt n opt of
+        [oi] -> putIState ist { idris_optimisation = addDef n oi { detaggable = True } opt }
+        _    -> putIState ist { idris_optimisation = addDef n (Optimise [] True) opt }
diff --git a/src/Idris/Elab/Value.hs b/src/Idris/Elab/Value.hs
--- a/src/Idris/Elab/Value.hs
+++ b/src/Idris/Elab/Value.hs
@@ -64,14 +64,15 @@
         --    * elaboration as a Type
         --    * elaboration as a function a -> b
 
-        (ElabResult tm' defer is ctxt' newDecls highlights, _) <-
-             tclift (elaborate ctxt (idris_datatypes i) (sMN 0 "val") infP initEState
+        (ElabResult tm' defer is ctxt' newDecls highlights newGName, _) <-
+             tclift (elaborate ctxt (idris_datatypes i) (idris_name i) (sMN 0 "val") infP initEState
                      (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))
 
         -- Extend the context with new definitions created
         setContext ctxt'
         processTacticDecls info newDecls
         sendHighlighting highlights
+        updateIState $ \i -> i { idris_name = newGName }
 
         let vtm = orderPats (getInferTerm tm')
 
diff --git a/src/Idris/Interactive.hs b/src/Idris/Interactive.hs
--- a/src/Idris/Interactive.hs
+++ b/src/Idris/Interactive.hs
@@ -172,7 +172,7 @@
                                         ++ with ++ "\n" ++
                                     unlines rest)
               runIO $ copyFile fb fn
-           else iPrintResult with
+           else iPrintResult (with ++ "\n")
   where getIndent s = length (takeWhile isSpace s)
 
 -- Replace the given metavariable on the given line with a 'case'
diff --git a/src/Idris/Parser/Expr.hs b/src/Idris/Parser/Expr.hs
--- a/src/Idris/Parser/Expr.hs
+++ b/src/Idris/Parser/Expr.hs
@@ -586,7 +586,7 @@
 
 {- | Parses a disambiguation expression
 Disamb ::=
-  '%' 'disamb' NameList Expr
+  'with' NameList Expr
   ;
 -}
 disamb :: SyntaxInfo -> IdrisParser PTerm
diff --git a/src/Idris/Parser/Helpers.hs b/src/Idris/Parser/Helpers.hs
--- a/src/Idris/Parser/Helpers.hs
+++ b/src/Idris/Parser/Helpers.hs
@@ -245,20 +245,20 @@
 
 -- | Idris Style for parsing identifiers/reserved keywords
 idrisStyle :: MonadicParsing m => IdentifierStyle m
-idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved Hi.Identifier Hi.ReservedIdentifier
-  where _styleName = "Idris"
-        _styleStart = satisfy isAlpha <|> oneOf "_"
-        _styleLetter = satisfy isAlphaNum <|> oneOf "_'."
-        _styleReserved = HS.fromList ["let", "in", "data", "codata", "record", "corecord", "Type",
-                                      "do", "dsl", "import", "impossible",
-                                      "case", "of", "total", "partial", "mutual",
-                                      "infix", "infixl", "infixr", "rewrite",
-                                      "where", "with", "syntax", "proof", "postulate",
-                                      "using", "namespace", "class", "instance",
-                                      "interface", "implementation", "parameters",
-                                      "public", "private", "export", "abstract", "implicit",
-                                      "quoteGoal", "constructor",
-                                      "if", "then", "else"]
+idrisStyle = IdentifierStyle {
+    _styleName = "Idris"
+  , _styleStart = satisfy isAlpha <|> oneOf "_"
+  , _styleLetter = satisfy isAlphaNum <|> oneOf "_'."
+  , _styleReserved = HS.fromList
+      ["let", "in", "data", "codata", "record", "corecord", "Type", "do", "dsl",
+      "import", "impossible", "case", "of", "total", "partial", "mutual",
+      "infix", "infixl", "infixr", "rewrite", "where", "with", "syntax",
+      "proof", "postulate", "using", "namespace", "class", "instance",
+      "interface", "implementation", "parameters", "public", "private",
+      "export", "abstract", "implicit", "quoteGoal", "constructor", "if",
+      "then", "else"]
+  , _styleHighlight = Hi.Identifier
+  , _styleReservedHighlight = Hi.ReservedIdentifier }
 
 char :: MonadicParsing m => Char -> m Char
 char = Chr.char
@@ -293,7 +293,7 @@
 -- reserved identifiers never contain line breaks.
 reservedFC :: MonadicParsing m => String -> m FC
 reservedFC str = do (FC file (l, c) _) <- getFC
-                    Tok.reserve idrisStyle str
+                    reserved str
                     return $ FC file (l, c) (l, c + length str)
 
 -- | Parse a reserved identfier, highlighting its span as a keyword
@@ -308,10 +308,9 @@
      notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
 
 reservedOpFC :: MonadicParsing m => String -> m FC
-reservedOpFC name = token $ try $ do (FC f (l, c) _) <- getFC
-                                     string name
-                                     notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
-                                     return (FC f (l, c) (l, c + length name))
+reservedOpFC name = do (FC f (l, c) _) <- getFC
+                       reservedOp name
+                       return (FC f (l, c) (l, c + length name))
 
 -- | Parses an identifier as a token
 identifier :: (MonadicParsing m) => m (String, FC)
@@ -393,7 +392,7 @@
 commentMarkers = [ "--", "|||" ]
 
 invalidOperators :: [String]
-invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"]
+invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!", "@"]
 
 -- | Parses an operator
 operator :: MonadicParsing m => m String
@@ -404,12 +403,9 @@
 
 -- | Parses an operator
 operatorFC :: MonadicParsing m => m (String, FC)
-operatorFC = do (op, fc) <- token $ do (FC f (l, c) _) <- getFC
-                                       op <- some operatorLetter
-                                       return (op, FC f (l, c) (l, c + length op))
-                when (op `elem` (invalidOperators ++ commentMarkers)) $
-                     fail $ op ++ " is not a valid operator"
-                return (op, fc)
+operatorFC = do (FC f (l, c) _) <- getFC
+                op <- operator
+                return (op, FC f (l, c) (l, c + length op))
 
 {- * Position helpers -}
 {- | Get filename from position (returns "(interactive)" when no source file is given)  -}
diff --git a/src/Idris/Prover.hs b/src/Idris/Prover.hs
--- a/src/Idris/Prover.hs
+++ b/src/Idris/Prover.hs
@@ -85,7 +85,7 @@
 
 prove :: Bool -> Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()
 prove mode opt ctxt lit n ty
-    = do ps <- fmap (\ist -> initElaborator n ctxt (idris_datatypes ist) ty) getIState
+    = do ps <- fmap (\ist -> initElaborator n ctxt (idris_datatypes ist) (idris_name ist) ty) getIState
          idemodePutSExp "start-proof-mode" n
          (tm, prf) <-
             if mode
diff --git a/src/Idris/Reflection.hs b/src/Idris/Reflection.hs
--- a/src/Idris/Reflection.hs
+++ b/src/Idris/Reflection.hs
@@ -48,6 +48,10 @@
 
 data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, [RCtorArg], Raw)] deriving Show
 
+data RConstructorDefn = RConstructor Name [RFunArg] Raw
+
+data RDataDefn = RDefineDatatype Name [RConstructorDefn]
+
 rArgOpts :: RErasure -> [ArgOpt]
 rArgOpts RErased = [InaccessibleArg]
 rArgOpts _ = []
@@ -963,7 +967,7 @@
     Right (TextPart msg)
 reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)
   | n == reflm "NamePart" =
-    case runElab initEState (reifyTTName ttn) (initElaborator (sMN 0 "hole") initContext emptyContext Erased) of
+    case runElab initEState (reifyTTName ttn) (initElaborator (sMN 0 "hole") initContext emptyContext 0 Erased) of
       Error e -> Left . InternalMsg $
        "could not reify name term " ++
        show ttn ++
@@ -971,7 +975,7 @@
       OK (n', _)-> Right $ NamePart n'
 reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
   | n == reflm "TermPart" =
-  case runElab initEState (reifyTT tm) (initElaborator (sMN 0 "hole") initContext emptyContext Erased) of
+  case runElab initEState (reifyTT tm) (initElaborator (sMN 0 "hole") initContext emptyContext 0 Erased) of
     Error e -> Left . InternalMsg $
       "could not reify reflected term " ++
       show tm ++
@@ -979,7 +983,7 @@
     OK (tm', _) -> Right $ TermPart tm'
 reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
   | n == reflm "RawPart" =
-  case runElab initEState (reifyRaw tm) (initElaborator (sMN 0 "hole") initContext emptyContext Erased) of
+  case runElab initEState (reifyRaw tm) (initElaborator (sMN 0 "hole") initContext emptyContext 0 Erased) of
     Error e -> Left . InternalMsg $
       "could not reify reflected raw term " ++
       show tm ++
@@ -1043,6 +1047,18 @@
           | 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."
+
+reifyRConstructorDefn :: Term -> ElabD RConstructorDefn
+reifyRConstructorDefn (App _ (App _ (App _ (P _ n _) cn) args) retTy)
+  | n == tacN "Constructor", Just args' <- unList args
+  = RConstructor <$> reifyTTName cn <*> mapM reifyRFunArg args' <*> reifyRaw retTy
+reifyRConstructorDefn aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RConstructorDefn"
+
+reifyRDataDefn :: Term -> ElabD RDataDefn
+reifyRDataDefn (App _ (App _ (P _ n _) tyn) ctors)
+  | n == tacN "DefineDatatype", Just ctors' <- unList ctors
+  = RDefineDatatype <$> reifyTTName tyn <*> mapM reifyRConstructorDefn ctors'
+reifyRDataDefn aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RDataDefn"
 
 envTupleType :: Raw
 envTupleType
diff --git a/src/Util/ScreenSize.hs b/src/Util/ScreenSize.hs
--- a/src/Util/ScreenSize.hs
+++ b/src/Util/ScreenSize.hs
@@ -1,24 +1,6 @@
-{-# LANGUAGE CPP #-}
 module Util.ScreenSize(getScreenWidth) where
 
-#ifndef CURSES
-
-getScreenWidth :: IO Int
-getScreenWidth = return 80
-
-#else
-
-import UI.HSCurses.Curses
-import System.IO (hIsTerminalDevice, stdout)
+import System.Console.Terminal.Size (size, width)
 
 getScreenWidth :: IO Int
-getScreenWidth = do term <- hIsTerminalDevice stdout
-                    if term
-                       then do
-                         initScr
-                         refresh
-                         size <- scrSize
-                         endWin
-                         return (snd size)
-                       else return 80
-#endif
+getScreenWidth = maybe 80 width `fmap` size
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,16 +1,16 @@
-resolver: lts-4.2
+resolver: lts-5.5
+
 packages:
-- '.'
+  - '.'
+
 flags:
-   idris:
-     FFI: true
-     GMP: True
-     curses: True
-extra-deps: 
-- annotated-wl-pprint-0.7.0
-- cheapskate-0.1.0.4
-- hscurses-1.4.2.0
-- libffi-0.1
+  idris:
+    FFI: true
+    GMP: true
+
+extra-deps:
+  - libffi-0.1
+
 nix:
-   enable: false
-   shell-file: stack-shell.nix
+  enable: false
+  shell-file: stack-shell.nix
diff --git a/test/Makefile b/test/Makefile
--- a/test/Makefile
+++ b/test/Makefile
@@ -12,7 +12,7 @@
 	@./runtest $(patsubst %.test,%,$@) -q
 
 test_js: runtest
-	@./runtest without sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 basic007 basic011 ffi006 ffi007 primitives005 opts --codegen node
+	@./runtest without sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 basic007 basic011 ffi006 ffi007 ffi008 primitives005 primitives006 opts --codegen node
 
 update: runtest
 	@./runtest all -u
diff --git a/test/ffi007/expected b/test/ffi007/expected
--- a/test/ffi007/expected
+++ b/test/ffi007/expected
@@ -6,3 +6,4 @@
 00000377
 I'm dynamic 3
 6
+7
diff --git a/test/ffi007/ffi007.c b/test/ffi007/ffi007.c
--- a/test/ffi007/ffi007.c
+++ b/test/ffi007/ffi007.c
@@ -28,3 +28,7 @@
 callback test_ffi6(void) {
     return &dynamic_fn;
 }
+
+void test_mulpar(void (*fn)(int, int)) {
+    fn(3,4);
+}
diff --git a/test/ffi007/ffi007.h b/test/ffi007/ffi007.h
--- a/test/ffi007/ffi007.h
+++ b/test/ffi007/ffi007.h
@@ -9,3 +9,5 @@
 void test_ffi3(void (*cb)(void));
 
 callback test_ffi6(void);
+
+void test_mulpar(void (*fn)(int, int));
diff --git a/test/ffi007/ffi007.idr b/test/ffi007/ffi007.idr
--- a/test/ffi007/ffi007.idr
+++ b/test/ffi007/ffi007.idr
@@ -34,6 +34,14 @@
 test7 : Ptr -> Int -> IO Int
 test7 fnptr i = foreign FFI_C "%dynamic" (Ptr -> Int -> IO Int) fnptr i
 
+adder : Int -> Int -> ()
+adder x y = unsafePerformIO $ do
+                printLn $ x + y
+
+test8 : IO ()
+test8 = foreign FFI_C "test_mulpar" (CFnPtr (Int -> Int -> ()) -> IO ())
+                                    (MkCFnPtr adder)
+
 main : IO ()
 main = do
             test
@@ -46,4 +54,5 @@
             fptr <- test6
             i <- test7 fptr 3
             printLn i
+            test8
             return ()
diff --git a/test/ffi008/expected b/test/ffi008/expected
new file mode 100644
--- /dev/null
+++ b/test/ffi008/expected
@@ -0,0 +1,5 @@
+True
+True
+a: 122 b: 0
+4
+00000010
diff --git a/test/ffi008/ffi008.c b/test/ffi008/ffi008.c
new file mode 100644
--- /dev/null
+++ b/test/ffi008/ffi008.c
@@ -0,0 +1,14 @@
+#include "ffi008.h"
+#include <stdio.h>
+
+int size1(void) {
+    return sizeof(struct test1);
+}
+
+int size2(void) {
+    return sizeof(struct test2);
+}
+
+void print_mystruct(void) {
+    printf("a: %d b: %d\n", mystruct.a, mystruct.b);
+}
diff --git a/test/ffi008/ffi008.h b/test/ffi008/ffi008.h
new file mode 100644
--- /dev/null
+++ b/test/ffi008/ffi008.h
@@ -0,0 +1,17 @@
+#include <stdint.h>
+
+struct test1 {
+    int8_t a;
+    int64_t b;
+};
+
+struct test2 {
+    int32_t a;
+    int16_t b;
+};
+
+struct test2 mystruct;
+
+int size1(void);
+int size2(void);
+void print_mystruct();
diff --git a/test/ffi008/ffi008.idr b/test/ffi008/ffi008.idr
new file mode 100644
--- /dev/null
+++ b/test/ffi008/ffi008.idr
@@ -0,0 +1,48 @@
+module Main
+
+import CFFI
+import Data.Vect
+
+%include C "ffi008.h"
+
+size1 : IO Int
+size1 = foreign FFI_C "size1" (IO Int)
+
+
+size2 : IO Int
+size2 = foreign FFI_C "size2" (IO Int)
+
+mystruct : IO Ptr
+mystruct = foreign FFI_C "&mystruct" (IO Ptr)
+
+print_mystruct : IO ()
+print_mystruct = foreign FFI_C "print_mystruct" (IO ())
+
+test1 : Composite
+test1 = STRUCT [I8, I64]
+
+test2 : Composite
+test2 = STRUCT [I32, I16]
+
+test3 : Composite
+test3 = STRUCT [DOUBLE, DOUBLE, I8, I64]
+
+test4 : Composite
+test4 = PACKEDSTRUCT [I8, I8, I8, I64]
+
+
+main : IO ()
+main = do
+    printLn $ sizeOf test1 == !size1
+    printLn $ sizeOf test2 == !size2
+    fms <- return $ (test2#0) !mystruct
+    poke I32 fms 122
+    print_mystruct
+    printLn $ fields test3
+    withAlloc test2 $ \p => do
+        f1 <- return $ (test2 # 0) p
+        poke I32 f1 8
+        update I32 f1 (* 2)
+        print !(peek I32 f1)
+    withAlloc PTR $ \p =>
+        poke PTR p fms
diff --git a/test/ffi008/run b/test/ffi008/run
new file mode 100644
--- /dev/null
+++ b/test/ffi008/run
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ ffi008.idr -o ffi008 -p contrib --cg-opt "ffi008.c"
+./ffi008
+rm -f ffi008 *.ibc
diff --git a/test/interactive001/expected b/test/interactive001/expected
--- a/test/interactive001/expected
+++ b/test/interactive001/expected
@@ -6,6 +6,7 @@
 f x :: map f xs
 isElem2 x (y :: ys) with (_)
   isElem2 x (y :: ys) | with_pat = ?isElem2_rhs
+
   isElem3 x (x :: ys) | (Yes Refl) = ?isElem3_rhs_3
 
               [] => ?bar_1
diff --git a/test/meta002/AgdaStyleReflection.idr b/test/meta002/AgdaStyleReflection.idr
--- a/test/meta002/AgdaStyleReflection.idr
+++ b/test/meta002/AgdaStyleReflection.idr
@@ -40,13 +40,6 @@
   | Constant Const
   | Ty
 
-unApply : Raw -> (Raw, List Raw)
-unApply tm = unApply' tm []
-  where unApply' : Raw -> List Raw -> (Raw, List Raw)
-        unApply' (RApp f x) xs = unApply' f (x::xs)
-        unApply' notApp xs = (notApp, xs)
-
-
 implementation Quotable Plicity Raw where
   quotedTy = `(Plicity)
   quote Explicit = `(Explicit)
diff --git a/test/meta002/DataDef.idr b/test/meta002/DataDef.idr
new file mode 100644
--- /dev/null
+++ b/test/meta002/DataDef.idr
@@ -0,0 +1,73 @@
+module DataDef
+
+foo : Elab ()
+foo = do declareDatatype $ Declare `{{DataDef.N}} [MkFunArg `{{n}} `(Nat) Explicit NotErased] `(Type)
+         defineDatatype $ DefineDatatype `{{DataDef.N}} [
+                            Constructor `{{MkN}} [MkFunArg `{{x}} `(Nat) Implicit NotErased] (RApp (Var `{{DataDef.N}}) (Var `{{x}})),
+                            Constructor `{{MkN'}} [MkFunArg `{{x}} `(Nat) Explicit NotErased] (RApp (Var `{{DataDef.N}}) (RApp (Var `{S}) (Var `{{x}})))
+                          ]
+%runElab foo
+
+one : N 1
+one = MkN
+
+two : N 2
+two = MkN' 1
+
+
+-- mutual
+--   data U : Type where
+--     Base : U
+--     Pi : (code : U) -> (el code -> U) -> U
+--   el : U -> Type
+--   el Base = Bool
+--   el (Pi code body) = (x : el code) -> el (body x)
+
+
+
+mkU : Elab ()
+mkU = do let U = `{{DataDef.U}}
+         let el = `{{DataDef.el}}
+         declareDatatype $ Declare U [] `(Type)
+         declareType $ Declare el [MkFunArg `{{code}} (Var U) Explicit NotErased] `(Type)
+         defineDatatype $ DefineDatatype U [
+                            Constructor `{{Base}} [] (Var U),
+                            Constructor `{{Pi}}
+                                        [MkFunArg `{{code}} (Var U) Explicit NotErased,
+                                         MkFunArg `{{body}} `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)) Explicit NotErased]
+                                        (Var U)
+                          ]
+         defineFunction $ DefineFun el [
+                            MkFunClause (RBind `{{code}} (PVar (Var U))
+                                           (RBind `{{body}} (PVar `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)))
+                                              (RApp (Var el)
+                                                    (RApp (RApp (Var `{{DataDef.Pi}})
+                                                                (Var `{{code}}))
+                                                          (Var `{{body}})))))
+                                        (RBind `{{code}} (PVar (Var U))
+                                           (RBind `{{body}} (PVar `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)))
+                                              (RBind `{{x}} (Pi (RApp (Var el) (Var `{{code}})) `(Type))
+                                                 (RApp (Var el) (RApp (Var `{{body}}) (Var `{{x}})))))),
+                            MkFunClause (RApp (Var el) (Var `{{DataDef.Base}})) `(Bool)
+
+                          ]
+
+%runElab mkU
+
+tt : el Base
+tt = True
+
+fun : el (Pi Base (\x => if x then Base else Pi Base (const Base)))
+fun = \x => (case x of
+               False => \y => False
+               True => False)
+
+
+nope : Elab ()
+nope = defineDatatype $ DefineDatatype `{Either} [
+           Constructor `{{Middle}} [ MkFunArg `{{x}} `(Type) Implicit NotErased
+                                   , MkFunArg `{{y}} `(Type) Implicit NotErased
+                                   ] `(Either ~(Var `{{x}}) ~(Var `{{y}}))
+       ]
+%runElab nope
+ 
diff --git a/test/meta002/expected b/test/meta002/expected
--- a/test/meta002/expected
+++ b/test/meta002/expected
@@ -1,9 +1,12 @@
+DataDef.idr:72:1-9:
+While running an elaboration script, the following error occurred:
+Prelude.Either.Either is already defined as a datatype.
 Tacs.idr:298:15:
 When checking right hand side of testElab3 with expected type
         DPair Ty (Tm [])
 
 Unifying ty and ARR ty t would lead to infinite value
-AgdaStyleReflection.idr:328:5:
+AgdaStyleReflection.idr:321:5:
 When checking right hand side of baz with expected type
         (Nat, Void)
 
diff --git a/test/meta002/run b/test/meta002/run
--- a/test/meta002/run
+++ b/test/meta002/run
@@ -1,4 +1,5 @@
 #!/usr/bin/env bash
+${IDRIS:-idris} $@ -p pruviloj --nocolour --check --consolewidth 70 DataDef.idr
 ${IDRIS:-idris} $@ -p pruviloj --nocolour --check --consolewidth 70 Tacs.idr
 ${IDRIS:-idris} $@ -p pruviloj --nocolour --check --consolewidth 70 AgdaStyleReflection.idr
 # Disabled due to excess memory consumption
diff --git a/test/primitives006/Data/ByteArray.idr b/test/primitives006/Data/ByteArray.idr
new file mode 100644
--- /dev/null
+++ b/test/primitives006/Data/ByteArray.idr
@@ -0,0 +1,100 @@
+module Data.ByteArray
+
+%include C "array.h"
+%link C "array.o"
+
+%access public export
+%default total
+
+namespace Byte
+  Byte : Type
+  Byte = Bits8
+
+  toInt : Byte -> Int
+  toInt = prim__zextB8_Int
+
+  fromInt : Int -> Byte
+  fromInt = prim__truncInt_B8
+
+export
+record ByteArray where
+  constructor BA
+  ptr : CData
+  sz : Int
+
+-- This needn't be precise; it just needs to be enough to be safe.
+export
+bytesPerInt : Int
+bytesPerInt = 8
+
+export
+allocate : Int -> IO ByteArray
+allocate sz = do
+  ptr <- foreign FFI_C "array_alloc" (Int -> IO CData) sz
+  return $ BA ptr sz
+
+export
+reallocate : Int -> ByteArray -> IO ()
+reallocate newSz (BA ptr sz)
+  = foreign FFI_C "array_realloc" (Int -> CData -> IO ()) sz ptr
+
+export
+peek : Int -> ByteArray -> IO Byte
+peek ofs (BA ptr sz)
+  = if (ofs < 0 || ofs >= sz)
+      then return 0
+      else foreign FFI_C "array_peek" (Int -> CData -> IO Byte) ofs ptr
+
+export
+peekInt : Int -> ByteArray -> IO Int
+peekInt ofs (BA ptr sz)
+  = if (ofs < 0 || ofs+bytesPerInt > sz)
+      then return 0
+      else foreign FFI_C "array_peek_int" (Int -> CData -> IO Int) ofs ptr
+
+export
+poke : Int -> Byte -> ByteArray -> IO ()
+poke ofs b (BA ptr sz)
+  = if (ofs < 0 || ofs >= sz)
+      then return ()
+      else foreign FFI_C "array_poke" (Int -> Byte -> CData -> IO ()) ofs b ptr
+
+export
+pokeInt : Int -> Int -> ByteArray -> IO ()
+pokeInt ofs i (BA ptr sz)
+  = if (ofs < 0 || ofs+bytesPerInt > sz)
+      then return ()
+      else foreign FFI_C "array_poke_int" (Int -> Int -> CData -> IO ()) ofs i ptr
+
+export
+copy : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO ()
+copy (BA srcPtr srcSz, srcIx) (BA dstPtr dstSz, dstIx) count
+  = if (srcIx < 0 || dstIx < 0 || (srcIx+count) > srcSz || (dstIx+count) > dstSz)
+      then return ()
+      else foreign FFI_C "array_copy" (CData -> Int -> CData -> Int -> Int -> IO ()) srcPtr srcIx dstPtr dstIx count
+
+export
+fill : Int -> Int -> Byte -> ByteArray -> IO ()
+fill ofs count b (BA ptr sz)
+  = if (ofs < 0 || ofs+count > sz)
+      then return ()
+      else foreign FFI_C "array_fill" (Int -> Int -> Byte -> CData -> IO ()) ofs count b ptr
+
+export
+size : ByteArray -> Int
+size (BA ptr sz) = sz
+
+export
+compare : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO Int
+compare (BA ptrL szL, ofsL) (BA ptrR szR, ofsR) count
+  = if (ofsL < 0 || ofsL+count > szL || ofsR < 0 || ofsR+count > szR)
+      then return 0
+      else foreign FFI_C "array_compare" (CData -> Int -> CData -> Int -> Int -> IO Int) ptrL ofsL ptrR ofsR count
+
+export
+find : Byte -> ByteArray -> Int -> Int -> IO (Maybe Int)
+find b (BA ptr sz) ofs end = do
+  ofs <- foreign FFI_C "array_find" (Byte -> CData -> Int -> Int -> IO Int) b ptr ofs end
+  if ofs < 0
+    then return $ Nothing
+    else return $ Just ofs
diff --git a/test/primitives006/Data/Bytes.idr b/test/primitives006/Data/Bytes.idr
new file mode 100644
--- /dev/null
+++ b/test/primitives006/Data/Bytes.idr
@@ -0,0 +1,287 @@
+module Data.Bytes
+
+import Data.ByteArray as BA
+
+%access public export
+%default total
+
+-- Structure of the allocated ByteArray
+--   [used_size][.....data.....]
+-- used_size is an int and it takes up BA.bytesPerInt bytes
+-- at the beginning of the array
+
+export
+record Bytes where
+  constructor B
+  arr : ByteArray
+  ofs : Int
+  end : Int  -- first offset not included in the array
+
+minimalCapacity : Int
+minimalCapacity = 16
+
+private
+dataOfs : Int
+dataOfs = 1 * BA.bytesPerInt
+
+private
+allocate : Int -> IO Bytes
+allocate capacity = do
+  arr <- BA.allocate (BA.bytesPerInt + capacity)
+  BA.pokeInt 0 dataOfs arr
+  BA.fill dataOfs capacity 0 arr  -- zero the array
+  return $ B arr dataOfs dataOfs
+
+export
+length : Bytes -> Int
+length (B arr ofs end) = end - ofs
+
+export
+empty : Bytes
+empty = unsafePerformIO $ allocate minimalCapacity
+
+export
+null : Bytes -> Bool
+null (B arr ofs end) = (ofs == end)
+
+%freeze empty
+
+-- factor=1 ~ copy
+-- factor=2 ~ grow
+private
+grow : Int -> Bytes -> IO Bytes
+grow factor (B arr ofs end) = do
+  maxUsed <- BA.peekInt 0 arr
+  let bytesUsed = end - ofs
+  let bytesAvailable =
+        if maxUsed > end
+          then bytesUsed
+          else BA.size arr - ofs
+  B arr' ofs' end' <- allocate $ (factor*bytesAvailable) `max` minimalCapacity
+  BA.copy (arr, ofs) (arr', ofs') bytesUsed
+  return $ B arr' ofs' (ofs' + bytesUsed)
+
+%assert_total
+export
+snoc : Bytes -> Byte -> Bytes
+snoc bs@(B arr ofs end) byte
+    = if end >= BA.size arr
+        then unsafePerformIO $ do  -- need more space
+          grown <- grow 2 bs
+          return $ snoc grown byte
+        else unsafePerformIO $ do
+          maxUsed <- BA.peekInt 0 arr
+          if maxUsed > end
+            then do  -- someone already took the headroom, need copying
+              copy <- grow 2 bs
+              return $ snoc copy byte
+            else do  -- can mutate
+              BA.pokeInt 0 (end+1) arr
+              BA.poke end byte arr
+              return $ B arr ofs (end+1)
+
+infixl 7 |>
+export
+(|>) : Bytes -> Byte -> Bytes
+(|>) = snoc
+
+namespace SnocView
+  data SnocView : Type where
+    Nil : SnocView
+    Snoc : (bs : Bytes) -> (b : Byte) -> SnocView
+
+  export
+  snocView : Bytes -> SnocView
+  snocView (B arr ofs end) =
+    if end == ofs
+      then SnocView.Nil
+      else unsafePerformIO $ do
+        last <- BA.peek (end-1) arr
+        return $ SnocView.Snoc (B arr ofs (end-1)) last
+
+namespace ConsView
+  data ConsView : Type where
+    Nil : ConsView
+    Cons : (b : Byte) -> (bs : Bytes) -> ConsView
+
+  export
+  consView : Bytes -> ConsView
+  consView (B arr ofs end) =
+    if end == ofs
+      then ConsView.Nil
+      else unsafePerformIO $ do
+        first <- BA.peek ofs arr
+        return $ ConsView.Cons first (B arr (ofs+1) end)
+
+infixr 7 ++
+%assert_total
+export
+(++) : Bytes -> Bytes -> Bytes
+(++) bsL@(B arrL ofsL endL) bsR@(B arrR ofsR endR)
+  = let countR = endR - ofsR in
+      if endL + countR > BA.size arrL
+        then unsafePerformIO $ do  -- need more space
+          grown <- grow 2 bsL
+          return $ grown ++ bsR
+        else unsafePerformIO $ do
+          maxUsedL <- BA.peekInt 0 arrL
+          if maxUsedL > endL
+            then do  -- headroom taken
+              copyL <- grow 2 bsL
+              return $ copyL ++ bsR
+            else do  -- can mutate
+              BA.pokeInt 0 (endL + countR) arrL
+              BA.copy (arrR, ofsR) (arrL, endL) countR
+              return $ B arrL ofsL (endL + countR)
+
+export
+dropPrefix : Int -> Bytes -> Bytes
+dropPrefix n (B arr ofs end) = B arr (((ofs + n) `min` end) `max` dataOfs) end
+
+export
+takePrefix : Int -> Bytes -> Bytes
+takePrefix n (B arr ofs end) = B arr ofs (((ofs + n) `min` end) `max` dataOfs)
+
+export
+pack : List Byte -> Bytes
+pack = fromList empty
+  where
+    fromList : Bytes -> List Byte -> Bytes
+    fromList bs []        = bs
+    fromList bs (x :: xs) = fromList (bs `snoc` x) xs
+
+export
+unpack : Bytes -> List Byte
+unpack bs with (consView bs)
+  | Nil       = []
+  | Cons x xs = x :: unpack (assert_smaller bs xs)
+
+export
+slice : Int -> Int -> Bytes -> Bytes
+slice ofs' end' (B arr ofs end)
+  = B arr
+        (((ofs + ofs') `min` end) `max` dataOfs)
+        (((ofs + end') `min` end) `max` dataOfs)
+
+-- Folds with early exit.
+-- If Bytes were a Functor, this would be equivalent
+-- to a Traversable implementation interpreted in the Either monad.
+data Result : Type -> Type where
+  Stop : (result : a) -> Result a
+  Cont : (acc : a) -> Result a
+
+export
+iterateR : (Byte -> a -> Result a) -> a -> Bytes -> a
+iterateR f acc bs with (snocView bs)
+  | Nil       = acc
+  | Snoc ys y with (f y acc)
+    | Stop result = result
+    | Cont acc'   = iterateR f acc' (assert_smaller bs ys)
+
+export
+iterateL : (a -> Byte -> Result a) -> a -> Bytes -> a
+iterateL f acc bs with (consView bs)
+  | Nil       = acc
+  | Cons y ys with (f acc y)
+    | Stop result = result
+    | Cont acc'   = iterateL f acc' (assert_smaller bs ys)
+
+infixl 3 .:
+private
+(.:) : (a -> b) -> (c -> d -> a) -> (c -> d -> b)
+(.:) g f x y = g (f x y)
+
+export
+foldr : (Byte -> a -> a) -> a -> Bytes -> a
+foldr f = iterateR (Cont .: f)
+
+export
+foldl : (a -> Byte -> a) -> a -> Bytes -> a
+foldl f = iterateL (Cont .: f)
+
+export
+spanLength : (Byte -> Bool) -> Bytes -> Int
+spanLength p = iterateL step 0
+  where
+    step : Int -> Byte -> Result Int
+    step n b with (p b)
+      | True  = Cont (1 + n)
+      | False = Stop n
+
+find : Byte -> Bytes -> Maybe Int
+find b (B arr ofs end) = unsafePerformIO $ BA.find b arr ofs end
+
+export
+splitAt : Int -> Bytes -> (Bytes, Bytes)
+splitAt n bs = (takePrefix n bs, dropPrefix n bs)
+
+export
+splitOn : Byte -> Bytes -> (Bytes, Bytes)
+splitOn b bs with (find b bs)
+  | Nothing  = (bs, empty)
+  | Just ofs = (takePrefix ofs bs, dropPrefix (ofs+1) bs)
+
+export
+splitsOn : Byte -> Bytes -> List Bytes
+splitsOn b bs with (find b bs)
+  | Nothing  = [bs]
+  | Just ofs = takePrefix ofs bs :: splitsOn b (assert_smaller bs $ dropPrefix (ofs+1) bs)
+
+export
+asciiLines : Bytes -> List Bytes
+asciiLines = splitsOn 0x0A
+
+export
+span : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
+span p bs = splitAt (spanLength p bs) bs
+
+export
+break : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
+break p bs = span (not . p) bs
+
+private
+cmp : Bytes -> Bytes -> Ordering
+cmp (B arrL ofsL endL) (B arrR ofsR endR) = unsafePerformIO $ do
+    let countL = endL - ofsL
+    let countR = endR - ofsR
+    let commonCount = countL `min` countR
+    result <- BA.compare (arrL, ofsL) (arrR, ofsR) commonCount
+    return $
+      if result /= 0
+        then i2o result
+        else compare countL countR
+  where
+    i2o : Int -> Ordering
+    i2o 0 = EQ
+    i2o i = if i < 0 then LT else GT
+
+implementation Eq Bytes where
+  xs == ys = (Bytes.cmp xs ys == EQ)
+
+implementation Ord Bytes where
+  compare = Bytes.cmp
+
+export
+toString : Bytes -> String
+toString = foldr (strCons . chr . toInt) ""
+
+export
+fromString : String -> Bytes
+fromString = foldl (\bs, c => bs |> fromInt (ord c)) empty . unpack
+
+implementation Show Bytes where
+  show = ("b" ++) . show . toString
+
+implementation Semigroup Bytes where
+  (<+>) = (++)
+
+implementation Monoid Bytes where
+  neutral = empty
+
+-- todo:
+--
+-- make indices Nats
+-- Build a ByteString on top of Bytes?
+-- migrate to (Bits 8)?
+--
+-- bidirectional growth?
diff --git a/test/primitives006/array.c b/test/primitives006/array.c
new file mode 100644
--- /dev/null
+++ b/test/primitives006/array.c
@@ -0,0 +1,62 @@
+#include "array.h"
+#include <string.h>
+
+int array_find(uint8_t byte, CData array, int ofs, int end)
+{
+    void * data = array->data + ofs;
+    void * result = memchr(data, (int) byte, (size_t) (end - ofs));
+    if (result == NULL)
+    {
+        return -1;
+    }
+    else
+    {
+        return (result - data);
+    }
+}
+
+void array_realloc(int size, CData array)
+{
+    array->data = realloc(array->data, (size_t) size);
+}
+
+CData array_alloc(int size)
+{
+    return cdata_allocate((size_t) size, free);
+}
+
+uint8_t array_peek(int ofs, CData array)
+{
+    return ((uint8_t *) array->data)[ofs];
+}
+
+void array_poke(int ofs, uint8_t byte, CData array)
+{
+    ((uint8_t *) array->data)[ofs] = byte;
+}
+
+int array_peek_int(int ofs, CData array)
+{
+    return *((int *) (array->data + ofs));
+}
+
+void array_poke_int(int ofs, int val, CData array)
+{
+    *((int *) (array->data + ofs)) = val;
+}
+
+void array_copy(CData src, int src_ofs, CData dst, int dst_ofs, int count)
+{
+    // memmove rather than memcpy in case the areas overlap
+    memmove(dst->data + dst_ofs, src->data + src_ofs, count);
+}
+
+void array_fill(int ofs, int count, uint8_t byte, CData array)
+{
+    memset(array->data + ofs, byte, count);
+}
+
+int array_compare(CData l, int lofs, CData r, int rofs, int count)
+{
+    return memcmp(l->data + lofs, r->data + rofs, count);
+}
diff --git a/test/primitives006/array.h b/test/primitives006/array.h
new file mode 100644
--- /dev/null
+++ b/test/primitives006/array.h
@@ -0,0 +1,18 @@
+#pragma once
+
+#include <stdint.h>
+#include <stddef.h>
+
+#include "idris_rts.h"
+
+
+CData array_alloc(int size);
+void array_realloc(int size, CData array);
+uint8_t array_peek(int ofs, CData array);
+int array_peek_int(int ofs, CData array);
+void array_poke(int ofs, uint8_t byte, CData array);
+void array_poke_int(int ofs, int i, CData array);
+void array_copy(CData src, int src_ofs, CData dst, int dst_ofs, int count);
+void array_fill(int ofs, int count, uint8_t byte, CData array);
+int array_compare(CData l, int lofs, CData r, int rofs, int count);
+int array_find(uint8_t byte, CData array, int ofs, int end);
diff --git a/test/primitives006/expected b/test/primitives006/expected
new file mode 100644
--- /dev/null
+++ b/test/primitives006/expected
@@ -0,0 +1,9 @@
+1024
+("01/8", (145536, 897))
+("02/8", (145536, 897))
+("03/8", (145536, 897))
+("04/8", (145536, 897))
+("05/8", (145536, 897))
+("06/8", (145536, 897))
+("07/8", (145536, 897))
+("08/8", (145536, 897))
diff --git a/test/primitives006/load-test.idr b/test/primitives006/load-test.idr
new file mode 100644
--- /dev/null
+++ b/test/primitives006/load-test.idr
@@ -0,0 +1,48 @@
+module Main
+
+import Data.Bytes as B
+import Data.ByteArray as BA
+
+-- %flag C "-g3 -ggdb -O0"
+%link C "array.o"
+
+initialBuf : Bytes
+initialBuf = pack . concat $ replicate 128 block
+  where
+    block : List Byte
+    block = [10,32,1,10,100,32,1,10,255,32,1,10,1,10,255,32,1,10,255,32,1,10,255,32,1,10]
+
+unRLE : Bytes -> Bytes
+unRLE = fst . iterateL phi (empty, Nothing)
+  where
+    phi : (Bytes, Maybe Byte) -> Byte -> Result (Bytes, Maybe Byte)
+    phi (bs, Nothing)  b = Cont (bs, Just b)
+    phi (bs, Just cnt) b = Cont (bs ++ pack (replicate (cast $ prim__zextB8_Int cnt) b), Nothing)
+
+unit : Int -> Byte -> IO ()
+unit n b =
+    let expanded = unRLE initialBuf
+      in let elines = map (flip snoc b) (asciiLines expanded)
+        in printLn $ (show b ++ "/" ++ show n, length expanded, length elines)
+
+alloc : Int -> Int -> IO Int
+alloc x 0 = return x
+alloc x i = do
+  -- allocate an array
+  arr <- BA.allocate (64 * 1024 * 1024)
+  -- write "i" at offset 63M
+  BA.pokeInt (63*1024*1024) i arr
+  -- read number from offset 63M
+  j <- BA.peekInt (63*1024*1024) arr
+  -- count matches
+  alloc (x + if i == j then 1 else 0) (i - 1)
+
+main : IO ()
+main = do
+    -- First allocate 1024 64M arrays to break the C heap if there's a bug
+    alloc 0 1024 >>= printLn
+
+    -- Then, test Bytes
+    traverse_ (unit n . prim__truncInt_B8) [1..n]
+  where
+    n = 8
diff --git a/test/primitives006/run b/test/primitives006/run
new file mode 100644
--- /dev/null
+++ b/test/primitives006/run
@@ -0,0 +1,6 @@
+#!/usr/bin/env bash
+${CC:-cc} -c -O2 -o array.o array.c $(${IDRIS:-idris} --include)
+${IDRIS:-idris} $@ -o load-test load-test.idr --nocolour --warnreach
+./load-test
+rm -f load-test *.o *.ibc
+find -name \*.ibc -delete
diff --git a/test/pruviloj001/pruviloj001.idr b/test/pruviloj001/pruviloj001.idr
--- a/test/pruviloj001/pruviloj001.idr
+++ b/test/pruviloj001/pruviloj001.idr
@@ -12,7 +12,7 @@
 auto : Elab ()
 auto = do compute
           attack
-          try $ repeatUntilFail intro'
+          try intros
           hs <- map fst <$> getEnv
           for_ hs $
             \ih => try (rewriteWith (Var ih))
@@ -23,10 +23,12 @@
 partial
 mush : Elab ()
 mush =
-    do n <- gensym "j"
+    do attack
+       n <- gensym "j"
        intro n
        try intros
        ignore $ induction (Var n) `andThen` auto
+       solve
 
 plusAssoc : (j, k, l : Nat) -> plus (plus j k) l = plus j (plus k l)
 plusAssoc = %runElab mush