From 52c103f018ab2b9783e3e6d9a9cb50d663d9484e Mon Sep 17 00:00:00 2001
From: Steven Shaw <steven@steshaw.org>
Date: Sun, 3 Sep 2017 15:04:08 +1000
Subject: [PATCH 01/27] Enable test interactive017.

---
 test/TestData.hs                       | 3 ++-
 test/interactive017/run                | 2 +-
 test/interactive017/shebang-args.idr   | 0
 test/interactive017/shebang-import.idr | 0
 test/interactive017/shebang-node.idr   | 0
 test/interactive017/shebang.idr        | 0
 6 files changed, 3 insertions(+), 2 deletions(-)
 mode change 100644 => 100755 test/interactive017/run
 mode change 100644 => 100755 test/interactive017/shebang-args.idr
 mode change 100644 => 100755 test/interactive017/shebang-import.idr
 mode change 100644 => 100755 test/interactive017/shebang-node.idr
 mode change 100644 => 100755 test/interactive017/shebang.idr

diff --git a/test/TestData.hs b/test/TestData.hs
index 29889d820..0e3d7521d 100644
--- a/test/TestData.hs
+++ b/test/TestData.hs
@@ -157,7 +157,8 @@ testFamiliesData = [
       ( 13, ANY  ),
       ( 14, C_CG ),
       ( 15, ANY  ),
-      ( 16, ANY  )]),
+      ( 16, ANY  ),
+      ( 17, ANY  )]),
   ("interfaces",      "Interfaces",
     [ (  1, ANY  ),
       (  2, ANY  ),
diff --git a/test/interactive017/run b/test/interactive017/run
old mode 100644
new mode 100755
index b0e3c3ad7..ae16ebf61
--- a/test/interactive017/run
+++ b/test/interactive017/run
@@ -6,4 +6,4 @@ PATH="../../scripts:$PATH"
 ./shebang-node.idr
 ./shebang-args.idr aaa
 ./shebang-args.idr bbb aaa
-./shebang-import.idr
\ No newline at end of file
+./shebang-import.idr
diff --git a/test/interactive017/shebang-args.idr b/test/interactive017/shebang-args.idr
old mode 100644
new mode 100755
diff --git a/test/interactive017/shebang-import.idr b/test/interactive017/shebang-import.idr
old mode 100644
new mode 100755
diff --git a/test/interactive017/shebang-node.idr b/test/interactive017/shebang-node.idr
old mode 100644
new mode 100755
diff --git a/test/interactive017/shebang.idr b/test/interactive017/shebang.idr
old mode 100644
new mode 100755

From f04722199188da57c4fd23bb0dde96907cf9f975 Mon Sep 17 00:00:00 2001
From: Steven Shaw <steven@steshaw.org>
Date: Mon, 4 Sep 2017 09:44:15 +1000
Subject: [PATCH 02/27] Add (broken) test case for "private functions"

---
 test/TestData.hs             |  3 ++-
 test/interactive018/Bar.idr  | 10 ++++++++++
 test/interactive018/Foo.idr  |  8 ++++++++
 test/interactive018/expected |  4 ++++
 test/interactive018/input    |  4 ++++
 test/interactive018/run      |  3 +++
 6 files changed, 31 insertions(+), 1 deletion(-)
 create mode 100644 test/interactive018/Bar.idr
 create mode 100644 test/interactive018/Foo.idr
 create mode 100644 test/interactive018/expected
 create mode 100644 test/interactive018/input
 create mode 100755 test/interactive018/run

diff --git a/test/TestData.hs b/test/TestData.hs
index 0e3d7521d..2b5f9383a 100644
--- a/test/TestData.hs
+++ b/test/TestData.hs
@@ -158,7 +158,8 @@ testFamiliesData = [
       ( 14, C_CG ),
       ( 15, ANY  ),
       ( 16, ANY  ),
-      ( 17, ANY  )]),
+      ( 17, ANY  ),
+      ( 18, ANY  )]),
   ("interfaces",      "Interfaces",
     [ (  1, ANY  ),
       (  2, ANY  ),
diff --git a/test/interactive018/Bar.idr b/test/interactive018/Bar.idr
new file mode 100644
index 000000000..e674b7ae6
--- /dev/null
+++ b/test/interactive018/Bar.idr
@@ -0,0 +1,10 @@
+module Bar
+
+import Foo
+
+bar_private : Nat -> Nat
+bar_private n = n
+
+export
+bar_visible : Nat -> Nat
+bar_visible n = n
diff --git a/test/interactive018/Foo.idr b/test/interactive018/Foo.idr
new file mode 100644
index 000000000..e7223cc17
--- /dev/null
+++ b/test/interactive018/Foo.idr
@@ -0,0 +1,8 @@
+module Foo
+
+foo_private : Nat -> Nat
+foo_private n = n
+
+export
+foo_visible : Nat -> Nat
+foo_visible n = n
diff --git a/test/interactive018/expected b/test/interactive018/expected
new file mode 100644
index 000000000..fc7601fa9
--- /dev/null
+++ b/test/interactive018/expected
@@ -0,0 +1,4 @@
+bar_private : Nat -> Nat
+bar_visible : Nat -> Nat
+No such variable foo_private
+foo_visible : Nat -> Nat
diff --git a/test/interactive018/input b/test/interactive018/input
new file mode 100644
index 000000000..c97886d21
--- /dev/null
+++ b/test/interactive018/input
@@ -0,0 +1,4 @@
+:t bar_private
+:t bar_visible
+:t foo_private
+:t foo_visible
diff --git a/test/interactive018/run b/test/interactive018/run
new file mode 100755
index 000000000..8903c2cb3
--- /dev/null
+++ b/test/interactive018/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ --quiet --port none Bar.idr < input
+rm -f *.ibc

From a1ac9a20562bf0fde4d07e76c489811de8b8bfdf Mon Sep 17 00:00:00 2001
From: Michael Morgan <morgan.michael@me.com>
Date: Mon, 4 Sep 2017 14:09:02 -0500
Subject: [PATCH 03/27] Text.Lexer: fix `reject` behavior at end-of-input

Previously, `reject` was implemented using `expect`, and inverting the
predicate used with `Pred`. This means that `reject` would fail if it's the
final lexer in the input, instead of succeeding like it should.

To fix this, the constructor `Expect` was renamed to `Lookahead`, with a new
boolean argument indicating positive or negative lookahead. This boolean is
processed in `scan`. Now, `reject` succeeds if the sub-lexer fails for any
reason, including end of input.
---
 libs/contrib/Text/Lexer.idr | 20 +++++++-------------
 1 file changed, 7 insertions(+), 13 deletions(-)

diff --git a/libs/contrib/Text/Lexer.idr b/libs/contrib/Text/Lexer.idr
index f5e6a4f16..c2817be85 100644
--- a/libs/contrib/Text/Lexer.idr
+++ b/libs/contrib/Text/Lexer.idr
@@ -9,7 +9,7 @@ export
 data Recognise : (consumes : Bool) -> Type where
      Empty : Recognise False
      Fail : Recognise c
-     Expect : Recognise c -> Recognise False
+     Lookahead : (positive : Bool) -> Recognise c -> Recognise False
      Pred : (Char -> Bool) -> Recognise True
      SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True
      SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)
@@ -47,18 +47,12 @@ fail = Fail
 ||| Positive lookahead. Never consumes input.
 export
 expect : Recognise c -> Recognise False
-expect = Expect
+expect = Lookahead True
 
 ||| Negative lookahead. Never consumes input.
 export
 reject : Recognise c -> Recognise False
-reject Empty            = Fail
-reject Fail             = Empty
-reject (Expect x)       = reject x
-reject (Pred f)         = Expect (Pred (not . f))
-reject (SeqEat r1 r2)   = reject r1 <|> Expect (SeqEat r1 (reject r2))
-reject (SeqEmpty r1 r2) = reject r1 <|> Expect (SeqEmpty r1 (reject r2))
-reject (Alt r1 r2)      = reject r1 <+> reject r2
+reject = Lookahead False
 
 ||| Recognise a specific character
 export
@@ -175,10 +169,10 @@ strTail start (MkStrLen str len)
 scan : Recognise c -> Nat -> StrLen -> Maybe Nat
 scan Empty idx str = pure idx
 scan Fail idx str = Nothing
-scan (Expect r) idx str
-    = case scan r idx str of
-           Just _  => pure idx
-           Nothing => Nothing
+scan (Lookahead positive r) idx str
+    = if isJust (scan r idx str) == positive
+         then Just idx
+         else Nothing
 scan (Pred f) idx str
     = do c <- strIndex str idx
          if f c

From 6739b011a6db9eee7b1947eafe80524633e33b6c Mon Sep 17 00:00:00 2001
From: Michael Morgan <morgan.michael@me.com>
Date: Mon, 4 Sep 2017 00:36:36 -0500
Subject: [PATCH 04/27] Text.Lexer: improve `choice`

Removed constraint requiring a non-empty list. Now, `choice` always
fails if the list is empty.
---
 libs/contrib/Text/Lexer.idr | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/libs/contrib/Text/Lexer.idr b/libs/contrib/Text/Lexer.idr
index f5e6a4f16..f93a202f1 100644
--- a/libs/contrib/Text/Lexer.idr
+++ b/libs/contrib/Text/Lexer.idr
@@ -113,11 +113,11 @@ export
 many : Lexer -> Recognise False
 many l = opt (some l)
 
-||| Recognise the first matching lexer from a non-empty list.
+||| Recognise the first matching lexer from a Foldable. Always consumes input
+||| if one of the options succeeds. Fails if the foldable is empty.
 export
-choice : (xs : List Lexer) -> {auto ok : NonEmpty xs} -> Lexer
-choice (x :: [])          = x
-choice (x :: xs@(_ :: _)) = x <|> choice xs
+choice : Foldable t => t Lexer -> Lexer
+choice xs = foldr Alt Fail xs
 
 ||| Recognise many instances of `l` until an instance of `end` is
 ||| encountered.

From d36f5e9a42e7a339aea39b02449f75aaab658f41 Mon Sep 17 00:00:00 2001
From: Michael Morgan <morgan.michael@me.com>
Date: Mon, 4 Sep 2017 00:36:51 -0500
Subject: [PATCH 05/27] Text.Lexer: add quantified lexer combinators

Add new combinators that allow for counted sub-lexer repetition.
This includes the combinators `atLeast`, `atMost`, `between`, and `exactly`.
---
 libs/contrib/Text/Lexer.idr | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/libs/contrib/Text/Lexer.idr b/libs/contrib/Text/Lexer.idr
index f93a202f1..427c6e13f 100644
--- a/libs/contrib/Text/Lexer.idr
+++ b/libs/contrib/Text/Lexer.idr
@@ -127,6 +127,34 @@ export
 manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
 manyTill l end = end <|> opt (l <+> manyTill l end)
 
+||| Recognise a sub-lexer at least `min` times. Consumes input unless
+||| min is zero.
+export
+atLeast : (min : Nat) -> (l : Lexer) -> Recognise (min > 0)
+atLeast Z l       = many l
+atLeast (S min) l = l <+> atLeast min l
+
+||| Recognise a sub-lexer at most `max` times. Not guaranteed to
+||| consume input.
+export
+atMost : (max : Nat) -> (l : Lexer) -> Recognise False
+atMost Z _     = Empty
+atMost (S k) l = atMost k l <+> opt l
+
+||| Recognise a sub-lexer repeated between `min` and `max` times. Fails
+||| if the inputs are out of order. Consumes input unless min is zero.
+export
+between : (min : Nat) -> (max : Nat) -> (l : Lexer) -> Recognise (min > 0)
+between Z max l           = atMost max l
+between (S min) Z _       = Fail
+between (S min) (S max) l = l <+> between min max l
+
+||| Recognise exactly `count` repeated occurrences of a sub-lexer.
+||| Consumes input unless count is zero.
+export
+exactly : (count : Nat) -> (l : Lexer) -> Recognise (count > 0)
+exactly n l = between n n l
+
 ||| Recognise any character
 export
 any : Lexer

From 5950e1e80a549f511119a52a2a6984659d273a27 Mon Sep 17 00:00:00 2001
From: Steven Shaw <steven@steshaw.org>
Date: Wed, 6 Sep 2017 18:38:54 +1000
Subject: [PATCH 06/27] Prevent private functions showing up in autocomplete
 and :t.

Fixes #1209.
---
 src/Idris/AbsSyntax.hs            |  5 ++--
 src/Idris/Completion.hs           | 16 +++++++----
 src/Idris/Core/Evaluate.hs        | 17 +++++++++---
 src/Idris/IBC.hs                  | 43 ++++++++++++++++-------------
 src/Idris/ModeCommon.hs           | 45 +++++++++++++++----------------
 src/Idris/Parser.hs               | 23 +++++-----------
 src/Idris/REPL.hs                 | 10 ++++---
 test/interactive018/Bar.idr       | 10 -------
 test/interactive018/Foo.idr       |  8 ------
 test/interactive018/Imported1.idr | 10 +++++++
 test/interactive018/Imported2.idr |  8 ++++++
 test/interactive018/Public1.idr   | 10 +++++++
 test/interactive018/Public2.idr   |  8 ++++++
 test/interactive018/Top.idr       | 11 ++++++++
 test/interactive018/expected      | 24 ++++++++++++++---
 test/interactive018/input         | 24 ++++++++++++++---
 test/interactive018/run           |  2 +-
 17 files changed, 173 insertions(+), 101 deletions(-)
 delete mode 100644 test/interactive018/Bar.idr
 delete mode 100644 test/interactive018/Foo.idr
 create mode 100644 test/interactive018/Imported1.idr
 create mode 100644 test/interactive018/Imported2.idr
 create mode 100644 test/interactive018/Public1.idr
 create mode 100644 test/interactive018/Public2.idr
 create mode 100644 test/interactive018/Top.idr

diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs
index bfd3520dd..866cc2b7d 100644
--- a/src/Idris/AbsSyntax.hs
+++ b/src/Idris/AbsSyntax.hs
@@ -7,6 +7,8 @@ Maintainer  : The Idris Community.
 -}
 
 {-# LANGUAGE DeriveFunctor, FlexibleContexts, PatternGuards #-}
+-- FIXME: {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# OPTIONS_GHC -fwarn-unused-imports #-}
 
 module Idris.AbsSyntax(
     module Idris.AbsSyntax
@@ -39,7 +41,6 @@ import System.IO.Error (tryIOError)
 
 import Data.Generics.Uniplate.Data (descend, descendM)
 
-import Debug.Trace
 import Util.DynamicLinker
 import Util.Pretty
 import Util.System
@@ -597,7 +598,7 @@ getHdrs :: Codegen -> Idris [String]
 getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
 
 getImported ::  Idris [(FilePath, Bool)]
-getImported = do i <- getIState; return (idris_imported i)
+getImported = idris_imported `fmap` getIState
 
 setErrSpan :: FC -> Idris ()
 setErrSpan x = do i <- getIState;
diff --git a/src/Idris/Completion.hs b/src/Idris/Completion.hs
index dadbf29e5..4093b151a 100644
--- a/src/Idris/Completion.hs
+++ b/src/Idris/Completion.hs
@@ -5,12 +5,16 @@ Copyright   :
 License     : BSD3
 Maintainer  : The Idris Community.
 -}
+
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# OPTIONS_GHC -fwarn-unused-imports #-}
+
 module Idris.Completion (replCompletion, proverCompletion) where
 
-import Idris.AbsSyntax (runIO)
+import Idris.AbsSyntax (runIO, getIState)
 import Idris.AbsSyntaxTree
 import Idris.Colours
-import Idris.Core.Evaluate (ctxtAlist, definitions)
+import Idris.Core.Evaluate (ctxtAlist, visibleDefinitions)
 import Idris.Core.TT
 import Idris.Help
 import Idris.Imports (installedPackages)
@@ -28,19 +32,21 @@ import qualified Data.Text as T
 import System.Console.ANSI (Color)
 import System.Console.Haskeline
 
+commands :: [String]
 commands = [ n | (names, _, _) <- allHelp ++ extraHelp, n <- names ]
 
 tacticArgs :: [(String, Maybe TacticArg)]
 tacticArgs = [ (name, args) | (names, args, _) <- Idris.Parser.Expr.tactics
                             , name <- names ]
+
+tactics :: [String]
 tactics = map fst tacticArgs
 
 -- | Get the user-visible names from the current interpreter state.
 names :: Idris [String]
-names = do i <- get
-           let ctxt = tt_ctxt i
+names = do ctxt <- tt_ctxt <$> getIState
            return $
-             mapMaybe nameString (allNames $ definitions ctxt) ++
+             mapMaybe nameString (allNames (visibleDefinitions ctxt)) ++
              "Type" : map fst Idris.Parser.Expr.constants
   where
     -- We need both fully qualified names and identifiers that map to them
diff --git a/src/Idris/Core/Evaluate.hs b/src/Idris/Core/Evaluate.hs
index 1f6acc8a3..5107f0aa9 100644
--- a/src/Idris/Core/Evaluate.hs
+++ b/src/Idris/Core/Evaluate.hs
@@ -5,9 +5,11 @@ Copyright   :
 License     : BSD3
 Maintainer  : The Idris Community.
 -}
+
 {-# LANGUAGE BangPatterns, DeriveGeneric, FlexibleInstances,
              MultiParamTypeClasses, PatternGuards #-}
 {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# OPTIONS_GHC -fwarn-unused-imports #-}
 
 module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
                 normaliseAll, normaliseBlocking, toValue, quoteTerm,
@@ -28,20 +30,19 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
                 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,
                 conGuarded,
                 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
+                visibleDefinitions,
                 isUniverse, linearCheck, linearCheckArg) where
 
 import Idris.Core.CaseTree
 import Idris.Core.TT
 
-import Control.Applicative hiding (Const)
 import Control.Monad.State
-import Data.Binary hiding (get, put)
-import qualified Data.Binary as B
 import Data.List
 import Data.Maybe (listToMaybe)
-import Debug.Trace
 import GHC.Generics (Generic)
 
+import qualified Data.Map.Strict as Map
+
 data EvalState = ES { limited :: [(Name, Int)],
                       nexthole :: Int,
                       blocking :: Bool }
@@ -1152,6 +1153,14 @@ conGuarded ctxt n tm = guarded n tm
           isConName f ctxt = any (guarded n) as
     guarded _ _ = False
 
+visibleDefinitions :: Context -> Ctxt TTDecl
+visibleDefinitions ctxt =
+  Map.filter (\m -> length m > 0) . Map.map onlyVisible . definitions $ ctxt
+  where
+    onlyVisible = Map.filter visible
+    visible (_def, _rigCount, _injectivity, accessibility, _totality, _metaInformation) =
+      accessibility `notElem` [Hidden, Private]
+
 lookupP :: Name -> Context -> [Term]
 lookupP = lookupP_all False False
 
diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs
index c4ef381d1..25cc4a300 100644
--- a/src/Idris/IBC.hs
+++ b/src/Idris/IBC.hs
@@ -5,20 +5,20 @@ Copyright   :
 License     : BSD3
 Maintainer  : The Idris Community.
 -}
+
 {-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
 {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# OPTIONS_GHC -fwarn-unused-imports #-}
 
 module Idris.IBC (loadIBC, loadPkgIndex,
                   writeIBC, writePkgIndex,
                   hasValidIBCVersion, IBCPhase(..)) where
 
 import Idris.AbsSyntax
-import Idris.Core.Binary
 import Idris.Core.CaseTree
 import Idris.Core.Evaluate
 import Idris.Core.TT
-import Idris.DeepSeq
-import Idris.Delaborate
+import Idris.DeepSeq ()
 import Idris.Docstrings (Docstring)
 import qualified Idris.Docstrings as D
 import Idris.Error
@@ -27,23 +27,15 @@ import Idris.Options
 import Idris.Output
 import IRTS.System (getIdrisLibDir)
 
-import Paths_idris
-
 import qualified Cheapskate.Types as CT
 import Codec.Archive.Zip
 import Control.DeepSeq
 import Control.Monad
-import Control.Monad.State.Strict hiding (get, put)
-import qualified Control.Monad.State.Strict as ST
 import Data.Binary
 import Data.ByteString.Lazy as B hiding (elem, length, map)
-import Data.Functor
 import Data.List as L
 import Data.Maybe (catMaybes)
 import qualified Data.Set as S
-import qualified Data.Text as T
-import Data.Vector.Binary
-import Debug.Trace
 import System.Directory
 import System.FilePath
 
@@ -131,7 +123,9 @@ loadIBC :: Bool -- ^ True = reexport, False = make everything private
         -> IBCPhase
         -> FilePath -> Idris ()
 loadIBC reexport phase fp
-           = do imps <- getImported
+           = do logIBC 1 $ "loadIBC (reexport, phase, fp)" ++ show (reexport, phase, fp)
+                imps <- getImported
+                logIBC 3 $ "loadIBC imps" ++ show imps
                 case lookup fp imps of
                     Nothing -> load True
                     Just p -> if (not p && reexport) then load False else return ()
@@ -517,13 +511,15 @@ processImports reexp phase fname ar = do
         ibcsd <- valIBCSubDir i
         ids <- rankedImportDirs fname
         putIState (i { imported = f : imported i })
-        let phase' = case phase of
-                         IBC_REPL _ -> IBC_REPL False
-                         p -> p
+        let (phase', reexp') = case phase of
+                         IBC_REPL True -> (IBC_REPL False, reexp)
+                         IBC_REPL False -> (IBC_Building, reexp && re)
+                         p -> (p, reexp && re)
         fp <- findIBC ids ibcsd f
+        logIBC 4 $ "processImports (fp, phase')" ++ show (fp, phase')
         case fp of
             Nothing -> do logIBC 2 $ "Failed to load ibc " ++ f
-            Just fn -> do loadIBC (reexp && re) phase' fn) fs
+            Just fn -> do loadIBC reexp' phase' fn) fs
 
 processImplicits :: Archive -> Idris ()
 processImplicits ar = do
@@ -639,6 +635,7 @@ processPatternDefs ar = do
 processDefs :: Archive -> Idris ()
 processDefs ar = do
         ds <- getEntry [] "ibc_defs" ar
+        logIBC 4 $ "processDefs ds" ++ show ds
         mapM_ (\ (n, d) -> do
             d' <- updateDef d
             case d' of
@@ -735,8 +732,11 @@ processAccess :: Bool -- ^ Reexporting?
            -> IBCPhase
            -> Archive -> Idris ()
 processAccess reexp phase ar = do
+    logIBC 3 $ "processAccess (reexp, phase)" ++ show (reexp, phase)
     ds <- getEntry [] "ibc_access" ar
+    logIBC 3 $ "processAccess ds" ++ show ds
     mapM_ (\ (n, a_in) -> do
+
         let a = if reexp then a_in else Hidden
         logIBC 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a
         updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) })
@@ -745,10 +745,15 @@ processAccess reexp phase ar = do
             then do
                 logIBC 2 $ "Not exporting " ++ show n
                 setAccessibility n Hidden
-            else logIBC 2 $ "Exporting " ++ show n
+            else
+                logIBC 2 $ "Exporting " ++ show n
+
         -- Everything should be available at the REPL from
-        -- things imported publicly
-        when (phase == IBC_REPL True) $ setAccessibility n Public) ds
+        -- things imported publicly.
+        when (phase == IBC_REPL True) $ do
+            logIBC 2 $ "Top level, exporting " ++ show n
+            setAccessibility n Public
+      ) ds
 
 processFlags :: Archive -> Idris ()
 processFlags ar = do
diff --git a/src/Idris/ModeCommon.hs b/src/Idris/ModeCommon.hs
index fbc3193b3..ca3f50ea3 100644
--- a/src/Idris/ModeCommon.hs
+++ b/src/Idris/ModeCommon.hs
@@ -4,6 +4,11 @@ Description : Common utilities used by all modes.
 License     : BSD3
 Maintainer  : The Idris Community.
 -}
