diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,36 @@
+# New in 0.13:
+
+## Language updates
+
+* `record` syntax now allows updating fields, including nested fields,
+  by applying a function using the `$=` operator.  For example:
+
+  ```
+  record Score where
+         constructor MkScore
+         correct : Nat
+         attempted : Nat
+
+  record GameState where
+         constructor MkGameState
+         score : Score
+         difficulty : Nat
+
+  correct : GameState -> GameState
+  correct st = record { score->correct $= (+1),
+                        score->attempted $= (+1) } st
+  ```
+
+## Library updates
+
+* The File Effect has been updated to take into account changes in
+  `Prelude.File` and to provide a 'better' API.
+
+## Tool updates
+
+* Idris' documentation system now displays the documentation for auto
+  implicits in the output of `:doc`. This is tested for in `docs005`.
+
 # New in 0.12:
 
 ## Language updates
diff --git a/CONTRIBUTORS b/CONTRIBUTORS
--- a/CONTRIBUTORS
+++ b/CONTRIBUTORS
@@ -3,20 +3,22 @@
 Ozgur Akgun
 Ahmad Salim Al-Sibahi
 Edward Chadwick Amsden
-Jan Bessai
 Michael R. Bernstein
+Jan Bessai
 Nicola Botta
 Edwin Brady
 Jakob Brünker
 Alyssa Carter
-David Raymond Christiansen
 Carter Charbonneau
+David Raymond Christiansen
 Aaron Craelius
 Jason Dagit
+Adam Sandberg Eriksson
 Guglielmo Fachini
 Simon Fowler
 Google
 Zack Grannan
+Sean Hunt
 Cezar Ionescu
 Heath Johns
 Irene Knapp
@@ -27,14 +29,14 @@
 Hannes Mehnert
 Mekeor Melire
 Melissa Mozifian
-Dominic Mulligan
 Jan de Muijnck-Hughes
+Dominic Mulligan
+Echo Nolan
 Tom Prince
 raichoo
 Philip Rasmussen
 Aistis Raulinaitis
 Reynir Reynisson
-Adam Sandberg Eriksson
 Seo Sanghyeon
 Benjamin Saunders
 Alexander Shabalin
@@ -47,5 +49,5 @@
 Dirk Ullrich
 Leif Warner
 Daniel Waterworth
+Eric Weinstein
 Jonas Westerlund
-Sean Hunt
diff --git a/idris.cabal b/idris.cabal
--- a/idris.cabal
+++ b/idris.cabal
@@ -1,5 +1,5 @@
 Name:           idris
-Version:        0.12
+Version:        0.12.1
 License:        BSD3
 License-file:   LICENSE
 Author:         Edwin Brady
