diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,46 @@
   dependent types
 * `rewrite` can now be given an optional rewriting lemma, with the syntax
   `rewrite [rule] using [rewrite_lemma] in [scope]`.
+
+* Reorganised elaboration of `implementation`, so that interfaces with
+  dependencies between methods now work more smoothly
+
+* Allow naming of parent implementations when defining an implementation.
+  For example:
+
+  ```
+  [PlusNatSemi] Semigroup Nat where
+    (<+>) x y = x + y
+  
+  [MultNatSemi] Semigroup Nat where
+    (<+>) x y = x * y
+  
+  -- use PlusNatSemi as the parent implementation
+  [PlusNatMonoid] Monoid Nat using PlusNatSemi where
+    neutral = 0
+  
+  -- use MultNatSemi as the parent implementation
+  [MultNatMonoid] Monoid Nat using MultNatSemi where
+    neutral = 1
+  ```
+
+* Interface definitions can now include data declarations (but not data
+  definitions). Any implementation of the interface must define the method
+  using a data type. The effect is to cause Idris to treat the method as
+  a data type (for unification and interface resolution purposes).
+
+* Experimentally, allow named implementations to be available by default in a
+  block of declarations with `using` notation. For example:
+
+  ```
+  using implementation PlusNatMonoid
+    test : Nat -> Nat
+    test x = x <+> x <+> neutral
+  ```
+
+* Constraint arguments can now appear anywhere in function types, not just
+  at the top level or after an implicit argument binding.
+
 * Experimental extended `with` syntax, which allows calling functions defined
   in a with block directly. For example:
 
@@ -39,6 +79,7 @@
   `Prelude.WellFounded`.
 * Added `Data.List.Views` with views on `List` and their covering functions.
 * Added `Data.Nat.Views` with views on `Nat` and their covering functions.