+
+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# OPTIONS_GHC -fwarn-unused-binds #-}
+{-# OPTIONS_GHC -fwarn-unused-imports #-}
+
 module Idris.ModeCommon where
 
 import Idris.AbsSyntax
@@ -25,16 +30,11 @@ import Prelude hiding (id, (.), (<$>))
 import Control.Category
 import Control.DeepSeq
 import Control.Monad
-import Control.Monad.Trans.State.Strict (get)
-import Data.List hiding (group)
-import Data.Maybe
 import Network.Socket (PortNumber)
-import System.Directory
 
 defaultPort :: PortNumber
 defaultPort = fromIntegral 4294
 
-
 loadInputs :: [FilePath] -> Maybe Int -> Idris [FilePath]
 loadInputs inputs toline -- furthest line to read in input source files
   = idrisCatch
@@ -49,6 +49,8 @@ loadInputs inputs toline -- furthest line to read in input source files
                                [] -> not (NoREPL `elem` opts)
                                _ -> True
 
+           logParser 3 $ show "loadInputs loadCode" ++ show loadCode
+
            -- For each ifile list, check it and build ibcs in the same clean IState
            -- so that they don't interfere with each other when checking
 
@@ -59,6 +61,7 @@ loadInputs inputs toline -- furthest line to read in input source files
            let ninputs = zip [1..] inputs
            ifiles <- mapWhileOK (\(num, input) ->
                 do putIState ist
+                   logParser 3 $ show "loadInputs (num, input)" ++ show (num, input)
                    modTree <- buildTree
                                    (map snd (take (num-1) ninputs))
                                    importlists
@@ -77,9 +80,18 @@ loadInputs inputs toline -- furthest line to read in input source files
            case errSpan inew of
               Nothing ->
                 do putIState $!! ist { idris_tyinfodata = tidata }
-                   ibcfiles <- mapM findNewIBC (nub (concatMap snd ifiles))
---                    logLvl 0 $ "Loading from " ++ show ibcfiles
-                   tryLoad True (IBC_REPL True) (mapMaybe id ibcfiles)
+                   logParser 3 $ "loadInputs ifiles" ++ show ifiles
+
+                   let fileToIFileType :: FilePath -> Idris IFileType
+                       fileToIFileType file = do
+                         ibcsd <- valIBCSubDir ist
+                         ids <- rankedImportDirs file
+                         findImport ids ibcsd file
+
+                   ibcfiles <- mapM fileToIFileType inputs
+                   logParser 3 $ show "loadInputs ibcfiles" ++ show ibcfiles
+
+                   tryLoad True (IBC_REPL True) ibcfiles
               _ -> return ()
            exports <- findExports
 
@@ -103,6 +115,8 @@ loadInputs inputs toline -- furthest line to read in input source files
          tryLoad keepstate phase [] = warnTotality >> return ()
          tryLoad keepstate phase (f : fs)
                  = do ist <- getIState
+                      logParser 3 $ "tryLoad (keepstate, phase, f : fs)" ++
+                        show (keepstate, phase, f : fs)
                       let maxline
                             = case toline of
                                 Nothing -> Nothing
@@ -142,21 +156,6 @@ loadInputs inputs toline -- furthest line to read in input source files
          fmatch xs ('.':'/':ys) = fmatch xs ys
          fmatch xs ys = xs == ys
 
-         findNewIBC :: IFileType -> Idris (Maybe IFileType)
-         findNewIBC i@(IBC _ _) = return (Just i)
-         findNewIBC s@(IDR f) = do ist <- get
-                                   ibcsd <- valIBCSubDir ist
-                                   let ibc = ibcPathNoFallback ibcsd f
-                                   ok <- runIO $ doesFileExist ibc
-                                   if ok then return (Just (IBC ibc s))
-                                         else return Nothing
-         findNewIBC s@(LIDR f) = do ist <- get
-                                    ibcsd <- valIBCSubDir ist
-                                    let ibc = ibcPathNoFallback ibcsd f
-                                    ok <- runIO $ doesFileExist ibc
-                                    if ok then return (Just (IBC ibc s))
-                                          else return Nothing
-
          -- Like mapM, but give up when there's an error
          mapWhileOK f [] = return []
          mapWhileOK f (x : xs) = do x' <- f x
diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs
index c45267d5e..31ccc541a 100644
--- a/src/Idris/Parser.hs
+++ b/src/Idris/Parser.hs
@@ -5,9 +5,13 @@ Copyright   :
 License     : BSD3
 Maintainer  : The Idris Community.
 -}
+
 {-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,
              PatternGuards #-}
 {-# OPTIONS_GHC -O0 #-}
+-- FIXME: {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# OPTIONS_GHC -fwarn-unused-imports #-}
+
 module Idris.Parser(module Idris.Parser,
                     module Idris.Parser.Expr,
                     module Idris.Parser.Data,
@@ -17,11 +21,9 @@ module Idris.Parser(module Idris.Parser,
 import Idris.AbsSyntax hiding (namespace, params)
 import Idris.Core.Evaluate
 import Idris.Core.TT
-import Idris.Coverage
 import Idris.Delaborate
 import Idris.Docstrings hiding (Unchecked)
 import Idris.DSL
-import Idris.Elab.Term
 import Idris.Elab.Value
 import Idris.ElabDecls
 import Idris.Error
@@ -33,15 +35,11 @@ import Idris.Parser.Data
 import Idris.Parser.Expr
 import Idris.Parser.Helpers
 import Idris.Parser.Ops
-import Idris.Providers
 import Idris.Termination
 import Idris.Unlit
 
-import Util.DynamicLinker
 import qualified Util.Pretty as P
-import Util.System (readSource, writeSource)
-
-import Paths_idris
+import Util.System (readSource)
 
 import Prelude hiding (pi)
 
@@ -53,24 +51,14 @@ import Data.Char
 import Data.Foldable (asum)
 import Data.Function
 import Data.Generics.Uniplate.Data (descendM)
-import qualified Data.HashSet as HS
 import Data.List
 import qualified Data.List.Split as Spl
 import qualified Data.Map as M
 import Data.Maybe
-import Data.Monoid
 import Data.Ord
-import qualified Data.Set as S
 import qualified Data.Text as T
-import Debug.Trace
 import qualified System.Directory as Dir (makeAbsolute)
 import System.FilePath
-import System.IO
-import qualified Text.Parser.Char as Chr
-import Text.Parser.Expression
-import Text.Parser.LookAhead
-import qualified Text.Parser.Token as Tok
-import qualified Text.Parser.Token.Highlight as Hi
 import Text.PrettyPrint.ANSI.Leijen (Doc, plain)
 import qualified Text.PrettyPrint.ANSI.Leijen as ANSI
 import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,
@@ -1685,6 +1673,7 @@ loadModule' f phase
 loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()
 loadFromIFile reexp phase i@(IBC fn src) maxline
    = do logParser 1 $ "Skipping " ++ getSrcFile i
+        logParser 3 $ "loadFromIFile i" ++ show i
         idrisCatch (loadIBC reexp phase fn)
                 (\err -> ierror $ LoadingFailed fn err)
   where
diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs
index 62a334c73..faeae0909 100644
--- a/src/Idris/REPL.hs
+++ b/src/Idris/REPL.hs
@@ -6,6 +6,8 @@ Maintainer  : The Idris Community.
 -}
 
 {-# LANGUAGE FlexibleContexts, PatternGuards #-}
+-- FIXME: {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
+{-# OPTIONS_GHC -fwarn-unused-imports #-}
 
 module Idris.REPL
   ( idemodeStart
@@ -49,7 +51,6 @@ import Idris.Core.Execute (execute)
 import Idris.Core.TT
 import Idris.Core.Unify
 import Idris.Core.WHNF
-import Idris.Coverage
 import Idris.DataOpts
 import Idris.Delaborate
 import Idris.Docs
@@ -98,8 +99,6 @@ import Util.Pretty hiding ((</>))
 import Util.System
 import Version_idris (gitHash)
 
-import Debug.Trace
-
 -- | Run the REPL
 repl :: IState -- ^ The initial state
      -> [FilePath] -- ^ The loaded modules
@@ -981,7 +980,7 @@ process fn (Check (PRef _ _ n))
    = do ctxt <- getContext
         ist <- getIState
         let ppo = ppOptionIst ist
-        case lookupNames n ctxt of
+        case lookupVisibleNames n ctxt of
           ts@(t:_) ->
             case lookup t (idris_metavars ist) of
                 Just (_, i, _, _, _) -> iRenderResult . fmap (fancifyAnnots ist True) $
@@ -989,6 +988,9 @@ process fn (Check (PRef _ _ n))
                 Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)
           [] -> iPrintError $ "No such variable " ++ show n
   where
+    lookupVisibleNames :: Name -> Context -> [Name]
+    lookupVisibleNames n ctxt = map fst $ lookupCtxtName n (visibleDefinitions ctxt)
+
     showMetavarInfo ppo ist n i
          = case lookupTy n (tt_ctxt ist) of
                 (ty:_) -> let ty' = normaliseC (tt_ctxt ist) [] ty in
diff --git a/test/interactive018/Bar.idr b/test/interactive018/Bar.idr
deleted file mode 100644
index e674b7ae6..000000000
--- a/test/interactive018/Bar.idr
+++ /dev/null
@@ -1,10 +0,0 @@
-module Bar
-
-import Foo
-
-bar_private : Nat -> Nat
-bar_private n = n
-
-export
-bar_visible : Nat -> Nat
-bar_visible n = n
diff --git a/test/interactive018/Foo.idr b/test/interactive018/Foo.idr
deleted file mode 100644
index e7223cc17..000000000
--- a/test/interactive018/Foo.idr
+++ /dev/null
@@ -1,8 +0,0 @@
-module Foo
-
-foo_private : Nat -> Nat
-foo_private n = n
-
-export
-foo_visible : Nat -> Nat
-foo_visible n = n
diff --git a/test/interactive018/Imported1.idr b/test/interactive018/Imported1.idr
new file mode 100644
index 000000000..7fddb0455
--- /dev/null
+++ b/test/interactive018/Imported1.idr
@@ -0,0 +1,10 @@
+module Imported1
+
+import Imported2
+
+imported1_private : a -> a
+imported1_private a = a
+
+export
+imported1_visible : a -> a
+imported1_visible a = a
diff --git a/test/interactive018/Imported2.idr b/test/interactive018/Imported2.idr
new file mode 100644
index 000000000..411825967
--- /dev/null
+++ b/test/interactive018/Imported2.idr
@@ -0,0 +1,8 @@
+module Imported1
+
+imported2_private : a -> a
+imported2_private a = a
+
+export
+imported2_visible : a -> a
+imported2_visible a = a
diff --git a/test/interactive018/Public1.idr b/test/interactive018/Public1.idr
new file mode 100644
index 000000000..d26d356d0
--- /dev/null
+++ b/test/interactive018/Public1.idr
@@ -0,0 +1,10 @@
+module Public1
+
+import public Public2
+
+public1_private : a -> a
+public1_private a = a
+
+export
+public1_visible : a -> a
+public1_visible a = a
diff --git a/test/interactive018/Public2.idr b/test/interactive018/Public2.idr
new file mode 100644
index 000000000..a42bbc06a
--- /dev/null
+++ b/test/interactive018/Public2.idr
@@ -0,0 +1,8 @@
+module Public2
+
+public2_private : a -> a
+public2_private a = a
+
+export
+public2_visible : a -> a
+public2_visible a = a
diff --git a/test/interactive018/Top.idr b/test/interactive018/Top.idr
new file mode 100644
index 000000000..684b1f134
--- /dev/null
+++ b/test/interactive018/Top.idr
@@ -0,0 +1,11 @@
+module Top
+
+import Imported1
+import public Public1
+
+top_private : a -> a
+top_private a = a
+
+export
+top_visible : a -> a
+top_visible a = a
diff --git a/test/interactive018/expected b/test/interactive018/expected
index fc7601fa9..6f77ba822 100644
--- a/test/interactive018/expected
+++ b/test/interactive018/expected
@@ -1,4 +1,20 @@
-bar_private : Nat -> Nat
-bar_visible : Nat -> Nat
-No such variable foo_private
-foo_visible : Nat -> Nat
+1 : Integer
+top_private : a -> a
+1 : Integer
+top_visible : a -> a
+No such variable imported1_private
+No such variable imported1_private
+1 : Integer
+imported1_visible : a -> a
+No such variable imported2_private
+No such variable imported2_private
+No such variable imported2_visible
+No such variable imported2_visible
+No such variable public1_private
+No such variable public1_private
+1 : Integer
+public1_visible : a -> a
+No such variable public2_private
+No such variable public2_private
+1 : Integer
+public2_visible : a -> a
diff --git a/test/interactive018/input b/test/interactive018/input
index c97886d21..3919f99d7 100644
--- a/test/interactive018/input
+++ b/test/interactive018/input
@@ -1,4 +1,20 @@
-:t bar_private
-:t bar_visible
-:t foo_private
-:t foo_visible
+top_private 1
+:t top_private
+top_visible 1
+:t top_visible
+imported1_private 1
+:t imported1_private
+imported1_visible 1
+:t imported1_visible
+imported2_private 1
+:t imported2_private
+imported2_visible 1
+:t imported2_visible
+public1_private 1
+:t public1_private
+public1_visible 1
+:t public1_visible
+public2_private 1
+:t public2_private
+public2_visible 1
+:t public2_visible
diff --git a/test/interactive018/run b/test/interactive018/run
index 8903c2cb3..83f327611 100755
--- a/test/interactive018/run
+++ b/test/interactive018/run
@@ -1,3 +1,3 @@
 #!/usr/bin/env bash
-${IDRIS:-idris} $@ --quiet --port none Bar.idr < input
+${IDRIS:-idris} $@ --quiet --port none Top.idr < input
 rm -f *.ibc

From 6e66041f5a364e2039136d574a5570432a483ce5 Mon Sep 17 00:00:00 2001
From: Steven Shaw <steven@steshaw.org>
Date: Wed, 6 Sep 2017 20:28:34 +1000
Subject: [PATCH 07/27] Tweak for stylish-haskell

---
 src/Idris/Completion.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Idris/Completion.hs b/src/Idris/Completion.hs
index 4093b151a..45845d906 100644
--- a/src/Idris/Completion.hs
+++ b/src/Idris/Completion.hs
@@ -11,7 +11,7 @@ Maintainer  : The Idris Community.
 
 module Idris.Completion (replCompletion, proverCompletion) where
 
-import Idris.AbsSyntax (runIO, getIState)
+import Idris.AbsSyntax (getIState, runIO)
 import Idris.AbsSyntaxTree
 import Idris.Colours
 import Idris.Core.Evaluate (ctxtAlist, visibleDefinitions)

From 1f1155ca2894567be8a4d5defafd9bb8aaf4f988 Mon Sep 17 00:00:00 2001
From: Steven Shaw <steven@steshaw.org>
Date: Wed, 6 Sep 2017 20:41:22 +1000
Subject: [PATCH 08/27] Disable interactive017 (again).

See https://github.com/idris-lang/Idris-dev/pull/4046#issuecomment-326910042
---
 test/TestData.hs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/test/TestData.hs b/test/TestData.hs
index 2b5f9383a..49cabb668 100644
--- a/test/TestData.hs
+++ b/test/TestData.hs
@@ -158,7 +158,9 @@ testFamiliesData = [
       ( 14, C_CG ),
       ( 15, ANY  ),
       ( 16, ANY  ),
-      ( 17, ANY  ),
+-- FIXME: Re-enable interactive017 once it works with and without node.
+-- FIXME: See https://github.com/idris-lang/Idris-dev/pull/4046#issuecomment-326910042
+--      ( 17, ANY  ),
       ( 18, ANY  )]),
   ("interfaces",      "Interfaces",
     [ (  1, ANY  ),

From 3559deb004894b32b70b896a9fb6c6945ff9cff6 Mon Sep 17 00:00:00 2001
From: Michael Morgan <morgan.michael@me.com>
Date: Wed, 6 Sep 2017 13:53:21 -0500
Subject: [PATCH 09/27] Text.Parser: implement `Functor (Grammar tok c)`

Also included:

* Operators `(<*>)`, `(<*)`, `(*>)`, analogous to those defined by
  the `Applicative` interface.

* The functions `join` and `choice`, which resemble `Prelude.Monad.join`
  and `Prelude.Applicative.choice`.
---
 libs/contrib/Text/Parser.idr | 61 ++++++++++++++++++++++++++++++++++--
 1 file changed, 59 insertions(+), 2 deletions(-)

diff --git a/libs/contrib/Text/Parser.idr b/libs/contrib/Text/Parser.idr
index 92d64e4f1..640f7c24e 100644
--- a/libs/contrib/Text/Parser.idr
+++ b/libs/contrib/Text/Parser.idr
@@ -40,18 +40,72 @@ inf False t = t
 ||| consumed and therefore the input is smaller)
 export %inline
 (>>=) : {c1 : Bool} ->
-        Grammar tok c1 a -> inf c1 (a -> Grammar tok c2 b) ->
+        Grammar tok c1 a ->
+        inf c1 (a -> Grammar tok c2 b) ->
         Grammar tok (c1 || c2) b
 (>>=) {c1 = False} = SeqEmpty
 (>>=) {c1 = True} = SeqEat
 
+||| Sequence a grammar followed by the grammar it returns.
+export
+join : {c1 : Bool} ->
+       Grammar tok c1 (Grammar tok c2 a) ->
+       Grammar tok (c1 || c2) a
+join {c1 = False} p = SeqEmpty p id
+join {c1 = True} p = SeqEat p id
+
 ||| Give two alternative grammars. If both consume, the combination is
 ||| guaranteed to consume.
 export
-(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->
+(<|>) : Grammar tok c1 ty ->
+        Grammar tok c2 ty ->
         Grammar tok (c1 && c2) ty
 (<|>) = Alt
 
+||| Allows the result of a grammar to be mapped to a different value.
+export
+Functor (Grammar tok c) where
+  map f (Empty val)  = Empty (f val)
+  map f (Fail msg)   = Fail msg
+  map f (Terminal g) = Terminal (\t => map f (g t))
+  map f (Alt x y)    = Alt (map f x) (map f y)
+  map f (SeqEat act next)
+      = SeqEat act (\val => map f (next val))
+  map f (SeqEmpty act next)
+      = SeqEmpty act (\val => map f (next val))
+  -- The remaining constructors (NextIs, EOF, Commit) have a fixed type,
+  -- so a sequence must be used.
+  map {c = False} f p = SeqEmpty p (Empty . f)
+
+||| Sequence a grammar with value type `a -> b` and a grammar
+||| with value type `a`. If both succeed, apply the function
+||| from the first grammar to the value from the second grammar.
+||| Guaranteed to consume if either grammar consumes.
+export
+(<*>) : {c1 : Bool} ->
+        Grammar tok c1 (a -> b) ->
+        inf c1 (Grammar tok c2 a) ->
+        Grammar tok (c1 || c2) b
+(<*>) {c1 = False} x y = SeqEmpty x (\f => map f y)
+(<*>) {c1 = True} x y = SeqEat x (\f => map f y)
+
+||| Sequence two grammars. If both succeed, use the value of the first one.
+||| Guaranteed to consume if either grammar consumes.
+export
+(<*) : Grammar tok c1 a ->
+       inf c1 (Grammar tok c2 b) ->
+       Grammar tok (c1 || c2) a
+(<*) x y = map const x <*> y
+
+||| Sequence two grammars. If both succeed, use the value of the second one.
+||| Guaranteed to consume if either grammar consumes.
+export
+(*>) : Grammar tok c1 a ->
+       inf c1 (Grammar tok c2 b) ->
+       Grammar tok (c1 || c2) b
+(*>) x y = map (const id) x <*> y
+
+||| Always succeed with the given value.
 export
 pure : (val : ty) -> Grammar tok False ty
 pure = Empty
@@ -226,6 +280,9 @@ optional : Grammar tok True a -> (ifNothing : a) ->
            Grammar tok False a
 optional p def = p <|> pure def
 
+||| Fold over a list of grammars until the first one succeeds.
+choice : Foldable t => t (Grammar tok True a) -> Grammar tok True a
+choice xs = foldr Alt (Fail "No more options") xs
 
 ||| Parse an instance of `p` that is between `left` and `right`.
 export

From 0482a74fe08c7cd7e1f63abbd012e133e1e62cc5 Mon Sep 17 00:00:00 2001
From: Michael Morgan <morgan.michael@me.com>
Date: Wed, 6 Sep 2017 17:45:32 -0500
Subject: [PATCH 10/27] Text.Lexer: refactoring

---
 libs/contrib/Text/Lexer.idr | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/libs/contrib/Text/Lexer.idr b/libs/contrib/Text/Lexer.idr
index f5e6a4f16..cfb0a7e98 100644
--- a/libs/contrib/Text/Lexer.idr
+++ b/libs/contrib/Text/Lexer.idr
@@ -220,7 +220,7 @@ digits = some digit
 ||| Recognise a single hexidecimal digit
 export
 hexDigit : Lexer
-hexDigit = digit <|> oneOf "abcdefABCDEF"
+hexDigit = pred isHexDigit
 
 ||| Recognise one or more hexidecimal digits
 export
@@ -325,7 +325,7 @@ intLit = opt (is '-') <+> digits
 ||| Recognise a hexidecimal literal, prefixed by "0x" or "0X"
 export
 hexLit : Lexer
-hexLit = is '0' <+> oneOf "xX" <+> hexDigits
+hexLit = approx "0x" <+> hexDigits
 
 ||| A mapping from lexers to the tokens they produce.
 ||| This is a list of pairs `(Lexer, String -> tokenType)`

From 82a82ab758d684e8d3447353d51f9571ba539b29 Mon Sep 17 00:00:00 2001
From: Michael Morgan <morgan.michael@me.com>
Date: Sat, 2 Sep 2017 17:50:36 -0500
Subject: [PATCH 11/27] Text.Lexer: fix behavior of `surround`

`manyTill` is a `Recognise False`. It will recognise either nothing,
or any number of `l` followed by an `end`. This makes it unsuited for
`surround`, because the end character is required.
---
 libs/contrib/Text/Lexer.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/libs/contrib/Text/Lexer.idr b/libs/contrib/Text/Lexer.idr
index cfb0a7e98..f06ddc120 100644
--- a/libs/contrib/Text/Lexer.idr
+++ b/libs/contrib/Text/Lexer.idr
@@ -291,7 +291,7 @@ symbols = some symbol
 ||| delimiting lexers
 export
 surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
-surround start end l = start <+> manyTill l end
+surround start end l = start <+> many (reject end <+> l) <+> end
 
 ||| Recognise zero or more occurrences of a sub-lexer surrounded
 ||| by the same quote lexer on both sides (useful for strings)

From 7e604f86fa0691e5c66f227ea0836aeb55d7792e Mon Sep 17 00:00:00 2001
From: Michael Morgan <morgan.michael@me.com>
Date: Sat, 2 Sep 2017 20:53:51 -0500
Subject: [PATCH 12/27] Text.Lexer: add `manyUntil` and `manyThen`

These new functions utilise lookahead to non-greedily consume a
sub-lexer until an endpoint lexer is recognised.

`manyUntil` does not consume the end lexer, and `manyThen` does.
---
 libs/contrib/Text/Lexer.idr | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/libs/contrib/Text/Lexer.idr b/libs/contrib/Text/Lexer.idr
index f06ddc120..9a35a6525 100644
--- a/libs/contrib/Text/Lexer.idr
+++ b/libs/contrib/Text/Lexer.idr
@@ -119,6 +119,20 @@ choice : (xs : List Lexer) -> {auto ok : NonEmpty xs} -> Lexer
 choice (x :: [])          = x
 choice (x :: xs@(_ :: _)) = x <|> choice xs
 
+||| Repeat the sub-lexer `l` zero or more times until the lexer
+||| `stopBefore` is encountered. `stopBefore` will not be consumed.
+||| Not guaranteed to consume input.
+export
+manyUntil : (stopBefore : Recognise c) -> (l : Lexer) -> Recognise False
+manyUntil stopBefore l = many (reject stopBefore <+> l)
+
+||| Repeat the sub-lexer `l` zero or more times until the lexer
+||| `stopAfter` is encountered, and consume it. Guaranteed to
+||| consume if `stopAfter` consumes.
+export
+manyThen : (stopAfter : Recognise c) -> (l : Lexer) -> Recognise c
+manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter
+
 ||| Recognise many instances of `l` until an instance of `end` is
 ||| encountered.
 |||
@@ -291,7 +305,7 @@ symbols = some symbol
 ||| delimiting lexers
 export
 surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
-surround start end l = start <+> many (reject end <+> l) <+> end
+surround start end l = start <+> manyThen end l
 
 ||| Recognise zero or more occurrences of a sub-lexer surrounded
 ||| by the same quote lexer on both sides (useful for strings)

From 7c2148d88ae5439f9cb146e8ce6a78aeb3017c22 Mon Sep 17 00:00:00 2001
From: Michael Morgan <morgan.michael@me.com>
Date: Sun, 3 Sep 2017 12:57:24 -0500
Subject: [PATCH 13/27] Text.Lexer: add newline and comment lexers

Adds `newline`, `newlines`. They recognise "\r\n", "\r", or "\n" as a newline.

Adds `blockComment` and `lineComment`.
---
 libs/contrib/Text/Lexer.idr | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/libs/contrib/Text/Lexer.idr b/libs/contrib/Text/Lexer.idr
index 9a35a6525..8905349cd 100644
--- a/libs/contrib/Text/Lexer.idr
+++ b/libs/contrib/Text/Lexer.idr
@@ -291,6 +291,17 @@ export
 spaces : Lexer
 spaces = some space
 
+||| Recognise a single newline sequence. Understands CRLF, CR, and LF
+export
+newline : Lexer
+newline = let crlf = "\r\n" in
+              exact crlf <|> oneOf crlf
+
+||| Recognise one or more newline sequences. Understands CRLF, CR, and LF
+export
+newlines : Lexer
+newlines = some newline
+
 ||| Recognise a single non-whitespace, non-alphanumeric character
 export
 symbol : Lexer
@@ -341,6 +352,25 @@ export
 hexLit : Lexer
 hexLit = approx "0x" <+> hexDigits
 
+||| Recognise `start`, then recognise all input until a newline is encountered,
+||| and consume the newline. Will succeed if end-of-input is encountered before
+||| a newline.
+export
+lineComment : (start : Lexer) -> Lexer
+lineComment start = start <+> manyUntil newline any <+> opt newline
+
+||| Recognise all input between `start` and `end` lexers.
+||| Supports balanced nesting.
+|||
+||| For block comments that don't support nesting (such as C-style comments),
+||| use `surround`.
+export
+blockComment : (start : Lexer) -> (end : Lexer) -> Lexer
+blockComment start end = start <+> middle <+> end
+  where
+    middle : Recognise False
+    middle = manyUntil end (blockComment start end <|> any)
+
 ||| A mapping from lexers to the tokens they produce.
 ||| This is a list of pairs `(Lexer, String -> tokenType)`
 ||| For each Lexer in the list, if a substring in the input matches, run

From 828de62b7a6a5d2ef2aa5e74faa11c5b53202d21 Mon Sep 17 00:00:00 2001
From: Michael Morgan <morgan.michael@me.com>
Date: Sat, 2 Sep 2017 21:00:16 -0500
Subject: [PATCH 14/27] Text.Lexer: deprecate `manyTill`

There is no exact replacement, but the behavior of `manyTill` is
inconsistent with what's expected from a lexer library that supports
lookahead. It consumes its terminator, but it's okay if it never sees
its terminator and the input ends instead.
---
 libs/contrib/Text/Lexer.idr | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/libs/contrib/Text/Lexer.idr b/libs/contrib/Text/Lexer.idr
index 8905349cd..7bce15a69 100644
--- a/libs/contrib/Text/Lexer.idr
+++ b/libs/contrib/Text/Lexer.idr
@@ -140,6 +140,8 @@ manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter
 export
 manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
 manyTill l end = end <|> opt (l <+> manyTill l end)
+%deprecate manyTill
+    "Prefer `lineComment`, or `manyUntil`/`manyThen` (argument order is flipped)."
 
 ||| Recognise any character
 export

From 8f6f9af5545c55eadad77b051a4fd255a94b3bc7 Mon Sep 17 00:00:00 2001
From: Steven Shaw <steven@steshaw.org>
Date: Fri, 8 Sep 2017 19:27:16 +1000
Subject: [PATCH 15/27] Code style tweak

---
 src/Idris/Completion.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Idris/Completion.hs b/src/Idris/Completion.hs
index 45845d906..d819f60f3 100644
--- a/src/Idris/Completion.hs
+++ b/src/Idris/Completion.hs
@@ -46,7 +46,7 @@ tactics = map fst tacticArgs
 names :: Idris [String]
 names = do ctxt <- tt_ctxt <$> getIState
            return $
-             mapMaybe nameString (allNames (visibleDefinitions ctxt)) ++
+             mapMaybe nameString (allNames $ visibleDefinitions ctxt) ++
              "Type" : map fst Idris.Parser.Expr.constants
   where
     -- We need both fully qualified names and identifiers that map to them

From 319166c1b30def0991c535f91757a42e2a75f15e Mon Sep 17 00:00:00 2001
From: Steven Shaw <steven@steshaw.org>
Date: Fri, 8 Sep 2017 19:46:34 +1000
Subject: [PATCH 16/27] Improve interactive018.

Have the visible definitions refer to the private definitions to give
more confidence that evaluation doesn't get stuck.
---
 test/interactive018/Imported1.idr | 4 ++--
 test/interactive018/Public1.idr   | 2 +-
 test/interactive018/Public2.idr   | 2 +-
 test/interactive018/Top.idr       | 4 ++--
 4 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/test/interactive018/Imported1.idr b/test/interactive018/Imported1.idr
index 7fddb0455..054998539 100644
--- a/test/interactive018/Imported1.idr
+++ b/test/interactive018/Imported1.idr
@@ -3,8 +3,8 @@ module Imported1
 import Imported2
 
 imported1_private : a -> a
-imported1_private a = a
+imported1_private = imported2_visible
 
 export
 imported1_visible : a -> a
-imported1_visible a = a
+imported1_visible = imported1_private
diff --git a/test/interactive018/Public1.idr b/test/interactive018/Public1.idr
index d26d356d0..53408339e 100644
--- a/test/interactive018/Public1.idr
+++ b/test/interactive018/Public1.idr
@@ -7,4 +7,4 @@ public1_private a = a
 
 export
 public1_visible : a -> a
-public1_visible a = a
+public1_visible = public1_private
diff --git a/test/interactive018/Public2.idr b/test/interactive018/Public2.idr
index a42bbc06a..22cd08ec1 100644
--- a/test/interactive018/Public2.idr
+++ b/test/interactive018/Public2.idr
@@ -5,4 +5,4 @@ public2_private a = a
 
 export
 public2_visible : a -> a
-public2_visible a = a
+public2_visible = public2_private
diff --git a/test/interactive018/Top.idr b/test/interactive018/Top.idr
index 684b1f134..21c14dd56 100644
--- a/test/interactive018/Top.idr
+++ b/test/interactive018/Top.idr
@@ -4,8 +4,8 @@ import Imported1
 import public Public1
 
 top_private : a -> a
-top_private a = a
+top_private = imported1_visible
 
 export
 top_visible : a -> a
-top_visible a = a
+top_visible = public2_visible

From 20236a988acf91dca68adfed6904b48c28e76c58 Mon Sep 17 00:00:00 2001
From: Steven Shaw <steven@steshaw.org>
Date: Fri, 8 Sep 2017 19:48:27 +1000
Subject: [PATCH 17/27] Remove FIXME.

It indicated that trying to turn on `-fwarn-incomplete-patterns` failed.
---
 src/Idris/AbsSyntax.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs
index 866cc2b7d..71c74a3c9 100644
--- a/src/Idris/AbsSyntax.hs
+++ b/src/Idris/AbsSyntax.hs
@@ -7,7 +7,6 @@ Maintainer  : The Idris Community.
 -}
 
 {-# LANGUAGE DeriveFunctor, FlexibleContexts, PatternGuards #-}
--- FIXME: {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
 {-# OPTIONS_GHC -fwarn-unused-imports #-}
 
 module Idris.AbsSyntax(

From b571e631df85a7e99e58db7f5a4defdcee02f573 Mon Sep 17 00:00:00 2001
From: Steven Shaw <steven@steshaw.org>
Date: Fri, 8 Sep 2017 19:59:22 +1000
Subject: [PATCH 18/27] Tweak coding style.

Dangling/hanging case.
---
 src/Idris/IBC.hs | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs
index 25cc4a300..3207c8a00 100644
--- a/src/Idris/IBC.hs
+++ b/src/Idris/IBC.hs
@@ -511,10 +511,11 @@ processImports reexp phase fname ar = do
         ibcsd <- valIBCSubDir i
         ids <- rankedImportDirs fname
         putIState (i { imported = f : imported i })
-        let (phase', reexp') = case phase of
-                         IBC_REPL True -> (IBC_REPL False, reexp)
-                         IBC_REPL False -> (IBC_Building, reexp && re)
-                         p -> (p, reexp && re)
+        let (phase', reexp') =
+              case phase of
+                IBC_REPL True -> (IBC_REPL False, reexp)
+                IBC_REPL False -> (IBC_Building, reexp && re)
+                p -> (p, reexp && re)
         fp <- findIBC ids ibcsd f
         logIBC 4 $ "processImports (fp, phase')" ++ show (fp, phase')
         case fp of

From f436c5ffb32dfda19b41f0cbf8049e46e62d7093 Mon Sep 17 00:00:00 2001
From: Jason Felice <jason.m.felice@gmail.com>
Date: Wed, 13 Sep 2017 10:35:45 -0400
Subject: [PATCH 19/27] Expose `@` patterns to where functions (#4057)

* Pass whereblock to desugarAs

* Bind @ variables in where clauses

* @ patterns don't shadow where-functions' lhs-bound names

* m@... doesn't shadow lhs vars in nested where block

* Simplify bindPats

* Rename for clarity

* Test case for doubly-nested @ pattern

* Update CHANGELOG.md
---
 CHANGELOG.md               |  3 +++
 src/Idris/Elab/AsPat.hs    | 30 +++++++++++++++++++--------
 src/Idris/Elab/Clause.hs   |  4 ++--
 test/TestData.hs           |  3 ++-
 test/basic020/basic020.idr | 42 ++++++++++++++++++++++++++++++++++++++
 test/basic020/expected     |  1 +
 test/basic020/run          |  4 ++++
 7 files changed, 75 insertions(+), 12 deletions(-)
 create mode 100644 test/basic020/basic020.idr
 create mode 100644 test/basic020/expected
 create mode 100755 test/basic020/run

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3f58b7353..753170cc2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,6 +2,9 @@
 
 + Addition of `Text.Literate`, a module for working with literate
   source files.
++ In `@`-patterns such as `x@p`, `x` is now in scope on the right-hand side
+  of any definitions in `where` clauses, provided the left-hand side of the
+  definition does not shadow it.
 
 # New in 1.1.1
 
diff --git a/src/Idris/Elab/AsPat.hs b/src/Idris/Elab/AsPat.hs
index 43b8411f2..eb85f54e3 100644
--- a/src/Idris/Elab/AsPat.hs
+++ b/src/Idris/Elab/AsPat.hs
@@ -12,18 +12,30 @@ import Idris.Core.TT
 
 import Control.Applicative
 import Control.Monad.State.Strict
-import Data.Generics.Uniplate.Data (transformM)
+import Data.Generics.Uniplate.Data (transformM, universe)
 
 -- | Desugar by changing x@y on lhs to let x = y in ... or rhs
-desugarAs :: PTerm -> PTerm -> (PTerm, PTerm)
-desugarAs lhs rhs
-    = let (lhs', pats) = runState (collectAs (replaceUnderscore lhs)) [] in
-          (lhs', bindPats pats rhs)
+desugarAs :: PTerm -> PTerm -> [PDecl] -> (PTerm, PTerm, [PDecl])
+desugarAs lhs rhs whereblock
+    = (lhs', bindOnRight rhs pats, map (bindInWhereDecl pats) whereblock)
   where
-    bindPats :: [(Name, FC, PTerm)] -> PTerm -> PTerm
-    bindPats [] rhs = rhs
-    bindPats ((n, fc, tm) : ps) rhs
-       = PLet fc n NoFC Placeholder tm (bindPats ps rhs)
+    (lhs', pats) = runState (collectAs (replaceUnderscore lhs)) []
+
+    bindOnRight :: PTerm -> [(Name, FC, PTerm)] -> PTerm
+    bindOnRight = foldr (\(n, fc, tm) -> PLet fc n NoFC Placeholder tm)
+
+    bindInWhereDecl :: [(Name, FC, PTerm)] -> PDecl -> PDecl
+    bindInWhereDecl pats (PClauses fc opts n clauses)
+       = PClauses fc opts n $ map (bindInWhereClause pats) clauses
+    bindInWhereDecl _ d = d
+
+    bindInWhereClause :: [(Name, FC, PTerm)] -> PClause -> PClause
+    bindInWhereClause pats (PClause fc n lhs ws rhs wb)
+       = let bound = [ n | (PRef _ _ n) <- universe lhs ]
+             pats' = filter (not . (`elem` bound) . \(n,_,_) -> n) pats
+             rhs'  = bindOnRight rhs pats' in
+         PClause fc n lhs ws rhs' $ map (bindInWhereDecl pats') wb
+    bindInWhereClause _ c = c
 
 collectAs :: PTerm -> State [(Name, FC, PTerm)] PTerm
 collectAs (PAs fc n tm) = do tm' <- collectAs tm
diff --git a/src/Idris/Elab/Clause.hs b/src/Idris/Elab/Clause.hs
index 1459173b5..2d6f53790 100644
--- a/src/Idris/Elab/Clause.hs
+++ b/src/Idris/Elab/Clause.hs
@@ -683,11 +683,11 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
                           logElab 5 $ "Elaborated impossible case " ++ showTmImpls lhs ++
                                       "\n" ++ show ptm
                           return (Left ptm, lhs)
-elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock)
+elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock_as)
    = do let tcgen = Dictionary `elem` opts
         push_estack fname False
         ctxt <- getContext
-        let (lhs_in, rhs_in) = desugarAs lhs_in_as rhs_in_as
+        let (lhs_in, rhs_in, whereblock) = desugarAs lhs_in_as rhs_in_as whereblock_as
 
         -- Build the LHS as an "Infer", and pull out its type and
         -- pattern bindings
diff --git a/test/TestData.hs b/test/TestData.hs
index 29889d820..9fa39d4cf 100644
--- a/test/TestData.hs
+++ b/test/TestData.hs
@@ -71,7 +71,8 @@ testFamiliesData = [
       ( 16, ANY  ),
       ( 17, ANY  ),
       ( 18, ANY  ),
-      ( 19, ANY  )]),
+      ( 19, ANY  ),
+      ( 20, ANY  )]),
   ("bignum",          "Bignum",
     [ (  1, ANY  ),
       (  2, ANY  )]),
diff --git a/test/basic020/basic020.idr b/test/basic020/basic020.idr
new file mode 100644
index 000000000..912e50b3b
--- /dev/null
+++ b/test/basic020/basic020.idr
@@ -0,0 +1,42 @@
+%default total
+
+data Ty = Ctor Int
+
+fn : Ty -> Ty
+fn m@(Ctor _) = y
+  where
+    y = m -- from @ pattern
+
+asPatternVisibleInWhere : fn (Ctor 42) = Ctor 42
+asPatternVisibleInWhere = Refl
+
+fn2 : Ty -> Ty
+fn2 m@(Ctor _) = y (Ctor 99)
+  where
+    y m = m -- should be the arg `m`, not the @ pattern
+
+lhsVariablesShadowAsPattern : fn2 (Ctor 42) = Ctor 99
+lhsVariablesShadowAsPattern = Refl
+
+fn3 : Ty -> Ty
+fn3 m@(Ctor _) = y (Ctor 99)
+  where
+    y m = z
+      where
+        z = m -- should be y's arg `m`, not @ pattern
+
+nestedWhereShadowsAsPattern : fn3 (Ctor 42) = Ctor 99
+nestedWhereShadowsAsPattern = Refl
+
+fn4 : Ty -> Ty
+fn4 m@(Ctor _) = y (Ctor 99)
+  where
+    y _ = z
+      where
+        z = m -- should be @ pattern
+
+nestedWhereExposesAsPattern : fn4 (Ctor 42) = Ctor 42
+nestedWhereExposesAsPattern = Refl
+
+main : IO ()
+main = putStrLn "OK"
diff --git a/test/basic020/expected b/test/basic020/expected
new file mode 100644
index 000000000..d86bac9de
--- /dev/null
+++ b/test/basic020/expected
@@ -0,0 +1 @@
+OK
diff --git a/test/basic020/run b/test/basic020/run
new file mode 100755
index 000000000..eaffe8085
--- /dev/null
+++ b/test/basic020/run
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ basic020.idr -o basic020
+./basic020
+rm -f basic020 *.ibc

From be8523f834faf04709cdf8e63bcf09ba942d20f3 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Sat, 16 Sep 2017 14:42:42 +0100
Subject: [PATCH 20/27] Fix for commit in Text.Parser

Need to remember the commit status of the branch after returning from
successfully parsing an alternative
---
 libs/contrib/Text/Parser.idr | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/libs/contrib/Text/Parser.idr b/libs/contrib/Text/Parser.idr
index 640f7c24e..0a0481066 100644
--- a/libs/contrib/Text/Parser.idr
+++ b/libs/contrib/Text/Parser.idr
@@ -152,12 +152,16 @@ data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
                    (val : ty) -> (more : List tok) ->
                    ParseResult (x :: xs ++ more) c ty
 
+-- Take the result of an alternative branch, reset the commit flag to
+-- the commit flag from the outer alternative, and weaken the 'consumes'
+-- flag to take both alternatives into account
 weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
-            ParseResult xs c ty -> ParseResult xs (whatever && c) ty
-weakenRes (Failure com msg ts) = Failure com msg ts
-weakenRes {whatever=True} (EmptyRes com val xs) = EmptyRes com val xs
-weakenRes {whatever=False} (EmptyRes com val xs) = EmptyRes com val xs
-weakenRes (NonEmptyRes com val more) = NonEmptyRes com val more
+            (com' : Bool) ->
+						ParseResult xs c ty -> ParseResult xs (whatever && c) ty
+weakenRes com' (Failure com msg ts) = Failure com' msg ts
+weakenRes {whatever=True} com' (EmptyRes com val xs) = EmptyRes com' val xs
+weakenRes {whatever=False} com' (EmptyRes com val xs) = EmptyRes com' val xs
+weakenRes com' (NonEmptyRes com val more) = NonEmptyRes com' val more
 
 shorter : (more : List tok) -> .(ys : List tok) ->
           LTE (S (length more)) (S (length (ys ++ more)))
@@ -192,7 +196,7 @@ doParse com xs act with (sizeAccessible xs)
           = if com' -- If the alternative had committed, don't try the
                     -- other branch (and reset commit flag)
                then Failure com msg ts
-               else weakenRes (doParse False xs y | sml)
+               else weakenRes com (doParse False xs y | sml)
     -- Successfully parsed the first option, so use the outer commit flag
     doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)
           = EmptyRes com val xs

From d4bd8e63534886faad116074a43c8cdc382fbabf Mon Sep 17 00:00:00 2001
From: Jason Felice <jason.m.felice@gmail.com>
Date: Sat, 16 Sep 2017 13:28:47 -0400
Subject: [PATCH 21/27] Clean up unused imports (#4065)

---
 codegen/idris-codegen-c/Main.hs          |  3 ---
 codegen/idris-codegen-javascript/Main.hs |  3 ---
 codegen/idris-codegen-node/Main.hs       |  3 ---
 idris.cabal                              |  1 -
 main/Main.hs                             |  7 +-----
 src/IRTS/BCImp.hs                        | 23 -----------------
 src/IRTS/Bytecode.hs                     |  1 -
 src/IRTS/CodegenC.hs                     |  4 ---
 src/IRTS/Compiler.hs                     | 10 --------
 src/IRTS/Defunctionalise.hs              |  1 -
 src/IRTS/DumpBC.hs                       |  1 -
 src/IRTS/JavaScript/LangTransforms.hs    |  5 ----
 src/IRTS/JavaScript/Name.hs              |  3 ---
 src/IRTS/JavaScript/PrimOp.hs            |  4 ---
 src/IRTS/JavaScript/Specialize.hs        |  3 ---
 src/IRTS/Lang.hs                         |  2 --
 src/IRTS/LangOpts.hs                     |  4 ---
 src/IRTS/Portable.hs                     |  2 --
 src/IRTS/Simplified.hs                   |  3 ---
 src/Idris/ASTUtils.hs                    |  1 -
 src/Idris/AbsSyntaxTree.hs               |  1 -
 src/Idris/Apropos.hs                     |  2 +-
 src/Idris/Chaser.hs                      |  6 +----
 src/Idris/Core/Binary.hs                 |  4 ---
 src/Idris/Core/CaseTree.hs               |  3 ---
 src/Idris/Core/Constraints.hs            |  6 ++---
 src/Idris/Core/Elaborate.hs              |  7 ------
 src/Idris/Core/Execute.hs                |  6 -----
 src/Idris/Core/ProofState.hs             |  2 --
 src/Idris/Core/ProofTerm.hs              |  3 ---
 src/Idris/Core/TT.hs                     |  9 ++-----
 src/Idris/Core/Typecheck.hs              |  3 ---
 src/Idris/Core/Unify.hs                  |  2 --
 src/Idris/Core/WHNF.hs                   |  3 ---
 src/Idris/Coverage.hs                    |  3 ---
 src/Idris/DSL.hs                         |  2 --
 src/Idris/DataOpts.hs                    |  6 -----
 src/Idris/DeepSeq.hs                     |  1 -
 src/Idris/Delaborate.hs                  |  3 +--
 src/Idris/Directives.hs                  |  1 -
 src/Idris/Elab/AsPat.hs                  |  1 -
 src/Idris/Elab/Clause.hs                 | 17 ++-----------
 src/Idris/Elab/Data.hs                   | 21 +---------------
 src/Idris/Elab/Implementation.hs         | 27 ++------------------
 src/Idris/Elab/Interface.hs              | 31 +----------------------
 src/Idris/Elab/Provider.hs               | 27 --------------------
 src/Idris/Elab/Record.hs                 | 15 +----------
 src/Idris/Elab/Rewrite.hs                |  3 ---
 src/Idris/Elab/RunElab.hs                |  4 +--
 src/Idris/Elab/Term.hs                   | 14 +++--------
 src/Idris/Elab/Transform.hs              | 30 +---------------------
 src/Idris/Elab/Type.hs                   | 29 +--------------------
 src/Idris/Elab/Utils.hs                  |  4 ---
 src/Idris/Elab/Value.hs                  | 32 ++----------------------
 src/Idris/ElabDecls.hs                   | 27 +-------------------
 src/Idris/Erasure.hs                     |  3 ---
 src/Idris/ErrReverse.hs                  |  1 -
 src/Idris/Error.hs                       |  7 ------
 src/Idris/IdeMode.hs                     |  2 +-
 src/Idris/IdrisDoc.hs                    | 13 +++-------
 src/Idris/Imports.hs                     |  1 -
 src/Idris/Info.hs                        |  1 -
 src/Idris/Output.hs                      |  5 ++--
 src/Idris/Package.hs                     |  5 +---
 src/Idris/Package/Parser.hs              |  6 -----
 src/Idris/Parser/Data.hs                 | 15 -----------
 src/Idris/Parser/Expr.hs                 | 12 ---------
 src/Idris/Parser/Helpers.hs              |  6 -----
 src/Idris/Parser/Ops.hs                  | 13 ----------
 src/Idris/PartialEval.hs                 |  3 ---
 src/Idris/Primitives.hs                  |  3 ---
 src/Idris/ProofSearch.hs                 |  3 ---
 src/Idris/Prover.hs                      |  8 +++---
 src/Idris/Providers.hs                   |  2 --
 src/Idris/REPL/Parser.hs                 |  5 +---
 src/Idris/Termination.hs                 |  3 +--
 src/Idris/Transforms.hs                  |  3 ---
 src/Idris/TypeSearch.hs                  |  2 +-
 src/Util/DynamicLinker.hs                | 29 +++++++++++++--------
 stack.yaml                               |  3 +++
 80 files changed, 60 insertions(+), 533 deletions(-)
 delete mode 100644 src/IRTS/BCImp.hs

diff --git a/codegen/idris-codegen-c/Main.hs b/codegen/idris-codegen-c/Main.hs
index a525d355d..594ea0d62 100644
--- a/codegen/idris-codegen-c/Main.hs
+++ b/codegen/idris-codegen-c/Main.hs
@@ -1,7 +1,6 @@
 module Main where
 
 import Idris.AbsSyntax
-import Idris.Core.TT
 import Idris.ElabDecls
 import Idris.Main
 import Idris.Options
@@ -10,8 +9,6 @@ import IRTS.Compiler
 
 import Util.System
 
-import Paths_idris
-
 import Control.Monad
 import System.Environment
 import System.Exit
diff --git a/codegen/idris-codegen-javascript/Main.hs b/codegen/idris-codegen-javascript/Main.hs
index 1d13a2612..e8728fcc6 100644
--- a/codegen/idris-codegen-javascript/Main.hs
+++ b/codegen/idris-codegen-javascript/Main.hs
@@ -1,15 +1,12 @@
 module Main where
 
 import Idris.AbsSyntax
-import Idris.Core.TT
 import Idris.ElabDecls
 import Idris.Main
 import Idris.Options
 import IRTS.CodegenJavaScript
 import IRTS.Compiler
 
-import Paths_idris
-
 import System.Environment
 import System.Exit
 
diff --git a/codegen/idris-codegen-node/Main.hs b/codegen/idris-codegen-node/Main.hs
index 3300f0fb7..b61e0e025 100644
--- a/codegen/idris-codegen-node/Main.hs
+++ b/codegen/idris-codegen-node/Main.hs
@@ -1,15 +1,12 @@
 module Main where
 
 import Idris.AbsSyntax
-import Idris.Core.TT
 import Idris.ElabDecls
 import Idris.Main
 import Idris.Options
 import IRTS.CodegenJavaScript
 import IRTS.Compiler
 
-import Paths_idris
-
 import System.Environment
 import System.Exit
 
diff --git a/idris.cabal b/idris.cabal
index d880d2bfd..52e2bc291 100644
--- a/idris.cabal
+++ b/idris.cabal
@@ -226,7 +226,6 @@ Library
                 , Idris.WhoCalls
                 , Idris.CmdOptions
 
-                , IRTS.BCImp
                 , IRTS.Bytecode
                 , IRTS.CodegenC
                 , IRTS.CodegenCommon
diff --git a/main/Main.hs b/main/Main.hs
index 26ea7032b..a90e2d3fc 100644
--- a/main/Main.hs
+++ b/main/Main.hs
@@ -2,9 +2,7 @@ module Main where
 
 import System.Exit (ExitCode(..), exitSuccess, exitWith)
 
-import Control.Monad (unless, when, (>=>))
-import Data.Foldable (foldrM)
-import Data.Maybe (fromMaybe)
+import Control.Monad (unless, when)
 
 import Idris.AbsSyntax
 import Idris.CmdOptions
@@ -16,9 +14,6 @@ import Idris.Package
 
 import Util.System (setupBundledCC)
 
-import System.Exit (ExitCode(..), exitWith)
-import Util.System (setupBundledCC)
-
 processShowOptions :: [Opt] -> Idris ()
 processShowOptions opts = runIO $ do
   when (ShowAll `elem` opts)          $ showExitIdrisInfo
diff --git a/src/IRTS/BCImp.hs b/src/IRTS/BCImp.hs
deleted file mode 100644
index 5bcf5857e..000000000
--- a/src/IRTS/BCImp.hs
+++ /dev/null
@@ -1,23 +0,0 @@
-{-|
-Module      : IRTS.BCImp
-Description : Bytecode for a register/variable based VM (e.g. for generating code in an imperative language where we let the language deal with GC)
-Copyright   :
-License     : BSD3
-Maintainer  : The Idris Community.
--}
-module IRTS.BCImp where
-
-import Idris.Core.TT
-import IRTS.Lang
-import IRTS.Simplified
-
-data Reg = RVal | L Int
-
-data BC = NOP
-
-toBC :: (Name, SDecl) -> (Name, [BC])
-toBC (n, SFun n' args locs exp)
-   = (n, bc RVal exp)
-
-bc :: Reg -> SExp -> [BC]
-bc = undefined
diff --git a/src/IRTS/Bytecode.hs b/src/IRTS/Bytecode.hs
index 24b9c97dc..fb27096b9 100644
--- a/src/IRTS/Bytecode.hs
+++ b/src/IRTS/Bytecode.hs
@@ -23,7 +23,6 @@ module IRTS.Bytecode where
 
 import Idris.Core.TT
 import IRTS.Defunctionalise
-import IRTS.Lang
 import IRTS.Simplified
 
 import Data.Maybe
diff --git a/src/IRTS/CodegenC.hs b/src/IRTS/CodegenC.hs
index 9aa9ac63e..a7c2aeaa3 100644
--- a/src/IRTS/CodegenC.hs
+++ b/src/IRTS/CodegenC.hs
@@ -9,12 +9,10 @@ Maintainer  : The Idris Community.
 
 module IRTS.CodegenC (codegenC) where
 
-import Idris.AbsSyntax
 import Idris.Core.TT
 import IRTS.Bytecode
 import IRTS.CodegenCommon
 import IRTS.Defunctionalise
-import IRTS.Lang
 import IRTS.Simplified
 import IRTS.System
 
@@ -24,9 +22,7 @@ import Control.Monad
 import Data.Bits
 import Data.Char
 import Data.List (intercalate, nubBy)
-import Debug.Trace
 import Numeric
-import System.Directory
 import System.Exit
 import System.FilePath ((<.>), (</>))
 import System.IO
diff --git a/src/IRTS/Compiler.hs b/src/IRTS/Compiler.hs
index 0af967bbd..09c7aca5c 100644
--- a/src/IRTS/Compiler.hs
+++ b/src/IRTS/Compiler.hs
@@ -10,7 +10,6 @@ Maintainer  : The Idris Community.
 module IRTS.Compiler(compile, generate) where
 
 import Idris.AbsSyntax
-import Idris.AbsSyntaxTree
 import Idris.ASTUtils
 import Idris.Core.CaseTree
 import Idris.Core.Evaluate
@@ -21,33 +20,24 @@ import Idris.Options
 import Idris.Output
 import IRTS.CodegenC
 import IRTS.CodegenCommon
-import IRTS.CodegenJavaScript
 import IRTS.Defunctionalise
 import IRTS.DumpBC
 import IRTS.Exports
 import IRTS.Inliner
-import IRTS.Lang
 import IRTS.LangOpts
 import IRTS.Portable
 import IRTS.Simplified
 
 import Prelude hiding (id, (.))
 
-import Control.Applicative
 import Control.Category
 import Control.Monad.State
-import Data.IntSet (IntSet)
-import qualified Data.IntSet as IS
 import Data.List
 import qualified Data.Map as M
-import Data.Maybe
 import Data.Ord
 import qualified Data.Set as S
-import Debug.Trace
 import System.Directory
-import System.Environment
 import System.Exit
-import System.FilePath (addTrailingPathSeparator, (</>))
 import System.IO
 import System.Process
 
diff --git a/src/IRTS/Defunctionalise.hs b/src/IRTS/Defunctionalise.hs
index 7994cf2b0..500ad08b6 100644
--- a/src/IRTS/Defunctionalise.hs
+++ b/src/IRTS/Defunctionalise.hs
@@ -32,7 +32,6 @@ import Control.Monad
 import Control.Monad.State
 import Data.List
 import Data.Maybe
-import Debug.Trace
 
 data DExp = DV Name
           | DApp Bool Name [DExp] -- True = tail call
diff --git a/src/IRTS/DumpBC.hs b/src/IRTS/DumpBC.hs
index 43f00761b..bcad069aa 100644
--- a/src/IRTS/DumpBC.hs
+++ b/src/IRTS/DumpBC.hs
@@ -9,7 +9,6 @@ module IRTS.DumpBC where
 
 import Idris.Core.TT
 import IRTS.Bytecode
-import IRTS.Lang
 import IRTS.Simplified
 
 import Data.List
diff --git a/src/IRTS/JavaScript/LangTransforms.hs b/src/IRTS/JavaScript/LangTransforms.hs
index 61c66cab4..7560bbd0e 100644
--- a/src/IRTS/JavaScript/LangTransforms.hs
+++ b/src/IRTS/JavaScript/LangTransforms.hs
@@ -12,23 +12,18 @@ module IRTS.JavaScript.LangTransforms( removeDeadCode
                                      ) where
 
 
-import Control.DeepSeq
-import Control.Monad.Trans.State
 import Data.List
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import Data.Maybe
 import Data.Set (Set)
 import qualified Data.Set as Set
-import Data.Text (Text)
-import qualified Data.Text as T
 import Idris.Core.CaseTree
 import Idris.Core.TT
 import IRTS.Lang
 
 import Data.Data
 import Data.Generics.Uniplate.Data
-import GHC.Generics (Generic)
 
 deriving instance Typeable FDesc
 deriving instance Data FDesc
diff --git a/src/IRTS/JavaScript/Name.hs b/src/IRTS/JavaScript/Name.hs
index 175a58874..546197e1f 100644
--- a/src/IRTS/JavaScript/Name.hs
+++ b/src/IRTS/JavaScript/Name.hs
@@ -20,12 +20,9 @@ module IRTS.JavaScript.Name
   ) where
 
 import Data.Char
-import Data.List
-import qualified Data.Map.Strict as Map
 import Data.Text (Text)
 import qualified Data.Text as T
 import Idris.Core.TT
-import IRTS.JavaScript.AST
 
 jsEscape :: String -> String
 jsEscape = concatMap jschar
diff --git a/src/IRTS/JavaScript/PrimOp.hs b/src/IRTS/JavaScript/PrimOp.hs
index 0e11a6429..668f9bd34 100644
--- a/src/IRTS/JavaScript/PrimOp.hs
+++ b/src/IRTS/JavaScript/PrimOp.hs
@@ -16,11 +16,7 @@ module IRTS.JavaScript.PrimOp
   , jsPrimCoerce
   ) where
 
-import Data.Char
-import Data.List
 import qualified Data.Map.Strict as Map
-import Data.Text (Text)
-import qualified Data.Text as T
 import Idris.Core.TT
 import IRTS.JavaScript.AST
 import IRTS.Lang
diff --git a/src/IRTS/JavaScript/Specialize.hs b/src/IRTS/JavaScript/Specialize.hs
index 2cf4e1275..910836bbe 100644
--- a/src/IRTS/JavaScript/Specialize.hs
+++ b/src/IRTS/JavaScript/Specialize.hs
@@ -17,10 +17,7 @@ module IRTS.JavaScript.Specialize
   , qualifyN
   ) where
 
-import Data.Char
-import Data.List
 import qualified Data.Map.Strict as Map
-import Data.Text (Text)
 import qualified Data.Text as T
 import Idris.Core.TT
 import IRTS.JavaScript.AST
diff --git a/src/IRTS/Lang.hs b/src/IRTS/Lang.hs
index 7384bf6bb..94487b342 100644
--- a/src/IRTS/Lang.hs
+++ b/src/IRTS/Lang.hs
@@ -13,12 +13,10 @@ module IRTS.Lang where
 import Idris.Core.CaseTree
 import Idris.Core.TT
 
-import Control.Applicative hiding (Const)
 import Control.Monad.State hiding (lift)
 import Data.Data (Data)
 import Data.List
 import Data.Typeable (Typeable)
-import Debug.Trace
 import GHC.Generics (Generic)
 
 data Endianness = Native | BE | LE deriving (Show, Eq)
diff --git a/src/IRTS/LangOpts.hs b/src/IRTS/LangOpts.hs
index 11be92877..90df9add0 100644
--- a/src/IRTS/LangOpts.hs
+++ b/src/IRTS/LangOpts.hs
@@ -9,14 +9,10 @@ Maintainer  : The Idris Community.
 
 module IRTS.LangOpts where
 
-import Idris.Core.CaseTree
 import Idris.Core.TT
 import IRTS.Lang
 
-import Control.Applicative hiding (Const)
 import Control.Monad.State hiding (lift)
-import Data.List
-import Debug.Trace
 
 inlineAll :: [(Name, LDecl)] -> [(Name, LDecl)]
 inlineAll lds = let defs = addAlist lds emptyContext in
diff --git a/src/IRTS/Portable.hs b/src/IRTS/Portable.hs
index 7840acf2e..7114d7d32 100644
--- a/src/IRTS/Portable.hs
+++ b/src/IRTS/Portable.hs
@@ -14,12 +14,10 @@ import Idris.Core.TT
 import IRTS.Bytecode
 import IRTS.CodegenCommon
 import IRTS.Defunctionalise
-import IRTS.Lang
 import IRTS.Simplified
 
 import Data.Aeson
 import qualified Data.ByteString.Lazy as B
-import qualified Data.Text as T
 import System.IO
 
 data CodegenFile = CGFile {
diff --git a/src/IRTS/Simplified.hs b/src/IRTS/Simplified.hs
index cb2573ed8..8a66bb461 100644
--- a/src/IRTS/Simplified.hs
+++ b/src/IRTS/Simplified.hs
@@ -10,12 +10,9 @@ module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where
 
 import Idris.Core.CaseTree
 import Idris.Core.TT
-import Idris.Core.Typecheck
 import IRTS.Defunctionalise
 
 import Control.Monad.State
-import Data.Maybe
-import Debug.Trace
 
 data SExp = SV LVar
           | SApp Bool Name [LVar]
diff --git a/src/Idris/ASTUtils.hs b/src/Idris/ASTUtils.hs
index dff453293..4e15d3f9e 100644
--- a/src/Idris/ASTUtils.hs
+++ b/src/Idris/ASTUtils.hs
@@ -52,7 +52,6 @@ import Idris.Options
 
 import Prelude hiding (id, (.))
 
-import Control.Applicative
 import Control.Category
 import Control.Monad.State.Class
 import Data.Maybe
diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs
index c81159cbd..a4b10ec6b 100644
--- a/src/Idris/AbsSyntaxTree.hs
+++ b/src/Idris/AbsSyntaxTree.hs
@@ -46,7 +46,6 @@ import qualified Data.Text as T
 import Data.Traversable (Traversable)
 import Data.Typeable
 import GHC.Generics (Generic)
-import Network.Socket (PortNumber)
 
 
 data ElabWhat = ETypes | EDefns | EAll
diff --git a/src/Idris/Apropos.hs b/src/Idris/Apropos.hs
index 51d9a1d39..e22e33228 100644
--- a/src/Idris/Apropos.hs
+++ b/src/Idris/Apropos.hs
@@ -11,7 +11,7 @@ module Idris.Apropos (apropos, aproposModules) where
 import Idris.AbsSyntax
 import Idris.Core.Evaluate (Def(..), ctxtAlist)
 import Idris.Core.TT (Binder(..), Const(..), Name(..), NameType(..), TT(..),
-                      Type, lookupCtxtExact, toAlist)
+                      Type, toAlist)
 import Idris.Docstrings (DocTerm, Docstring, containsText)
 
 import Data.List (intersperse, nub, nubBy)
diff --git a/src/Idris/Chaser.hs b/src/Idris/Chaser.hs
index 7c7592add..49cc280e8 100644
--- a/src/Idris/Chaser.hs
+++ b/src/Idris/Chaser.hs
@@ -16,19 +16,15 @@ module Idris.Chaser(
 import Idris.AbsSyntax
 import Idris.Core.TT
 import Idris.Error
-import Idris.IBC
 import Idris.Imports
 import Idris.Parser
 import Idris.Unlit
 
 import Control.Monad.State
-import Control.Monad.Trans
 import Data.List
 import Data.Time.Clock
-import Debug.Trace
 import System.Directory
-import System.FilePath
-import Util.System (readSource, writeSource)
+import Util.System (readSource)
 
 data ModuleTree = MTree { mod_path :: IFileType,
                           mod_needsRecheck :: Bool,
diff --git a/src/Idris/Core/Binary.hs b/src/Idris/Core/Binary.hs
index 9c36ab8ec..e7ff10d94 100644
--- a/src/Idris/Core/Binary.hs
+++ b/src/Idris/Core/Binary.hs
@@ -13,14 +13,10 @@ module Idris.Core.Binary where
 import Idris.Core.TT
 
 import Control.Applicative ((<$>), (<*>))
-import Control.DeepSeq (($!!))
 import Control.Monad (liftM2)
 import Data.Binary
 import Data.Binary.Get
 import Data.Binary.Put
-import qualified Data.Text as T
-import qualified Data.Text.Encoding as E
-import Data.Vector.Binary
 
 instance Binary ErrorReportPart where
   put (TextPart msg) = do putWord8 0 ; put msg
diff --git a/src/Idris/Core/CaseTree.hs b/src/Idris/Core/CaseTree.hs
index 45e7af535..67bd9860d 100644
--- a/src/Idris/Core/CaseTree.hs
+++ b/src/Idris/Core/CaseTree.hs
@@ -31,14 +31,11 @@ module Idris.Core.CaseTree (
 
 import Idris.Core.TT
 
-import Control.Applicative hiding (Const)
 import Control.Monad.Reader
 import Control.Monad.State
 import Data.List hiding (partition)
 import qualified Data.List (partition)
-import Data.Maybe
 import qualified Data.Set as S
-import Debug.Trace
 import GHC.Generics (Generic)
 
 data CaseDef = CaseDef [Name] !SC [Term]
diff --git a/src/Idris/Core/Constraints.hs b/src/Idris/Core/Constraints.hs
index bbb56286d..44d8a2ffe 100644
--- a/src/Idris/Core/Constraints.hs
+++ b/src/Idris/Core/Constraints.hs
@@ -8,15 +8,13 @@ Maintainer  : The Idris Community.
 -}
 module Idris.Core.Constraints ( ucheck ) where
 
-import Idris.Core.TT (ConstraintFC(..), Err'(..), FC(..), TC(..),
-                      UConstraint(..), UExp(..))
+import Idris.Core.TT (ConstraintFC(..), Err'(..), TC(..), UConstraint(..),
+                      UExp(..))
 
-import Control.Applicative
 import Control.Monad.State.Strict
 import Data.List (partition)
 import qualified Data.Map.Strict as M
 import qualified Data.Set as S
-import Debug.Trace
 
 -- | Check that a list of universe constraints can be satisfied.
 ucheck :: S.Set ConstraintFC -> TC ()
diff --git a/src/Idris/Core/Elaborate.hs b/src/Idris/Core/Elaborate.hs
index c2a9cecdd..282722bd7 100644
--- a/src/Idris/Core/Elaborate.hs
+++ b/src/Idris/Core/Elaborate.hs
@@ -16,7 +16,6 @@ module Idris.Core.Elaborate (
   , module Idris.Core.ProofState
   ) where
 
-import Idris.Core.DeepSeq
 import Idris.Core.Evaluate
 import Idris.Core.ProofState
 import Idris.Core.ProofTerm (bound_in, bound_in_term, getProofTerm, mkProofTerm,
@@ -24,15 +23,9 @@ import Idris.Core.ProofTerm (bound_in, bound_in_term, getProofTerm, mkProofTerm,
 import Idris.Core.TT
 import Idris.Core.Typecheck
 import Idris.Core.Unify
-import Idris.Core.WHNF
 
-import Util.Pretty hiding (fill)
-
-import Control.DeepSeq
 import Control.Monad.State.Strict
-import Data.Char
 import Data.List
-import Debug.Trace
 
 data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
   deriving Show
diff --git a/src/Idris/Core/Execute.hs b/src/Idris/Core/Execute.hs
index ff1757ba9..29dcf19be 100644
--- a/src/Idris/Core/Execute.hs
+++ b/src/Idris/Core/Execute.hs
@@ -11,7 +11,6 @@ Maintainer  : The Idris Community.
 module Idris.Core.Execute (execute) where
 
 import Idris.AbsSyntax
-import Idris.AbsSyntaxTree
 import Idris.Core.CaseTree
 import Idris.Core.Evaluate
 import Idris.Core.TT
@@ -22,15 +21,11 @@ import IRTS.Lang (FDesc(..), FType(..))
 import Util.DynamicLinker
 import Util.System
 
-import Control.Applicative hiding (Const)
 import Control.Exception
-import Control.Monad hiding (forM)
 import Control.Monad.Trans
 import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)
 import Control.Monad.Trans.State.Strict
-import Data.Bits
 import Data.IORef
-import qualified Data.Map as M
 import Data.Maybe
 import Data.Time.Clock.POSIX (getPOSIXTime)
 import Data.Traversable (forM)
@@ -42,7 +37,6 @@ import System.IO.Unsafe
 #ifdef IDRIS_FFI
 import Foreign.C.String
 import Foreign.LibFFI
-import Foreign.Marshal.Alloc (free)
 import Foreign.Ptr
 #endif
 
diff --git a/src/Idris/Core/ProofState.hs b/src/Idris/Core/ProofState.hs
index 05d225a7c..4ea2f4e4b 100644
--- a/src/Idris/Core/ProofState.hs
+++ b/src/Idris/Core/ProofState.hs
@@ -28,11 +28,9 @@ import Idris.Core.WHNF
 
 import Util.Pretty hiding (fill)
 
-import Control.Applicative hiding (empty)
 import Control.Arrow ((***))
 import Control.Monad.State.Strict
 import Data.List
-import Debug.Trace
 
 data ProofState = PS { thname            :: Name,
                        holes             :: [Name], -- ^ holes still to be solved
diff --git a/src/Idris/Core/ProofTerm.hs b/src/Idris/Core/ProofTerm.hs
index 6f9aa3223..fbfc72f3d 100644
--- a/src/Idris/Core/ProofTerm.hs
+++ b/src/Idris/Core/ProofTerm.hs
@@ -18,11 +18,8 @@ module Idris.Core.ProofTerm(
 
 import Idris.Core.Evaluate
 import Idris.Core.TT
-import Idris.Core.Typecheck
 
 import Control.Monad.State.Strict
-import Data.List
-import Debug.Trace
 
 -- | A zipper over terms, in order to efficiently update proof terms.
 data TermPath = Top
diff --git a/src/Idris/Core/TT.hs b/src/Idris/Core/TT.hs
index 2451259e2..b13817938 100644
--- a/src/Idris/Core/TT.hs
+++ b/src/Idris/Core/TT.hs
@@ -60,29 +60,24 @@ import Util.Pretty hiding (Str)
 -- Work around AMP without CPP
 import Prelude (Bool(..), Double, Enum(..), Eq(..), FilePath, Functor(..), Int,
                 Integer, Maybe(..), Monad(..), Num(..), Ord(..), Ordering(..),
-                Read(..), Show(..), String, div, error, flip, fst, mod, not,
-                otherwise, read, snd, ($), (&&), (.), (||))
+                Show(..), String, div, error, fst, mod, not, otherwise, read,
+                snd, ($), (&&), (.), (||))
 
 import Control.Applicative (Alternative, Applicative(..))
 import qualified Control.Applicative as A (Alternative(..))
 import Control.DeepSeq (($!!))
 import Control.Monad.State.Strict
-import Control.Monad.Trans.Except (Except(..))
 import Data.Binary hiding (get, put)
-import qualified Data.Binary as B
 import Data.Char
 import Data.Data (Data)
 import Data.Foldable (Foldable)
 import Data.List hiding (group, insert)
 import qualified Data.Map.Strict as Map
 import Data.Maybe (listToMaybe)
-import Data.Monoid (mconcat)
 import Data.Set (Set, fromList, insert, member)
 import qualified Data.Text as T
 import Data.Traversable (Traversable)
 import Data.Typeable (Typeable)
-import Data.Vector.Unboxed (Vector)
-import qualified Data.Vector.Unboxed as V
 import Debug.Trace
 import Foreign.Storable (sizeOf)
 import GHC.Generics (Generic)
diff --git a/src/Idris/Core/Typecheck.hs b/src/Idris/Core/Typecheck.hs
index 2555e76e7..40b33e55d 100644
--- a/src/Idris/Core/Typecheck.hs
+++ b/src/Idris/Core/Typecheck.hs
@@ -13,11 +13,8 @@ module Idris.Core.Typecheck where
 
 import Idris.Core.Evaluate
 import Idris.Core.TT
-import Idris.Core.WHNF
 
 import Control.Monad.State
-import qualified Data.Vector.Unboxed as V (length)
-import Debug.Trace
 
 -- To check conversion, normalise each term wrt the current environment.
 -- Since we haven't converted everything to de Bruijn indices yet, we'll have to
diff --git a/src/Idris/Core/Unify.hs b/src/Idris/Core/Unify.hs
index bb029e3d0..89f1ca225 100644
--- a/src/Idris/Core/Unify.hs
+++ b/src/Idris/Core/Unify.hs
@@ -22,11 +22,9 @@ module Idris.Core.Unify(
 import Idris.Core.Evaluate
 import Idris.Core.TT
 
-import Control.Monad
 import Control.Monad.State.Strict
 import Data.List
 import Data.Maybe
-import Debug.Trace
 
 -- terms which need to be injective, with the things we're trying to unify
 -- at the time
diff --git a/src/Idris/Core/WHNF.hs b/src/Idris/Core/WHNF.hs
index 0a5fc8220..059ccfa16 100644
--- a/src/Idris/Core/WHNF.hs
+++ b/src/Idris/Core/WHNF.hs
@@ -12,11 +12,8 @@ module Idris.Core.WHNF(whnf, whnfArgs, WEnv) where
 
 import Idris.Core.CaseTree
 import Idris.Core.Evaluate hiding (quote)
-import qualified Idris.Core.Evaluate as Evaluate
 import Idris.Core.TT
 
-import Debug.Trace
-
 -- | A stack entry consists of a term and the environment it is to be
 -- evaluated in (i.e. it's a thunk)
 type StackEntry = (Term, WEnv)
diff --git a/src/Idris/Coverage.hs b/src/Idris/Coverage.hs
index e42c1606c..b17eb4a35 100644
--- a/src/Idris/Coverage.hs
+++ b/src/Idris/Coverage.hs
@@ -16,14 +16,11 @@ import Idris.Core.TT
 import Idris.Delaborate
 import Idris.Elab.Utils
 import Idris.Error
-import Idris.Output (iWarn, iputStrLn)
 
 import Control.Monad.State.Strict
 import Data.Char
-import Data.Either
 import Data.List
 import Data.Maybe
-import Debug.Trace
 
 -- | Generate a pattern from an 'impossible' LHS.
 --
diff --git a/src/Idris/DSL.hs b/src/Idris/DSL.hs
index 81ebea564..5b25b7217 100644
--- a/src/Idris/DSL.hs
+++ b/src/Idris/DSL.hs
@@ -11,12 +11,10 @@ Maintainer  : The Idris Community.
 module Idris.DSL where
 
 import Idris.AbsSyntax
-import Idris.Core.Evaluate
 import Idris.Core.TT
 
 import Control.Monad.State.Strict
 import Data.Generics.Uniplate.Data (transform)
-import Debug.Trace
 
 debindApp :: SyntaxInfo -> PTerm -> PTerm
 debindApp syn t = debind (dsl_bind (dsl_info syn)) t
diff --git a/src/Idris/DataOpts.hs b/src/Idris/DataOpts.hs
index 6fe17fd6c..e11458779 100644
--- a/src/Idris/DataOpts.hs
+++ b/src/Idris/DataOpts.hs
@@ -10,14 +10,8 @@ Maintainer  : The Idris Community.
 module Idris.DataOpts(applyOpts) where
 
 import Idris.AbsSyntax
-import Idris.AbsSyntaxTree
 import Idris.Core.TT
 
-import Control.Applicative
-import Data.List
-import Data.Maybe
-import Debug.Trace
-
 class Optimisable term where
     applyOpts :: term -> Idris term
 
diff --git a/src/Idris/DeepSeq.hs b/src/Idris/DeepSeq.hs
index e7ccafbd7..08a3ada7d 100644
--- a/src/Idris/DeepSeq.hs
+++ b/src/Idris/DeepSeq.hs
@@ -24,7 +24,6 @@ import IRTS.Lang (PrimFn(..))
 
 import Util.DynamicLinker
 
-import qualified Cheapskate.Types as CT
 import Control.DeepSeq
 import Network.Socket (PortNumber)
 
diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs
index 2a8426e1f..4f8f3a36a 100644
--- a/src/Idris/Delaborate.hs
+++ b/src/Idris/Delaborate.hs
@@ -26,10 +26,9 @@ import Prelude hiding ((<$>))
 import Control.Applicative (Alternative((<|>)))
 import Control.Monad.State
 import Data.Generics.Uniplate.Data (transform)
-import Data.List (intersperse, nub)
+import Data.List (nub)
 import Data.Maybe (mapMaybe)
 import qualified Data.Text as T
-import Debug.Trace
 
 bugaddr = "https://github.com/idris-lang/Idris-dev/issues"
 
diff --git a/src/Idris/Directives.hs b/src/Idris/Directives.hs
index 4f95bf645..e1f4a02da 100644
--- a/src/Idris/Directives.hs
+++ b/src/Idris/Directives.hs
@@ -8,7 +8,6 @@ Maintainer  : The Idris Community.
 module Idris.Directives(directiveAction) where
 
 import Idris.AbsSyntax
-import Idris.ASTUtils
 import Idris.Core.Evaluate
 import Idris.Core.TT
 import Idris.Imports
diff --git a/src/Idris/Elab/AsPat.hs b/src/Idris/Elab/AsPat.hs
index eb85f54e3..e44e50b0c 100644
--- a/src/Idris/Elab/AsPat.hs
+++ b/src/Idris/Elab/AsPat.hs
@@ -10,7 +10,6 @@ module Idris.Elab.AsPat(desugarAs) where
 import Idris.AbsSyntax
 import Idris.Core.TT
 
-import Control.Applicative
 import Control.Monad.State.Strict
 import Data.Generics.Uniplate.Data (transformM, universe)
 
diff --git a/src/Idris/Elab/Clause.hs b/src/Idris/Elab/Clause.hs
index 2d6f53790..8a74e3824 100644
--- a/src/Idris/Elab/Clause.hs
+++ b/src/Idris/Elab/Clause.hs
@@ -13,51 +13,38 @@ import Idris.ASTUtils
 import Idris.Core.CaseTree
 import Idris.Core.Elaborate hiding (Tactic(..))
 import Idris.Core.Evaluate
-import Idris.Core.Execute
 import Idris.Core.TT
 import Idris.Core.Typecheck
 import Idris.Core.WHNF
 import Idris.Coverage
 import Idris.DataOpts
-import Idris.DeepSeq
+import Idris.DeepSeq ()
 import Idris.Delaborate
 import Idris.Docstrings hiding (Unchecked)
-import Idris.DSL
 import Idris.Elab.AsPat
 import Idris.Elab.Term
 import Idris.Elab.Transform
 import Idris.Elab.Type
 import Idris.Elab.Utils
 import Idris.Error
-import Idris.Imports
 import Idris.Inliner
 import Idris.Options
-import Idris.Output (iRenderResult, iWarn, iputStrLn, pshow, sendHighlighting)
+import Idris.Output (iputStrLn, pshow, sendHighlighting)
 import Idris.PartialEval
-import Idris.Primitives
-import Idris.Providers
 import Idris.Termination
 import Idris.Transforms
-import IRTS.Lang
 
 import Util.Pretty hiding ((<$>))
-import Util.Pretty (pretty, text)
 
 import Prelude hiding (id, (.))
 
-import Control.Applicative hiding (Const)
 import Control.Category
 import Control.DeepSeq
 import Control.Monad
 import qualified Control.Monad.State.Lazy as LState
 import Control.Monad.State.Strict as State
-import Data.Char (isLetter, toLower)
 import Data.List
-import Data.List.Split (splitOn)
-import qualified Data.Map as Map
 import Data.Maybe
-import qualified Data.Set as S
-import qualified Data.Text as T
 import Data.Word
 import Debug.Trace
 import Numeric
diff --git a/src/Idris/Elab/Data.hs b/src/Idris/Elab/Data.hs
index 539171fb3..f0faef72c 100644
--- a/src/Idris/Elab/Data.hs
+++ b/src/Idris/Elab/Data.hs
@@ -10,49 +10,30 @@ module Idris.Elab.Data(elabData) where
 
 import Idris.AbsSyntax
 import Idris.ASTUtils
-import Idris.Core.CaseTree
-import Idris.Core.Elaborate hiding (Tactic(..))
 import Idris.Core.Evaluate
-import Idris.Core.Execute
 import Idris.Core.TT
 import Idris.Core.Typecheck
-import Idris.Coverage
-import Idris.DataOpts
-import Idris.DeepSeq
 import Idris.Delaborate
 import Idris.Docstrings
-import Idris.DSL
 import Idris.Elab.Rewrite
-import Idris.Elab.Term
 import Idris.Elab.Type
 import Idris.Elab.Utils
 import Idris.Elab.Value
 import Idris.Error
-import Idris.Imports
-import Idris.Inliner
-import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
-import Idris.PartialEval
-import Idris.Primitives
-import Idris.Providers
-import IRTS.Lang
+import Idris.Output (iWarn, sendHighlighting)
 
 import Util.Pretty
 
 import Prelude hiding (id, (.))
 
-import Control.Applicative hiding (Const)
 import Control.Category
-import Control.DeepSeq
 import Control.Monad
 import Control.Monad.State.Strict as State
 import Data.Char (isLetter, toLower)
 import Data.List
-import Data.List.Split (splitOn)
 import qualified Data.Map as Map
 import Data.Maybe
-import qualified Data.Set as S
 import qualified Data.Text as T
-import Debug.Trace
 
 warnLC :: FC -> Name -> Idris ()
 warnLC fc n
diff --git a/src/Idris/Elab/Implementation.hs b/src/Idris/Elab/Implementation.hs
index 1a1862c98..5b4683635 100644
--- a/src/Idris/Elab/Implementation.hs
+++ b/src/Idris/Elab/Implementation.hs
@@ -9,50 +9,27 @@ Maintainer  : The Idris Community.
 module Idris.Elab.Implementation(elabImplementation) where
 
 import Idris.AbsSyntax
-import Idris.ASTUtils
 import Idris.Core.CaseTree
 import Idris.Core.Elaborate hiding (Tactic(..))
 import Idris.Core.Evaluate
-import Idris.Core.Execute
 import Idris.Core.TT
-import Idris.Core.Typecheck
-import Idris.Coverage
-import Idris.DataOpts
-import Idris.DeepSeq
 import Idris.Delaborate
 import Idris.Docstrings
-import Idris.DSL
-import Idris.Elab.Data
 import Idris.Elab.Term
 import Idris.Elab.Type
 import Idris.Elab.Utils
 import Idris.Error
-import Idris.Imports
-import Idris.Inliner
-import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
-import Idris.PartialEval
-import Idris.Primitives
-import Idris.Providers
-import IRTS.Lang
+import Idris.Output (iWarn, sendHighlighting)
 
-import Util.Pretty (pretty, text)
+import Util.Pretty (text)
 
 import Prelude hiding (id, (.))
 
-import Control.Applicative hiding (Const)
 import Control.Category
-import Control.DeepSeq
 import Control.Monad
-import Control.Monad.State.Strict as State
-import Data.Char (isLetter, toLower)
 import Data.List
-import Data.List.Split (splitOn)
-import qualified Data.Map as Map
 import Data.Maybe
-import qualified Data.Set as S
 import qualified Data.Text as T
-import Debug.Trace
-
 
 elabImplementation :: ElabInfo
                    -> SyntaxInfo
diff --git a/src/Idris/Elab/Interface.hs b/src/Idris/Elab/Interface.hs
index f08041122..96b274307 100644
--- a/src/Idris/Elab/Interface.hs
+++ b/src/Idris/Elab/Interface.hs
@@ -10,51 +10,22 @@ Maintainer  : The Idris Community.
 module Idris.Elab.Interface(elabInterface) where
 
 import Idris.AbsSyntax
-import Idris.ASTUtils
-import Idris.Core.CaseTree
-import Idris.Core.Elaborate hiding (Tactic(..))
 import Idris.Core.Evaluate
-import Idris.Core.Execute
 import Idris.Core.TT
-import Idris.Core.Typecheck
-import Idris.Coverage
-import Idris.DataOpts
-import Idris.DeepSeq
 import Idris.Delaborate
 import Idris.Docstrings
-import Idris.DSL
 import Idris.Elab.Data
-import Idris.Elab.Term
-import Idris.Elab.Type
 import Idris.Elab.Utils
 import Idris.Error
-import Idris.Imports
-import Idris.Inliner
-import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
-import Idris.PartialEval
-import Idris.Primitives
-import Idris.Providers
-import IRTS.Lang
-
-import Util.Pretty (pretty, text)
+import Idris.Output (sendHighlighting)
 
 import Prelude hiding (id, (.))
 
-import Control.Applicative hiding (Const)
 import Control.Category
-import Control.DeepSeq
 import Control.Monad
-import Control.Monad.State.Strict as State
-import Data.Char (isLetter, toLower)
 import Data.Generics.Uniplate.Data (transform)
 import Data.List
-import Data.List.Split (splitOn)
-import qualified Data.Map as Map
 import Data.Maybe
-import qualified Data.Set as S
-import qualified Data.Text as T
-import Debug.Trace
-
 
 data MArgTy = IA Name | EA Name | CA deriving Show
 
diff --git a/src/Idris/Elab/Provider.hs b/src/Idris/Elab/Provider.hs
index 5acabad3f..05c15568b 100644
--- a/src/Idris/Elab/Provider.hs
+++ b/src/Idris/Elab/Provider.hs
@@ -9,51 +9,24 @@ Maintainer  : The Idris Community.
 module Idris.Elab.Provider(elabProvider) where
 
 import Idris.AbsSyntax
-import Idris.ASTUtils
-import Idris.Core.CaseTree
-import Idris.Core.Elaborate hiding (Tactic(..))
 import Idris.Core.Evaluate
 import Idris.Core.Execute
 import Idris.Core.TT
 import Idris.Core.Typecheck
-import Idris.Coverage
-import Idris.DataOpts
-import Idris.DeepSeq
 import Idris.Delaborate
 import Idris.Docstrings
-import Idris.DSL
 import Idris.Elab.Clause
 import Idris.Elab.Term
 import Idris.Elab.Type
-import Idris.Elab.Utils
 import Idris.Elab.Value
 import Idris.Error
-import Idris.Imports
-import Idris.Inliner
 import Idris.Options
-import Idris.Output (iWarn, iputStrLn, pshow)
-import Idris.PartialEval
-import Idris.Primitives
 import Idris.Providers
-import IRTS.Lang
-
-import Util.Pretty (pretty, text)
 
 import Prelude hiding (id, (.))
 
-import Control.Applicative hiding (Const)
 import Control.Category
-import Control.DeepSeq
 import Control.Monad
-import Control.Monad.State.Strict as State
-import Data.Char (isLetter, toLower)
-import Data.List
-import Data.List.Split (splitOn)
-import qualified Data.Map as Map
-import Data.Maybe
-import qualified Data.Set as S
-import qualified Data.Text as T
-import Debug.Trace
 
 -- | Elaborate a type provider
 elabProvider :: Docstring (Either Err PTerm) -> ElabInfo -> SyntaxInfo -> FC -> FC -> ProvideWhat -> Name -> Idris ()
diff --git a/src/Idris/Elab/Record.hs b/src/Idris/Elab/Record.hs
index 7a2c28121..cf0d5bc61 100644
--- a/src/Idris/Elab/Record.hs
+++ b/src/Idris/Elab/Record.hs
@@ -11,25 +11,12 @@ module Idris.Elab.Record(elabRecord) where
 import Idris.AbsSyntax
 import Idris.Core.Evaluate
 import Idris.Core.TT
-import Idris.Coverage
-import Idris.DataOpts
-import Idris.DeepSeq
 import Idris.Delaborate
 import Idris.Docstrings
 import Idris.Elab.Data
-import Idris.Elab.Data
-import Idris.Elab.Term
-import Idris.Elab.Type
-import Idris.Elab.Utils
 import Idris.Error
-import Idris.Imports
-import Idris.Inliner
-import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
+import Idris.Output (sendHighlighting)
 import Idris.Parser.Expr (tryFullExpr)
-import Idris.PartialEval
-import Idris.Primitives
-import Idris.Providers
-import IRTS.Lang
 
 import Control.Monad
 import Data.List
diff --git a/src/Idris/Elab/Rewrite.hs b/src/Idris/Elab/Rewrite.hs
index 372739ec6..6cc0a9c04 100644
--- a/src/Idris/Elab/Rewrite.hs
+++ b/src/Idris/Elab/Rewrite.hs
@@ -10,7 +10,6 @@ Maintainer  : The Idris Community.
 module Idris.Elab.Rewrite(elabRewrite, elabRewriteLemma) where
 
 import Idris.AbsSyntax
-import Idris.AbsSyntaxTree
 import Idris.Core.Elaborate
 import Idris.Core.Evaluate
 import Idris.Core.TT
@@ -20,8 +19,6 @@ import Idris.Error
 
 import Control.Monad
 import Control.Monad.State.Strict
-import Data.List
-import Debug.Trace
 
 elabRewrite :: (PTerm -> ElabD ()) -> IState ->
                FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> ElabD ()
diff --git a/src/Idris/Elab/RunElab.hs b/src/Idris/Elab/RunElab.hs
index c5342943c..876da02bb 100644
--- a/src/Idris/Elab/RunElab.hs
+++ b/src/Idris/Elab/RunElab.hs
@@ -9,14 +9,12 @@ module Idris.Elab.RunElab (elabRunElab) where
 
 import Idris.AbsSyntax
 import Idris.Core.Elaborate hiding (Tactic(..))
-import Idris.Core.Evaluate
-import Idris.Core.Execute
 import Idris.Core.TT
 import Idris.Core.Typecheck
 import Idris.Elab.Term
 import Idris.Elab.Value (elabVal)
 import Idris.Error
-import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
+import Idris.Output (sendHighlighting)
 
 elabScriptTy :: Type
 elabScriptTy = App Complete (P Ref (sNS (sUN "Elab") ["Elab", "Reflection", "Language"]) Erased)
diff --git a/src/Idris/Elab/Term.hs b/src/Idris/Elab/Term.hs
index 0e2e4a0df..bb43d63bf 100644
--- a/src/Idris/Elab/Term.hs
+++ b/src/Idris/Elab/Term.hs
@@ -10,40 +10,34 @@ Maintainer  : The Idris Community.
 module Idris.Elab.Term where
 
 import Idris.AbsSyntax
-import Idris.AbsSyntaxTree
-import Idris.Core.CaseTree (SC, SC'(STerm), findCalls, findUsedArgs)
+import Idris.Core.CaseTree (SC'(STerm), findCalls)
 import Idris.Core.Elaborate hiding (Tactic(..))
 import Idris.Core.Evaluate
 import Idris.Core.ProofTerm (getProofTerm)
 import Idris.Core.TT
 import Idris.Core.Typecheck (check, converts, isType, recheck)
 import Idris.Core.Unify
-import Idris.Core.WHNF (whnf, whnfArgs)
-import Idris.Coverage (genClauses, recoverableCoverage, validCoverageCase)
+import Idris.Core.WHNF (whnf)
+import Idris.Coverage (genClauses, recoverableCoverage)
 import Idris.Delaborate
-import Idris.DSL
 import Idris.Elab.Quasiquote (extractUnquotes)
 import Idris.Elab.Rewrite
 import Idris.Elab.Utils
 import Idris.Error
 import Idris.ErrReverse (errReverse)
 import Idris.Options
-import Idris.Output (pshow)
 import Idris.ProofSearch
 import Idris.Reflection
 import Idris.Termination (buildSCG, checkDeclTotality, checkPositive)
 
-import qualified Util.Pretty as U
-
 import Control.Applicative ((<$>))
 import Control.Monad
 import Control.Monad.State.Strict
 import Data.Foldable (for_)
 import Data.List
 import qualified Data.Map as M
-import Data.Maybe (catMaybes, fromMaybe, mapMaybe, maybeToList)
+import Data.Maybe (fromMaybe, mapMaybe, maybeToList)
 import qualified Data.Set as S
-import qualified Data.Text as T
 import Debug.Trace
 
 data ElabMode = ETyDecl | ETransLHS | ELHS | EImpossible | ERHS
diff --git a/src/Idris/Elab/Transform.hs b/src/Idris/Elab/Transform.hs
index c49f38641..c35e08593 100644
--- a/src/Idris/Elab/Transform.hs
+++ b/src/Idris/Elab/Transform.hs
@@ -9,47 +9,19 @@ Maintainer  : The Idris Community.
 module Idris.Elab.Transform where
 
 import Idris.AbsSyntax
-import Idris.ASTUtils
-import Idris.Core.CaseTree
 import Idris.Core.Elaborate hiding (Tactic(..))
-import Idris.Core.Evaluate
-import Idris.Core.Execute
 import Idris.Core.TT
 import Idris.Core.Typecheck
-import Idris.Coverage
-import Idris.DataOpts
-import Idris.DeepSeq
-import Idris.Delaborate
-import Idris.Docstrings
-import Idris.DSL
 import Idris.Elab.Term
 import Idris.Elab.Utils
 import Idris.Error
-import Idris.Imports
-import Idris.Inliner
-import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
-import Idris.PartialEval
-import Idris.Primitives
-import Idris.Providers
-import IRTS.Lang
-
-import Util.Pretty (pretty, text)
+import Idris.Output (sendHighlighting)
 
 import Prelude hiding (id, (.))
 
-import Control.Applicative hiding (Const)
 import Control.Category
-import Control.DeepSeq
 import Control.Monad
 import Control.Monad.State.Strict as State
-import Data.Char (isLetter, toLower)
-import Data.List
-import Data.List.Split (splitOn)
-import qualified Data.Map as Map
-import Data.Maybe
-import qualified Data.Set as S
-import qualified Data.Text as T
-import Debug.Trace
 
 elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)
 elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in
diff --git a/src/Idris/Elab/Type.hs b/src/Idris/Elab/Type.hs
index b43a1918c..64bea8e28 100644
--- a/src/Idris/Elab/Type.hs
+++ b/src/Idris/Elab/Type.hs
@@ -13,50 +13,23 @@ module Idris.Elab.Type (
 
 import Idris.AbsSyntax
 import Idris.ASTUtils
-import Idris.Core.CaseTree
 import Idris.Core.Elaborate hiding (Tactic(..))
 import Idris.Core.Evaluate
-import Idris.Core.Execute
 import Idris.Core.TT
-import Idris.Core.Typecheck
 import Idris.Core.WHNF
-import Idris.Coverage
-import Idris.DataOpts
-import Idris.DeepSeq
-import Idris.Delaborate
 import Idris.Docstrings (Docstring)
-import Idris.DSL
 import Idris.Elab.Term
 import Idris.Elab.Utils
 import Idris.Elab.Value
 import Idris.Error
-import Idris.Imports
-import Idris.Inliner
 import Idris.Options
-import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
-import Idris.PartialEval
-import Idris.Primitives
-import Idris.Providers
-import IRTS.Lang
-
-import Util.Pretty (pretty, text)
+import Idris.Output (sendHighlighting)
 
 import Prelude hiding (id, (.))
 
-import Control.Applicative hiding (Const)
 import Control.Category
-import Control.DeepSeq
 import Control.Monad
-import Control.Monad.State.Strict as State
-import Data.Char (isLetter, toLower)
-import Data.List
-import Data.List.Split (splitOn)
-import qualified Data.Map as Map
-import Data.Maybe
 import qualified Data.Set as S
-import qualified Data.Text as T
-import qualified Data.Traversable as Traversable
-import Debug.Trace
 
 buildType :: ElabInfo
           -> SyntaxInfo
diff --git a/src/Idris/Elab/Utils.hs b/src/Idris/Elab/Utils.hs
index 6e6803f62..dcaf9a495 100644
--- a/src/Idris/Elab/Utils.hs
+++ b/src/Idris/Elab/Utils.hs
@@ -14,7 +14,6 @@ import Idris.Core.Evaluate
 import Idris.Core.TT
 import Idris.Core.Typecheck
 import Idris.Core.WHNF
-import Idris.DeepSeq
 import Idris.Delaborate
 import Idris.Docstrings
 import Idris.Error
@@ -22,14 +21,11 @@ import Idris.Output
 
 import Util.Pretty
 
-import Control.Applicative hiding (Const)
 import Control.Monad
 import Control.Monad.State
 import Data.List
 import qualified Data.Map as Map
 import Data.Maybe
-import qualified Data.Traversable as Traversable
-import Debug.Trace
 
 recheckC = recheckC_borrowing False True []
 
diff --git a/src/Idris/Elab/Value.hs b/src/Idris/Elab/Value.hs
index 84efcbae2..41c8f7084 100644
--- a/src/Idris/Elab/Value.hs
+++ b/src/Idris/Elab/Value.hs
@@ -13,48 +13,20 @@ module Idris.Elab.Value(
   ) where
 
 import Idris.AbsSyntax
-import Idris.ASTUtils
-import Idris.Core.CaseTree
 import Idris.Core.Elaborate hiding (Tactic(..))
 import Idris.Core.Evaluate hiding (Unchecked)
-import Idris.Core.Execute
 import Idris.Core.TT
-import Idris.Core.Typecheck
-import Idris.Coverage
-import Idris.DataOpts
-import Idris.DeepSeq
-import Idris.Delaborate
 import Idris.Docstrings
-import Idris.DSL
 import Idris.Elab.Term
 import Idris.Elab.Utils
 import Idris.Error
-import Idris.Imports
-import Idris.Inliner
-import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
-import Idris.PartialEval
-import Idris.Primitives
-import Idris.Providers
-import IRTS.Lang
-
-import Util.Pretty (pretty, text)
+import Idris.Output (sendHighlighting)
 
 import Prelude hiding (id, (.))
 
-import Control.Applicative hiding (Const)
 import Control.Category
-import Control.DeepSeq
-import Control.Monad
-import Control.Monad.State.Strict as State
-import Data.Char (isLetter, toLower)
-import Data.List
-import Data.List.Split (splitOn)
-import qualified Data.Map as Map
-import Data.Maybe
-import qualified Data.Set as S
-import qualified Data.Text as T
+import Data.Char (toLower)
 import qualified Data.Traversable as Traversable
-import Debug.Trace
 
 -- | Elaborate a value, returning any new bindings created (this will only
 -- happen if elaborating as a pattern clause)
diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs
index 0d631ab6c..03656546d 100644
--- a/src/Idris/ElabDecls.hs
+++ b/src/Idris/ElabDecls.hs
@@ -12,20 +12,10 @@ Maintainer  : The Idris Community.
 module Idris.ElabDecls where
 
 import Idris.AbsSyntax
-import Idris.ASTUtils
-import Idris.Core.CaseTree
-import Idris.Core.Elaborate hiding (Tactic(..))
 import Idris.Core.Evaluate
-import Idris.Core.Execute
 import Idris.Core.TT
-import Idris.Core.Typecheck
-import Idris.Coverage
-import Idris.DataOpts
-import Idris.DeepSeq
-import Idris.Delaborate
 import Idris.Directives
 import Idris.Docstrings hiding (Unchecked)
-import Idris.DSL
 import Idris.Elab.Clause
 import Idris.Elab.Data
 import Idris.Elab.Implementation
@@ -36,36 +26,21 @@ import Idris.Elab.RunElab
 import Idris.Elab.Term
 import Idris.Elab.Transform
 import Idris.Elab.Type
-import Idris.Elab.Utils
 import Idris.Elab.Value
 import Idris.Error
-import Idris.Imports
-import Idris.Inliner
 import Idris.Options
-import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
-import Idris.PartialEval
+import Idris.Output (sendHighlighting)
 import Idris.Primitives
-import Idris.Providers
 import Idris.Termination
 import IRTS.Lang
 
-import Util.Pretty (pretty, text)
-
 import Prelude hiding (id, (.))
 
-import Control.Applicative hiding (Const)
 import Control.Category
-import Control.DeepSeq
 import Control.Monad
 import Control.Monad.State.Strict as State
-import Data.Char (isLetter, toLower)
-import Data.List
-import Data.List.Split (splitOn)
-import qualified Data.Map as Map
 import Data.Maybe
-import qualified Data.Set as S
 import qualified Data.Text as T
-import Debug.Trace
 
 -- | Top level elaborator info, supporting recursive elaboration
 recinfo :: FC -> ElabInfo
diff --git a/src/Idris/Erasure.hs b/src/Idris/Erasure.hs
index 51c74d452..7429889df 100644
--- a/src/Idris/Erasure.hs
+++ b/src/Idris/Erasure.hs
@@ -20,7 +20,6 @@ import Idris.Primitives
 
 import Prelude hiding (id, (.))
 
-import Control.Applicative
 import Control.Arrow
 import Control.Category
 import Control.Monad.State
@@ -36,8 +35,6 @@ import Data.Set (Set)
 import qualified Data.Set as S
 import Data.Text (pack)
 import qualified Data.Text as T
-import Debug.Trace
-import System.IO.Unsafe
 
 -- | UseMap maps names to the set of used (reachable) argument
 -- positions.
diff --git a/src/Idris/ErrReverse.hs b/src/Idris/ErrReverse.hs
index 8d72e7cba..698ca596d 100644
--- a/src/Idris/ErrReverse.hs
+++ b/src/Idris/ErrReverse.hs
@@ -15,7 +15,6 @@ import Idris.Core.TT
 import Util.Pretty
 
 import Data.List
-import Debug.Trace
 
 -- | For display purposes, apply any 'error reversal' transformations
 -- so that errors will be more readable,
diff --git a/src/Idris/Error.hs b/src/Idris/Error.hs
index e44af6eab..c31ecaa06 100644
--- a/src/Idris/Error.hs
+++ b/src/Idris/Error.hs
@@ -14,23 +14,16 @@ import Idris.AbsSyntax
 import Idris.Core.Constraints
 import Idris.Core.Evaluate (ctxtAlist)
 import Idris.Core.TT
-import Idris.Core.Typecheck
 import Idris.Delaborate
 import Idris.Output
 
 import Prelude hiding (catch)
 
 import Control.Monad (when)
-import Control.Monad.State.Strict
-import Data.Char
 import qualified Data.Foldable as Foldable
 import Data.List (intercalate, isPrefixOf)
 import qualified Data.Set as S
 import qualified Data.Text as T
-import qualified Data.Traversable as Traversable
-import Data.Typeable
-import System.Console.Haskeline
-import System.Console.Haskeline.MonadException
 import System.IO.Error (ioeGetErrorString, isUserError)
 
 iucheck :: Idris ()
diff --git a/src/Idris/IdeMode.hs b/src/Idris/IdeMode.hs
index ce3422ff9..a14bcaf1f 100644
--- a/src/Idris/IdeMode.hs
+++ b/src/Idris/IdeMode.hs
@@ -11,7 +11,7 @@ Maintainer  : The Idris Community.
 
 module Idris.IdeMode(parseMessage, convSExp, WhatDocs(..), IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar, sExpToString) where
 
-import Idris.Core.Binary
+import Idris.Core.Binary ()
 import Idris.Core.TT
 
 import Control.Applicative hiding (Const)
diff --git a/src/Idris/IdrisDoc.hs b/src/Idris/IdrisDoc.hs
index f74ef41e9..eb370f47c 100644
--- a/src/Idris/IdrisDoc.hs
+++ b/src/Idris/IdrisDoc.hs
@@ -10,11 +10,10 @@ Maintainer  : The Idris Community.
 module Idris.IdrisDoc (generateDocs) where
 
 import Idris.AbsSyntax
-import Idris.Core.Evaluate (Accessibility(..), Def(..), ctxtAlist, isDConName,
-                            isFnName, isTConName, lookupDefAcc)
-import Idris.Core.TT (Name(..), OutputAnnotation(..), SpecialName(..),
-                      TextFormatting(..), constIsType, nsroot, sUN, str,
-                      toAlist, txt)
+import Idris.Core.Evaluate (Accessibility(..), ctxtAlist, isDConName, isFnName,
+                            isTConName, lookupDefAcc)
+import Idris.Core.TT (Name(..), OutputAnnotation(..), TextFormatting(..),
+                      constIsType, nsroot, sUN, str, toAlist, txt)
 import Idris.Docs
 import Idris.Docstrings (nullDocstring)
 import qualified Idris.Docstrings as Docstrings
@@ -26,17 +25,13 @@ import Control.Applicative ((<|>))
 import Control.Monad (forM_)
 import Control.Monad.Trans.Except
 import Control.Monad.Trans.State.Strict
-import qualified Data.ByteString as BS
 import qualified Data.ByteString.Lazy as BS2
 import qualified Data.List as L
-import qualified Data.List.Split as LS
 import qualified Data.Map as M hiding ((!))
 import Data.Maybe
 import Data.Monoid (mempty)
-import qualified Data.Ord (compare)
 import qualified Data.Set as S
 import qualified Data.Text as T
-import qualified Data.Text.Encoding as E
 import System.Directory
 import System.FilePath
 import System.IO
diff --git a/src/Idris/Imports.hs b/src/Idris/Imports.hs
index 3f1e4c084..b082f6c3b 100644
--- a/src/Idris/Imports.hs
+++ b/src/Idris/Imports.hs
@@ -13,7 +13,6 @@ module Idris.Imports(
 import Idris.AbsSyntax
 import Idris.Core.TT
 import Idris.Error
-import Idris.Output
 import IRTS.System (getIdrisLibDir)
 
 import Control.Applicative ((<$>))
diff --git a/src/Idris/Info.hs b/src/Idris/Info.hs
index 0d380a6ba..089c62c6e 100644
--- a/src/Idris/Info.hs
+++ b/src/Idris/Info.hs
@@ -29,7 +29,6 @@ import Idris.Imports (installedPackages)
 import Idris.Options (loggingCatsStr)
 import qualified IRTS.System as S
 
-import Paths_idris
 import Version_idris (gitHash)
 
 import Data.Version
diff --git a/src/Idris/Output.hs b/src/Idris/Output.hs
index 46550c719..e80028e3c 100644
--- a/src/Idris/Output.hs
+++ b/src/Idris/Output.hs
@@ -13,7 +13,7 @@ module Idris.Output where
 
 import Idris.AbsSyntax
 import Idris.Colours (hEndColourise, hStartColourise)
-import Idris.Core.Evaluate (isDConName, isFnName, isTConName, normaliseAll)
+import Idris.Core.Evaluate (normaliseAll)
 import Idris.Core.TT
 import Idris.Delaborate
 import Idris.Docstrings
@@ -27,13 +27,12 @@ import Util.System (isATTY)
 import Prelude hiding ((<$>))
 
 import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)
-import Data.Char (isAlpha)
 import Data.List (intersperse, nub)
 import Data.Maybe (fromMaybe)
 import System.Console.Haskeline.MonadException (MonadException(controlIO),
                                                 RunIO(RunIO))
 import System.FilePath (replaceExtension)
-import System.IO (Handle, hPutStr, hPutStrLn, stdout)
+import System.IO (Handle, hPutStr, hPutStrLn)
 
 instance MonadException m => MonadException (ExceptT Err m) where
     controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let
diff --git a/src/Idris/Package.hs b/src/Idris/Package.hs
index f7708ae95..85fa3dd63 100644
--- a/src/Idris/Package.hs
+++ b/src/Idris/Package.hs
@@ -12,7 +12,7 @@ import System.Directory
 import System.Directory (copyFile, createDirectoryIfMissing)
 import System.Exit
 import System.FilePath (addExtension, addTrailingPathSeparator, dropExtension,
-                        hasExtension, normalise, takeDirectory, takeExtension,
+                        hasExtension, takeDirectory, takeExtension,
                         takeFileName, (</>))
 import System.IO
 import System.Process
@@ -23,10 +23,8 @@ import Control.Monad
 import Control.Monad.Trans.Except (runExceptT)
 import Control.Monad.Trans.State.Strict (execStateT)
 import Data.Either (partitionEithers)
-import Data.Either (partitionEithers)
 import Data.List
 import Data.List.Split (splitOn)
-import Data.Maybe (fromMaybe)
 
 import Idris.AbsSyntax
 import Idris.Core.TT
@@ -38,7 +36,6 @@ import Idris.Main (idris, idrisMain)
 import Idris.Options
 import Idris.Output
 import Idris.Parser (loadModule)
-import Idris.REPL
 
 import Idris.Package.Common
 import Idris.Package.Parser
diff --git a/src/Idris/Package/Parser.hs b/src/Idris/Package/Parser.hs
index 102ec6aba..5da1465e7 100644
--- a/src/Idris/Package/Parser.hs
+++ b/src/Idris/Package/Parser.hs
@@ -8,19 +8,13 @@ Maintainer  : The Idris Community.
 {-# LANGUAGE CPP, ConstraintKinds, FlexibleInstances, TypeSynonymInstances #-}
 module Idris.Package.Parser where
 
-import Idris.AbsSyntaxTree
 import Idris.CmdOptions
-import Idris.Core.TT
 import Idris.Package.Common
 import Idris.Parser.Helpers hiding (stringLiteral)
-import Idris.REPL
-
-import Util.System
 
 import Control.Applicative
 import Control.Monad.State.Strict
 import Data.List (union)
-import Data.Maybe (fromJust, isNothing)
 import System.Directory (doesFileExist)
 import System.Exit
 import System.FilePath (isValid, takeExtension, takeFileName)
diff --git a/src/Idris/Parser/Data.hs b/src/Idris/Parser/Data.hs
index d15c7653a..38538eb7f 100644
--- a/src/Idris/Parser/Data.hs
+++ b/src/Idris/Parser/Data.hs
@@ -12,7 +12,6 @@ import Idris.AbsSyntax
 import Idris.Core.Evaluate
 import Idris.Core.TT
 import Idris.Docstrings
-import Idris.DSL
 import Idris.Options
 import Idris.Parser.Expr
 import Idris.Parser.Helpers
@@ -21,25 +20,11 @@ import Idris.Parser.Ops
 import Prelude hiding (pi)
 
 import Control.Applicative
-import Control.Monad
 import Control.Monad.State.Strict
-import qualified Data.ByteString.UTF8 as UTF8
-import Data.Char
-import qualified Data.HashSet as HS
 import Data.List
-import qualified Data.List.Split as Spl
 import Data.Maybe
-import Data.Monoid
-import qualified Data.Text as T
-import Debug.Trace
-import qualified Text.Parser.Char as Chr
-import Text.Parser.Expression
-import Text.Parser.LookAhead
-import qualified Text.Parser.Token as Tok
-import qualified Text.Parser.Token.Highlight as Hi
 import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,
                       stringLiteral, symbol, whiteSpace)
-import Text.Trifecta.Delta
 
 {- | Parses a record type declaration
 Record ::=
diff --git a/src/Idris/Parser/Expr.hs b/src/Idris/Parser/Expr.hs
index 134f63915..eb3eff09d 100644
--- a/src/Idris/Parser/Expr.hs
+++ b/src/Idris/Parser/Expr.hs
@@ -21,24 +21,12 @@ import Prelude hiding (pi)
 import Control.Applicative
 import Control.Monad
 import Control.Monad.State.Strict
-import qualified Data.ByteString.UTF8 as UTF8
-import Data.Char
 import Data.Function (on)
-import qualified Data.HashSet as HS
 import Data.List
-import qualified Data.List.Split as Spl
 import Data.Maybe
-import Data.Monoid
-import qualified Data.Text as T
-import Debug.Trace
-import qualified Text.Parser.Char as Chr
 import Text.Parser.Expression
-import Text.Parser.LookAhead
-import qualified Text.Parser.Token as Tok
-import qualified Text.Parser.Token.Highlight as Hi
 import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,
                       stringLiteral, symbol, whiteSpace)
-import Text.Trifecta.Delta
 
 -- | Allow implicit type declarations
 allowImp :: SyntaxInfo -> SyntaxInfo
diff --git a/src/Idris/Parser/Helpers.hs b/src/Idris/Parser/Helpers.hs
index 35b281df8..eeac0d342 100644
--- a/src/Idris/Parser/Helpers.hs
+++ b/src/Idris/Parser/Helpers.hs
@@ -18,8 +18,6 @@ import Idris.Docstrings
 import Idris.Options
 import Idris.Output (iWarn)
 
-import qualified Util.Pretty as Pretty (text)
-
 import Prelude hiding (pi)
 
 import Control.Applicative
@@ -29,15 +27,11 @@ import qualified Data.ByteString.UTF8 as UTF8
 import Data.Char
 import qualified Data.HashSet as HS
 import Data.List
-import qualified Data.List.Split as Spl
 import qualified Data.Map as M
 import Data.Maybe
-import Data.Monoid
 import qualified Data.Text as T
-import Debug.Trace
 import System.FilePath
 import qualified Text.Parser.Char as Chr
-import Text.Parser.Expression
 import Text.Parser.LookAhead
 import qualified Text.Parser.Token as Tok
 import qualified Text.Parser.Token.Highlight as Hi
diff --git a/src/Idris/Parser/Ops.hs b/src/Idris/Parser/Ops.hs
index b26835652..39e5bb132 100644
--- a/src/Idris/Parser/Ops.hs
+++ b/src/Idris/Parser/Ops.hs
@@ -18,23 +18,10 @@ import Prelude hiding (pi)
 import Control.Applicative
 import Control.Monad
 import Control.Monad.State.Strict
-import qualified Data.ByteString.UTF8 as UTF8
-import Data.Char
-import qualified Data.HashSet as HS
 import Data.List
-import qualified Data.List.Split as Spl
-import Data.Maybe
-import Data.Monoid
-import qualified Data.Text as T
-import Debug.Trace
-import qualified Text.Parser.Char as Chr
 import Text.Parser.Expression
-import Text.Parser.LookAhead
-import qualified Text.Parser.Token as Tok
-import qualified Text.Parser.Token.Highlight as Hi
 import Text.Trifecta hiding (char, charLiteral, natural, span, string,
                       stringLiteral, symbol, whiteSpace)
-import Text.Trifecta.Delta
 
 -- | Creates table for fixity declarations to build expression parser
 -- using pre-build and user-defined operator/fixity declarations
diff --git a/src/Idris/PartialEval.hs b/src/Idris/PartialEval.hs
index a1376aa96..d0c23a9a1 100644
--- a/src/Idris/PartialEval.hs
+++ b/src/Idris/PartialEval.hs
@@ -19,10 +19,7 @@ import Idris.Core.Evaluate
 import Idris.Core.TT
 import Idris.Delaborate
 
-import Control.Applicative
 import Control.Monad.State
-import Data.Maybe
-import Debug.Trace
 
 -- | Data type representing binding-time annotations for partial evaluation of arguments
 data PEArgType = ImplicitS Name -- ^ Implicit static argument
diff --git a/src/Idris/Primitives.hs b/src/Idris/Primitives.hs
index 882cd7149..477f52fb6 100644
--- a/src/Idris/Primitives.hs
+++ b/src/Idris/Primitives.hs
@@ -9,7 +9,6 @@ Maintainer  : The Idris Community.
 
 module Idris.Primitives(primitives, Prim(..)) where
 
-import Idris.AbsSyntax
 import Idris.Core.Evaluate
 import Idris.Core.TT
 import IRTS.Lang
@@ -18,9 +17,7 @@ import Data.Bits
 import Data.Char
 import Data.Function (on)
 import Data.Int
-import qualified Data.Vector.Unboxed as V
 import Data.Word
-import Debug.Trace
 
 data Prim = Prim { p_name  :: Name,
                    p_type  :: Type,
diff --git a/src/Idris/ProofSearch.hs b/src/Idris/ProofSearch.hs
index 06973adf9..e1a6204ff 100644
--- a/src/Idris/ProofSearch.hs
+++ b/src/Idris/ProofSearch.hs
@@ -16,14 +16,11 @@ module Idris.ProofSearch(
   ) where
 
 import Idris.AbsSyntax
-import Idris.Core.CaseTree
 import Idris.Core.Elaborate hiding (Tactic(..))
 import Idris.Core.Evaluate
 import Idris.Core.TT
-import Idris.Core.Typecheck
 import Idris.Core.Unify
 import Idris.Delaborate
-import Idris.Error
 
 import Control.Applicative ((<$>))
 import Control.Monad
diff --git a/src/Idris/Prover.hs b/src/Idris/Prover.hs
index 3d1569354..db0548f6b 100644
--- a/src/Idris/Prover.hs
+++ b/src/Idris/Prover.hs
@@ -11,12 +11,11 @@ module Idris.Prover (prover, showProof, showRunElab) where
 -- Hack for GHC 7.10 and earlier compat without CPP or warnings
 -- This exludes (<$>) as fmap, because wl-pprint uses it for newline
 import Prelude (Bool(..), Either(..), Eq(..), Maybe(..), Show(..), String,
-                concatMap, elem, error, flip, foldl, foldr, fst, id, init,
-                length, lines, map, not, null, repeat, reverse, tail, zip, ($),
-                (&&), (++), (.), (||))
+                concatMap, elem, error, foldl, foldr, fst, id, init, length,
+                lines, map, not, null, repeat, reverse, tail, zip, ($), (&&),
+                (++), (.), (||))
 
 import Idris.AbsSyntax
-import Idris.AbsSyntaxTree
 import Idris.Completion
 import Idris.Core.CaseTree
 import Idris.Core.Elaborate hiding (Tactic(..))
@@ -41,7 +40,6 @@ import Util.Pretty
 
 import Control.DeepSeq
 import Control.Monad.State.Strict
-import Debug.Trace
 import System.Console.Haskeline
 import System.Console.Haskeline.History
 import System.IO (Handle, hPutStrLn, stdin, stdout)
diff --git a/src/Idris/Providers.hs b/src/Idris/Providers.hs
index cc77e14e5..965491824 100644
--- a/src/Idris/Providers.hs
+++ b/src/Idris/Providers.hs
@@ -13,8 +13,6 @@ module Idris.Providers (
   ) where
 
 import Idris.AbsSyntax
-import Idris.AbsSyntaxTree
-import Idris.Core.Evaluate
 import Idris.Core.TT
 import Idris.Error
 
diff --git a/src/Idris/REPL/Parser.hs b/src/Idris/REPL/Parser.hs
index 77b21bcef..cdfcde7f8 100644
--- a/src/Idris/REPL/Parser.hs
+++ b/src/Idris/REPL/Parser.hs
@@ -21,17 +21,14 @@ import Idris.REPL.Commands
 
 import Control.Applicative
 import Control.Monad.State.Strict
-import qualified Data.ByteString.UTF8 as UTF8
 import Data.Char (isSpace, toLower)
 import Data.List
 import Data.List.Split (splitOn)
-import Debug.Trace
 import System.Console.ANSI (Color(..))
 import System.FilePath ((</>))
 import Text.Parser.Char (anyChar, oneOf)
 import Text.Parser.Combinators
-import Text.Trifecta (Result, parseString)
-import Text.Trifecta.Delta
+import Text.Trifecta (Result)
 
 parseCmd :: IState -> String -> String -> Result (Either String Command)
 parseCmd i inputname = P.runparser pCmd i inputname . trim
diff --git a/src/Idris/Termination.hs b/src/Idris/Termination.hs
index faecb04d8..a57e961ea 100644
--- a/src/Idris/Termination.hs
+++ b/src/Idris/Termination.hs
@@ -15,10 +15,9 @@ import Idris.Core.TT
 import Idris.Delaborate
 import Idris.Error
 import Idris.Options
-import Idris.Output (iWarn, iputStrLn)
+import Idris.Output (iWarn)
 
 import Control.Monad.State.Strict
-import Data.Char
 import Data.Either
 import Data.List
 import Data.Maybe
diff --git a/src/Idris/Transforms.hs b/src/Idris/Transforms.hs
index 6c7532a62..c372fc1bd 100644
--- a/src/Idris/Transforms.hs
+++ b/src/Idris/Transforms.hs
@@ -16,11 +16,8 @@ module Idris.Transforms(
   ) where
 
 import Idris.AbsSyntax
-import Idris.Core.CaseTree
 import Idris.Core.TT
 
-import Debug.Trace
-
 transformPats :: IState -> [Either Term (Term, Term)] ->
                 [Either Term (Term, Term)]
 transformPats ist ps = map tClause ps where
diff --git a/src/Idris/TypeSearch.hs b/src/Idris/TypeSearch.hs
index cfa72f4a9..99a00741e 100644
--- a/src/Idris/TypeSearch.hs
+++ b/src/Idris/TypeSearch.hs
@@ -14,7 +14,7 @@ module Idris.TypeSearch (
   ) where
 
 import Idris.AbsSyntax (addImpl, addUsingConstraints, getIState, implicit,
-                        logLvl, putIState)
+                        putIState)
 import Idris.AbsSyntaxTree (IState(idris_docstrings, idris_interfaces, idris_outputmode, tt_ctxt),
                             Idris, InterfaceInfo, OutputMode(..), PTerm,
                             defaultSyntax, eqTy, implicitAllowed,
diff --git a/src/Util/DynamicLinker.hs b/src/Util/DynamicLinker.hs
index 1119a97e5..08db317e9 100644
--- a/src/Util/DynamicLinker.hs
+++ b/src/Util/DynamicLinker.hs
@@ -13,22 +13,29 @@ module Util.DynamicLinker ( ForeignFun(..)
                           ) where
 
 #ifdef IDRIS_FFI
-import Foreign.LibFFI
-import Foreign.Ptr (FunPtr, Ptr, castPtrToFunPtr, nullFunPtr, nullPtr)
 import System.Directory
-#ifndef mingw32_HOST_OS
-import Control.Exception (IOException, throwIO, try)
-import Data.Array (Array, bounds, inRange, (!))
-import Data.Functor ((<$>))
-import Data.Maybe (catMaybes)
-import System.FilePath.Posix ((</>))
-import System.Posix.DynamicLinker
-import Text.Regex.TDFA
-#else
+#ifdef mingw32_HOST_OS
 import qualified Control.Exception as Exception (IOException, catch)
+import Foreign.Ptr (FunPtr, castPtrToFunPtr, nullFunPtr, nullPtr)
 import System.FilePath.Windows ((</>))
 import System.Win32.DLL
 import System.Win32.Types
+#else
+import Control.Exception (IOException, throwIO, try)
+import Foreign.Ptr (FunPtr, nullFunPtr, nullPtr)
+#ifdef linux_HOST_OS
+import Data.Array (bounds, inRange, (!))
+import Data.Functor ((<$>))
+import Data.Maybe (catMaybes)
+#else
+import Data.Array (bounds, (!))
+#endif
+import System.FilePath.Posix ((</>))
+import System.Posix.DynamicLinker
+import Text.Regex.TDFA
+#endif
+
+#ifdef mingw32_HOST_OS
 type DL = HMODULE
 #endif
 
diff --git a/stack.yaml b/stack.yaml
index 2c59b993e..459786f2d 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -9,6 +9,9 @@ flags:
     FFI: true
     GMP: true
 
+ghc-options:
+  idris: -fwarn-unused-imports -fwarn-unused-binds
+
 extra-deps:
   - binary-0.8.5.1
   - cheapskate-0.1.1

From 04d015141a51c9781442b64770355d8252e5defd Mon Sep 17 00:00:00 2001
From: Steven Shaw <steven@steshaw.org>
Date: Sun, 17 Sep 2017 11:37:36 +1000
Subject: [PATCH 22/27] Changelog entry for "hiding private functions".

See #1209.
---
 CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 753170cc2..41f31bc14 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,8 @@
 + In `@`-patterns such as `x@p`, `x` is now in scope on the right-hand side
   of any definitions in `where` clauses, provided the left-hand side of the
   definition does not shadow it.
++ Private functions are no longer visible in the REPL except for modules
+  that are explicitly loaded.
 
 # New in 1.1.1
 

From 83bb62fe530badd1ca1d0b665f767987335a889f Mon Sep 17 00:00:00 2001
From: Jason Felice <jason.m.felice@gmail.com>
Date: Sun, 17 Sep 2017 03:39:35 -0400
Subject: [PATCH 23/27] Unused binds (#4067)

---
 src/IRTS/CodegenC.hs                  | 13 +---
 src/IRTS/Defunctionalise.hs           | 52 +---------------
 src/IRTS/JavaScript/LangTransforms.hs |  5 --
 src/IRTS/JavaScript/Specialize.hs     | 11 ----
 src/Idris/AbsSyntax.hs                | 34 +----------
 src/Idris/AbsSyntaxTree.hs            | 15 -----
 src/Idris/Apropos.hs                  |  8 +--
 src/Idris/Chaser.hs                   |  3 -
 src/Idris/Completion.hs               |  5 --
 src/Idris/Core/CaseTree.hs            | 57 -----------------
 src/Idris/Core/Elaborate.hs           | 12 ----
 src/Idris/Core/Evaluate.hs            | 41 -------------
 src/Idris/Core/Execute.hs             | 35 +----------
 src/Idris/Core/ProofState.hs          | 66 +++-----------------
 src/Idris/Core/ProofTerm.hs           | 10 ---
 src/Idris/Core/TT.hs                  | 18 ------
 src/Idris/Core/Typecheck.hs           | 31 ----------
 src/Idris/Core/Unify.hs               | 88 ---------------------------
 src/Idris/Coverage.hs                 |  7 ---
 src/Idris/DSL.hs                      |  3 +-
 src/Idris/Delaborate.hs               |  9 +--
 src/Idris/Docs.hs                     |  4 --
 src/Idris/Elab/Clause.hs              | 39 ++----------
 src/Idris/Elab/Data.hs                | 23 +------
 src/Idris/Elab/Implementation.hs      |  4 --
 src/Idris/Elab/Interface.hs           | 16 +----
 src/Idris/Elab/Record.hs              | 26 --------
 src/Idris/Elab/Term.hs                | 52 +---------------
 src/Idris/Elab/Transform.hs           |  1 -
 src/Idris/Elab/Type.hs                | 13 ----
 src/Idris/Elab/Utils.hs               |  3 +-
 src/Idris/ElabDecls.hs                |  6 --
 src/Idris/Erasure.hs                  |  4 --
 src/Idris/ErrReverse.hs               | 11 ----
 src/Idris/IBC.hs                      | 13 +---
 src/Idris/IdeMode.hs                  |  3 -
 src/Idris/IdrisDoc.hs                 |  7 ---
 src/Idris/Imports.hs                  |  4 +-
 src/Idris/Interactive.hs              |  4 +-
 src/Idris/Package.hs                  |  2 -
 src/Idris/Parser.hs                   | 15 +----
 src/Idris/Parser/Data.hs              | 10 ---
 src/Idris/PartialEval.hs              |  4 --
 src/Idris/Primitives.hs               | 39 +-----------
 src/Idris/ProofSearch.hs              | 15 +----
 src/Idris/Prover.hs                   |  3 +-
 src/Idris/REPL.hs                     | 19 +-----
 src/Idris/REPL/Parser.hs              |  2 -
 src/Idris/Termination.hs              | 11 +---
 src/Idris/TypeSearch.hs               |  8 +--
 50 files changed, 43 insertions(+), 841 deletions(-)

diff --git a/src/IRTS/CodegenC.hs b/src/IRTS/CodegenC.hs
index a7c2aeaa3..39c76e320 100644
--- a/src/IRTS/CodegenC.hs
+++ b/src/IRTS/CodegenC.hs
@@ -201,11 +201,7 @@ bcc i (MKCON l loc tag args)
     = indent i ++ alloc loc tag ++
       indent i ++ setArgs 0 args ++ "\n" ++
       indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"
-
---         "MKCON(vm, " ++ creg l ++ ", " ++ show tag ++ ", " ++
---         show (length args) ++ concatMap showArg args ++ ");\n"
-  where showArg r = ", " ++ creg r
-        setArgs i [] = ""
+  where setArgs i [] = ""
         setArgs i (x : xs) = "SETARG(" ++ creg Tmp ++ ", " ++ show i ++ ", " ++ creg x ++
                              "); " ++ setArgs (i + 1) xs
         alloc Nothing tag
@@ -301,13 +297,6 @@ bcc i (CONSTCASE r code def)
     iCase v (B64 w, bc) =
         indent i ++ "if (GETBITS64(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
            ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
-    showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"
-                         ++ concatMap (bcc (i+1)) bc ++
-                            indent (i + 1) ++ "break;\n"
-    showDef i Nothing = ""
-    showDef i (Just c) = indent i ++ "default:\n"
-                         ++ concatMap (bcc (i+1)) c ++
-                            indent (i + 1) ++ "break;\n"
     showDefS i Nothing = ""
     showDefS i (Just c) = concatMap (bcc (i+1)) c
 
diff --git a/src/IRTS/Defunctionalise.hs b/src/IRTS/Defunctionalise.hs
index 500ad08b6..26340a888 100644
--- a/src/IRTS/Defunctionalise.hs
+++ b/src/IRTS/Defunctionalise.hs
@@ -164,32 +164,6 @@ addApps defs (n, LFun _ _ args e)
 --          = chainAPPLY (DApp False (sMN 0 "APPLY2") [f, a, b]) as
     chainAPPLY f (a : as) = chainAPPLY (DApp False (sMN 0 "APPLY") [f, a]) as
 
-    -- if anything in the DExp is projected from, we'll need to evaluate it,
-    -- but we only want to do it once, rather than every time we project.
-
-    preEval [] t = t
-    preEval (x : xs) t
-       | needsEval x t = DLet x (DV x) (preEval xs t)
-       | otherwise = preEval xs t
-
-    needsEval x (DApp _ _ args) = any (needsEval x) args
-    needsEval x (DC _ _ _ args) = any (needsEval x) args
-    needsEval x (DCase up e alts) = needsEval x e || any nec alts
-      where nec (DConCase _ _ _ e) = needsEval x e
-            nec (DConstCase _ e) = needsEval x e
-            nec (DDefaultCase e) = needsEval x e
-    needsEval x (DChkCase e alts) = needsEval x e || any nec alts
-      where nec (DConCase _ _ _ e) = needsEval x e
-            nec (DConstCase _ e) = needsEval x e
-            nec (DDefaultCase e) = needsEval x e
-    needsEval x (DLet n v e)
-          | x == n = needsEval x v
-          | otherwise = needsEval x v || needsEval x e
-    needsEval x (DForeign _ _ args) = any (needsEval x) (map snd args)
-    needsEval x (DOp op args) = any (needsEval x) args
-    needsEval x (DProj (DV x') _) = x == x'
-    needsEval x _ = False
-
 eEVAL x = DApp False (sMN 0 "EVAL") [x]
 
 data EvalApply a = EvalCase (Name -> a)
@@ -221,7 +195,6 @@ toConsA ns (n, i)
 --                 (DApp False n (map DV (take i (genArgs 0))))))))
           = mkApplyCase n ar i
     | otherwise = []
-  where dupdate tlarg x = x
 
 mkApplyCase fname n ar | n == ar = []
 mkApplyCase fname n ar
@@ -330,30 +303,7 @@ instance Show DExp where
 -- 'max' branches
 mkBigCase cn max arg branches
    | length branches <= max = DChkCase arg branches
-   | otherwise = -- DChkCase arg branches -- until I think of something...
-       -- divide the branches into groups of at most max (by tag),
-       -- generate a new case and shrink, recursively
-       let bs = sortBy tagOrd branches
-           (all, def) = case (last bs) of
-                    DDefaultCase t -> (init all, Just (DDefaultCase t))
-                    _ -> (all, Nothing)
-           bss = groupsOf max all
-           cs = map mkCase bss in
-           DChkCase arg branches
-
-    where mkCase bs = DChkCase arg bs
-
-          tagOrd (DConCase t _ _ _) (DConCase t' _ _ _) = compare t t'
-          tagOrd (DConstCase c _) (DConstCase c' _) = compare c c'
-          tagOrd (DDefaultCase _) (DDefaultCase _) = EQ
-
-          tagOrd (DConCase _ _ _ _) (DDefaultCase _) = LT
-          tagOrd (DConCase _ _ _ _) (DConstCase _ _) = LT
-          tagOrd (DConstCase _ _) (DDefaultCase _) = LT
-
-          tagOrd (DDefaultCase _) (DConCase _ _ _ _) = GT
-          tagOrd (DConstCase _ _) (DConCase _ _ _ _) = GT
-          tagOrd (DDefaultCase _) (DConstCase _ _) = GT
+   | otherwise = DChkCase arg branches
 
 groupsOf :: Int -> [DAlt] -> [[DAlt]]
 groupsOf x [] = []
diff --git a/src/IRTS/JavaScript/LangTransforms.hs b/src/IRTS/JavaScript/LangTransforms.hs
index 7560bbd0e..f6a6013fc 100644
--- a/src/IRTS/JavaScript/LangTransforms.hs
+++ b/src/IRTS/JavaScript/LangTransforms.hs
@@ -44,11 +44,6 @@ deriving instance Data LOpt
 restrictKeys :: Ord k => Map k a -> Set k -> Map k a
 restrictKeys m s = Map.filterWithKey (\k _ -> k `Set.member` s) m
 
-mapMapListKeys :: Ord k => (a->a) -> [k] -> Map k a -> Map k a
-mapMapListKeys _ [] x = x
-mapMapListKeys f (t:r) x = mapMapListKeys f r $ Map.adjust f t x
-
-
 extractGlobs :: Map Name LDecl -> LDecl -> [Name]
 extractGlobs defs (LConstructor _ _ _) = []
 extractGlobs defs (LFun _ _ _ e) =
diff --git a/src/IRTS/JavaScript/Specialize.hs b/src/IRTS/JavaScript/Specialize.hs
index 910836bbe..6189b1c3b 100644
--- a/src/IRTS/JavaScript/Specialize.hs
+++ b/src/IRTS/JavaScript/Specialize.hs
@@ -59,23 +59,12 @@ constructorOptimizeDB =
     ]
     -- constructors
   where
-    nil = const $ JsArray []
-    cons [h, t] = JsMethod (JsArray [h]) "concat" [t]
-    -- tests
-    --trueTest e = JsUniOp (T.pack "!") $ JsUniOp (T.pack "!") e
     trueTest = id
     falseTest e = JsUniOp (T.pack "!") e
-    emptyList e = JsBinOp "===" (JsProp e "length") (JsInt 0)
-    fillList e = JsBinOp ">" (JsProp e "length") (JsInt 0)
     ltTest e = JsBinOp "<" e (JsInt 0)
     eqTest e = JsBinOp "===" e (JsInt 0)
     gtTest e = JsBinOp ">" e (JsInt 0)
-    noneTest e = JsBinOp "===" e JsUndefined
-    notNoneTest e = JsBinOp "!==" e JsUndefined
     -- projections
-    justProj x n = x
-    uncons x 1 = JsArrayProj (JsInt 0) x
-    uncons x 2 = JsMethod x "slice" [JsInt 1]
     cantProj x j = error $ "This type should be projected"
     item :: String
          -> String
diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs
index 71c74a3c9..060c4e910 100644
--- a/src/Idris/AbsSyntax.hs
+++ b/src/Idris/AbsSyntax.hs
@@ -1465,28 +1465,7 @@ expandImplementationScope ist dec ps ns d = d
 -- * if there's a function type, next (2)
 -- * finally, everything else (3)
 getPriority :: IState -> PTerm -> Int
-getPriority i tm = 1 -- pri tm
-  where
-    pri (PRef _ _ n) =
-        case lookupP n (tt_ctxt i) of
-            ((P (DCon _ _ _) _ _):_) -> 1
-            ((P (TCon _ _) _ _):_) -> 1
-            ((P Ref _ _):_) -> 1
-            [] -> 0 -- must be locally bound, if it's not an error...
-    pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))
-    pri (PTrue _ _) = 0
-    pri (PRewrite _ _ l r _) = max 1 (max (pri l) (pri r))
-    pri (PApp _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
-    pri (PAppBind _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))
-    pri (PCase _ f as) = max 1 (max (pri f) (foldr (max . pri . snd) 0 as))
-    pri (PTyped l r) = pri l
-    pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))
-    pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
-    pri (PAlternative _ a as) = maximum (map pri as)
-    pri (PConstant _ _) = 0
-    pri Placeholder = 1
-    pri _ = 3
-
+getPriority i tm = 1
 
 addStatics :: Name -> Term -> PTerm -> Idris ()
 addStatics n tm ptm =
@@ -2013,9 +1992,6 @@ aiFn topname inpat True qq imp_meths ist fc f ffc ds []
           unqualified (NS _ _) = False
           unqualified _ = True
 
-          constructor (TyDecl (DCon _ _ _) _) = True
-          constructor _ = False
-
           conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia
 
           vname (UN n) = True -- non qualified
@@ -2202,12 +2178,8 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
        -- check will not necessarily fully resolve constructor names,
        -- and these bare names will otherwise get in the way of
        -- impossbility checking.
-       | -- Just fn <- getFn f,
-         canBeDConName fn ctxt
+       | canBeDConName fn ctxt
           = PApp fc f (fmap (fmap su) args)
-      where getFn (PRef _ _ fn) = Just fn
-            getFn (PApp _ f args) = getFn f
-            getFn _ = Nothing
     su (PApp fc f args)
           = PHidden (PApp fc f args)
     su (PAlternative ms b alts)
@@ -2264,8 +2236,6 @@ findStatics ist tm = let (ns, ss) = fs tm
                               (ns, ss)
         fs _ = ([], [])
 
-        inOne n ns = length (filter id (map (elem n) ns)) == 1
-
         pos ns ss (PPi p n fc t sc)
             | elem n ss = do sc' <- pos ns ss sc
                              spos <- get
diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs
index a4b10ec6b..f234638c8 100644
--- a/src/Idris/AbsSyntaxTree.hs
+++ b/src/Idris/AbsSyntaxTree.hs
@@ -2200,7 +2200,6 @@ showName ist bnd ppo colour n = case ist of
           showbasic (MN i s)  = str s
           showbasic (NS n s)  = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
           showbasic (SN s)    = show s
-          fst3 (x, _, _) = x
           colourise n t = let ctxt' = fmap tt_ctxt ist in
                           case ctxt' of
                             Nothing -> name
@@ -2348,20 +2347,6 @@ implicitNamesIn uvars ist tm
     addFn n = do (imps, fns) <- get
                  put (imps, n: fns)
 
-    notCAF []                 = False
-    notCAF (PExp _ _ _ _ : _) = True
-    notCAF (_ : xs)           = notCAF xs
-
-    notHidden (n, _) = case getAccessibility n of
-                            Hidden  -> False
-                            Private -> False
-                            _       -> True
-
-    getAccessibility n
-             = case lookupDefAccExact n False (tt_ctxt ist) of
-                    Just (n,t)  -> t
-                    _           -> Public
-
     ni 0 env (PRef _ _ n@(NS _ _))
         | not (n `elem` env)
           -- Never implicitly bind if there's a namespace
diff --git a/src/Idris/Apropos.hs b/src/Idris/Apropos.hs
index e22e33228..91446286e 100644
--- a/src/Idris/Apropos.hs
+++ b/src/Idris/Apropos.hs
@@ -11,7 +11,7 @@ module Idris.Apropos (apropos, aproposModules) where
 import Idris.AbsSyntax
 import Idris.Core.Evaluate (Def(..), ctxtAlist)
 import Idris.Core.TT (Binder(..), Const(..), Name(..), NameType(..), TT(..),
-                      Type, toAlist)
+                      toAlist)
 import Idris.Docstrings (DocTerm, Docstring, containsText)
 
 import Data.List (intersperse, nub, nubBy)
@@ -104,9 +104,3 @@ instance (Apropos a) => Apropos (Maybe a) where
 
 instance (Apropos a) => Apropos [a] where
   isApropos str xs = any (isApropos str) xs
-
-defType :: Def -> Type
-defType (Function t _) = t
-defType (TyDecl _ t) = t
-defType (Operator t _ _) = t
-defType (CaseOp _ t _ _ _ _) = t
diff --git a/src/Idris/Chaser.hs b/src/Idris/Chaser.hs
index 49cc280e8..da81d5936 100644
--- a/src/Idris/Chaser.hs
+++ b/src/Idris/Chaser.hs
@@ -58,9 +58,6 @@ getModuleFiles ts = nub $ execState (modList ts) [] where
 --                 when (not (ibc p) || rechk) $
                 mapM_ (modTree (getSrc p : path)) deps
 
-   ibc (IBC _ _) = True
-   ibc _ = False
-
    chkReload False p = p
    chkReload True (IBC fn src) = chkReload True src
    chkReload True p = p
diff --git a/src/Idris/Completion.hs b/src/Idris/Completion.hs
index d819f60f3..eb679bd8b 100644
--- a/src/Idris/Completion.hs
+++ b/src/Idris/Completion.hs
@@ -67,11 +67,6 @@ metavars :: Idris [String]
 metavars = do i <- get
               return . map (show . nsroot) $ map fst (filter (\(_, (_,_,_,t,_)) -> not t) (idris_metavars i)) \\ primDefs
 
-
-modules :: Idris [String]
-modules = do i <- get
-             return $ map show $ imported i
-
 namespaces :: Idris [String]
 namespaces = do
   ctxt <- fmap tt_ctxt get
diff --git a/src/Idris/Core/CaseTree.hs b/src/Idris/Core/CaseTree.hs
index 67bd9860d..15bef022d 100644
--- a/src/Idris/Core/CaseTree.hs
+++ b/src/Idris/Core/CaseTree.hs
@@ -268,7 +268,6 @@ simpleCase tc defcase reflect phase fc inacc argtys cs erInfo
                  = return $ CaseDef [] (UnmatchedCase (show fc ++ ":No pattern clauses")) []
  sc' tc defcase phase fc cs
       = let proj       = phase == RunTime
-            vnames     = fstT (head cs)
             pats       = map (\ (avs, l, r) ->
                                    (avs, toPats reflect tc l, (l, r))) cs
             chkPats    = mapM chkAccessible pats in
@@ -285,10 +284,7 @@ simpleCase tc defcase reflect phase fc inacc argtys cs erInfo
                                 else return t
                 Error err -> Error (At fc err)
     where args = map (\i -> sMN i "e") [0..]
-          defaultCase True = STerm Erased
-          defaultCase False = UnmatchedCase "Error"
           fstT (x, _, _) = x
-          lstT (_, _, x) = x
 
           -- Check that all pattern variables are reachable by a case split
           -- Otherwise, they won't make sense on the RHS.
@@ -303,48 +299,6 @@ simpleCase tc defcase reflect phase fc inacc argtys cs erInfo
           acc (PSuc p : xs) n = acc (p : xs) n
           acc (_ : xs) n = acc xs n
 
--- For each 'Case', make sure every choice is in the same type family,
--- as directed by the variable type (i.e. there is no implicit type casing
--- going on).
-
-checkSameTypes :: [(Name, Type)] -> SC -> Bool
-checkSameTypes tys (Case _ n alts)
-        = case lookup n tys of
-               Just t -> and (map (checkAlts t) alts)
-               _ -> and (map ((checkSameTypes tys).getSC) alts)
-  where
-    checkAlts t (ConCase n _ _ sc) = isType n t && checkSameTypes tys sc
-    checkAlts (Constant t) (ConstCase c sc) = isConstType c t && checkSameTypes tys sc
-    checkAlts _ (ConstCase c sc) = False
-    checkAlts _ _ = True
-
-    getSC (ConCase _ _ _ sc) = sc
-    getSC (FnCase _ _ sc) = sc
-    getSC (ConstCase _ sc) = sc
-    getSC (SucCase _ sc) = sc
-    getSC (DefaultCase sc) = sc
-checkSameTypes _ _ = True
-
--- FIXME: All we're actually doing here is checking that we haven't arrived
--- at a specific constructor for a polymorphic argument. I *think* this
--- is sufficient, but if it turns out not to be, fix it!
---
--- Issue #1718 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1718
-isType n t | (P (TCon _ _) _ _, _) <- unApply t = True
-isType n t | (P Ref _ _, _) <- unApply t = True
-isType n t = False
-
-isConstType (I _) (AType (ATInt ITNative)) = True
-isConstType (BI _) (AType (ATInt ITBig)) = True
-isConstType (Fl _) (AType ATFloat) = True
-isConstType (Ch _) (AType (ATInt ITChar)) = True
-isConstType (Str _) StrType = True
-isConstType (B8 _) (AType (ATInt _)) = True
-isConstType (B16 _) (AType (ATInt _)) = True
-isConstType (B32 _) (AType (ATInt _)) = True
-isConstType (B64 _) (AType (ATInt _)) = True
-isConstType _ _ = False
-
 data Pat = PCon Bool Name Int [Pat]
          | PConst Const
          | PInferred Pat
@@ -400,12 +354,6 @@ toPat reflect tc = map $ toPat' []
 
     toPat' _ t = PAny
 
-    fixedN IT8 = "Bits8"
-    fixedN IT16 = "Bits16"
-    fixedN IT32 = "Bits32"
-    fixedN IT64 = "Bits64"
-
-
 data Partition = Cons [Clause]
                | Vars [Clause]
     deriving Show
@@ -663,9 +611,6 @@ argsToAlt inacc rs@((r, m) : rest) = do
       where
         (acc, inacc) = partitionAcc r
 
-    uniq i (UN n) = MN i n
-    uniq i n = n
-
 getVar :: String -> CaseBuilder Name
 getVar b = do (t, v, ntys) <- get; put (t, v+1, ntys); return (sMN v b)
 
@@ -869,5 +814,3 @@ mkForce = mkForceSC
         = SucCase sn (mkForceSC n arg rhs)
     mkForceAlt n arg (DefaultCase rhs)
         = DefaultCase (mkForceSC n arg rhs)
-
-    forceTm n arg t = subst n arg t
diff --git a/src/Idris/Core/Elaborate.hs b/src/Idris/Core/Elaborate.hs
index 282722bd7..8ae5e889b 100644
--- a/src/Idris/Core/Elaborate.hs
+++ b/src/Idris/Core/Elaborate.hs
@@ -607,9 +607,6 @@ prepare_apply fn imps =
                         lift $ tfail $ TooManyArguments n
             | otherwise = fail $ "Too many arguments for " ++ show fn
 
-    doClaim ((i, _), n, t) = do claim n t
-                                when i (movelast n)
-
     mkMN n@(MN i _) = n
     mkMN n@(UN x) = MN 99999 x
     mkMN n@(SN s) = sMN 99999 (show s)
@@ -666,8 +663,6 @@ apply' fillt fn imps =
            | i = getNonUnify acc is as
            | otherwise = getNonUnify (t : acc) is as
 
---         getNonUnify imps args = map fst (filter (not . snd) (zip (map snd args) (map fst imps)))
-
 
 apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()
 apply2 fn elabs =
@@ -675,7 +670,6 @@ apply2 fn elabs =
        fill (raw_apply fn (map (Var . snd) args))
        elabArgs (map snd args) elabs
        ES (p, a) s prev <- get
-       let (n, hs) = unified p
        end_unify
        solve
   where elabArgs [] [] = return $! ()
@@ -693,16 +687,10 @@ apply_elab n args =
        env <- get_env
        claims <- doClaims (normalise ctxt env ty) args []
        prep_fill n (map fst claims)
-       let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims
        elabClaims [] False claims
        complete_fill
        end_unify
   where
-    priOrder Nothing Nothing = EQ
-    priOrder Nothing _ = LT
-    priOrder _ Nothing = GT
-    priOrder (Just (x, _)) (Just (y, _)) = compare x y
-
     doClaims (Bind n' (Pi _ _ t _) sc) (i : is) claims =
         do n <- unique_hole (mkMN n')
            when (null claims) (start_unify n)
diff --git a/src/Idris/Core/Evaluate.hs b/src/Idris/Core/Evaluate.hs
index 5107f0aa9..c7a866fe7 100644
--- a/src/Idris/Core/Evaluate.hs
+++ b/src/Idris/Core/Evaluate.hs
@@ -206,16 +206,6 @@ unfold ctxt env ns t
 finalEntry :: (Name, RigCount, Binder (TT Name)) -> (Name, RigCount, Binder (TT Name))
 finalEntry (n, r, b) = (n, r, fmap finalise b)
 
-bindEnv :: EnvTT n -> TT n -> TT n
-bindEnv [] tm = tm
-bindEnv ((n, r, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)
-bindEnv ((n, r, b):bs)       tm = Bind n b (bindEnv bs tm)
-
-unbindEnv :: EnvTT n -> TT n -> TT n
-unbindEnv [] tm = tm
-unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
-unbindEnv env tm = error "Impossible case occurred: couldn't unbind env."
-
 usable :: Bool -- specialising
           -> Bool -- unfolding only
           -> Int -- Reduction depth limit (when simplifying/at REPL)
@@ -393,22 +383,6 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
     evApply ntimes stk top env args f
           = apply ntimes stk top env f args
 
-    reapply ntimes stk top env f@(VP Ref n ty) args
-       = let val = lookupDefAccExact n (spec || (atRepl && noFree env) || runtime) ctxt in
-         case val of
-              Just (CaseOp ci _ _ _ _ cd, acc) ->
-                 let (ns, tree) = getCases cd in
-                     do c <- evCase ntimes n (n:stk) top env ns args tree
-                        case c of
-                             (Nothing, _) -> return $ unload env (VP Ref n ty) args
-                             (Just v, rest) -> evApply ntimes stk top env rest v
-              _ -> case args of
-                        (a : as) -> return $ unload env f (a : as)
-                        [] -> return f
-    reapply ntimes stk top env (VApp f a) args
-            = reapply ntimes stk top env f (a : args)
-    reapply ntimes stk top env v args = return v
-
     apply ntimes stk top env (VBind True n (Lam _ t) sc) (a:as)
          = do a' <- sc a
               app <- apply ntimes stk top env a' as
@@ -741,13 +715,6 @@ convEq ctxt holes topx topy = ceq [] topx topy where
                                   (caseeq ((x,y):ps) xdef ydef)
                  _ -> return False
 
--- SPECIALISATION -----------------------------------------------------------
--- We need too much control to be able to do this by tweaking the main
--- evaluator
-
-spec :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval (TT Name)
-spec ctxt statics genv tm = error "spec undefined"
-
 -- CONTEXTS -----------------------------------------------------------------
 
 {-| A definition is either a simple function (just an expression with a type),
@@ -985,7 +952,6 @@ addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)
                      CaseDef args_rt sc_rt _) ->
                        let inl = alwaysInline -- tcdict
                            inlc = (inl || small n args_ct sc_ct) && (not asserted)
-                           inlr = inl || small n args_rt sc_rt
                            cdef = CaseDefs (args_ct, sc_ct)
                                            (args_rt, sc_rt)
                            op = (CaseOp (ci { case_inlinable = inlc })
@@ -1249,13 +1215,6 @@ linearCheckArg ctxt ty = mapM_ checkNameOK (allTTNames ty)
                   tfail $ Msg $ show f ++ " can only appear in a linear binding"
               _ -> return ()
 
-    checkArgs (Bind n (Pi RigW _ ty _) sc)
-        = do mapM_ checkNameOK (allTTNames ty)
-             checkArgs (substV (P Bound n Erased) sc)
-    checkArgs (Bind n (Pi _ _ _ _) sc)
-          = checkArgs (substV (P Bound n Erased) sc)
-    checkArgs _ = return ()
-
 -- Check if a name is reducible in the type checker. Partial definitions
 -- are not reducible (so treated as a constant)
 tcReducible :: Name -> Context -> Bool
diff --git a/src/Idris/Core/Execute.hs b/src/Idris/Core/Execute.hs
index 29dcf19be..fa0ef07c0 100644
--- a/src/Idris/Core/Execute.hs
+++ b/src/Idris/Core/Execute.hs
@@ -45,10 +45,6 @@ execute :: Term -> Idris Term
 execute tm = fail "libffi not supported, rebuild Idris with -f FFI"
 #else
 -- else is rest of file
-readMay :: (Read a) => String -> Maybe a
-readMay s = case reads s of
-              [(x, "")] -> Just x
-              _         -> Nothing
 
 data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show
 
@@ -164,9 +160,6 @@ runExec ex st = fst <$> runStateT (runExceptT ex) st
 getExecState :: Exec ExecState
 getExecState = lift get
 
-putExecState :: ExecState -> Exec ()
-putExecState = lift . put
-
 execFail :: Err -> Exec a
 execFail = throwE
 
@@ -475,8 +468,8 @@ execForeign env ctxt arity ty fn xs onfail
 execForeign env ctxt arity ty fn xs onfail
    = case foreignFromTT arity ty fn xs of
         Just ffun@(FFun f argTs retT) | length xs >= arity ->
-           do let (args', xs') = (take arity xs, -- foreign args
-                                  drop arity xs) -- rest
+           do let (_, xs') = (take arity xs, -- foreign args
+                              drop arity xs) -- rest
               res <- call ffun (map snd argTs)
               case res of
                    Nothing -> fail $ "Could not call foreign function \"" ++ f ++
@@ -704,26 +697,6 @@ foreignFromTT arity ty (EConstant (Str name)) args
          return $ FFun name argFTyVals (toFDesc ty)
 foreignFromTT arity ty fn args = trace ("failed to construct ffun from " ++ show (ty,fn,args)) Nothing
 
-getFTy :: ExecVal -> Maybe FType
-getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))
-  | fi == txt "FIntT" =
-    case str intTy of
-      "ITNative" -> Just (FArith (ATInt ITNative))
-      "ITChar" -> Just (FArith (ATInt ITChar))
-      "IT8" -> Just (FArith (ATInt (ITFixed IT8)))
-      "IT16" -> Just (FArith (ATInt (ITFixed IT16)))
-      "IT32" -> Just (FArith (ATInt (ITFixed IT32)))
-      "IT64" -> Just (FArith (ATInt (ITFixed IT64)))
-      _ -> Nothing
-getFTy (EP _ (UN t) _) =
-    case str t of
-      "FFloat"  -> Just (FArith ATFloat)
-      "FString" -> Just FString
-      "FPtr"    -> Just FPtr
-      "FUnit"   -> Just FUnit
-      _         -> Nothing
-getFTy _ = Nothing
-
 unEList :: ExecVal -> Maybe [ExecVal]
 unEList tm = case unApplyV tm of
                (nil, [_]) -> Just []
@@ -733,10 +706,6 @@ unEList tm = case unApplyV tm of
                (f, args) -> Nothing
 
 
-toConst :: Term -> Maybe Const
-toConst (Constant c) = Just c
-toConst _ = Nothing
-
 mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]
 mapMaybeM f [] = return []
 mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs
diff --git a/src/Idris/Core/ProofState.hs b/src/Idris/Core/ProofState.hs
index 4ea2f4e4b..c792e95ca 100644
--- a/src/Idris/Core/ProofState.hs
+++ b/src/Idris/Core/ProofState.hs
@@ -179,7 +179,6 @@ match_unify' :: Context -> Env ->
 match_unify' ctxt env (topx, xfrom) (topy, yfrom) =
    do ps <- get
       let while = while_elaborating ps
-      let dont = dontunify ps
       let inj = injective ps
       traceWhen (unifylog ps)
                 ("Matching " ++ show (topx, topy) ++
@@ -492,15 +491,6 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
                   Nothing -> error ("deferType can't find " ++ show n)
 deferType _ _ _ _ _ _ = fail "Can't defer a non-hole focus."
 
-regret :: RunTactic
-regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
-    do action (\ps -> let hs = holes ps in
-                          ps { holes = hs \\ [x] })
-       return sc
-regret ctxt env (Bind x (Hole t) _)
-    = fail $ show x ++ " : " ++ show t ++ " is not solved..."
-regret _ _ _ = fail "The current focus is not a hole."
-
 unifyGoal :: Raw -> RunTactic
 unifyGoal tm ctxt env h@(Bind x b sc) =
     do (tmv, _) <- lift $ check ctxt env tm
@@ -527,14 +517,8 @@ exact _ _ _ _ = fail "Can't fill here."
 fill :: Raw -> RunTactic
 fill guess ctxt env (Bind x (Hole ty) sc) =
     do (val, valty) <- lift $ check ctxt env guess
---        let valtyn = normalise ctxt env valty
---        let tyn = normalise ctxt env ty
-       ns <- unify' ctxt env (valty, Just $ SourceTerm val)
-                             (ty, Just (chkPurpose val ty))
-       ps <- get
-       let (uh, uns) = unified ps
---        put (ps { unified = (uh, uns ++ ns) })
---        addLog (show (uh, uns ++ ns))
+       unify' ctxt env (valty, Just $ SourceTerm val)
+                       (ty, Just (chkPurpose val ty))
        return $ Bind x (Guess ty val) sc
   where
     -- some expected types show up commonly in errors and indicate a
@@ -550,14 +534,8 @@ fill _ _ _ _ = fail "Can't fill here."
 match_fill :: Raw -> RunTactic
 match_fill guess ctxt env (Bind x (Hole ty) sc) =
     do (val, valty) <- lift $ check ctxt env guess
---        let valtyn = normalise ctxt env valty
---        let tyn = normalise ctxt env ty
-       ns <- match_unify' ctxt env (valty, Just $ SourceTerm val)
-                                   (ty, Just ExpectedType)
-       ps <- get
-       let (uh, uns) = unified ps
---        put (ps { unified = (uh, uns ++ ns) })
---        addLog (show (uh, uns ++ ns))
+       match_unify' ctxt env (valty, Just $ SourceTerm val)
+                             (ty, Just ExpectedType)
        return $ Bind x (Guess ty val) sc
 match_fill _ _ _ _ = fail "Can't fill here."
 
@@ -571,11 +549,8 @@ complete_fill :: RunTactic
 complete_fill ctxt env (Bind x (Guess ty val) sc) =
     do let guess = forget val
        (val', valty) <- lift $ check ctxt env guess
-       ns <- unify' ctxt env (valty, Just $ SourceTerm val')
-                             (ty, Just ExpectedType)
-       ps <- get
-       let (uh, uns) = unified ps
---        put (ps { unified = (uh, uns ++ ns) })
+       unify' ctxt env (valty, Just $ SourceTerm val')
+                       (ty, Just ExpectedType)
        return $ Bind x (Guess ty val) sc
 complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
 
@@ -586,7 +561,6 @@ complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
 solve :: RunTactic
 solve ctxt env (Bind x (Guess ty val) sc)
    = do ps <- get
-        let (uh, uns) = unified ps
         dropdots <-
              case lookup x (notunified ps) of
                 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $
@@ -603,7 +577,7 @@ solve ctxt env (Bind x (Guess ty val) sc)
                             recents = x : recents ps,
                             implementations = implementations ps \\ [x],
                             dotted = dropUnified dropdots (dotted ps) })
-        let (locked, did) = tryLock (holes ps \\ [x]) (updsubst x val sc) in
+        let (locked, _) = tryLock (holes ps \\ [x]) (updsubst x val sc) in
             return locked
   where dropUnified ddots [] = []
         dropUnified ddots ((x, es) : ds)
@@ -628,7 +602,6 @@ solve ctxt env (Bind x (Guess ty val) sc)
                   (Bind n (Let ty' val') sc', tyl && vall && scl)
         tryLock hs t@(Bind n b sc)
             = let (bt', btl) = tryLock hs (binderTy b)
-                  (val', vall) = tryLock hs val
                   (sc', scl) = tryLock hs sc in
                   (Bind n (b { binderTy = bt' }) sc', btl && scl)
         tryLock hs t = (t, True)
@@ -654,13 +627,9 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
                     x@(Bind y (Pi _ _ s _) _) -> x
                     _ -> normalise ctxt env t
        (tyv, tyt) <- lift $ check ctxt env ty
---        ns <- lift $ unify ctxt env tyv t'
        case t' of
            Bind y (Pi rig _ s _) t -> let t' = updsubst y (P Bound n s) t in
-                                        do ns <- unify' ctxt env (s, Nothing) (tyv, Nothing)
-                                           ps <- get
-                                           let (uh, uns) = unified ps
---                                            put (ps { unified = (uh, uns ++ ns) })
+                                        do unify' ctxt env (s, Nothing) (tyv, Nothing)
                                            return $ Bind n (Lam rig tyv) (Bind x (Hole t') (P Bound x t'))
            _ -> lift $ tfail $ CantIntroduce t'
 introTy ty n ctxt env _ = fail "Can't introduce here."
@@ -758,7 +727,7 @@ casetac :: Raw -> Bool -> RunTactic
 casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
   (tmv, tmt) <- lift $ check ctxt env tm
   let tmt' = normalise ctxt env tmt
-  let (tacn, tacstr, tactt) = if induction
+  let (tacn, tacstr, _) = if induction
               then (ElimN, "eliminator", "Induction")
               else (CaseN (FC' emptyFC), "case analysis", "Case analysis")
   case unApply tmt' of
@@ -771,13 +740,9 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
                                _ -> return []
              let (params, indicies) = splitTyArgs param_pos tyargs
              let args     = getArgTys elimTy
-             let pmargs   = take (length params) args
              let args'    = drop (length params) args
-             let propTy   = head args'
              let restargs = init $ tail args'
              let consargs = take (length restargs - length indicies) restargs
-             let indxargs = drop (length restargs - length indicies) restargs
-             let scr      = last $ tail args'
              let indxnames = makeIndexNames indicies
              currentNames <- query $ allTTNames . getProofTerm . pterm
              let tmnm = case tm of
@@ -799,8 +764,7 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
           xs -> lift $ tfail $ Msg $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm
     _ -> lift $ tfail $ NoEliminator (if induction then "induction" else "case analysis")
                                      tmt'
-    where scname = sMN 0 "scarg"
-          makeConsArg (nm, ty) = P Bound nm ty
+    where makeConsArg (nm, ty) = P Bound nm ty
           bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v
           bindConsArgs [] v = v
           addConsHole (nm, ty) =
@@ -879,8 +843,6 @@ start_unify :: Name -> RunTactic
 start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })
                                return tm
 
-tmap f (a, b, c) = (f a, b, c)
-
 solve_unified :: RunTactic
 solve_unified ctxt env tm =
     do ps <- get
@@ -929,14 +891,6 @@ updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)
                (updateSolvedTerm ns r, fmap (updateProv ns) rp) (updateError ns e) xs sc
 updateError ns e = e
 
-updateRes ns [] = []
-updateRes ns ((x, t) : ts) = (x, updateSolvedTerm ns t) : updateRes ns ts
-
-solveInProblems x val [] = []
-solveInProblems x val ((l, r, env, err) : ps)
-   = ((psubst x val l, psubst x val r,
-       updateEnv [(x, val)] env, err) : solveInProblems x val ps)
-
 mergeNotunified :: Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)
 mergeNotunified env holes ns = mnu ns [] [] where
   mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)
diff --git a/src/Idris/Core/ProofTerm.hs b/src/Idris/Core/ProofTerm.hs
index fbfc72f3d..1cfb94f96 100644
--- a/src/Idris/Core/ProofTerm.hs
+++ b/src/Idris/Core/ProofTerm.hs
@@ -195,16 +195,6 @@ updateSolvedTerm' xs x = updateSolved' xs x where
     updateSolvedB' xs b = let (ty', u) = updateSolved' xs (binderTy b) in
                               if u then (b { binderTy = ty' }, u) else (b, False)
 
-    noneOf ns (P _ n _) | n `elem` ns = False
-    noneOf ns (App s f a) = noneOf ns a && noneOf ns f
-    noneOf ns (Bind n (Hole ty) t) = n `notElem` ns && noneOf ns ty && noneOf ns t
-    noneOf ns (Bind n b t) = noneOf ns t && noneOfB ns b
-      where
-        noneOfB ns (Let t v) = noneOf ns t && noneOf ns v
-        noneOfB ns (Guess t v) = noneOf ns t && noneOf ns v
-        noneOfB ns b = noneOf ns (binderTy b)
-    noneOf ns _ = True
-
 -- | As 'subst', in TT, but takes advantage of knowing not to substitute
 -- under Complete applications.
 updsubst :: Eq n => n {-^ The id to replace -} ->
diff --git a/src/Idris/Core/TT.hs b/src/Idris/Core/TT.hs
index b13817938..5e03b88d4 100644
--- a/src/Idris/Core/TT.hs
+++ b/src/Idris/Core/TT.hs
@@ -79,7 +79,6 @@ import qualified Data.Text as T
 import Data.Traversable (Traversable)
 import Data.Typeable (Typeable)
 import Debug.Trace
-import Foreign.Storable (sizeOf)
 import GHC.Generics (Generic)
 import Numeric (showIntAtBase)
 import Numeric.IEEE (IEEE(identicalIEEE))
@@ -431,13 +430,6 @@ instance Show a => Show (TC a) where
 tfail :: Err -> TC a
 tfail e = Error e
 
-failMsg :: String -> TC a
-failMsg str = Error (Msg str)
-
-trun :: FC -> TC a -> TC a
-trun fc (OK a)    = OK a
-trun fc (Error e) = Error (At fc e)
-
 discard :: Monad m => m a -> m ()
 discard f = f >> return ()
 
@@ -510,9 +502,6 @@ deriving instance Binary SpecialName
 sImplementationN :: Name -> [String] -> SpecialName
 sImplementationN n ss = ImplementationN n (map T.pack ss)
 
-sParentN :: Name -> String -> SpecialName
-sParentN n s = ParentN n (T.pack s)
-
 instance Sized Name where
   size (UN n)     = 1
   size (NS n els) = 1 + length els
@@ -699,13 +688,6 @@ nativeTyWidth IT16 = 16
 nativeTyWidth IT32 = 32
 nativeTyWidth IT64 = 64
 
-{-# DEPRECATED intTyWidth "Non-total function, use nativeTyWidth and appropriate casing" #-}
-intTyWidth :: IntTy -> Int
-intTyWidth (ITFixed n) = nativeTyWidth n
-intTyWidth ITNative = 8 * sizeOf (0 :: Int)
-intTyWidth ITChar = error "IRTS.Lang.intTyWidth: Characters have platform and backend dependent width"
-intTyWidth ITBig = error "IRTS.Lang.intTyWidth: Big integers have variable width"
-
 data Const = I Int | BI Integer | Fl Double | Ch Char | Str String
            | B8 Word8 | B16 Word16 | B32 Word32 | B64 Word64
            | AType ArithTy | StrType
diff --git a/src/Idris/Core/Typecheck.hs b/src/Idris/Core/Typecheck.hs
index 40b33e55d..7c3ae87d8 100644
--- a/src/Idris/Core/Typecheck.hs
+++ b/src/Idris/Core/Typecheck.hs
@@ -205,12 +205,6 @@ check' holes tcns ctxt env top
                            Just v' -> v'
            (tv, tt, tns) <- chk Rig0 st (Just maxu) ((n, Rig0, Pi Rig0 i sv kv) : envZero env) t
 
---            convertsC ctxt env st (TType maxu)
---            convertsC ctxt env tt (TType maxu)
---            when holes $ put (v, cs)
---            return (Bind n (Pi i (uniqueBinders (map fst env) sv) (TType maxu))
---                      (pToV n tv), TType maxu)
-
            case (normalise ctxt env st, normalise ctxt env tt) of
                 (TType su, TType tu) -> do
                     when (not holes) $ do (v, cs) <- get
@@ -224,21 +218,6 @@ check' holes tcns ctxt env top
                     return (Bind n (Pi rig i (uniqueBinders (map fstEnv env) sv) k')
                                 (pToV n tv), k', sns ++ tns)
 
-      where mkUniquePi kv (Bind n (Pi rig i s k) sc)
-                    = let k' = smaller kv k in
-                          Bind n (Pi rig i s k') (mkUniquePi k' sc)
-            mkUniquePi kv (Bind n (Lam rig t) sc)
-                    = Bind n (Lam rig (mkUniquePi kv t)) (mkUniquePi kv sc)
-            mkUniquePi kv (Bind n (Let t v) sc)
-                    = Bind n (Let (mkUniquePi kv t) v) (mkUniquePi kv sc)
-            mkUniquePi kv t = t
-
-            -- Kind of the whole thing is the kind of the most unique thing
-            -- in the environment (because uniqueness taints everything...)
-            mostUnique [] k = k
-            mostUnique (Pi _ _ _ pk : es) k = mostUnique es (smaller pk k)
-            mostUnique (_ : es) k = mostUnique es k
-
   chk rigc u lvl env (RBind n b sc)
       = do (b', bt', bns) <- checkBinder b
            (scv, sct, scns) <- chk rigc (smaller bt' u) Nothing ((n, getCount b, b'):env) sc
@@ -261,7 +240,6 @@ check' holes tcns ctxt env top
 
           checkBinder (Lam rig t)
             = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
-                 let tv' = normalise ctxt env tv
                  convType tcns ctxt env tt
                  return (Lam rig tv, tt, [])
           checkBinder (Let t v)
@@ -270,14 +248,12 @@ check' holes tcns ctxt env top
                  -- (or rather, like an application of a lambda, multiply)
                  -- (Consider: adding a single use let?)
                  (vv, vt, vns) <- chk (rigMult rigc RigW) u Nothing env v
-                 let tv' = normalise ctxt env tv
                  convertsC ctxt env vt tv
                  convType tcns ctxt env tt
                  return (Let tv vv, tt, vns)
           checkBinder (NLet t v)
             = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
                  (vv, vt, vns) <- chk rigc u Nothing env v
-                 let tv' = normalise ctxt env tv
                  convertsC ctxt env vt tv
                  convType tcns ctxt env tt
                  return (NLet tv vv, tt, vns)
@@ -285,12 +261,10 @@ check' holes tcns ctxt env top
             | not holes = lift $ tfail (IncompleteTerm undefined)
             | otherwise
                    = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
-                        let tv' = normalise ctxt env tv
                         convType tcns ctxt env tt
                         return (Hole tv, tt, [])
           checkBinder (GHole i ns t)
             = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
-                 let tv' = normalise ctxt env tv
                  convType tcns ctxt env tt
                  return (GHole i ns tv, tt, [])
           checkBinder (Guess t v)
@@ -298,20 +272,15 @@ check' holes tcns ctxt env top
             | otherwise
                    = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
                         (vv, vt, vns) <- chk rigc u Nothing env v
-                        let tv' = normalise ctxt env tv
                         convertsC ctxt env vt tv
                         convType tcns ctxt env tt
                         return (Guess tv vv, tt, vns)
           checkBinder (PVar rig t)
             = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
-                 let tv' = normalise ctxt env tv
                  convType tcns ctxt env tt
-                 -- Normalised version, for erasure purposes (it's easier
-                 -- to tell if it's a collapsible variable)
                  return (PVar rig tv, tt, [])
           checkBinder (PVTy t)
             = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
-                 let tv' = normalise ctxt env tv
                  convType tcns ctxt env tt
                  return (PVTy tv, tt, [])
 
diff --git a/src/Idris/Core/Unify.hs b/src/Idris/Core/Unify.hs
index 89f1ca225..39ce9b7ed 100644
--- a/src/Idris/Core/Unify.hs
+++ b/src/Idris/Core/Unify.hs
@@ -37,7 +37,6 @@ data FailContext = FailContext { fail_sourceloc :: FC,
                                }
   deriving (Eq, Show)
 
-type Injs = [(TT Name, TT Name, TT Name)]
 type Fails = [(TT Name, TT Name, -- unification error
                Bool, -- ready to retry yet
                Env, Err, [FailContext], FailAt)]
@@ -55,10 +54,6 @@ unrecoverable = any bad
 data UInfo = UI Int Fails
      deriving Show
 
-data UResult a = UOK a
-               | UPartOK a
-               | UFail Err
-
 -- | Smart constructor for unification errors that takes into account the FailContext
 cantUnify :: [FailContext] -> Bool -> (t, Maybe Provenance) -> (t, Maybe Provenance) -> (Err' t) -> [(Name, t)] -> Int -> Err' t
 cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i
@@ -189,16 +184,10 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =
         | otherwise = checkScope ns (x, tm)
 
     checkScope ns (x, tm) =
---           case boundVs (envPos x 0 env) tm of
---                [] -> return [(x, tm)]
---                (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
---                                      (impl ns tm) (errEnv env))
         let v = highV (-1) tm in
             if v >= length ns
                then lift $ tfail (Msg "SCOPE ERROR")
                else return [(x, bind v ns tm)]
-      where impl [] tm = tm
-            impl ((n, _) : ns) tm = impl ns (substV (P Bound n Erased) tm)
 
     bind i ns tm
       | i < 0 = tm
@@ -255,20 +244,6 @@ trimSolutions (topx, xfrom) (topy, yfrom) from env topns = followSols [] (dropPa
         followSols vs (n : ns) = do ns' <- followSols vs ns
                                     return $ n : ns'
 
-expandLets env (x, tm) = (x, doSubst (reverse env) tm)
-  where
-    doSubst [] tm = tm
-    doSubst ((n, Let v t) : env) tm
-        = doSubst env (subst n v tm)
-    doSubst (_ : env) tm
-        = doSubst env tm
-
-hasv :: TT Name -> Bool
-hasv (V x) = True
-hasv (App _ f a) = hasv f || hasv a
-hasv (Bind x b sc) = hasv (binderTy b) || hasv sc
-hasv _ = False
-
 unify :: Context -> Env ->
          (TT Name, Maybe Provenance) ->
          (TT Name, Maybe Provenance) ->
@@ -295,10 +270,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
 --         Error e@(CantUnify False _ _ _ _ _)  -> tfail e
                        Error e -> tfail e
   where
-    headDiff (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x /= y
-    headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y
-    headDiff _ _ = False
-
     injective (P (DCon _ _ _) _ _) = True
     injective (P (TCon _ _) _ _) = True
 --     injective (P Ref n _)
@@ -325,10 +296,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
     sc i = do UI s f <- get
               put (UI (s+i) f)
 
-    errors :: StateT UInfo TC Bool
-    errors = do UI s f <- get
-                return (not (null f))
-
     uplus u1 u2 = do UI s f <- get
                      r <- u1
                      UI s f' <- get
@@ -340,12 +307,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
           StateT UInfo
           TC [(Name, TT Name)]
     un = un' env
---     un fn names x y
---         = let (xf, _) = unApply x
---               (yf, _) = unApply y in
---               if headDiff xf yf then unifyFail x y else
---                   uplus (un' fn names x y)
---                         (un' fn names (hnf ctxt env x) (hnf ctxt env y))
 
     un' :: Env -> Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
            StateT UInfo
@@ -575,26 +536,11 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
                 = unifyFail appx appy
             checkHeads _ _ = return []
 
-            numArgs tm = let (f, args) = unApply tm in length args
-
             metavarApp tm = let (f, args) = unApply tm in
                                 (metavar f &&
                                  all (\x -> metavarApp x) args
                                     && nub args == args) ||
                                        globmetavar tm
-            metavarArgs tm = let (f, args) = unApply tm in
-                                 all (\x -> metavar x || inenv x) args
-                                   && nub args == args
-            metavarApp' tm = let (f, args) = unApply tm in
-                                 all (\x -> pat x || metavar x) (f : args)
-                                   && nub args == args
-
-            rigid (P (DCon _ _ _) _ _) = True
-            rigid (P (TCon _ _) _ _) = True
-            rigid t@(P Ref _ _)  = inenv t || globmetavar t
-            rigid (Constant _)       = True
-            rigid (App _ f a)        = rigid f && rigid a
-            rigid t                  = not (metavar t) || globmetavar t
 
             globmetavar t = case unApply t  of
                                 (P _ x _, _) ->
@@ -608,14 +554,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
                                              (x `elem` holes || holeIn env x))
                                           || globmetavar t
                              _ -> False
-            pat t = case t of
-                         P _ x _ -> x `elem` holes || patIn env x
-                         _ -> False
-            inenv t = case t of
-                           P _ x _ -> x `elem` (map fstEnv env)
-                           _ -> False
-
-            notFn t = injective t || metavar t || inenv t
 
             injectiveTC t@(P Ref n _) t'@(P Ref n' _)
                 | Just ni <- lookupInjectiveExact n ctxt,
@@ -680,16 +618,10 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
         | otherwise = checkScope ns (x, tm)
 
     checkScope ns (x, tm) | pureTerm tm =
---           case boundVs (envPos x 0 env) tm of
---                [] -> return [(x, tm)]
---                (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))
---                                      (impl ns tm) (errEnv env))
         let v = highV (-1) tm in
             if v >= length ns
                then lift $ tfail (Msg "SCOPE ERROR")
                else return [(x, bind v ns tm)]
-      where impl [] tm = tm
-            impl (((n, _), _) : ns) tm = impl ns (substV (P Bound n Erased) tm)
     checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")
 
     bind i ns tm
@@ -708,15 +640,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
                           sc 1
                           combine env bnames as (ns' ++ bs)
 
-boundVs :: Int -> Term -> [Int]
-boundVs i (V j) | j < i = []
-                | otherwise = [j]
-boundVs i (Bind n b sc) = boundVs (i + 1) sc
-boundVs i (App _ f x) = let fs = boundVs i f
-                            xs = boundVs i x in
-                            nub (fs ++ xs)
-boundVs i _ = []
-
 highV :: Int -> Term -> Int
 highV i (V j) | j > i = j
                 | otherwise = i
@@ -724,11 +647,6 @@ highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]
 highV i (App _ f x) = max (highV i f) (highV i x)
 highV i _ = i
 
-envPos x i [] = 0
-envPos x i ((y, _) : ys) | x == y = i
-                         | otherwise = envPos x (i + 1) ys
-
-
 -- If there are any clashes of constructors, deem it unrecoverable, otherwise some
 -- more work may help.
 -- FIXME: Depending on how overloading gets used, this may cause problems. Better
@@ -794,9 +712,3 @@ holeIn env n = case lookupBinder n env of
                     Just (Hole _) -> True
                     Just (Guess _ _) -> True
                     _ -> False
-
-patIn :: Env -> Name -> Bool
-patIn env n = case lookupBinder n env of
-                    Just (PVar _ _) -> True
-                    Just (PVTy _) -> True
-                    _ -> False
diff --git a/src/Idris/Coverage.hs b/src/Idris/Coverage.hs
index b17eb4a35..4634ad88b 100644
--- a/src/Idris/Coverage.hs
+++ b/src/Idris/Coverage.hs
@@ -281,10 +281,6 @@ addMissingConsSt ist (Case t n alts) = liftM (Case t n) (addMissingAlts n alts)
     collectConsts (ConstCase c sc) = Just c
     collectConsts _ = Nothing
 
-    hasDefault (DefaultCase (UnmatchedCase _)) = False
-    hasDefault (DefaultCase _) = True
-    hasDefault _ = False
-
     getConType n = do ty <- lookupTyExact n (tt_ctxt ist)
                       case unApply (getRetTy (normalise (tt_ctxt ist) [] ty)) of
                            (P _ tyn _, _) -> Just tyn
@@ -333,9 +329,6 @@ trimOverlapping sc = trim [] [] sc
     trimAlts cs nots vn (DefaultCase sc : rest)
         = DefaultCase (trim cs nots sc) : trimAlts cs nots vn rest
 
-    isConMatch c (ConCase cn t args sc) = c == cn
-    isConMatch _ _ = False
-
     substMatch :: (Name, [Name]) -> [CaseAlt] -> [CaseAlt]
     substMatch ca [] = []
     substMatch (c,args) (ConCase cn t args' sc : _)
diff --git a/src/Idris/DSL.hs b/src/Idris/DSL.hs
index 5b25b7217..9b455238e 100644
--- a/src/Idris/DSL.hs
+++ b/src/Idris/DSL.hs
@@ -167,8 +167,7 @@ var dsl n t i = v' i t where
     setFC fc t = t
 
 unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm
-unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in
-                                        mkap (getFn e)
+unIdiom ap pure fc e@(PApp _ _ _) = mkap (getFn e)
   where
     getFn (PApp fc f args) = (PApp fc pure [pexp f], args)
     getFn f = (f, [])
diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs
index 4f8f3a36a..52e8c5e3b 100644
--- a/src/Idris/Delaborate.hs
+++ b/src/Idris/Delaborate.hs
@@ -191,13 +191,6 @@ delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm
     de tys env _ (TType i) = PType un
     de tys env _ (UType u) = PUniverse un u
 
-    dens x | fullname = x
-    dens ns@(NS n _) = case lookupCtxt n (idris_implicits ist) of
-                              [_] -> n -- just one thing
-                              [] -> n -- metavariables have no implicits
-                              _ -> ns
-    dens n = n
-
     deFn tys env (App _ f a) args = deFn tys env f (a:args)
     deFn tys env (P _ n _) [l,r]
          | n == pairTy    = PPair un [] IsType (de tys env [] l) (de tys env [] r)
@@ -353,7 +346,7 @@ pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
              then text "Unification failure" <$> showSc i sc
              else empty
 pprintErr' i (CantConvert x_in y_in env) =
- let (x_ns, y_ns, nms) = renameMNs x_in y_in
+ let (x_ns, y_ns, _) = renameMNs x_in y_in
      (x, y) = addImplicitDiffs (delabSugared i (flagUnique x_ns))
                                (delabSugared i (flagUnique y_ns)) in
   text "Type mismatch between" <>
diff --git a/src/Idris/Docs.hs b/src/Idris/Docs.hs
index 6463e9d12..411c98f18 100644
--- a/src/Idris/Docs.hs
+++ b/src/Idris/Docs.hs
@@ -240,10 +240,6 @@ pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_
     updateRef nm (PRef fc _ _) = PRef fc [] nm
     updateRef _  pt          = pt
 
-    isSubInterface (PPi (Constraint _ _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args'
-    isSubInterface (PPi _   _            _ _ pt)                                           = isSubInterface pt
-    isSubInterface _                                                                       = False
-
     prettyConstraints =
       cat (punctuate (comma <> space) (map (pprintPTerm ppo params' [] infixes) constraints))
 
diff --git a/src/Idris/Elab/Clause.hs b/src/Idris/Elab/Clause.hs
index 8a74e3824..a3cb203d2 100644
--- a/src/Idris/Elab/Clause.hs
+++ b/src/Idris/Elab/Clause.hs
@@ -27,7 +27,6 @@ import Idris.Elab.Transform
 import Idris.Elab.Type
 import Idris.Elab.Utils
 import Idris.Error
-import Idris.Inliner
 import Idris.Options
 import Idris.Output (iputStrLn, pshow, sendHighlighting)
 import Idris.PartialEval
@@ -140,12 +139,6 @@ elabClauses info' fc opts n_in cs =
            -- optimisation applied to LHS
            let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $
                           map debind pats_forced
-           -- pdef_cov is the pattern definition without forcing, which
-           -- we feed to the coverage checker (we need to know what the
-           -- programmer wrote before forcing erasure)
-           let pdef_cov
-                    = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $
-                          map debind pats_raw
            -- pdef_pe is the one which will get further optimised
            -- for run-time, with no forcing optimisation of the LHS because
            -- the affects erasure. Also, it's partially evaluated
@@ -160,8 +153,6 @@ elabClauses info' fc opts n_in cs =
            -- help with later inlinings.
 
            ist <- getIState
-           let pdef_inl = inlineDef ist pdef
-
            numArgs <- tclift $ sameLength pdef
 
            case specNames opts of
@@ -184,7 +175,6 @@ elabClauses info' fc opts n_in cs =
                               missing' <- checkPossibles info fc True n missing
                               -- Filter out the ones which match one of the
                               -- given cases (including impossible ones)
-                              let clhs = map getLHS pdef
                               logElab 2 $ "Must be unreachable (" ++ show (length missing') ++ "):\n" ++
                                           showSep "\n" (map showTmImpls missing') ++
                                          "\nAgainst: " ++
@@ -232,7 +222,6 @@ elabClauses info' fc opts n_in cs =
            logElab 3 $ "Optimised: " ++ show tree'
            ctxt <- getContext
            ist <- getIState
-           let opt = idris_optimisation ist
            putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)
                                                 (idris_patdefs ist) })
            let caseInfo = CaseInfo (inlinable opts) (inlinable opts) (dictionary opts)
@@ -302,15 +291,6 @@ elabClauses info' fc opts n_in cs =
                                   return ()
 
   where
-    noMatch i cs tm = all (\x -> case trim_matchClause i (delab' i x True True) tm of
-                                      Right _ -> False
-                                      Left miss -> True) cs
-      where
-        trim_matchClause i (PApp fcl fl ls) (PApp fcr fr rs)
-            = let args = min (length ls) (length rs) in
-                  matchClause i (PApp fcl fl (take args ls))
-                                (PApp fcr fr (take args rs))
-
     checkUndefined n ctxt = case lookupDef n ctxt of
                                  [] -> return ()
                                  [TyDecl _ _] -> return ()
@@ -358,7 +338,7 @@ elabClauses info' fc opts n_in cs =
 
     sameLength ((_, x, _) : xs)
         = do l <- sameLength xs
-             let (f, as) = unApply x
+             let (_, as) = unApply x
              if (null xs || l == length as) then return (length as)
                 else tfail (At fc (Msg "Clauses have differing numbers of arguments "))
     sameLength [] = return 0
@@ -671,8 +651,7 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
                                       "\n" ++ show ptm
                           return (Left ptm, lhs)
 elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock_as)
-   = do let tcgen = Dictionary `elem` opts
-        push_estack fname False
+   = do push_estack fname False
         ctxt <- getContext
         let (lhs_in, rhs_in, whereblock) = desugarAs lhs_in_as rhs_in_as whereblock_as
 
@@ -903,8 +882,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
     pinfo info ns ds i
           = let newps = params info ++ ns
                 dsParams = map (\n -> (n, map fst newps)) ds
-                newb = addAlist dsParams (inblock info)
-                l = liftname info in
+                newb = addAlist dsParams (inblock info) in
                 info { params = newps,
                        inblock = newb,
                        liftname = id -- (\n -> case lookupCtxt n newb of
@@ -953,8 +931,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
     isOutsideWith _ = True
 
 elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
-   = do let tcgen = Dictionary `elem` opts
-        ctxt <- getContext
+   = do ctxt <- getContext
         -- Build the LHS as an "Infer", and pull out its type and
         -- pattern bindings
         i <- getIState
@@ -1176,9 +1153,6 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
     mkAux pn wname toplhs ns ns' c
         = ifail $ show fc ++ ":badly formed with clause"
 
-    addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])
-    addArg (PRef fc hls f) w = PApp fc (PRef fc hls f) [pexp w]
-
     -- ns, arguments which don't depend on the with argument
     -- ns', arguments which do
     updateLHS n pn wname mvars ns_in ns_in' (PApp fc (PRef fc' hls' n') args) w
@@ -1202,11 +1176,6 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
     updateWithTerm ist pn wname toplhs ns_in ns_in' tm
           = mapPT updateApp tm
        where
-         arity (PApp _ _ as) = length as
-         arity _ = 0
-
-         lhs_arity = arity toplhs
-
          currentFn fname (PAlternative _ _ as)
               | Just tm <- getApp as = tm
             where getApp (tm@(PApp _ (PRef _ _ f) _) : as)
diff --git a/src/Idris/Elab/Data.hs b/src/Idris/Elab/Data.hs
index f0faef72c..b5fab1e85 100644
--- a/src/Idris/Elab/Data.hs
+++ b/src/Idris/Elab/Data.hs
@@ -42,8 +42,7 @@ warnLC fc n
 
 elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris ()
 elabData info syn doc argDocs fc opts (PLaterdecl n nfc t_in)
-    = do let codata = Codata `elem` opts
-         logElab 1 (show (fc, doc))
+    = do logElab 1 (show (fc, doc))
          checkUndefined fc n
          when (implicitable (nsroot n)) $ warnLC fc n
          (cty, _, t, inacc) <- buildType info syn fc [] n t_in
@@ -73,7 +72,6 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)
                         rt -> tclift $ tfail (At fc (Elaborating "type constructor " n Nothing (Msg "Not a valid type constructor")))
          cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons
          ttag <- getName
-         let as = map (const (Left (Msg ""))) (getArgTys cty)
 
          ctxt <- getContext
          let params = findParams n (normalise ctxt [] cty) (map snd cons)
@@ -151,8 +149,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)
         cinfo info ds
           = let newps = params info
                 dsParams = map (\n -> (n, [])) ds
-                newb = addAlist dsParams (inblock info)
-                l = liftname info in
+                newb = addAlist dsParams (inblock info) in
                 info { params = newps,
                        inblock = newb,
                        liftname = id -- Is this appropriate?
@@ -226,12 +223,6 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen
     getTyName (PRef _ _ n) = n == nsroot tn
     getTyName _ = False
 
-
-    getNamePos :: Int -> PTerm -> Name -> Maybe Int
-    getNamePos i (PPi _ n _ _ sc) x | n == x = Just i
-                                    | otherwise = getNamePos (i + 1) sc x
-    getNamePos _ _ _ = Nothing
-
     -- if the constructor is a UniqueType, the datatype must be too
     -- (AnyType is fine, since that is checked for uniqueness too)
     -- if hte contructor is AnyType, the datatype must be at least AnyType
@@ -339,7 +330,7 @@ elabCaseFun ind paramPos n ty cons info = do
   elimLog "Elaborating case function"
   put (Map.fromList $ zip (concatMap (\(_, p, _, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))
   let (cnstrs, _) = splitPi ty
-  let (splittedTy@(pms, idxs)) = splitPms cnstrs
+  let (pms, idxs) = splitPms cnstrs
   generalParams <- namePis False pms
   motiveIdxs    <- namePis False idxs
   let motive = mkMotive n paramPos generalParams motiveIdxs
@@ -377,10 +368,6 @@ elabCaseFun ind paramPos n ty cons info = do
         elimDeclName :: Name
         elimDeclName = if ind then SN . ElimN $ n else SN . CaseN (FC' elimFC) $ n
 
-        applyNS :: Name -> [String] -> Name
-        applyNS n []  = n
-        applyNS n ns  = sNS n ns
-
         splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)
         splitPi = splitPi' []
           where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)
@@ -421,10 +408,6 @@ elabCaseFun ind paramPos n ty cons info = do
         simpleName (MN i n) = str n ++ show i
         simpleName n        = show n
 
-        nameSpaces :: Name -> [String]
-        nameSpaces (NS _ ns) = map str ns
-        nameSpaces _         = []
-
         freshName :: String -> EliminatorState Name
         freshName key = do
           nameMap <- get
diff --git a/src/Idris/Elab/Implementation.hs b/src/Idris/Elab/Implementation.hs
index 5b4683635..76451d4b8 100644
--- a/src/Idris/Elab/Implementation.hs
+++ b/src/Idris/Elab/Implementation.hs
@@ -56,7 +56,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
                   [] -> ifail $ show fc ++ ":" ++ show n ++ " is not an interface"
                   cs -> tclift $ tfail $ At fc
                            (CantResolveAlts (map fst cs))
-    let constraint = PApp fc (PRef fc [] n) (map pexp ps)
     let iname = mkiname n (namespace info) ps expn
     putIState (ist { hide_list = addDef iname acc (hide_list ist) })
     ist <- getIState
@@ -144,7 +143,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
          let wbVals_orig = map (decorateid (decorate ns iname)) ds'
          ist <- getIState
          let wbVals = map (expandParamsD False ist id pextra (map methName mtys)) wbVals_orig
-         let wb = wbTys ++ wbVals
 
          logElab 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)
          logElab 3 $ "Implementation is " ++ show ps ++ " implicits " ++ show (concat (nub wparams))
@@ -277,8 +275,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex
     mkMethApp ps (n, _, _, ty)
               = lamBind 0 ty (papp fc (PRef fc [] n)
                      (ps ++ map (toExp . fst) pextra ++ methArgs 0 ty))
-       where
-          needed is p = pname p `elem` map pname is
 
     lamBind i (PPi (Constraint _ _ _) _ _ _ sc) sc'
           = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
diff --git a/src/Idris/Elab/Interface.hs b/src/Idris/Elab/Interface.hs
index 96b274307..f1d4dbe37 100644
--- a/src/Idris/Elab/Interface.hs
+++ b/src/Idris/Elab/Interface.hs
@@ -94,8 +94,7 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn
              ims <- mapM (tdecl impps mnames) mdecls
              defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)
                           (filter clause ds)
-             let (methods, imethods)
-                  = unzip (map (\ (x, y, z) -> (x, y)) ims)
+             let imethods = map (\ (x, y, z) -> y) ims
              let defaults = map (\ (x, (y, z)) -> (x,y)) defs
 
              addInterface tn (CI cn (map nodoc imethods) defaults idecls
@@ -367,13 +366,6 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn
              return (PTy doc [] syn fc o m mfc ty',
                      PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []])
 
-    updateIMethod :: [(Name, PTerm)] ->
-                     (Name, (a, b, c, d, PTerm)) ->
-                     (Name, (a, b, c, d, PTerm))
-    updateIMethod ns tm@(n, (isf, mfc, doc, o, ty))
-       | Just ty' <- lookup (nsroot n) ns = (n, (isf, mfc, doc, o, ty'))
-       | otherwise = tm
-
     getMArgs (PPi (Imp _ _ _ _ _ _) n _ ty sc) = IA n : getMArgs sc
     getMArgs (PPi (Exp _ _ _ _) n _ ty sc) = EA n : getMArgs sc
     getMArgs (PPi (Constraint _ _ _) n _ ty sc) = CA : getMArgs sc
@@ -423,12 +415,6 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn
     toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)
     toExp ns e sc = sc
 
--- | Get the method declaration name corresponding to a user-provided name
-mdec :: Name -> Name
-mdec (UN n) = SN (MethodN (UN n))
-mdec (NS x n) = NS (mdec x) n
-mdec x = x
-
 -- | Get the docstring corresponding to a member, if one exists
 memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))
 memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)
diff --git a/src/Idris/Elab/Record.hs b/src/Idris/Elab/Record.hs
index cf0d5bc61..ff0012e4c 100644
--- a/src/Idris/Elab/Record.hs
+++ b/src/Idris/Elab/Record.hs
@@ -16,7 +16,6 @@ import Idris.Docstrings
 import Idris.Elab.Data
 import Idris.Error
 import Idris.Output (sendHighlighting)
-import Idris.Parser.Expr (tryFullExpr)
 
 import Control.Monad
 import Data.List
@@ -212,15 +211,6 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target
     isFieldOrParam' :: (Name, a) -> Bool
     isFieldOrParam' = isFieldOrParam . fst
 
-    isField :: Name -> Bool
-    isField = flip elem fieldNames
-
-    isField' :: (Name, a, b, c, d, f) -> Bool
-    isField' (n, _, _, _, _, _) = isField n
-
-    fieldTerms :: [PTerm]
-    fieldTerms = [t | (_, _, _, t, _) <- fields]
-
     -- Delabs the TT to PTerm
     -- This is not good.
     -- However, for machine generated implicits, there seems to be no PTerm available.
@@ -239,13 +229,6 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target
     freeName (NS n s) = NS (freeName n) s
     freeName n = n
 
-    -- | Zips together parameters with their documentation. If no documentation for a given field exists, an empty docstring is used.
-    zipParams :: IState -> [(Name, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, PTerm, Docstring (Either Err PTerm))]
-    zipParams i ((n, _, t) : rest) ((_, d) : rest') = (n, t, d) : (zipParams i rest rest')
-    zipParams i ((n, _, t) : rest) [] = (n, t, emptyDoc) : (zipParams i rest [])
-      where emptyDoc = annotCode (tryFullExpr rsyn i) emptyDocstring
-    zipParams _ [] [] = []
-
     paramName :: Name -> Name
     paramName (UN n) = sUN ("param_" ++ str n)
     paramName (MN i n) = sMN i ("param_" ++ str n)
@@ -282,15 +265,6 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target
         fieldDep :: Name -> PTerm -> (Name, [Name])
         fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)
 
-    -- | A list of fields depending on another field.
-    dependentFields :: [Name]
-    dependentFields = filter depends fieldNames
-      where
-        depends :: Name -> Bool
-        depends n = case lookup n fieldDependencies of
-                      Just xs -> not $ null xs
-                      Nothing -> False
-
     -- | A list of fields depended on by other fields.
     dependedOn :: [Name]
     dependedOn = concat ((catMaybes (map (\x -> lookup x fieldDependencies) fieldNames)))
diff --git a/src/Idris/Elab/Term.hs b/src/Idris/Elab/Term.hs
index bb43d63bf..3208f6c8c 100644
--- a/src/Idris/Elab/Term.hs
+++ b/src/Idris/Elab/Term.hs
@@ -79,7 +79,6 @@ build :: IState
       -> ElabD ElabResult
 build ist info emode opts fn tm
     = do elab ist info emode opts fn tm
-         let tmIn = tm
          let inf = case lookupCtxt fn (idris_tyinfodata ist) of
                         [TIPartial] -> True
                         _ -> False
@@ -157,8 +156,7 @@ buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name ->
          PTerm ->
          ElabD ElabResult
 buildTC ist info emode opts fn ns tm
-    = do let tmIn = tm
-         let inf = case lookupCtxt fn (idris_tyinfodata ist) of
+    = do let inf = case lookupCtxt fn (idris_tyinfodata ist) of
                         [TIPartial] -> True
                         _ -> False
          -- set name supply to begin after highest index in tm
@@ -184,7 +182,6 @@ buildTC ist info emode opts fn ns tm
          if (log /= "")
             then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
             else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
-  where pattern = emode == ELHS || emode == EImpossible
 
 -- | return whether arguments of the given constructor name can be
 -- matched on. If they're polymorphic, no, unless the type has beed
@@ -241,7 +238,6 @@ elab ist info emode opts fn tm
     = do let loglvl = opt_logLevel (idris_options ist)
          when (loglvl > 5) $ unifyLog True
          compute -- expand type synonyms, etc
-         let fc = maybe "(unknown)"
          elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)
          est <- getAux
          sequence_ (get_delayed_elab est)
@@ -277,14 +273,6 @@ elab ist info emode opts fn tm
         Placeholder -> (True, priority arg)
         tm -> (False, priority arg)
 
-    toElab ina arg = case getTm arg of
-        Placeholder -> Nothing
-        v -> Just (priority arg, elabE ina (elabFC info) v)
-
-    toElab' ina arg = case getTm arg of
-        Placeholder -> Nothing
-        v -> Just (elabE ina (elabFC info) v)
-
     mkPat = do hs <- get_holes
                tm <- get_term
                case hs of
@@ -350,18 +338,6 @@ elab ist info emode opts fn tm
     notDelay t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = False
     notDelay _ = True
 
-    local f = do e <- get_env
-                 return (f `elem` map fstEnv e)
-
-    -- | Is a constant a type?
-    constType :: Const -> Bool
-    constType (AType _) = True
-    constType StrType = True
-    constType VoidType = True
-    constType _ = False
-
-    -- "guarded" means immediately under a constructor, to help find patvars
-
     elab' :: ElabCtxt  -- ^ (in an argument, guarded, in a type, in a quasiquote)
           -> Maybe FC -- ^ The closest FC in the syntax tree, if applicable
           -> PTerm -- ^ The term to elaborate
@@ -597,13 +573,6 @@ elab ist info emode opts fn tm
                          (P _ n' _, _) -> n == n'
                          _ -> False
 
-        showQuick (CantUnify _ (l, _) (r, _) _ _ _)
-            = show (l, r)
-        showQuick (ElaboratingArg _ _ _ e) = showQuick e
-        showQuick (At _ e) = showQuick e
-        showQuick (ProofSearchFail (Msg _)) = "search fail"
-        showQuick _ = "No chance"
-
     elab' ina _ (PPatvar fc n) | bindfree
         = do patvar n
              update_term liftPats
@@ -621,8 +590,6 @@ elab ist info emode opts fn tm
         = do ty <- goal
              testImplicitWarning fc n ty
              let ina = e_inarg ec
-                 guarded = e_guarded ec
-                 inty = e_intype ec
              ctxt <- get_context
              env <- get_env
 
@@ -884,7 +851,6 @@ elab ist info emode opts fn tm
                         _ -> do mapM_ setInjective (map getTm args)
                                 -- maybe more things are solvable now
                                 unifyProblems
-                    let guarded = isConName f ctxt
 --                    trace ("args is " ++ show args) $ return ()
                     ns <- apply (Var f) (map isph args)
 --                    trace ("ns is " ++ show ns) $ return ()
@@ -994,10 +960,6 @@ elab ist info emode opts fn tm
             getDets i ds (a : as) | i `elem` ds = a : getDets (i + 1) ds as
                                   | otherwise = getDets (i + 1) ds as
 
-            tacTm (PTactics _) = True
-            tacTm (PProof _) = True
-            tacTm _ = False
-
             setInjective (PRef _ _ n) = setinj n
             setInjective (PApp _ (PRef _ _ n) _) = setinj n
             setInjective _ = return ()
@@ -1072,7 +1034,6 @@ elab ist info emode opts fn tm
              matchProblems True
              args <- get_env
              envU <- mapM (getKind args) args
-             let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts
 
              -- Drop the unique arguments used in the term already
              -- and in the scrutinee (since it's
@@ -1150,12 +1111,6 @@ elab ist info emode opts fn tm
                                     UType AllTypes -> return (n, True)
                                     _ -> return (n, False)
 
-              tcName tm | (P _ n _, _) <- unApply tm
-                  = case lookupCtxt n (idris_interfaces ist) of
-                         [_] -> True
-                         _ -> False
-              tcName _ = False
-
               isNotLift env n
                  = case lookupBinder n env of
                         Just ty ->
@@ -1164,10 +1119,6 @@ elab ist info emode opts fn tm
                                   _ -> False
                         _ -> False
 
-              usedIn ns (n, b)
-                 = n `elem` ns
-                     || any (\x -> x `elem` ns) (allTTNames (binderTy b))
-
     elab' ina fc (PUnifyLog t) = do unifyLog True
                                     elab' ina fc t
                                     unifyLog False
@@ -2710,7 +2661,6 @@ processTacticDecls info steps =
 
     RDatatypeDefnInstrs tyn tyconTy ctors ->
       do let cn (n, _, _) = n
-             cimpls (_, impls, _) = impls
              cty (_, _, t) = t
          addIBC (IBCDef tyn)
          mapM_ (addIBC . IBCDef . cn) ctors
diff --git a/src/Idris/Elab/Transform.hs b/src/Idris/Elab/Transform.hs
index c35e08593..b1a72097f 100644
--- a/src/Idris/Elab/Transform.hs
+++ b/src/Idris/Elab/Transform.hs
@@ -38,7 +38,6 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in
          sendHighlighting highlights
          updateIState $ \i -> i { idris_name = newGName }
          let lhs_tm = orderPats (getInferTerm lhs')
-         let lhs_ty = getInferType lhs'
          let newargs = pvars i lhs_tm
 
          (clhs_tm_in, clhs_ty) <- recheckC_borrowing False False [] (constraintNS info) fc id [] lhs_tm
diff --git a/src/Idris/Elab/Type.hs b/src/Idris/Elab/Type.hs
index 64bea8e28..7e01b1e8a 100644
--- a/src/Idris/Elab/Type.hs
+++ b/src/Idris/Elab/Type.hs
@@ -169,11 +169,6 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par
          addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (PTyped (PRef fc [] n) ty')) -- (mergeTy ty' (delab i nty')))
 
          let (fam, _) = unApply (getRetTy nty')
-         let corec = case fam of
-                        P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of
-                                        [TI _ True _ _ _ _] -> True
-                                        _ -> False
-                        _ -> False
          -- Productivity checking now via checking for guarded 'Delay'
          let opts' = opts -- if corec then (Coinductive : opts) else opts
          let usety = if norm then nty' else nty
@@ -224,14 +219,6 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par
               _ -> return ()
          return usety
   where
-    -- for making an internalapp, we only want the explicit ones, and don't
-    -- want the parameters, so just take the arguments which correspond to the
-    -- user declared explicit ones
-    mergeTy (PPi e n fc ty sc) (PPi e' n' _ _ sc')
-         | e == e' = PPi e n fc ty (mergeTy sc sc')
-         | otherwise = mergeTy sc sc'
-    mergeTy _ sc = sc
-
     ffiexport = sNS (sUN "FFI_Export") ["FFI_Export"]
 
     err = txt "Err"
diff --git a/src/Idris/Elab/Utils.hs b/src/Idris/Elab/Utils.hs
index dcaf9a495..cf0d222f4 100644
--- a/src/Idris/Elab/Utils.hs
+++ b/src/Idris/Elab/Utils.hs
@@ -118,7 +118,6 @@ elabCaseBlock :: ElabInfo -> FnOpts -> PDecl -> Idris ()
 elabCaseBlock info opts d@(PClauses f o n ps)
         = do addIBC (IBCDef n)
              logElab 5 $ "CASE BLOCK: " ++ show (n, d)
-             let opts' = nub (o ++ opts)
              -- propagate totality assertion to the new definitions
              let opts' = filter propagatable opts
              setFlags n opts'
@@ -746,7 +745,7 @@ pruneByType _ _ t _ _ as = as
 -- to it later - just returns 'var' for now. EB)
 isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool
 isPlausible ist var env n ty
-    = let (hvar, interfaces) = collectConstraints [] [] ty in
+    = let (hvar, _) = collectConstraints [] [] ty in
           case hvar of
                Nothing -> True
                Just rth -> var -- trace (show (rth, interfaces)) var
diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs
index 03656546d..8fd757e30 100644
--- a/src/Idris/ElabDecls.hs
+++ b/src/Idris/ElabDecls.hs
@@ -244,12 +244,6 @@ elabDecl' what info (PParams f ns ps)
          let nblock = pblock i
          mapM_ (elabDecl' what info) nblock
   where
-    pinfo = let ds = concatMap tldeclared ps
-                newps = params info ++ ns
-                dsParams = map (\n -> (n, map fst newps)) ds
-                newb = addAlist dsParams (inblock info) in
-                info { params = newps,
-                       inblock = newb }
     pblock i = map (expandParamsD False i id ns
                       (concatMap tldeclared ps)) ps
 
diff --git a/src/Idris/Erasure.hs b/src/Idris/Erasure.hs
index 7429889df..623667cca 100644
--- a/src/Idris/Erasure.hs
+++ b/src/Idris/Erasure.hs
@@ -287,7 +287,6 @@ buildDepMap ci used externs ctx startNames
         -- mini-DSL for postulates
         (==>) ds rs = (S.fromList ds, M.fromList [(r, S.empty) | r <- rs])
         it n is = [(sUN n, Arg i) | i <- is]
-        mn n is = [(MN 0 $ pack n, Arg i) | i <- is]
 
         -- believe_me is special because it does not use all its arguments
         specialPrims = S.fromList [sUN "prim__believe_me"]
@@ -624,9 +623,6 @@ buildDepMap ci used externs ctx startNames
     union :: Deps -> Deps -> Deps
     union = M.unionWith (M.unionWith S.union)
 
-    unions :: [Deps] -> Deps
-    unions = M.unionsWith (M.unionWith S.union)
-
     unionMap :: (a -> Deps) -> [a] -> Deps
     unionMap f = M.unionsWith (M.unionWith S.union) . map f
 
diff --git a/src/Idris/ErrReverse.hs b/src/Idris/ErrReverse.hs
index 698ca596d..fbfbcb550 100644
--- a/src/Idris/ErrReverse.hs
+++ b/src/Idris/ErrReverse.hs
@@ -12,7 +12,6 @@ module Idris.ErrReverse(errReverse) where
 import Idris.AbsSyntax
 import Idris.Core.Evaluate (unfold)
 import Idris.Core.TT
-import Util.Pretty
 
 import Data.List
 
@@ -72,13 +71,3 @@ errReverse ist t = rewrite 5 (do_unfold t) -- (elideLambdas t)
                                              Just (fs ++ as)
     -- no matching Binds, for now...
     match' ns x y = if x == y then Just [] else Nothing
-
-    -- if the term under a lambda is huge, there's no much point in showing
-    -- it as it won't be very enlightening.
-
-    elideLambdas (App s f a) = App s (elideLambdas f) (elideLambdas a)
-    elideLambdas (Bind n (Lam _ t) sc)
-       | size sc > 200 = P Ref (sUN "...") Erased
-    elideLambdas (Bind n b sc)
-       = Bind n (fmap elideLambdas b) (elideLambdas sc)
-    elideLambdas t = t
diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs
index 3207c8a00..4b8fb7471 100644
--- a/src/Idris/IBC.hs
+++ b/src/Idris/IBC.hs
@@ -51,7 +51,6 @@ data IBCPhase = IBC_Building  -- ^ when building the module tree
 data IBCFile = IBCFile {
     ver                        :: Word16
   , sourcefile                 :: FilePath
-  , ibc_reachablenames         :: ![Name]
   , ibc_imports                :: ![(Bool, FilePath)]
   , ibc_importdirs             :: ![FilePath]
   , ibc_sourcedirs             :: ![FilePath]
@@ -108,7 +107,7 @@ deriving instance Binary IBCFile
 !-}
 
 initIBC :: IBCFile
-initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []
+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []
 
 hasValidIBCVersion :: FilePath -> Idris Bool
 hasValidIBCVersion fp = do
@@ -1123,16 +1122,6 @@ instance Binary Accessibility where
                    3 -> return Hidden
                    _ -> error "Corrupted binary data for Accessibility"
 
-safeToEnum :: (Enum a, Bounded a, Integral int) => String -> int -> a
-safeToEnum label x' = result
-  where
-    x = fromIntegral x'
-    result
-        |  x < fromEnum (minBound `asTypeOf` result)
-        || x > fromEnum (maxBound `asTypeOf` result)
-            = error $ label ++ ": corrupted binary representation in IBC"
-        | otherwise = toEnum x
-
 instance Binary PReason where
         put x
           = case x of
diff --git a/src/Idris/IdeMode.hs b/src/Idris/IdeMode.hs
index a14bcaf1f..e91dc948a 100644
--- a/src/Idris/IdeMode.hs
+++ b/src/Idris/IdeMode.hs
@@ -176,9 +176,6 @@ instance SExpable OutputAnnotation where
 encodeName :: Name -> String
 encodeName n = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $ n
 
-decodeName :: String -> Name
-decodeName = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString
-
 encodeTerm :: [(Name, Bool)] -> Term -> String
 encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $
                     (bnd, tm)
diff --git a/src/Idris/IdrisDoc.hs b/src/Idris/IdrisDoc.hs
index eb370f47c..deccfc1d8 100644
--- a/src/Idris/IdrisDoc.hs
+++ b/src/Idris/IdrisDoc.hs
@@ -248,13 +248,6 @@ getAccess ist n =
      [(_, acc)] -> acc
      _          -> Private
 
--- | Simple predicate for whether an NsItem has Docs
-hasDoc :: NsItem -- ^ The NsItem to test
-       -> Bool   -- ^ The result
-hasDoc (_, Just _, _) = True
-hasDoc _              = False
-
-
 -- | Predicate saying whether a Name possibly may have docs defined
 --   Without this, getDocs from Idris.Docs may fail a pattern match.
 mayHaveDocs :: Name -- ^ The Name to test
diff --git a/src/Idris/Imports.hs b/src/Idris/Imports.hs
index b082f6c3b..f66574066 100644
--- a/src/Idris/Imports.hs
+++ b/src/Idris/Imports.hs
@@ -29,13 +29,13 @@ pkgIndex :: String -> FilePath
 pkgIndex s = "00" ++ s ++ "-idx.ibc"
 
 srcPath :: FilePath -> FilePath
-srcPath fp = let (n, ext) = splitExtension fp in
+srcPath fp = let (_, ext) = splitExtension fp in
                  case ext of
                     ".idr" -> fp
                     _ -> fp ++ ".idr"
 
 lsrcPath :: FilePath -> FilePath
-lsrcPath fp = let (n, ext) = splitExtension fp in
+lsrcPath fp = let (_, ext) = splitExtension fp in
                   case ext of
                      ".lidr" -> fp
                      _ -> fp ++ ".lidr"
diff --git a/src/Idris/Interactive.hs b/src/Idris/Interactive.hs
index 7278100f9..10a12e041 100644
--- a/src/Idris/Interactive.hs
+++ b/src/Idris/Interactive.hs
@@ -382,9 +382,7 @@ makeLemma fn updatefile l n
                                                                  StringAtom lem_app]]]
                         in runIO . hPutStrLn h $ convSExp "return" good n
 
-  where getIndent s = length (takeWhile isSpace s)
-
-        appArgs skip 0 _ = ""
+  where appArgs skip 0 _ = ""
         appArgs skip i (Bind n@(UN c) (Pi _ _ _ _) sc)
            | (thead c /= '_' && n `notElem` skip)
                 = " " ++ show n ++ appArgs skip (i - 1) sc
diff --git a/src/Idris/Package.hs b/src/Idris/Package.hs
index 85fa3dd63..b49cca089 100644
--- a/src/Idris/Package.hs
+++ b/src/Idris/Package.hs
@@ -333,11 +333,9 @@ auditPackage True  ipkg = do
     getIdrisFiles :: FilePath -> IO [FilePath]
     getIdrisFiles dir = do
       contents <- getDirectoryContents dir
-      let contents' = filter (\fname -> fname /= "." && fname /= "..") contents
 
       -- [ NOTE ] Directory >= 1.2.5.0 introduced `listDirectory` but later versions of directory appear to be causing problems with ghc 7.10.3 and cabal 1.22 in travis. Let's reintroduce the old ranges for directory to be sure.
 
-
       files <- forM contents (findRest dir)
       return $ filter (isIdrisFile) (concat files)
 
diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs
index 31ccc541a..744647f32 100644
--- a/src/Idris/Parser.hs
+++ b/src/Idris/Parser.hs
@@ -794,7 +794,6 @@ mutual :: SyntaxInfo -> IdrisParser [PDecl]
 mutual syn =
     do reservedHL "mutual"
        openBlock
-       let pvars = syn_params syn
        ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
        closeBlock
        fc <- getFC
@@ -1145,7 +1144,6 @@ clause syn
                         Just t -> return t
                         Nothing -> fail "Invalid clause"
               (do r <- rhs syn n
-                  let ctxt = tt_ctxt ist
                   let wsyn = syn { syn_namespace = [], syn_toplevel = False }
                   (wheres, nmap) <- choice [do x <- whereBlock n wsyn
                                                popIndent
@@ -1169,8 +1167,6 @@ clause syn
               fc <- getFC
               n_in <- fst <$> fnName; let n = expandNS syn n_in
               r <- rhs syn n
-              ist <- get
-              let ctxt = tt_ctxt ist
               let wsyn = syn { syn_namespace = [] }
               (wheres, nmap) <- choice [do x <- whereBlock n wsyn
                                            popIndent
@@ -1227,8 +1223,6 @@ clause syn
               wargs <- many (wExpr syn)
               let capp = PApp fc (PRef nfc [nfc] n) args
               (do r <- rhs syn n
-                  ist <- get
-                  let ctxt = tt_ctxt ist
                   let wsyn = syn { syn_namespace = [] }
                   (wheres, nmap) <- choice [do x <- whereBlock n wsyn
                                                popIndent
@@ -1573,11 +1567,6 @@ parseImports fname input
                      let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp
                      return ((mdoc, mname, ps, mrk'), annots, i)
 
-        imp m = ImportInfo False (toPath m)
-                           Nothing [] NoFC NoFC
-        ns = Spl.splitOn "."
-        toPath = foldl1' (</>) . ns
-
         addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]
         addPath [] _ = []
         addPath ((fc, AnnNamespace ns Nothing) : annots) path =
@@ -1882,8 +1871,6 @@ loadSource lidr f toline
 
 {-| Adds names to hide list -}
 addHides :: Ctxt Accessibility -> Idris ()
-addHides xs = do i <- getIState
-                 let defh = default_access i
-                 mapM_ doHide (toAlist xs)
+addHides xs = mapM_ doHide (toAlist xs)
   where doHide (n, a) = do setAccessibility n a
                            addIBC (IBCAccess n a)
diff --git a/src/Idris/Parser/Data.hs b/src/Idris/Parser/Data.hs
index 38538eb7f..ccff010d4 100644
--- a/src/Idris/Parser/Data.hs
+++ b/src/Idris/Parser/Data.hs
@@ -9,7 +9,6 @@ Maintainer  : The Idris Community.
 module Idris.Parser.Data where
 
 import Idris.AbsSyntax
-import Idris.Core.Evaluate
 import Idris.Core.TT
 import Idris.Docstrings
 import Idris.Options
@@ -55,18 +54,9 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do
                 return $ PRecord doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc syn
              <?> "record type declaration"
   where
-    getRecNames :: SyntaxInfo -> PTerm -> [Name]
-    getRecNames syn (PPi _ n _ _ sc) = [expandNS syn n, expandNS syn (mkType n)]
-                                         ++ getRecNames syn sc
-    getRecNames _ _ = []
-
     getName (Just (n, _), _, _, _) = Just n
     getName _ = Nothing
 
-    toFreeze :: Maybe Accessibility -> Maybe Accessibility
-    toFreeze (Just Frozen) = Just Private
-    toFreeze x = x
-
     recordBody :: SyntaxInfo -> Name -> IdrisParser ([((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))], Maybe (Name, FC), Docstring (Either Err PTerm))
     recordBody syn tyn = do
         ist <- get
diff --git a/src/Idris/PartialEval.hs b/src/Idris/PartialEval.hs
index d0c23a9a1..e48084a66 100644
--- a/src/Idris/PartialEval.hs
+++ b/src/Idris/PartialEval.hs
@@ -258,10 +258,6 @@ mkNewPats ist d ns newname sname lhs rhs =
     mkRHSargs (_ : ns) as = mkRHSargs ns as
     mkRHSargs _ _ = []
 
-    mkSubst :: (Term, Term) -> Maybe (Name, Term)
-    mkSubst (P _ n _, t) = Just (n, t)
-    mkSubst _ = Nothing
-
 -- | Creates a new declaration for a specialised function application.
 -- Simple version at the moment: just create a version which is a direct
 -- application of the function to be specialised.
diff --git a/src/Idris/Primitives.hs b/src/Idris/Primitives.hs
index 477f52fb6..9077d8e58 100644
--- a/src/Idris/Primitives.hs
+++ b/src/Idris/Primitives.hs
@@ -17,7 +17,6 @@ import Data.Bits
 import Data.Char
 import Data.Function (on)
 import Data.Int
-import Data.Word
 
 data Prim = Prim { p_name  :: Name,
                    p_type  :: Type,
@@ -31,10 +30,9 @@ ty :: [Const] -> Const -> Type
 ty []     x = Constant x
 ty (t:ts) x = Bind (sMN 0 "T") (Pi RigW Nothing (Constant t) (TType (UVar [] (-3)))) (ty ts x)
 
-total, partial, iopartial :: Totality
+total, partial :: Totality
 total = Total []
 partial = Partial NotCovering
-iopartial = Partial ExternalIO
 
 primitives :: [Prim]
 primitives =
@@ -232,36 +230,6 @@ intConv ity =
                (1, LFloatInt ity) total
     ]
 
-bitcastPrim :: ArithTy -> ArithTy -> (ArithTy -> [Const] -> Maybe Const) -> PrimFn -> Prim
-bitcastPrim from to impl prim =
-    Prim (sUN $ "prim__bitcast" ++ aTyName from ++ "_" ++ aTyName to) (ty [AType from] (AType to)) 1 (impl to)
-         (1, prim) total
-
-concatWord8 :: (Word8, Word8) -> Word16
-concatWord8 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 8)
-
-concatWord16 :: (Word16, Word16) -> Word32
-concatWord16 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 16)
-
-concatWord32 :: (Word32, Word32) -> Word64
-concatWord32 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 32)
-
-truncWord16 :: Bool -> Word16 -> Word8
-truncWord16 True x = fromIntegral (x `shiftR` 8)
-truncWord16 False x = fromIntegral x
-
-truncWord32 :: Bool -> Word32 -> Word16
-truncWord32 True x = fromIntegral (x `shiftR` 16)
-truncWord32 False x = fromIntegral x
-
-truncWord64 :: Bool -> Word64 -> Word32
-truncWord64 True x = fromIntegral (x `shiftR` 32)
-truncWord64 False x = fromIntegral x
-
-aTyName :: ArithTy -> String
-aTyName (ATInt t) = intTyName t
-aTyName ATFloat = "Float"
-
 iCmp  :: IntTy -> String -> Bool -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim
 iCmp ity op self impl irop totality
     = Prim (sUN $ "prim__" ++ op ++ intTyName ity)
@@ -292,11 +260,6 @@ bfBin op [Fl x, Fl y] = let i = (if op x y then 1 else 0) in
                         Just $ I i
 bfBin _ _ = Nothing
 
-bcBin :: (Char -> Char -> Bool) -> [Const] -> Maybe Const
-bcBin op [Ch x, Ch y] = let i = (if op x y then 1 else 0) in
-                        Just $ I i
-bcBin _ _ = Nothing
-
 bsBin :: (String -> String -> Bool) -> [Const] -> Maybe Const
 bsBin op [Str x, Str y]
     = let i = (if op x y then 1 else 0) in
diff --git a/src/Idris/ProofSearch.hs b/src/Idris/ProofSearch.hs
index e1a6204ff..378822f66 100644
--- a/src/Idris/ProofSearch.hs
+++ b/src/Idris/ProofSearch.hs
@@ -27,7 +27,6 @@ import Control.Monad
 import Control.Monad.State.Strict
 import Data.List
 import qualified Data.Set as S
-import Debug.Trace
 
 -- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm
 
@@ -49,7 +48,6 @@ trivialHoles psnames ok elab ist
         tryAll ((x, _, b):xs)
            = do -- if type of x has any holes in it, move on
                 hs <- get_holes
-                let badhs = hs -- filter (flip notElem holesOK) hs
                 g <- goal
                 -- anywhere but the top is okay for a hole, if holesOK set
                 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))
@@ -85,7 +83,6 @@ trivialTCs ok elab ist
         tryAll ((x, _, b):xs)
            = do -- if type of x has any holes in it, move on
                 hs <- get_holes
-                let badhs = hs -- filter (flip notElem holesOK) hs
                 g <- goal
                 env <- get_env
                 -- anywhere but the top is okay for a hole, if holesOK set
@@ -230,9 +227,6 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi
        | (P _ fn _, args@(_:_)) <- unApply fa = fn `notElem` hs
     notHole _ _ = True
 
-    inHS hs (P _ n _) = n `elem` hs
-    isHS _ _ = False
-
     toUN t@(P nt (MN i n) ty)
        | ('_':xs) <- str n = t
        | otherwise = P nt (UN n) ty
@@ -441,12 +435,6 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist
     isMeta ns (P _ n _) = n `elem` ns
     isMeta _ _ = False
 
-    notHole hs (P _ n _, c)
-       | (P _ cn _, _) <- unApply (getRetTy c),
-         n `elem` hs && isConName cn (tt_ctxt ist) = False
-       | Constant _ <- c = not (n `elem` hs)
-    notHole _ _ = True
-
     numinterface = sNS (sUN "Num") ["Interfaces","Prelude"]
 
     addDefault t num@(P _ nc _) [P Bound a _] | nc == numinterface && defaultOn
@@ -484,7 +472,6 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist
        | otherwise
            = do lams <- introImps
                 t <- goal
-                let (tc, ttypes) = trace (show t) $ unApply (getRetTy t)
 --                 if (all boundVar ttypes) then resolveTC (depth - 1) fn impls ist
 --                   else do
                    -- if there's a hole in the goal, don't even try
@@ -502,7 +489,7 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist
 --                 traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
                 mapM_ (\ (_,n) -> do focus n
                                      t' <- goal
-                                     let (tc', ttype) = unApply (getRetTy t')
+                                     let (tc', _) = unApply (getRetTy t')
                                      let got = fst (unApply (getRetTy t))
                                      let depth' = if tc' `elem` tcs
                                                      then depth - 1 else depth
diff --git a/src/Idris/Prover.hs b/src/Idris/Prover.hs
index db0548f6b..265218ecc 100644
--- a/src/Idris/Prover.hs
+++ b/src/Idris/Prover.hs
@@ -164,7 +164,7 @@ dumpState ist inElab menv ps | (h : hs) <- holes ps = do
   iputGoal rendered
 
   where
-    (h : hs) = holes ps -- apparently the pattern guards don't give us this
+    (h : _) = holes ps -- apparently the pattern guards don't give us this
 
     ppo = ppOptionIst ist
 
@@ -500,7 +500,6 @@ checkType e prf t = do
         putIState ist { tt_ctxt = ctxt' }
         (tm, ty) <- elabVal (recinfo proverfc) ERHS t
         let ppo = ppOptionIst ist
-            ty'     = normaliseC ctxt [] ty
             infixes = idris_infixes ist
             action = case tm of
               TType _ ->
diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs
index 1f9b64995..6de4d45b4 100644
--- a/src/Idris/REPL.hs
+++ b/src/Idris/REPL.hs
@@ -402,7 +402,6 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =
                          | (n, (_, i, _, _, _)) <- idris_metavars ist
                          , not (n `elem` primDefs)
                          ]
-     let ppo = ppOptionIst ist
      -- splitMvs is a list of pairs of names and their split types
      let splitMvs = [ (n, (premises, concl, tm))
                     | (n, i, ty) <- mvTys ist mvs
@@ -420,14 +419,11 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =
      runIO . hPutStrLn h $
        IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", mvOutput) id
   where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)
-        firstOfThree (x, y, z) = x
-        mapThird f xs = map (\(x, y, z) -> (x, y, f z)) xs
-
         -- | Split a function type into a pair of premises, conclusion.
         -- Each maintains both the original and delaborated versions.
         splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
         splitPi ist i (Bind n (Pi _ _ t _) rest) | i > 0 =
-          let (hs, c, pc) = splitPi ist (i - 1) rest in
+          let (hs, c, _) = splitPi ist (i - 1) rest in
             ((n, t, delabTy' ist [] [] t False False True):hs,
              c, delabTy' ist [] [] c False False True)
         splitPi ist i tm = ([], tm, delabTy' ist [] [] tm False False True)
@@ -1021,8 +1017,7 @@ process fn (Check t)
    = do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t
         ctxt <- getContext
         ist <- getIState
-        let ppo = ppOptionIst ist
-            ty' = if opt_evaltypes (idris_options ist)
+        let ty' = if opt_evaltypes (idris_options ist)
                      then normaliseC ctxt [] ty
                      else ty
         case tm of
@@ -1127,7 +1122,6 @@ process fn (DebugInfo n)
         when (not (null imps)) $ iputStrLn (show imps)
         let d = lookupDefAcc n False (tt_ctxt i)
         when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))
-        let cg = lookupCtxtName n (idris_callgraph i)
         i <- getIState
         let cg' = lookupCtxtName n (idris_callgraph i)
         sc <- checkSizeChange n
@@ -1457,12 +1451,6 @@ process fn (TransformInfo n)
                     ts' = showTrans i ts in
                     ppTm lhs <+> text " ==> " <+> ppTm rhs : ts'
 
---               iRenderOutput (pretty lhs)
---                    iputStrLn "  ==>  "
---                    iPrintTermWithType (pprintDelab i rhs)
---                    iputStrLn "---------------"
---                    showTrans i ts
-
 process fn (PPrint fmt width (PRef _ _ n))
    = do outs <- pprintDef False n
         iPrintResult =<< renderExternal fmt width (vsep outs)
@@ -1470,10 +1458,7 @@ process fn (PPrint fmt width (PRef _ _ n))
 
 process fn (PPrint fmt width t)
    = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t
-        ctxt <- getContext
         ist <- getIState
-        let ppo = ppOptionIst ist
-            ty' = normaliseC ctxt [] ty
         iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)
 
 
diff --git a/src/Idris/REPL/Parser.hs b/src/Idris/REPL/Parser.hs
index cdfcde7f8..f6f0956da 100644
--- a/src/Idris/REPL/Parser.hs
+++ b/src/Idris/REPL/Parser.hs
@@ -178,8 +178,6 @@ namespaceArgCmd names command doc =
   (names, NamespaceArg, doc, namespaceArg command)
 exprArgCmd names command doc =
   (names, ExprArg, doc, exprArg command)
-metavarArgCmd names command doc =
-  (names, MetaVarArg, doc, fnNameArg command)
 optArgCmd names command doc =
   (names, OptionArg, doc, optArg command)
 proofArgCmd names command doc =
diff --git a/src/Idris/Termination.hs b/src/Idris/Termination.hs
index a57e961ea..ffafb23e8 100644
--- a/src/Idris/Termination.hs
+++ b/src/Idris/Termination.hs
@@ -142,9 +142,6 @@ checkPositive mut_ns (cn, ty')
 calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality
 calcTotality fc n pats
     = do i <- getIState
-         let opts = case lookupCtxt n (idris_flags i) of
-                            [fs] -> fs
-                            _ -> []
          case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
             (failure : _) -> return failure
             _ -> checkSizeChange n
@@ -301,7 +298,7 @@ buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]
 buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
   scgPat (lhs, rhs) = let lhs' = delazy lhs
                           rhs' = delazy rhs
-                          (f, pargs) = unApply (dePat lhs') in
+                          (_, pargs) = unApply (dePat lhs') in
                             findCalls [] Toplevel (dePat rhs') (patvars lhs')
                                       (zip pargs [0..])
 
@@ -392,7 +389,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
   fccPat cases pvs pargs args g (lhs, rhs)
       = let lhs' = delazy lhs
             rhs' = delazy rhs
-            (f, pargs_case) = unApply (dePat lhs')
+            (_, pargs_case) = unApply (dePat lhs')
             -- pargs is a pair of a term, and the argument position that
             -- term appears in. If any of the arguments to the case block
             -- are also on the lhs, we also want those patterns to appear
@@ -544,10 +541,6 @@ checkMP ist topfn i mp = if i > 0
                                collapse paths
                      else tryPath 0 [] mp 0
   where
-    tryPath' d path mp arg
-           = let res = tryPath d path mp arg in
-                 trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res
-
     mkBig (e, d) = (e, 10000)
 
     tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality
diff --git a/src/Idris/TypeSearch.hs b/src/Idris/TypeSearch.hs
index 99a00741e..4bbbfa007 100644
--- a/src/Idris/TypeSearch.hs
+++ b/src/Idris/TypeSearch.hs
@@ -13,8 +13,7 @@ module Idris.TypeSearch (
   , defaultScoreFunction
   ) where
 
-import Idris.AbsSyntax (addImpl, addUsingConstraints, getIState, implicit,
-                        putIState)
+import Idris.AbsSyntax (addUsingConstraints, getIState, implicit, putIState)
 import Idris.AbsSyntaxTree (IState(idris_docstrings, idris_interfaces, idris_outputmode, tt_ctxt),
                             Idris, InterfaceInfo, OutputMode(..), PTerm,
                             defaultSyntax, eqTy, implicitAllowed,
@@ -58,7 +57,6 @@ searchByType pkgs pterm = do
   mapM_ loadPkgIndex pkgs
   pterm' <- addUsingConstraints syn emptyFC pterm
   pterm'' <- implicit toplevel syn name pterm'
-  let pterm'''  = addImpl [] i pterm''
   ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name NoFC pterm'
   let names = searchUsing searchPred i ty
   let names' = take numLimit names
@@ -304,7 +302,7 @@ interfaceUnify interfaceInfo ctxt ty tyTry = do
 
 isInterfaceArg :: Ctxt InterfaceInfo -> Type -> Bool
 isInterfaceArg interfaceInfo ty = not (null (getInterfaceName clss >>= flip lookupCtxt interfaceInfo)) where
-  (clss, args) = unApply ty
+  (clss, _) = unApply ty
   getInterfaceName (P (TCon _ _) interfaceName _) = [interfaceName]
   getInterfaceName _ = []
 
@@ -358,8 +356,6 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh
     usedns = map fst startingHoles
     startingHoles = argNames1 ++ argNames2
 
-    startingTypes = [(retTy1, retTy2)]
-
 
   startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)
   startQueueOfQueues = Q.fromList $ mapMaybe getStartQueues types

From 921ac8fd76d1a8ff46a6f40e3b6d6a3cc76803ec Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Sun, 17 Sep 2017 13:06:46 +0100
Subject: [PATCH 24/27] Added Data.IORef

This is intended for simple mutable state in IO, which is sometimes
useful for efficiency of global state.

STRef could work similarly, at some point.
---
 CHANGELOG.md               |  9 +++++++--
 libs/base/Data/IORef.idr   | 28 ++++++++++++++++++++++++++++
 libs/base/base.ipkg        |  1 +
 rts/idris_gc.c             |  8 +++++++-
 rts/idris_rts.c            | 20 ++++++++++++++++++++
 rts/idris_rts.h            | 10 ++++++++--
 test/TestData.hs           |  3 ++-
 test/basic021/basic021.idr | 13 +++++++++++++
 test/basic021/expected     |  1 +
 test/basic021/run          |  4 ++++
 10 files changed, 91 insertions(+), 6 deletions(-)
 create mode 100644 libs/base/Data/IORef.idr
 create mode 100644 test/basic021/basic021.idr
 create mode 100644 test/basic021/expected
 create mode 100755 test/basic021/run

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 41f31bc14..25e4078dc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,13 +1,18 @@
 # New in 1.1.*
 
-+ Addition of `Text.Literate`, a module for working with literate
-  source files.
+## Language updates
+
 + In `@`-patterns such as `x@p`, `x` is now in scope on the right-hand side
   of any definitions in `where` clauses, provided the left-hand side of the
   definition does not shadow it.
 + Private functions are no longer visible in the REPL except for modules
   that are explicitly loaded.
 
+## Library Updates
+
++ Added `Text.Literate`, a module for working with literate source files.
++ Added `Data.IORef`, for working with mutable references in `IO`.
+
 # New in 1.1.1
 
 + Erasure analysis is now faster thanks to a bit smarter constraint solving.
diff --git a/libs/base/Data/IORef.idr b/libs/base/Data/IORef.idr
new file mode 100644
index 000000000..bb5ecb5b3
--- /dev/null
+++ b/libs/base/Data/IORef.idr
@@ -0,0 +1,28 @@
+module Data.IORef
+
+export
+data IORef a = MkIORef a
+
+export
+newIORef : a -> IO (IORef a)
+newIORef val
+    = do MkRaw ref <- foreign FFI_C "idris_newRef" (Raw a -> IO (Raw a)) (MkRaw val)
+         pure (MkIORef ref)
+
+export
+readIORef : IORef a -> IO a
+readIORef (MkIORef ref)
+    = do MkRaw val <- foreign FFI_C "idris_readRef" (Raw a -> IO (Raw a)) (MkRaw ref)
+         pure val
+
+export
+writeIORef : IORef a -> a -> IO ()
+writeIORef (MkIORef old) val
+    = foreign FFI_C "idris_writeRef" (Raw a -> Raw a -> IO ())
+              (MkRaw old) (MkRaw val)
+
+export
+modifyIORef : IORef a -> (a -> a) -> IO ()
+modifyIORef ref fn
+    = do val <- readIORef ref
+         writeIORef ref (fn val)
diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg
index 8604ad2fa..80118bcf4 100644
--- a/libs/base/base.ipkg
+++ b/libs/base/base.ipkg
@@ -21,6 +21,7 @@ modules = System,
           Data.HVect,
           Data.Complex,
           Data.Erased,
+          Data.IORef,
           Data.List,
           Data.List.Views,
           Data.List.Quantifiers,
diff --git a/rts/idris_gc.c b/rts/idris_gc.c
index 9ffe94218..49ae86816 100644
--- a/rts/idris_gc.c
+++ b/rts/idris_gc.c
@@ -50,6 +50,9 @@ VAL copy(VM* vm, VAL x) {
     case CT_BITS64:
         cl = idris_b64CopyForGC(vm, x);
         break;
+    case CT_REF:
+        cl = idris_newRefLock((VAL)(x->info.ptr), 1);
+        break;
     case CT_FWD:
         return x->info.ptr;
     case CT_RAWDATA:
@@ -79,7 +82,7 @@ void cheney(VM *vm) {
     while(scan < vm->heap.next) {
        size_t inc = *((size_t*)scan);
        VAL heap_item = (VAL)(scan+sizeof(size_t));
-       // If it's a CT_CON or CT_STROFFSET, copy its arguments
+       // If it's a CT_CON, CT_REF or CT_STROFFSET, copy its arguments
        switch(GETTY(heap_item)) {
        case CT_CON:
            ar = ARITY(heap_item);
@@ -88,6 +91,9 @@ void cheney(VM *vm) {
                heap_item->info.c.args[i] = newptr;
            }
            break;
+       case CT_REF:
+           heap_item->info.ptr = copy(vm, (VAL)(heap_item->info.ptr));
+           break;
        case CT_STROFFSET:
            heap_item->info.str_offset->str
                = copy(vm, heap_item->info.str_offset->str);
diff --git a/rts/idris_rts.c b/rts/idris_rts.c
index 8cf3699c6..afad1b343 100644
--- a/rts/idris_rts.c
+++ b/rts/idris_rts.c
@@ -776,6 +776,26 @@ VAL idris_strRev(VM* vm, VAL str) {
     return cl;
 }
 
+VAL idris_newRefLock(VAL x, int outerlock) {
+    Closure* cl = allocate(sizeof(Closure), outerlock);
+    SETTY(cl, CT_REF);
+    cl->info.ptr = (void*)x;
+    return cl;
+}
+
+VAL idris_newRef(VAL x) {
+    return idris_newRefLock(x, 0);
+}
+
+void idris_writeRef(VAL ref, VAL x) {
+    ref->info.ptr = (void*)x;
+    SETTY(ref, CT_REF);
+}
+
+VAL idris_readRef(VAL ref) {
+    return (VAL)(ref->info.ptr);
+}
+
 VAL idris_systemInfo(VM* vm, VAL index) {
     int i = GETINT(index);
     switch(i) {
diff --git a/rts/idris_rts.h b/rts/idris_rts.h
index 11dd77454..89885be32 100644
--- a/rts/idris_rts.h
+++ b/rts/idris_rts.h
@@ -26,8 +26,8 @@
 // Closures
 typedef enum {
     CT_CON, CT_INT, CT_BIGINT, CT_FLOAT, CT_STRING, CT_STROFFSET,
-    CT_BITS8, CT_BITS16, CT_BITS32, CT_BITS64, CT_UNIT, CT_PTR, CT_FWD,
-    CT_MANAGEDPTR, CT_RAWDATA, CT_CDATA
+    CT_BITS8, CT_BITS16, CT_BITS32, CT_BITS64, CT_UNIT, CT_PTR, CT_REF,
+    CT_FWD, CT_MANAGEDPTR, CT_RAWDATA, CT_CDATA
 } ClosureType;
 
 typedef struct Closure *VAL;
@@ -401,6 +401,12 @@ VAL idris_strIndex(VM* vm, VAL str, VAL i);
 VAL idris_strRev(VM* vm, VAL str);
 VAL idris_substr(VM* vm, VAL offset, VAL length, VAL str);
 
+// Support for IORefs
+VAL idris_newRefLock(VAL x, int outerlock);
+VAL idris_newRef(VAL x);
+void idris_writeRef(VAL ref, VAL x);
+VAL idris_readRef(VAL ref);
+
 // system infox
 // used indices:
 //   0 returns backend
diff --git a/test/TestData.hs b/test/TestData.hs
index 229ee17d2..63d9118b5 100644
--- a/test/TestData.hs
+++ b/test/TestData.hs
@@ -72,7 +72,8 @@ testFamiliesData = [
       ( 17, ANY  ),
       ( 18, ANY  ),
       ( 19, ANY  ),
-      ( 20, ANY  )]),
+      ( 20, ANY  ),
+      ( 21, ANY  )]),
   ("bignum",          "Bignum",
     [ (  1, ANY  ),
       (  2, ANY  )]),
diff --git a/test/basic021/basic021.idr b/test/basic021/basic021.idr
new file mode 100644
index 000000000..df0786cb3
--- /dev/null
+++ b/test/basic021/basic021.idr
@@ -0,0 +1,13 @@
+import Data.IORef
+
+count : Nat -> IORef Integer -> IO ()
+count Z ref
+    = do x <- readIORef ref
+         printLn x
+count (S k) ref
+    = do modifyIORef ref (+1)
+         count k ref
+
+main : IO ()
+main = do r <- newIORef 0
+          count 1000000 r
diff --git a/test/basic021/expected b/test/basic021/expected
new file mode 100644
index 000000000..749fce669
--- /dev/null
+++ b/test/basic021/expected
@@ -0,0 +1 @@
+1000000
diff --git a/test/basic021/run b/test/basic021/run
new file mode 100755
index 000000000..fe2fae925
--- /dev/null
+++ b/test/basic021/run
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ basic021.idr -o basic021
+./basic021
+rm -f basic021 *.ibc

From f2790b0f553cafe7046100dcd4e37cfa38b41f3c Mon Sep 17 00:00:00 2001
From: Ahmad Salim Al-Sibahi <asal@itu.dk>
Date: Sun, 17 Sep 2017 18:37:56 +0200
Subject: [PATCH 25/27] Update CHANGELOG.md

---
 CHANGELOG.md | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 25e4078dc..d87af9099 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,14 +5,17 @@
 + In `@`-patterns such as `x@p`, `x` is now in scope on the right-hand side
   of any definitions in `where` clauses, provided the left-hand side of the
   definition does not shadow it.
-+ Private functions are no longer visible in the REPL except for modules
-  that are explicitly loaded.
+
 
 ## Library Updates
 
 + Added `Text.Literate`, a module for working with literate source files.
 + Added `Data.IORef`, for working with mutable references in `IO`.
 
+## Tool Updates
++ Private functions are no longer visible in the REPL except for modules
+  that are explicitly loaded.
+
 # New in 1.1.1
 
 + Erasure analysis is now faster thanks to a bit smarter constraint solving.

From 8cb13377494d0ae9d0d009aca831158514374e38 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Sun, 17 Sep 2017 17:33:02 +0100
Subject: [PATCH 26/27] Fix deprecation warning in Text.Literate

---
 libs/contrib/Text/Literate.idr | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/libs/contrib/Text/Literate.idr b/libs/contrib/Text/Literate.idr
index ae1b0fb43..9b80ff5c3 100644
--- a/libs/contrib/Text/Literate.idr
+++ b/libs/contrib/Text/Literate.idr
@@ -30,13 +30,13 @@ import Data.List.Views
 %default total
 
 untilEOL : Recognise False
-untilEOL = manyTill any (is '\n')
+untilEOL = manyUntil (is '\n') any
 
 line : String -> Lexer
 line s = exact s <+> space <+> untilEOL
 
 block : String -> String -> Lexer
-block s e = exact s <+> manyTill any (exact e)
+block s e = exact s <+> manyUntil (exact e) any 
 
 data Token = CodeBlock String String String
            | Any String

From 7e800ca01ae65b9f6e43ac77c5b394efe91f5fa4 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Sun, 17 Sep 2017 17:33:19 +0100
Subject: [PATCH 27/27] Small tweak to inlining

Choose whether to inline based on size of runtime thing (which might
have had partial evaluation applied, thus be very different) rather than
compile time thing. This seems to make little difference to run time,
but can prevent a lot of breaking of sharing and duplicated definitions
in defunctionalisation, thus making compile time much faster.
---
 src/IRTS/Compiler.hs       | 4 +++-
 src/Idris/Core/CaseTree.hs | 2 +-
 src/Idris/Core/Evaluate.hs | 2 +-
 src/Idris/ElabDecls.hs     | 2 ++
 4 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/IRTS/Compiler.hs b/src/IRTS/Compiler.hs
index 09c7aca5c..923e07b78 100644
--- a/src/IRTS/Compiler.hs
+++ b/src/IRTS/Compiler.hs
@@ -506,7 +506,9 @@ doForeign vs env (ret : fname : world : args)
         = do let l' = toFDesc l
              r' <- irTerm (sMN 0 "__foreignCall") vs env r
              return (l', r')
-    splitArg _ = ifail "Badly formed foreign function call"
+    splitArg _ = ifail $ "Badly formed foreign function call: " ++
+                         show (ret : fname : world : args)
+     
 
     toFDesc (Constant (Str str)) = FStr str
     toFDesc tm
diff --git a/src/Idris/Core/CaseTree.hs b/src/Idris/Core/CaseTree.hs
index 15bef022d..cb8e40ec2 100644
--- a/src/Idris/Core/CaseTree.hs
+++ b/src/Idris/Core/CaseTree.hs
@@ -122,7 +122,7 @@ instance TermSize CaseAlt where
 small :: Name -> [Name] -> SC -> Bool
 small n args t = let as = findAllUsedArgs t args in
                      length as == length (nub as) &&
-                     termsize n t < 10
+                     termsize n t < 20
 
 namesUsed :: SC -> [Name]
 namesUsed sc = nub $ nu' [] sc where
diff --git a/src/Idris/Core/Evaluate.hs b/src/Idris/Core/Evaluate.hs
index c7a866fe7..b0fc24ea7 100644
--- a/src/Idris/Core/Evaluate.hs
+++ b/src/Idris/Core/Evaluate.hs
@@ -951,7 +951,7 @@ addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)
                     ( CaseDef args_ct sc_ct _,
                      CaseDef args_rt sc_rt _) ->
                        let inl = alwaysInline -- tcdict
-                           inlc = (inl || small n args_ct sc_ct) && (not asserted)
+                           inlc = (inl || small n args_rt sc_rt) && (not asserted)
                            cdef = CaseDefs (args_ct, sc_ct)
                                            (args_rt, sc_rt)
                            op = (CaseOp (ci { case_inlinable = inlc })
diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs
index 8fd757e30..a35c92e90 100644
--- a/src/Idris/ElabDecls.hs
+++ b/src/Idris/ElabDecls.hs
@@ -280,6 +280,8 @@ elabDecl' _ info (PDSL n dsl)
            ifail "You must turn on the DSLNotation extension to use a dsl block"
          putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })
          addIBC (IBCDSL n)
+elabDecl' what info (PDirective i@(DLogging _))
+  = directiveAction i
 elabDecl' what info (PDirective i)
   | what /= EDefns = directiveAction i
 elabDecl' what info (PProvider doc syn fc nfc provWhat n)