@@ -580,6 +580,9 @@
                        test/interfaces005/*.idr
                        test/interfaces005/run
                        test/interfaces005/expected
+                       test/interfaces006/*.idr
+                       test/interfaces006/run
+                       test/interfaces006/expected
 
                        test/io001/run
                        test/io001/*.idr
@@ -708,6 +711,12 @@
                        test/records003/run
                        test/records003/*.idr
                        test/records003/expected
+                       test/records004/run
+                       test/records004/*.idr
+                       test/records004/expected
+                       test/records005/run
+                       test/records005/*.idr
+                       test/records005/expected
 
                        test/sourceLocation001/run
                        test/sourceLocation001/*.idr
@@ -849,7 +858,16 @@
                        test/docs003/input
                        test/docs003/*.idr
                        test/docs003/expected
+                       test/docs004/run
+                       test/docs004/input
+                       test/docs004/*.idr
+                       test/docs004/expected
+                       test/docs005/run
+                       test/docs005/input
+                       test/docs005/*.idr
+                       test/docs005/expected
 
+
                        benchmarks/ALL
                        benchmarks/*.pl
                        benchmarks/README
@@ -1026,8 +1044,9 @@
                 , annotated-wl-pprint >= 0.7 && < 0.8
                 , ansi-terminal < 0.7
                 , ansi-wl-pprint < 0.7
+                , array >= 0.4.0.1 && < 0.6
                 , base64-bytestring < 1.1
-                , binary >= 0.7 && < 0.8
+                , binary >= 0.7 && < 0.9
                 , blaze-html >= 0.6.1.3 && < 0.9
                 , blaze-markup >= 0.5.2.1 && < 0.8
                 , bytestring < 0.11
@@ -1044,14 +1063,14 @@
                 , optparse-applicative >= 0.11 && < 0.13
                 , parsers >= 0.9 && < 0.13
                 , pretty < 1.2
-                , process < 1.3
+                , regex-tdfa >= 1.2
                 , split < 0.3
                 , terminal-size < 0.4
                 , text >=1.2.1.0 && < 1.3
-                , time >= 1.4 && < 1.6
-                , transformers < 0.5
+                , time >= 1.4 && < 1.7
+                , transformers < 0.6
                 , transformers-compat >= 0.3
-                , trifecta >= 1.1 && < 1.6
+                , trifecta >= 1.6 && < 1.7
                 , uniplate >=1.6 && < 1.7
                 , unordered-containers < 0.3
                 , utf8-string < 1.1
@@ -1062,9 +1081,14 @@
                 , fsnotify >= 0.2 && < 2.2
                 , async < 2.2
 
+
   -- zlib >= 0.6.1 is broken with GHC < 7.10.3
+  -- Travis is broken for 7.6 and 7.8 with a newer process
   if impl(ghc < 7.10.3)
      build-depends: zlib < 0.6.1
+                  , process < 1.3
+  else
+     build-depends: process < 1.5
 
   Extensions:     MultiParamTypeClasses
                 , DeriveFoldable
diff --git a/libs/base/Control/Monad/RWS.idr b/libs/base/Control/Monad/RWS.idr
--- a/libs/base/Control/Monad/RWS.idr
+++ b/libs/base/Control/Monad/RWS.idr
@@ -8,7 +8,7 @@
 %access public export
 
 ||| A combination of the Reader, Writer, and State monads
-interface (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadRWS r w s (m : Type -> Type) where {}
+interface (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadRWS r w s (m : Type -> Type) | m where {}
 
 ||| The transformer on which the RWS monad is based
 record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where
diff --git a/libs/base/Control/Monad/Reader.idr b/libs/base/Control/Monad/Reader.idr
--- a/libs/base/Control/Monad/Reader.idr
+++ b/libs/base/Control/Monad/Reader.idr
@@ -7,7 +7,7 @@
 %access public export
 
 ||| A monad representing a computation that runs in an immutable context
-interface Monad m => MonadReader r (m : Type -> Type) where
+interface Monad m => MonadReader r (m : Type -> Type) | m where
     ||| Return the context
     ask   : m r
     ||| Temprorarily modify the input and run an action in the new context
diff --git a/libs/base/Control/Monad/State.idr b/libs/base/Control/Monad/State.idr
--- a/libs/base/Control/Monad/State.idr
+++ b/libs/base/Control/Monad/State.idr
@@ -6,64 +6,64 @@
 %access public export
 
 ||| A computation which runs in a context and produces an output
-interface Monad m => MonadState s (m : Type -> Type) | m where
+interface Monad m => MonadState stateType (m : Type -> Type) | m where
     ||| Get the context
-    get : m s
+    get : m stateType
     ||| Write a new context/output
-    put : s -> m ()
+    put : stateType -> m ()
 
 ||| The transformer on which the State monad is based
-record StateT (s : Type) (m : Type -> Type) (a : Type) where
+record StateT (stateType : Type) (m : Type -> Type) (a : Type) where
   constructor ST
-  runStateT : s -> m (a, s)
+  runStateT : stateType -> m (a, stateType)
 
-implementation Functor f => Functor (StateT s f) where
+implementation Functor f => Functor (StateT stateType f) where
     map f (ST g) = ST (\st => map (mapFst f) (g st)) where
        mapFst : (a -> x) -> (a, s) -> (x, s)
        mapFst fn (a, b) = (fn a, b)
 
-implementation Monad f => Applicative (StateT s f) where
+implementation Monad f => Applicative (StateT stateType f) where
     pure x = ST (\st => pure (x, st))
 
     (ST f) <*> (ST a) = ST (\st => do (g, r) <- f st
                                       (b, t) <- a r
                                       return (g b, t))
 
-implementation Monad m => Monad (StateT s m) where
+implementation Monad m => Monad (StateT stateType m) where
     (ST f) >>= k = ST (\st => do (v, st') <- f st
                                  let ST kv = k v
                                  kv st')
 
-implementation Monad m => MonadState s (StateT s m) where
+implementation Monad m => MonadState stateType (StateT stateType m) where
     get   = ST (\x => return (x, x))
     put x = ST (\y => return ((), x))
 
-implementation MonadTrans (StateT s) where
+implementation MonadTrans (StateT stateType) where
     lift x = ST (\st => do r <- x
                            return (r, st))
 
 ||| Apply a function to modify the context of this computation
-modify : MonadState s m => (s -> s) -> m ()
+modify : MonadState stateType m => (stateType -> stateType) -> m ()
 modify f = do s <- get
               put (f s)
 
 ||| Evaluate a function in the context held by this computation
-gets : MonadState s m => (s -> a) -> m a
+gets : MonadState stateType m => (stateType -> a) -> m a
 gets f = do s <- get
             return (f s)
 
 ||| The State monad. See the MonadState interface
-State : Type -> Type -> Type
+State : (stateType : Type) -> (ty : Type) -> Type
 State = \s, a => StateT s Identity a
 
 ||| Unwrap a State monad computation.
-runState : StateT s Identity a -> s -> (a, s)
+runState : StateT stateType Identity a -> stateType -> (a, stateType)
 runState act = runIdentity . runStateT act
 
 ||| Unwrap a State monad computation, but discard the final state.
-evalState : State s a -> s -> a
+evalState : State stateType a -> stateType -> a
 evalState m = fst . runState m
 
 ||| Unwrap a State monad computation, but discard the resulting value.
-execState : State s a -> s -> s
+execState : State stateType a -> stateType -> stateType
 execState m = snd . runState m
diff --git a/libs/base/Control/Monad/Writer.idr b/libs/base/Control/Monad/Writer.idr
--- a/libs/base/Control/Monad/Writer.idr
+++ b/libs/base/Control/Monad/Writer.idr
@@ -7,7 +7,7 @@
 %access public export
 
 ||| A monad representing a computation that produces a stream of output
-interface (Monoid w, Monad m) => MonadWriter w (m : Type -> Type) where
+interface (Monoid w, Monad m) => MonadWriter w (m : Type -> Type) | m where
     ||| tell w produces the output w
     tell   : w -> m ()
     ||| Execute an action and add it's output to the value of the computation
diff --git a/libs/effects/Effect/File.idr b/libs/effects/Effect/File.idr
--- a/libs/effects/Effect/File.idr
+++ b/libs/effects/Effect/File.idr
@@ -1,4 +1,4 @@
--- -------------------------------------------------------- [ Effectful FileIO ]
+||| Effectful file operations.
 module Effect.File
 
 import Effects
@@ -6,188 +6,423 @@
 
 %access public export
 
-||| A Dependent type to describe File Handles. File handles are
-||| parameterised with the current state of the file: Closed; Open for
-||| reading; and Open for writing.
-|||
-||| @ m The file mode.
-data OpenFile : (m : Mode) -> Type where
-     FH : File -> OpenFile m
+-- -------------------------------------------------------------- [ Predicates ]
 
-openOK : Mode -> Bool -> Type
-openOK m True = OpenFile m
-openOK m False = ()
+||| A record of the file modes that can read from a file.
+data ValidModeRead : Mode -> Type where
+  VMRRead   : ValidModeRead Read
+  VMRReadW  : ValidModeRead ReadWrite
+  VMRReadWT : ValidModeRead ReadWriteTruncate
+  VMRReadA  : ValidModeRead ReadAppend
 
--- ------------------------------------------------------------ [ The Protocol ]
+||| A record of the file modes that can write from a file.
+data ValidModeWrite : Mode -> Type where
+  VMWWrite  : ValidModeWrite WriteTruncate
+  VMWAppend : ValidModeWrite Append
+  VMWReadW  : ValidModeWrite ReadWrite
+  VMWReadWT : ValidModeWrite ReadWriteTruncate
 
-||| Here the protocol for resource access is defined as an effect.
-||| The state transitions diagram for the protocol is as follows:
-|||
-|||     digraph G {
+-- -------------------------------------------------- [ Custom Error Reporting ]
+
+namespace FileResult
+
+  ||| A type to describe the return type of file operations.
+  data ResultDesc = SUCCESS | RESULT
+
+  ||| A custom return type for file operations that is dependent on
+  ||| the type of file operation.
+  |||
+  ||| @desc Parameterises the constructors to describe if the function
+  |||       returns a value or not.
+  ||| @ty   The return type for a file operation that returns a value.
+  |||
+  data FileOpReturnTy : (desc : ResultDesc)
+                     -> (ty : Type)
+                     -> Type where
+
+    ||| The operation completed successfully and doesn't return a
+    ||| result.
+    Success : FileOpReturnTy SUCCESS ty
+
+    ||| The operation returns a result of type `ty`.
+    |||
+    ||| @ty The value returned.
+    Result : ty -> FileOpReturnTy RESULT ty
+
+    ||| The operation failed and the RTS produced the given error.
+    |||
+    ||| @err The reported error code.
+    FError : (err : FileError) -> FileOpReturnTy desc ty
+
+  ||| Type alias to describe a file operatons that returns a result.
+  FileOpResult : Type -> Type
+  FileOpResult ty = FileOpReturnTy RESULT ty
+
+  ||| Type alias to describe file oeprations that indicate success.
+  FileOpSuccess : Type
+  FileOpSuccess = FileOpReturnTy SUCCESS ()
+
+-- ------------------------------------------------------------ [ The Resource ]
+
+||| The file handle associated with the effect.
 |||
-|||       empty; read; write; // States
+||| @m The `Mode` that the handle was generated under.
+data FileHandle : (m : Mode) -> Type where
+    FH : File -> FileHandle m
+
+-- ---------------------------------------------- [ Resource Type Construction ]
+
+||| Calculates the type for the resource being computed over.  `Unit`
+||| to describe pre-and-post file handle acquisistion, and `FileHandle
+||| m` when a file handle has been aqcuired.
 |||
-|||       empty -> read [label="Open R"];
-|||       read -> empty [label="Close"];
-|||       read -> read [label="ReadLine"];
-|||       read -> read [label="EOF"];
+||| @m The mode the file handle was generated under.
+||| @ty The functions return type.
+calcResourceTy : (m  : Mode)
+              -> (ty : FileOpReturnTy fOpTy retTy)
+              -> Type
+calcResourceTy _ (FError e) = ()
+calcResourceTy m _          = FileHandle m
+
+-- ------------------------------------------------------- [ Effect Definition ]
+
+||| An effect to describe operations on a file.
+data FileE : Effect where
+
+  -- Open/Close
+
+  Open : (fname : String)
+      -> (m : Mode)
+      -> sig FileE
+             (FileOpSuccess)
+             ()
+             (\res => calcResourceTy m res)
+
+  OpenX : (fname : String)
+       -> (m : Mode)
+       -> sig FileE
+              (FileOpSuccess)
+              ()
+              (\res => calcResourceTy m res)
+
+  Close : sig FileE () (FileHandle m) ()
+
+  -- Read
+
+  FGetC : {auto prf : ValidModeRead m}
+       -> sig FileE
+              (FileOpResult Char)
+              (FileHandle m)
+              (FileHandle m)
+
+  FGetLine : {auto prf : ValidModeRead m}
+          -> sig FileE
+                 (FileOpResult String)
+                 (FileHandle m)
+                 (FileHandle m)
+
+  FReadFile : (fname : String)
+           -> sig FileE
+                  (FileOpResult String)
+                  ()
+                  ()
+  -- Write
+  FPutStr : (str : String)
+         -> {auto prf : ValidModeWrite m}
+         -> sig FileE
+                (FileOpSuccess)
+                (FileHandle m)
+                (FileHandle m)
+
+  FPutStrLn : (str : String)
+           -> {auto prf : ValidModeWrite m}
+           -> sig FileE
+                  (FileOpSuccess)
+                  (FileHandle m)
+                  (FileHandle m)
+
+  FWriteFile : (fname    : String)
+            -> (contents : String)
+            -> sig FileE
+                   (FileOpSuccess)
+                   ()
+
+  -- Flush
+  FFlush : sig FileE
+               ()
+               (FileHandle m)
+               (FileHandle m)
+
+  -- Query
+  FEOF : {auto prf : ValidModeRead m}
+      -> sig FileE
+             Bool
+             (FileHandle m)
+
+-- ---------------------------------------------------------------------- [ IO ]
+
+Handler FileE IO where
+
+  -- Open Close
+  handle () (Open fname m) k = do
+      res <- openFile fname m
+      case res of
+        Left err => k (FError err) ()
+        Right fh => k Success      (FH fh)
+
+  handle () (OpenX fname m) k = do
+      res <- openFileX fname m
+      case res of
+        Left err => k (FError err) ()
+        Right fh => k Success      (FH fh)
+
+  handle (FH h) Close k = do
+      closeFile h
+      k () ()
+
+  -- Read
+  handle (FH h) FGetC k = do
+      res <- fgetc h
+      case res of
+        Left err => k (FError err) (FH h)
+        Right  c => k (Result c)   (FH h)
+
+  handle (FH h) FGetLine k = do
+      res <- fGetLine h
+      case res of
+        Left err => k (FError err) (FH h)
+        Right ln => k (Result ln)  (FH h)
+
+  handle () (FReadFile fname) k = do
+      res <- readFile fname
+      case res of
+        Left err  => k (FError err) ()
+        Right str => k (Result str) ()
+
+  -- Write
+  handle (FH fh) (FPutStr str) k = do
+      res <- fPutStr fh str
+      case res of
+        Left err => k (FError err) (FH fh)
+        Right () => k Success      (FH fh)
+
+  handle (FH fh) (FPutStrLn str) k = do
+      res <- fPutStr fh str
+      case res of
+        Left err => k (FError err) (FH fh)
+        Right () => k Success      (FH fh)
+
+  handle () (FWriteFile fname str) k = do
+      res <- writeFile fname str
+      case res of
+        Left err => k (FError err) ()
+        Right () => k Success      ()
+
+  -- Flush
+  handle (FH fh) FFlush k = do
+      fflush fh
+      k () (FH fh)
+
+  -- Query
+  handle (FH fh) FEOF k = do
+      res <- fEOF fh
+      k res (FH fh)
+
+-- ---------------------------------------------------------------- [ IOExcept ]
+
+Handler FileE (IOExcept a) where
+
+  -- Open Close
+  handle () (Open fname m) k = do
+      res <- ioe_lift $ openFile fname m
+      case res of
+        Left err => k (FError err) ()
+        Right fh => k Success      (FH fh)
+
+  handle () (OpenX fname m) k = do
+      res <- ioe_lift $ openFileX fname m
+      case res of
+        Left err => k (FError err) ()
+        Right fh => k Success      (FH fh)
+
+  handle (FH h) Close k = do
+      ioe_lift $ closeFile h
+      k () ()
+
+  -- Read
+  handle (FH h) FGetC k = do
+      res <- ioe_lift $ fgetc h
+      case res of
+        Left err => k (FError err) (FH h)
+        Right  c => k (Result c)   (FH h)
+
+  handle (FH h) FGetLine k = do
+      res <- ioe_lift $ fGetLine h
+      case res of
+        Left err => k (FError err) (FH h)
+        Right ln => k (Result ln)  (FH h)
+
+  handle () (FReadFile fname) k = do
+      res <- ioe_lift $ readFile fname
+      case res of
+        Left err  => k (FError err) ()
+        Right str => k (Result str) ()
+
+  -- Write
+  handle (FH fh) (FPutStr str) k = do
+      res <- ioe_lift $ fPutStr fh str
+      case res of
+        Left err => k (FError err) (FH fh)
+        Right () => k Success      (FH fh)
+
+  handle (FH fh) (FPutStrLn str) k = do
+      res <- ioe_lift $ fPutStr fh str
+      case res of
+        Left err => k (FError err) (FH fh)
+        Right () => k Success      (FH fh)
+
+  handle () (FWriteFile fname str) k = do
+      res <- ioe_lift $ writeFile fname str
+      case res of
+        Left err => k (FError err) ()
+        Right () => k Success      ()
+
+  -- Flush
+  handle (FH fh) FFlush k = do
+      ioe_lift $ fflush fh
+      k () (FH fh)
+
+
+  -- Query
+  handle (FH fh) FEOF k = do
+      res <- ioe_lift $ fEOF fh
+      k res (FH fh)
+
+-- ------------------------------------------------------ [ Effect and Helpers ]
+
+||| Effectful operations for interacting with files.
 |||
-|||       empty -> write [label="Open W"];
-|||       write -> empty [label="Close"];
-|||       write -> write [label="WriteLine"];
+||| The `FILE` effect is parameterised by a file handle once a handle has been acquired, and Unit (`()`) if the file handle is expected to be released once the function has returned.
 |||
-|||     }
-data FileIO : Effect where
-  ||| Open a file with the specified mode.
-  |||
-  ||| Opening a file successful moves the state from 'empty' to the
-  ||| specified mode. If not successful the state is still 'empty'.
-  |||
-  ||| @ fname The file name to be opened.
-  ||| @ m The file mode.
-  Open : (fname: String)
-         -> (m : Mode)
-         -> sig FileIO Bool () (\res => case res of
-                                             True => OpenFile m
-                                             False => ())
-
-  ||| Close a file.
-  |||
-  ||| Closing a file moves the state from Open to closed.
-  Close : sig FileIO () (OpenFile m) ()
+FILE : (ty : Type) -> EFFECT
+FILE t = MkEff t FileE
 
-  ||| Read a line from the file.
-  |||
-  ||| Only files that are open for reading can be read.
-  ReadLine : sig FileIO String (OpenFile Read)
+||| A file has been opened for reading.
+R : Type
+R = FileHandle Read
 
-  ||| Write a string to a file.
-  |||
-  ||| Only file that are open for writing can be written to.
-  WriteString : String -> sig FileIO () (OpenFile WriteTruncate)
+||| A file has been opened for writing.
+W : Type
+W = FileHandle WriteTruncate
 
-  ||| End of file?
-  |||
-  ||| Only files open for reading can be tested for EOF
-  EOF : sig FileIO Bool (OpenFile Read)
+||| A file can only be appeneded to.
+A : Type
+A = FileHandle Append
 
--- ------------------------------------------------------------ [ The Handlers ]
+||| A file can be read and written to.
+RW : Type
+RW = FileHandle ReadWrite
 
---- An implementation of the resource access protocol for the IO Context.
-implementation Handler FileIO IO where
-    handle () (Open fname m) k = do Right h <- openFile fname m
-                                        | Left err => k False ()
-                                    k True (FH h)
-    handle (FH h) Close      k = do closeFile h
-                                    k () ()
-    handle (FH h) ReadLine        k = do Right str <- fGetLine h
-                                         -- Need proper error handling!
-                                             | Left err => k "" (FH h)
-                                         k str (FH h)
-    handle (FH h) (WriteString str) k = do Right () <- fPutStr h str
-                                             | Left err => k () (FH h)
-                                           k () (FH h)
-    handle (FH h) EOF             k = do e <- fEOF h
-                                         k e (FH h)
+||| A file opened for reading and writing and has been truncated to
+||| zero if it previsiouly existed.
+RWPlus : Type
+RWPlus = FileHandle ReadWriteTruncate
 
-implementation Handler FileIO (IOExcept a) where
-    handle () (Open fname m) k = do Right h <- ioe_lift $ openFile fname m
-                                        | Left err => k False ()
-                                    k True (FH h)
-    handle (FH h) Close      k = do ioe_lift $ closeFile h
-                                    k () ()
-    handle (FH h) ReadLine        k = do Right str <- ioe_lift $ fGetLine h
-                                         -- Need proper error handling!
-                                             | Left err => k "" (FH h)
-                                         k str (FH h)
-    handle (FH h) (WriteString str) k = do Right () <- ioe_lift $ fPutStr h str
-                                             | Left err => k () (FH h)
-                                           k () (FH h)
-    handle (FH h) EOF             k = do e <- ioe_lift $ fEOF h
-                                         k e (FH h)
+||| A file will read from the beginning and write at the end.
+APlus : Type
+APlus = FileHandle ReadAppend
 
--- -------------------------------------------------------------- [ The Effect ]
-FILE_IO : Type -> EFFECT
-FILE_IO t = MkEff t FileIO
+-- --------------------------------------------------------------------- [ API ]
 
--- ------------------------------------------------------------ [ The Bindings ]
---
--- Bind the IO context handlers to functions. These functions will run
--- in the IO context.
---
+-- -------------------------------------------------------- [ Open/Close/Query ]
 
-||| Open a file with the specified mode.
+||| Open a file.
 |||
-||| @ fname The file name to be opened.
-||| @ m The file mode.
+||| @ fname the filename.
+||| @ m     the mode; either Read, WriteTruncate, Append, ReadWrite,
+|||         ReadWriteTruncate, or ReadAppend
+|||
 open : (fname : String)
-       -> (m : Mode)
-       -> Eff Bool [FILE_IO ()]
-                   (\res => [FILE_IO (case res of
-                                           True => OpenFile m
-                                           False => ())])
+    -> (m : Mode)
+    -> Eff (FileOpSuccess)
+           [FILE ()]
+           (\res => [FILE (calcResourceTy m res)])
 open f m = call $ Open f m
 
+||| Open a file using C11 extended modes.
+|||
+||| @ fname the filename
+||| @ m     the mode; either Read, WriteTruncate, Append, ReadWrite,
+|||         ReadWriteTruncate, or ReadAppend
+openX : (fname : String)
+     -> (m : Mode)
+     -> Eff (FileOpSuccess)
+            [FILE ()]
+            (\res => [FILE (calcResourceTy m res)])
+openX f m = call $ OpenX f m
 
 ||| Close a file.
-close : Eff () [FILE_IO (OpenFile m)] [FILE_IO ()]
-close = call $ Close
+close : Eff () [FILE (FileHandle m)] [FILE ()]
+close = call (Close)
 
-||| Read a line from the file.
-readLine : Eff String [FILE_IO (OpenFile Read)]
-readLine = call $ ReadLine
+||| Have we reached the end of the file.
+eof : {auto prf : ValidModeRead m}
+    -> Eff Bool [FILE (FileHandle m)]
+eof = call FEOF
 
-||| Write a string to a file.
-writeString : String -> Eff () [FILE_IO (OpenFile WriteTruncate)]
-writeString str = call $ WriteString str
+flush : Eff () [FILE (FileHandle m)]
+flush = call FFlush
 
-||| Write a line to a file.
-writeLine : String -> Eff () [FILE_IO (OpenFile WriteTruncate)]
-writeLine str = call $ WriteString (str ++ "\n")
+-- -------------------------------------------------------------------- [ Read ]
 
-||| End of file?
-eof : Eff Bool [FILE_IO (OpenFile Read)]
-eof = call $ EOF
+||| Read a `Char`.
+readChar : {auto prf : ValidModeRead m}
+      -> Eff (FileOpResult Char)
+             [FILE (FileHandle m)]
+readChar = call FGetC
 
-||| Read a complete file, returning a user defined error if
-||| unsuccesful.
-|||
-readFile : (errFunc : String -> e)
-        -> (fname   : String)
-        -> Eff (Either e String) [FILE_IO ()]
-readFile errFunc fname = do
-    case !(open fname Read) of
-      False => pure $ Left (errFunc fname)
-      True => do
-        src <- readAcc ""
-        close
-        pure $ Right src
-  where
-    readAcc : String -> Eff String [FILE_IO (OpenFile Read)]
-    readAcc acc = if (not !(eof))
-                     then readAcc (acc ++ !(readLine))
-                     else pure acc
+||| Read a complete line.
+readLine : {auto prf : ValidModeRead m}
+        -> Eff (FileOpResult String)
+               [FILE (FileHandle m)]
+readLine = call FGetLine
 
-||| Write a file containing the provided string, returning a user
-||| defined error if unsuccesful.
-|||
-writeFile : (errFunc : String -> e)
-         -> (fname   : String)
-         -> (content : String)
-         -> Eff (Either e ()) [FILE_IO ()]
-writeFile errFunc fname content = do
-    case !(open fname WriteTruncate) of
-      True => do
-        writeString content
-        close
-        pure $ Right ()
-      False => pure $ Left (errFunc fname)
+-- ------------------------------------------------------------------- [ Write ]
 
+||| Write a string to the file.
+writeString : (str : String)
+           -> {auto prf : ValidModeWrite m}
+           -> Eff (FileOpSuccess)
+                  [FILE (FileHandle m)]
+writeString str = call $ FPutStr str
 
-namespace Default
-  readFile : String -> Eff (Either String String) [FILE_IO ()]
-  readFile = File.readFile id
+||| Write a complete line to the file.
+writeLine : (str : String)
+         -> {auto prf : ValidModeWrite m}
+         -> Eff (FileOpSuccess)
+                [FILE (FileHandle m)]
+writeLine str = call $ FPutStrLn str
 
-  writeFile : String -> String -> Eff (Either String ()) [FILE_IO ()]
-  writeFile = File.writeFile id
+-- -------------------------------------------------------------- [ Whole File ]
+
+||| Read the contents of a file into a string.
+|||
+||| This checks the size of
+||| the file before beginning to read, and only reads that many bytes,
+||| to ensure that it remains a total function if the file is appended
+||| to while being read.
+|||
+||| Returns an error if fname is not a normal file.
+readFile : (fname : String)
+        -> Eff (FileOpResult String)
+               [FILE ()]
+readFile fn = call $ FReadFile fn
+
+||| Create a file and write contents to the file.
+writeFile : (fname    : String)
+         -> (contents : String)
+         -> Eff (FileOpSuccess)
+                [FILE ()]
+writeFile fn str = call $ FWriteFile fn str
+
 -- --------------------------------------------------------------------- [ EOF ]
diff --git a/libs/prelude/Builtins.idr b/libs/prelude/Builtins.idr
--- a/libs/prelude/Builtins.idr
+++ b/libs/prelude/Builtins.idr
@@ -12,7 +12,7 @@
 namespace Builtins
   ||| The non-dependent pair type, also known as conjunction.
   ||| @A the type of the left elements in the pair
-  ||| @B the type of the left elements in the pair
+  ||| @B the type of the right elements in the pair
   %elim data Pair : (A : Type) -> (B : Type) -> Type where
      ||| A pair of elements
      ||| @a the left element of the pair
@@ -26,7 +26,7 @@
   ||| The non-dependent pair type, also known as conjunction, usable with
   ||| UniqueTypes.
   ||| @A the type of the left elements in the pair
-  ||| @B the type of the left elements in the pair
+  ||| @B the type of the right elements in the pair
   data UPair : (A : AnyType) -> (B : AnyType) -> AnyType where
      ||| A pair of elements
      ||| @a the left element of the pair
@@ -73,7 +73,6 @@
 
 ||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
 data Symbol_ : String -> Type where
-
 
 infix 5 ~=~
 
diff --git a/libs/prelude/Prelude/Traversable.idr b/libs/prelude/Prelude/Traversable.idr
--- a/libs/prelude/Prelude/Traversable.idr
+++ b/libs/prelude/Prelude/Traversable.idr
@@ -9,20 +9,28 @@
 
 %access public export
 
+||| Map each element of a structure to a computation, evaluate those
+||| computations and discard the results.
 traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
 traverse_ f = foldr ((*>) . f) (pure ())
 
+||| Evaluate each computation in a structure and discard the results
 sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
 sequence_ = foldr (*>) (pure ())
 
+||| Like `traverse_` but with the arguments flipped
 for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
 for_ = flip traverse_
 
 interface (Functor t, Foldable t) => Traversable (t : Type -> Type) where
+  ||| Map each element of a structure to a computation, evaluate those
+  ||| computations and combine the results.
   traverse : Applicative f => (a -> f b) -> t a -> f (t b)
 
+||| Evaluate each computation in a structure and collect the results
 sequence : (Traversable t, Applicative f) => t (f a) -> f (t a)
 sequence = traverse id
 
+||| Like `traverse` but with the arguments flipped
 for : (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)
 for = flip traverse
diff --git a/rts/idris_rts.c b/rts/idris_rts.c
--- a/rts/idris_rts.c
+++ b/rts/idris_rts.c
@@ -792,6 +792,9 @@
     case CT_MANAGEDPTR:
         cl = MKMPTRc(vm, x->info.mptr->data, x->info.mptr->size);
         break;
+    case CT_CDATA:
+        cl = MKCDATAc(vm, x->info.c_heap_item);
+        break;
     case CT_BITS8:
         cl = idris_b8CopyForGC(vm, x);
         break;
diff --git a/src/IRTS/CodegenCommon.hs b/src/IRTS/CodegenCommon.hs
--- a/src/IRTS/CodegenCommon.hs
+++ b/src/IRTS/CodegenCommon.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DeriveGeneric #-}
 {-|
 Module      : IRTS.CodegenCommon
 Description : Common data structures required for all code generators.
@@ -7,12 +8,14 @@
 -}
 module IRTS.CodegenCommon where
 
+import GHC.Generics (Generic)
+
 import Idris.Core.TT
 import IRTS.Simplified
 import IRTS.Defunctionalise
 
 data DbgLevel = NONE | DEBUG | TRACE deriving Eq
-data OutputType = Raw | Object | Executable deriving (Eq, Show)
+data OutputType = Raw | Object | Executable deriving (Eq, Show, Generic)
 
 -- | Everything which might be needed in a code generator.
 --
diff --git a/src/IRTS/CodegenJavaScript.hs b/src/IRTS/CodegenJavaScript.hs
--- a/src/IRTS/CodegenJavaScript.hs
+++ b/src/IRTS/CodegenJavaScript.hs
@@ -17,6 +17,7 @@
 import Idris.AbsSyntax hiding (TypeCase)
 import IRTS.Bytecode
 import IRTS.Lang
+import IRTS.Exports
 import IRTS.Simplified
 import IRTS.Defunctionalise
 import IRTS.CodegenCommon
@@ -103,12 +104,12 @@
 codegenJavaScript :: CodeGenerator
 codegenJavaScript ci =
   codegenJS_all JavaScript (simpleDecls ci)
-    (includes ci) [] (outputFile ci) (outputType ci)
+    (includes ci) [] (outputFile ci) (exportDecls ci) (outputType ci)
 
 codegenNode :: CodeGenerator
 codegenNode ci =
   codegenJS_all Node (simpleDecls ci)
-    (includes ci) (compileLibs ci) (outputFile ci) (outputType ci)
+    (includes ci) (compileLibs ci) (outputFile ci) (exportDecls ci) (outputType ci)
 
 codegenJS_all
   :: JSTarget
@@ -116,14 +117,16 @@
   -> [FilePath]
   -> [String]
   -> FilePath
+  -> [ExportIFace]
   -> OutputType
   -> IO ()
-codegenJS_all target definitions includes libs filename outputType = do
+codegenJS_all target definitions includes libs filename exports outputType = do
   let bytecode = map toBC definitions
   let info = initCompileInfo bytecode
   let js = concatMap (translateDecl info) bytecode
   let full = concatMap processFunction js
-  let code = deadCodeElim full
+  let exportedNames = map translateName ((getExpNames exports) ++ [sUN "call__IO"])
+  let code = deadCodeElim exportedNames full
   let ext = takeExtension filename
   let isHtml = target == JavaScript && ext == ".html"
   let htmlPrologue = T.pack "<!doctype html><html><head><script>\n"
@@ -150,6 +153,7 @@
   let jsSource = T.pack runtime
                  `T.append` T.concat (map compileJS opt)
                  `T.append` T.concat (map compileJS cons)
+                 `T.append` T.concat (map compileJS (map genInterface (concatMap getExps exports)))
                  `T.append` main
                  `T.append` invokeMain
   let source = if isHtml
@@ -161,14 +165,17 @@
                                             , writable   = True
                                             })
     where
-      deadCodeElim :: [JS] -> [JS]
-      deadCodeElim js = concatMap collectFunctions js
+      deadCodeElim :: [String] -> [JS] -> [JS]
+      deadCodeElim exports js = concatMap (collectFunctions exports) js
         where
-          collectFunctions :: JS -> [JS]
-          collectFunctions fun@(JSAlloc name _)
+          collectFunctions :: [String] -> JS -> [JS]
+          collectFunctions _ fun@(JSAlloc name _)
             | name == translateName (sMN 0 "runMain") = [fun]
 
-          collectFunctions fun@(JSAlloc name (Just (JSFunction _ body))) =
+          collectFunctions exports fun@(JSAlloc name _)
+            | name `elem` exports = [fun]
+
+          collectFunctions _ fun@(JSAlloc name (Just (JSFunction _ body))) =
             let invokations = sum $ map (
                     \x -> execState (countInvokations name x) 0
                   ) js
@@ -273,6 +280,7 @@
 
       invokeMain :: T.Text
       invokeMain = compileJS $ JSApp (JSIdent "main") []
+      getExps (Export _ _ exp) = exp
 
 optimizeConstructors :: [JS] -> ([JS], [JS])
 optimizeConstructors js =
@@ -1236,6 +1244,33 @@
 
 jsPOP :: JS
 jsPOP = JSApp (JSProj jsCALLSTACK "pop") []
+
+genInterface :: Export -> JS
+genInterface (ExportData name) = JSNoop
+genInterface (ExportFun name (FStr jsName) ret args) = JSAlloc jsName
+        (Just (JSFunction [] (JSSeq  $
+            jsFUNPRELUDE ++
+            pushArgs nargs ++
+            [jsSTOREOLD d,
+             jsBASETOP d 0,
+             jsADDTOP d nargs,
+             jsCALL d name] ++
+            retval ret)))
+    where
+        nargs = length args
+        d = CompileInfo [] [] False
+        pushArg n = JSAssign (jsTOP n) (JSIndex (JSIdent "arguments") (JSNum (JSInt n)))
+        pushArgs 0 = []
+        pushArgs n = (pushArg (n-1)):pushArgs (n-1)
+        retval (FIO t) = [JSApp (JSIdent "i$RUN") [],
+                          JSAssign (jsTOP 0) JSNull,
+                          JSAssign (jsTOP 1) JSNull,
+                          JSAssign (jsTOP 2) (translateReg RVal),
+                          jsSTOREOLD d,
+                          jsBASETOP d 0,
+                          jsADDTOP d 3,
+                          jsCALL d (sUN "call__IO")] ++ retval t
+        retval t = [JSApp (JSIdent "i$RUN") [], JSReturn (translateReg RVal)]
 
 translateBC :: CompileInfo -> BC -> JS
 translateBC info bc
diff --git a/src/IRTS/Compiler.hs b/src/IRTS/Compiler.hs
--- a/src/IRTS/Compiler.hs
+++ b/src/IRTS/Compiler.hs
@@ -529,8 +529,8 @@
 -- Transform matching on Delay to applications of Force.
 irSC top vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])
     | delay == txt "Delay"
-    = do sc' <- irSC top vs $ mkForce n' n sc
-         return $ LLet n' (LForce (LV (Glob n))) sc'
+    = do sc' <- irSC top vs sc -- mkForce n' n sc
+         return $ lsubst n' (LForce (LV (Glob n))) sc'
 
 -- There are two transformations in this case:
 --
diff --git a/src/IRTS/Lang.hs b/src/IRTS/Lang.hs
--- a/src/IRTS/Lang.hs
+++ b/src/IRTS/Lang.hs
@@ -5,7 +5,7 @@
 License     : BSD3
 Maintainer  : The Idris Community.
 -}
-{-# LANGUAGE PatternGuards, DeriveFunctor #-}
+{-# LANGUAGE PatternGuards, DeriveFunctor, DeriveGeneric #-}
 
 module IRTS.Lang where
 
@@ -17,6 +17,7 @@
 
 import Data.List
 import Debug.Trace
+import GHC.Generics (Generic)
 
 data Endianness = Native | BE | LE deriving (Show, Eq)
 
@@ -93,7 +94,7 @@
                    -- core or another machine. 'id' is a valid implementation
             | LExternal Name
             | LNoOp
-  deriving (Show, Eq)
+  deriving (Show, Eq, Generic)
 
 -- Supported target languages for foreign calls
 
@@ -301,6 +302,30 @@
 usedIn env (LForeign _ _ args) = concatMap (usedIn env) (map snd args)
 usedIn env (LOp f args) = concatMap (usedIn env) args
 usedIn env _ = []
+
+lsubst :: Name -> LExp -> LExp -> LExp
+lsubst n new (LV (Glob x)) | n == x = new
+lsubst n new (LApp t e args) = let e' = lsubst n new e
+                                   args' = map (lsubst n new) args in
+                                   LApp t e' args'
+lsubst n new (LLazyApp fn args) = let args' = map (lsubst n new) args in
+                                      LLazyApp fn args'
+lsubst n new (LLazyExp e) = LLazyExp (lsubst n new e)
+lsubst n new (LForce e) = LForce (lsubst n new e)
+lsubst n new (LLet v val sc) = LLet v (lsubst n new val) (lsubst n new sc)
+lsubst n new (LLam ns sc) = LLam ns (lsubst n new sc)
+lsubst n new (LProj e i) = LProj (lsubst n new e) i
+lsubst n new (LCon lv t cn args) = let args' = map (lsubst n new) args in
+                                       LCon lv t cn args'
+lsubst n new (LOp op args) = let args' = map (lsubst n new) args in
+                                 LOp op args'
+lsubst n new (LForeign fd rd args) 
+     = let args' = map (\(d, a) -> (d, lsubst n new a)) args in
+           LForeign fd rd args'
+lsubst n new (LCase t e alts) = let e' = lsubst n new e
+                                    alts' = map (fmap (lsubst n new)) alts in
+                                    LCase t e' alts'
+lsubst n new tm = tm
 
 instance Show LExp where
    show e = show' [] "" e where
diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs
--- a/src/Idris/AbsSyntaxTree.hs
+++ b/src/Idris/AbsSyntaxTree.hs
@@ -6,7 +6,8 @@
 Maintainer  : The Idris Community.
 -}
 {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
-             DeriveDataTypeable, TypeSynonymInstances, PatternGuards #-}
+             DeriveDataTypeable, DeriveGeneric, TypeSynonymInstances,
+             PatternGuards #-}
 
 module Idris.AbsSyntaxTree where
 
@@ -47,6 +48,7 @@
 import Data.Traversable (Traversable)
 import Data.Typeable
 import Data.Foldable (Foldable)
+import GHC.Generics (Generic)
 
 import Debug.Trace
 
@@ -112,7 +114,7 @@
   , opt_evaltypes    :: Bool           -- ^ normalise types in `:t`
   , opt_desugarnats  :: Bool
   , opt_autoimpls    :: Bool
-  } deriving (Show, Eq)
+  } deriving (Show, Eq, Generic)
 
 defaultOpts = IOption { opt_logLevel   = 0
                       , opt_logcats    = []
@@ -150,7 +152,7 @@
   } deriving (Show)
 
 data Optimisation = PETransform -- ^ partial eval and associated transforms
-  deriving (Show, Eq)
+  deriving (Show, Eq, Generic)
 
 defaultOptimise = [PETransform]
 
@@ -185,7 +187,8 @@
 ppOptionIst :: IState -> PPOption
 ppOptionIst = ppOption . idris_options
 
-data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
+data LanguageExt = TypeProviders | ErrorReflection
+  deriving (Show, Eq, Read, Ord, Generic)
 
 -- | The output mode in use
 data OutputMode = RawOutput Handle       -- ^ Print user output directly to the handle
@@ -196,13 +199,13 @@
 data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
                   | ColsWide Int   -- ^ Manually specified - must be positive
                   | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
-   deriving (Show, Eq)
+   deriving (Show, Eq, Generic)
 
 -- | 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)
+  deriving (Show, Eq, Generic)
 
 -- | The global state used in the Idris monad
 data IState = IState {
@@ -305,13 +308,14 @@
   , idris_ttstats                :: M.Map Term (Int, Term)
   , idris_fragile                :: Ctxt String               -- ^ Fragile names and explanation.
   }
+  deriving Generic
 
 -- Required for parsers library, and therefore trifecta
 instance Show IState where
   show = const "{internal state}"
 
 data SizeChange = Smaller | Same | Bigger | Unknown
-    deriving (Show, Eq)
+    deriving (Show, Eq, Generic)
 {-!
 deriving instance Binary SizeChange
 deriving instance NFData SizeChange
@@ -324,7 +328,7 @@
     calls   :: [Name]
   , scg     :: [SCGEntry]
   , usedpos :: [(Int, [UsageReason])]
-  } deriving Show
+  } deriving (Show, Generic)
 {-!
 deriving instance Binary CGInfo
 deriving instance NFData CGInfo
@@ -384,7 +388,7 @@
               | IBCDeprecate Name String
               | IBCFragile Name String
               | IBCConstraint FC UConstraint
-  deriving Show
+  deriving (Show, Generic)
 
 -- | The initial state for the compiler
 idrisInit :: IState
@@ -420,12 +424,12 @@
 
 data Codegen = Via IRFormat String
              | Bytecode
-    deriving (Show, Eq)
+    deriving (Show, Eq, Generic)
 {-!
 deriving instance NFData Codegen
 !-}
 
-data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq)
+data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)
 
 data HowMuchDocs = FullDocs | OverviewDocs
 
@@ -511,7 +515,7 @@
             | IErasure
             | ICoverage
             | IIBC
-            deriving (Show, Eq, Ord)
+            deriving (Show, Eq, Ord, Generic)
 
 strLogCat :: LogCat -> String
 strLogCat IParse    = "parser"
@@ -606,7 +610,7 @@
          | DesugarNats
          | NoElimDeprecationWarnings      -- ^ Don't show deprecation warnings for %elim
          | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics
-    deriving (Show, Eq)
+    deriving (Show, Eq, Generic)
 
 data ElabShellCmd = EQED
                   | EAbandon
@@ -625,7 +629,7 @@
             | Infixr  { prec :: Int }
             | InfixN  { prec :: Int }
             | PrefixN { prec :: Int }
-    deriving Eq
+    deriving (Eq, Generic)
 {-!
 deriving instance Binary Fixity
 deriving instance NFData Fixity
@@ -638,7 +642,7 @@
     show (PrefixN i) = "prefix " ++ show i
 
 data FixDecl = Fix Fixity String
-    deriving Eq
+    deriving (Eq, Generic)
 
 instance Show FixDecl where
   show (Fix f s) = show f ++ " " ++ s
@@ -653,7 +657,7 @@
 
 
 data Static = Static | Dynamic
-  deriving (Show, Eq, Data, Typeable)
+  deriving (Show, Eq, Data, Generic, Typeable)
 {-!
 deriving instance Binary Static
 deriving instance NFData Static
@@ -677,7 +681,7 @@
                       , pstatic  :: Static
                       , pscript  :: PTerm
                       }
-             deriving (Show, Eq, Data, Typeable)
+             deriving (Show, Eq, Data, Generic, Typeable)
 
 {-!
 deriving instance Binary Plicity
@@ -721,7 +725,7 @@
            | Constructor -- ^ Data constructor type
            | AutoHint    -- ^ use in auto implicit search
            | PEGenerated -- ^ generated by partial evaluator
-    deriving (Show, Eq)
+    deriving (Show, Eq, Generic)
 {-!
 deriving instance Binary FnOpt
 deriving instance NFData FnOpt
@@ -739,7 +743,7 @@
 -- | Type provider - what to provide
 data ProvideWhat' t = ProvTerm t t     -- ^ the first is the goal type, the second is the term
                     | ProvPostulate t  -- ^ goal type must be Type, so only term
-    deriving (Show, Eq, Functor)
+    deriving (Show, Eq, Functor, Generic)
 
 type ProvideWhat = ProvideWhat' PTerm
 
@@ -824,7 +828,7 @@
    -- | FC is decl-level, for errors, and Strings represent the
    -- namespace
    | PRunElabDecl FC t [String]
- deriving Functor
+ deriving (Functor, Generic)
 {-!
 deriving instance Binary PDecl'
 deriving instance NFData PDecl'
@@ -851,6 +855,7 @@
                | DFragile Name String
                | DAutoImplicits Bool
                | DUsed FC Name Name
+  deriving Generic
 
 -- | A set of instructions for things that need to happen in IState
 -- after a term elaboration when there's been reflected elaboration.
@@ -895,7 +900,7 @@
                 | PWith    FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
                 | PClauseR FC        [t] t                    [PDecl' t]
                 | PWithR   FC        [t] t (Maybe (Name, FC)) [PDecl' t]
-    deriving Functor
+    deriving (Functor, Generic)
 {-!
 deriving instance Binary PClause'
 deriving instance NFData PClause'
@@ -913,7 +918,7 @@
   | PLaterdecl { d_name    :: Name
                , d_name_fc :: FC
                , d_tcon    :: t
-  } deriving Functor
+  } deriving (Functor, Generic)
 
 -- | Transform the FCs in a PData and its associated terms. The first
 -- function transforms the general-purpose FCs, and the second
@@ -1103,7 +1108,7 @@
 data PunInfo = IsType
              | IsTerm
              | TypeOrTerm
-             deriving (Eq, Show, Data, Typeable)
+             deriving (Eq, Show, Data, Typeable, Generic)
 
 -- | High level language terms
 data PTerm = PQuote Raw         -- ^ Inclusion of a core term into the
@@ -1170,12 +1175,12 @@
            | PConstSugar FC PTerm
              -- ^ A desugared constant. The FC is a precise source
              -- location that will be used to highlight it later.
-       deriving (Eq, Data, Typeable)
+       deriving (Eq, Data, Typeable, Generic)
 
 data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
               | FirstSuccess
               | TryImplicit
-       deriving (Eq, Data, Typeable)
+       deriving (Eq, Data, Generic, Typeable)
 
 -- | Transform the FCs in a PTerm. The first function transforms the
 -- general-purpose FCs, and the second transforms those that are used
@@ -1296,7 +1301,7 @@
                 | TFail [ErrorReportPart]
                 | Qed | Abandon
                 | SourceFC
-    deriving (Show, Eq, Functor, Foldable, Traversable, Data, Typeable)
+    deriving (Show, Eq, Functor, Foldable, Traversable, Data, Generic, Typeable)
 {-!
 deriving instance Binary PTactic'
 deriving instance NFData PTactic'
@@ -1343,7 +1348,7 @@
             | DoBindP FC t t [(t,t)]
             | DoLet  FC Name FC t t   -- ^ second FC is precise name location
             | DoLetP FC t t
-    deriving (Eq, Functor, Data, Typeable)
+    deriving (Eq, Functor, Data, Generic, Typeable)
 {-!
 deriving instance Binary PDo'
 deriving instance NFData PDo'
@@ -1384,13 +1389,13 @@
                             , getScript :: t
                             , getTm     :: t
                             }
-             deriving (Show, Eq, Functor, Data, Typeable)
+             deriving (Show, Eq, Functor, Data, Generic, Typeable)
 
 data ArgOpt = AlwaysShow
             | HideDisplay
             | InaccessibleArg
             | UnknownImp
-            deriving (Show, Eq, Data, Typeable)
+            deriving (Show, Eq, Data, Generic, Typeable)
 
 instance Sized a => Sized (PArg' a) where
   size (PImp p _ l nm trm)            = 1 + size nm + size trm
@@ -1480,7 +1485,7 @@
   , class_params               :: [Name]
   , class_instances            :: [(Name, Bool)] -- ^ the Bool is whether to include in instance search, so named instances are excluded
   , class_determiners          :: [Int]
-  } deriving Show
+  } deriving (Show, Generic)
 {-!
 deriving instance Binary ClassInfo
 deriving instance NFData ClassInfo
@@ -1491,17 +1496,17 @@
     record_parameters  :: [(Name,PTerm)]
   , record_constructor :: Name
   , record_projections :: [Name]
-  } deriving Show
+  } deriving (Show, Generic)
 
 -- Type inference data
 
 data TIData = TIPartial         -- ^ a function with a partially defined type
             | TISolution [Term] -- ^ possible solutions to a metavariable in a type
-    deriving Show
+    deriving (Show, Generic)
 
 -- | Miscellaneous information about functions
 data FnInfo = FnInfo { fn_params :: [Int] }
-    deriving Show
+    deriving (Show, Generic)
 {-!
 deriving instance Binary FnInfo
 deriving instance NFData FnInfo
@@ -1510,7 +1515,7 @@
 data OptInfo = Optimise {
     inaccessible :: [(Int,Name)]  -- includes names for error reporting
   , detaggable :: Bool
-  } deriving Show
+  } deriving (Show, Generic)
 {-!
 deriving instance Binary OptInfo
 deriving instance NFData OptInfo
@@ -1528,7 +1533,7 @@
   , dsl_lambda  :: Maybe t
   , dsl_let     :: Maybe t
   , dsl_pi      :: Maybe t
-  } deriving (Show, Functor)
+  } deriving (Show, Functor, Generic)
 {-!
 deriving instance Binary DSL'
 deriving instance NFData DSL'
@@ -1539,7 +1544,7 @@
 data SynContext = PatternSyntax
                 | TermSyntax
                 | AnySyntax
-    deriving Show
+    deriving (Show, Generic)
 {-!
 deriving instance Binary SynContext
 deriving instance NFData SynContext
@@ -1547,7 +1552,7 @@
 
 data Syntax = Rule [SSymbol] PTerm SynContext
             | DeclRule [SSymbol] [PDecl]
-    deriving Show
+    deriving (Show, Generic)
 
 syntaxNames :: Syntax -> [Name]
 syntaxNames (Rule syms _ _) = mapMaybe ename syms
@@ -1570,7 +1575,7 @@
              | Binding Name
              | Expr Name
              | SimpleExpr Name
-    deriving (Show, Eq)
+    deriving (Show, Eq, Generic)
 
 
 {-!
@@ -1579,6 +1584,7 @@
 !-}
 
 newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
+  deriving Generic
 
 emptySyntaxRules :: SyntaxRules
 emptySyntaxRules = SyntaxRules []
@@ -1632,7 +1638,7 @@
 
 data Using = UImplicit Name PTerm
            | UConstraint Name [Name]
-    deriving (Show, Eq, Data, Typeable)
+    deriving (Show, Eq, Data, Generic, Typeable)
 {-!
 deriving instance Binary Using
 deriving instance NFData Using
@@ -1656,7 +1662,7 @@
   , syn_in_quasiquote :: Int
   , syn_toplevel      :: Bool
   , withAppAllowed    :: Bool
-  } deriving Show
+  } deriving (Show, Generic)
 {-!
 deriving instance NFData SyntaxInfo
 deriving instance Binary SyntaxInfo
diff --git a/src/Idris/CaseSplit.hs b/src/Idris/CaseSplit.hs
--- a/src/Idris/CaseSplit.hs
+++ b/src/Idris/CaseSplit.hs
@@ -75,7 +75,7 @@
         logElab 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)
 --         iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))
 --         iputStrLn (show pats)
-        let t = mergeUserImpl (addImplPat ist t') (delab ist tm)
+        let t = mergeUserImpl (addImplPat ist t') (delabDirect ist tm)
         let ctxt = tt_ctxt ist
         case lookup n pats of
              Nothing -> ifail $ show n ++ " is not a pattern variable"
@@ -247,7 +247,7 @@
 elabNewPat :: PTerm -> Idris (Bool, PTerm)
 elabNewPat t = idrisCatch (do (tm, ty) <- elabVal (recinfo (fileFC "casesplit")) ELHS t
                               i <- getIState
-                              return (True, delab i tm))
+                              return (True, delabDirect i tm))
                           (\e -> do i <- getIState
                                     logElab 5 $ "Not a valid split:\n" ++ showTmImpls t ++ "\n"
                                                      ++ pshow i e
diff --git a/src/Idris/Colours.hs b/src/Idris/Colours.hs
--- a/src/Idris/Colours.hs
+++ b/src/Idris/Colours.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DeriveGeneric #-}
 {-|
 Module      : Idris.Colours
 Description : Support for colours within Idris.
@@ -14,6 +15,7 @@
   , colourisePrompt, colourise, ColourType(..), hStartColourise, hEndColourise
   ) where
 
+import GHC.Generics (Generic)
 import System.Console.ANSI
 import System.IO (Handle)
 
@@ -37,7 +39,7 @@
                                , promptColour    :: IdrisColour
                                , postulateColour :: IdrisColour
                                }
-                   deriving (Eq, Show)
+                   deriving (Eq, Show, Generic)
 
 -- | Idris's default console colour theme
 defaultTheme :: ColourTheme
diff --git a/src/Idris/Core/CaseTree.hs b/src/Idris/Core/CaseTree.hs
--- a/src/Idris/Core/CaseTree.hs
+++ b/src/Idris/Core/CaseTree.hs
@@ -18,7 +18,8 @@
 in order to allow for better optimisation opportunities.
 
 -}
-{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances #-}
+{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances,
+    DeriveGeneric #-}
 
 module Idris.Core.CaseTree (
     CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo
@@ -36,6 +37,7 @@
 import Data.List hiding (partition)
 import qualified Data.List(partition)
 import Debug.Trace
+import GHC.Generics (Generic)
 
 data CaseDef = CaseDef [Name] !SC [Term]
     deriving Show
@@ -45,14 +47,14 @@
            | STerm !t
            | UnmatchedCase String -- ^ error message
            | ImpossibleCase -- ^ already checked to be impossible
-    deriving (Eq, Ord, Functor)
+    deriving (Eq, Ord, Functor, Generic)
 {-!
 deriving instance Binary SC'
 deriving instance NFData SC'
 !-}
 
 data CaseType = Updatable | Shared
-   deriving (Eq, Ord, Show)
+   deriving (Eq, Ord, Show, Generic)
 
 type SC = SC' Term
 
@@ -61,7 +63,7 @@
                 | ConstCase Const         !(SC' t)
                 | SucCase Name            !(SC' t)
                 | DefaultCase             !(SC' t)
-    deriving (Show, Eq, Ord, Functor)
+    deriving (Show, Eq, Ord, Functor, Generic)
 {-!
 deriving instance Binary CaseAlt'
 deriving instance NFData CaseAlt'
@@ -249,7 +251,8 @@
 -- Work Right to Left
 
 simpleCase :: Bool -> SC -> Bool ->
-              Phase -> FC -> [Int] -> [Type] ->
+              Phase -> FC -> [Int] -> 
+              [(Type, Bool)] -> -- (Argument type, whether it's canonical)
               [([Name], Term, Term)] ->
               ErasureInfo ->
               TC CaseDef
@@ -271,7 +274,7 @@
                 OK pats ->
                     let numargs    = length (fst (head pats))
                         ns         = take numargs args
-                        (ns', ps') = order [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats
+                        (ns', ps') = order phase [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats (map snd argtys)
                         (tree, st) = runCaseBuilder erInfo
                                          (match ns' ps' defcase)
                                          ([], numargs, [])
@@ -429,28 +432,38 @@
 --
 -- The first argument means [(Name, IsInaccessible)].
 
-order :: [(Name, Bool)] -> [Clause] -> ([Name], [Clause])
-order []  cs = ([], cs)
-order ns' [] = (map fst ns', [])
-order ns' cs = let patnames = transpose (map (zip ns') (map fst cs))
-                   -- only sort the arguments where there is no clash in
-                   -- constructor tags between families, and no constructor/constant
-                   -- clash, because otherwise we can't reliable make the
-                   -- case distinction on evaluation
-                   (patnames_ord, patnames_rest)
-                        = Data.List.partition (noClash . map snd) patnames
-                   -- note: sortBy . reverse is not nonsense because sortBy is stable
-                   pats' = transpose (sortBy moreDistinct (reverse patnames_ord)
-                                         ++ patnames_rest) in
-                   (getNOrder pats', zipWith rebuild pats' cs)
+order :: Phase -> [(Name, Bool)] -> [Clause] -> [Bool] -> ([Name], [Clause])
+-- do nothing at compile time: FIXME (EB): Put this in after checking 
+-- implications for Franck's reflection work... see issue 3233
+-- order CompileTime ns cs _ = (map fst ns, cs) 
+order _ []  cs cans = ([], cs)
+order _ ns' [] cans = (map fst ns', [])
+order phase ns' cs cans 
+    = let patnames = transpose (map (zip ns') (map (zip cans) (map fst cs)))
+          -- only sort the arguments where there is no clash in
+          -- constructor tags between families, the argument type is canonical,
+          -- and no constructor/constant
+          -- clash, because otherwise we can't reliable make the
+          -- case distinction on evaluation
+          (patnames_ord, patnames_rest)
+                = Data.List.partition (noClash . map snd) patnames 
+          patnames_ord' = case phase of
+                               CompileTime -> patnames_ord
+                               -- reversing tends to make better case trees
+                               -- and helps erasure
+                               RunTime -> reverse patnames_ord
+          pats' = transpose (sortBy moreDistinct patnames_ord'
+                                       ++ patnames_rest) in
+          (getNOrder pats', zipWith rebuild pats' cs)
   where
     getNOrder [] = error $ "Failed order on " ++ show (map fst ns', cs)
     getNOrder (c : _) = map (fst . fst) c
 
-    rebuild patnames clause = (map snd patnames, snd clause)
+    rebuild patnames clause = (map (snd . snd) patnames, snd clause)
 
     noClash [] = True
-    noClash (p : ps) = not (any (clashPat p) ps) && noClash ps
+    noClash ((can, p) : ps) = can && not (any (clashPat p) (map snd ps)) 
+                                  && noClash ps
 
     clashPat (PCon _ _ _ _) (PConst _) = True
     clashPat (PConst _) (PCon _ _ _ _) = True
@@ -460,12 +473,13 @@
     clashPat _ _ = False
 
     -- this compares (+isInaccessible, -numberOfCases)
-    moreDistinct xs ys = compare (snd . fst . head $ xs, numNames [] (map snd ys))
-                                 (snd . fst . head $ ys, numNames [] (map snd xs))
+    moreDistinct xs ys 
+        = compare (snd . fst . head $ xs, numNames [] (map snd ys))
+                  (snd . fst . head $ ys, numNames [] (map snd xs))
 
-    numNames xs (PCon _ n _ _ : ps)
+    numNames xs ((_, PCon _ n _ _) : ps)
         | not (Left n `elem` xs) = numNames (Left n : xs) ps
-    numNames xs (PConst c : ps)
+    numNames xs ((_, PConst c) : ps)
         | not (Right c `elem` xs) = numNames (Right c : xs) ps
     numNames xs (_ : ps) = numNames xs ps
     numNames xs [] = length xs
diff --git a/src/Idris/Core/DeepSeq.hs b/src/Idris/Core/DeepSeq.hs
--- a/src/Idris/Core/DeepSeq.hs
+++ b/src/Idris/Core/DeepSeq.hs
@@ -1,6 +1,6 @@
 {-|
 Module      : Idris.Core.DeepSeq
-Description : Marshalling information for TT.
+Description : NFData instances for TT.
 Copyright   :
 License     : BSD3
 Maintainer  : The Idris Community.
@@ -16,287 +16,46 @@
 
 import Control.DeepSeq
 
-instance NFData Name where
-        rnf (UN x1) = rnf x1 `seq` ()
-        rnf (NS x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (MN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (SN x1) = rnf x1 `seq` ()
-        rnf (SymRef x1) = rnf x1 `seq` ()
+instance NFData Name
 
-instance NFData Context where
-  rnf ctxt = rnf (next_tvar ctxt) `seq` rnf (definitions ctxt) `seq` ()
+instance NFData Context
 
 -- | Forcing the contents of a context, for diagnosing and working
 -- around space leaks
 forceDefCtxt :: Context -> Context
 forceDefCtxt (force -> !ctxt) = ctxt
 
-instance NFData NameOutput where
-    rnf TypeOutput = ()
-    rnf FunOutput = ()
-    rnf DataOutput = ()
-    rnf MetavarOutput = ()
-    rnf PostulateOutput = ()
-
-instance NFData TextFormatting where
-  rnf BoldText = ()
-  rnf ItalicText = ()
-  rnf UnderlineText = ()
-
-instance NFData Ordering where
-  rnf LT = ()
-  rnf EQ = ()
-  rnf GT = ()
-
-instance NFData OutputAnnotation where
-  rnf (AnnName x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-  rnf (AnnBoundName x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-  rnf (AnnConst x1) = rnf x1 `seq` ()
-  rnf (AnnData x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-  rnf (AnnType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-  rnf (AnnKeyword) = ()
-  rnf (AnnFC x) = rnf x `seq` ()
-  rnf (AnnTextFmt x) = rnf x `seq` ()
-  rnf (AnnLink x) = rnf x `seq` ()
-  rnf (AnnTerm x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-  rnf (AnnSearchResult  x1) = rnf x1 `seq` ()
-  rnf (AnnErr x1) = rnf x1 `seq` ()
-  rnf (AnnNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-  rnf (AnnQuasiquote) = ()
-  rnf (AnnAntiquote) = ()
-
-instance NFData SpecialName where
-        rnf (WhereN x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (WithN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (InstanceN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (ParentN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (MethodN x1) = rnf x1 `seq` ()
-        rnf (CaseN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (ElimN x1) = rnf x1 `seq` ()
-        rnf (InstanceCtorN x1) = rnf x1 `seq` ()
-        rnf (MetaN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-
-instance NFData Universe where
-        rnf NullType = ()
-        rnf UniqueType = ()
-        rnf AllTypes = ()
-
-instance NFData Raw where
-        rnf (Var x1) = rnf x1 `seq` ()
-        rnf (RBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (RApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf RType = ()
-        rnf (RUType x1) = rnf x1 `seq` ()
-        rnf (RConstant x1) = x1 `seq` ()
-
-instance NFData FC where
-        rnf (FC x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf NoFC = ()
-        rnf (FileFC f) = rnf f `seq` ()
-
-instance NFData FC' where
-        rnf (FC' fc) = rnf fc `seq` ()
-
-instance NFData Provenance where
-        rnf ExpectedType = ()
-        rnf InferredVal = ()
-        rnf GivenVal = ()
-        rnf (SourceTerm x1) = rnf x1 `seq` ()
-        rnf (TooManyArgs x1) = rnf x1 `seq` ()
-
-instance NFData UConstraint where
-  rnf (ULT x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-  rnf (ULE x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-
-instance NFData ConstraintFC where
-  rnf (ConstraintFC x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-
-instance NFData Err where
-        rnf (Msg x1) = rnf x1 `seq` ()
-        rnf (InternalMsg x1) = rnf x1 `seq` ()
-        rnf (CantUnify x1 x2 x3 x4 x5 x6)
-          = rnf x1 `seq`
-              rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
-        rnf (InfiniteUnify x1 x2 x3)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (CantConvert x1 x2 x3)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (UnifyScope x1 x2 x3 x4)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-        rnf (ElaboratingArg x1 x2 x3 x4)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-        rnf (CantInferType x1) = rnf x1 `seq` ()
-        rnf (CantMatch x1) = rnf x1 `seq` ()
-        rnf (ReflectionError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (ReflectionFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (CantSolveGoal x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (UniqueError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (UniqueKindError x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (NotEquality x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (NonFunctionType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (CantIntroduce x1) = rnf x1 `seq` ()
-        rnf (TooManyArguments x1) = rnf x1 `seq` ()
-        rnf (WithFnType x1) = rnf x1 `seq` ()
-        rnf (NoSuchVariable x1) = rnf x1 `seq` ()
-        rnf (NoTypeDecl x1) = rnf x1 `seq` ()
-        rnf (NotInjective x1 x2 x3)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (CantResolve x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (InvalidTCArg x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (CantResolveAlts x1) = rnf x1 `seq` ()
-        rnf (NoValidAlts x1) = rnf x1 `seq` ()
-        rnf (IncompleteTerm x1) = rnf x1 `seq` ()
-        rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (UniverseError x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
-        rnf ProgramLineComment = ()
-        rnf (Inaccessible x1) = rnf x1 `seq` ()
-        rnf (UnknownImplicit x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (NonCollapsiblePostulate x1) = rnf x1 `seq` ()
-        rnf (AlreadyDefined x1) = rnf x1 `seq` ()
-        rnf (ProofSearchFail x1) = rnf x1 `seq` ()
-        rnf (NoRewriting x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (At x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (Elaborating x1 x2 x3 x4)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-        rnf (ProviderError x1) = rnf x1 `seq` ()
-        rnf (LoadingFailed x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (ElabScriptDebug x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (ElabScriptStuck x1) = rnf x1 `seq` ()
-        rnf (RunningElabScript x1) = rnf x1 `seq` ()
-        rnf (ElabScriptStaging x1) = rnf x1 `seq` ()
-        rnf (FancyMsg x1) = rnf x1 `seq` ()
-
-instance NFData ErrorReportPart where
-  rnf (TextPart x1) = rnf x1 `seq` ()
-  rnf (TermPart x1) = rnf x1 `seq` ()
-  rnf (RawPart x1) = rnf x1 `seq` ()
-  rnf (NamePart x1) = rnf x1 `seq` ()
-  rnf (SubReport x1) = rnf x1 `seq` ()
-
-instance NFData ImplicitInfo where
-        rnf (Impl x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-
-instance (NFData b) => NFData (Binder b) where
-        rnf (Lam x1) = rnf x1 `seq` ()
-        rnf (Pi x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (Let x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (NLet x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (Hole x1) = rnf x1 `seq` ()
-        rnf (GHole x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (Guess x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (PVar x1) = rnf x1 `seq` ()
-        rnf (PVTy x1) = rnf x1 `seq` ()
-
-instance NFData UExp where
-        rnf (UVar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (UVal x1) = rnf x1 `seq` ()
-
-instance NFData NameType where
-        rnf Bound = ()
-        rnf Ref = ()
-        rnf (DCon x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (TCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-
-instance NFData NativeTy where
-        rnf IT8 = ()
-        rnf IT16 = ()
-        rnf IT32 = ()
-        rnf IT64 = ()
-
-instance NFData IntTy where
-        rnf (ITFixed x1) = rnf x1 `seq` ()
-        rnf ITNative = ()
-        rnf ITBig = ()
-        rnf ITChar = ()
-
-instance NFData ArithTy where
-        rnf (ATInt x1) = rnf x1 `seq` ()
-        rnf ATFloat = ()
-
-instance NFData Const where
-        rnf (I x1) = rnf x1 `seq` ()
-        rnf (BI x1) = rnf x1 `seq` ()
-        rnf (Fl x1) = rnf x1 `seq` ()
-        rnf (Ch x1) = rnf x1 `seq` ()
-        rnf (Str x1) = rnf x1 `seq` ()
-        rnf (B8 x1) = rnf x1 `seq` ()
-        rnf (B16 x1) = rnf x1 `seq` ()
-        rnf (B32 x1) = rnf x1 `seq` ()
-        rnf (B64 x1) = rnf x1 `seq` ()
-        rnf (AType x1) = rnf x1 `seq` ()
-        rnf WorldType = ()
-        rnf TheWorld = ()
-        rnf StrType = ()
-        rnf VoidType = ()
-        rnf Forgot = ()
-
-instance (NFData n) => NFData (TT n) where
-        rnf (P x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (V x1) = rnf x1 `seq` ()
-        rnf (Bind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (App x1 x2 x3) = rnf x2 `seq` rnf x3 `seq` ()
-        rnf (Constant x1) = rnf x1 `seq` ()
-        rnf (Proj x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf Erased = ()
-        rnf Impossible = ()
-        rnf (TType x1) = rnf x1 `seq` ()
-        rnf (UType _) = ()
-
-instance NFData Accessibility where
-        rnf Public = ()
-        rnf Frozen = ()
-        rnf Hidden = ()
-        rnf Private = ()
-
-
-instance NFData Totality where
-        rnf (Total x1) = rnf x1 `seq` ()
-        rnf Productive = ()
-        rnf (Partial x1) = rnf x1 `seq` ()
-        rnf Unchecked = ()
-        rnf Generated = ()
-
-instance NFData PReason where
-        rnf (Other x1) = rnf x1 `seq` ()
-        rnf Itself = ()
-        rnf NotCovering = ()
-        rnf NotPositive = ()
-        rnf (UseUndef x1) = rnf x1 `seq` ()
-        rnf ExternalIO = ()
-        rnf BelieveMe = ()
-        rnf (Mutual x1) = rnf x1 `seq` ()
-        rnf NotProductive = ()
-
-instance NFData MetaInformation where
-        rnf EmptyMI = ()
-        rnf (DataMI x1) = rnf x1 `seq` ()
-
-instance NFData Def where
-        rnf (Function x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (TyDecl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (Operator x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (CaseOp x1 x2 x3 x4 x5 x6)
-          = rnf x1 `seq`
-              rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
-
-instance NFData CaseInfo where
-        rnf (CaseInfo x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-
-instance NFData CaseDefs where
-        rnf (CaseDefs x1 x2 x3 x4)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-
-instance (NFData t) => NFData (SC' t) where
-        rnf (Case _ x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (ProjCase x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (STerm x1) = rnf x1 `seq` ()
-        rnf (UnmatchedCase x1) = rnf x1 `seq` ()
-        rnf ImpossibleCase = ()
-
-instance (NFData t) => NFData (CaseAlt' t) where
-        rnf (ConCase x1 x2 x3 x4)
-          = x1 `seq` x2 `seq` x3 `seq` rnf x4 `seq` ()
-        rnf (FnCase x1 x2 x3) = x1 `seq` x2 `seq` rnf x3 `seq` ()
-        rnf (ConstCase x1 x2) = x1 `seq` rnf x2 `seq` ()
-        rnf (SucCase x1 x2) = x1 `seq` rnf x2 `seq` ()
-        rnf (DefaultCase x1) = rnf x1 `seq` ()
+instance NFData NameOutput
+instance NFData TextFormatting
+instance NFData Ordering
+instance NFData OutputAnnotation
+instance NFData SpecialName
+instance NFData Universe
+instance NFData Raw
+instance NFData FC
+instance NFData FC'
+instance NFData Provenance
+instance NFData UConstraint
+instance NFData ConstraintFC
+instance NFData Err
+instance NFData ErrorReportPart
+instance NFData ImplicitInfo
+instance (NFData b) => NFData (Binder b)
+instance NFData UExp
+instance NFData NameType
+instance NFData NativeTy
+instance NFData IntTy
+instance NFData ArithTy
+instance NFData Const
+instance (NFData a) => NFData (AppStatus a)
+instance (NFData n) => NFData (TT n)
+instance NFData Accessibility
+instance NFData Totality
+instance NFData PReason
+instance NFData MetaInformation
+instance NFData Def
+instance NFData CaseInfo
+instance NFData CaseDefs
+instance NFData CaseType
+instance (NFData t) => NFData (SC' t)
+instance (NFData t) => NFData (CaseAlt' t)
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,7 +6,7 @@
 Maintainer  : The Idris Community.
 -}
 {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, BangPatterns,
-             PatternGuards #-}
+             PatternGuards, DeriveGeneric #-}
 {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
 
 module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
@@ -21,7 +21,8 @@
                 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
                 mapDefCtxt,
                 lookupTotal, lookupTotalExact, lookupInjectiveExact,
-                lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
+                lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, 
+                isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,
                 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
                 isUniverse) where
 
@@ -31,6 +32,7 @@
 import qualified Data.Binary as B
 import Data.Binary hiding (get, put)
 import Data.Maybe (listToMaybe)
+import GHC.Generics (Generic)
 
 import Idris.Core.TT
 import Idris.Core.CaseTree
@@ -696,10 +698,11 @@
          | Operator Type Int ([Value] -> Maybe Value)
          | CaseOp CaseInfo
                   !Type
-                  ![Type] -- argument types
+                  ![(Type, Bool)] -- argument types, whether canonical
                   ![Either Term (Term, Term)] -- original definition
                   ![([Name], Term, Term)] -- simplified for totality check definition
                   !CaseDefs
+  deriving Generic
 --                   [Name] SC -- Compile time case definition
 --                   [Name] SC -- Run time cae definitions
 
@@ -709,12 +712,14 @@
                   cases_inlined :: !([Name], SC),
                   cases_runtime :: !([Name], SC)
                 }
+  deriving Generic
 
 data CaseInfo = CaseInfo {
                   case_inlinable :: Bool, -- decided by machine
                   case_alwaysinline :: Bool, -- decided by %inline flag
                   tc_dictionary :: Bool
                 }
+  deriving Generic
 
 {-!
 deriving instance Binary Def
@@ -761,7 +766,7 @@
 -- Private => Programs can't access the name, doesn't reduce internally
 
 data Accessibility = Hidden | Public | Frozen | Private
-    deriving (Eq, Ord)
+    deriving (Eq, Ord, Generic)
 {-!
 deriving instance NFData Accessibility
 !-}
@@ -780,7 +785,7 @@
               | Partial PReason
               | Unchecked
               | Generated
-    deriving Eq
+    deriving (Eq, Generic)
 {-!
 deriving instance NFData Totality
 !-}
@@ -788,7 +793,7 @@
 -- | Reasons why a function may not be total
 data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name
              | ExternalIO | BelieveMe | Mutual [Name] | NotProductive
-    deriving (Show, Eq)
+    deriving (Show, Eq, Generic)
 {-!
 deriving instance NFData PReason
 !-}
@@ -825,14 +830,14 @@
 data MetaInformation =
       EmptyMI -- ^ No meta-information
     | DataMI [Int] -- ^ Meta information for a data declaration with position of parameters
-  deriving (Eq, Show)
+  deriving (Eq, Show, Generic)
 
 -- | Contexts used for global definitions and for proof state. They contain
 -- universe constraints and existing definitions.
 data Context = MkContext {
                   next_tvar       :: Int,
                   definitions     :: Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation)
-                } deriving Show
+                } deriving (Show, Generic)
 
 
 -- | The initial empty context
@@ -911,7 +916,7 @@
 addCasedef :: Name -> ErasureInfo -> CaseInfo ->
               Bool -> SC -> -- default case
               Bool -> Bool ->
-              [Type] -> -- argument types
+              [(Type, Bool)] -> -- argument types, whether canonical
               [Int] ->  -- inaccessible arguments
               [Either Term (Term, Term)] ->
               [([Name], Term, Term)] -> -- totality
@@ -1014,6 +1019,15 @@
 -- | Get the single type that matches some name precisely
 lookupTyExact :: Name -> Context -> Maybe Type
 lookupTyExact n ctxt = fmap snd (lookupTyNameExact n ctxt)
+
+-- | Return true if the given type is a concrete type familyor primitive
+-- False it it's a function to compute a type or a variable
+isCanonical :: Type -> Context -> Bool
+isCanonical t ctxt
+     = case unApply t of
+            (P _ n _, _) -> isConName n ctxt
+            (Constant _, _) -> True
+            _ -> False
 
 isConName :: Name -> Context -> Bool
 isConName n ctxt = isTConName n ctxt || isDConName n ctxt
diff --git a/src/Idris/Core/ProofState.hs b/src/Idris/Core/ProofState.hs
--- a/src/Idris/Core/ProofState.hs
+++ b/src/Idris/Core/ProofState.hs
@@ -1058,7 +1058,7 @@
                                          (getProofTerm (pterm ps)) }, "")
 processTactic UnifyProblems ps
     = do let (ns', probs') = updateProblems ps [] (map setReady (problems ps))
-             pterm' = updateSolved ns' (pterm ps)
+             pterm' = orderUpdateSolved ns' (pterm ps)
          traceWhen (unifylog ps) ("(UnifyProblems) Dropping holes: " ++ show (map fst ns')) $
           return (ps { pterm = pterm', solved = Nothing, problems = probs',
                        previous = Just ps, plog = "",
@@ -1067,6 +1067,8 @@
                        dotted = filter (notIn ns') (dotted ps),
                        holes = holes ps \\ (map fst ns') }, plog ps)
    where notIn ns (h, _) = h `notElem` map fst ns
+         orderUpdateSolved [] t = t
+         orderUpdateSolved (n : ns) t = orderUpdateSolved ns (updateSolved [n] t)
 processTactic (MatchProblems all) ps
     = do let (ns', probs') = matchProblems all ps [] (map setReady (problems ps))
              (ns'', probs'') = matchProblems all ps ns' probs'
diff --git a/src/Idris/Core/TT.hs b/src/Idris/Core/TT.hs
--- a/src/Idris/Core/TT.hs
+++ b/src/Idris/Core/TT.hs
@@ -23,7 +23,7 @@
      programs with implicit syntax into fully explicit terms.
 -}
 {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor,
-             DeriveDataTypeable, PatternGuards #-}
+             DeriveDataTypeable, DeriveGeneric, PatternGuards #-}
 {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
 module Idris.Core.TT(
     AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..)
@@ -80,6 +80,7 @@
 import qualified Data.Binary as B
 import Data.Binary hiding (get, put)
 import Foreign.Storable (sizeOf)
+import GHC.Generics (Generic)
 
 import Numeric.IEEE (IEEE (identicalIEEE))
 
@@ -96,7 +97,7 @@
              }
         | NoFC -- ^ Locations for machine-generated terms
         | FileFC { _fc_fname :: String } -- ^ Locations with file only
-  deriving (Data, Typeable, Ord)
+  deriving (Data, Generic, Typeable, Ord)
 
 -- TODO: find uses and destroy them, doing this case analysis at call sites
 -- | Give a notion of filename associated with an FC
@@ -159,7 +160,7 @@
   _ == _ = True
 
 -- | FC with equality
-newtype FC' = FC' { unwrapFC :: FC } deriving (Data, Typeable, Ord)
+newtype FC' = FC' { unwrapFC :: FC } deriving (Data, Generic, Typeable, Ord)
 
 instance Eq FC' where
   FC' fc == FC' fc' = fcEq fc fc'
@@ -198,10 +199,10 @@
     show (FileFC f) = f
 
 -- | Output annotation for pretty-printed name - decides colour
-data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving (Show, Eq)
+data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving (Show, Eq, Generic)
 
 -- | Text formatting output
-data TextFormatting = BoldText | ItalicText | UnderlineText deriving (Show, Eq)
+data TextFormatting = BoldText | ItalicText | UnderlineText deriving (Show, Eq, Generic)
 
 -- | Output annotations for pretty-printing
 data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)
@@ -227,7 +228,7 @@
                         -- from that file.
                       | AnnQuasiquote
                       | AnnAntiquote
-  deriving (Show, Eq)
+  deriving (Show, Eq, Generic)
 
 -- | Used for error reflection
 data ErrorReportPart = TextPart String
@@ -235,7 +236,7 @@
                      | TermPart Term
                      | RawPart Raw
                      | SubReport [ErrorReportPart]
-                       deriving (Show, Eq, Data, Typeable)
+                       deriving (Show, Eq, Data, Generic, Typeable)
 
 
 data Provenance = ExpectedType
@@ -243,7 +244,7 @@
                 | InferredVal
                 | GivenVal
                 | SourceTerm Term
-  deriving (Show, Eq, Data, Typeable)
+  deriving (Show, Eq, Data, Generic, Typeable)
 {-!
 deriving instance NFData Err
 deriving instance Binary Err
@@ -309,7 +310,7 @@
           | RunningElabScript (Err' t) -- ^ The error occurred during a top-level elaboration script
           | ElabScriptStaging Name
           | FancyMsg [ErrorReportPart]
-  deriving (Eq, Functor, Data, Typeable)
+  deriving (Eq, Functor, Data, Generic, Typeable)
 
 type Err = Err' Term
 
@@ -467,7 +468,7 @@
           | MN !Int !T.Text -- ^ Machine chosen names
           | SN !SpecialName -- ^ Decorated function names
           | SymRef Int -- ^ Reference to IBC file symbol table (used during serialisation)
-  deriving (Eq, Ord, Data, Typeable)
+  deriving (Eq, Ord, Data, Generic, Typeable)
 
 txt :: String -> T.Text
 txt = T.pack
@@ -510,7 +511,7 @@
                  | ElimN !Name
                  | InstanceCtorN !Name
                  | MetaN !Name !Name
-  deriving (Eq, Ord, Data, Typeable)
+  deriving (Eq, Ord, Data, Generic, Typeable)
 {-!
 deriving instance Binary SpecialName
 deriving instance NFData SpecialName
@@ -675,7 +676,7 @@
 addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)
 
 data NativeTy = IT8 | IT16 | IT32 | IT64
-    deriving (Show, Eq, Ord, Enum, Data, Typeable)
+    deriving (Show, Eq, Ord, Enum, Data, Generic, Typeable)
 
 instance Pretty NativeTy OutputAnnotation where
     pretty IT8  = text "Bits8"
@@ -684,7 +685,7 @@
     pretty IT64 = text "Bits64"
 
 data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar
-    deriving (Show, Eq, Ord, Data, Typeable)
+    deriving (Show, Eq, Ord, Data, Generic, Typeable)
 
 intTyName :: IntTy -> String
 intTyName ITNative = "Int"
@@ -693,7 +694,7 @@
 intTyName (ITChar) = "Char"
 
 data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors https://github.com/idris-lang/Idris-dev/issues/1723
-    deriving (Show, Eq, Ord, Data, Typeable)
+    deriving (Show, Eq, Ord, Data, Generic, Typeable)
 {-!
 deriving instance NFData IntTy
 deriving instance NFData NativeTy
@@ -725,7 +726,7 @@
            | AType ArithTy | StrType
            | WorldType | TheWorld
            | VoidType | Forgot
-  deriving (Ord, Data, Typeable)
+  deriving (Ord, Data, Generic, Typeable)
 
 -- We need to compare Double using bit-pattern identity rather than
 -- Haskell's Eq, which equates 0.0 and -0.0, leading to a
@@ -821,7 +822,7 @@
 constDocs prim                             = "Undocumented"
 
 data Universe = NullType | UniqueType | AllTypes
-  deriving (Eq, Ord, Data, Typeable)
+  deriving (Eq, Ord, Data, Generic, Typeable)
 
 instance Show Universe where
     show UniqueType = "UniqueType"
@@ -834,7 +835,7 @@
          | RType
          | RUType Universe
          | RConstant Const
-  deriving (Show, Eq, Data, Typeable)
+  deriving (Show, Eq, Data, Generic, Typeable)
 
 instance Sized Raw where
   size (Var name) = 1
@@ -854,7 +855,7 @@
 
 data ImplicitInfo = Impl { tcinstance :: Bool, toplevel_imp :: Bool,
                            machine_gen :: Bool }
-  deriving (Show, Eq, Ord, Data, Typeable)
+  deriving (Show, Eq, Ord, Data, Generic, Typeable)
 
 {-!
 deriving instance Binary ImplicitInfo
@@ -906,7 +907,7 @@
                 -- that make up pattern-match clauses)
               | PVTy  { binderTy  :: !b }
                 -- ^ The type of a pattern binding
-  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Typeable)
+  deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)
 {-!
 deriving instance Binary Binder
 deriving instance NFData Binder
@@ -951,7 +952,7 @@
 -- | Universe expressions for universe checking
 data UExp = UVar String Int -- ^ universe variable, with source file to disambiguate
           | UVal Int -- ^ explicit universe level
-  deriving (Eq, Ord, Data, Typeable)
+  deriving (Eq, Ord, Data, Generic, Typeable)
 {-!
 deriving instance NFData UExp
 !-}
@@ -969,11 +970,11 @@
 -- | Universe constraints
 data UConstraint = ULT UExp UExp -- ^ Strictly less than
                  | ULE UExp UExp -- ^ Less than or equal to
-  deriving (Eq, Ord, Data, Typeable)
+  deriving (Eq, Ord, Data, Generic, Typeable)
 
 data ConstraintFC = ConstraintFC { uconstraint :: UConstraint,
                                    ufc :: FC }
-  deriving (Show, Data, Typeable)
+  deriving (Show, Data, Generic, Typeable)
 
 instance Eq ConstraintFC where
     x == y = uconstraint x == uconstraint y
@@ -991,7 +992,7 @@
               | Ref
               | DCon {nt_tag :: Int, nt_arity :: Int, nt_unique :: Bool} -- ^ Data constructor
               | TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor
-  deriving (Show, Ord, Data, Typeable)
+  deriving (Show, Ord, Data, Generic, Typeable)
 {-!
 deriving instance Binary NameType
 deriving instance NFData NameType
@@ -1013,7 +1014,7 @@
 data AppStatus n = Complete
                  | MaybeHoles
                  | Holes [n]
-    deriving (Eq, Ord, Functor, Data, Typeable, Show)
+    deriving (Eq, Ord, Functor, Data, Generic, Typeable, Show)
 
 -- | Terms in the core language. The type parameter is the type of
 -- identifiers used for bindings and explicit named references;
@@ -1031,7 +1032,7 @@
           | Impossible -- ^ special case for totality checking
           | TType UExp -- ^ the type of types at some level
           | UType Universe -- ^ Uniqueness type universe (disjoint from TType)
-  deriving (Ord, Functor, Data, Typeable)
+  deriving (Ord, Functor, Data, Generic, Typeable)
 {-!
 deriving instance Binary TT
 deriving instance NFData TT
@@ -1096,7 +1097,7 @@
              | DefaultEliminator -- ^ Set if an eliminator should be generated for data type
              | DefaultCaseFun -- ^ Set if a case function should be generated for data type
              | DataErrRev
-    deriving (Show, Eq)
+    deriving (Show, Eq, Generic)
 
 type DataOpts = [DataOpt]
 
@@ -1105,7 +1106,7 @@
                      data_opts :: DataOpts,
                      param_pos :: [Int],
                      mutual_types :: [Name] }
-    deriving Show
+    deriving (Show, Generic)
 {-!
 deriving instance Binary TypeInfo
 deriving instance NFData TypeInfo
diff --git a/src/Idris/Coverage.hs b/src/Idris/Coverage.hs
--- a/src/Idris/Coverage.hs
+++ b/src/Idris/Coverage.hs
@@ -557,8 +557,9 @@
                             findCalls [] Toplevel (dePat rhs') (patvars lhs')
                                       (zip pargs [0..])
 
-  findCalls cases Delayed ap@(P _ n _) pvs args
-     | n == topfn = []
+  -- Under a delay, calls are excluded from the graph - if it's a call to a
+  -- non-total function we'll find that in the final totality check
+  findCalls cases Delayed ap@(P _ n _) pvs args = []
   findCalls cases guarded ap@(App _ f a) pvs pargs
      -- under a call to "assert_total", don't do any checking, just believe
      -- that it is total.
diff --git a/src/Idris/DeepSeq.hs b/src/Idris/DeepSeq.hs
--- a/src/Idris/DeepSeq.hs
+++ b/src/Idris/DeepSeq.hs
@@ -1,6 +1,6 @@
 {-|
 Module      : Idris.DeepSeq
-Description : Specify how to marshall Idris' IR.
+Description : NFData instances for Idris' types
 Copyright   :
 License     : BSD3
 Maintainer  : The Idris Community.
@@ -26,323 +26,10 @@
 import qualified Cheapskate.Types as CT
 import qualified Idris.Docstrings as D
 
-instance NFData a => NFData (D.Docstring a) where
-  rnf (D.DocString opts contents) = rnf opts `seq` rnf contents `seq` ()
-
+-- These types don't have Generic instances
 instance NFData CT.Options where
   rnf (CT.Options x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
 
-instance NFData ConsoleWidth where
-  rnf InfinitelyWide = ()
-  rnf (ColsWide x) = rnf x `seq` ()
-  rnf AutomaticWidth = ()
-
-instance NFData PrimFn where
-    rnf (LPlus x) = rnf x `seq` ()
-    rnf (LMinus x) = rnf x `seq` ()
-    rnf (LTimes x) = rnf x `seq` ()
-    rnf (LUDiv x) = rnf x `seq` ()
-    rnf (LSDiv x) = rnf x `seq` ()
-    rnf (LURem x) = rnf x `seq` ()
-    rnf (LSRem x) = rnf x `seq` ()
-    rnf (LAnd x) = rnf x `seq` ()
-    rnf (LOr x) = rnf x `seq` ()
-    rnf (LXOr x) = rnf x `seq` ()
-    rnf (LCompl x) = rnf x `seq` ()
-    rnf (LSHL x) = rnf x `seq` ()
-    rnf (LLSHR x) = rnf x `seq` ()
-    rnf (LASHR x) = rnf x `seq` ()
-    rnf (LEq x) = rnf x `seq` ()
-    rnf (LLt x) = rnf x `seq` ()
-    rnf (LLe x) = rnf x `seq` ()
-    rnf (LGt x) = rnf x `seq` ()
-    rnf (LGe x) = rnf x `seq` ()
-    rnf (LSLt x) = rnf x `seq` ()
-    rnf (LSLe x) = rnf x `seq` ()
-    rnf (LSGt x) = rnf x `seq` ()
-    rnf (LSGe x) = rnf x `seq` ()
-    rnf (LSExt x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-    rnf (LZExt x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-    rnf (LTrunc x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-    rnf (LStrConcat) = ()
-    rnf (LStrLt) = ()
-    rnf (LStrEq) = ()
-    rnf (LStrLen) = ()
-    rnf (LIntFloat x) = rnf x `seq` ()
-    rnf (LFloatInt x) = rnf x `seq` ()
-    rnf (LIntStr x) = rnf x `seq` ()
-    rnf (LStrInt x) = rnf x `seq` ()
-    rnf (LFloatStr) = ()
-    rnf (LStrFloat) = ()
-    rnf (LChInt x) = rnf x `seq` ()
-    rnf (LIntCh x) = rnf x `seq` ()
-    rnf (LBitCast x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-    rnf (LFExp) = ()
-    rnf (LFLog) = ()
-    rnf (LFSin) = ()
-    rnf (LFCos) = ()
-    rnf (LFTan) = ()
-    rnf (LFASin) = ()
-    rnf (LFACos) = ()
-    rnf (LFATan) = ()
-    rnf (LFSqrt) = ()
-    rnf (LFFloor) = ()
-    rnf (LFCeil) = ()
-    rnf (LFNegate) = ()
-    rnf (LStrHead) = ()
-    rnf (LStrTail) = ()
-    rnf (LStrCons) = ()
-    rnf (LStrIndex) = ()
-    rnf (LStrRev) = ()
-    rnf (LStrSubstr) = ()
-    rnf (LReadStr) = ()
-    rnf (LWriteStr) = ()
-    rnf (LSystemInfo) = ()
-    rnf (LFork) = ()
-    rnf (LPar) = ()
-    rnf (LExternal x) = rnf x `seq` ()
-    rnf (LNoOp) = ()
-
-instance NFData SyntaxRules where
-    rnf (SyntaxRules xs) = rnf xs `seq` ()
-
-instance NFData DynamicLib where
-    rnf (Lib x _) = rnf x `seq` ()
-
-
-instance NFData Opt where
-    rnf (Filename str) = rnf  str `seq` ()
-    rnf (Quiet) = ()
-    rnf (NoBanner) = ()
-    rnf (ColourREPL bool) = rnf  bool `seq` ()
-    rnf (Idemode) = ()
-    rnf (IdemodeSocket) = ()
-    rnf (ShowLoggingCats) = ()
-    rnf (ShowLibs) = ()
-    rnf (ShowLibdir) = ()
-    rnf (ShowIncs) = ()
-    rnf (ShowPkgs) = ()
-    rnf (NoBasePkgs) = ()
-    rnf (NoPrelude) = ()
-    rnf (NoBuiltins) = ()
-    rnf (NoREPL) = ()
-    rnf (OLogging i) = rnf  i `seq` ()
-    rnf (OLogCats cs) = rnf  cs `seq` ()
-    rnf (Output str) = rnf  str `seq` ()
-    rnf (Interface) = ()
-    rnf (TypeCase) = ()
-    rnf (TypeInType) = ()
-    rnf (DefaultTotal) = ()
-    rnf (DefaultPartial) = ()
-    rnf (WarnPartial) = ()
-    rnf (WarnReach) = ()
-    rnf (EvalTypes) = ()
-    rnf (DesugarNats) = ()
-    rnf (NoCoverage) = ()
-    rnf (ErrContext) = ()
-    rnf (ShowImpl) = ()
-    rnf (Verbose) = ()
-    rnf (Port str) = rnf  str `seq` ()
-    rnf (IBCSubDir str) = rnf  str `seq` ()
-    rnf (ImportDir str) = rnf  str `seq` ()
-    rnf (PkgBuild str) = rnf  str `seq` ()
-    rnf (PkgInstall str) = rnf  str `seq` ()
-    rnf (PkgClean str) = rnf  str `seq` ()
-    rnf (PkgCheck str) = rnf  str `seq` ()
-    rnf (PkgREPL str) = rnf  str `seq` ()
-    rnf (PkgMkDoc str) = rnf  str `seq` ()
-    rnf (PkgTest str) = rnf  str `seq` ()
-    rnf (PkgIndex fp) = rnf  fp `seq` ()
-    rnf (WarnOnly) = ()
-    rnf (Pkg str) = rnf  str `seq` ()
-    rnf (BCAsm str) = rnf  str `seq` ()
-    rnf (DumpDefun str) = rnf  str `seq` ()
-    rnf (DumpCases str) = rnf  str `seq` ()
-    rnf (UseCodegen cg) = rnf  cg `seq` ()
-    rnf (CodegenArgs str) = rnf  str `seq` ()
-    rnf (OutputTy ot) = rnf  ot `seq` ()
-    rnf (Extension le) = rnf  le `seq` ()
-    rnf (InterpretScript str) = rnf  str `seq` ()
-    rnf (EvalExpr str) = rnf  str `seq` ()
-    rnf (TargetTriple str) = rnf  str `seq` ()
-    rnf (TargetCPU str) = rnf  str `seq` ()
-    rnf (OptLevel i) = rnf  i `seq` ()
-    rnf (AddOpt o) = rnf  o `seq` ()
-    rnf (RemoveOpt o) = rnf  o `seq` ()
-    rnf (Client str) = rnf  str `seq` ()
-    rnf (ShowOrigErr) = ()
-    rnf (AutoWidth) = ()
-    rnf (AutoSolve) = ()
-    rnf (UseConsoleWidth cw) = rnf  cw `seq` ()
-    rnf DumpHighlights = ()
-    rnf NoElimDeprecationWarnings = ()
-    rnf NoOldTacticDeprecationWarnings = ()
-
-
-instance NFData TIData where
-    rnf TIPartial = ()
-    rnf (TISolution xs) = rnf xs `seq` ()
-
-instance NFData IOption where
-    rnf (IOption
-         opt_logLevel
-         opt_logcats
-         opt_typecase
-         opt_typeintype
-         opt_coverage
-         opt_showimp
-         opt_errContext
-         opt_repl
-         opt_verbose
-         opt_nobanner
-         opt_quiet
-         opt_codegen
-         opt_outputTy
-         opt_ibcsubdir
-         opt_importdirs
-         opt_triple
-         opt_cpu
-         opt_cmdline
-         opt_origerr
-         opt_autoSolve
-         opt_autoImport
-         opt_optimise
-         opt_printdepth
-         opt_evaltypes
-         opt_desugarnats
-         opt_autoimpls) =
-         rnf opt_logLevel
-         `seq` rnf opt_typecase
-         `seq` rnf opt_typeintype
-         `seq` rnf opt_coverage
-         `seq` rnf opt_showimp
-         `seq` rnf opt_errContext
-         `seq` rnf opt_repl
-         `seq` rnf opt_verbose
-         `seq` rnf opt_nobanner
-         `seq` rnf opt_quiet
-         `seq` rnf opt_codegen
-         `seq` rnf opt_outputTy
-         `seq` rnf opt_ibcsubdir
-         `seq` rnf opt_importdirs
-         `seq` rnf opt_triple
-         `seq` rnf opt_cpu
-         `seq` rnf opt_cmdline
-         `seq` rnf opt_origerr
-         `seq` rnf opt_autoSolve
-         `seq` rnf opt_autoImport
-         `seq` rnf opt_optimise
-         `seq` rnf opt_printdepth
-         `seq` rnf opt_evaltypes
-         `seq` rnf opt_desugarnats
-         `seq` rnf opt_autoimpls
-         `seq` ()
-
-instance NFData LanguageExt where
-    rnf TypeProviders = ()
-    rnf ErrorReflection = ()
-
-instance NFData Optimisation where
-    rnf PETransform = ()
-
-instance NFData ColourTheme where
-    rnf (ColourTheme keywordColour
-                     boundVarColour
-                     implicitColour
-                     functionColour
-                     typeColour
-                     dataColour
-                     promptColour
-                     postulateColour) =
-        rnf keywordColour
-        `seq` rnf boundVarColour
-        `seq` rnf implicitColour
-        `seq` rnf functionColour
-        `seq` rnf typeColour
-        `seq` rnf dataColour
-        `seq` rnf promptColour
-        `seq` rnf postulateColour
-        `seq` ()
-
-instance NFData IdrisColour where
-  rnf (IdrisColour _ x2 x3 x4 x5) = rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
-
-instance NFData OutputType where
-    rnf Raw        = ()
-    rnf Object     = ()
-    rnf Executable = ()
-
-instance NFData IBCWrite where
-    rnf (IBCFix fixDecl) = rnf fixDecl `seq` ()
-    rnf (IBCImp name) = rnf name `seq` ()
-    rnf (IBCStatic name) = rnf name `seq` ()
-    rnf (IBCClass name) = rnf name `seq` ()
-    rnf (IBCInstance b1 b2 n1 n2) = rnf b1 `seq` rnf b2 `seq` rnf n1 `seq` rnf n2 `seq` ()
-    rnf (IBCDSL name) = rnf name `seq` ()
-    rnf (IBCData name) = rnf name `seq` ()
-    rnf (IBCOpt name) = rnf name `seq` ()
-    rnf (IBCMetavar name) = rnf name `seq` ()
-    rnf (IBCSyntax syntax) = rnf syntax `seq` ()
-    rnf (IBCKeyword string) = rnf string `seq` ()
-    rnf (IBCImport imp) = rnf imp `seq` ()
-    rnf (IBCImportDir filePath) = rnf filePath `seq` ()
-    rnf (IBCObj codegen filePath) = rnf codegen `seq` rnf filePath `seq` ()
-    rnf (IBCLib codegen string) = rnf codegen `seq` rnf string `seq` ()
-    rnf (IBCCGFlag codegen string) = rnf codegen `seq` rnf string `seq` ()
-    rnf (IBCDyLib string) = rnf string `seq` ()
-    rnf (IBCHeader codegen string) = rnf codegen `seq` rnf string `seq` ()
-    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` ()
-    rnf (IBCErrRev terms) = rnf terms `seq` ()
-    rnf (IBCCG name) = rnf name `seq` ()
-    rnf (IBCDoc name) = rnf name `seq` ()
-    rnf (IBCCoercion name) = rnf name `seq` ()
-    rnf (IBCDef name) = rnf name `seq` ()
-    rnf (IBCNameHint names) = rnf names `seq` ()
-    rnf (IBCLineApp filePath int pTerm) = rnf filePath `seq` rnf int `seq` rnf pTerm `seq` ()
-    rnf (IBCErrorHandler name) = rnf name `seq` ()
-    rnf (IBCFunctionErrorHandler n1 n2 n3) = rnf n1 `seq` rnf n2 `seq` rnf n3 `seq` ()
-    rnf (IBCPostulate name) = rnf name `seq` ()
-    rnf (IBCExtern extern) = rnf extern `seq` ()
-    rnf (IBCTotCheckErr fc string) = rnf fc `seq` rnf string `seq` ()
-    rnf (IBCParsedRegion fc) = rnf fc `seq` ()
-    rnf (IBCModDocs name) = rnf name `seq` ()
-    rnf (IBCUsage usage) = rnf usage `seq` ()
-    rnf (IBCExport name) = rnf name `seq` ()
-    rnf (IBCAutoHint n1 n2) = rnf n1 `seq` rnf n2 `seq` ()
-    rnf (IBCDeprecate n1 n2) = rnf n1 `seq` rnf n2 `seq` ()
-    rnf (IBCRecord x) = rnf x `seq` ()
-    rnf (IBCFragile n1 n2) = rnf n1 `seq` rnf n2 `seq` ()
-    rnf (IBCConstraint n1 n2) = rnf n1 `seq` rnf n2 `seq` ()
-
-
-instance NFData a => NFData (D.Block a) where
-  rnf (D.Para lines) = rnf lines `seq` ()
-  rnf (D.Header i lines) = rnf i `seq` rnf lines `seq` ()
-  rnf (D.Blockquote bs) = rnf bs `seq` ()
-  rnf (D.List b t xs) = rnf b `seq` rnf t `seq` rnf xs `seq` ()
-  rnf (D.CodeBlock attr txt tm) = rnf attr `seq` rnf txt `seq` ()
-  rnf (D.HtmlBlock txt) = rnf txt `seq` ()
-  rnf D.HRule = ()
-
-instance NFData a => NFData (D.Inline a) where
-  rnf (D.Str txt) = rnf txt `seq` ()
-  rnf D.Space = ()
-  rnf D.SoftBreak = ()
-  rnf D.LineBreak = ()
-  rnf (D.Emph xs) = rnf xs `seq` ()
-  rnf (D.Strong xs) = rnf xs `seq` ()
-  rnf (D.Code xs tm) = rnf xs `seq` rnf tm `seq` ()
-  rnf (D.Link a b xs) = rnf a `seq` rnf b `seq` rnf xs `seq` ()
-  rnf (D.Image a b c) = rnf a `seq` rnf b `seq` rnf c `seq` ()
-  rnf (D.Entity a) = rnf a `seq` ()
-  rnf (D.RawHtml x) = rnf x `seq` ()
-
 instance NFData CT.ListType where
   rnf (CT.Bullet c) = rnf c `seq` ()
   rnf (CT.Numbered nw i) = rnf nw `seq` rnf i `seq` ()
@@ -354,373 +41,65 @@
   rnf CT.PeriodFollowing = ()
   rnf CT.ParenFollowing = ()
 
-instance NFData DocTerm where
-        rnf Unchecked = ()
-        rnf (Checked x1) = rnf x1 `seq` ()
-        rnf (Example x1) = rnf x1 `seq` ()
-        rnf (Failing x1) = rnf x1 `seq` ()
-
--- All generated by 'derive'
-
-instance NFData SizeChange where
-        rnf Smaller = ()
-        rnf Same = ()
-        rnf Bigger = ()
-        rnf Unknown = ()
-
-instance NFData FnInfo where
-        rnf (FnInfo x1) = rnf x1 `seq` ()
-
-instance NFData Codegen where
-        rnf (Via x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf Bytecode = ()
-
-instance NFData IRFormat where
-        rnf _ = ()
-
-instance NFData LogCat where
-       rnf _ = ()
-
-instance NFData CGInfo where
-        rnf (CGInfo x1 x2 x3)
-          = rnf x1 `seq`
-              rnf x2 `seq` rnf x3 `seq` ()
-
-instance NFData Fixity where
-        rnf (Infixl x1) = rnf x1 `seq` ()
-        rnf (Infixr x1) = rnf x1 `seq` ()
-        rnf (InfixN x1) = rnf x1 `seq` ()
-        rnf (PrefixN x1) = rnf x1 `seq` ()
-
-instance NFData FixDecl where
-        rnf (Fix x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-
-instance NFData Static where
-        rnf Static = ()
-        rnf Dynamic = ()
-
-instance NFData ArgOpt where
-        rnf _ = ()
-
-instance NFData Plicity where
-        rnf (Imp x1 x2 x3 x4 x5)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
-        rnf (Exp x1 x2 x3)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (Constraint x1 x2)
-          = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (TacImp x1 x2 x3)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-
-instance NFData FnOpt where
-        rnf Inlinable = ()
-        rnf TotalFn = ()
-        rnf PartialFn = ()
-        rnf CoveringFn = ()
-        rnf Coinductive = ()
-        rnf AssertTotal = ()
-        rnf Dictionary = ()
-        rnf Implicit = ()
-        rnf NoImplicit = ()
-        rnf (CExport x1) = rnf x1 `seq` ()
-        rnf ErrorHandler = ()
-        rnf ErrorReverse = ()
-        rnf Reflection = ()
-        rnf (Specialise x1) = rnf x1 `seq` ()
-        rnf Constructor = ()
-        rnf AutoHint = ()
-        rnf PEGenerated = ()
-
-instance NFData DataOpt where
-        rnf Codata = ()
-        rnf DefaultEliminator = ()
-        rnf DefaultCaseFun = ()
-        rnf DataErrRev = ()
-
-instance (NFData t) => NFData (PDecl' t) where
-        rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (PTy x1 x2 x3 x4 x5 x6 x7 x8)
-          = 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 (PPostulate x1 x2 x3 x4 x5 x6 x7 x8)
-          = 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 (PClauses x1 x2 x3 x4)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-        rnf (PCAF x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (PData x1 x2 x3 x4 x5 x6)
-          = rnf x1 `seq`
-              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`
-              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 (PClass x1 x2 x3 x4 x5 x6 x8 x7 x9 x10 x11 x12)
-          = 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 (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`
-                  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 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` ()
-        rnf (PDirective x1) = ()
-        rnf (PProvider x1 x2 x3 x4 x5 x6)
-          = rnf x1 `seq`
-              rnf x2 `seq`
-                rnf x3 `seq`
-                  rnf x4 `seq`
-                    rnf x5 `seq` rnf x6 `seq` ()
-        rnf (PTransform x1 x2 x3 x4)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-        rnf (PRunElabDecl x1 x2 x3)
-          = rnf x1 `seq` rnf x2 `seq` x3 `seq` ()
-
-instance NFData t => NFData (ProvideWhat' t)  where
-        rnf (ProvTerm ty tm)   = rnf ty `seq` rnf tm `seq` ()
-        rnf (ProvPostulate tm) = rnf tm `seq` ()
-
-instance NFData PunInfo where
-        rnf x = x `seq` ()
-
-instance (NFData t) => NFData (PClause' t) where
-        rnf (PClause x1 x2 x3 x4 x5 x6)
-          = rnf x1 `seq`
-              rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
-        rnf (PWith x1 x2 x3 x4 x5 x6 x7)
-          = rnf x1 `seq`
-              rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()
-        rnf (PClauseR x1 x2 x3 x4)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-        rnf (PWithR x1 x2 x3 x4 x5)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
-
-instance (NFData t) => NFData (PData' t) where
-        rnf (PDatadecl x1 x2 x3 x4)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-        rnf (PLaterdecl x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-
-instance NFData PTerm where
-        rnf (PQuote x1) = rnf x1 `seq` ()
-        rnf (PRef x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` x3 `seq` ()
-        rnf (PInferRef x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` x3 `seq` ()
-        rnf (PPatvar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (PLam _ x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-        rnf (PPi x1 x2 x3 x4 x5)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
-        rnf (PLet _ x1 x2 x3 x4 x5)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
-        rnf (PTyped x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (PAppImpl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (PApp x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (PWithApp x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (PAppBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (PMatchApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (PCase x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (PIfThenElse x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-        rnf (PTrue x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (PResolveTC x1) = rnf x1 `seq` ()
-        rnf (PRewrite x1 x2 x3 x4 x5)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
-        rnf (PPair x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` x5 `seq` ()
-        rnf (PDPair x1 x2 x3 x4 x5 x6)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` x6 `seq` ()
-        rnf (PAs x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (PAlternative x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (PHidden x1) = rnf x1 `seq` ()
-        rnf (PType fc) = rnf fc `seq` ()
-        rnf (PUniverse _) = ()
-        rnf (PGoal x1 x2 x3 x4)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-        rnf (PConstant x1 x2) = x1 `seq` x2 `seq` ()
-        rnf Placeholder = ()
-        rnf (PDoBlock x1) = rnf x1 `seq` ()
-        rnf (PIdiom x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (PReturn x1) = rnf x1 `seq` ()
-        rnf (PMetavar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (PProof x1) = rnf x1 `seq` ()
-        rnf (PTactics x1) = rnf x1 `seq` ()
-        rnf (PElabError x1) = rnf x1 `seq` ()
-        rnf PImpossible = ()
-        rnf (PCoerced x1) = rnf x1 `seq` ()
-        rnf (PDisamb x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (PUnifyLog x1) = rnf x1 `seq` ()
-        rnf (PNoImplicits x1) = rnf x1 `seq` ()
-        rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (PUnquote x1) = rnf x1 `seq` ()
-        rnf (PQuoteName x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (PRunElab x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (PConstSugar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-
-instance NFData PAltType where
-        rnf (ExactlyOne x1) = rnf x1 `seq` ()
-        rnf FirstSuccess = ()
-        rnf TryImplicit = ()
-
-instance (NFData t) => NFData (PTactic' t) where
-        rnf (Intro x1) = rnf x1 `seq` ()
-        rnf Intros = ()
-        rnf (Focus x1) = rnf x1 `seq` ()
-        rnf (Refine x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (Rewrite x1) = rnf x1 `seq` ()
-        rnf DoUnify = ()
-        rnf (Induction x1) = rnf x1 `seq` ()
-        rnf (CaseTac x1) = rnf x1 `seq` ()
-        rnf (Equiv x1) = rnf x1 `seq` ()
-        rnf (Claim x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (MatchRefine x1) = rnf x1 `seq` ()
-        rnf (LetTac x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (LetTacTy x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (Exact x1) = rnf x1 `seq` ()
-        rnf Compute = ()
-        rnf Trivial = ()
-        rnf TCInstance = ()
-        rnf (ProofSearch r r1 r2 x1 x2 x3)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf Solve = ()
-        rnf Attack = ()
-        rnf ProofState = ()
-        rnf ProofTerm = ()
-        rnf Undo = ()
-        rnf (Try x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (TSeq x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (ApplyTactic x1) = rnf x1 `seq` ()
-        rnf (ByReflection x1) = rnf x1 `seq` ()
-        rnf (Reflect x1) = rnf x1 `seq` ()
-        rnf (Fill x1) = rnf x1 `seq` ()
-        rnf (GoalType x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf Qed = ()
-        rnf Abandon = ()
-        rnf (TCheck x1) = rnf x1 `seq` ()
-        rnf (TEval x1) = rnf x1 `seq` ()
-        rnf (TDocStr x1) = x1 `seq` ()
-        rnf (TSearch x1) = rnf x1 `seq` ()
-        rnf Skip = ()
-        rnf (TFail x1) = rnf x1 `seq` ()
-        rnf SourceFC = ()
-        rnf Unfocus = ()
-
-instance (NFData t) => NFData (PDo' t) where
-        rnf (DoExp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (DoBind x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-        rnf (DoBindP x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-        rnf (DoLet x1 x2 x3 x4 x5)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
-        rnf (DoLetP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-
-instance (NFData t) => NFData (PArg' t) where
-        rnf (PImp x1 x2 x3 x4 x5)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
-        rnf (PExp x1 x2 x3 x4)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-        rnf (PConstraint x1 x2 x3 x4)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-        rnf (PTacImplicit x1 x2 x3 x4 x5)
-          = rnf x1 `seq`
-              rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
-
-instance NFData ClassInfo where
-        rnf (CI x1 x2 x3 x4 x5 x6 x7)
-          = rnf x1 `seq`
-              rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()
-
-instance NFData RecordInfo where
-        rnf (RI x1 x2 x3)
-          = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-
-instance NFData OptInfo where
-        rnf (Optimise x1 x2)
-          = rnf x1 `seq` rnf x2 `seq` ()
-
-instance NFData TypeInfo where
-        rnf (TI x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
-
-instance (NFData t) => NFData (DSL' t) where
-        rnf (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)
-          = 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` ()
-
-instance NFData SynContext where
-        rnf PatternSyntax = ()
-        rnf TermSyntax = ()
-        rnf AnySyntax = ()
-
-instance NFData Syntax where
-        rnf (Rule x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (DeclRule x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-
-instance NFData SSymbol where
-        rnf (Keyword x1) = rnf x1 `seq` ()
-        rnf (Symbol x1) = rnf x1 `seq` ()
-        rnf (Binding x1) = rnf x1 `seq` ()
-        rnf (Expr x1) = rnf x1 `seq` ()
-        rnf (SimpleExpr x1) = rnf x1 `seq` ()
-
-instance NFData Using where
-        rnf (UImplicit x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
-        rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
+instance NFData DynamicLib where
+    rnf (Lib x _) = rnf x `seq` ()
 
-instance NFData SyntaxInfo where
-        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 x15 `seq` ()
+instance NFData IdrisColour where
+  rnf (IdrisColour _ x2 x3 x4 x5) = rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
 
+-- Handle doesn't have an NFData instance
 instance NFData OutputMode where
-  rnf (RawOutput x) = () -- no instance for Handle, so this is a bit wrong
+  rnf (RawOutput x) = ()
   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 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 x77 `seq` ()
+instance NFData a => NFData (D.Docstring a)
+instance NFData ConsoleWidth
+instance NFData PrimFn
+instance NFData SyntaxRules
+instance NFData Opt
+instance NFData TIData
+instance NFData IOption
+instance NFData LanguageExt
+instance NFData Optimisation
+instance NFData ColourTheme
+instance NFData OutputType
+instance NFData IBCWrite
+instance NFData a => NFData (D.Block a)
+instance NFData a => NFData (D.Inline a)
+instance NFData DocTerm
+instance NFData SizeChange
+instance NFData FnInfo
+instance NFData Codegen
+instance NFData IRFormat
+instance NFData LogCat
+instance NFData CGInfo
+instance NFData Fixity
+instance NFData FixDecl
+instance NFData Static
+instance NFData ArgOpt
+instance NFData Plicity
+instance NFData FnOpt
+instance NFData DataOpt
+instance NFData Directive
+instance (NFData t) => NFData (PDecl' t)
+instance NFData t => NFData (ProvideWhat' t)
+instance NFData PunInfo
+instance (NFData t) => NFData (PClause' t)
+instance (NFData t) => NFData (PData' t)
+instance NFData PTerm
+instance NFData PAltType
+instance (NFData t) => NFData (PTactic' t)
+instance (NFData t) => NFData (PDo' t)
+instance (NFData t) => NFData (PArg' t)
+instance NFData ClassInfo
+instance NFData RecordInfo
+instance NFData OptInfo
+instance NFData TypeInfo
+instance (NFData t) => NFData (DSL' t)
+instance NFData SynContext
+instance NFData Syntax
+instance NFData SSymbol
+instance NFData Using
+instance NFData SyntaxInfo
+instance NFData DefaultTotality
+instance NFData IState
diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs
--- a/src/Idris/Delaborate.hs
+++ b/src/Idris/Delaborate.hs
@@ -8,7 +8,7 @@
 {-# LANGUAGE PatternGuards #-}
 {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
 module Idris.Delaborate (
-    annName, bugaddr, delab, delab', delabMV, delabSugared
+    annName, bugaddr, delab, delabDirect, delab', delabMV, delabSugared
   , delabTy, delabTy', fancifyAnnots, pprintDelab, pprintNoDelab
   , pprintDelabTy, pprintErr, resugar
   ) where
@@ -81,30 +81,50 @@
 
 -- | Delaborate a term without resugaring
 delab :: IState -> Term -> PTerm
-delab i tm = delab' i tm False False
+delab i tm = delab' i tm False False 
 
 delabMV :: IState -> Term -> PTerm
-delabMV i tm = delab' i tm False True
+delabMV i tm = delab' i tm False True 
 
+-- | Delaborate a term directly, leaving case applications as they are.
+-- We need this for interactive case splitting, where we need access to the
+-- underlying function in a delaborated form, to generate the right patterns
+delabDirect :: IState -> Term -> PTerm
+delabDirect i tm = delabTy' i [] tm False False False
+
 delabTy :: IState -> Name -> PTerm
 delabTy i n
     = case lookupTy n (tt_ctxt i) of
            (ty:_) -> case lookupCtxt n (idris_implicits i) of
-                         (imps:_) -> delabTy' i imps ty False False
-                         _ -> delabTy' i [] ty False False
+                         (imps:_) -> delabTy' i imps ty False False True
+                         _ -> delabTy' i [] ty False False True
            [] -> error "delabTy: got non-existing name"
 
 delab' :: IState -> Term -> Bool -> Bool -> PTerm
-delab' i t f mvs = delabTy' i [] t f mvs
+delab' i t f mvs = delabTy' i [] t f mvs True
 
 delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any
           -> Term
           -> Bool -- ^ use full names
           -> Bool -- ^ Don't treat metavariables specially
+          -> Bool -- ^ resugar cases
           -> PTerm
-delabTy' ist imps tm fullname mvs = de [] imps tm
+delabTy' ist imps tm fullname mvs docases = de [] imps tm
   where
     un = fileFC "(val)"
+    
+    -- Special case for spotting applications of case functions
+    -- (Normally the scrutinee is let-bound, but hole types get normalised,
+    -- so they could appear in this form. The scrutinee is always added as
+    -- the last argument,
+    -- although that's not always the thing that gets pattern matched
+    -- in the elaborated block)
+    de env imps sc
+          | docases
+          , isCaseApp sc
+          , (P _ cOp _, args@(_:_)) <- unApply sc
+          , Just caseblock <- delabCase env imps (last args) cOp args 
+                 = caseblock
 
     de env _ (App _ f a) = deFn env f [a]
     de env _ (V i)     | i < length env = PRef un [] (snd (env!!i))
@@ -141,9 +161,10 @@
           = PPi expl n NoFC (de env [] ty) (de ((n,n):env) [] sc)
 
     de env imps (Bind n (Let ty val) sc)
-          | isCaseApp sc
+          | docases
+          , isCaseApp sc
           , (P _ cOp _, args) <- unApply sc
-          , Just caseblock    <- delabCase env imps n val cOp args = caseblock
+          , Just caseblock    <- delabCase env imps val cOp args = caseblock
           | otherwise    =
               PLet un n NoFC (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)
     de env _ (Bind n (Hole ty) sc) = de ((n, sUN "[__]"):env) [] sc
@@ -206,8 +227,8 @@
             isCN (SN (CaseN _ _)) = True
             isCN _ = False
 
-    delabCase :: [(Name, Name)] -> [PArg] -> Name -> Term -> Name -> [Term] -> Maybe PTerm
-    delabCase env imps scvar scrutinee caseName caseArgs =
+    delabCase :: [(Name, Name)] -> [PArg] -> Term -> Name -> [Term] -> Maybe PTerm
+    delabCase env imps scrutinee caseName caseArgs =
       do cases <- case lookupCtxt caseName (idris_patdefs ist) of
                     [(cases, _)] -> return cases
                     _ -> Nothing
@@ -247,8 +268,8 @@
     = case lookupTy n (tt_ctxt i) of
            (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $
                      case lookupCtxt n (idris_implicits i) of
-                         (imps:_) -> resugar i $ delabTy' i imps ty False False
-                         _ -> resugar i $ delabTy' i [] ty False False
+                         (imps:_) -> resugar i $ delabTy' i imps ty False False True
+                         _ -> resugar i $ delabTy' i [] ty False False True
            [] -> error "pprintDelabTy got a name that doesn't exist"
 
 pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
diff --git a/src/Idris/Docs.hs b/src/Idris/Docs.hs
--- a/src/Idris/Docs.hs
+++ b/src/Idris/Docs.hs
@@ -69,49 +69,62 @@
                 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d
 
 pprintFD :: IState -> Bool -> Bool -> FunDoc -> Doc OutputAnnotation
-pprintFD ist totalityFlag nsFlag (FD n doc args ty f)
-    = nest 4 (prettyName True nsFlag [] n <+> colon <+>
-              pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
-                                     , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>
-              -- show doc
-              renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc <$>
-              -- show fixity
-              maybe empty (\f -> text (show f) <> line) f <>
-              -- show arguments doc
-              let argshow = showArgs args [] in
-              (if not (null argshow)
-                then nest 4 $ text "Arguments:" <$> vsep argshow
-                else empty) <>
-              -- show totality status
-              let totality = getTotality in
-              (if totalityFlag && not (null totality) then
-                line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)
-               else
-                empty))
+pprintFD ist totalityFlag nsFlag (FD n doc args ty f) =
+          nest 4 (prettyName True nsFlag [] n
+      <+> colon
+      <+> pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
+                             , not (T.isPrefixOf (T.pack "__") n') ] infixes ty
+      -- show doc
+      <$> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc
+      -- show fixity
+      <$> maybe empty (\f -> text (show f) <> line) f
+      -- show arguments doc
+      <> let argshow = showArgs args [] in
+           (if not (null argshow)
+             then nest 4 $ text "Arguments:" <$> vsep argshow
+             else empty)
+      -- show totality status
+      <> let totality = getTotality in
+           (if totalityFlag && not (null totality)
+              then line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)
+              else empty))
 
-    where ppo = ppOptionIst ist
-          infixes = idris_infixes ist
-          showArgs ((n, ty, Exp {}, Just d):args) bnd
-             = bindingOf n False <+> colon <+>
-               pprintPTerm ppo bnd [] infixes ty <>
-               showDoc ist d <> line
-               :
-               showArgs args ((n, False):bnd)
-          showArgs ((n, ty, Constraint {}, Just d):args) bnd
-             = text "Class constraint" <+>
-               pprintPTerm ppo bnd [] infixes ty <> showDoc ist d <> line
-               :
-               showArgs args ((n, True):bnd)
-          showArgs ((n, ty, Imp {}, Just d):args) bnd
-             = text "(implicit)" <+>
-               bindingOf n True <+> colon <+>
-               pprintPTerm ppo bnd [] infixes ty <>
-               showDoc ist d <> line
-               :
-               showArgs args ((n, True):bnd)
-          showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
-          showArgs []                  _ = []
-          getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)
+    where
+      ppo = ppOptionIst ist
+
+      infixes = idris_infixes ist
+
+      -- Recurse over and show the Function's Documented arguments
+      showArgs ((n, ty, Exp {}, Just d):args)        bnd = -- Explicitly bound.
+            bindingOf n False
+        <+> colon
+        <+> pprintPTerm ppo bnd [] infixes ty
+        <> showDoc ist d
+        <> line : showArgs args ((n, False):bnd)
+      showArgs ((n, ty, Constraint {}, Just d):args) bnd = -- Class constraints.
+            text "Class constraint"
+        <+> pprintPTerm ppo bnd [] infixes ty
+        <> showDoc ist d
+        <> line : showArgs args ((n, True):bnd)
+      showArgs ((n, ty, Imp {}, Just d):args)        bnd = -- Implicit arguments.
+            text "(implicit)"
+        <+> bindingOf n True
+        <+> colon
+        <+> pprintPTerm ppo bnd [] infixes ty
+        <> showDoc ist d
+        <> line : showArgs args ((n, True):bnd)
+      showArgs ((n, ty, TacImp{}, Just d):args)      bnd = -- Tacit implicits
+            text "(auto implicit)"
+        <+> bindingOf n True
+        <+> colon
+        <+> pprintPTerm ppo bnd [] infixes ty
+        <> showDoc ist d
+        <> line : showArgs args ((n, True):bnd)
+      showArgs ((n, _, _, _):args)                   bnd = -- Anything else
+            showArgs args ((n, True):bnd)
+      showArgs []                                    _   = [] -- end of arguments
+
+      getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)
 
 pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
 pprintFDWithTotality ist = pprintFD ist True
diff --git a/src/Idris/Docstrings.hs b/src/Idris/Docstrings.hs
--- a/src/Idris/Docstrings.hs
+++ b/src/Idris/Docstrings.hs
@@ -6,7 +6,7 @@
 Maintainer  : The Idris Community.
 -}
 
-{-# LANGUAGE DeriveFunctor, ScopedTypeVariables #-}
+{-# LANGUAGE DeriveFunctor, DeriveGeneric, ScopedTypeVariables #-}
 {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
 module Idris.Docstrings (
     Docstring(..), Block(..), Inline(..), parseDocstring, renderDocstring
@@ -30,7 +30,7 @@
 import Data.Traversable (Traversable)
 import qualified Data.Sequence as S
 
-import Control.DeepSeq (NFData(..))
+import GHC.Generics (Generic)
 
 import Text.Blaze.Html (Html)
 
@@ -39,7 +39,7 @@
              | Checked Term
              | Example Term
              | Failing Err
-  deriving Show
+  deriving (Show, Generic)
 
 -- | Render a term in the documentation
 renderDocTerm :: (Term -> Doc OutputAnnotation) -> (Term -> Term) -> DocTerm -> String -> Doc OutputAnnotation
@@ -53,7 +53,7 @@
 -- | Representation of Idris's inline documentation. The type paramter
 -- represents the type of terms that are associated with code blocks.
 data Docstring a = DocString CT.Options (Blocks a)
-  deriving (Show, Functor, Foldable, Traversable)
+  deriving (Show, Functor, Foldable, Traversable, Generic)
 
 type Blocks a = S.Seq (Block a)
 
@@ -65,7 +65,7 @@
              | CodeBlock CT.CodeAttr T.Text a
              | HtmlBlock T.Text
              | HRule
-             deriving (Show, Functor, Foldable, Traversable)
+             deriving (Show, Functor, Foldable, Traversable, Generic)
 
 data Inline a = Str T.Text
               | Space
@@ -78,7 +78,7 @@
               | Image (Inlines a) T.Text T.Text
               | Entity T.Text
               | RawHtml T.Text
-              deriving (Show, Functor, Foldable, Traversable)
+              deriving (Show, Functor, Foldable, Traversable, Generic)
 
 type Inlines a = S.Seq (Inline a)
 
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
@@ -84,7 +84,8 @@
                     -- question: CAFs in where blocks?
                     tclift $ tfail $ At fc (NoTypeDecl n)
               [ty] -> return ty
-           let atys = map snd (getArgTys fty)
+           let atys_in = map snd (getArgTys (normalise ctxt [] fty))
+           let atys = map (\x -> (x, isCanonical x ctxt)) atys_in
            cs_elab <- mapM (elabClause info opts)
                            (zip [0..] cs)
            ctxt <- getContext
@@ -670,7 +671,9 @@
                     (do pbinds ist lhs_tm
                         -- proof search can use explicitly written names
                         mapM_ addPSname (allNamesIn lhs_in)
-                        mapM_ setinj (nub (tcparams ++ inj))
+                        ulog <- getUnifyLog
+                        traceWhen ulog ("Setting injective: " ++ show (nub (tcparams ++ inj))) $
+                          mapM_ setinj (nub (tcparams ++ inj))
                         setNextName
                         (ElabResult _ _ is ctxt' newDecls highlights newGName) <-
                           errAt "right hand side of " fname (Just clhsty)
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
@@ -310,7 +310,7 @@
         apt <- expandToArity t
         itm <- if not pattern then insertImpLam ina apt else return apt
         ct <- insertCoerce ina itm
-        t' <- insertLazy ct
+        t' <- insertLazy ina ct
         g <- goal
         tm <- get_term
         ps <- get_probs
@@ -624,7 +624,7 @@
                       do patvar n
                          update_term liftPats
                          highlightSource fc (AnnBoundName n False)
-               else if (defined && not guarded)
+               else if defined
                        then do apply (Var n) []
                                annot <- findHighlight n
                                solve
@@ -834,6 +834,7 @@
             ty <- goal
             fty <- get_type (Var f)
             ctxt <- get_context
+            let dataCon = isDConName f ctxt
             annot <- findHighlight f
             mapM_ checkKnownImplicit args_in
             let args = insertScopedImps fc (normalise ctxt env fty) args_in
@@ -849,7 +850,8 @@
                then -- simple app, as below
                     do simple_app False
                                   (elabE (ina { e_isfn = True }) (Just fc) (PRef ffc hls f))
-                                  (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))
+                                  (elabE (ina { e_inarg = True,
+                                                e_guarded = dataCon }) (Just fc) (getTm (head args)))
                                   (show tm)
                        solve
                        mapM (uncurry highlightSource) $
@@ -873,7 +875,8 @@
                     ns <- apply (Var f) (map isph args)
 --                    trace ("ns is " ++ show ns) $ return ()
                     -- mark any type class arguments as injective
-                    when (not pattern) $ mapM_ checkIfInjective (map snd ns)
+--                     when (not pattern) $ 
+                    mapM_ checkIfInjective (map snd ns)
                     unifyProblems -- try again with the new information,
                                   -- to help with disambiguation
                     ulog <- getUnifyLog
@@ -882,7 +885,8 @@
                     mapM (uncurry highlightSource) $
                       (ffc, annot) : map (\f -> (f, annot)) hls
 
-                    elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })
+                    elabArgs ist (ina { e_inarg = e_inarg ina || not isinf,
+                                        e_guarded = dataCon })
                            [] fc False f
                              (zip ns (unmatchableArgs ++ repeat False))
                              (f == sUN "Force")
@@ -909,8 +913,7 @@
                                  ivs' <- get_instances
                                  -- Attempt to resolve any type classes which have 'complete' types,
                                  -- i.e. no holes in them
-                                 when (not pattern || (e_inarg ina && not tcgen &&
-                                                      not (e_guarded ina))) $
+                                 when (not pattern || (e_inarg ina && not tcgen)) $ 
                                     mapM_ (\n -> do focus n
                                                     g <- goal
                                                     env <- get_env
@@ -962,7 +965,9 @@
                                         -- maybe we can solve more things now...
                                            ulog <- getUnifyLog
                                            probs <- get_probs
-                                           traceWhen ulog ("Injective now " ++ show args ++ "\n" ++ qshow probs) $
+                                           inj <- get_inj
+                                           traceWhen ulog ("Injective now " ++ show args ++ "\nAll: " ++ show inj 
+                                                            ++ "\nProblems: " ++ qshow probs) $
                                              unifyProblems
                                            probs <- get_probs
                                            traceWhen ulog (qshow probs) $ return ()
@@ -1409,14 +1414,14 @@
     -- first. We need to do this brute force approach, rather than anything
     -- more precise, since there may be various other ambiguities to resolve
     -- first.
-    insertLazy :: PTerm -> ElabD PTerm
-    insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t
-    insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t
-    insertLazy (PCoerced t) = return t
-    -- Don't add a delay to pattern variables, since they can be forced
-    -- on the rhs
-    insertLazy t@(PPatvar _ _) | pattern = return t
-    insertLazy t =
+    insertLazy :: ElabCtxt -> PTerm -> ElabD PTerm
+    insertLazy ina t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t
+    insertLazy ina t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t
+    insertLazy ina (PCoerced t) = return t
+    -- Don't add a delay to top level pattern variables, since they 
+    -- can be forced on the rhs if needed
+    insertLazy ina t@(PPatvar _ _) | pattern && not (e_guarded ina) = return t
+    insertLazy ina t =
         do ty <- goal
            env <- get_env
            let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)
@@ -1923,11 +1928,13 @@
                                                 in (ns, lhs', Impossible))
                             clauses'
          let clauses''' = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses''
+         let argtys = map (\x -> (x, isCanonical x ctxt))
+                          (map snd (getArgTys (normalise ctxt [] ty)))
          ctxt'<- lift $
                   addCasedef n (const [])
                              info False (STerm Erased)
                              True False -- TODO what are these?
-                             (map snd $ getArgTys ty) [] -- TODO inaccessible types
+                             argtys [] -- TODO inaccessible types
                              clauses'
                              clauses'''
                              clauses'''
@@ -2007,15 +2014,27 @@
         getRetTy (Bind _ (Pi _ _ _) sc) = getRetTy sc
         getRetTy ty = ty
 
+    elabScriptStuck :: Term -> ElabD a
+    elabScriptStuck x = lift . tfail $ ElabScriptStuck x
+
+
+    -- Should be dependent
+    tacTmArgs :: Int -> Term -> [Term] -> ElabD [Term]
+    tacTmArgs l t args | length args == l = return args
+                       | otherwise        = elabScriptStuck t -- Probably should be an argument size mismatch internal error
+
+
     -- | Do a step in the reflected elaborator monad. The input is the
     -- step, the output is the (reflected) term returned.
     runTacTm :: Term -> ElabD Term
-    runTacTm (unApply -> tac@(P _ n _, args))
-      | n == tacN "Prim__Solve", [] <- args
-      = do solve
+    runTacTm tac@(unApply -> (P _ n _, args))
+      | n == tacN "Prim__Solve"
+      = do ~[] <- tacTmArgs 0 tac args -- patterns are irrefutable because `tacTmArgs` returns lists of exactly the size given to it as first argument
+           solve
            returnUnit
-      | n == tacN "Prim__Goal", [] <- args
-      = do hs <- get_holes
+      | n == tacN "Prim__Goal"
+      = do ~[] <- tacTmArgs 0 tac args
+           hs <- get_holes
            case hs of
              (h : _) -> do t <- goal
                            fmap fst . checkClosed $
@@ -2024,15 +2043,18 @@
              [] -> lift . tfail . Msg $
                      "Elaboration is complete. There are no goals."
 
-      | n == tacN "Prim__Holes", [] <- args
-      = do hs <- get_holes
+      | n == tacN "Prim__Holes"
+      = do ~[] <- tacTmArgs 0 tac args
+           hs <- get_holes
            fmap fst . checkClosed $
              mkList (Var $ reflm "TTName") (map reflectName hs)
-      | n == tacN "Prim__Guess", [] <- args
-      = do g <- get_guess
+      | n == tacN "Prim__Guess"
+      = do ~[] <- tacTmArgs 0 tac args
+           g <- get_guess
            fmap fst . checkClosed $ reflect g
-      | n == tacN "Prim__LookupTy", [n] <- args
-      = do n' <- reifyTTName n
+      | n == tacN "Prim__LookupTy"
+      = do ~[name] <- tacTmArgs 1 tac args
+           n' <- reifyTTName name
            ctxt <- get_context
            let getNameTypeAndType = \case Function ty _       -> (Ref, ty)
                                           TyDecl nt ty        -> (nt, ty)
@@ -2053,20 +2075,23 @@
                                              , raw_apply (Var pairTy) [ Var (reflm "NameType")
                                                                        , Var (reflm "TT")]])
                      defs
-      | n == tacN "Prim__LookupDatatype", [name] <- args
-      = do n' <- reifyTTName name
+      | n == tacN "Prim__LookupDatatype"
+      = do ~[name] <- tacTmArgs 1 tac args
+           n' <- reifyTTName name
            datatypes <- get_datatypes
            ctxt <- get_context
            fmap fst . checkClosed $
              rawList (Var (tacN "Datatype"))
                      (map reflectDatatype (buildDatatypes ist n'))
-      | n == tacN "Prim__LookupFunDefn", [name] <- args
-      = do n' <- reifyTTName name
+      | n == tacN "Prim__LookupFunDefn"
+      = do ~[name] <- tacTmArgs 1 tac args
+           n' <- reifyTTName name
            fmap fst . checkClosed $
              rawList (RApp (Var $ tacN "FunDefn") (Var $ reflm "TT"))
                (map reflectFunDefn (buildFunDefns ist n'))
-      | n == tacN "Prim__LookupArgs", [name] <- args
-      = do n' <- reifyTTName name
+      | n == tacN "Prim__LookupArgs"
+      = do ~[name] <- tacTmArgs 1 tac args
+           n' <- reifyTTName name
            let listTy = Var (sNS (sUN "List") ["List", "Prelude"])
                listFunArg = RApp listTy (Var (tacN "FunArg"))
             -- Idris tuples nest to the right
@@ -2089,37 +2114,45 @@
                                                                              (Var (tacN "FunArg"))
                                                                       , Var (reflm "Raw")]])
                      out
-      | n == tacN "Prim__SourceLocation", [] <- args
-      = fmap fst . checkClosed $
-          reflectFC fc
-      | n == tacN "Prim__Namespace", [] <- args
-      = fmap fst . checkClosed $
-          rawList (RConstant StrType) (map (RConstant . Str) ns)
-      | n == tacN "Prim__Env", [] <- args
-      = do env <- get_env
+      | n == tacN "Prim__SourceLocation"
+      = do ~[] <- tacTmArgs 0 tac args
+           fmap fst . checkClosed $
+             reflectFC fc
+      | n == tacN "Prim__Namespace"
+      = do ~[] <- tacTmArgs 0 tac args
+           fmap fst . checkClosed $
+             rawList (RConstant StrType) (map (RConstant . Str) ns)
+      | n == tacN "Prim__Env"
+      = do ~[] <- tacTmArgs 0 tac args
+           env <- get_env
            fmap fst . checkClosed $ reflectEnv env
-      | n == tacN "Prim__Fail", [_a, errs] <- args
-      = do errs' <- eval errs
+      | n == tacN "Prim__Fail"
+      = do ~[_a, errs] <- tacTmArgs 2 tac args
+           errs' <- eval errs
            parts <- reifyReportParts errs'
            lift . tfail $ ReflectionError [parts] (Msg "")
-      | n == tacN "Prim__PureElab", [_a, tm] <- args
-      = return tm
-      | n == tacN "Prim__BindElab", [_a, _b, first, andThen] <- args
-      = do first' <- eval first
+      | n == tacN "Prim__PureElab"
+      = do ~[_a, tm] <- tacTmArgs 2 tac args
+           return tm
+      | n == tacN "Prim__BindElab"
+      = do ~[_a, _b, first, andThen] <- tacTmArgs 4 tac args
+           first' <- eval first
            res <- eval =<< runTacTm first'
            next <- eval (App Complete andThen res)
            runTacTm next
-      | n == tacN "Prim__Try", [_a, first, alt] <- args
-      = do first' <- eval first
+      | n == tacN "Prim__Try"
+      = do ~[_a, first, alt] <- tacTmArgs 3 tac args
+           first' <- eval first
            alt' <- eval alt
            try' (runTacTm first') (runTacTm alt') True
-      | n == tacN "Prim__Fill", [raw] <- args
-      = do raw' <- reifyRaw =<< eval raw
+      | n == tacN "Prim__Fill"
+      = do ~[raw] <- tacTmArgs 1 tac args
+           raw' <- reifyRaw =<< eval raw
            apply raw' []
            returnUnit
       | n == tacN "Prim__Apply" || n == tacN "Prim__MatchApply"
-      , [raw, argSpec] <- args
-      = do raw' <- reifyRaw =<< eval raw
+      = do ~[raw, argSpec] <- tacTmArgs 2 tac args
+           raw' <- reifyRaw =<< eval raw
            argSpec' <- map (\b -> (b, 0)) <$> reifyList reifyBool argSpec
            let op = if n == tacN "Prim__Apply"
                        then apply
@@ -2131,89 +2164,105 @@
                                (reflectName n1, reflectName n2)
                      | (n1, n2) <- ns
                      ]
-      | n == tacN "Prim__Gensym", [hint] <- args
-      = do hintStr <- eval hint
+      | n == tacN "Prim__Gensym"
+      = do ~[hint] <- tacTmArgs 1 tac args
+           hintStr <- eval hint
            case hintStr of
              Constant (Str h) -> do
                n <- getNameFrom (sMN 0 h)
                fmap fst $ get_type_val (reflectName n)
              _ -> fail "no hint"
-      | n == tacN "Prim__Claim", [n, ty] <- args
-      = do n' <- reifyTTName n
+      | n == tacN "Prim__Claim"
+      = do ~[n, ty] <- tacTmArgs 2 tac args
+           n' <- reifyTTName n
            ty' <- reifyRaw ty
            claim n' ty'
            returnUnit
-      | n == tacN "Prim__Check", [env', raw] <- args
-      = do env <- reifyEnv env'
+      | n == tacN "Prim__Check"
+      = do ~[env', raw] <- tacTmArgs 2 tac args
+           env <- reifyEnv env'
            raw' <- reifyRaw =<< eval raw
            ctxt <- get_context
            (tm, ty) <- lift $ check ctxt env raw'
            fmap fst . checkClosed $
              rawPair (Var (reflm "TT"), Var (reflm "TT"))
                      (reflect tm,       reflect ty)
-      | n == tacN "Prim__Attack", [] <- args
-      = do attack
+      | n == tacN "Prim__Attack"
+      = do ~[] <- tacTmArgs 0 tac args
+           attack
            returnUnit
-      | n == tacN "Prim__Rewrite", [rule] <- args
-      = do r <- reifyRaw rule
+      | n == tacN "Prim__Rewrite"
+      = do ~[rule] <- tacTmArgs 1 tac args
+           r <- reifyRaw rule
            rewrite r
            returnUnit
-      | n == tacN "Prim__Focus", [what] <- args
-      = do n' <- reifyTTName what
+      | n == tacN "Prim__Focus"
+      = do ~[what] <- tacTmArgs 1 tac args
+           n' <- reifyTTName what
            hs <- get_holes
            if elem n' hs
               then focus n' >> returnUnit
               else lift . tfail . Msg $ "The name " ++ show n' ++ " does not denote a hole"
-      | n == tacN "Prim__Unfocus", [what] <- args
-      = do n' <- reifyTTName what
+      | n == tacN "Prim__Unfocus"
+      = do ~[what] <- tacTmArgs 1 tac args
+           n' <- reifyTTName what
            movelast n'
            returnUnit
-      | n == tacN "Prim__Intro", [mn] <- args
-      = do n <- case fromTTMaybe mn of
+      | n == tacN "Prim__Intro"
+      = do ~[mn] <- tacTmArgs 1 tac args
+           n <- case fromTTMaybe mn of
                   Nothing -> return Nothing
                   Just name -> fmap Just $ reifyTTName name
            intro n
            returnUnit
-      | n == tacN "Prim__Forall", [n, ty] <- args
-      = do n' <- reifyTTName n
+      | n == tacN "Prim__Forall"
+      = do ~[n, ty] <- tacTmArgs 2 tac args
+           n' <- reifyTTName n
            ty' <- reifyRaw ty
            forall n' Nothing ty'
            returnUnit
-      | n == tacN "Prim__PatVar", [n] <- args
-      = do n' <- reifyTTName n
+      | n == tacN "Prim__PatVar"
+      = do ~[n] <- tacTmArgs 1 tac args
+           n' <- reifyTTName n
            patvar' n'
            returnUnit
-      | n == tacN "Prim__PatBind", [n] <- args
-      = do n' <- reifyTTName n
+      | n == tacN "Prim__PatBind"
+      = do ~[n] <- tacTmArgs 1 tac args
+           n' <- reifyTTName n
            patbind n'
            returnUnit
-      | n == tacN "Prim__LetBind", [n, ty, tm] <- args
-      = do n' <- reifyTTName n
+      | n == tacN "Prim__LetBind"
+      = do ~[n, ty, tm] <- tacTmArgs 3 tac args
+           n' <- reifyTTName n
            ty' <- reifyRaw ty
            tm' <- reifyRaw tm
            letbind n' ty' tm'
            returnUnit
-      | n == tacN "Prim__Compute", [] <- args
-      = do compute ; returnUnit
-      | n == tacN "Prim__Normalise", [env, tm] <- args
-      = do env' <- reifyEnv env
+      | n == tacN "Prim__Compute"
+      = do ~[] <- tacTmArgs 0 tac args; compute ; returnUnit
+      | n == tacN "Prim__Normalise"
+      = do ~[env, tm] <- tacTmArgs 2 tac args
+           env' <- reifyEnv env
            tm' <- reifyTT tm
            ctxt <- get_context
            let out = normaliseAll ctxt env' (finalise tm')
            fmap fst . checkClosed $ reflect out
-      | n == tacN "Prim__Whnf", [tm] <- args
-      = do tm' <- reifyTT tm
+      | n == tacN "Prim__Whnf"
+      = do ~[tm] <- tacTmArgs 1 tac args
+           tm' <- reifyTT tm
            ctxt <- get_context
            fmap fst . checkClosed . reflect $ whnf ctxt tm'
-      | n == tacN "Prim__Converts", [env, tm1, tm2] <- args
-      = do env' <- reifyEnv env
+      | n == tacN "Prim__Converts"
+      = do ~[env, tm1, tm2] <- tacTmArgs 3 tac args
+           env' <- reifyEnv env
            tm1' <- reifyTT tm1
            tm2' <- reifyTT tm2
            ctxt <- get_context
            lift $ converts ctxt env' tm1' tm2'
            returnUnit
-      | n == tacN "Prim__DeclareType", [decl] <- args
-      = do (RDeclare n args res) <- reifyTyDecl decl
+      | n == tacN "Prim__DeclareType"
+      = do ~[decl] <- tacTmArgs 1 tac args
+           (RDeclare n args res) <- reifyTyDecl decl
            ctxt <- get_context
            let rty = foldr mkPi res args
            (checked, ty') <- lift $ check ctxt [] rty
@@ -2225,12 +2274,14 @@
            updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
                                                new_tyDecls e }
            returnUnit
-      | n == tacN "Prim__DefineFunction", [decl] <- args
-      = do defn <- reifyFunDefn decl
+      | n == tacN "Prim__DefineFunction"
+      = do ~[decl] <- tacTmArgs 1 tac args
+           defn <- reifyFunDefn decl
            defineFunction defn
            returnUnit
-      | n == tacN "Prim__DeclareDatatype", [decl] <- args
-      = do RDeclare n args resTy <- reifyTyDecl decl
+      | n == tacN "Prim__DeclareDatatype"
+      = do ~[decl] <- tacTmArgs 1 tac args
+           RDeclare n args resTy <- reifyTyDecl decl
            ctxt <- get_context
            let tcTy = foldr mkPi resTy args
            (checked, ty') <- lift $ check ctxt [] tcTy
@@ -2240,8 +2291,9 @@
            set_context ctxt'
            updateAux $ \e -> e { new_tyDecls = RDatatypeDeclInstrs n (map rFunArgToPArg args) : new_tyDecls e }
            returnUnit
-      | n == tacN "Prim__DefineDatatype", [defn] <- args
-      = do RDefineDatatype n ctors <- reifyRDataDefn defn
+      | n == tacN "Prim__DefineDatatype"
+      = do ~[defn] <- tacTmArgs 1 tac args
+           RDefineDatatype n ctors <- reifyRDataDefn defn
            ctxt <- get_context
            tyconTy <- case lookupTyExact n ctxt of
                         Just t -> return t
@@ -2264,24 +2316,28 @@
            -- the rest happens in a bit
            updateAux $ \e -> e { new_tyDecls = RDatatypeDefnInstrs n tyconTy ctors' : new_tyDecls e }
            returnUnit
-      | n == tacN "Prim__AddInstance", [cls, inst] <- args
-      = do className <- reifyTTName cls
+      | n == tacN "Prim__AddInstance"
+      = do ~[cls, inst] <- tacTmArgs 2 tac args
+           className <- reifyTTName cls
            instName <- reifyTTName inst
            updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
                                                new_tyDecls e }
            returnUnit
-      | n == tacN "Prim__IsTCName", [n] <- args
-      = do n' <- reifyTTName n
+      | n == tacN "Prim__IsTCName"
+      = do ~[n] <- tacTmArgs 1 tac args
+           n' <- reifyTTName n
            case lookupCtxtExact n' (idris_classes ist) of
              Just _ -> fmap fst . checkClosed $ Var (sNS (sUN "True") ["Bool", "Prelude"])
              Nothing -> fmap fst . checkClosed $ Var (sNS (sUN "False") ["Bool", "Prelude"])
-      | n == tacN "Prim__ResolveTC", [fn] <- args
-      = do g <- goal
+      | n == tacN "Prim__ResolveTC"
+      = do ~[fn] <- tacTmArgs 1 tac args
+           g <- goal
            fn <- reifyTTName fn
            resolveTC' False True 100 g fn ist
            returnUnit
-      | n == tacN "Prim__Search", [depth, hints] <- args
-      = do d <- eval depth
+      | n == tacN "Prim__Search"
+      = do ~[depth, hints] <- tacTmArgs 2 tac args
+           d <- eval depth
            hints' <- eval hints
            case (d, unList hints') of
              (Constant (I i), Just hs) ->
@@ -2293,8 +2349,9 @@
              (Constant (I _), Nothing ) ->
                lift . tfail . InternalMsg $ "Not a list: " ++ show hints'
              (_, _) -> lift . tfail . InternalMsg $ "Can't reify int " ++ show d
-      | n == tacN "Prim__RecursiveElab", [goal, script] <- args
-      = do goal' <- reifyRaw goal
+      | n == tacN "Prim__RecursiveElab"
+      = do ~[goal, script] <- tacTmArgs 2 tac args
+           goal' <- reifyRaw goal
            ctxt <- get_context
            script <- eval script
            (goalTT, goalTy) <- lift $ check ctxt [] goal'
@@ -2327,8 +2384,9 @@
            fmap fst . checkClosed $
              rawPair (Var $ reflm "TT", Var $ reflm "TT")
                      (tm', ty')
-      | n == tacN "Prim__Metavar", [n] <- args
-      = do n' <- reifyTTName n
+      | n == tacN "Prim__Metavar"
+      = do ~[n] <- tacTmArgs 1 tac args
+           n' <- reifyTTName n
            ctxt <- get_context
            ptm <- get_term
            -- See documentation above in the elab case for PMetavar
@@ -2338,8 +2396,9 @@
            defer unique_used mvn
            solve
            returnUnit
-      | n == tacN "Prim__Fixity", [op'] <- args
-      = do opTm <- eval op'
+      | n == tacN "Prim__Fixity"
+      = do ~[op'] <- tacTmArgs 1 tac args
+           opTm <- eval op'
            case opTm of
              Constant (Str op) ->
                let opChars = ":!#$%&*+./<=>?@\\^|-~"
@@ -2352,11 +2411,12 @@
                             [f]  -> fmap fst . checkClosed $ reflectFixity f
                             many -> lift . tfail . InternalMsg $ "Ambiguous fixity for '" ++ op ++ "'!  Found " ++ show many
              _ -> lift . tfail . Msg $ "Not a constant string for an operator name: " ++ show opTm
-      | n == tacN "Prim__Debug", [ty, msg] <- args
-      = do msg' <- eval msg
+      | n == tacN "Prim__Debug"
+      = do ~[ty, msg] <- tacTmArgs 2 tac args
+           msg' <- eval msg
            parts <- reifyReportParts msg
            debugElaborator parts
-    runTacTm x = lift . tfail $ ElabScriptStuck x
+    runTacTm x = elabScriptStuck x
 
 -- Running tactics directly
 -- if a tactic adds unification problems, return an error
@@ -2540,7 +2600,7 @@
              focus script
              ptm <- get_term
              elab ist toplevel ERHS [] (sMN 0 "tac")
-                  (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])
+                  (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True True)])
              (script', _) <- get_type_val (Var scriptvar)
              -- now that we have the script apply
              -- it to the reflected goal
diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs
--- a/src/Idris/IBC.hs
+++ b/src/Idris/IBC.hs
@@ -49,7 +49,7 @@
 import Debug.Trace
 
 ibcVersion :: Word16
-ibcVersion = 144
+ibcVersion = 145
 
 -- | When IBC is being loaded - we'll load different things (and omit
 -- different structures/definitions) depending on which phase we're in.
diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs
--- a/src/Idris/Parser.hs
+++ b/src/Idris/Parser.hs
@@ -1569,7 +1569,7 @@
 parseImports fname input
     = do i <- getIState
          case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of
-              Failure err -> fail (show err)
+              Failure (ErrInfo err _) -> fail (show err)
               Success (x, annots, i) ->
                 do putIState i
                    fname' <- runIO $ Dir.makeAbsolute fname
@@ -1631,7 +1631,7 @@
 parseProg syn fname input mrk
     = do i <- getIState
          case runparser mainProg i fname input of
-            Failure doc     -> do -- FIXME: Get error location from trifecta
+            Failure (ErrInfo doc _)     -> do -- FIXME: Get error location from trifecta
                                   -- this can't be the solution!
                                   -- Issue #1575 on the issue tracker.
                                   --    https://github.com/idris-lang/Idris-dev/issues/1575
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
@@ -829,6 +829,9 @@
   ;
 @
 -}
+
+data SetOrUpdate = FieldSet PTerm | FieldUpdate PTerm
+
 recordType :: SyntaxInfo -> IdrisParser PTerm
 recordType syn =
       do kw <- reservedFC "record"
@@ -836,7 +839,7 @@
          fgs <- fieldGetOrSet
          lchar '}'
          fc <- getFC
-         rec <- optional (simpleExpr syn)
+         rec <- optional (do notEndApp; simpleExpr syn)
          highlightP kw AnnKeyword
          case fgs of
               Left fields ->
@@ -854,28 +857,34 @@
                    Just v -> return (getAll fc (reverse fields) v)
 
        <?> "record setting expression"
-   where fieldSet :: IdrisParser ([Name], PTerm)
+   where fieldSet :: IdrisParser ([Name], SetOrUpdate)
          fieldSet = do ns <- fieldGet
-                       lchar '='
-                       e <- expr syn
-                       return (ns, e)
+                       (do lchar '='
+                           e <- expr syn
+                           return (ns, FieldSet e))
+                         <|> do symbol "$="
+                                e <- expr syn
+                                return (ns, FieldUpdate e)
                     <?> "field setter"
 
          fieldGet :: IdrisParser [Name]
          fieldGet = sepBy1 (fst <$> fnName) (symbol "->")
 
-         fieldGetOrSet :: IdrisParser (Either [([Name], PTerm)] [Name])
+         fieldGetOrSet :: IdrisParser (Either [([Name], SetOrUpdate)] [Name])
          fieldGetOrSet = try (do fs <- sepBy1 fieldSet (lchar ',')
                                  return (Left fs))
                      <|> do f <- fieldGet
                             return (Right f)
 
-         applyAll :: FC -> [([Name], PTerm)] -> PTerm -> PTerm
+         applyAll :: FC -> [([Name], SetOrUpdate)] -> PTerm -> PTerm
          applyAll fc [] x = x
          applyAll fc ((ns, e) : es) x
             = applyAll fc es (doUpdate fc ns e x)
 
-         doUpdate fc [n] e get
+         doUpdate fc ns (FieldUpdate e) get
+              = let get' = getAll fc (reverse ns) get in
+                    doUpdate fc ns (FieldSet (PApp fc e [pexp get'])) get
+         doUpdate fc [n] (FieldSet e) get
               = PApp fc (PRef fc [] (mkType n)) [pexp e, pexp get]
          doUpdate fc (n : ns) e get
               = PApp fc (PRef fc [] (mkType n))
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
@@ -58,6 +58,21 @@
 
 deriving instance Parsing IdrisInnerParser
 
+#if MIN_VERSION_base(4,9,0)
+instance {-# OVERLAPPING #-} DeltaParsing IdrisParser where
+  line = lift line
+  {-# INLINE line #-}
+  position = lift position
+  {-# INLINE position #-}
+  slicedWith f (StateT m) = StateT $ \s -> slicedWith (\(a,s') b -> (f a b, s')) $ m s
+  {-# INLINE slicedWith #-}
+  rend = lift rend
+  {-# INLINE rend #-}
+  restOfLine = lift restOfLine
+  {-# INLINE restOfLine #-}
+
+#endif
+
 #if MIN_VERSION_base(4,8,0)
 instance {-# OVERLAPPING #-} TokenParsing IdrisParser where
 #else
diff --git a/src/Idris/Prover.hs b/src/Idris/Prover.hs
--- a/src/Idris/Prover.hs
+++ b/src/Idris/Prover.hs
@@ -39,7 +39,7 @@
 import Idris.Output
 import Idris.TypeSearch (searchByType)
 
-import Text.Trifecta.Result(Result(..))
+import Text.Trifecta.Result(Result(..), ErrInfo(..))
 
 import System.IO (Handle, stdin, stdout, hPutStrLn)
 import System.Console.Haskeline
@@ -325,7 +325,7 @@
        (d, prev', st, done, prf', env', res) <-
          idrisCatch
            (case cmd of
-              Failure err ->
+              Failure (ErrInfo err _) ->
                 return (False, prev, e, False, prf, env, Left . Msg . show . fixColour (idris_colourRepl ist) $ err)
               Success (Left cmd') ->
                 case cmd' of
@@ -440,7 +440,7 @@
             _ -> return ()
          (d, st, done, prf', res) <- idrisCatch
            (case cmd of
-              Failure err -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)
+              Failure (ErrInfo err _) -> return (False, e, False, prf, Left . Msg . show . fixColour (idris_colourRepl i) $ err)
               Success Undo -> do (_, st) <- elabStep e loadState
                                  return (True, st, False, init prf, Right $ iPrintResult "")
               Success ProofState -> return (True, e, False, prf, Right $ iPrintResult "")
diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs
--- a/src/Idris/REPL.hs
+++ b/src/Idris/REPL.hs
@@ -80,7 +80,7 @@
 import Data.List (groupBy)
 import qualified Data.Text as T
 
-import Text.Trifecta.Result(Result(..))
+import Text.Trifecta.Result(Result(..), ErrInfo(..))
 
 import System.Console.Haskeline as H
 import System.FilePath
@@ -190,7 +190,7 @@
                  IO (IState, FilePath)
 processNetCmd orig i h fn cmd
     = do res <- case parseCmd i "(net)" cmd of
-                  Failure err -> return (Left (Msg " invalid command"))
+                  Failure (ErrInfo err _) -> return (Left (Msg " invalid command"))
                   Success (Right c) -> runExceptT $ evalStateT (processNet fn c) i
                   Success (Left err) -> return (Left (Msg err))
          case res of
@@ -307,7 +307,7 @@
   do c <- colourise
      i <- getIState
      case parseCmd i "(input)" cmd of
-       Failure err -> iPrintError $ show (fixColour False err)
+       Failure (ErrInfo err _) -> iPrintError $ show (fixColour False err)
        Success (Right (Prove mode n')) ->
          idrisCatch
            (do process fn (Prove mode n')
@@ -435,9 +435,9 @@
         splitPi :: IState -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
         splitPi ist (Bind n (Pi _ t _) rest) =
           let (hs, c, pc) = splitPi ist rest in
-            ((n, t, delabTy' ist [] t False False):hs,
-             c, delabTy' ist [] c False False)
-        splitPi ist tm = ([], tm, delabTy' ist [] tm False False)
+            ((n, t, delabTy' ist [] t False False True):hs,
+             c, delabTy' ist [] c False False True)
+        splitPi ist tm = ([], tm, delabTy' ist [] tm False False True)
 
         -- | Get the types of a list of metavariable names
         mvTys :: IState -> [Name] -> [(Name, Type)]
@@ -722,8 +722,8 @@
          let fn = fromMaybe "" (listToMaybe inputs)
          c <- colourise
          case parseCmd i "(input)" cmd of
-            Failure err ->   do iputStrLn $ show (fixColour c err)
-                                return (Just inputs)
+            Failure (ErrInfo err _) ->   do iputStrLn $ show (fixColour c err)
+                                            return (Just inputs)
             Success (Right Reload) ->
                 reload orig inputs
             Success (Right Watch) ->
@@ -1787,8 +1787,8 @@
                      mapM_ (\str -> do ist <- getIState
                                        c <- colourise
                                        case parseExpr ist str of
-                                         Failure err -> do iputStrLn $ show (fixColour c err)
-                                                           runIO $ exitWith (ExitFailure 1)
+                                         Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)
+                                                                       runIO $ exitWith (ExitFailure 1)
                                          Success e -> process "" (Eval e))
                            exprs
                      runIO exitSuccess
@@ -1843,8 +1843,8 @@
 execScript expr = do i <- getIState
                      c <- colourise
                      case parseExpr i expr of
-                          Failure err -> do iputStrLn $ show (fixColour c err)
-                                            runIO $ exitWith (ExitFailure 1)
+                          Failure (ErrInfo err _) -> do iputStrLn $ show (fixColour c err)
+                                                        runIO $ exitWith (ExitFailure 1)
                           Success term -> do ctxt <- getContext
                                              (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term
                                              res <- execute tm
@@ -1879,7 +1879,7 @@
                            runInit h
           processLine i cmd input clr =
               case parseCmd i input cmd of
-                   Failure err -> runIO $ print (fixColour clr err)
+                   Failure (ErrInfo err _) -> runIO $ print (fixColour clr err)
                    Success (Right Reload) -> iPrintError "Init scripts cannot reload the file"
                    Success (Right (Load f _)) -> iPrintError "Init scripts cannot load files"
                    Success (Right (ModImport f)) -> iPrintError "Init scripts cannot import modules"
diff --git a/src/Pkg/PParser.hs b/src/Pkg/PParser.hs
--- a/src/Pkg/PParser.hs
+++ b/src/Pkg/PParser.hs
@@ -59,6 +59,20 @@
 instance HasLastTokenSpan PParser where
   getLastTokenSpan = return Nothing
 
+#if MIN_VERSION_base(4,9,0)
+instance {-# OVERLAPPING #-} DeltaParsing PParser where
+  line = lift line
+  {-# INLINE line #-}
+  position = lift position
+  {-# INLINE position #-}
+  slicedWith f (StateT m) = StateT $ \s -> slicedWith (\(a,s') b -> (f a b, s')) $ m s
+  {-# INLINE slicedWith #-}
+  rend = lift rend
+  {-# INLINE rend #-}
+  restOfLine = lift restOfLine
+  {-# INLINE restOfLine #-}
+#endif
+
 #if MIN_VERSION_base(4,8,0)
 instance {-# OVERLAPPING #-} TokenParsing PParser where
 #else
@@ -71,7 +85,7 @@
 parseDesc fp = do
     p <- readFile fp
     case runparser pPkg defaultPkg fp p of
-      Failure err -> fail (show $ PP.plain err)
+      Failure (ErrInfo err _) -> fail (show $ PP.plain err)
       Success x -> return x
 
 pPkg :: PParser PkgDesc
diff --git a/src/Util/DynamicLinker.hs b/src/Util/DynamicLinker.hs
--- a/src/Util/DynamicLinker.hs
+++ b/src/Util/DynamicLinker.hs
@@ -5,7 +5,7 @@
 License     : BSD3
 Maintainer  : The Idris Community.
 -}
-{-# LANGUAGE ExistentialQuantification, CPP #-}
+{-# LANGUAGE ExistentialQuantification, CPP, ScopedTypeVariables #-}
 module Util.DynamicLinker ( ForeignFun(..)
                           , DynamicLib(..)
                           , tryLoadLib
@@ -17,8 +17,13 @@
 import Foreign.Ptr (Ptr(), nullPtr, FunPtr, nullFunPtr, castPtrToFunPtr)
 import System.Directory
 #ifndef mingw32_HOST_OS
+import Control.Exception (try, IOException, throwIO)
+import Data.Array (Array, inRange, bounds, (!))
+import Data.Functor ((<$>))
+import Data.Maybe (catMaybes)
 import System.Posix.DynamicLinker
 import System.FilePath.Posix ((</>))
+import Text.Regex.TDFA
 #else
 import qualified Control.Exception as Exception (catch, IOException)
 import System.Win32.DLL
@@ -69,13 +74,69 @@
                           return $ maybe (lib ++ "." ++ hostDynamicLibExt) id found
 
 #ifndef mingw32_HOST_OS
+-- Load a dynamic library on POSIX systems.
+-- In the simple case, we just find the appropriate filename and call dlopen().
+-- In the complicated case our "foo.so" isn't actually a library. Some of the
+-- .so files on modern Linux systems are linker scripts instead. dlopen()
+-- doesn't know anything about those. We need to look inside the script for the
+-- actual library path and load that. This is a horrible hack, the correct
+-- method would be to actually parse the scripts and execute them. The approach
+-- below is what GHC does.
 tryLoadLib :: [FilePath] -> String -> IO (Maybe DynamicLib)
-tryLoadLib dirs lib = do filename <- libFileName dirs lib
-                         handle <- dlopen filename [RTLD_NOW, RTLD_GLOBAL]
-                         if undl handle == nullPtr
-                           then return Nothing
-                           else return . Just $ Lib lib handle
+tryLoadLib dirs lib = do
+  filename <- libFileName dirs lib
+  res :: Either IOException DL <- try $
+    dlopen filename [RTLD_NOW, RTLD_GLOBAL]
+  mbDL <- case res of
+    Right handle -> return $ Just handle
+#ifdef linux_HOST_OS
+    Left ex ->
+      -- dlopen failed, run a regex to see if the error message looks like it
+      -- could be a linker script.
+      case matchAllText invalidLibRegex (show ex) of
+        (x:_) -> do
+          if inRange (bounds x) 1
+            then do
+              -- filename above may be a relative path. Get the full path out of
+              -- the error message.
+              let realPath = fst $ x ! 1
+              fileLines <- lines <$> readFile realPath
+              -- Go down the linker script line by line looking for .so
+              -- filenames and try each one.
+              let matches = catMaybes $ map
+                    (getLastMatch . matchAllText linkerScriptRegex)
+                    fileLines
+              mapMFirst (\f -> dlopen f [RTLD_NOW, RTLD_GLOBAL]) matches
+            else return Nothing
+        [] -> return Nothing
+#else
+    Left ex -> throwIO ex
+#endif
+  case mbDL of
+    Just handle -> if undl handle == nullPtr
+                   then return Nothing
+                   else return . Just $ Lib lib handle
+    Nothing     -> return Nothing
 
+getLastMatch :: [MatchText String] -> Maybe String
+getLastMatch [] = Nothing
+getLastMatch (x:_) = case bounds x of
+  (low, high) -> if low > high
+                 then Nothing
+                 else Just $ fst $ x ! high
+
+mapMFirst :: (a -> IO b) -> [a] -> IO (Maybe b)
+mapMFirst f []     = return Nothing
+mapMFirst f (a:as) = do res <- try (f a)
+                        case res of
+                          Left (ex :: IOException) -> mapMFirst f as
+                          Right res -> return $ Just res
+
+invalidLibRegex :: Regex
+invalidLibRegex = makeRegex "(([^ \t()])+\\.so([^ \t:()])*):([ \t])*(invalid ELF header|file too short)"
+
+linkerScriptRegex :: Regex
+linkerScriptRegex = makeRegex "(GROUP|INPUT) *\\( *([^ )]+)"
 
 tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun)
 tryLoadFn fn (Lib _ h) = do cFn <- dlsym h fn
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,7 +1,7 @@
-resolver: lts-5.11
+resolver: lts-6.5
 
 packages:
-  - '.'
+  - location: .
 
 flags:
   idris:
@@ -10,6 +10,7 @@
 
 extra-deps:
   - libffi-0.1
+  - trifecta-1.6
 
 nix:
   enable: false
diff --git a/test/docs004/docs004.idr b/test/docs004/docs004.idr
new file mode 100644
--- /dev/null
+++ b/test/docs004/docs004.idr
@@ -0,0 +1,11 @@
+module Main
+
+||| Some record Foo
+||| @a a type
+record Foo a where
+  ||| Constructor for Foo
+  constructor MkFoo
+  ||| A field bar
+  bar : Nat
+  ||| A field baz
+  baz : Bool
diff --git a/test/docs004/expected b/test/docs004/expected
new file mode 100644
--- /dev/null
+++ b/test/docs004/expected
@@ -0,0 +1,18 @@
+Main.MkFoo : (bar : Nat) -> (baz : Bool) -> Foo a
+    Constructor for Foo
+    Arguments:
+        (implicit) a : Type  -- a type
+        
+        bar : Nat  -- A field bar
+        
+        baz : Bool  -- A field baz
+        
+    The function is Total
+Main.Foo.bar : (rec : Foo a) -> Nat
+    A field bar
+    
+    The function is Total
+Main.Foo.baz : (rec : Foo a) -> Bool
+    A field baz
+    
+    The function is Total
diff --git a/test/docs004/input b/test/docs004/input
new file mode 100644
--- /dev/null
+++ b/test/docs004/input
@@ -0,0 +1,3 @@
+:doc MkFoo
+:doc bar
+:doc baz
diff --git a/test/docs004/run b/test/docs004/run
new file mode 100644
--- /dev/null
+++ b/test/docs004/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} --quiet --nocolor docs004.idr < input
+rm *.ibc
diff --git a/test/docs005/docs005.idr b/test/docs005/docs005.idr
new file mode 100644
--- /dev/null
+++ b/test/docs005/docs005.idr
@@ -0,0 +1,19 @@
+module docs005
+
+import Data.List
+
+%default total
+
+||| A foobar with an auto implicit
+data Foobar : Type where
+  ||| New Foo
+  |||
+  ||| @xs Some `xs`
+  ||| @ys Some `ys`
+  ||| @prf The prf
+  ||| @prf1 A prf
+  NewFoo : (xs : List String)
+        -> (ys : List Nat)
+        -> {prf1 : NonEmpty xs}
+        -> {auto prf : NonEmpty ys}
+        -> Foobar
diff --git a/test/docs005/expected b/test/docs005/expected
new file mode 100644
--- /dev/null
+++ b/test/docs005/expected
@@ -0,0 +1,29 @@
+Data type docs005.Foobar : Type
+    A foobar with an auto implicit
+    
+Constructors:
+    NewFoo : (xs : List String) ->
+        (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
+        New Foo
+        Arguments:
+            xs : List String  -- Some xs
+            
+            ys : List Nat  -- Some ys
+            
+            (implicit) prf1 : NonEmpty xs  -- A prf
+            
+            (auto implicit) prf : NonEmpty ys  -- The prf
+            
+docs005.NewFoo : (xs : List String) ->
+    (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
+    New Foo
+    Arguments:
+        xs : List String  -- Some xs
+        
+        ys : List Nat  -- Some ys
+        
+        (implicit) prf1 : NonEmpty xs  -- A prf
+        
+        (auto implicit) prf : NonEmpty ys  -- The prf
+        
+    The function is Total
diff --git a/test/docs005/input b/test/docs005/input
new file mode 100644
--- /dev/null
+++ b/test/docs005/input
@@ -0,0 +1,2 @@
+:doc Foobar
+:doc NewFoo
diff --git a/test/docs005/run b/test/docs005/run
new file mode 100644
--- /dev/null
+++ b/test/docs005/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} --quiet --nocolor docs005.idr < input
+rm *.ibc
diff --git a/test/effects001/test021.idr b/test/effects001/test021.idr
--- a/test/effects001/test021.idr
+++ b/test/effects001/test021.idr
@@ -8,27 +8,41 @@
 
 data Count : Type where
 
-FileIO : Type -> Type -> Type
-FileIO st t = Eff t [FILE_IO st, STDIO, Count ::: STATE Int]
 
-readFile : FileIO (OpenFile Read) (List String)
-readFile = readAcc [] where
-    readAcc : List String -> FileIO (OpenFile Read) (List String)
-    readAcc acc = do e <- eof
-                     if (not e)
-                        then do str <- readLine
-                                Count :- put (!(Count :- get) + 1)
-                                readAcc (str :: acc)
-                        else return (reverse acc)
-
-testFile : FileIO () ()
-testFile = do True <- open "testFile" Read  | False => putStrLn "Error!"
-              fcontents <- readFile
-              putStrLn (show fcontents)
-              close
-              putStrLn (show !(Count :- get))
+TestFileIO : Type -> Type -> Type
+TestFileIO st t = Eff t [FILE st, STDIO, Count ::: STATE Int]
 
-main : IO ()
-main = run testFile 
+readFileCount : Eff (FileOpResult (List String)) [FILE R, STDIO, Count ::: STATE Int]
+readFileCount = readAcc []
+  where
+    readAcc : List String
+           -> Eff (FileOpResult (List String)) [FILE R, STDIO, Count ::: STATE Int]
+    readAcc acc = do
+      e <- eof
+      if (not e)
+         then do
+           (Result str) <- readLine
+                         | (FError err) => pure (FError err)
+           Count :- put (!(Count :- get) + 1)
+           readAcc (str :: acc)
+         else do
+           let res = reverse acc
+           pure $ Result res
 
+testFile : TestFileIO () ()
+testFile = do
+    Success <- open "testFile" Read
+             | (FError err) => do
+                 putStrLn "Error!"
+                 pure ()
+    (Result fcontents) <- readFileCount
+                        | (FError err) => do
+                            close
+                            putStrLn "Error!"
+                            pure ()
+    putStrLn (show fcontents)
+    close
+    putStrLn (show !(Count :- get))
 
+main : IO ()
+main = run testFile
diff --git a/test/interfaces006/expected b/test/interfaces006/expected
new file mode 100644
--- /dev/null
+++ b/test/interfaces006/expected
diff --git a/test/interfaces006/interfaces006.idr b/test/interfaces006/interfaces006.idr
new file mode 100644
--- /dev/null
+++ b/test/interfaces006/interfaces006.idr
@@ -0,0 +1,19 @@
+module Categories
+
+infixr 9 .
+interface Category (c: k -> k -> Type) where
+  id: c x x
+  (.): c y z -> c x y -> c x z
+
+interface Category c => Functor (c: k -> k -> Type) (f: k -> k) where
+  map: c x y -> c (f x) (f y)
+
+infixr 1 =<<
+interface Functor c m => Monad (c: k -> k -> Type) (m: k -> k) where
+  return: c x (m x)
+  join: c (m (m x)) (m x)
+  (=<<) : c x (m y) -> c (m x) (m y)
+
+  join = (=<<) id
+  (=<<) f = join . map f
+
diff --git a/test/interfaces006/run b/test/interfaces006/run
new file mode 100644
--- /dev/null
+++ b/test/interfaces006/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces006.idr --noprelude --check
+rm -rf *.ibc
diff --git a/test/records004/expected b/test/records004/expected
new file mode 100644
--- /dev/null
+++ b/test/records004/expected
@@ -0,0 +1,3 @@
+"Fred"
+"Joe"
+"Bloggs"
diff --git a/test/records004/records004.idr b/test/records004/records004.idr
new file mode 100644
--- /dev/null
+++ b/test/records004/records004.idr
@@ -0,0 +1,13 @@
+-- Test for multiple field declarations on one line with the same type
+
+record Person where
+  constructor MkPerson
+  firstName, middleName, lastName : String
+
+fred : Person
+fred = MkPerson "Fred" "Joe" "Bloggs"
+
+main : IO ()
+main = do printLn (firstName fred)
+          printLn (middleName fred)
+          printLn (lastName fred)
diff --git a/test/records004/run b/test/records004/run
new file mode 100644
--- /dev/null
+++ b/test/records004/run
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ records004.idr -o records004
+./records004
+rm -f records004 *.ibc
diff --git a/test/records005/expected b/test/records005/expected
new file mode 100644
--- /dev/null
+++ b/test/records005/expected
@@ -0,0 +1,4 @@
+1/2
+Difficulty: 12
+0/0
+Difficulty: 12
diff --git a/test/records005/records005.idr b/test/records005/records005.idr
new file mode 100644
--- /dev/null
+++ b/test/records005/records005.idr
@@ -0,0 +1,39 @@
+record Score where
+       constructor MkScore
+       correct : Nat
+       attempted : Nat
+
+record GameState where
+       constructor MkGameState
+       score : Score
+       difficulty : Nat
+
+Show GameState where
+    show st = show (correct (score st)) ++ "/" 
+              ++ show (attempted (score st)) ++ "\n"
+              ++ "Difficulty: " ++ show (difficulty st)
+
+initState : GameState
+initState = MkGameState (MkScore 0 0) 12
+
+-- Test record update syntax
+
+correct : GameState -> GameState
+correct = record { score->correct $= (+1),
+                   score->attempted $= (+1) }
+
+wrong : GameState -> GameState
+wrong = record { score->attempted $= (+1) }
+
+restart : GameState -> GameState
+restart = record { score->attempted = 0,
+                   score->correct = 0 }
+
+
+main : IO ()
+main = do let st = initState
+          let st' = correct st
+          let st'' = wrong st'
+          printLn st''
+          printLn (restart st'')
+
diff --git a/test/records005/run b/test/records005/run
new file mode 100644
--- /dev/null
+++ b/test/records005/run
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ records005.idr -o records005
+./records005
+rm -f records005 *.ibc
diff --git a/test/runtest.hs b/test/runtest.hs
--- a/test/runtest.hs
+++ b/test/runtest.hs
@@ -130,6 +130,7 @@
     -- that depend on that distinction in other contexts.
     -- Also rewrite newlines for consistency.
        norm ('\r':'\n':xs) = '\n' : norm xs
+       norm ('\\':'\\':xs) = '/' : norm xs
        norm ('\\':xs) = '/' : norm xs
        norm (x : xs) = x : norm xs
        norm [] = []