+* Added `Data.Primitives.Views` with views on various primitive types and their covering functions.
 
 ## Miscellaneous updates
 
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -157,9 +157,9 @@
 
 * [Idris Wiki](https://github.com/idris-lang/Idris-dev/wiki);
 * [Zen Of Idris](https://github.com/idris-lang/Idris-dev/wiki/The-Zen-of-Idris);
-* Idris FAQs: [Official](http://www.idris-lang.org/documentation/faq/); [Unofficial](https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ);
+* Idris FAQs: [Official](https://idris.readthedocs.io/en/latest/faq/faq.html); [Unofficial](https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ);
 * [Idris Manual](https://github.com/idris-lang/Idris-dev/wiki/Manual);
-* [Idris Tutorial](http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf);
+* [Idris Tutorial](https://idris.readthedocs.io/en/latest/tutorial/index.html);
 * [Idris News](http://www.idris-lang.org/news/);
 * [other Idris docs](http://www.idris-lang.org/documentation/).
 * [Using Pull Requests](https://help.github.com/articles/using-pull-requests)
diff --git a/Setup.hs b/Setup.hs
--- a/Setup.hs
+++ b/Setup.hs
@@ -38,7 +38,8 @@
 -- Make Commands
 
 -- use GNU make on FreeBSD
-#if defined(freebsd_HOST_OS) || defined(dragonfly_HOST_OS)
+#if defined(freebsd_HOST_OS) || defined(dragonfly_HOST_OS)\
+    || defined(openbsd_HOST_OS) || defined(netbsd_HOST_OS)
 mymake = "gmake"
 #else
 mymake = "make"
diff --git a/codegen/idris-codegen-c/Main.hs b/codegen/idris-codegen-c/Main.hs
--- a/codegen/idris-codegen-c/Main.hs
+++ b/codegen/idris-codegen-c/Main.hs
@@ -40,7 +40,7 @@
                  mainProg <- if interface opts
                                 then liftM Just elabMain
                                 else return Nothing
-                 ir <- compile (Via "c") (output opts) mainProg
+                 ir <- compile (Via IBCFormat "c") (output opts) mainProg
                  runIO $ codegenC ir
 
 main :: IO ()
diff --git a/codegen/idris-codegen-javascript/Main.hs b/codegen/idris-codegen-javascript/Main.hs
--- a/codegen/idris-codegen-javascript/Main.hs
+++ b/codegen/idris-codegen-javascript/Main.hs
@@ -34,7 +34,7 @@
 jsMain opts = do elabPrims
                  loadInputs (inputs opts) Nothing
                  mainProg <- elabMain
-                 ir <- compile (Via "javascript") (output opts) (Just mainProg)
+                 ir <- compile (Via IBCFormat "javascript") (output opts) (Just mainProg)
                  runIO $ codegenJavaScript ir
 
 main :: IO ()
diff --git a/codegen/idris-codegen-node/Main.hs b/codegen/idris-codegen-node/Main.hs
--- a/codegen/idris-codegen-node/Main.hs
+++ b/codegen/idris-codegen-node/Main.hs
@@ -33,7 +33,7 @@
 jsMain opts = do elabPrims
                  loadInputs (inputs opts) Nothing
                  mainProg <- elabMain
-                 ir <- compile (Via "node") (output opts) (Just mainProg)
+                 ir <- compile (Via IBCFormat "node") (output opts) (Just mainProg)
                  runIO $ codegenNode ir
 
 main :: IO ()
diff --git a/idris.cabal b/idris.cabal
--- a/idris.cabal
+++ b/idris.cabal
@@ -1,5 +1,5 @@
 Name:           idris
-Version:        0.11.1
+Version:        0.11.2
 License:        BSD3
 License-file:   LICENSE
 Author:         Edwin Brady
@@ -115,6 +115,7 @@
                        libs/base/Control/Monad/*.idr
                        libs/base/Data/*.idr
                        libs/base/Data/Nat/*.idr
+                       libs/base/Data/Primitives/*.idr
                        libs/base/Data/List/*.idr
                        libs/base/Data/Vect/*.idr
                        libs/base/Data/String/*.idr
@@ -399,11 +400,6 @@
                        test/bignum002/*.idr
                        test/bignum002/expected
 
-                       test/classes001/*.idr
-                       test/classes001/run
-                       test/classes001/expected
-                       test/classes001/input
-
                        test/corecords001/*.idr
                        test/corecords001/run
                        test/corecords001/expected
@@ -414,6 +410,9 @@
                        test/directives001/*.idr
                        test/directives001/run
                        test/directives001/expected
+                       test/directives002/*.idr
+                       test/directives002/run
+                       test/directives002/expected
 
                        test/delab001/*.idr
                        test/delab001/run
@@ -609,6 +608,23 @@
                        test/interactive013/run
                        test/interactive013/*.idr
 
+                       test/interfaces001/*.idr
+                       test/interfaces001/run
+                       test/interfaces001/expected
+                       test/interfaces001/input
+                       test/interfaces002/*.idr
+                       test/interfaces002/run
+                       test/interfaces002/expected
+                       test/interfaces003/*.idr
+                       test/interfaces003/run
+                       test/interfaces003/expected
+                       test/interfaces004/*.idr
+                       test/interfaces004/run
+                       test/interfaces004/expected
+                       test/interfaces005/*.idr
+                       test/interfaces005/run
+                       test/interfaces005/expected
+
                        test/io001/run
                        test/io001/*.idr
                        test/io001/expected
@@ -1016,6 +1032,7 @@
                 , IRTS.Inliner
                 , IRTS.Lang
                 , IRTS.LangOpts
+                , IRTS.Portable
                 , IRTS.Simplified
                 , IRTS.System
 
@@ -1036,6 +1053,7 @@
                 , Tools_idris
 
   Build-depends:  base >=4 && <5
+                , aeson >= 0.6 && < 0.12
                 , annotated-wl-pprint >= 0.7 && < 0.8
                 , ansi-terminal < 0.7
                 , ansi-wl-pprint < 0.7
@@ -1072,7 +1090,7 @@
                 , vector-binary-instances < 0.3
                 , zip-archive > 0.2.3.5 && < 0.4
                 , safe
-                , fsnotify < 2.2
+                , fsnotify >= 0.2 && < 2.2
                 , async < 2.2
 
   -- zlib >= 0.6.1 is broken with GHC < 7.10.3
@@ -1090,19 +1108,14 @@
   ghc-prof-options: -auto-all -caf-all
 
   if os(linux)
-     cpp-options:   -DLINUX
      build-depends: unix < 2.8
   if os(freebsd)
-     cpp-options:   -DFREEBSD
      build-depends: unix < 2.8
 --   if os(dragonfly)
---      cpp-options:   -DDRAGONFLY
 --      build-depends: unix < 2.8
   if os(darwin)
-     cpp-options:   -DMACOSX
      build-depends: unix < 2.8
   if os(windows)
-     cpp-options:   -DWINDOWS
      build-depends: Win32 < 2.4
   if flag(FFI)
      build-depends: libffi < 0.2
diff --git a/libs/base/Data/Fin.idr b/libs/base/Data/Fin.idr
--- a/libs/base/Data/Fin.idr
+++ b/libs/base/Data/Fin.idr
@@ -127,6 +127,17 @@
 fromInteger {n} x {prf} with (integerToFin x n)
   fromInteger {n} x {prf = ItIsJust} | Just y = y
 
+||| Convert an Integer to a Fin in the required bounds/
+||| This is essentially a composition of `mod` and `fromInteger`
+export
+restrict : (n : Nat) -> Integer -> Fin (S n)
+restrict n val = let val' = assert_total (abs (mod val (cast (S n)))) in
+                     -- reasoning about primitives, so we need the
+                     -- 'believe_me'. It's fine because val' must be
+                     -- in the right range
+                     fromInteger val'
+                         {prf = believe_me {a=IsJust (Just val')} ItIsJust}
+
 %language ErrorReflection
 
 ||| Attempt to convert a reflected (fromInteger n) to a Nat
diff --git a/libs/base/Data/Primitives/Views.idr b/libs/base/Data/Primitives/Views.idr
new file mode 100644
--- /dev/null
+++ b/libs/base/Data/Primitives/Views.idr
@@ -0,0 +1,75 @@
+module Data.Primitives.Views
+
+-- We need all the believe_mes and asserts throughout this file because we're
+-- working with primitive here! We also have separate implementations per
+-- primitive, rather than using interfaces, because we're only going to trust
+-- the primitive implementations.
+
+namespace Integer
+  ||| View for expressing a number as a multiplication + a remainder
+  public export
+  data Divides : Integer -> (d : Integer) -> Type where
+       DivByZero : Divides x 0
+       DivBy : (prf : rem >= 0 && rem < d = True) ->
+               Divides ((d * div) + rem) d
+    
+  ||| Covering function for the `Divides` view
+  export
+  divides : (val : Integer) -> (d : Integer) -> Divides val d
+  divides val 0 = DivByZero
+  divides val d
+         = let dividend = if d < 0 then -(val `div` abs d)
+                                   else val `div` d
+               remainder = val `mod` d in
+               believe_me (DivBy {d} {div = dividend} {rem = remainder}
+                                 (believe_me (Refl {x = True})))
+
+  ||| View for recursion over Integers
+  data IntegerRec : Integer -> Type where
+       IntegerZ : IntegerRec 0
+       IntegerSucc : IntegerRec (n - 1) -> IntegerRec n
+       IntegerPred : IntegerRec ((-n) + 1) -> IntegerRec (-n)
+  
+  ||| Covering function for `IntegerRec`
+  integerRec : (x : Integer) -> IntegerRec x
+  integerRec 0 = IntegerZ
+  integerRec x = if x > 0 then IntegerSucc (assert_total (integerRec (x - 1)))
+                      else believe_me (IntegerPred {n=-x} 
+                                (assert_total (believe_me (integerRec (x + 1)))))
+
+namespace Int
+  ||| View for expressing a number as a multiplication + a remainder
+  public export
+  data Divides : Int -> (d : Int) -> Type where
+       DivByZero : Int.Divides x 0
+       DivBy : (prf : rem >= 0 && rem < d = True) ->
+               Int.Divides ((d * div) + rem) d
+   
+  -- I have assumed, but not actually verified, that this will still
+  -- give a right result (i.e. still adding up) when the Ints overflow.
+  -- TODO: Someone please check this and fix if necessary...
+
+  ||| Covering function for the `Divides` view
+  export
+  divides : (val : Int) -> (d : Int) -> Divides val d
+  divides val 0 = DivByZero
+  divides val d
+         = let dividend = if d < 0 then -(val `div` abs d)
+                                   else val `div` d
+               remainder = val `mod` d in
+               believe_me (DivBy {d} {div = dividend} {rem = remainder}
+                                 (believe_me (Refl {x = True})))
+
+  ||| View for recursion over Ints
+  data IntRec : Int -> Type where
+       IntZ : IntRec 0
+       IntSucc : IntRec (n - 1) -> IntRec n
+       IntPred : IntRec ((-n) + 1) -> IntRec (-n)
+  
+  ||| Covering function for `IntRec`
+  intRec : (x : Int) -> IntRec x
+  intRec 0 = IntZ
+  intRec x = if x > 0 then IntSucc (assert_total (intRec (x - 1)))
+                      else believe_me (IntPred {n=-x}
+                                (assert_total (believe_me (intRec (x + 1)))))
+  
diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg
--- a/libs/base/base.ipkg
+++ b/libs/base/base.ipkg
@@ -19,6 +19,7 @@
           Data.Erased, Data.List, Data.List.Views,
           Data.List.Quantifiers,
           Data.Nat.Views,
+          Data.Primitives.Views,
           Data.String.Views,
           Data.So, Data.String,
 
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
@@ -28,7 +28,7 @@
   applicativeHomomorphism : (x : a) -> (g : a -> b) ->
                             (<*>) {f} (pure g) (pure x) = pure {f} (g x)
   applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
-                           g <*> pure x = pure (\g' : a -> b => g' x) <*> g
+                           g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g
 
 interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
   monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
diff --git a/libs/contrib/Network/Socket.idr b/libs/contrib/Network/Socket.idr
--- a/libs/contrib/Network/Socket.idr
+++ b/libs/contrib/Network/Socket.idr
@@ -273,6 +273,7 @@
 freeRecvfromStruct : RecvfromStructPtr -> IO ()
 freeRecvfromStruct (RFPtr p) = foreign FFI_C "idrnet_free_recvfrom_struct" (Ptr -> IO ()) p
 
+export
 recv : Socket -> Int -> IO (Either SocketError (String, ByteLength))
 recv sock len = do
   -- Firstly make the request, get some kind of recv structure which
@@ -309,6 +310,7 @@
   else
     return $ Right recv_res
 
+export
 sendTo : Socket -> SocketAddress -> Port -> String -> IO (Either SocketError ByteLength)
 sendTo sock addr p dat = do
   sendto_res <- foreign FFI_C "idrnet_sendto"
@@ -344,6 +346,7 @@
   port <- foreign FFI_C "idrnet_sockaddr_ipv4_port" (Ptr -> IO Int) sockaddr_ptr
   return port
 
+export
 recvFrom : Socket -> ByteLength -> IO (Either SocketError (UDPAddrInfo, String, ByteLength))
 recvFrom sock bl = do
   recv_ptr <- foreign FFI_C "idrnet_recvfrom" (Int -> Int -> IO Ptr)
diff --git a/libs/prelude/Builtins.idr b/libs/prelude/Builtins.idr
--- a/libs/prelude/Builtins.idr
+++ b/libs/prelude/Builtins.idr
@@ -106,38 +106,41 @@
 trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c
 trans Refl Refl = Refl
 
-||| There are two types of laziness: that arising from lazy functions, and that
-||| arising from codata. They differ in their totality condition.
-data LazyType = LazyCodata | LazyEval
+||| Two types of delayed computation: that arising from lazy functions, and that
+||| arising from infinite data. They differ in their totality condition.
+data DelayReason = Infinite | LazyValue
 
 ||| The underlying implementation of Lazy and Inf.
 %error_reverse
-data Lazy' : LazyType -> Type -> Type where
+data Delayed : DelayReason -> Type -> Type where
      ||| A delayed computation.
      |||
      ||| Delay is inserted automatically by the elaborator where necessary.
      |||
      ||| Note that compiled code gives `Delay` special semantics.
-     ||| @ t   whether this is laziness from codata or normal lazy evaluation
+     ||| @ t   whether this is laziness from an infinite structure or lazy evaluation
      ||| @ a   the type of the eventual value
      ||| @ val a computation that will produce a value
-     Delay : {t, a : _} -> (val : a) -> Lazy' t a
+     Delay : {t, a : _} -> (val : a) -> Delayed t a
 
 ||| Compute a value from a delayed computation.
 |||
 ||| Inserted by the elaborator where necessary.
-Force : {t, a : _} -> Lazy' t a -> a
+Force : {t, a : _} -> Delayed t a -> a
 Force (Delay x) = x
 
-||| Lazily evaluated values. This has special evaluation semantics.
+||| Lazily evaluated values. 
+||| At run time, the delayed value will only be computed when required by
+||| a case split.
 Lazy : Type -> Type
-Lazy t = Lazy' LazyEval t
+Lazy t = Delayed LazyValue t
 
-||| Recursive parameters to codata. Inserted automatically by the elaborator
-||| on a "codata" definition but is necessary by hand if mixing inductive and
-||| coinductive parameters.
+||| Possibly infinite data. 
+||| A value which may be infinite is accepted by the totality checker if
+||| it appears under a data constructor. At run time, the delayed value will
+||| only be computed when required by a case split.
 Inf : Type -> Type
-Inf t = Lazy' LazyCodata t
+Inf t = Delayed Infinite t
 
 namespace Ownership
   ||| A read-only version of a unique value
diff --git a/libs/prelude/Prelude/File.idr b/libs/prelude/Prelude/File.idr
--- a/libs/prelude/Prelude/File.idr
+++ b/libs/prelude/Prelude/File.idr
@@ -233,7 +233,7 @@
                        return (p > 0)
 
 ||| Read the contents of a file into a string
-partial -- might be reading something infinitely long like /dev/null ...
+-- might be reading something infinitely long like /dev/null ...
 covering export
 readFile : String -> IO (Either FileError String)
 readFile fn = do Right h <- openFile fn Read
@@ -242,7 +242,7 @@
                  closeFile h
                  return c
   where
-    partial
+    covering
     readFile' : File -> String -> IO (Either FileError String)
     readFile' h contents =
        do x <- fEOF h
diff --git a/libs/prelude/Prelude/Stream.idr b/libs/prelude/Prelude/Stream.idr
--- a/libs/prelude/Prelude/Stream.idr
+++ b/libs/prelude/Prelude/Stream.idr
@@ -13,8 +13,8 @@
 %default total
 
 ||| An infinite stream
-codata Stream : Type -> Type where
-  (::) : (e : a) -> Stream a -> Stream a
+data Stream : Type -> Type where
+  (::) : (e : a) -> Inf (Stream a) -> Stream a
 
 -- Hints for interactive editing
 %name Stream xs,ys,zs,ws
diff --git a/rts/idris_gc.c b/rts/idris_gc.c
--- a/rts/idris_gc.c
+++ b/rts/idris_gc.c
@@ -4,7 +4,7 @@
 #include <assert.h>
 
 VAL copy(VM* vm, VAL x) {
-    int i, ar;
+    int ar;
     Closure* cl = NULL;
     if (x==NULL || ISINT(x)) {
         return x;
@@ -16,9 +16,7 @@
             return x;
         } else {
             allocCon(cl, vm, CTAG(x), ar, 1);
-            for(i = 0; i < ar; ++i) {
-                cl->info.c.args[i] = x->info.c.args[i];
-            }
+            memcpy(&(cl->info.c.args), &(x->info.c.args), sizeof(VAL)*ar);
         }
         break;
     case CT_FLOAT:
diff --git a/rts/idris_main.c b/rts/idris_main.c
--- a/rts/idris_main.c
+++ b/rts/idris_main.c
@@ -4,7 +4,7 @@
 #include "idris_gmp.h"
 // The default options should give satisfactory results under many circumstances.
 RTSOpts opts = { 
-    .init_heap_size = 4096000,
+    .init_heap_size = 16384000,
     .max_stack_size = 4096000,
     .show_summary   = 0
 };
diff --git a/rts/idris_rts.c b/rts/idris_rts.c
--- a/rts/idris_rts.c
+++ b/rts/idris_rts.c
@@ -391,20 +391,6 @@
     return cl;
 }
 
-void PROJECT(VM* vm, VAL r, int loc, int arity) {
-    int i;
-    for(i = 0; i < arity; ++i) {
-        LOC(i+loc) = r->info.c.args[i];
-    }
-}
-
-void SLIDE(VM* vm, int args) {
-    int i;
-    for(i = 0; i < args; ++i) {
-        LOC(i) = TOP(i);
-    }
-}
-
 void dumpStack(VM* vm) {
     int i = 0;
     VAL* root;
diff --git a/rts/idris_rts.h b/rts/idris_rts.h
--- a/rts/idris_rts.h
+++ b/rts/idris_rts.h
@@ -259,8 +259,10 @@
 #define SETARG(x, i, a) ((x)->info.c.args)[i] = ((VAL)(a))
 #define GETARG(x, i) ((x)->info.c.args)[i]
 
-void PROJECT(VM* vm, VAL r, int loc, int arity);
-void SLIDE(VM* vm, int args);
+#define PROJECT(vm,r,loc,num) \
+    memcpy(&(LOC(loc)), &((r)->info.c.args), sizeof(VAL)*num)
+#define SLIDE(vm, args) \
+    memcpy(&(LOC(0)), &(TOP(0)), sizeof(VAL)*args)
 
 void* allocate(size_t size, int outerlock);
 // void* allocCon(VM* vm, int arity, int outerlock);
diff --git a/src/IRTS/Compiler.hs b/src/IRTS/Compiler.hs
--- a/src/IRTS/Compiler.hs
+++ b/src/IRTS/Compiler.hs
@@ -12,6 +12,7 @@
 import IRTS.CodegenJavaScript
 import IRTS.Inliner
 import IRTS.Exports
+import IRTS.Portable
 
 import Idris.AbsSyntax
 import Idris.AbsSyntaxTree
@@ -125,13 +126,21 @@
 generate codegen mainmod ir
   = case codegen of
        -- Built-in code generators (FIXME: lift these out!)
-       Via "c" -> codegenC ir
+       Via _ "c" -> codegenC ir
        -- Any external code generator
-       Via cg -> do let cmd = "idris-codegen-" ++ cg
-                        args = [mainmod, "-o", outputFile ir] ++ compilerFlags ir
-                    exit <- rawSystem cmd args
-                    when (exit /= ExitSuccess) $
-                       putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)
+       Via fm cg -> do input <- case fm of
+                                    IBCFormat -> return mainmod
+                                    JSONFormat -> do
+                                        tempdir <- getTemporaryDirectory
+                                        (fn, h) <- openTempFile tempdir "idris-cg.json"
+                                        writePortable h ir
+                                        hClose h
+                                        return fn
+                       let cmd = "idris-codegen-" ++ cg
+                           args = [input, "-o", outputFile ir] ++ compilerFlags ir
+                       exit <- rawSystem cmd args
+                       when (exit /= ExitSuccess) $
+                            putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)
        Bytecode -> dumpBC (simpleDecls ir) (outputFile ir)
 
 irMain :: TT Name -> Idris LDecl
@@ -350,7 +359,7 @@
 
             -- overapplied
             GT  -> ifail ("overapplied data constructor: " ++ show tm ++
-                          "\nDEBUG INFO:\n" ++ 
+                          "\nDEBUG INFO:\n" ++
                           "Arity: " ++ show arity ++ "\n" ++
                           "Arguments: " ++ show args ++ "\n" ++
                           "Pruned arguments: " ++ show argsPruned)
@@ -439,7 +448,7 @@
             | otherwise = n
 
         used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
-        fst4 (x,_,_,_) = x
+        fst4 (x,_,_,_,_) = x
 
 irTerm vs env (P _ n _) = return $ LV (Glob n)
 irTerm vs env (V i)
diff --git a/src/IRTS/Defunctionalise.hs b/src/IRTS/Defunctionalise.hs
--- a/src/IRTS/Defunctionalise.hs
+++ b/src/IRTS/Defunctionalise.hs
@@ -51,8 +51,9 @@
            newacons = sortBy conord $ concatMap (toConsA anames') (getFn all)
            eval = mkEval newecons
            app = mkApply newacons
+           app2 = mkApply2 newacons
            condecls = declare nexttag (newecons ++ newacons) in
-           addAlist (eval : app : condecls ++ allD) emptyContext
+           addAlist (eval : app : app2 : condecls ++ allD) emptyContext
    where conord (n, _, _) (n', _, _) = compare n n'
 
 getFn :: [(Name, LDecl)] -> [(Name, Int)]
@@ -152,6 +153,8 @@
              = return $ chainAPPLY (DApp False n (take ar args)) (drop ar args)
 
     chainAPPLY f [] = f
+--     chainAPPLY f (a : b : as) 
+--          = chainAPPLY (DApp False (sMN 0 "APPLY2") [f, a, b]) as
     chainAPPLY f (a : as) = chainAPPLY (DApp False (sMN 0 "APPLY") [f, a]) as
 
     -- if anything in the DExp is projected from, we'll need to evaluate it,
@@ -184,6 +187,7 @@
 
 data EvalApply a = EvalCase (Name -> a)
                  | ApplyCase a
+                 | Apply2Case a
 
 -- For a function name, generate a list of
 -- data constuctors, and whether to handle them in EVAL or APPLY
@@ -219,7 +223,15 @@
                   (DApp False (mkUnderCon fname (ar - (n + 1)))
                        (map (DV . Glob) (take n (genArgs 0) ++
                          [sMN 0 "arg"])))))
-                            : mkApplyCase fname (n + 1) ar
+                            : 
+              if (ar - (n + 2) >=0 )
+                 then (nm, n, Apply2Case (DConCase (-1) nm (take n (genArgs 0))
+                      (DApp False (mkUnderCon fname (ar - (n + 2)))
+                       (map (DV . Glob) (take n (genArgs 0) ++
+                         [sMN 0 "arg0", sMN 0 "arg1"])))))
+                            :
+                            mkApplyCase fname (n + 1) ar
+                 else mkApplyCase fname (n + 1) ar
 
 mkEval :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)
 mkEval xs = (sMN 0 "EVAL", DFun (sMN 0 "EVAL") [sMN 0 "arg"]
@@ -241,6 +253,25 @@
                                     [DDefaultCase DNothing])))
   where
     applyCase (n, t, ApplyCase x) = Just x
+    applyCase _ = Nothing
+
+mkApply2 :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)
+mkApply2 xs = (sMN 0 "APPLY2", DFun (sMN 0 "APPLY2") [sMN 0 "fn", sMN 0 "arg0", sMN 0 "arg1"]
+                             (case mapMaybe applyCase xs of
+                                [] -> DNothing
+                                cases ->
+                                    mkBigCase (sMN 0 "APPLY") 256
+                                               (DV (Glob (sMN 0 "fn")))
+                                              (cases ++
+                                    [DDefaultCase 
+                                       (DApp False (sMN 0 "APPLY")
+                                       [DApp False (sMN 0 "APPLY")
+                                              [DV (Glob (sMN 0 "fn")),
+                                               DV (Glob (sMN 0 "arg0"))],
+                                               DV (Glob (sMN 0 "arg1"))])
+                                               ])))
+  where
+    applyCase (n, t, Apply2Case x) = Just x
     applyCase _ = Nothing
 
 
diff --git a/src/IRTS/Portable.hs b/src/IRTS/Portable.hs
new file mode 100644
--- /dev/null
+++ b/src/IRTS/Portable.hs
@@ -0,0 +1,277 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module IRTS.Portable (writePortable) where
+
+import Data.Aeson
+import qualified Data.ByteString.Lazy as B
+import qualified Data.Text as T
+
+import Idris.Core.CaseTree
+import Idris.Core.TT
+
+import IRTS.Bytecode
+import IRTS.CodegenCommon
+import IRTS.Defunctionalise
+import IRTS.Lang
+import IRTS.Simplified
+
+import System.IO
+
+data CodegenFile = CGFile {
+    fileType :: String,
+    version :: Int,
+    cgInfo :: CodegenInfo
+}
+
+-- Update the version when the format changes
+formatVersion :: Int
+formatVersion = 1
+
+writePortable :: Handle -> CodegenInfo -> IO ()
+writePortable file ci = do
+    let json = encode $ CGFile "idris-codegen" formatVersion ci
+    B.hPut file json
+
+instance ToJSON CodegenFile where
+    toJSON (CGFile ft v ci) = object ["file-type" .= ft,
+                                      "version" .= v,
+                                      "codegen-info" .= toJSON ci]
+
+instance ToJSON CodegenInfo where
+    toJSON ci = object ["output-file" .= (outputFile ci),
+                        "includes" .= (includes ci),
+                        "import-dirs" .= (importDirs ci),
+                        "compile-objs" .= (compileObjs ci),
+                        "compile-libs" .= (compileLibs ci),
+                        "compiler-flags" .= (compilerFlags ci),
+                        "interfaces" .= (interfaces ci),
+                        "exports" .= (exportDecls ci),
+                        "lift-decls" .= (liftDecls ci),
+                        "defun-decls" .= (defunDecls ci),
+                        "simple-decls" .= (simpleDecls ci),
+                        "bytecode" .= (map toBC (simpleDecls ci))]
+
+instance ToJSON Name where
+    toJSON n = toJSON $ showCG n
+
+instance ToJSON ExportIFace where
+    toJSON (Export n f xs) = object ["ffi-desc" .= n,
+                                     "interface-file" .= f,
+                                     "exports" .= xs]
+
+instance ToJSON FDesc where
+    toJSON (FCon n) = object ["FCon" .= n]
+    toJSON (FStr s) = object ["FStr" .= s]
+    toJSON (FUnknown) = object ["FUnknown" .= Null]
+    toJSON (FIO fd) = object ["FIO" .= fd]
+    toJSON (FApp n xs) = object ["FApp" .= (n, xs)]
+
+instance ToJSON Export where
+    toJSON (ExportData fd) = object ["ExportData" .= fd]
+    toJSON (ExportFun n dsc ret args) = object ["ExportFun" .= (n, dsc, ret, args)]
+
+instance ToJSON LDecl where
+    toJSON (LFun opts name args def) = object ["LFun" .= (opts, name, args, def)]
+    toJSON (LConstructor name tag ar) = object ["LConstructor" .= (name, tag, ar)]
+
+instance ToJSON LOpt where
+    toJSON Inline = String "Inline"
+    toJSON NoInline = String "NoInline"
+
+instance ToJSON LExp where
+    toJSON (LV lv) = object ["LV" .= lv]
+    toJSON (LApp tail exp args) = object ["LApp" .= (tail, exp, args)]
+    toJSON (LLazyApp name exps) = object ["LLazyApp" .= (name, exps)]
+    toJSON (LLazyExp exp) = object ["LLazyExp" .= exp]
+    toJSON (LForce exp) = object ["LForce" .= exp]
+    toJSON (LLet name a b) = object ["LLet" .= (name, a, b)]
+    toJSON (LLam args exp) = object ["LLam" .= (args, exp)]
+    toJSON (LProj exp i) = object ["LProj" .= (exp, i)]
+    toJSON (LCon lv i n exps) = object ["LCon" .= (lv, i, n, exps)]
+    toJSON (LCase ct exp alts) = object ["LCase" .= (ct, exp, alts)]
+    toJSON (LConst c) = object ["LConst" .= c]
+    toJSON (LForeign fd ret exps) = object ["LForeign" .= (fd, ret, exps)]
+    toJSON (LOp prim exps) = object ["LOp" .= (prim, exps)]
+    toJSON LNothing = object ["LNothing" .= Null]
+    toJSON (LError s) = object ["LError" .= s]
+
+instance ToJSON LVar where
+    toJSON (Loc i) = object ["Loc" .= i]
+    toJSON (Glob n) = object ["Glob" .= n]
+
+instance ToJSON CaseType where
+    toJSON Updatable = String "Updatable"
+    toJSON Shared = String "Shared"
+
+instance ToJSON LAlt where
+    toJSON (LConCase i n ns exp) = object ["LConCase" .= (i, n, ns, exp)]
+    toJSON (LConstCase c exp) = object ["LConstCase" .= (c, exp)]
+    toJSON (LDefaultCase exp) = object ["LDefaultCase" .= exp]
+
+instance ToJSON Const where
+    toJSON (I i) = object ["int" .= i]
+    toJSON (BI i) = object ["bigint" .= (show i)]
+    toJSON (Fl d) = object ["double" .= d]
+    toJSON (Ch c) = object ["char" .= (show c)]
+    toJSON (Str s) = object ["string" .= s]
+    toJSON (B8 b) = object ["bits8" .= b]
+    toJSON (B16 b) = object ["bits16" .= b]
+    toJSON (B32 b) = object ["bits32" .= b]
+    toJSON (B64 b) = object ["bits64" .= b]
+    toJSON (AType at) = object ["atype" .= at]
+    toJSON StrType = object ["strtype" .= Null]
+    toJSON WorldType = object ["worldtype" .= Null]
+    toJSON TheWorld = object ["theworld" .= Null]
+    toJSON VoidType = object ["voidtype" .= Null]
+    toJSON Forgot = object ["forgot" .= Null]
+
+instance ToJSON ArithTy where
+    toJSON (ATInt it) = object ["ATInt" .= it]
+    toJSON ATFloat = object ["ATFloat" .= Null]
+
+instance ToJSON IntTy where
+    toJSON it = toJSON $ intTyName it
+
+instance ToJSON PrimFn where
+    toJSON (LPlus aty) = object ["LPlus" .= aty]
+    toJSON (LMinus aty) = object ["LMinus" .= aty]
+    toJSON (LTimes aty) = object ["LTimes" .= aty]
+    toJSON (LUDiv aty) = object ["LUDiv" .= aty]
+    toJSON (LSDiv aty) = object ["LSDiv" .= aty]
+    toJSON (LAnd ity) = object ["LAnd" .= ity]
+    toJSON (LOr ity) = object ["LOr" .= ity]
+    toJSON (LXOr ity) = object ["LXOr" .= ity]
+    toJSON (LCompl ity) = object ["LCompl" .= ity]
+    toJSON (LSHL ity) = object ["LSHL" .= ity]
+    toJSON (LLSHR ity) = object ["LLSHR" .= ity]
+    toJSON (LASHR ity) = object ["LASHR" .= ity]
+    toJSON (LEq aty) = object ["LEq" .= aty]
+    toJSON (LLt ity) = object ["LLt" .= ity]
+    toJSON (LLe ity) = object ["LLe" .= ity]
+    toJSON (LGt ity) = object ["LGt" .= ity]
+    toJSON (LGe ity) = object ["LGe" .= ity]
+    toJSON (LSLt aty) = object ["LSLt" .= aty]
+    toJSON (LSLe aty) = object ["LSLe" .= aty]
+    toJSON (LSGt aty) = object ["LSGt" .= aty]
+    toJSON (LSGe aty) = object ["LSGe" .= aty]
+    toJSON (LZExt from to) = object ["LZExt" .= (from, to)]
+    toJSON (LSExt from to) = object ["LSExt" .= (from, to)]
+    toJSON (LTrunc from to) = object ["LTrunc" .= (from, to)]
+    toJSON LStrConcat = object ["LStrConcat" .= Null]
+    toJSON LStrLt = object ["LStrLt" .= Null]
+    toJSON LStrEq = object ["LStrEq" .= Null]
+    toJSON LStrLen = object ["LStrLen" .= Null]
+    toJSON (LIntFloat ity) = object ["LIntFloat" .= ity]
+    toJSON (LFloatInt ity) = object ["LFloatInt" .= ity]
+    toJSON (LIntStr ity) = object ["LIntStr" .= ity]
+    toJSON (LStrInt ity) = object ["LStrInt" .= ity]
+    toJSON (LIntCh ity) = object ["LIntCh" .= ity]
+    toJSON (LChInt ity) = object ["LChInt" .= ity]
+    toJSON LFloatStr = object ["LFloatStr" .= Null]
+    toJSON LStrFloat = object ["LStrFloat" .= Null]
+    toJSON (LBitCast from to) = object ["LBitCast" .= (from, to)]
+    toJSON LFExp = object ["LFExp" .= Null]
+    toJSON LFLog = object ["LFLog" .= Null]
+    toJSON LFSin = object ["LFSin" .= Null]
+    toJSON LFCos = object ["LFCos" .= Null]
+    toJSON LFTan = object ["LFTan" .= Null]
+    toJSON LFASin = object ["LFASin" .= Null]
+    toJSON LFACos = object ["LFACos" .= Null]
+    toJSON LFATan = object ["LFATan" .= Null]
+    toJSON LFSqrt = object ["LFSqrt" .= Null]
+    toJSON LFFloor = object ["LFFloor" .= Null]
+    toJSON LFCeil = object ["LFCeil" .= Null]
+    toJSON LFNegate = object ["LFNegate" .= Null]
+    toJSON LStrHead = object ["LStrHead" .= Null]
+    toJSON LStrTail = object ["LStrTail" .= Null]
+    toJSON LStrCons = object ["LStrCons" .= Null]
+    toJSON LStrIndex = object ["LStrIndex" .= Null]
+    toJSON LStrRev = object ["LStrRev" .= Null]
+    toJSON LStrSubstr = object ["LStrSubstr" .= Null]
+    toJSON LReadStr = object ["LReadStr" .= Null]
+    toJSON LWriteStr = object ["LWriteStr" .= Null]
+    toJSON LSystemInfo = object ["LSystemInfo" .= Null]
+    toJSON LFork = object ["LFork" .= Null]
+    toJSON LPar = object ["LPar" .= Null]
+    toJSON (LExternal name) = object ["LExternal" .= name]
+    toJSON LNoOp = object ["LNoOp" .= Null]
+
+
+
+
+
+instance ToJSON DDecl where
+    toJSON (DFun name args exp) = object ["DFun" .= (name, args, exp)]
+    toJSON (DConstructor name tag arity) = object ["DConstructor" .= (name, tag, arity)]
+
+instance ToJSON DExp where
+    toJSON (DV lv) = object ["DV" .= lv]
+    toJSON (DApp tail name exps) = object ["DApp" .= (tail, name, exps)]
+    toJSON (DLet name a b) = object ["DLet" .= (name, a, b)]
+    toJSON (DUpdate name exp) = object ["DUpdate" .= (name,exp)]
+    toJSON (DProj exp i) = object ["DProj" .= (exp, i)]
+    toJSON (DC lv i name exp) = object ["DC" .= (lv, i, name, exp)]
+    toJSON (DCase ct exp alts) = object ["DCase" .= (ct, exp, alts)]
+    toJSON (DChkCase exp alts) = object ["DChkCase" .= (exp, alts)]
+    toJSON (DConst c) = object ["DConst" .= c]
+    toJSON (DForeign fd ret exps) = object ["DForeign" .= (fd, ret, exps)]
+    toJSON (DOp prim exps) = object ["DOp" .= (prim, exps)]
+    toJSON DNothing = object ["DNothing" .= Null]
+    toJSON (DError s) = object ["DError" .= s]
+
+instance ToJSON DAlt where
+    toJSON (DConCase i n ns exp) = object ["DConCase" .= (i, n, ns, exp)]
+    toJSON (DConstCase c exp) = object ["DConstCase" .= (c, exp)]
+    toJSON (DDefaultCase exp) = object ["DDefaultCase" .= exp]
+
+instance ToJSON SDecl where
+    toJSON (SFun name args i exp) = object ["SFun" .= (name, args, i, exp)]
+
+instance ToJSON SExp where
+    toJSON (SV lv) = object ["SV" .= lv]
+    toJSON (SApp tail name exps) = object ["SApp" .= (tail, name, exps)]
+    toJSON (SLet lv a b) = object ["SLet" .= (lv, a, b)]
+    toJSON (SUpdate lv exp) = object ["SUpdate" .= (lv, exp)]
+    toJSON (SProj lv i) = object ["DProj" .= (lv, i)]
+    toJSON (SCon lv i name vars) = object ["SCon" .= (lv, i, name, vars)]
+    toJSON (SCase ct lv alts) = object ["SCase" .= (ct, lv, alts)]
+    toJSON (SChkCase lv alts) = object ["DChkCase" .= (lv, alts)]
+    toJSON (SConst c) = object ["SConst" .= c]
+    toJSON (SForeign fd ret exps) = object ["SForeign" .= (fd, ret, exps)]
+    toJSON (SOp prim vars) = object ["DOp" .= (prim, vars)]
+    toJSON SNothing = object ["SNothing" .= Null]
+    toJSON (SError s) = object ["SError" .= s]
+
+instance ToJSON SAlt where
+    toJSON (SConCase i j n ns exp) = object ["SConCase" .= (i, j, n, ns, exp)]
+    toJSON (SConstCase c exp) = object ["SConstCase" .= (c, exp)]
+    toJSON (SDefaultCase exp) = object ["SDefaultCase" .= exp]
+
+instance ToJSON BC where
+    toJSON (ASSIGN r1 r2) = object ["ASSIGN" .= (r1, r2)]
+    toJSON (ASSIGNCONST r c) = object ["ASSIGNCONST" .= (r, c)]
+    toJSON (UPDATE r1 r2) = object ["UPDATE" .= (r1, r2)]
+    toJSON (MKCON con mr i regs) = object ["MKCON" .= (con, mr, i, regs)]
+    toJSON (CASE b r alts def) = object ["CASE" .= (b, r, alts, def)]
+    toJSON (PROJECT r loc arity) = object ["PROJECT" .= (r, loc, arity)]
+    toJSON (PROJECTINTO r1 r2 loc) = object ["PROJECTINTO" .= (r1, r2, loc)]
+    toJSON (CONSTCASE r alts def) = object ["CONSTCASE" .= (r, alts, def)]
+    toJSON (CALL name) = object ["CALL" .= name]
+    toJSON (TAILCALL name) = object ["TAILCALL" .= name]
+    toJSON (FOREIGNCALL r fd ret exps) = object ["FOREIGNCALL" .= (r, fd, ret, exps)]
+    toJSON (SLIDE i) = object ["SLIDE" .= i]
+    toJSON (RESERVE i) = object ["RESERVE" .= i]
+    toJSON (ADDTOP i) = object ["ADDTOP" .= i]
+    toJSON (TOPBASE i) = object ["TOPBASE" .= i]
+    toJSON (BASETOP i) = object ["BASETOP" .= i]
+    toJSON REBASE = object ["REBASE" .= Null]
+    toJSON STOREOLD = object ["STOREOLD" .= Null]
+    toJSON (OP r prim args) = object ["OP" .= (r, prim, args)]
+    toJSON (NULL r) = object ["NULL" .= r]
+    toJSON (ERROR s) = object ["ERROR" .= s]
+
+instance ToJSON Reg where
+    toJSON RVal = object ["RVal" .= Null]
+    toJSON (T i) = object ["T" .= i]
+    toJSON (L i) = object ["L" .= i]
+    toJSON Tmp = object ["Tmp" .= Null]
diff --git a/src/IRTS/System.hs b/src/IRTS/System.hs
--- a/src/IRTS/System.hs
+++ b/src/IRTS/System.hs
@@ -29,7 +29,8 @@
 getTargetDir :: IO String
 getTargetDir = overrideDataDirWith "TARGET"
 
-#if defined(FREEBSD) || defined(DRAGONFLY)
+#if defined(freebsd_HOST_OS) || defined(dragonfly_HOST_OS)\
+    || defined(openbsd_HOST_OS) || defined(netbsd_HOST_OS)
 extraLib = ["-L/usr/local/lib"]
 extraInclude = ["-I/usr/local/include"]
 #else
diff --git a/src/Idris/ASTUtils.hs b/src/Idris/ASTUtils.hs
--- a/src/Idris/ASTUtils.hs
+++ b/src/Idris/ASTUtils.hs
@@ -138,7 +138,7 @@
 -------------
 -- This has a terrible name, but I'm not sure of a better one that isn't
 -- confusingly close to tt_ctxt
-known_terms :: Field IState (Ctxt (Def, Accessibility, Totality, MetaInformation))
+known_terms :: Field IState (Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation))
 known_terms = Field (definitions . tt_ctxt)
                     (\v state -> state {tt_ctxt = (tt_ctxt state) {definitions = v}})
 
diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs
--- a/src/Idris/AbsSyntax.hs
+++ b/src/Idris/AbsSyntax.hs
@@ -45,7 +45,11 @@
 getContext = do i <- getIState; return (tt_ctxt i)
 
 forCodegen :: Codegen -> [(Codegen, a)] -> [a]
-forCodegen tgt xs = [x | (tgt', x) <- xs, tgt == tgt']
+forCodegen tgt xs = [x | (tgt', x) <- xs, eqLang tgt tgt']
+    where
+        eqLang (Via _ x) (Via _ y) = x == y
+        eqLang Bytecode Bytecode = True
+        eqLang _ _ = False
 
 getObjectFiles :: Codegen -> Idris [FilePath]
 getObjectFiles tgt = do i <- getIState; return (forCodegen tgt $ idris_objs i)
@@ -218,6 +222,12 @@
               let ctxt = setTotal n a (tt_ctxt i)
               putIState $ i { tt_ctxt = ctxt }
 
+setInjectivity :: Name -> Injectivity -> Idris ()
+setInjectivity n a
+         = do i <- getIState
+              let ctxt = setInjective n a (tt_ctxt i)
+              putIState $ i { tt_ctxt = ctxt }
+
 getTotality :: Name -> Idris Totality
 getTotality n
          = do i <- getIState
@@ -446,6 +456,33 @@
         chaser (NS n _) = chaser n
         chaser _ = False
 
+-- Add a privileged implementation - one which instance search will happily
+-- resolve immediately if it is type correct
+-- This is used for naming parent implementations when defining an
+-- implementation with constraints.
+-- Returns the old list, so we can revert easily at the end of a block
+
+addOpenImpl :: [Name] -> Idris [Name]
+addOpenImpl ns = do ist <- getIState
+                    ns' <- mapM (checkValid ist) ns
+                    let open = idris_openimpls ist
+                    putIState $ ist { idris_openimpls = nub (ns' ++ open) }
+                    return open
+  where
+    checkValid ist n
+      = case lookupCtxtName n (idris_implicits ist) of
+             [(n', _)] -> return n'
+             []        -> throwError (NoSuchVariable n)
+             more      -> throwError (CantResolveAlts (map fst more))
+
+setOpenImpl :: [Name] -> Idris ()
+setOpenImpl ns = do ist <- getIState
+                    putIState $ ist { idris_openimpls = ns }
+
+getOpenImpl :: Idris [Name]
+getOpenImpl = do ist <- getIState
+                 return (idris_openimpls ist)
+
 addClass :: Name -> ClassInfo -> Idris ()
 addClass n i
    = do ist <- getIState
@@ -913,6 +950,7 @@
 codegen = do i <- getIState
              return (opt_codegen (idris_options i))
 
+
 setOutputTy :: OutputType -> Idris ()
 setOutputTy t = do i <- getIState
                    let opts = idris_options i
@@ -1249,7 +1287,7 @@
     updateps yn nm [] = []
     updateps yn nm (((a, t), i):as)
         | (a `elem` nm) == yn = (a, t) : updateps yn nm as
-        | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as
+        | otherwise = (sMN i (show a ++ "_shadow"), t) : updateps yn nm as
 
     removeBound lhs ns = ns \\ nub (bnames lhs)
 
@@ -1290,19 +1328,28 @@
            (map (expandParamsD rhs ist dec ps ns) decls)
            cn
            cd
-expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs acc opts n nfc params ty cn decls)
-   = PInstance doc argDocs info f
+expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
+   = let cn' = case cn of
+                    Just n -> if n `elem` ns then Just (dec n) else Just n
+                    Nothing -> Nothing in
+     PInstance doc argDocs info f
            (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)
-           acc opts n
+           pnames acc opts n
            nfc
            (map (expandParams dec ps ns []) params)
+           (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) pextra)
            (expandParams dec ps ns [] ty)
-           cn
-           (map (expandParamsD rhs ist dec ps ns) decls)
+           cn'
+           (map (expandParamsD True ist dec ps ns) decls)
 expandParamsD rhs ist dec ps ns d = d
 
 mapsnd f (x, t) = (x, f t)
 
+expandInstanceScope ist dec ps ns (PInstance doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)
+    = PInstance doc argDocs info f cs pnames acc opts n nfc params (ps ++ pextra)
+                ty cn decls
+expandInstanceScope ist dec ps ns d = d
+
 -- Calculate a priority for a type, for deciding elaboration order
 -- * if it's just a type variable or concrete type, do it early (0)
 -- * if there's only type variables and injective constructors, do it next (1)
@@ -2287,7 +2334,7 @@
     sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)
     sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)
     sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)
-    sm 0 (PAlternative ms a as) 
+    sm 0 (PAlternative ms a as)
           = PAlternative (map shadowAlt ms) a (map (sm 0) as)
     sm 0 (PTactics ts) = PTactics (map (fmap (sm 0)) ts)
     sm 0 (PProof ts) = PProof (map (fmap (sm 0)) ts)
diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs
--- a/src/Idris/AbsSyntaxTree.hs
+++ b/src/Idris/AbsSyntaxTree.hs
@@ -112,7 +112,7 @@
                       , opt_verbose    = True
                       , opt_nobanner   = False
                       , opt_quiet      = False
-                      , opt_codegen    = Via "c"
+                      , opt_codegen    = Via IBCFormat "c"
                       , opt_outputTy   = Executable
                       , opt_ibcsubdir  = ""
                       , opt_importdirs = []
@@ -181,6 +181,11 @@
                   | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
    deriving (Show, Eq)
 
+-- | If a function has no totality annotation, what do we assume?
+data DefaultTotality = DefaultCheckingTotal    -- ^ Total
+                     | DefaultCheckingPartial  -- ^ Partial
+                     | DefaultCheckingCovering -- ^Total coverage, but may diverge
+  deriving (Show, Eq)
 
 -- | The global state used in the Idris monad
 data IState = IState {
@@ -191,6 +196,7 @@
     idris_implicits :: Ctxt [PArg],
     idris_statics :: Ctxt [Bool],
     idris_classes :: Ctxt ClassInfo,
+    idris_openimpls :: [Name], -- ^ Privileged implementations, will resolve immediately
     idris_records :: Ctxt RecordInfo,
     idris_dsls :: Ctxt DSL,
     idris_optimisation :: Ctxt OptInfo,
@@ -244,7 +250,7 @@
     idris_parsedSpan :: Maybe FC,
     hide_list :: Ctxt Accessibility,
     default_access :: Accessibility,
-    default_total :: Bool,
+    default_total :: DefaultTotality,
     ibc_write :: [IBCWrite],
     compiled_so :: Maybe String,
     idris_dynamic_libs :: [DynamicLib],
@@ -327,6 +333,7 @@
               | IBCAccess Name Accessibility
               | IBCMetaInformation Name MetaInformation
               | IBCTotal Name Totality
+              | IBCInjective Name Injectivity
               | IBCFlags Name [FnOpt]
               | IBCFnInfo Name FnInfo
               | IBCTrans Name (Term, Term)
@@ -354,13 +361,13 @@
 -- | The initial state for the compiler
 idrisInit :: IState
 idrisInit = IState initContext S.empty []
-                   emptyContext emptyContext emptyContext emptyContext
+                   emptyContext emptyContext emptyContext [] emptyContext
                    emptyContext emptyContext emptyContext emptyContext
                    emptyContext emptyContext emptyContext emptyContext
                    emptyContext emptyContext emptyContext emptyContext
                    emptyContext
                    [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
-                   [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private False [] Nothing [] []
+                   [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
                    (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
                    AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
                    emptyContext S.empty M.empty emptyContext
@@ -379,18 +386,15 @@
 
 -- Commands in the REPL
 
-data Codegen = Via String
---              | ViaC
---              | ViaJava
---              | ViaNode
---              | ViaJavaScript
---              | ViaLLVM
+data Codegen = Via IRFormat String
              | Bytecode
     deriving (Show, Eq)
 {-!
 deriving instance NFData Codegen
 !-}
 
+data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq)
+
 data HowMuchDocs = FullDocs | OverviewDocs
 
 -- | REPL commands
@@ -703,6 +707,7 @@
    | PCAF     FC Name t -- ^ Top level constant
    | PData    (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)  -- ^ Data declaration.
    | PParams  FC [(Name, t)] [PDecl' t] -- ^ Params block
+   | POpenInterfaces FC [Name] [PDecl' t] -- ^ Open block/declaration
    | PNamespace String FC [PDecl' t]
      -- ^ New namespace, where FC is accurate location of the
      -- namespace in the file
@@ -733,11 +738,13 @@
        [(Name, Docstring (Either Err t))] -- Parameter docs
        SyntaxInfo
        FC [(Name, t)] -- constraints
+       [Name] -- parent dictionaries to search for constraints
        Accessibility
        FnOpts
        Name -- class
        FC -- precise location of class
        [t] -- parameters
+       [(Name, t)] -- Extra names in scope in the body
        t -- full instance type
        (Maybe Name) -- explicit name
        [PDecl' t]
@@ -766,8 +773,9 @@
                | DInclude Codegen String
                | DHide Name
                | DFreeze Name
+               | DInjective Name
                | DAccess Accessibility
-               | DDefault Bool
+               | DDefault DefaultTotality
                | DLogging Integer
                | DDynamicLibs [String]
                | DNameHint Name FC [(Name, FC)]
@@ -880,6 +888,8 @@
     PParams (f fc)
             (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
             (map (mapPDeclFC f g) decls)
+mapPDeclFC f g (POpenInterfaces fc ifs decls) =
+    POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
 mapPDeclFC f g (PNamespace ns fc decls) =
     PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
 mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
@@ -900,10 +910,11 @@
            (map (mapPDeclFC f g) body)
            (fmap (\(n, nfc) -> (n, g nfc)) ctor)
            ctorDoc
-mapPDeclFC f g (PInstance doc paramDocs syn fc constrs cn acc opts cnfc params instTy instN body) =
+mapPDeclFC f g (PInstance doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra instTy instN body) =
     PInstance doc paramDocs syn (f fc)
               (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
-              cn acc opts (g cnfc) (map (mapPTermFC f g) params)
+              pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
+              (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
               (mapPTermFC f g instTy)
               instN
               (map (mapPDeclFC f g) body)
@@ -940,10 +951,14 @@
    where fstt (_, _, a, _, _, _, _) = a
 declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
 declared (PParams _ _ ds) = concatMap declared ds
+declared (POpenInterfaces _ _ ds) = concatMap declared ds
 declared (PNamespace _ _ ds) = concatMap declared ds
 declared (PRecord _ _ _ _ n  _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
 declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
-declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = []
+declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
+    = case mn of
+           Nothing -> []
+           Just n -> [n]
 declared (PDSL n _) = [n]
 declared (PSyntax _ _) = []
 declared (PMutual _ ds) = concatMap declared ds
@@ -960,10 +975,14 @@
 tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
    where fstt (_, _, a, _, _, _, _) = a
 tldeclared (PParams _ _ ds)                       = []
+tldeclared (POpenInterfaces _ _ ds)               = concatMap tldeclared ds
 tldeclared (PMutual _ ds)                         = concatMap tldeclared ds
 tldeclared (PNamespace _ _ ds)                    = concatMap tldeclared ds
 tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _)     = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
-tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _)    = []
+tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
+    = case mn of
+           Nothing -> []
+           Just n -> [n]
 tldeclared _                                      = []
 
 defined :: PDecl -> [Name]
@@ -976,10 +995,14 @@
    where fstt (_, _, a, _, _, _, _) = a
 defined (PData _ _ _ _ _ (PLaterdecl n _ _))      = []
 defined (PParams _ _ ds)                          = concatMap defined ds
+defined (POpenInterfaces _ _ ds)                  = concatMap defined ds
 defined (PNamespace _ _ ds)                       = concatMap defined ds
 defined (PRecord _ _ _ _ n _ _ _ _ cn _ _)        = n : map fst (maybeToList cn)
 defined (PClass _ _ _ _ n _ _ _ _ ms cn _)        = n : (map fst (maybeToList cn) ++ concatMap defined ms)
-defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _)     = []
+defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
+    = case mn of
+           Nothing -> []
+           Just n -> [n]
 defined (PDSL n _)                                = [n]
 defined (PSyntax _ _)                             = []
 defined (PMutual _ ds)                            = concatMap defined ds
@@ -1353,7 +1376,7 @@
 -- Type class data
 
 data ClassInfo = CI { instanceCtorName :: Name,
-                      class_methods :: [(Name, (FnOpts, PTerm))],
+                      class_methods :: [(Name, (Bool, FnOpts, PTerm))], -- flag whether it's a "data" method
                       class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
                       class_default_superclasses :: [PDecl],
                       class_params :: [Name],
@@ -1523,6 +1546,7 @@
                         decoration :: Name -> Name,
                         inPattern :: Bool,
                         implicitAllowed :: Bool,
+                        constraintAllowed :: Bool,
                         maxline :: Maybe Int,
                         mut_nesting :: Int,
                         dsl_info :: DSL,
@@ -1535,7 +1559,7 @@
 deriving instance Binary SyntaxInfo
 !-}
 
-defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0 True True
+defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
 
 expandNS :: SyntaxInfo -> Name -> Name
 expandNS syn n@(NS _ _) = n
@@ -1792,6 +1816,9 @@
       depth d . bracket p startPrec $
       lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
       rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
+    prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
+      | basename neg == sUN "negate" =
+         lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
     -- This case preserves the behavior of the former constructor PEq.
     -- It should be removed if feasible when the pretty-printing of infix
     -- operators in general is improved.
@@ -2163,11 +2190,12 @@
                                       indent 2 (vsep (map (showCImp o) cs))
 showDeclImp o (PData _ _ _ _ _ d)   = showDImp o { ppopt_impl = True } d
 showDeclImp o (PParams _ ns ps)     = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
+showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
 showDeclImp o (PNamespace n fc ps)  = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
 showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
 showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)
    = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
-showDeclImp o (PInstance _ _ _ _ cs acc _ n _ _ t _ ds)
+showDeclImp o (PInstance _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
    = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
 showDeclImp _ _ = text "..."
 -- showDeclImp (PImport o) = "import " ++ o
diff --git a/src/Idris/CaseSplit.hs b/src/Idris/CaseSplit.hs
--- a/src/Idris/CaseSplit.hs
+++ b/src/Idris/CaseSplit.hs
@@ -12,6 +12,7 @@
 import Idris.ElabDecls
 import Idris.Delaborate
 import Idris.Parser
+import Idris.Parser.Helpers
 import Idris.Error
 import Idris.Output
 
@@ -284,10 +285,12 @@
 
 replaceSplits :: String -> [[(Name, PTerm)]] -> Bool -> Idris [String]
 replaceSplits l ups impossible
-    = updateRHSs 1 (map (rep (expandBraces l)) ups)
+    = do ist <- getIState
+         updateRHSs 1 (map (rep ist (expandBraces l)) ups)
   where
-    rep str [] = str ++ "\n"
-    rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups
+    rep ist str [] = str ++ "\n"
+    rep ist str ((n, tm) : ups) 
+        = rep ist (updatePat False (show n) (nshow (resugar ist tm)) str) ups
 
     updateRHSs i [] = return []
     updateRHSs i (x : xs)
@@ -368,6 +371,20 @@
              (before, ('_' : after)) -> nameRoot (acc ++ [before]) after
              _ -> showSep "_" (acc ++ [nm])
 
+-- Show a name for use in pattern definitions on the lhs
+showLHSName :: Name -> String
+showLHSName n = let fn = show n in 
+                    if any (flip elem opChars) fn
+                       then "(" ++ fn ++ ")"
+                       else fn
+
+-- Show a name for the purpose of generating a metavariable name on the rhs
+showRHSName :: Name -> String
+showRHSName n = let fn = show n in 
+                    if any (flip elem opChars) fn
+                       then "op"
+                       else fn
+
 getClause :: Int      -- ^ line number that the type is declared on
           -> Name     -- ^ Function name
           -> Name     -- ^ User given name
@@ -383,8 +400,8 @@
                                     x -> x
                       ist <- get
                       let ap = mkApp ist ty []
-                      return (show un ++ " " ++ ap ++ "= ?"
-                                      ++ show un ++ "_rhs")
+                      return (showLHSName un ++ " " ++ ap ++ "= ?"
+                                      ++ showRHSName un ++ "_rhs")
    where mkApp :: IState -> PTerm -> [Name] -> String
          mkApp i (PPi (Exp _ _ False) (MN _ _) _ ty sc) used
                = let n = getNameFrom i used ty in
@@ -410,14 +427,14 @@
                                                           sUN "z"]) used
 
          -- write method declarations, indent with 4 spaces
-         mkClassBodies :: IState -> [(Name, (FnOpts, PTerm))] -> String
+         mkClassBodies :: IState -> [(Name, (Bool, FnOpts, PTerm))] -> String
          mkClassBodies i ns
              = showSep "\n"
-                  (zipWith (\(n, (_, ty)) m -> "    " ++
+                  (zipWith (\(n, (_, _, ty)) m -> "    " ++
                             def (show (nsroot n)) ++ " "
                                  ++ mkApp i ty []
                                  ++ "= ?"
-                                 ++ show un ++ "_rhs_" ++ show m) ns [1..])
+                                 ++ showRHSName un ++ "_rhs_" ++ show m) ns [1..])
 
          def n@(x:xs) | not (isAlphaNum x) = "(" ++ n ++ ")"
          def n = n
@@ -431,7 +448,7 @@
                        let ty = case ty_in of
                                      PTyped n t -> t
                                      x -> x
-                       return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")
+                       return (mkApp ty ++ " = ?" ++ showRHSName fn ++ "_rhs")
    where mkApp (PPi _ _ _ _ sc) = mkApp sc
          mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn
 
@@ -451,7 +468,7 @@
          newpat ('>':patstr) = '>':newpat patstr
          newpat patstr =
            "  " ++
-           replaceRHS patstr "| with_pat = ?" ++ show n ++ "_rhs"
+           replaceRHS patstr "| with_pat = ?" ++ showRHSName n ++ "_rhs"
 
 -- Replace _ with names in missing clauses
 
diff --git a/src/Idris/CmdOptions.hs b/src/Idris/CmdOptions.hs
--- a/src/Idris/CmdOptions.hs
+++ b/src/Idris/CmdOptions.hs
@@ -149,6 +149,12 @@
   <|> ((\s -> UseCodegen $ parseCodegen s) <$> strOption (long "codegen"
                                                        <> metavar "TARGET"
                                                        <> help "Select code generator: C, Javascript, Node and bytecode are bundled with Idris"))
+
+
+  <|> ((\s -> UseCodegen $ Via JSONFormat s) <$> strOption (long "portable-codegen"
+                                                         <> metavar "TARGET"
+                                                         <> help "Pass the name of the code generator. This option is for codegens that take JSON formatted IR."))
+
   <|> (CodegenArgs <$> strOption (long "cg-opt"
                                <> metavar "ARG"
                                <> help "Arguments to pass to code generator"))
@@ -206,7 +212,8 @@
 
 parseCodegen :: String -> Codegen
 parseCodegen "bytecode" = Bytecode
-parseCodegen cg         = Via (map toLower cg)
+parseCodegen cg         = Via IBCFormat (map toLower cg)
+
 
 parseLogCats :: Monad m => String -> m [LogCat]
 parseLogCats s =
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
@@ -6,14 +6,15 @@
                 normaliseAll, normaliseBlocking, toValue, quoteTerm,
                 rt_simplify, simplify, specialise, hnf, convEq, convEq',
                 Def(..), CaseInfo(..), CaseDefs(..),
-                Accessibility(..), Totality(..), PReason(..), MetaInformation(..),
+                Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..),
                 Context, initContext, ctxtAlist, next_tvar,
-                addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
+                addToCtxt, setAccess, setInjective, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
                 addDatatype, addCasedef, simplifyCasedef, addOperator,
                 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
                 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
                 mapDefCtxt, 
-                lookupTotal, lookupTotalExact, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
+                lookupTotal, lookupTotalExact, lookupInjectiveExact,
+                lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
                 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
                 isUniverse) where
 
@@ -759,6 +760,8 @@
   show Private = "private"
   show Hidden = "hidden"
 
+type Injectivity = Bool
+
 -- | The result of totality checking
 data Totality = Total [Int] -- ^ well-founded arguments
               | Productive -- ^ productive
@@ -816,7 +819,7 @@
 -- universe constraints and existing definitions.
 data Context = MkContext {
                   next_tvar       :: Int,
-                  definitions     :: Ctxt (Def, Accessibility, Totality, MetaInformation)
+                  definitions     :: Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation)
                 } deriving Show
 
 
@@ -826,47 +829,53 @@
 
 mapDefCtxt :: (Def -> Def) -> Context -> Context
 mapDefCtxt f (MkContext t !defs) = MkContext t (mapCtxt f' defs)
-   where f' (!d, a, t, m) = f' (f d, a, t, m)
+   where f' (!d, i, a, t, m) = f' (f d, i, a, t, m)
 
 -- | Get the definitions from a context
 ctxtAlist :: Context -> [(Name, Def)]
-ctxtAlist ctxt = map (\(n, (d, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)
+ctxtAlist ctxt = map (\(n, (d, i, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)
 
 veval ctxt env t = evalState (eval False ctxt [] env t []) initEval
 
 addToCtxt :: Name -> Term -> Type -> Context -> Context
 addToCtxt n tm ty uctxt
     = let ctxt = definitions uctxt
-          !ctxt' = addDef n (Function ty tm, Public, Unchecked, EmptyMI) ctxt in
+          !ctxt' = addDef n (Function ty tm, False, Public, Unchecked, EmptyMI) ctxt in
           uctxt { definitions = ctxt' }
 
 setAccess :: Name -> Accessibility -> Context -> Context
 setAccess n a uctxt
     = let ctxt = definitions uctxt
-          !ctxt' = updateDef n (\ (d, _, t, m) -> (d, a, t, m)) ctxt in
+          !ctxt' = updateDef n (\ (d, i, _, t, m) -> (d, i, a, t, m)) ctxt in
           uctxt { definitions = ctxt' }
 
+setInjective :: Name -> Injectivity -> Context -> Context
+setInjective n i uctxt
+    = let ctxt = definitions uctxt
+          !ctxt' = updateDef n (\ (d, _, a, t, m) -> (d, i, a, t, m)) ctxt in
+          uctxt { definitions = ctxt' }
+
 setTotal :: Name -> Totality -> Context -> Context
 setTotal n t uctxt
     = let ctxt = definitions uctxt
-          !ctxt' = updateDef n (\ (d, a, _, m) -> (d, a, t, m)) ctxt in
+          !ctxt' = updateDef n (\ (d, i, a, _, m) -> (d, i, a, t, m)) ctxt in
           uctxt { definitions = ctxt' }
 
 setMetaInformation :: Name -> MetaInformation -> Context -> Context
 setMetaInformation n m uctxt
     = let ctxt = definitions uctxt
-          !ctxt' = updateDef n (\ (d, a, t, _) -> (d, a, t, m)) ctxt in
+          !ctxt' = updateDef n (\ (d, i, a, t, _) -> (d, i, a, t, m)) ctxt in
           uctxt { definitions = ctxt' }
 
 addCtxtDef :: Name -> Def -> Context -> Context
 addCtxtDef n d c = let ctxt = definitions c
-                       !ctxt' = addDef n (d, Public, Unchecked, EmptyMI) $! ctxt in
+                       !ctxt' = addDef n (d, False, Public, Unchecked, EmptyMI) $! ctxt in
                        c { definitions = ctxt' }
 
 addTyDecl :: Name -> NameType -> Type -> Context -> Context
 addTyDecl n nt ty uctxt
     = let ctxt = definitions uctxt
-          !ctxt' = addDef n (TyDecl nt ty, Public, Unchecked, EmptyMI) ctxt in
+          !ctxt' = addDef n (TyDecl nt ty, False, Public, Unchecked, EmptyMI) ctxt in
           uctxt { definitions = ctxt' }
 
 addDatatype :: Datatype Name -> Context -> Context
@@ -874,14 +883,14 @@
     = let ctxt = definitions uctxt
           ty' = normalise uctxt [] ty
           !ctxt' = addCons 0 cons (addDef n
-                     (TyDecl (TCon tag (arity ty')) ty, Public, Unchecked, EmptyMI) ctxt) in
+                     (TyDecl (TCon tag (arity ty')) ty, True, Public, Unchecked, EmptyMI) ctxt) in
           uctxt { definitions = ctxt' }
   where
     addCons tag [] ctxt = ctxt
     addCons tag ((n, ty) : cons) ctxt
         = let ty' = normalise uctxt [] ty in
               addCons (tag+1) cons (addDef n
-                  (TyDecl (DCon tag (arity ty') unique) ty, Public, Unchecked, EmptyMI) ctxt)
+                  (TyDecl (DCon tag (arity ty') unique) ty, True, Public, Unchecked, EmptyMI) ctxt)
 
 -- FIXME: Too many arguments! Refactor all these Bools.
 --
@@ -923,7 +932,7 @@
                                            (args_rt, sc_rt)
                            op = (CaseOp (ci { case_inlinable = inlc })
                                                 ty argtys ps_in ps_tot cdef,
-                                 access, Unchecked, EmptyMI)
+                                 False, access, Unchecked, EmptyMI)
                        in return $ addDef n op ctxt
 --                    other -> tfail (Msg $ "Error adding case def: " ++ show other)
          return uctxt { definitions = ctxt' }
@@ -933,15 +942,15 @@
 simplifyCasedef n ei uctxt
    = do let ctxt = definitions uctxt
         ctxt' <- case lookupCtxt n ctxt of
-                   [(CaseOp ci ty atys [] ps _, acc, tot, metainf)] ->
+                   [(CaseOp ci ty atys [] ps _, inj, acc, tot, metainf)] ->
                       return ctxt -- nothing to simplify (or already done...)
-                   [(CaseOp ci ty atys ps_in ps cd, acc, tot, metainf)] ->
+                   [(CaseOp ci ty atys ps_in ps cd, inj, acc, tot, metainf)] ->
                       do let ps_in' = map simpl ps_in
                              pdef = map debind ps_in'
                          CaseDef args sc _ <- simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei
                          return $ addDef n (CaseOp ci
                                               ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),
-                                              acc, tot, metainf) ctxt
+                                              inj, acc, tot, metainf) ctxt
 
                    _ -> return ctxt
         return uctxt { definitions = ctxt' }
@@ -961,10 +970,10 @@
                Context -> Context
 addOperator n ty a op uctxt
     = let ctxt = definitions uctxt
-          ctxt' = addDef n (Operator ty a op, Public, Unchecked, EmptyMI) ctxt in
+          ctxt' = addDef n (Operator ty a op, False, Public, Unchecked, EmptyMI) ctxt in
           uctxt { definitions = ctxt' }
 
-tfst (a, _, _, _) = a
+tfst (a, _, _, _, _) = a
 
 lookupNames :: Name -> Context -> [Name]
 lookupNames n ctxt
@@ -1041,10 +1050,10 @@
 lookupP_all all exact n ctxt
    = do (n', def) <- names 
         p <- case def of
-          (Function ty tm, a, _, _)      -> return (P Ref n' ty, a)
-          (TyDecl nt ty, a, _, _)        -> return (P nt n' ty, a)
-          (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n' ty, a)
-          (Operator ty _ _, a, _, _)     -> return (P Ref n' ty, a)
+          (Function ty tm, inj, a, _, _)      -> return (P Ref n' ty, a)
+          (TyDecl nt ty, _, a, _, _)        -> return (P nt n' ty, a)
+          (CaseOp _ ty _ _ _ _, inj, a, _, _) -> return (P Ref n' ty, a)
+          (Operator ty _ _, inj, a, _, _)     -> return (P Ref n' ty, a)
         case snd p of
           Hidden -> if all then return (fst p) else []
           Private -> if all then return (fst p) else []
@@ -1071,25 +1080,29 @@
 lookupDefAcc n mkpublic ctxt
     = map mkp $ lookupCtxt n (definitions ctxt)
   -- io_bind a special case for REPL prettiness
-  where mkp (d, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))
-                             then (d, Public) else (d, a)
+  where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))
+                                   then (d, Public) else (d, a)
 
 lookupDefAccExact :: Name -> Bool -> Context ->
                      Maybe (Def, Accessibility)
 lookupDefAccExact n mkpublic ctxt
     = fmap mkp $ lookupCtxtExact n (definitions ctxt)
   -- io_bind a special case for REPL prettiness
-  where mkp (d, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))
-                             then (d, Public) else (d, a)
+  where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))
+                                   then (d, Public) else (d, a)
 
 lookupTotal :: Name -> Context -> [Totality]
 lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)
-  where mkt (d, a, t, m) = t
+  where mkt (d, inj, 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
+  where mkt (d, inj, a, t, m) = t
 
+lookupInjectiveExact :: Name -> Context -> Maybe Injectivity
+lookupInjectiveExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)
+  where mkt (d, inj, a, t, m) = inj
+
 -- Check if a name is reducible in the type checker. Partial definitions
 -- are not reducible (so treated as a constant)
 tcReducible :: Name -> Context -> Bool
@@ -1100,10 +1113,10 @@
 
 lookupMetaInformation :: Name -> Context -> [MetaInformation]
 lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)
-  where mkm (d, a, t, m) = m
+  where mkm (d, inj, a, t, m) = m
 
 lookupNameTotal :: Name -> Context -> [(Name, Totality)]
-lookupNameTotal n = map (\(n, (_, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions
+lookupNameTotal n = map (\(n, (_, _, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions
 
 
 lookupVal :: Name -> Context -> [Value]
diff --git a/src/Idris/Core/Unify.hs b/src/Idris/Core/Unify.hs
--- a/src/Idris/Core/Unify.hs
+++ b/src/Idris/Core/Unify.hs
@@ -292,6 +292,8 @@
 
     injective (P (DCon _ _ _) _ _) = True
     injective (P (TCon _ _) _ _) = True
+    injective (P Ref n _) 
+         | Just i <- lookupInjectiveExact n ctxt = i
     injective (App _ f a)        = injective f -- && injective a
     injective _                  = False
 
@@ -573,7 +575,7 @@
 
             rigid (P (DCon _ _ _) _ _) = True
             rigid (P (TCon _ _) _ _) = True
-            rigid t@(P Ref _ _)      = inenv t || globmetavar t
+            rigid t@(P Ref _ _)  = inenv t || globmetavar t
             rigid (Constant _)       = True
             rigid (App _ f a)        = rigid f && rigid a
             rigid t                  = not (metavar t) || globmetavar t
@@ -710,9 +712,9 @@
 -- Issue #1722 on the issue tracker https://github.com/idris-lang/Idris-dev/issues/1722
 --
 recoverable t@(App _ _ _) _
-    | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False
+    | (P _ (UN l) _, _) <- unApply t, l == txt "Delayed" = False
 recoverable _ t@(App _ _ _)
-    | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False
+    | (P _ (UN l) _, _) <- unApply t, l == txt "Delayed" = False
 recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y
 recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y
 recoverable (TType _) (P (DCon _ _ _) y _) = False
diff --git a/src/Idris/Core/WHNF.hs b/src/Idris/Core/WHNF.hs
--- a/src/Idris/Core/WHNF.hs
+++ b/src/Idris/Core/WHNF.hs
@@ -75,6 +75,7 @@
           = let wp = case nt of
                           DCon t a u -> WDCon t a u n (ty, env)
                           TCon t a -> WTCon t a n (ty, env)
+                          Ref -> WPRef n (ty, env)
                           _ -> WPRef n (ty, env)
                         in
             case lookupDefExact n ctxt of
diff --git a/src/Idris/Coverage.hs b/src/Idris/Coverage.hs
--- a/src/Idris/Coverage.hs
+++ b/src/Idris/Coverage.hs
@@ -493,9 +493,9 @@
      | (P _ (UN l) _, [_, _, arg]) <- unApply t,
        l == txt "Force" = delazy' all arg
      | (P _ (UN l) _, [P _ (UN lty) _, _, arg]) <- unApply t,
-       l == txt "Delay" && (all || lty == txt "LazyEval") = delazy arg
+       l == txt "Delay" && (all || lty /= txt "Infinite") = delazy arg
      | (P _ (UN l) _, [P _ (UN lty) _, arg]) <- unApply t,
-       l == txt "Lazy'" && (all || lty == txt "LazyEval") = delazy' all arg
+       l == txt "Delayed" && (all || lty /= txt "Infinite") = delazy' all arg
 delazy' all (App s f a) = App s (delazy' all f) (delazy' all a)
 delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)
 delazy' all t = t
@@ -518,6 +518,10 @@
      -- that it is total.
      | (P _ (UN at) _, [_, _]) <- unApply ap,
        at == txt "assert_total" = []
+     -- don't go under calls to functions which are asserted total
+     | (P _ n _, _) <- unApply ap,
+       Just opts <- lookupCtxtExact n (idris_flags ist),
+       AssertTotal `elem` opts = []
      -- under a guarded call to "Delay LazyCodata", we are 'Delayed', so don't
      -- check under guarded constructors.
      | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
@@ -745,8 +749,11 @@
         | [TyDecl (TCon _ _) _] <- lookupDef f (tt_ctxt ist)
             = Total []
     tryPath desc path (e@(f, args) : es) arg
+        | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
         | e `elem` es && allNothing args = Partial (Mutual [f])
     tryPath desc path (e@(f, nextargs) : es) arg
+        | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
+        | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
         | Just d <- lookup (e, arg) path
             = if desc - d > 0 -- Now lower than when we were last here
                    then -- trace ("Descent " ++ show (desc - d) ++ " "
@@ -781,8 +788,6 @@
 --                   trace (show (desc, argspos, path, es, pathres)) $
                    collapse pathres
 
-        | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a
-        | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])
         | otherwise = Unchecked
 
 allNothing :: [Maybe a] -> Bool
@@ -808,3 +813,18 @@
 collapse' def (d : xs)         = collapse' d xs
 -- collapse' Unchecked []         = Total []
 collapse' def []               = def
+
+totalityCheckBlock :: Idris ()
+totalityCheckBlock = do
+         ist <- getIState
+         -- Do totality checking after entire mutual block
+         mapM_ (\n -> do logElab 5 $ "Simplifying " ++ show n
+                         ctxt' <- do ctxt <- getContext
+                                     tclift $ simplifyCasedef n (getErasureInfo ist) ctxt
+                         setContext ctxt')
+                 (map snd (idris_totcheck ist))
+         mapM_ buildSCG (idris_totcheck ist)
+         mapM_ checkDeclTotality (idris_totcheck ist)
+         clear_totcheck
+
+
diff --git a/src/Idris/DeepSeq.hs b/src/Idris/DeepSeq.hs
--- a/src/Idris/DeepSeq.hs
+++ b/src/Idris/DeepSeq.hs
@@ -284,6 +284,7 @@
     rnf (IBCAccess name accessibility) = rnf name `seq` rnf accessibility `seq` ()
     rnf (IBCMetaInformation name metaInformation) = rnf name `seq` rnf metaInformation `seq` ()
     rnf (IBCTotal name totality) = rnf name `seq` rnf totality `seq` ()
+    rnf (IBCInjective name inj) = rnf name `seq` rnf inj `seq` ()
     rnf (IBCFlags name fnOpts) = rnf name `seq` rnf fnOpts `seq` ()
     rnf (IBCFnInfo name fnInfo) = rnf name `seq` rnf fnInfo `seq` ()
     rnf (IBCTrans name terms) = rnf name `seq` rnf terms `seq` ()
@@ -360,9 +361,12 @@
         rnf (FnInfo x1) = rnf x1 `seq` ()
 
 instance NFData Codegen where
-        rnf (Via x1) = rnf x1 `seq` ()
+        rnf (Via x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
         rnf Bytecode = ()
 
+instance NFData IRFormat where
+        rnf _ = ()
+
 instance NFData LogCat where
        rnf _ = ()
 
@@ -444,6 +448,7 @@
               rnf x2 `seq`
                 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
         rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
+        rnf (POpenInterfaces x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
         rnf (PNamespace x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
         rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)
           = rnf x1 `seq`
@@ -468,7 +473,7 @@
                             rnf x9 `seq`
                               rnf x10 `seq`
                                 rnf x11 `seq` rnf x12 `seq` ()
-        rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)
+        rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)
           = rnf x1 `seq`
               rnf x2 `seq`
                 rnf x3 `seq`
@@ -477,7 +482,7 @@
                       rnf x6 `seq`
                         rnf x7 `seq`
                           rnf x8 `seq`
-                            rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` ()
+                            rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` ()
         rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
         rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
         rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
@@ -682,25 +687,29 @@
         rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
 
 instance NFData SyntaxInfo where
-        rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)
+        rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)
           = rnf x1 `seq`
               rnf x2 `seq`
                 rnf x3 `seq`
                   rnf x4 `seq`
                     rnf x5 `seq`
-                      rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` ()
+                      rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` ()
 
 instance NFData OutputMode where
   rnf (RawOutput x) = () -- no instance for Handle, so this is a bit wrong
   rnf (IdeMode x y) = rnf x `seq` ()
 
+instance NFData DefaultTotality where
+  rnf DefaultCheckingTotal = ()
+  rnf DefaultCheckingPartial = ()
+  rnf DefaultCheckingCovering = ()
 
 instance NFData IState where
   rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20
               x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40
               x41 x42 x43 x44 x45 x46 x47 x48 x49 x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x60
-              x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74 x75 x76)
+              x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74 x75 x76 x77)
      = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` () `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` rnf x16 `seq` rnf x17 `seq` rnf x18 `seq` rnf x19 `seq` rnf x20 `seq`
        rnf x21 `seq` rnf x22 `seq` rnf x23 `seq` rnf x24 `seq` rnf x25 `seq` rnf x26 `seq` rnf x27 `seq` rnf x28 `seq` rnf x29 `seq` rnf x30 `seq` rnf x31 `seq` rnf x32 `seq` rnf x33 `seq` rnf x34 `seq` rnf x35 `seq` rnf x36 `seq` rnf x37 `seq` rnf x38 `seq` rnf x39 `seq` rnf x40 `seq`
        rnf x41 `seq` rnf x42 `seq` rnf x43 `seq` rnf x44 `seq` rnf x45 `seq` rnf x46 `seq` rnf x47 `seq` rnf x48 `seq` rnf x49 `seq` rnf x50 `seq` rnf x51 `seq` rnf x52 `seq` rnf x53 `seq` rnf x54 `seq` rnf x55 `seq` rnf x56 `seq` rnf x57 `seq` rnf x58 `seq` rnf x59 `seq` rnf x60 `seq`
-       rnf x61 `seq` rnf x62 `seq` rnf x63 `seq` rnf x64 `seq` rnf x65 `seq` rnf x66 `seq` rnf x67 `seq` rnf x68 `seq` rnf x69 `seq` rnf x70 `seq` rnf x71 `seq` rnf x72 `seq` rnf x73 `seq` rnf x74 `seq` rnf x75 `seq` rnf x76 `seq` ()
+       rnf x61 `seq` rnf x62 `seq` rnf x63 `seq` rnf x64 `seq` rnf x65 `seq` rnf x66 `seq` rnf x67 `seq` rnf x68 `seq` rnf x69 `seq` rnf x70 `seq` rnf x71 `seq` rnf x72 `seq` rnf x73 `seq` rnf x74 `seq` rnf x75 `seq` rnf x76 `seq` rnf x77 `seq` ()
diff --git a/src/Idris/Directives.hs b/src/Idris/Directives.hs
--- a/src/Idris/Directives.hs
+++ b/src/Idris/Directives.hs
@@ -42,6 +42,11 @@
   mapM_ (\n -> do
             setAccessibility n Frozen
             addIBC (IBCAccess n Frozen)) ns
+directiveAction (DInjective n') = do
+  ns <- allNamespaces n'
+  mapM_ (\n -> do
+            setInjectivity n True
+            addIBC (IBCInjective n True)) ns
 
 directiveAction (DAccess acc) = do updateIState (\i -> i { default_access = acc })
 
diff --git a/src/Idris/Docs.hs b/src/Idris/Docs.hs
--- a/src/Idris/Docs.hs
+++ b/src/Idris/Docs.hs
@@ -319,8 +319,8 @@
     namedInst n@(UN _)  = Just n
     namedInst _         = Nothing
     
-    getDInst (PInstance _ _ _ _ _ _ _ _ _ _ t _ _) = Just t
-    getDInst _                                     = Nothing
+    getDInst (PInstance _ _ _ _ _ _ _ _ _ _ _ _ t _ _) = Just t
+    getDInst _                                         = Nothing
 
     isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args'))
       = nm == n && map getTm args == map getTm args'
diff --git a/src/Idris/Elab/Class.hs b/src/Idris/Elab/Class.hs
--- a/src/Idris/Elab/Class.hs
+++ b/src/Idris/Elab/Class.hs
@@ -119,6 +119,11 @@
          -- Elaborate the the top level methods
          mapM_ (rec_elabDecl info EAll info) (concat fns)
 
+         -- Flag all the top level data declarations as injective
+         mapM_ (\n -> do setInjectivity n True
+                         addIBC (IBCInjective n True))
+               (map fst (filter (\(_, (inj, _, _, _, _)) -> inj) imethods))
+
          -- add the default definitions
          mapM_ (rec_elabDecl info EAll info) (concat (map (snd.snd) defs))
          addIBC (IBCClass tn)
@@ -130,7 +135,7 @@
            maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn
 
   where
-    nodoc (n, (_, _, o, t)) = (n, (o, t))
+    nodoc (n, (inj, _, _, o, t)) = (n, (inj, o, t))
 
     pibind [] x = x
     pibind ((n, ty): ns) x = PPi expl n NoFC ty (pibind ns (chkUniq ty x))
@@ -144,7 +149,7 @@
 
     -- TODO: probably should normalise
     checkDefaultSuperclassInstance :: PDecl -> Idris ()
-    checkDefaultSuperclassInstance (PInstance _ _ _ fc cs _ _ n _ ps _ _ _)
+    checkDefaultSuperclassInstance (PInstance _ _ _ fc cs _ _ _ n _ ps _ _ _ _)
         = do when (not $ null cs) . tclift
                 $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))
              i <- getIState
@@ -171,14 +176,26 @@
     conbind [] x = x
 
     getMName (PTy _ _ _ _ _ n nfc _) = nsroot n
+    getMName (PData _ _ _ _ _ (PLaterdecl n nfc _)) = nsroot n
+
     tdecl allmeths (PTy doc _ syn _ o n nfc t)
            = do t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t
                 logElab 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
                 return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),
-                         (n, (nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)
+                         (n, (False, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)
                                               (\ l s p -> Imp l s p Nothing True) t'))),
                          (n, (nfc, syn, o, t) ) )
-    tdecl _ _ = ifail "Not allowed in a class declaration"
+    tdecl allmeths (PData doc _ syn _ _ (PLaterdecl n nfc t)) 
+           = do let o = []
+                t' <- implicit' info syn (map (\(n, _, _) -> n) ps ++ allmeths) n t
+                logElab 2 $ "Data method " ++ show n ++ " : " ++ showTmImpls t'
+                return ( (n, (toExp (map (\(pn, _, _) -> pn) ps) Exp t')),
+                         (n, (True, nfc, doc, o, (toExp (map (\(pn, _, _) -> pn) ps)
+                                              (\ l s p -> Imp l s p Nothing True) t'))),
+                         (n, (nfc, syn, o, t) ) )
+    tdecl allmeths (PData doc _ syn _ _ _) 
+         = ierror $ At fc (Msg "Data definitions not allowed in a class declaration")
+    tdecl _ _ = ierror $ At fc (Msg "Not allowed in a class declaration")
 
     -- Create default definitions
     defdecl mtys c d@(PClauses fc opts n cs) =
@@ -190,17 +207,18 @@
                                PClauses fc (o ++ opts) n cs]
                  logElab 1 (show ds)
                  return (n, ((defaultdec n, ds!!1), ds))
-            _ -> ifail $ show n ++ " is not a method"
+            _ -> ierror $ At fc (Msg (show n ++ " is not a method"))
     defdecl _ _ _ = ifail "Can't happen (defdecl)"
 
     defaultdec (UN n) = sUN ("default#" ++ str n)
     defaultdec (NS n ns) = NS (defaultdec n) ns
 
-    tydecl (PTy _ _ _ _ _ _ _ _) = True
+    tydecl (PTy{}) = True
+    tydecl (PData _ _ _ _ _ _) = True
     tydecl _ = False
-    instdecl (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = True
+    instdecl (PInstance{}) = True
     instdecl _ = False
-    clause (PClauses _ _ _ _) = True
+    clause (PClauses{}) = True
     clause _ = False
 
     -- Generate a function for chasing a dictionary constraint
@@ -233,10 +251,10 @@
     tfun :: Name -- ^ The name of the class
          -> PTerm -- ^ A constraint for the class, to be inserted under the implicit bindings
          -> SyntaxInfo -> [Name] -- ^ All the method names
-         -> (Name, (FC, Docstring (Either Err PTerm), FnOpts, PTerm))
+         -> (Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))
             -- ^ The present declaration
          -> Idris [PDecl]
-    tfun cn c syn all (m, (mfc, doc, o, ty))
+    tfun cn c syn all (m, (isdata, mfc, doc, o, ty))
         = do let ty' = expandMethNS syn (insertConstraint c all ty)
              let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]
              let capp = PApp fc (PRef fc [] cn) (map (pexp . PRef fc []) mnames)
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
@@ -194,17 +194,11 @@
            logElab 5 $ "After data structure transformations:\n" ++ show pdef'
 
            ist <- getIState
-  --          let wf = wellFounded ist n sc
-           let tot | pcover || AssertTotal `elem` opts = Unchecked -- finish later
+           let tot | pcover = Unchecked -- finish later
+                   | AssertTotal `elem` opts = Total []
                    | PEGenerated `elem` opts = Generated
                    | otherwise = Partial NotCovering -- already know it's not total
 
-  --          case lookupCtxt (namespace info) n (idris_flags ist) of
-  --             [fs] -> if TotalFn `elem` fs
-  --                       then case tot of
-  --                               Total _ -> return ()
-  --                               t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))
-  --             _ -> return ()
            case tree of
                CaseDef _ _ [] -> return ()
                CaseDef _ _ xs -> mapM_ (\x ->
@@ -506,29 +500,6 @@
                                   else return (validCoverageCase ctxt err ||
                                                  recoverableCoverage ctxt err)
 
-
-propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm
-propagateParams i ps t bound tm@(PApp _ (PRef fc hls n) args)
-     = PApp fc (PRef fc hls n) (addP t args)
-   where addP (Bind n _ sc) (t : ts)
-              | Placeholder <- getTm t,
-                n `elem` ps,
-                not (n `elem` bound)
-                    = t { getTm = PPatvar NoFC n } : addP sc ts
-         addP (Bind n _ sc) (t : ts) = t : addP sc ts
-         addP _ ts = ts
-propagateParams i ps t bound (PApp fc ap args)
-     = PApp fc (propagateParams i ps t bound ap) args
-propagateParams i ps t bound (PRef fc hls n)
-     = case lookupCtxt n (idris_implicits i) of
-            [is] -> let ps' = filter (isImplicit is) ps in
-                        PApp fc (PRef fc hls n) (map (\x -> pimp x (PRef fc [] x) True) ps')
-            _ -> PRef fc hls n
-    where isImplicit [] n = False
-          isImplicit (PImp _ _ _ x _ : is) n | x == n = True
-          isImplicit (_ : is) n = isImplicit is n
-propagateParams i ps t bound x = x
-
 findUnique :: Context -> Env -> Term -> [Name]
 findUnique ctxt env (Bind n b sc)
    = let rawTy = forgetEnv (map fst env) (binderTy b)
@@ -583,6 +554,7 @@
 
         let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $
                     propagateParams i params norm_ty (allNamesIn lhs_in) (addImplPat i lhs_in)
+        
 --         let lhs = mkLHSapp $
 --                     propagateParams i params fn_ty (addImplPat i lhs_in)
         logElab 10 (show (params, fn_ty) ++ " " ++ showTmImpls (addImplPat i lhs_in))
@@ -657,6 +629,7 @@
 
         let winfo = (pinfo info newargs defs windex) { elabFC = Just fc }
         let wb = map (mkStatic static_names) $
+                 map (expandInstanceScope ist decorate newargs defs) $
                  map (expandParamsD False ist decorate newargs defs) whereblock
 
         -- Split the where block into declarations with a type, and those
@@ -664,7 +637,7 @@
         -- Elaborate those with a type *before* RHS, those without *after*
         let (wbefore, wafter) = sepBlocks wb
 
-        logElab 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
+        logElab 5 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter
         mapM_ (rec_elabDecl info EAll winfo) wbefore
         -- Now build the RHS, using the type of the LHS as the goal.
         i <- getIState -- new implicits from where block
@@ -1068,9 +1041,18 @@
 
          lhs_arity = arity toplhs
 
-         updateApp wtm@(PWithApp fcw tm warg) = 
+         currentFn fname (PAlternative _ _ as)
+              | Just tm <- getApp as = tm
+            where getApp (tm@(PApp _ (PRef _ _ f) _) : as)
+                      | f == fname = Just tm
+                  getApp (_ : as) = getApp as
+                  getApp [] = Nothing
+         currentFn _ tm = tm
+
+         updateApp wtm@(PWithApp fcw tm_in warg) = 
+           let tm = currentFn fname tm_in in
               case matchClause ist toplhs tm of
-                Left _ -> PElabError (Msg (show fc ++ ":with application does not match top level"))
+                Left _ -> PElabError (Msg (show fc ++ ":with application does not match top level "))
                 Right mvars -> 
                    let ns = map (keepMvar (map fst mvars) fcw) ns_in
                        ns' = map (keepMvar (map fst mvars) fcw) ns_in' 
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
@@ -216,8 +216,8 @@
 
     mkLazy (PPi pl n nfc ty sc)
         = let ty' = if getTyName ty
-                       then PApp fc (PRef fc [] (sUN "Lazy'"))
-                            [pexp (PRef fc [] (sUN "LazyCodata")),
+                       then PApp fc (PRef fc [] (sUN "Delayed"))
+                            [pexp (PRef fc [] (sUN "Infinite")),
                              pexp ty]
                        else ty in
               PPi pl n nfc ty' (mkLazy sc)
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
@@ -55,15 +55,17 @@
                 [(Name, Docstring (Either Err PTerm))] ->
                 ElabWhat -> -- phase
                 FC -> [(Name, PTerm)] -> -- constraints
+                [Name] -> -- parent dictionary names (optionally)
                 Accessibility ->
                 FnOpts ->
                 Name -> -- the class
                 FC -> -- precise location of class name
                 [PTerm] -> -- class parameters (i.e. instance)
+                [(Name, PTerm)] -> -- Extra arguments in scope (e.g. instance in where block)
                 PTerm -> -- full instance type
                 Maybe Name -> -- explicit name
                 [PDecl] -> Idris ()
-elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do
+elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t expn ds = do
     ist <- getIState
     (n, ci) <- case lookupCtxtName n (idris_classes ist) of
                   [c] -> return c
@@ -79,7 +81,8 @@
 
     let emptyclass = null (class_methods ci)
     when (what /= EDefns) $ do
-         nty <- elabType' True info syn doc argDocs fc totopts iname NoFC t
+         nty <- elabType' True info syn doc argDocs fc totopts iname NoFC 
+                          (piBindp expl_param pextra t)
          -- if the instance type matches any of the instances we have already,
          -- and it's not a named instance, then it's overlapping, so report an error
          case expn of
@@ -88,6 +91,9 @@
                           addInstance intInst True n iname
             Just _ -> addInstance intInst False n iname
     when (what /= ETypes && (not (null ds && not emptyclass))) $ do
+         -- Add the parent implementation names to the privileged set
+         oldOpen <- addOpenImpl parents
+
          let ips = zip (class_params ci) ps
          let ns = case n of
                     NS n ns' -> ns'
@@ -101,17 +107,31 @@
          ist <- getIState
          let pnames = nub $ map pname (concat (nub wparams)) ++
                           concatMap (namesIn [] ist) ps
+
          let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)
          undefinedSuperclassInstances <- filterM (fmap not . isOverlapping ist) superclassInstances
          mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances
+         
+         ist <- getIState
+         -- Bring variables in instance head into scope when building the
+         -- dictionary
+         let headVars = nub $ concatMap getHeadVars ps
+         let (headVarTypes, ty)
+                = case lookupTyExact iname (tt_ctxt ist) of
+                              Just ty -> (map (\n -> (n, getTypeIn ist n ty)) headVars, ty)
+                              _ -> (zip headVars (repeat Placeholder), Erased)
+         logElab 3 $ "Head var types " ++ show headVarTypes ++ " from " ++ show ty
+         
          let all_meths = map (nsroot . fst) (class_methods ci)
-         let mtys = map (\ (n, (op, t)) ->
+         let mtys = map (\ (n, (inj, op, t)) ->
                    let t_in = substMatchesShadow ips pnames t
-                       mnamemap = map (\n -> (n, PRef fc [] (decorate ns iname n)))
+                       mnamemap = 
+                          map (\n -> (n, PApp fc (PRef fc [] (decorate ns iname n))
+                                              (map (toImp fc) headVars)))
                                       all_meths
                        t' = substMatchesShadow mnamemap pnames t_in in
                        (decorate ns iname n,
-                           op, coninsert cs t', t'))
+                           op, coninsert cs pextra t', t'))
               (class_methods ci)
          logElab 3 (show (mtys, ips))
          logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (class_methods ci)))
@@ -119,38 +139,63 @@
          logElab 3 ("After defaults: " ++ show ds_defs ++ "\n")
          let ds' = reorderDefs (map fst (class_methods ci)) $ ds_defs
          logElab 1 ("Reordered: " ++ show ds' ++ "\n")
+
          mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))
          mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')
          let wbTys = map mkTyDecl mtys
-         let wbVals = map (decorateid (decorate ns iname)) ds'
+         let wbVals_orig = map (decorateid (decorate ns iname)) ds'
+         ist <- getIState
+         let wbVals = map (expandParamsD False ist id pextra (map methName mtys)) wbVals_orig
          let wb = wbTys ++ wbVals
+
          logElab 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)
          logElab 3 $ "Instance is " ++ show ps ++ " implicits " ++
                                       show (concat (nub wparams))
 
-         -- Bring variables in instance head into scope
-         let headVars = nub $ mapMaybe (\p -> case p of
-                                               PRef _ _ n ->
-                                                  case lookupTy n (tt_ctxt ist) of
-                                                      [] -> Just n
-                                                      _ -> Nothing
-                                               _ -> Nothing) ps
---          let lhs = PRef fc iname
-         let lhs = PApp fc (PRef fc [] iname)
-                           (map (\n -> pimp n (PRef fc [] n) True) headVars)
+
+         let lhsImps = map (\n -> pimp n (PRef fc [] n) True) headVars
+
+         let lhs = PApp fc (PRef fc [] iname) (lhsImps ++ map (toExp .fst) pextra)
          let rhs = PApp fc (PRef fc [] (instanceCtorName ci))
-                           (map (pexp . mkMethApp) mtys)
+                           (map (pexp . (mkMethApp lhsImps)) mtys)
 
-         logElab 5 $ "Instance LHS " ++ show totopts ++ "\n" ++ show lhs ++ " " ++ show headVars
+         logElab 5 $ "Instance LHS " ++ show totopts ++ "\n" ++ showTmImpls lhs ++ " " ++ show headVars
          logElab 5 $ "Instance RHS " ++ show rhs
 
-         let idecls = [PClauses fc totopts iname
-                                 [PClause fc iname lhs [] rhs wb]]
-         logElab 1 (show idecls)
          push_estack iname True
+         logElab 3 ("Method types: " ++ show wbTys)
+         logElab 3 ("Method bodies (before params): " ++ show wbVals_orig)
+         logElab 3 ("Method bodies: " ++ show wbVals)
+
+         let idecls = [PClauses fc totopts iname
+                              [PClause fc iname lhs [] rhs []]]
+
+         mapM_ (rec_elabDecl info EAll info) (map (impBind headVarTypes) wbTys)
          mapM_ (rec_elabDecl info EAll info) idecls
+
+         ctxt <- getContext
+         let ifn_ty = case lookupTyExact iname ctxt of
+                           Just t -> t
+                           Nothing -> error "Can't happen (interface constructor)"
+         let ifn_is = case lookupCtxtExact iname (idris_implicits ist) of
+                           Just t -> t
+                           Nothing -> []
+         let prop_params = getParamsInType ist [] ifn_is ifn_ty
+
+         logElab 3 $ "Propagating parameters to methods: " 
+                           ++ show (iname, prop_params)
+
+         let wbVals' = map (addParams prop_params) wbVals
+
+         mapM_ (rec_elabDecl info EAll info) wbVals'
+         
+         mapM_ (checkInjectiveDef fc (class_methods ci)) (zip ds' wbVals')
+
          pop_estack
-         ist <- getIState
+
+         setOpenImpl oldOpen
+--          totalityCheckBlock
+
          checkInjectiveArgs fc n (class_determiners ci) (lookupTyExact iname (tt_ctxt ist))
          addIBC (IBCInstance intInst (isNothing expn) n iname)
 
@@ -166,10 +211,13 @@
                           Just m -> sNS (SN (sInstanceN n' (map show ps'))) m
           Just nm -> nm
 
-    substInstance ips pnames (PInstance doc argDocs syn _ cs acc opts n nfc ps t expn ds)
-        = PInstance doc argDocs syn fc cs acc opts n nfc (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds
+    substInstance ips pnames (PInstance doc argDocs syn _ cs parents acc opts n nfc ps pextra t expn ds)
+        = PInstance doc argDocs syn fc cs parents acc opts n nfc 
+                     (map (substMatchesShadow ips pnames) ps) 
+                     pextra
+                     (substMatchesShadow ips pnames t) expn ds
 
-    isOverlapping i (PInstance doc argDocs syn _ _ _ _ n nfc ps t expn _)
+    isOverlapping i (PInstance doc argDocs syn _ _ _ _ _ n nfc ps pextra t expn _)
         = case lookupCtxtName n (idris_classes i) of
             [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in
                             case lookupTy iname (tt_ctxt i) of
@@ -226,8 +274,15 @@
               map snd (filter (\(i, _) -> i `elem` dets) a')
     keepDets dets t = t
 
-    mkMethApp (n, _, _, ty)
-          = lamBind 0 ty (papp fc (PRef fc [] n) (methArgs 0 ty))
+    methName (n, _, _, _) = n
+    toExp n = pexp (PRef fc [] n) 
+
+    mkMethApp ps (n, _, _, ty) 
+              = lamBind 0 ty (papp fc (PRef fc [] n) 
+                     (ps ++ map (toExp . fst) pextra ++ methArgs 0 ty))
+       where
+          needed is p = pname p `elem` map pname is
+
     lamBind i (PPi (Constraint _ _) _ _ _ sc) sc'
           = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
     lamBind i (PPi _ n _ ty sc) sc'
@@ -254,8 +309,10 @@
                 _ -> return ps'
     getWParams (_ : ps) = getWParams ps
 
-    decorate ns iname (UN n)        = NS (SN (MethodN (UN n))) ns
-    decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns
+    decorate ns iname (NS (UN nm) s)
+         = NS (SN (WhereN 0 iname (SN (MethodN (UN nm))))) ns
+    decorate ns iname nm  
+         = NS (SN (WhereN 0 iname (SN (MethodN nm)))) ns
 
     mkTyDecl (n, op, t, _)
         = PTy emptyDocstring [] syn fc op n NoFC
@@ -265,10 +322,14 @@
     conbind ((c,ty) : ns) x = PPi constraint c NoFC ty (conbind ns x)
     conbind [] x = x
 
-    coninsert :: [(Name, PTerm)] -> PTerm -> PTerm
-    coninsert cs (PPi p@(Imp _ _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs sc)
-    coninsert cs sc = conbind cs sc
+    extrabind :: [(Name, PTerm)] -> PTerm -> PTerm
+    extrabind ((c,ty) : ns) x = PPi expl c NoFC ty (extrabind ns x)
+    extrabind [] x = x
 
+    coninsert :: [(Name, PTerm)] -> [(Name, PTerm)] -> PTerm -> PTerm
+    coninsert cs ex (PPi p@(Imp _ _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs ex sc)
+    coninsert cs ex sc = conbind cs (extrabind ex sc)
+
     -- Reorder declarations to be in the same order as defined in the
     -- class declaration (important so that we insert default definitions
     -- in the right place, and so that dependencies between methods are
@@ -314,6 +375,100 @@
     clauseFor m iname ns (PClauses _ _ m' _)
        = decorate ns iname m == decorate ns iname m'
     clauseFor m iname ns _ = False
+         
+getHeadVars :: PTerm -> [Name]
+getHeadVars (PRef _ _ n) | implicitable n = [n]
+getHeadVars (PApp _ _ args) = concatMap getHeadVars (map getTm args)
+getHeadVars (PPair _ _ _ l r) = getHeadVars l ++ getHeadVars r
+getHeadVars (PDPair _ _ _ l t r) = getHeadVars l ++ getHeadVars t ++ getHeadVars t
+getHeadVars _ = []
+
+-- Implicitly bind variables from the instance head in method types
+impBind :: [(Name, PTerm)] -> PDecl -> PDecl
+impBind vs (PTy d ds syn fc opts n fc' t)
+     = PTy d ds syn fc opts n fc' 
+          (doImpBind (filter (\(n, ty) -> n `notElem` boundIn t) vs) t)
+  where
+    doImpBind [] ty = ty
+    doImpBind ((n, argty) : ns) ty 
+       = PPi impl n NoFC argty (doImpBind ns ty)
+
+    boundIn (PPi _ n _ _ sc) = n : boundIn sc
+    boundIn _ = []
+
+getTypeIn :: IState -> Name -> Type -> PTerm
+getTypeIn ist n (Bind x b sc)
+    | n == x = delab ist (binderTy b)
+    | otherwise = getTypeIn ist n (substV (P Ref x Erased) sc)
+getTypeIn ist n tm = Placeholder
+
+toImp fc n = pimp n (PRef fc [] n) True
+
+-- Propagate class parameters to method bodies, if they're not already 
+-- there, and they are needed (i.e. appear in method's type)
+addParams :: [Name] -> PDecl -> PDecl
+addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)
+  where
+    addCParams (PClause fc n lhs ws rhs wb)
+        = PClause fc n (addTmParams (dropPs (allNamesIn lhs) ps) lhs) ws rhs wb
+    addCParams (PWith fc n lhs ws sc pn ds)
+        = PWith fc n (addTmParams (dropPs (allNamesIn lhs) ps) lhs) ws sc pn 
+                      (map (addParams ps) ds)
+    addCParams c = c
+
+    addTmParams ps (PRef fc hls n) 
+        = PApp fc (PRef fc hls n) (map (toImp fc) ps)
+    addTmParams ps (PApp fc ap@(PRef fc' hls n) args)
+        = PApp fc ap (mergePs (map (toImp fc) ps) args)
+    addTmParams ps tm = tm
+
+    mergePs [] args = args
+    mergePs (p : ps) args
+         | isImplicit p,
+           pname p `notElem` map pname args
+               = p : mergePs ps args
+       where
+         isImplicit (PExp{}) = False
+         isImplicit _ = True
+    mergePs (p : ps) args
+         = mergePs ps args
+
+    -- Don't propagate a parameter if the name is rebound explicitly
+    dropPs :: [Name] -> [Name] -> [Name]
+    dropPs ns = filter (\x -> x `notElem` ns)
+
+addParams ps d = d
+
+-- Check a given method definition is injective, if the class info
+-- says it needs to be.
+-- Takes originally written decl and the one with name decoration, so
+-- we know which name to look up.
+checkInjectiveDef :: FC -> [(Name, (Bool, FnOpts, PTerm))] -> 
+                           (PDecl, PDecl) -> Idris ()
+checkInjectiveDef fc ns (PClauses _ _ n cs, PClauses _ _ elabn _)
+   | Just (True, _, _) <- clookup n ns
+          = do ist <- getIState
+               case lookupDefExact elabn (tt_ctxt ist) of
+                    Just (CaseOp _ _ _ _ _ cdefs) ->
+                       checkInjectiveCase ist (snd (cases_compiletime cdefs))
+  where
+    checkInjectiveCase ist (STerm tm) 
+         = checkInjectiveApp ist (fst (unApply tm))
+    checkInjectiveCase _ _ = notifail
+
+    checkInjectiveApp ist (P (TCon _ _) n _) = return ()
+    checkInjectiveApp ist (P (DCon _ _ _) n _) = return ()
+    checkInjectiveApp ist (P Ref n _) 
+        | Just True <- lookupInjectiveExact n (tt_ctxt ist) = return ()
+    checkInjectiveApp ist (P Ref n _) = notifail
+    checkInjectiveApp _ _ = notifail
+
+    notifail = ierror $ At fc (Msg (show n ++ " must be defined by a type or data constructor"))
+
+    clookup n [] = Nothing
+    clookup n ((n', d) : ds) | nsroot n == nsroot n' = Just d
+                             | otherwise = Nothing
+checkInjectiveDef fc ns _ = return()
 
 checkInjectiveArgs :: FC -> Name -> [Int] -> Maybe Type -> Idris ()
 checkInjectiveArgs fc n ds Nothing = return ()
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
@@ -85,7 +85,7 @@
               mapM_ (\n -> when (n `elem` hs) $
                              do focus n
                                 g <- goal
-                                try (resolveTC' True False 10 g fn ist)
+                                try (resolveTC' True True 10 g fn ist)
                                     (movelast n)) ivs
          ivs <- get_instances
          hs <- get_holes
@@ -313,13 +313,13 @@
 
     forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)
        | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
-            ht == txt "Lazy'" = notDelay orig
+            ht == txt "Delayed" = notDelay orig
     forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)
        | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),
-            ht == txt "Lazy'" = notDelay orig
+            ht == txt "Delayed" = notDelay orig
     forceErr orig env (InfiniteUnify _ t _)
        | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
-            ht == txt "Lazy'" = notDelay orig
+            ht == txt "Delayed" = notDelay orig
     forceErr orig env (Elaborating _ _ _ t) = forceErr orig env t
     forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t
     forceErr orig env (At _ t) = forceErr orig env t
@@ -482,7 +482,7 @@
                      return $ pruneByType env tc (unDelay ty) ist as
 
               unDelay t | (P _ (UN l) _, [_, arg]) <- unApply t,
-                          l == txt "Lazy'" = unDelay arg
+                          l == txt "Delayed" = unDelay arg
                         | otherwise = t
 
               isAmbiguous (CantResolveAlts _) = delayok
@@ -1400,7 +1400,7 @@
            let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)
            let tries = [mkDelay env t, t]
            case tyh of
-                P _ (UN l) _ | l == txt "Lazy'"
+                P _ (UN l) _ | l == txt "Delayed"
                     -> return (PAlternative [] FirstSuccess tries)
                 _ -> return t
       where
@@ -1630,7 +1630,8 @@
     ctxt = tt_ctxt ist
 
     -- Get the function at the head of the alternative and see if it's
-    -- a plausible match against the goal type. Keep if so.
+    -- a plausible match against the goal type. Keep if so. Also keep if
+    -- there is a possible coercion to the goal type.
     headIs var f (PRef _ _ f') = typeHead var f f'
     headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])
         | l == txt "Delay" = headIs var f (getTm arg)
@@ -1652,6 +1653,7 @@
                                           (V _, _) ->
                                               isPlausible ist var env n ty
                                           _ -> matching (getRetTy ty') goalty 
+                                                 || isCoercion (getRetTy ty') goalty
 -- May be useful to keep for debugging purposes for a bit:
 --                                                let res = matching (getRetTy ty') goalty in
 --                                                   traceWhen (not res)
@@ -1678,6 +1680,30 @@
     matching (TType _) (TType _) = True
     matching (UType _) (UType _) = True
     matching l r = l == r
+
+    -- Return whether there is a possible coercion between the return type
+    -- of an alternative and the goal type
+    isCoercion rty gty | (P _ r _, _) <- unApply rty
+            = not (null (getCoercionsBetween r gty))
+    isCoercion _ _ = False
+ 
+    getCoercionsBetween :: Name -> Type -> [Name]
+    getCoercionsBetween r goal
+       = let cs = getCoercionsTo ist goal in
+             findCoercions r cs
+        where findCoercions t [] = []
+              findCoercions t (n : ns) =
+                 let ps = case lookupTy n (tt_ctxt ist) of
+                               [ty'] -> let as = map snd (getArgTys (normalise (tt_ctxt ist) [] ty')) in
+                                            [n | any useR as]
+                               _ -> [] in
+                     ps ++ findCoercions t ns
+
+              useR ty = 
+                  case unApply (getRetTy ty) of
+                       (P _ t _, _) -> t == r
+                       _ -> False
+
 
 pruneByType _ t _ _ as = as
 
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
@@ -426,3 +426,27 @@
     displayImpWarning (fc, n) =
        iputStrLn $ show fc ++ ":WARNING: " ++ show (nsroot n) ++ " is bound as an implicit\n"
                    ++ "\tDid you mean to refer to " ++ show n ++ "?"
+
+propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm
+propagateParams i ps t bound tm@(PApp _ (PRef fc hls n) args)
+     = PApp fc (PRef fc hls n) (addP t args)
+   where addP (Bind n _ sc) (t : ts)
+              | Placeholder <- getTm t,
+                n `elem` ps,
+                not (n `elem` bound)
+                    = t { getTm = PPatvar NoFC n } : addP sc ts
+         addP (Bind n _ sc) (t : ts) = t : addP sc ts
+         addP _ ts = ts
+propagateParams i ps t bound (PApp fc ap args)
+     = PApp fc (propagateParams i ps t bound ap) args
+propagateParams i ps t bound (PRef fc hls n)
+     = case lookupCtxt n (idris_implicits i) of
+            [is] -> let ps' = filter (isImplicit is) ps in
+                        PApp fc (PRef fc hls n) (map (\x -> pimp x (PRef fc [] x) True) ps')
+            _ -> PRef fc hls n
+    where isImplicit [] n = False
+          isImplicit (PImp _ _ _ x _ : is) n | x == n = True
+          isImplicit (_ : is) n = isImplicit is n
+propagateParams i ps t bound x = x
+
+
diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs
--- a/src/Idris/ElabDecls.hs
+++ b/src/Idris/ElabDecls.hs
@@ -239,6 +239,11 @@
     pblock i = map (expandParamsD False i id ns
                       (concatMap tldeclared ps)) ps
 
+elabDecl' what info (POpenInterfaces f ns ds)
+    = do open <- addOpenImpl ns
+         mapM_ (elabDecl' what info) ds
+         setOpenImpl open
+
 elabDecl' what info (PNamespace n nfc ps) =
   do mapM_ (elabDecl' what ninfo) ps
      let ns = reverse (map T.pack newNS)
@@ -251,9 +256,9 @@
   | what /= EDefns
     = do logElab 1 $ "Elaborating class " ++ show n
          elabClass info (s { syn_params = [] }) doc f cs n nfc ps pdocs fds ds cn cd
-elabDecl' what info (PInstance doc argDocs s f cs acc fnopts n nfc ps t expn ds)
+elabDecl' what info (PInstance doc argDocs s f cs pnames acc fnopts n nfc ps pextra t expn ds)
     = do logElab 1 $ "Elaborating instance " ++ show n
-         elabInstance info s doc argDocs what f cs acc fnopts n nfc ps t expn ds
+         elabInstance info s doc argDocs what f cs pnames acc fnopts n nfc ps pextra t expn ds
 elabDecl' what info (PRecord doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn)
     = do logElab 1 $ "Elaborating record " ++ show name
          elabRecord info what doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn
diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs
--- a/src/Idris/IBC.hs
+++ b/src/Idris/IBC.hs
@@ -40,7 +40,7 @@
 import Codec.Archive.Zip
 
 ibcVersion :: Word16
-ibcVersion = 138
+ibcVersion = 143
 
 -- When IBC is being loaded - we'll load different things (and omit different
 -- structures/definitions) depending on which phase we're in
@@ -95,6 +95,7 @@
                          ibc_deprecated :: ![(Name, String)],
                          ibc_defs :: ![(Name, Def)],
                          ibc_total :: ![(Name, Totality)],
+                         ibc_injective :: ![(Name, Injectivity)],
                          ibc_access :: ![(Name, Accessibility)],
                          ibc_fragile :: ![(Name, String)]
                        }
@@ -104,7 +105,7 @@
 !-}
 
 initIBC :: IBCFile
-initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] []
+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] []
 
 hasValidIBCVersion :: FilePath -> Idris Bool
 hasValidIBCVersion fp = do
@@ -197,6 +198,7 @@
                        makeEntry "ibc_deprecated"  (ibc_deprecated i),
                        makeEntry "ibc_defs"  (ibc_defs i),
                        makeEntry "ibc_total"  (ibc_total i),
+                       makeEntry "ibc_injective"  (ibc_injective i),
                        makeEntry "ibc_access"  (ibc_access i),
                        makeEntry "ibc_fragile" (ibc_fragile i)]
 
@@ -300,6 +302,7 @@
 ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }
 ibc i (IBCFnInfo n a) f = return f { ibc_fninfo = (n,a) : ibc_fninfo f }
 ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }
+ibc i (IBCInjective n a) f = return f { ibc_injective = (n,a) : ibc_injective f }
 ibc i (IBCTrans n t) f = return f { ibc_transforms = (n, t) : ibc_transforms f }
 ibc i (IBCErrRev t) f = return f { ibc_errRev = t : ibc_errRev f }
 ibc i (IBCLineApp fp l t) f
@@ -394,6 +397,7 @@
                 processDeprecate archive
                 processDefs archive
                 processTotal archive
+                processInjective archive
                 processAccess reexp phase archive
                 processFragile archive
 
@@ -718,6 +722,11 @@
     ds <- getEntry [] "ibc_total" ar
     mapM_ (\ (n, a) -> updateIState (\i -> i { tt_ctxt = setTotal n a (tt_ctxt i) })) ds
 
+processInjective :: Archive -> Idris ()
+processInjective ar = do
+    ds <- getEntry [] "ibc_injective" ar
+    mapM_ (\ (n, a) -> updateIState (\i -> i { tt_ctxt = setInjective n a (tt_ctxt i) })) ds
+
 processTotalityCheckError :: Archive -> Idris ()
 processTotalityCheckError ar = do
     es <- getEntry [] "ibc_totcheckfail" ar
@@ -1371,7 +1380,7 @@
                                                put x10
                                                put x11
                                                put x12
-                PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ->
+                PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ->
                   do putWord8 8
                      put x1
                      put x2
@@ -1386,6 +1395,8 @@
                      put x11
                      put x12
                      put x13
+                     put x14
+                     put x15
                 PDSL x1 x2 -> do putWord8 9
                                  put x1
                                  put x2
@@ -1427,6 +1438,10 @@
                                             put x1
                                             put x2
                                             put x3
+                POpenInterfaces x1 x2 x3 -> do putWord8 18
+                                               put x1
+                                               put x2
+                                               put x3
         get
           = do i <- getWord8
                case i of
@@ -1502,7 +1517,9 @@
                            x11 <- get
                            x12 <- get
                            x13 <- get
-                           return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)
+                           x14 <- get
+                           x15 <- get
+                           return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)
                    9 -> do x1 <- get
                            x2 <- get
                            return (PDSL x1 x2)
@@ -1542,6 +1559,10 @@
                             x2 <- get
                             x3 <- get
                             return (PRunElabDecl x1 x2 x3)
+                   18 -> do x1 <- get
+                            x2 <- get
+                            x3 <- get
+                            return (POpenInterfaces x1 x2 x3)
                    _ -> error "Corrupted binary data for PDecl'"
 
 instance Binary t => Binary (ProvideWhat' t) where
@@ -1570,7 +1591,7 @@
                     _ -> error "Corrupted binary data for Using"
 
 instance Binary SyntaxInfo where
-        put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _ _ _)
+        put (Syn x1 x2 x3 x4 _ _ x5 x6 x7 _ _ x8 _ _ _)
           = do put x1
                put x2
                put x3
@@ -1578,6 +1599,7 @@
                put x5
                put x6
                put x7
+               put x8
         get
           = do x1 <- get
                x2 <- get
@@ -1586,7 +1608,8 @@
                x5 <- get
                x6 <- get
                x7 <- get
-               return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0 True True)
+               x8 <- get
+               return (Syn x1 x2 x3 x4 [] id x5 x6 x7 Nothing 0 x8 0 True True)
 
 instance (Binary t) => Binary (PClause' t) where
         put x
@@ -2438,13 +2461,25 @@
 instance Binary Codegen where
         put x
           = case x of
-                Via str -> do putWord8 0
-                              put str
+                Via ir str -> do putWord8 0
+                                 put ir
+                                 put str
                 Bytecode -> putWord8 1
         get
           = do i <- getWord8
                case i of
                   0 -> do x1 <- get
-                          return (Via x1)
+                          x2 <- get
+                          return (Via x1 x2)
                   1 -> return Bytecode
                   _ -> error  "Corrupted binary data for Codegen"
+
+instance Binary IRFormat where
+    put x = case x of
+                IBCFormat -> putWord8 0
+                JSONFormat -> putWord8 1
+    get = do i <- getWord8
+             case i of
+                0 -> return IBCFormat
+                1 -> return JSONFormat
+                _ -> error  "Corrupted binary data for IRFormat"
diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs
--- a/src/Idris/Parser.hs
+++ b/src/Idris/Parser.hs
@@ -213,6 +213,7 @@
   where declBody :: Bool -> IdrisParser [PDecl]
         declBody b =
                    try (instance_ True syn)
+                   <|> try (openInterface syn)
                    <|> declBody' b
                    <|> using_ syn
                    <|> params syn
@@ -337,9 +338,9 @@
                   (map (updateNs ns) ds)
                   (updateRecCon ns cname)
                   cdocs
-    updateNs ns (PInstance docs pdocs s fc cs acc opts cn fc' ps ity ni ds)
-         = PInstance docs pdocs s fc cs acc opts (updateB ns cn) fc'
-                     ps ity (fmap (updateB ns) ni)
+    updateNs ns (PInstance docs pdocs s fc cs pnames acc opts cn fc' ps pextra ity ni ds)
+         = PInstance docs pdocs s fc cs pnames acc opts (updateB ns cn) fc'
+                     ps pextra ity (fmap (updateB ns) ni)
                             (map (updateNs ns) ds)
     updateNs ns (PMutual fc ds) = PMutual fc (map (updateNs ns) ds)
     updateNs ns (PProvider docs s fc fc' pw n)
@@ -594,18 +595,12 @@
               do (doc, argDocs, fc, opts', n, nfc, acc) <- try (do
                         pushIndent
                         (doc, argDocs) <- docstring syn
-                        ist <- get
-                        let initOpts = if default_total ist
-                                          then [TotalFn]
-                                          else []
-                        opts <- fnOpts initOpts
-                        acc <- accessibility
-                        opts' <- fnOpts opts
+                        (opts, acc) <- fnOpts
                         (n_in, nfc) <- fnName
                         let n = expandNS syn n_in
                         fc <- getFC
                         lchar ':'
-                        return (doc, argDocs, fc, opts', n, nfc, acc))
+                        return (doc, argDocs, fc, opts, n, nfc, acc))
                  ty <- typeExpr (allowImp syn)
                  terminator
                  -- If it's a top level function, note the accessibility
@@ -633,10 +628,40 @@
                            | otherwise                 = return True
           fixityOK _        = return True
 
-{-| Parses function options given initial options
+{-| Parses a series of function and accessbility options
 
 @
-FnOpts ::= 'total'
+FnOpts ::= FnOpt* Accessibility FnOpt*
+@
+ -}
+fnOpts :: IdrisParser ([FnOpt], Accessibility)
+fnOpts = do
+    opts <- many fnOpt
+    acc <- accessibility
+    opts' <- many fnOpt
+    let allOpts = opts ++ opts'
+    let existingTotality = allOpts `intersect` [TotalFn, CoveringFn, PartialFn]
+    opts'' <- addDefaultTotality (nub existingTotality) allOpts
+    return (opts'', acc)
+  where prettyTot TotalFn = "total"
+        prettyTot PartialFn = "partial"
+        prettyTot CoveringFn = "covering"
+        addDefaultTotality [] opts = do
+          ist <- get
+          case default_total ist of
+            DefaultCheckingTotal    -> return (TotalFn:opts)
+            DefaultCheckingCovering -> return (CoveringFn:opts)
+            DefaultCheckingPartial  -> return opts -- Don't add partial so that --warn-partial still reports warnings if necessary
+        addDefaultTotality [tot] opts = return opts
+        -- Should really be a semantics error instead of a parser error
+        addDefaultTotality (tot1:tot2:tots) opts =
+          fail ("Conflicting totality modifiers specified " ++ prettyTot tot1 ++ " and " ++ prettyTot tot2)
+
+
+{-| Parses a function option
+
+@
+FnOpt ::= 'total'
   | 'partial'
   | 'covering'
   | 'implicit'
@@ -659,37 +684,31 @@
   ;
 @
 -}
--- FIXME: Check compatability for function options (i.e. partal/total)
---
--- Issue #1574 on the issue tracker.
---     https://github.com/idris-lang/Idris-dev/issues/1574
-fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
-fnOpts opts
-        = do reservedHL "total"; fnOpts (TotalFn : opts)
-  <|> do reservedHL "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
-  <|> do reservedHL "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))
-  <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;
-              fnOpts (CExport c : opts)
-  <|> do try (lchar '%' *> reserved "no_implicit");
-              fnOpts (NoImplicit : opts)
-  <|> do try (lchar '%' *> reserved "inline");
-              fnOpts (Inlinable : opts)
-  <|> do try (lchar '%' *> reserved "assert_total");
-              fnOpts (AssertTotal : opts)
-  <|> do try (lchar '%' *> reserved "error_handler");
-             fnOpts (ErrorHandler : opts)
-  <|> do try (lchar '%' *> reserved "error_reverse");
-             fnOpts (ErrorReverse : opts)
-  <|> do try (lchar '%' *> reserved "reflection");
-              fnOpts (Reflection : opts)
-  <|> do try (lchar '%' *> reserved "hint");
-              fnOpts (AutoHint : opts)
-  <|> do lchar '%'; reserved "specialise";
-         lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
-         fnOpts (Specialise ns : opts)
-  <|> do reservedHL "implicit"; fnOpts (Implicit : opts)
-  <|> return opts
-  <?> "function modifier"
+fnOpt :: IdrisParser FnOpt
+fnOpt = do reservedHL "total"; return TotalFn
+        <|> do reservedHL "partial"; return PartialFn
+        <|> do reservedHL "covering"; return CoveringFn
+        <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;
+                    return $ CExport c
+        <|> do try (lchar '%' *> reserved "no_implicit");
+                    return NoImplicit
+        <|> do try (lchar '%' *> reserved "inline");
+                    return Inlinable
+        <|> do try (lchar '%' *> reserved "assert_total");
+                    return AssertTotal
+        <|> do try (lchar '%' *> reserved "error_handler");
+                    return ErrorHandler
+        <|> do try (lchar '%' *> reserved "error_reverse");
+                    return ErrorReverse
+        <|> do try (lchar '%' *> reserved "reflection");
+                    return Reflection
+        <|> do try (lchar '%' *> reserved "hint");
+                    return AutoHint
+        <|> do lchar '%'; reserved "specialise";
+               lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']';
+               return $ Specialise ns
+        <|> do reservedHL "implicit"; return Implicit
+        <?> "function modifier"
   where nameTimes :: IdrisParser (Name, Maybe Int)
         nameTimes = do n <- fst <$> fnName
                        t <- option Nothing (do reds <- fmap fst natural
@@ -711,12 +730,7 @@
                                    ext <- ppostDecl
                                    return (doc, ext)
                    ist <- get
-                   let initOpts = if default_total ist
-                                     then [TotalFn]
-                                     else []
-                   opts <- fnOpts initOpts
-                   acc <- accessibility
-                   opts' <- fnOpts opts
+                   (opts, acc) <- fnOpts
                    (n_in, nfc) <- fnName
                    let n = expandNS syn n_in
                    lchar ':'
@@ -724,7 +738,7 @@
                    fc <- getFC
                    terminator
                    addAcc n acc
-                   return (PPostulate ext doc syn fc nfc opts' n ty)
+                   return (PPostulate ext doc syn fc nfc opts n ty)
                  <?> "postulate"
    where ppostDecl = do fc <- reservedHL "postulate"; return False
                  <|> do lchar '%'; reserved "extern"; return True
@@ -767,6 +781,26 @@
        return [PParams fc ns' (concat ds)]
     <?> "parameters declaration"
 
+{- | Parses an open block
+
+-}
+
+openInterface :: SyntaxInfo -> IdrisParser [PDecl]
+openInterface syn =
+    do reservedHL "using"
+       reservedHL "implementation"
+       fc <- getFC
+       ns <- sepBy1 fnName (lchar ',')
+
+       openBlock
+       ds <- many (decl syn)
+       closeBlock
+       return [POpenInterfaces fc (map fst ns) (concat ds)]
+    <?> "open interface declaration"
+
+
+
+
 {- | Parses a mutual declaration (for mutually recursive functions)
 
 @
@@ -843,7 +877,10 @@
                     ist <- get
                     let cd' = annotate syn ist cd
 
-                    ds <- many (notEndBlock >> try (instance_ True syn) <|> fnDecl syn)
+                    ds <- many (notEndBlock >> try (instance_ True syn)
+                                               <|> do x <- data_ syn
+                                                      return [x]
+                                               <|> fnDecl syn)
                     closeBlock
                     return (cn, cd', concat ds)
                  <?> "class block"
@@ -919,15 +956,8 @@
 instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]
 instance_ kwopt syn
               = do ist <- get
-                   let initOpts = if default_total ist
-                                          then [TotalFn]
-                                          else []
-
                    (doc, argDocs) <- docstring syn
-                   opts <- fnOpts initOpts
-                   acc <- accessibility
-                   opts' <- fnOpts opts
-
+                   (opts, acc) <- fnOpts
                    if kwopt then optional instanceKeyword
                             else do instanceKeyword
                                     return (Just ())
@@ -940,8 +970,9 @@
                    args <- many (simpleExpr syn)
                    let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)
                    let t = bindList (PPi constraint) cs sc
+                   pnames <- instanceUsing
                    ds <- instanceBlock syn
-                   return [PInstance doc argDocs syn fc cs' acc opts' cn cnfc args t en ds]
+                   return [PInstance doc argDocs syn fc cs' pnames acc opts cn cnfc args [] t en ds]
                  <?> "implementation declaration"
   where instanceName :: IdrisParser Name
         instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'
@@ -954,6 +985,12 @@
                              fc <- getFC
                              parserWarning fc Nothing (Msg "The 'instance' keyword is deprecated. Use 'implementation' (or omit it) instead.")
 
+        instanceUsing :: IdrisParser [Name]
+        instanceUsing = do reservedHL "using"
+                           ns <- sepBy1 fnName (lchar ',')
+                           return (map fst ns)
+                        <|> return []
+
 -- | Parse a docstring
 docstring :: SyntaxInfo
           -> IdrisParser (Docstring (Either Err PTerm),
@@ -1013,7 +1050,7 @@
                         t <- typeExpr (disallowImp syn)
                         return (UImplicit x t))
             <|> do c <- fst <$> fnName
-                   xs <- some (fst <$> fnName)
+                   xs <- many (fst <$> fnName)
                    return (UConstraint c xs)
             <?> "using declaration"
 
@@ -1201,13 +1238,12 @@
                    return $ PWith fc n capp wargs wval pn withs)
        <|> do pushIndent
               (n_in, nfc) <- fnName; let n = expandNS syn n_in
-              cargs <- many (constraintArg syn)
               fc <- getFC
               args <- many (try (implicitArg (syn { inPattern = True } ))
+                            <|> try (constraintArg (syn { inPattern = True }))
                             <|> (fmap pexp (argExpr syn)))
               wargs <- many (wExpr syn)
-              let capp = PApp fc (PRef nfc [nfc] n)
-                           (cargs ++ args)
+              let capp = PApp fc (PRef nfc [nfc] n) args
               (do r <- rhs syn n
                   ist <- get
                   let ctxt = tt_ctxt ist
@@ -1288,7 +1324,7 @@
 -}
 codegen_ :: IdrisParser Codegen
 codegen_ = do n <- fst <$> identifier
-              return (Via (map toLower n))
+              return (Via IBCFormat (map toLower n))
        <|> do reserved "Bytecode"; return Bytecode
        <?> "code generation language"
 
@@ -1343,6 +1379,10 @@
                     return [PDirective (DHide n)]
              <|> do try (lchar '%' *> reserved "freeze"); n <- fst <$> iName []
                     return [PDirective (DFreeze n)]
+             -- injectivity assertins are intended for debugging purposes
+             -- only, and won't be documented/could be removed at any point
+             <|> do try (lchar '%' *> reserved "assert_injective"); n <- fst <$> fnName
+                    return [PDirective (DInjective n)]
              <|> do try (lchar '%' *> reserved "access")
                     acc <- accessibility
                     ist <- get
@@ -1396,14 +1436,15 @@
 {- | Parses a totality
 
 @
-Totality ::= 'partial' | 'total'
+Totality ::= 'partial' | 'total' | 'covering'
 @
 
 -}
-totality :: IdrisParser Bool
+totality :: IdrisParser DefaultTotality
 totality
-        = do reservedHL "total";   return True
-      <|> do reservedHL "partial"; return False
+        = do reservedHL "total";   return DefaultCheckingTotal
+      <|> do reservedHL "partial"; return DefaultCheckingPartial
+      <|> do reservedHL "covering"; return DefaultCheckingCovering
 
 {- | Parses a type provider
 
@@ -1768,10 +1809,15 @@
 
                   -- Redo totality check for deferred names
                   let deftots = idris_defertotcheck i
-                  logLvl 1 $ "Totality checking " ++ show deftots
+                  logLvl 2 $ "Totality checking " ++ show deftots
                   mapM_ (\x -> do tot <- getTotality x
                                   case tot of
-                                       Total _ -> setTotality x Unchecked
+                                       Total _ ->
+                                         do let opts = case lookupCtxtExact x (idris_flags i) of
+                                                          Just os -> os
+                                                          Nothing -> []
+                                            when (AssertTotal `notElem` opts) $
+                                                setTotality x Unchecked
                                        _ -> return ()) (map snd deftots)
                   mapM_ buildSCG deftots
                   mapM_ checkDeclTotality deftots
diff --git a/src/Idris/Parser/Data.hs b/src/Idris/Parser/Data.hs
--- a/src/Idris/Parser/Data.hs
+++ b/src/Idris/Parser/Data.hs
@@ -204,18 +204,21 @@
                fc <- getFC
                (tyn_in, nfc) <- fnName
                (do try (lchar ':')
-                   popIndent
                    ty <- typeExpr (allowImp syn)
                    let tyn = expandNS syn tyn_in
-                   option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do
+                   d <- option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do
                      reservedHL "where"
                      cons <- indentedBlock (constructor syn)
                      accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons)
-                     return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons))) <|> (do
-                    args <- many (fst <$> name)
+                     return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons))
+                   terminator
+                   return d) <|> (do
+                    args <- many (do notEndApp
+                                     x <- fst <$> name
+                                     return x)
                     let ty = bindArgs (map (const (PType fc)) args) (PType fc)
                     let tyn = expandNS syn tyn_in
-                    option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do
+                    d <- option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do
                       try (lchar '=') <|> do reservedHL "where"
                                              let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "
                                              let n  = show tyn_in ++ " "
@@ -228,13 +231,14 @@
                                              let fix3 = s ++ ": " ++ ss ++ " -> Type where\n  ..."
                                              fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
                       cons <- sepBy1 (simpleConstructor (syn { withAppAllowed = False })) (reservedOp "|")
-                      terminator
                       let conty = mkPApp fc (PRef fc [] tyn) (map (PRef fc []) args)
                       cons' <- mapM (\ (doc, argDocs, x, xfc, cargs, cfc, fs) ->
                                    do let cty = bindArgs cargs conty
                                       return (doc, argDocs, x, xfc, cty, cfc, fs)) cons
                       accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons')
-                      return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons')))
+                      return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons'))
+                    terminator
+                    return d)
            <?> "data type declaration"
   where
     mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
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
@@ -36,12 +36,18 @@
 
 -- | Allow implicit type declarations
 allowImp :: SyntaxInfo -> SyntaxInfo
-allowImp syn = syn { implicitAllowed = True }
+allowImp syn = syn { implicitAllowed = True,
+                     constraintAllowed = False }
 
 -- | Disallow implicit type declarations
 disallowImp :: SyntaxInfo -> SyntaxInfo
-disallowImp syn = syn { implicitAllowed = False }
+disallowImp syn = syn { implicitAllowed = False,
+                        constraintAllowed = False }
 
+-- | Allow scoped constraint arguments
+allowConstr :: SyntaxInfo -> SyntaxInfo
+allowConstr syn = syn { constraintAllowed = True }
+
 {-| Parses an expression as a whole
 @
   FullExpr ::= Expr EOF_t;
@@ -327,7 +333,7 @@
 @
 -}
 caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
-caseOption syn = do lhs <- expr (syn { inPattern = True })
+caseOption syn = do lhs <- expr (disallowImp (syn { inPattern = True }))
                     r <- impossible <|> symbol "=>" *> expr syn
                     return (lhs, r)
                  <?> "case option"
@@ -432,7 +438,7 @@
         <|> do lchar '_'; return Placeholder
         <?> "expression"
 
-{- |Parses an expression in braces
+{- |Parses an expression in parentheses
 @
 Bracketed ::= '(' Bracketed'
 @
@@ -477,8 +483,8 @@
                          Just o -> return $ PLam fc0 (sMN 1000 "ARG") NoFC Placeholder
                              (PApp fc0 (PRef fc0 [] (sUN o)) [pexp l,
                                                               pexp (PRef fc0 [] (sMN 1000 "ARG"))]))
-        <|> do l <- expr syn
-               bracketedExpr syn open l
+        <|> do l <- expr (allowConstr syn)
+               bracketedExpr (allowConstr syn) open l
 
 
 
@@ -891,7 +897,7 @@
  -}
 typeExpr :: SyntaxInfo -> IdrisParser PTerm
 typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []
-                  sc <- expr syn
+                  sc <- expr (allowConstr syn)
                   return (bindList (PPi constraint) cs sc)
                <?> "type signature"
 
@@ -916,13 +922,13 @@
 -}
 lambda :: SyntaxInfo -> IdrisParser PTerm
 lambda syn = do lchar '\\' <?> "lambda expression"
-                ((do xt <- try $ tyOptDeclList syn
+                ((do xt <- try $ tyOptDeclList (disallowImp syn)
                      fc <- getFC
                      sc <- lambdaTail
                      return (bindList (PLam fc) xt sc))
                  <|>
                  (do ps <- sepBy (do fc <- getFC
-                                     e <- simpleExpr (syn { inPattern = True })
+                                     e <- simpleExpr (disallowImp (syn { inPattern = True }))
                                      return (fc, e))
                                  (lchar ',')
                      sc <- lambdaTail
@@ -1055,7 +1061,7 @@
 explicitPi opts st syn
    = do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')
         binder <- bindsymbol opts st syn
-        sc <- expr syn
+        sc <- expr (allowConstr syn)
         return (bindList (PPi binder) xt sc)
 
 autoImplicit opts st syn
@@ -1064,7 +1070,7 @@
         xt <- typeDeclList syn
         lchar '}'
         symbol "->"
-        sc <- expr syn
+        sc <- expr (allowConstr syn)
         highlightP kw AnnKeyword
         return (bindList (PPi
           (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]))) xt sc)
@@ -1078,7 +1084,7 @@
    xt <- typeDeclList syn
    lchar '}'
    symbol "->"
-   sc <- expr syn
+   sc <- expr (allowConstr syn)
    highlightP kw AnnKeyword
    return (bindList (PPi (TacImp [] Dynamic script)) xt sc)
 
@@ -1096,6 +1102,14 @@
    return (bindList (PPi im) xt
            (bindList (PPi cl) cs sc))
 
+constraintPi opts st syn =
+   do cs <- constraintList1 syn
+      sc <- expr syn
+      if implicitAllowed syn
+         then return (bindList (PPi constraint) cs sc)
+         else return (bindList (PPi (Imp opts st False (Just (Impl True False)) True))
+                               cs sc)
+
 implicitPi opts st syn =
       autoImplicit opts st syn
         <|> defaultImplicit opts st syn
@@ -1114,7 +1128,10 @@
         st   <- static
         explicitPi opts st syn
          <|> try (do lchar '{'; implicitPi opts st syn)
-            <|> unboundPi opts st syn
+         <|> if constraintAllowed syn 
+                then try (constraintPi opts st syn)
+                         <|> unboundPi opts st syn
+                else unboundPi opts st syn
   <?> "dependent type signature"
 
 {- | Parses Possible Options for Pi Expressions
@@ -1152,9 +1169,9 @@
                               return [(defname, NoFC, t)])
                   <?> "type constraint list"
   where nexpr = try (do (n, fc) <- name; lchar ':'
-                        e <- expr syn
+                        e <- expr (disallowImp syn)
                         return (n, fc, e))
-                <|> do e <- expr syn
+                <|> do e <- expr (disallowImp syn)
                        return (defname, NoFC, e)
         defname = sMN 0 "constraint"
 
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
@@ -687,11 +687,12 @@
         fcOf :: PDecl -> FC
         fcOf (PClauses fc _ _ _) = fc
 collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
+collect (POpenInterfaces f ns ps : ds) = POpenInterfaces f ns (collect ps) : collect ds
 collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds
 collect (PNamespace ns fc ps : ds) = PNamespace ns fc (collect ps) : collect ds
 collect (PClass doc f s cs n nfc ps pdocs fds ds cn cd : ds')
     = PClass doc f s cs n nfc ps pdocs fds (collect ds) cn cd : collect ds'
-collect (PInstance doc argDocs f s cs acc opts n nfc ps t en ds : ds')
-    = PInstance doc argDocs f s cs acc opts n nfc ps t en (collect ds) : collect ds'
+collect (PInstance doc argDocs f s cs pnames acc opts n nfc ps pextra t en ds : ds')
+    = PInstance doc argDocs f s cs pnames acc opts n nfc ps pextra t en (collect ds) : collect ds'
 collect (d : ds) = d : collect ds
 collect [] = []
diff --git a/src/Idris/ProofSearch.hs b/src/Idris/ProofSearch.hs
--- a/src/Idris/ProofSearch.hs
+++ b/src/Idris/ProofSearch.hs
@@ -339,25 +339,37 @@
 -- | Resolve interfaces. This will only pick up 'normal' implementations, never
 -- named implementations (which is enforced by 'findInstances').
 resolveTC :: Bool -- ^ using default Int
-          -> Bool -- ^ allow metavariables in the goal
+          -> Bool -- ^ allow open implementations
           -> Int -- ^ depth
           -> Term -- ^ top level goal, for error messages
           -> Name -- ^ top level function name, to prevent loops
           -> (PTerm -> ElabD ()) -- ^ top level elaborator
           -> IState -> ElabD ()
-resolveTC def mvok depth top fn elab ist
-   = do hs <- get_holes
-        resTC' [] def hs depth top fn elab ist
+resolveTC def openOK depth top fn elab ist
+  = do hs <- get_holes
+       resTC' [] def openOK hs depth top fn elab ist
 
-resTC' tcs def topholes 0 topg fn elab ist = fail $ "Can't resolve interface"
-resTC' tcs def topholes 1 topg fn elab ist = try' (trivial elab ist) (resolveTC def False 0 topg fn elab ist) True
-resTC' tcs defaultOn topholes depth topg fn elab ist
+resTC' tcs def openOK topholes 0 topg fn elab ist = fail $ "Can't resolve interface"
+resTC' tcs def openOK topholes 1 topg fn elab ist = try' (trivial elab ist) (resolveTC def False 0 topg fn elab ist) True
+resTC' tcs defaultOn openOK topholes depth topg fn elab ist
   = do compute
-       g <- goal
+       if openOK
+          then try' (resolveOpen (idris_openimpls ist))
+                    resolveNormal
+                    True
+          else resolveNormal
+
+  where
+    -- try all the Open implementations first
+    resolveOpen open = do t <- goal
+                          blunderbuss t depth [] open
+
+    resolveNormal = do
        -- Resolution can proceed only if there is something concrete in the
        -- determining argument positions. Keep track of the holes in the
        -- non-determining position, because it's okay for 'trivial' to solve
        -- those holes and no others.
+       g <- goal
        let (argsok, okholePos) = case tcArgsOK g topholes of
                                     Nothing -> (False, [])
                                     Just hs -> (True, hs)
@@ -380,9 +392,9 @@
             try' (trivialTCs okholes elab ist)
                 (do addDefault t tc ttypes
                     let stk = map fst (filter snd $ elab_stack ist)
-                    let insts = findInstances ist t
+                    let insts = idris_openimpls ist ++ findInstances ist t 
                     blunderbuss t depth stk (stk ++ insts)) True
-  where
+
     -- returns Just hs if okay, where hs are holes which are okay in the
     -- goal, or Nothing if not okay to proceed
     tcArgsOK ty hs | (P _ nc _, as) <- unApply (getRetTy ty), nc == numclass && defaultOn
@@ -491,7 +503,7 @@
                                      let got = fst (unApply (getRetTy t))
                                      let depth' = if tc' `elem` tcs
                                                      then depth - 1 else depth
-                                     resTC' (got : tcs) defaultOn topholes depth' topg fn elab ist)
+                                     resTC' (got : tcs) defaultOn openOK topholes depth' topg fn elab ist)
                       (filter (\ (x, y) -> not x) (zip (map fst imps) args))
                 -- if there's any arguments left, we've failed to resolve
                 hs <- get_holes
diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs
--- a/src/Idris/REPL.hs
+++ b/src/Idris/REPL.hs
@@ -903,8 +903,8 @@
   fixClauses :: PDecl' t -> PDecl' t
   fixClauses (PClauses fc opts _ css@(clause:cs)) =
     PClauses fc opts (getClauseName clause) css
-  fixClauses (PInstance doc argDocs syn fc constraints acc opts cls nfc parms ty instName decls) =
-    PInstance doc argDocs syn fc constraints acc opts cls nfc parms ty instName (map fixClauses decls)
+  fixClauses (PInstance doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty instName decls) =
+    PInstance doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty instName (map fixClauses decls)
   fixClauses decl = decl
 
 process fn (Undefine names) = undefine names
@@ -1249,7 +1249,6 @@
                                             [pexp $ PRef fc [] mainname])
                                return (Just m')
                        ir <- compile codegen f m
-
                        i <- getIState
                        runIO $ generate codegen (fst (head (idris_imported i))) ir
   where fc = fileFC "main"
@@ -1688,7 +1687,7 @@
                               Object else Executable
                      xs -> last xs
        let cgn = case opt getCodegen opts of
-                   [] -> Via "c"
+                   [] -> Via IBCFormat "c"
                    xs -> last xs
        let cgFlags = opt getCodegenArgs opts
 
@@ -1703,7 +1702,7 @@
        let port = getPort opts
 
        when (DefaultTotal `elem` opts) $ do i <- getIState
-                                            putIState (i { default_total = True })
+                                            putIState (i { default_total = DefaultCheckingTotal })
        tty <- runIO $ isATTY
        setColourise $ not quiet && last (tty : opt getColour opts)
 
diff --git a/src/Idris/REPL/Parser.hs b/src/Idris/REPL/Parser.hs
--- a/src/Idris/REPL/Parser.hs
+++ b/src/Idris/REPL/Parser.hs
@@ -358,13 +358,13 @@
 
 cmd_compile :: String -> P.IdrisParser (Either String Command)
 cmd_compile name = do
-    let defaultCodegen = Via "c"
+    let defaultCodegen = Via IBCFormat "c"
 
     let codegenOption :: P.IdrisParser Codegen
         codegenOption = do
             let bytecodeCodegen = discard (P.symbol "bytecode") *> return Bytecode
                 viaCodegen = do x <- fst <$> P.identifier
-                                return (Via (map toLower x))
+                                return (Via IBCFormat (map toLower x))
             bytecodeCodegen <|> viaCodegen
 
     let hasOneArg = do
diff --git a/src/Idris/TypeSearch.hs b/src/Idris/TypeSearch.hs
--- a/src/Idris/TypeSearch.hs
+++ b/src/Idris/TypeSearch.hs
@@ -92,8 +92,8 @@
   matcher = matchTypesBulk istate maxScore ty1
 
 
-typeFromDef :: (Def, b, c, d) -> Maybe Type
-typeFromDef (def, _, _, _) = get def where
+typeFromDef :: (Def, i, b, c, d) -> Maybe Type
+typeFromDef (def, _, _, _, _) = get def where
   get :: Def -> Maybe Type
   get (Function ty _) = Just ty
   get (TyDecl _ ty) = Just ty
@@ -101,10 +101,10 @@
   get (CaseOp _ ty _ _ _ _)  = Just ty
   get _ = Nothing
 
--- Replace all occurences of `Lazy' s t` with `t` in a type
+-- Replace all occurences of `Delayed s t` with `t` in a type
 unLazy :: Type -> Type
 unLazy typ = case typ of
-  App _ (App _ (P _ lazy _) _) ty | lazy == sUN "Lazy'" -> unLazy ty
+  App _ (App _ (P _ lazy _) _) ty | lazy == sUN "Delayed" -> unLazy ty
   Bind name binder ty -> Bind name (fmap unLazy binder) (unLazy ty)
   App s t1 t2 -> App s (unLazy t1) (unLazy t2)
   Proj ty i -> Proj (unLazy ty) i
diff --git a/src/Util/DynamicLinker.hs b/src/Util/DynamicLinker.hs
--- a/src/Util/DynamicLinker.hs
+++ b/src/Util/DynamicLinker.hs
@@ -7,7 +7,7 @@
 import Foreign.LibFFI
 import Foreign.Ptr (Ptr(), nullPtr, FunPtr, nullFunPtr, castPtrToFunPtr)
 import System.Directory
-#ifndef WINDOWS
+#ifndef mingw32_HOST_OS
 import System.Posix.DynamicLinker
 import System.FilePath.Posix ((</>))
 #else
@@ -19,16 +19,14 @@
 #endif
 
 hostDynamicLibExt :: String
-#ifdef LINUX
+#if defined(linux_HOST_OS) || defined(freebsd_HOST_OS) \
+    || defined(dragonfly_HOST_OS) || defined(openbsd_HOST_OS) \
+    || defined(netbsd_HOST_OS)
 hostDynamicLibExt = "so"
-#elif MACOSX
+#elif defined(darwin_HOST_OS)
 hostDynamicLibExt = "dylib"
-#elif WINDOWS
+#elif defined(mingw32_HOST_OS)
 hostDynamicLibExt = "dll"
-#elif FREEBSD
-hostDynamicLibExt = "so"
-#elif DRAGONFLY
-hostDynamicLibExt = "so"
 #else
 hostDynamicLibExt = error $ unwords
   [ "Undefined file extension for dynamic libraries"
@@ -61,7 +59,7 @@
                                    map ("."</>) names ++ [d </> f | d <- cwd:dirs, f <- names]
                           return $ maybe (lib ++ "." ++ hostDynamicLibExt) id found
 
-#ifndef WINDOWS
+#ifndef mingw32_HOST_OS
 tryLoadLib :: [FilePath] -> String -> IO (Maybe DynamicLib)
 tryLoadLib dirs lib = do filename <- libFileName dirs lib
                          handle <- dlopen filename [RTLD_NOW, RTLD_GLOBAL]
diff --git a/test/classes001/ClassName.idr b/test/classes001/ClassName.idr
deleted file mode 100644
--- a/test/classes001/ClassName.idr
+++ /dev/null
@@ -1,49 +0,0 @@
-module ClassName
-
-||| A fancy shower with a constructor
-||| @ a the thing to be shown
-interface MyShow a where
-  ||| Build a MyShow
-  constructor MkMyShow
-  ||| The shower
-  ||| @ x will become a string
-  myShow : (x : a) -> String
-
-twiceAString : MyShow a => a -> String
-twiceAString x = myShow x ++ myShow x
-
-implementation MyShow Integer where
-  myShow x = show x
-
-badShow : MyShow Integer
-badShow = MkMyShow (const "hej")
-
-test1 : twiceAString 2 = "22"
-test1 = Refl
-
-test2 : twiceAString @{ClassName.badShow} 2 = "hejhej"
-test2 = Refl
-
-
-||| Parent interface fun
-interface MyMagma a where
-  constructor MkMyMagma
-  total op : a -> a -> a
-
-||| Semigroup
-interface MyMagma a => MySemigroup a where
-  constructor MkMySemigroup
-  total isAssoc : (x, y, z : a) -> op x $ op y z = op (op x y) z
-
-implementation [addition] MyMagma Nat where
-  op = plus
-
-additionS : MySemigroup Nat
-additionS = MkMySemigroup @{addition} plusAssociative
-
-doIt : MySemigroup a => a -> List a -> a
-doIt x [] = x
-doIt x (y :: xs) = doIt (x `op` y) xs
-
-test : Nat
-test = doIt @{additionS} 22 [1,2,3,4]
diff --git a/test/classes001/expected b/test/classes001/expected
deleted file mode 100644
--- a/test/classes001/expected
+++ /dev/null
@@ -1,29 +0,0 @@
-Interface MyShow
-    A fancy shower with a constructor
-
-Parameters:
-    a   -- the thing to be shown
-
-Methods:
-    myShow : MyShow a => (x : a) -> String
-        The shower
-        
-        The function is Total
-Implementation constructor:
-    MkMyShow : (myShow : a -> String) -> MyShow a
-        Build a MyShow
-        Arguments:
-            (implicit) a : Type  -- the thing to be shown
-            
-            myShow : a -> String  -- The shower
-            
-Implementations:
-    MyShow Integer
-MkMyShow : (myShow : a -> String) -> MyShow a
-    Build a MyShow
-    Arguments:
-        (implicit) a : Type  -- the thing to be shown
-        
-        myShow : a -> String  -- The shower
-        
-    The function is Total
diff --git a/test/classes001/input b/test/classes001/input
deleted file mode 100644
--- a/test/classes001/input
+++ /dev/null
@@ -1,2 +0,0 @@
-:doc MyShow
-:doc MkMyShow
diff --git a/test/classes001/run b/test/classes001/run
deleted file mode 100644
--- a/test/classes001/run
+++ /dev/null
@@ -1,3 +0,0 @@
-#!/usr/bin/env bash
-${IDRIS:-idris} $@ --quiet --nocolour --consolewidth 70 ClassName.idr < input
-rm -f bounded001 *.ibc
diff --git a/test/directives002/directives002.idr b/test/directives002/directives002.idr
new file mode 100644
--- /dev/null
+++ b/test/directives002/directives002.idr
@@ -0,0 +1,14 @@
+module directives002
+
+%access export
+%default covering
+
+loop : ()
+loop = loop
+  
+namespace Main
+  total
+  main : IO ()
+  main = do
+    pure loop
+    putStrLn $ "Hello World"
diff --git a/test/directives002/expected b/test/directives002/expected
new file mode 100644
--- /dev/null
+++ b/test/directives002/expected
@@ -0,0 +1,2 @@
+directives002.idr:12:3:
+directives002.Main.main is possibly not total due to: directives002.loop
diff --git a/test/directives002/run b/test/directives002/run
new file mode 100644
--- /dev/null
+++ b/test/directives002/run
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ directives002.idr --check --nocolour
+
+rm -f directives002 *.ibc
diff --git a/test/interfaces001/ClassName.idr b/test/interfaces001/ClassName.idr
new file mode 100644
--- /dev/null
+++ b/test/interfaces001/ClassName.idr
@@ -0,0 +1,49 @@
+module ClassName
+
+||| A fancy shower with a constructor
+||| @ a the thing to be shown
+interface MyShow a where
+  ||| Build a MyShow
+  constructor MkMyShow
+  ||| The shower
+  ||| @ x will become a string
+  myShow : (x : a) -> String
+
+twiceAString : MyShow a => a -> String
+twiceAString x = myShow x ++ myShow x
+
+implementation MyShow Integer where
+  myShow x = show x
+
+badShow : MyShow Integer
+badShow = MkMyShow (const "hej")
+
+test1 : twiceAString 2 = "22"
+test1 = Refl
+
+test2 : twiceAString @{ClassName.badShow} 2 = "hejhej"
+test2 = Refl
+
+
+||| Parent interface fun
+interface MyMagma a where
+  constructor MkMyMagma
+  total op : a -> a -> a
+
+||| Semigroup
+interface MyMagma a => MySemigroup a where
+  constructor MkMySemigroup
+  total isAssoc : (x, y, z : a) -> op x $ op y z = op (op x y) z
+
+implementation [addition] MyMagma Nat where
+  op = plus
+
+additionS : MySemigroup Nat
+additionS = MkMySemigroup @{addition} plusAssociative
+
+doIt : MySemigroup a => a -> List a -> a
+doIt x [] = x
+doIt x (y :: xs) = doIt (x `op` y) xs
+
+test : Nat
+test = doIt @{additionS} 22 [1,2,3,4]
diff --git a/test/interfaces001/expected b/test/interfaces001/expected
new file mode 100644
--- /dev/null
+++ b/test/interfaces001/expected
@@ -0,0 +1,29 @@
+Interface MyShow
+    A fancy shower with a constructor
+
+Parameters:
+    a   -- the thing to be shown
+
+Methods:
+    myShow : MyShow a => (x : a) -> String
+        The shower
+        
+        The function is Total
+Implementation constructor:
+    MkMyShow : (myShow : a -> String) -> MyShow a
+        Build a MyShow
+        Arguments:
+            (implicit) a : Type  -- the thing to be shown
+            
+            myShow : a -> String  -- The shower
+            
+Implementations:
+    MyShow Integer
+MkMyShow : (myShow : a -> String) -> MyShow a
+    Build a MyShow
+    Arguments:
+        (implicit) a : Type  -- the thing to be shown
+        
+        myShow : a -> String  -- The shower
+        
+    The function is Total
diff --git a/test/interfaces001/input b/test/interfaces001/input
new file mode 100644
--- /dev/null
+++ b/test/interfaces001/input
@@ -0,0 +1,2 @@
+:doc MyShow
+:doc MkMyShow
diff --git a/test/interfaces001/run b/test/interfaces001/run
new file mode 100644
--- /dev/null
+++ b/test/interfaces001/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ --quiet --nocolour --consolewidth 70 ClassName.idr < input
+rm -f *.ibc
diff --git a/test/interfaces002/expected b/test/interfaces002/expected
new file mode 100644
--- /dev/null
+++ b/test/interfaces002/expected
@@ -0,0 +1,1 @@
+41
diff --git a/test/interfaces002/interfaces002.idr b/test/interfaces002/interfaces002.idr
new file mode 100644
--- /dev/null
+++ b/test/interfaces002/interfaces002.idr
@@ -0,0 +1,39 @@
+import Data.Vect
+
+interface ArrayM where
+  Array : (n : Nat) -> (a : Type) -> Type
+  
+  create : (n : Nat) -> a -> Array n a
+
+  lkp : (i : Nat) -> (prf : LTE (S i) n) -> Array n a -> a
+  upd : a -> (i : Nat) -> (prf : LT i n) -> Array n a -> Array n a
+
+using (ArrayM)
+  sumArrayHelp : Num a => (k : Nat) -> LT k (S n) -> Array n a -> a
+  sumArrayHelp Z x y = 0
+  sumArrayHelp (S k) (LTESucc prf) y 
+    = lkp k prf y + sumArrayHelp k (lteSuccRight prf) y
+
+  sumArray : Array n Int -> Int
+  sumArray {n} x = sumArrayHelp n lteRefl x
+
+implementation ArrayM where
+  Array = Vect 
+
+  create n x = replicate n x
+
+  lkp Z (LTESucc x) (y :: xs) = y
+  lkp (S k) (LTESucc x) (y :: xs) = lkp k x xs
+
+  upd val Z (LTESucc p) (_ :: xs) = val :: xs 
+  upd val (S k) (LTESucc p) (x :: xs) = x :: upd val k p xs
+
+-- using (ArrayM as vectArray)
+
+testSum : Array n Int -> Int
+testSum = sumArray 
+
+main : IO ()
+main = printLn (testSum (upd 11 1 (LTESucc (LTESucc LTEZero)) (create 4 10)))
+
+
diff --git a/test/interfaces002/run b/test/interfaces002/run
new file mode 100644
--- /dev/null
+++ b/test/interfaces002/run
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces002.idr -o interfaces002
+./interfaces002
+rm -f interfaces002 *.ibc
diff --git a/test/interfaces003/expected b/test/interfaces003/expected
new file mode 100644
--- /dev/null
+++ b/test/interfaces003/expected
@@ -0,0 +1,2 @@
+10
+9
diff --git a/test/interfaces003/interfaces003.idr b/test/interfaces003/interfaces003.idr
new file mode 100644
--- /dev/null
+++ b/test/interfaces003/interfaces003.idr
@@ -0,0 +1,22 @@
+interface NumMod where
+    number : Bool -> Int
+
+implementation [Five] NumMod where
+    number b = 5
+
+foo : NumMod => Int
+foo = number True + number False
+
+Increment : Int -> NumMod -> NumMod
+Increment inc x = AddOne
+   where
+     foo : NumMod
+     foo = x
+
+     implementation [AddOne] NumMod where
+       number x = if x then number@{foo} x + inc else inc
+
+using implementation Five
+  main : IO ()
+  main = do printLn foo 
+            printLn (foo @{Increment 2 Five})
diff --git a/test/interfaces003/run b/test/interfaces003/run
new file mode 100644
--- /dev/null
+++ b/test/interfaces003/run
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces003.idr -o interfaces003
+./interfaces003
+rm -f interfaces003 *.ibc
diff --git a/test/interfaces004/expected b/test/interfaces004/expected
new file mode 100644
--- /dev/null
+++ b/test/interfaces004/expected
@@ -0,0 +1,4 @@
+12
+36
+True
+False
diff --git a/test/interfaces004/interfaces004.idr b/test/interfaces004/interfaces004.idr
new file mode 100644
--- /dev/null
+++ b/test/interfaces004/interfaces004.idr
@@ -0,0 +1,35 @@
+
+[PlusNatSemi] Semigroup Nat where
+  (<+>) x y = x + y
+
+[MultNatSemi] Semigroup Nat where
+  (<+>) x y = x * y
+
+[PlusNatMonoid] Monoid Nat using PlusNatSemi where
+  neutral = 0
+
+[MultNatMonoid] Monoid Nat using MultNatSemi where
+  neutral = 1
+
+test : Monoid a => a -> a
+test x = x <+> x <+> neutral
+
+[CmpLess] Ord Int where
+  compare x y = if (x == y) then EQ else
+                   if (boolOp prim__sltInt x y) then GT else LT
+
+foo : Int -> Int -> Bool
+foo x y = x < y
+
+using implementation CmpLess
+  foo' : Int -> Int -> Bool
+  foo' x y = x < y
+
+using implementation PlusNatMonoid
+  main : IO ()
+  main = do printLn (test (the Nat 6))
+            printLn (test @{MultNatMonoid} 6)
+            
+            printLn (foo 3 4)
+            printLn (foo' 3 4)
+            
diff --git a/test/interfaces004/run b/test/interfaces004/run
new file mode 100644
--- /dev/null
+++ b/test/interfaces004/run
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces004.idr -o interfaces004
+./interfaces004
+rm -f interfaces004 *.ibc
diff --git a/test/interfaces005/expected b/test/interfaces005/expected
new file mode 100644
--- /dev/null
+++ b/test/interfaces005/expected
@@ -0,0 +1,7 @@
+interfaces005a.idr:18:3:
+Set.TreeSet.Set must be defined by a type or data constructor
+No such variable TreeSet
+interfaces005b.idr:4:11:
+Data definitions not allowed in a class declaration
+interfaces005b.idr:18:3:SetSig is not an interface
+No such variable TreeSet
diff --git a/test/interfaces005/interfaces005.idr b/test/interfaces005/interfaces005.idr
new file mode 100644
--- /dev/null
+++ b/test/interfaces005/interfaces005.idr
@@ -0,0 +1,53 @@
+module Set
+ 
+public export
+interface SetSig a where
+  data SetT : Type -> Type
+
+  new : SetT a
+  insert : a -> SetT a -> SetT a
+  member : a -> SetT a -> Bool
+
+Set : (a : Type) -> SetSig a => Type
+Set (a) @{sig} = SetT @{sig} a
+
+data Tree a = Leaf | Node (Tree a) a (Tree a)
+
+mkTree : Type -> Type
+mkTree = Tree
+
+namespace TreeSet
+  export
+  [TreeSet] Ord a => SetSig a where
+
+    SetT = Tree 
+
+    new = Leaf
+
+    insert x Leaf = Node Leaf x Leaf
+    insert x (Node l val r) = case compare x val of
+                                   LT => Node (insert x l) val r
+                                   EQ => Node l val r
+                                   GT => Node l val (insert x r)
+
+    member x Leaf = False
+    member x (Node l val r) = case compare x val of
+                                   LT => member x l
+                                   EQ => True
+                                   GT => member x r
+
+using implementation TreeSet
+
+  test : Set Nat
+  test = insert 3 $ 
+         insert 2 $ 
+         insert 7 $ 
+         insert 3 $ 
+         insert 4 $ 
+         insert 5 new 
+
+  foo : Bool
+  foo = member 6 test
+
+  bar : Bool
+  bar = member 3 test
diff --git a/test/interfaces005/interfaces005a.idr b/test/interfaces005/interfaces005a.idr
new file mode 100644
--- /dev/null
+++ b/test/interfaces005/interfaces005a.idr
@@ -0,0 +1,50 @@
+module Set
+ 
+public export
+interface SetSig a where
+  data Set : Type -> Type
+
+  new : Set a
+  insert : a -> Set a -> Set a
+  member : a -> Set a -> Bool
+
+data Tree a = Leaf | Node (Tree a) a (Tree a)
+
+mkTree : Type -> Type
+mkTree = Tree
+
+namespace TreeSet
+  export
+  [TreeSet] Ord a => SetSig a where
+
+    Set = mkTree 
+
+    new = Leaf
+
+    insert x Leaf = Node Leaf x Leaf
+    insert x (Node l val r) = case compare x val of
+                                   LT => Node (insert x l) val r
+                                   EQ => Node l val r
+                                   GT => Node l val (insert x r)
+
+    member x Leaf = False
+    member x (Node l val r) = case compare x val of
+                                   LT => member x l
+                                   EQ => True
+                                   GT => member x r
+
+using implementation TreeSet
+
+  test : Set @{TreeSet {a=Nat}} Nat
+  test = insert 3 $ 
+         insert 2 $ 
+         insert 7 $ 
+         insert 3 $ 
+         insert 4 $ 
+         insert 5 new 
+
+  foo : Bool
+  foo = member 6 test
+
+  bar : Bool
+  bar = member 3 test
diff --git a/test/interfaces005/interfaces005b.idr b/test/interfaces005/interfaces005b.idr
new file mode 100644
--- /dev/null
+++ b/test/interfaces005/interfaces005b.idr
@@ -0,0 +1,50 @@
+module Set
+ 
+public export
+interface SetSig a where
+  data Set : Type -> Type where MkSet : List a -> Set a
+
+  new : Set a
+  insert : a -> Set a -> Set a
+  member : a -> Set a -> Bool
+
+data Tree a = Leaf | Node (Tree a) a (Tree a)
+
+mkTree : Type -> Type
+mkTree = Tree
+
+namespace TreeSet
+  export
+  [TreeSet] Ord a => SetSig a where
+
+    Set = Tree 
+
+    new = Leaf
+
+    insert x Leaf = Node Leaf x Leaf
+    insert x (Node l val r) = case compare x val of
+                                   LT => Node (insert x l) val r
+                                   EQ => Node l val r
+                                   GT => Node l val (insert x r)
+
+    member x Leaf = False
+    member x (Node l val r) = case compare x val of
+                                   LT => member x l
+                                   EQ => True
+                                   GT => member x r
+
+using implementation TreeSet
+
+  test : Set @{TreeSet {a=Nat}} Nat
+  test = insert 3 $ 
+         insert 2 $ 
+         insert 7 $ 
+         insert 3 $ 
+         insert 4 $ 
+         insert 5 new 
+
+  foo : Bool
+  foo = member 6 test
+
+  bar : Bool
+  bar = member 3 test
diff --git a/test/interfaces005/run b/test/interfaces005/run
new file mode 100644
--- /dev/null
+++ b/test/interfaces005/run
@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces005.idr --check
+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces005a.idr --check
+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces005b.idr --check
+rm -rf *.ibc
diff --git a/test/reg072/expected b/test/reg072/expected
--- a/test/reg072/expected
+++ b/test/reg072/expected
@@ -6,7 +6,7 @@
         Type mismatch between
                 x = x (Type of Refl)
         and
-                negate 0.0 = 0.0 (Expected type)
+                (-0.0) = 0.0 (Expected type)
         
         Specifically:
                 Type mismatch between