From d6d07ff197b082bf4e25e6daaede73aa193a977e Mon Sep 17 00:00:00 2001
From: Calvin Beck <hobbes@ualberta.ca>
Date: Sat, 28 Feb 2015 12:58:26 -0700
Subject: [PATCH 1/6] GC check allocation of new heap.

---
 rts/idris_gc.c | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/rts/idris_gc.c b/rts/idris_gc.c
index 5f3b85aad..ec5917779 100644
--- a/rts/idris_gc.c
+++ b/rts/idris_gc.c
@@ -119,6 +119,14 @@ void idris_gc(VM* vm) {
     char* newheap = malloc(vm->heap.size);
     char* oldheap = vm->heap.heap;
 
+    if (newheap == NULL) {
+        fprintf(stderr,
+                "GC ERROR: Unable to allocate new heap. Requested %zd bytes.\n",
+                vm->heap.size);
+        
+        exit(EXIT_FAILURE);
+    }
+    
     vm->heap.heap = newheap;
 #ifdef FORCE_ALIGNMENT
     if (((i_int)(vm->heap.heap)&1) == 1) {

From 8f9ac37a02af2d45c2ca52c6a37076eafecd4166 Mon Sep 17 00:00:00 2001
From: Calvin Beck <hobbes@ualberta.ca>
Date: Sat, 28 Feb 2015 14:41:22 -0700
Subject: [PATCH 2/6] Generalized alloc_heap so it could be reused for garbage
 collection.

---
 rts/idris_gc.c   | 17 +++--------------
 rts/idris_heap.c |  9 ++++++---
 rts/idris_heap.h |  2 +-
 rts/idris_rts.c  |  2 +-
 4 files changed, 11 insertions(+), 19 deletions(-)

diff --git a/rts/idris_gc.c b/rts/idris_gc.c
index 5f3b85aad..21a727523 100644
--- a/rts/idris_gc.c
+++ b/rts/idris_gc.c
@@ -116,19 +116,8 @@ void idris_gc(VM* vm) {
     if (vm->heap.old != NULL)
         free(vm->heap.old);
 
-    char* newheap = malloc(vm->heap.size);
-    char* oldheap = vm->heap.heap;
-
-    vm->heap.heap = newheap;
-#ifdef FORCE_ALIGNMENT
-    if (((i_int)(vm->heap.heap)&1) == 1) {
-        vm->heap.next = newheap + 1;
-    } else
-#endif
-    {
-        vm->heap.next = newheap;
-    }
-    vm->heap.end  = newheap + vm->heap.size;
+    /* Allocate swap heap. */
+    alloc_heap(&vm->heap, vm->heap.size, vm->heap.growth, vm->heap.heap);
 
     VAL* root;
 
@@ -143,6 +132,7 @@ void idris_gc(VM* vm) {
         msg->msg = copy(vm, msg->msg);
     }
 #endif
+
     vm->ret = copy(vm, vm->ret);
     vm->reg1 = copy(vm, vm->reg1);
 
@@ -154,7 +144,6 @@ void idris_gc(VM* vm) {
     if ((vm->heap.next - vm->heap.heap) > vm->heap.size >> 1) {
         vm->heap.size += vm->heap.growth;
     }
-    vm->heap.old = oldheap;
 
     STATS_LEAVE_GC(vm->stats, vm->heap.size, vm->heap.next - vm->heap.heap)
     HEAP_CHECK(vm)
diff --git a/rts/idris_heap.c b/rts/idris_heap.c
index e94fbb23a..47dfc3965 100644
--- a/rts/idris_heap.c
+++ b/rts/idris_heap.c
@@ -5,7 +5,9 @@
 #include <stddef.h>
 #include <stdio.h>
 
-void alloc_heap(Heap * h, size_t heap_size) 
+
+/* Used for initializing the heap. */
+void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old) 
 {
     char * mem = malloc(heap_size); 
     if (mem == NULL) {
@@ -27,9 +29,9 @@ void alloc_heap(Heap * h, size_t heap_size)
     h->end  = h->heap + heap_size;
 
     h->size   = heap_size;
-    h->growth = heap_size;
+    h->growth = growth;
 
-    h->old = NULL;
+    h->old = old;
 }
 
 void free_heap(Heap * h) {
@@ -40,6 +42,7 @@ void free_heap(Heap * h) {
     }
 }
 
+
 // TODO: more testing
 /******************** Heap testing ********************************************/
 void heap_check_underflow(Heap * heap) {
diff --git a/rts/idris_heap.h b/rts/idris_heap.h
index 3ebb1e3b2..1d10d9dfb 100644
--- a/rts/idris_heap.h
+++ b/rts/idris_heap.h
@@ -14,7 +14,7 @@ typedef struct {
 } Heap;
 
 
-void alloc_heap(Heap * heap, size_t heap_size);
+void alloc_heap(Heap * heap, size_t heap_size, size_t growth, char * old);
 void free_heap(Heap * heap);
 
 
diff --git a/rts/idris_rts.c b/rts/idris_rts.c
index 46060f2a8..e034bafc6 100644
--- a/rts/idris_rts.c
+++ b/rts/idris_rts.c
@@ -29,7 +29,7 @@ VM* init_vm(int stack_size, size_t heap_size,
     vm->valstack_base = valstack;
     vm->stack_max = valstack + stack_size;
 
-    alloc_heap(&(vm->heap), heap_size);
+    alloc_heap(&(vm->heap), heap_size, heap_size, NULL);
 
     vm->ret = NULL;
     vm->reg1 = NULL;

From 15737d9c4bf0f9e485d207170a68c5eb5374cede Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Thu, 19 Mar 2015 12:56:05 +0000
Subject: [PATCH 3/6] Trickiness with implicits in dependent classes

Need to expand implicits for methods in the dictionary declarataion, but
not quite the same way as for the top level function of the same name
(i.e. need to leave out the dictionary itself).

Fixes #1975
---
 idris.cabal                |  3 +++
 src/Idris/AbsSyntax.hs     | 46 +++++++++++++++++++++++---------------
 src/Idris/AbsSyntaxTree.hs |  5 ++++-
 src/Idris/Coverage.hs      |  2 +-
 src/Idris/DeepSeq.hs       |  4 ++--
 src/Idris/Elab/Class.hs    | 22 +++++++++---------
 src/Idris/Elab/Clause.hs   |  2 +-
 src/Idris/Elab/Data.hs     |  3 ++-
 src/Idris/Elab/Instance.hs |  2 +-
 src/Idris/Elab/Type.hs     |  8 +++----
 src/Idris/Elab/Value.hs    |  2 +-
 src/Idris/IBC.hs           |  4 ++--
 src/Idris/TypeSearch.hs    |  2 +-
 test/reg059/expected       |  0
 test/reg059/reg059.idr     |  8 +++++++
 test/reg059/run            |  3 +++
 16 files changed, 72 insertions(+), 44 deletions(-)
 create mode 100644 test/reg059/expected
 create mode 100644 test/reg059/reg059.idr
 create mode 100755 test/reg059/run

diff --git a/idris.cabal b/idris.cabal
index 105817db0..01d9747e1 100644
--- a/idris.cabal
+++ b/idris.cabal
@@ -289,6 +289,9 @@ Extra-source-files:
                        test/reg058/run
                        test/reg058/*.idr
                        test/reg058/expected
+                       test/reg059/run
+                       test/reg059/*.idr
+                       test/reg059/expected
 
                        test/basic001/run
                        test/basic001/*.idr
diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs
index 9163c6a14..e6baaaa34 100644
--- a/src/Idris/AbsSyntax.hs
+++ b/src/Idris/AbsSyntax.hs
@@ -1481,31 +1481,34 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
 
 -- Add implicit arguments in function calls
 addImplPat :: IState -> PTerm -> PTerm
-addImplPat = addImpl' True [] []
+addImplPat = addImpl' True [] [] []
 
 addImplBound :: IState -> [Name] -> PTerm -> PTerm
-addImplBound ist ns = addImpl' False ns [] ist
+addImplBound ist ns = addImpl' False ns [] [] ist
 
 addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
-addImplBoundInf ist ns inf = addImpl' False ns inf ist
+addImplBoundInf ist ns inf = addImpl' False ns inf [] ist
 
 -- | Add the implicit arguments to applications in the term
-addImpl :: IState -> PTerm -> PTerm
+-- [Name] gives the names to always expend, even when under a binder of
+-- that name (this is to expand methods with implicit arguments in dependent
+-- type classes).
+addImpl :: [Name] -> IState -> PTerm -> PTerm
 addImpl = addImpl' False [] []
 
 -- TODO: in patterns, don't add implicits to function names guarded by constructors
 -- and *not* inside a PHidden
 
-addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
-addImpl' inpat env infns ist ptm
+addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
+addImpl' inpat env infns imp_meths ist ptm
          = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)
   where
     ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
     ai qq env ds (PRef fc f)
         | f `elem` infns = PInferRef fc f
-        | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []
+        | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq imp_meths ist fc f ds []
     ai qq env ds (PHidden (PRef fc f))
-        | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq ist fc f ds [])
+        | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq imp_meths ist fc f ds [])
     ai qq env ds (PEq fc lt rt l r)
       = let lt' = ai qq env ds lt
             rt' = ai qq env ds rt
@@ -1541,7 +1544,7 @@ addImpl' inpat env infns ist ptm
         | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)
         | not (f `elem` map fst env)
                           = let as' = map (fmap (ai qq env ds)) as in
-                                handleErr $ aiFn inpat False qq ist fc f ds as'
+                                handleErr $ aiFn inpat False qq imp_meths ist fc f ds as'
         | Just (Just ty) <- lookup f env =
              let as' = map (fmap (ai qq env ds)) as
                  arity = getPArity ty in
@@ -1576,7 +1579,9 @@ addImpl' inpat env infns ist ptm
              _ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])
     ai qq env ds (PPi p n ty sc)
       = let ty' = ai qq env ds ty
-            sc' = ai qq ((n, Just ty):env) ds sc in
+            env' = if n `elem` imp_meths then env
+                      else ((n, Just ty) : env)
+            sc' = ai qq env' ds sc in
             PPi p n ty' sc'
     ai qq env ds (PGoal fc r n sc)
       = let r' = ai qq env ds r
@@ -1600,8 +1605,8 @@ addImpl' inpat env infns ist ptm
 -- if in a pattern, and there are no arguments, and there's no possible
 -- names with zero explicit arguments, don't add implicits.
 
-aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
-aiFn inpat True qq ist fc f ds []
+aiFn :: Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm
+aiFn inpat True qq imp_meths ist fc f ds []
   = case lookupDef f (tt_ctxt ist) of
         [] -> Right $ PPatvar fc f
         alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
@@ -1609,7 +1614,7 @@ aiFn inpat True qq ist fc f ds []
                     if (not (vname f) || tcname f
                            || any (conCaf (tt_ctxt ist)) ialts)
 --                            any constructor alts || any allImp ialts))
-                        then aiFn inpat False qq ist fc f ds [] -- use it as a constructor
+                        then aiFn inpat False qq imp_meths ist fc f ds [] -- use it as a constructor
                         else Right $ PPatvar fc f
     where imp (PExp _ _ _ _) = False
           imp _ = True
@@ -1623,9 +1628,9 @@ aiFn inpat True qq ist fc f ds []
           vname (UN n) = True -- non qualified
           vname _ = False
 
-aiFn inpat expat qq ist fc f ds as
+aiFn inpat expat qq imp_meths ist fc f ds as
     | f `elem` primNames = Right $ PApp fc (PRef fc f) as
-aiFn inpat expat qq ist fc f ds as
+aiFn inpat expat qq imp_meths ist fc f ds as
           -- This is where namespaces get resolved by adding PAlternative
      = do let ns = lookupCtxtName f (idris_implicits ist)
           let nh = filter (\(n, _) -> notHidden n) ns
@@ -1633,15 +1638,20 @@ aiFn inpat expat qq ist fc f ds as
                          [] -> nh
                          x -> x
           case ns' of
-            [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
+            [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc (isImpName f f')) (insertImpl ns as)
             [] -> if f `elem` (map fst (idris_metavars ist))
                     then Right $ PApp fc (PRef fc f) as
                     else Right $ mkPApp fc (length as) (PRef fc f) as
             alts -> Right $
                          PAlternative True $
-                           map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
+                           map (\(f', ns) -> mkPApp fc (length ns) (PRef fc (isImpName f f'))
                                                   (insertImpl ns as)) alts
   where
+    -- if the name is in imp_meths, we should actually refer to the bound
+    -- name rather than the global one after expanding implicits
+    isImpName f f' | f `elem` imp_meths = f
+                   | otherwise = f'
+
     trimAlts [] alts = alts
     trimAlts ns alts
         = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts
@@ -1685,7 +1695,7 @@ aiFn inpat expat qq ist fc f ds as
               PImp p True l n Placeholder :
                 insImpAcc (M.insert n Placeholder pnas) ps given imps
     insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =
-      let sc = addImpl ist (substMatches (M.toList pnas) sc') in
+      let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in
         case find n imps [] of
             Just (tm, imps') ->
               PTacImplicit p l n sc tm :
diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs
index a909112c7..057dd7921 100644
--- a/src/Idris/AbsSyntaxTree.hs
+++ b/src/Idris/AbsSyntaxTree.hs
@@ -1198,6 +1198,9 @@ data SyntaxInfo = Syn { using :: [Using],
                         syn_params :: [(Name, PTerm)],
                         syn_namespace :: [String],
                         no_imp :: [Name],
+                        imp_methods :: [Name], -- class methods. When expanding
+                           -- implicits, these should be expanded even under
+                           -- binders
                         decoration :: Name -> Name,
                         inPattern :: Bool,
                         implicitAllowed :: Bool,
@@ -1211,7 +1214,7 @@ deriving instance NFData SyntaxInfo
 deriving instance Binary SyntaxInfo
 !-}
 
-defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0
+defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0
 
 expandNS :: SyntaxInfo -> Name -> Name
 expandNS syn n@(NS _ _) = n
diff --git a/src/Idris/Coverage.hs b/src/Idris/Coverage.hs
index da1dcba58..1bc6b39ea 100644
--- a/src/Idris/Coverage.hs
+++ b/src/Idris/Coverage.hs
@@ -24,7 +24,7 @@ import Control.Monad.State.Strict
 -- provided explicitly from new clause generation.
 mkPatTm :: PTerm -> Idris Term
 mkPatTm t = do i <- getIState
-               let timp = addImpl' True [] [] i t
+               let timp = addImpl' True [] [] [] i t
                evalStateT (toTT (mapPT deNS timp)) 0
   where
     toTT (PRef _ n) = do i <- lift getIState
diff --git a/src/Idris/DeepSeq.hs b/src/Idris/DeepSeq.hs
index cd62fae18..8ae758578 100644
--- a/src/Idris/DeepSeq.hs
+++ b/src/Idris/DeepSeq.hs
@@ -353,10 +353,10 @@ instance NFData Using where
         rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
 
 instance NFData SyntaxInfo where
-        rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)
+        rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)
           = rnf x1 `seq`
               rnf x2 `seq`
                 rnf x3 `seq`
                   rnf x4 `seq`
                     rnf x5 `seq`
-                      rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()
+                      rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()
diff --git a/src/Idris/Elab/Class.hs b/src/Idris/Elab/Class.hs
index a7f9485d8..c9eff361a 100644
--- a/src/Idris/Elab/Class.hs
+++ b/src/Idris/Elab/Class.hs
@@ -77,28 +77,28 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
               = unzip (map (\ ( x,y,z) -> (x, y)) ims)
          let defaults = map (\ (x, (y, z)) -> (x,y)) defs
          -- build instance constructor type
-         -- decorate names of functions to ensure they can't be referred
-         -- to elsewhere in the class declaration
          let cty = impbind ps $ conbind constraints
                       $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)
                                constraint
          let cons = [(emptyDocstring, [], cn, cty, fc, [])]
          let ddecl = PDatadecl tn tty cons
          logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)
-         elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl
-
+         -- Elaborate the data declaration
+         elabData info (syn { no_imp = no_imp syn ++ mnames,
+                              imp_methods = mnames }) doc pDocs fc [] ddecl
          dets <- findDets cn fds
          addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [] dets)
+
          -- for each constraint, build a top level function to chase it
-         logLvl 5 $ "Building functions"
---          let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps
---                                       ++ using syn }
-         fns <- mapM (cfun cn constraint syn (map fst imethods)) constraints
-         mapM_ (rec_elabDecl info EAll info) (concat fns)
+         cfns <- mapM (cfun cn constraint syn (map fst imethods)) constraints
+         mapM_ (rec_elabDecl info EAll info) (concat cfns)
+
          -- for each method, build a top level function
          fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods
          logLvl 5 $ "Functions " ++ show fns
+         -- Elaborate the the top level methods
          mapM_ (rec_elabDecl info EAll info) (concat fns)
+
          -- add the default definitions
          mapM_ (rec_elabDecl info EAll info) (concat (map (snd.snd) defs))
          addIBC (IBCClass tn)
@@ -134,8 +134,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
 
     getMName (PTy _ _ _ _ _ n _) = nsroot n
     tdecl allmeths (PTy doc _ syn _ o n t)
-           = do t' <- implicit' info syn allmeths n t
-                logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
+           = do t' <- implicit' info syn (map fst ps ++ allmeths) n t
+                logLvl 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
                 return ( (n, (toExp (map fst ps) Exp t')),
                          (n, (doc, o, (toExp (map fst ps)
                                          (\ l s p -> Imp l s p Nothing) t'))),
diff --git a/src/Idris/Elab/Clause.hs b/src/Idris/Elab/Clause.hs
index 2828558ce..6d6fe687f 100644
--- a/src/Idris/Elab/Clause.hs
+++ b/src/Idris/Elab/Clause.hs
@@ -548,7 +548,7 @@ elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
 elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
    = do let tcgen = Dictionary `elem` opts
         i <- get
-        let lhs = addImpl i lhs_in
+        let lhs = addImpl [] i lhs_in
         b <- checkPossible info fc tcgen fname lhs_in
         case b of
             True -> tclift $ tfail (At fc
diff --git a/src/Idris/Elab/Data.hs b/src/Idris/Elab/Data.hs
index c1396c9f6..772ce9bfd 100644
--- a/src/Idris/Elab/Data.hs
+++ b/src/Idris/Elab/Data.hs
@@ -215,6 +215,7 @@ elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
            Idris (Name, Type)
 elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
     = do checkUndefined fc n
+         logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in
          (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)
          ctxt <- getContext
          let cty' = normalise ctxt [] cty
@@ -223,7 +224,7 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
          -- Check that the constructor type is, in fact, a part of the family being defined
          tyIs n cty'
 
-         logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
+         logLvl 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t
          logLvl 5 $ "Inaccessible args: " ++ show inacc
          logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'
 
diff --git a/src/Idris/Elab/Instance.hs b/src/Idris/Elab/Instance.hs
index c0191303d..9ab3d0ae3 100644
--- a/src/Idris/Elab/Instance.hs
+++ b/src/Idris/Elab/Instance.hs
@@ -167,7 +167,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do
         = do ty' <- addUsingConstraints syn fc t
              -- TODO think: something more in info?
              ty' <- implicit info syn iname ty'
-             let ty = addImpl i ty'
+             let ty = addImpl [] i ty'
              ctxt <- getContext
              (ElabResult tyT _ _ ctxt' newDecls, _) <-
                 tclift $ elaborate ctxt iname (TType (UVal 0)) initEState
diff --git a/src/Idris/Elab/Type.hs b/src/Idris/Elab/Type.hs
index b8ce1ed68..defecb461 100644
--- a/src/Idris/Elab/Type.hs
+++ b/src/Idris/Elab/Type.hs
@@ -57,13 +57,13 @@ buildType info syn fc opts n ty' = do
          ctxt <- getContext
          i <- getIState
 
-         logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'
+         logLvl 2 $ show n ++ " pre-type " ++ showTmImpls ty' ++ show (no_imp syn)
          ty' <- addUsingConstraints syn fc ty'
          ty' <- addUsingImpls syn n fc ty'
-         let ty = addImpl i ty'
+         let ty = addImpl (imp_methods syn) i ty'
 
-         logLvl 3 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'
-         logLvl 3 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty
+         logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'
+         logLvl 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty
 
          (ElabResult tyT' defer is ctxt' newDecls, log) <-
             tclift $ elaborate ctxt n (TType (UVal 0)) initEState
diff --git a/src/Idris/Elab/Value.hs b/src/Idris/Elab/Value.hs
index 289aabfd4..02676f8a3 100644
--- a/src/Idris/Elab/Value.hs
+++ b/src/Idris/Elab/Value.hs
@@ -56,7 +56,7 @@ elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Nam
 elabValBind info aspat norm tm_in
    = do ctxt <- getContext
         i <- getIState
-        let tm = addImpl i tm_in
+        let tm = addImpl [] i tm_in
         logLvl 10 (showTmImpls tm)
         -- try:
         --    * ordinary elaboration
diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs
index 9293211b2..97b4785b1 100644
--- a/src/Idris/IBC.hs
+++ b/src/Idris/IBC.hs
@@ -1420,7 +1420,7 @@ instance Binary Using where
                     _ -> error "Corrupted binary data for Using"
 
 instance Binary SyntaxInfo where
-        put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7 _)
+        put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _)
           = do put x1
                put x2
                put x3
@@ -1436,7 +1436,7 @@ instance Binary SyntaxInfo where
                x5 <- get
                x6 <- get
                x7 <- get
-               return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7 0)
+               return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0)
 
 instance (Binary t) => Binary (PClause' t) where
         put x
diff --git a/src/Idris/TypeSearch.hs b/src/Idris/TypeSearch.hs
index 99b9caab3..ea9865327 100644
--- a/src/Idris/TypeSearch.hs
+++ b/src/Idris/TypeSearch.hs
@@ -46,7 +46,7 @@ searchByType pkgs pterm = do
   mapM_ loadPkgIndex pkgs
   pterm' <- addUsingConstraints syn emptyFC pterm
   pterm'' <- implicit toplevel syn name pterm'
-  let pterm'''  = addImpl i pterm''
+  let pterm'''  = addImpl [] i pterm''
   ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name pterm'
   let names = searchUsing searchPred i ty
   let names' = take numLimit names
diff --git a/test/reg059/expected b/test/reg059/expected
new file mode 100644
index 000000000..e69de29bb
diff --git a/test/reg059/reg059.idr b/test/reg059/reg059.idr
new file mode 100644
index 000000000..e6ae64732
--- /dev/null
+++ b/test/reg059/reg059.idr
@@ -0,0 +1,8 @@
+class Monad m => ContainerMonad (m : Type -> Type) where
+    Elem : a -> m a -> Type
+    tagElem : (mx : m a) -> m (x : a ** Elem x mx)
+
+class Monad m => ContainerMonad2 a (m : Type -> Type) where
+    Elem2 : a -> m a -> Type
+    tagElem2 : (mx : m a) -> m (x : a ** Elem2 x mx)
+
diff --git a/test/reg059/run b/test/reg059/run
new file mode 100755
index 000000000..7083398b4
--- /dev/null
+++ b/test/reg059/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+idris $@ reg059.idr --check
+rm -f *.ibc

From f4aaf01b348f7aa9d0f93072a16d938614ad199f Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Thu, 19 Mar 2015 16:23:43 +0000
Subject: [PATCH 4/6] Guard !! in forgetEnv

This means we get better error messages if there are scoping issues,
particularly as caused by 'where' clauses with missing types that can't
be inferred.

Fixes #1978
---
 src/Idris/Core/TT.hs        | 36 ++++++++++++++++++++++++++----------
 src/Idris/Elab/Clause.hs    | 18 +++++++++---------
 src/Idris/Elab/Instance.hs  |  2 +-
 src/Idris/Elab/Transform.hs |  4 ++--
 src/Idris/Elab/Type.hs      |  6 +++---
 src/Idris/Elab/Utils.hs     | 28 +++++++++++++++++-----------
 src/Idris/Elab/Value.hs     |  4 ++--
 src/Idris/ElabTerm.hs       |  2 +-
 src/Idris/Prover.hs         |  2 +-
 test/quasiquote001/expected |  4 ++--
 test/unique001/expected     |  2 +-
 11 files changed, 65 insertions(+), 43 deletions(-)

diff --git a/src/Idris/Core/TT.hs b/src/Idris/Core/TT.hs
index 4ec9d6c29..bdaefe790 100644
--- a/src/Idris/Core/TT.hs
+++ b/src/Idris/Core/TT.hs
@@ -1170,17 +1170,33 @@ unList tm = case unApply tm of
 forget :: TT Name -> Raw
 forget tm = forgetEnv [] tm
 
+safeForget :: TT Name -> Maybe Raw
+safeForget tm = safeForgetEnv [] tm
+
 forgetEnv :: [Name] -> TT Name -> Raw
-forgetEnv env (P _ n _) = Var n
-forgetEnv env (V i)     = Var (env !! i)
-forgetEnv env (Bind n b sc) = let n' = uniqueName n env in
-                                  RBind n' (fmap (forgetEnv env) b)
-                                           (forgetEnv (n':env) sc)
-forgetEnv env (App f a) = RApp (forgetEnv env f) (forgetEnv env a)
-forgetEnv env (Constant c) = RConstant c
-forgetEnv env (TType i) = RType
-forgetEnv env (UType u) = RUType u
-forgetEnv env Erased    = RConstant Forgot
+forgetEnv env tm = case safeForgetEnv env tm of
+                     Just t' -> t'
+                     Nothing -> error $ "Scope error in " ++ show tm
+
+
+safeForgetEnv :: [Name] -> TT Name -> Maybe Raw
+safeForgetEnv env (P _ n _) = Just $ Var n
+safeForgetEnv env (V i) | i < length env = Just $ Var (env !! i)
+                        | otherwise = Nothing 
+safeForgetEnv env (Bind n b sc) 
+     = do let n' = uniqueName n env
+          b' <- safeForgetEnvB env b
+          sc' <- safeForgetEnv (n':env) sc
+          Just $ RBind n' b' sc'
+  where safeForgetEnvB env (Let t v) = liftM2 Let (safeForgetEnv env t) 
+                                                  (safeForgetEnv env v)
+        safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)
+                                  Just $ fmap (\_ -> ty') b 
+safeForgetEnv env (App f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)
+safeForgetEnv env (Constant c) = Just $ RConstant c
+safeForgetEnv env (TType i) = Just RType
+safeForgetEnv env (UType u) = Just $ RUType u
+safeForgetEnv env Erased    = Just $ RConstant Forgot
 
 -- | Introduce a 'Bind' into the given term for each element of the
 -- given list of (name, binder) pairs.
diff --git a/src/Idris/Elab/Clause.hs b/src/Idris/Elab/Clause.hs
index 6d6fe687f..1bf55e883 100644
--- a/src/Idris/Elab/Clause.hs
+++ b/src/Idris/Elab/Clause.hs
@@ -603,7 +603,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
         -- If we're inferring metavariables in the type, don't recheck,
         -- because we're only doing this to try to work out those metavariables
         (clhs_c, clhsty) <- if not inf
-                               then recheckC fc [] lhs_tm
+                               then recheckC fc id [] lhs_tm
                                else return (lhs_tm, lhs_ty)
         let clhs = normalise ctxt [] clhs_c
         let borrowed = borrowedNames [] clhs
@@ -681,7 +681,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
         logLvl 4 $ "---> " ++ show rhs'
         when (not (null defer)) $ iLOG $ "DEFERRED " ++
                     show (map (\ (n, (_,_,t)) -> (n, t)) defer)
-        def' <- checkDef fc defer
+        def' <- checkDef fc (Elaborating "deferred type of ") defer
         let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
         addDeferred def''
         mapM_ (\(n, _) -> addIBC (IBCDef n)) def''
@@ -700,7 +700,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
         logLvl 6 $ " ==> " ++ show (forget rhs')
 
         (crhs, crhsty) <- if not inf
-                             then recheckC_borrowing True borrowed fc [] rhs'
+                             then recheckC_borrowing True borrowed fc id [] rhs'
                              else return (rhs', clhsty)
         logLvl 6 $ " ==> " ++ show crhsty ++ "   against   " ++ show clhsty
         ctxt <- getContext
@@ -828,7 +828,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
         let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))
         let static_names = getStaticNames i lhs_tm
         logLvl 5 (show lhs_tm ++ "\n" ++ show static_names)
-        (clhs, clhsty) <- recheckC fc [] lhs_tm
+        (clhs, clhsty) <- recheckC fc id [] lhs_tm
         logLvl 5 ("Checked " ++ show clhs)
         let bargs = getPBtys (explicitNames (normalise ctxt [] lhs_tm))
         let wval = addImplBound i (map fst bargs) wval_in
@@ -847,12 +847,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
                             return (tt, d, is, ctxt', newDecls))
         setContext ctxt'
         processTacticDecls newDecls
-        def' <- checkDef fc defer
+        def' <- checkDef fc iderr defer
         let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
         addDeferred def''
         mapM_ (elabCaseBlock info opts) is
         logLvl 5 ("Checked wval " ++ show wval')
-        (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')
+        (cwval, cwvalty) <- recheckC fc id [] (getInferTerm wval')
         let cwvaltyN = explicitNames (normalise ctxt [] cwvalty)
         let cwvalN = explicitNames (normalise ctxt [] cwval)
         logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)
@@ -907,7 +907,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
         addIBC (IBCImp wname)
         addIBC (IBCStatic wname)
 
-        def' <- checkDef fc [(wname, (-1, Nothing, wtype))]
+        def' <- checkDef fc iderr [(wname, (-1, Nothing, wtype))]
         let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
         addDeferred def''
 
@@ -943,12 +943,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
         setContext ctxt'
         processTacticDecls newDecls
 
-        def' <- checkDef fc defer
+        def' <- checkDef fc iderr defer
         let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'
         addDeferred def''
         mapM_ (elabCaseBlock info opts) is
         logLvl 5 ("Checked RHS " ++ show rhs')
-        (crhs, crhsty) <- recheckC fc [] rhs'
+        (crhs, crhsty) <- recheckC fc id [] rhs'
         return $ (Right (clhs, crhs), lhs)
   where
     getImps (Bind n (Pi _ _ _) t) = pexp Placeholder : getImps t
diff --git a/src/Idris/Elab/Instance.hs b/src/Idris/Elab/Instance.hs
index 9ab3d0ae3..d4ea61b14 100644
--- a/src/Idris/Elab/Instance.hs
+++ b/src/Idris/Elab/Instance.hs
@@ -175,7 +175,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do
              setContext ctxt'
              processTacticDecls newDecls
              ctxt <- getContext
-             (cty, _) <- recheckC fc [] tyT
+             (cty, _) <- recheckC fc id [] tyT
              let nty = normalise ctxt [] cty
              return $ any (isJust . findOverlapping i (class_determiners ci) (delab i nty)) (class_instances ci)
 
diff --git a/src/Idris/Elab/Transform.hs b/src/Idris/Elab/Transform.hs
index 22ad47b41..a2d17c62f 100644
--- a/src/Idris/Elab/Transform.hs
+++ b/src/Idris/Elab/Transform.hs
@@ -63,7 +63,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
          let lhs_ty = getInferType lhs'
          let newargs = pvars i lhs_tm
 
-         (clhs_tm_in, clhs_ty) <- recheckC fc [] lhs_tm
+         (clhs_tm_in, clhs_ty) <- recheckC fc id [] lhs_tm
          let clhs_tm = renamepats pnames clhs_tm_in
          logLvl 3 ("Transform LHS " ++ show clhs_tm)
 
@@ -80,7 +80,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
          setContext ctxt'
          processTacticDecls newDecls
 
-         (crhs_tm_in, crhs_ty) <- recheckC fc [] rhs'
+         (crhs_tm_in, crhs_ty) <- recheckC fc id [] rhs'
          let crhs_tm = renamepats pnames crhs_tm_in
          logLvl 3 ("Transform RHS " ++ show crhs_tm)
 
diff --git a/src/Idris/Elab/Type.hs b/src/Idris/Elab/Type.hs
index defecb461..cdd4db209 100644
--- a/src/Idris/Elab/Type.hs
+++ b/src/Idris/Elab/Type.hs
@@ -75,7 +75,7 @@ buildType info syn fc opts n ty' = do
 
          logLvl 3 $ show ty ++ "\nElaborated: " ++ show tyT'
 
-         ds <- checkAddDef True False fc defer
+         ds <- checkAddDef True False fc iderr defer
          -- if the type is not complete, note that we'll need to infer
          -- things later (for solving metavariables)
          when (not (null ds)) $ addTyInferred n
@@ -85,7 +85,7 @@ buildType info syn fc opts n ty' = do
          logLvl 5 $ "Rechecking"
          logLvl 6 $ show tyT
          logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT
-         (cty, ckind)   <- recheckC fc [] tyT
+         (cty, ckind)   <- recheckC fc id [] tyT
 
          -- record the implicit and inaccessible arguments
          i <- getIState
@@ -154,7 +154,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
          -- 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
-         ds <- checkDef fc [(n, (-1, Nothing, usety))]
+         ds <- checkDef fc iderr [(n, (-1, Nothing, usety))]
          addIBC (IBCDef n)
          let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
          addDeferred ds'
diff --git a/src/Idris/Elab/Utils.hs b/src/Idris/Elab/Utils.hs
index 6b8e52f80..2147e863b 100644
--- a/src/Idris/Elab/Utils.hs
+++ b/src/Idris/Elab/Utils.hs
@@ -24,30 +24,36 @@ import qualified Data.Map as Map
 
 recheckC = recheckC_borrowing False []
 
-recheckC_borrowing uniq_check bs fc env t
+recheckC_borrowing uniq_check bs fc mkerr env t
     = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
          ctxt <- getContext
-         (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env (forget t) t of
-                                   Error e -> tfail (At fc e)
+         t' <- case safeForget t of
+                    Just ft -> return ft
+                    Nothing -> tclift $ tfail $ mkerr (At fc (IncompleteTerm t))
+         (tm, ty, cs) <- tclift $ case recheck_borrowing uniq_check bs ctxt env t' t of
+                                   Error e -> tfail (At fc (mkerr e))
                                    OK x -> return x
          logLvl 6 $ "CONSTRAINTS ADDED: " ++ show cs
          addConstraints fc cs
          return (tm, ty)
 
-checkDef :: FC -> [(Name, (Int, Maybe Name, Type))]
-         -> Idris [(Name, (Int, Maybe Name, Type))]
-checkDef fc ns = checkAddDef False True fc ns
+iderr :: Name -> Err -> Err
+iderr _ e = e
 
-checkAddDef :: Bool -> Bool -> FC
+checkDef :: FC -> (Name -> Err -> Err) -> [(Name, (Int, Maybe Name, Type))]
+         -> Idris [(Name, (Int, Maybe Name, Type))]
+checkDef fc mkerr ns = checkAddDef False True fc mkerr ns
+
+checkAddDef :: Bool -> Bool -> FC -> (Name -> Err -> Err)
             -> [(Name, (Int, Maybe Name, Type))]
             -> Idris [(Name, (Int, Maybe Name, Type))]
-checkAddDef add toplvl fc [] = return []
-checkAddDef add toplvl fc ((n, (i, top, t)) : ns) 
+checkAddDef add toplvl fc mkerr [] = return []
+checkAddDef add toplvl fc mkerr ((n, (i, top, t)) : ns) 
                = do ctxt <- getContext
-                    (t', _) <- recheckC fc [] t
+                    (t', _) <- recheckC fc (mkerr n) [] t
                     when add $ do addDeferred [(n, (i, top, t, toplvl))]
                                   addIBC (IBCDef n)
-                    ns' <- checkAddDef add toplvl fc ns
+                    ns' <- checkAddDef add toplvl fc mkerr ns
                     return ((n, (i, top, t')) : ns')
 
 -- | Get the list of (index, name) of inaccessible arguments from an elaborated
diff --git a/src/Idris/Elab/Value.hs b/src/Idris/Elab/Value.hs
index 02676f8a3..d21c8ff43 100644
--- a/src/Idris/Elab/Value.hs
+++ b/src/Idris/Elab/Value.hs
@@ -73,13 +73,13 @@ elabValBind info aspat norm tm_in
 
         let vtm = orderPats (getInferTerm tm')
 
-        def' <- checkDef (fileFC "(input)") defer
+        def' <- checkDef (fileFC "(input)") iderr defer
         let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
         addDeferred def''
         mapM_ (elabCaseBlock info []) is
 
         logLvl 3 ("Value: " ++ show vtm)
-        (vtm_in, vty) <- recheckC (fileFC "(input)") [] vtm
+        (vtm_in, vty) <- recheckC (fileFC "(input)") id [] vtm
 
         let vtm = if norm then normalise (tt_ctxt i) [] vtm_in
                           else vtm_in
diff --git a/src/Idris/ElabTerm.hs b/src/Idris/ElabTerm.hs
index 7a3447857..0e03f7e51 100644
--- a/src/Idris/ElabTerm.hs
+++ b/src/Idris/ElabTerm.hs
@@ -57,7 +57,7 @@ processTacticDecls info =
        updateIState $ \i -> i { idris_implicits =
                                   addDef n impls (idris_implicits i) }
        addIBC (IBCImp n)
-       ds <- checkDef fc [(n, (-1, Nothing, ty))]
+       ds <- checkDef fc iderr [(n, (-1, Nothing, ty))]
        addIBC (IBCDef n)
        let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
        addDeferred ds'
diff --git a/src/Idris/Prover.hs b/src/Idris/Prover.hs
index cea77de4e..64307d95f 100644
--- a/src/Idris/Prover.hs
+++ b/src/Idris/Prover.hs
@@ -78,7 +78,7 @@ prove opt ctxt lit n ty
          putIState (i { proof_list = (n, prf) : proofs })
          let tree = simpleCase False (STerm Erased) False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]
          logLvl 3 (show tree)
-         (ptm, pty) <- recheckC (fileFC "proof") [] tm
+         (ptm, pty) <- recheckC (fileFC "proof") id [] tm
          logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
                    "Expected type:" ++ show ty)
          case converts ctxt [] ty pty of
diff --git a/test/quasiquote001/expected b/test/quasiquote001/expected
index d5a4d7514..0ae58405a 100644
--- a/test/quasiquote001/expected
+++ b/test/quasiquote001/expected
@@ -1,5 +1,5 @@
 (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN Unit) (TType (UVar -1))))))
 --------------
-(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 48))) (TType (UVar 50))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 52))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 54)))))
+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 32))) (TType (UVar 34))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 36))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 38)))))
 --------------
-(App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (TType (UVar 48))) (TType (UVar 48)))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (TType (UVar 48))) (TType (UVar 48))))
+(App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (TType (UVar 32))) (TType (UVar 32)))) (App (App (App (App (P (DCon 0 4) (NS (UN MkPair) ["Builtins"]) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (NS (UN Pair) ["Builtins"]) Erased) (V 3)) (V 2))))))) (TType (UVar 30))) (TType (UVar 32))) (TType (UVar 32))) (TType (UVar 32))))
diff --git a/test/unique001/expected b/test/unique001/expected
index 02a87e2d3..307826897 100644
--- a/test/unique001/expected
+++ b/test/unique001/expected
@@ -17,4 +17,4 @@ with
 unique001b.idr:16:7:Borrowed name xs must not be used on RHS
 unique001c.idr:46:6:Unique name f is used more than once
 unique001d.idr:3:7:Borrowed name x must not be used on RHS
-unique001e.idr:4:11:Constructor Main.:: has a UniqueType, but the data type does not
+unique001e.idr:3:10:Constructor Main.Nil has a UniqueType, but the data type does not

From a281e23a3657399c2803601161481f25b85df14d Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Thu, 19 Mar 2015 17:03:20 +0000
Subject: [PATCH 5/6] Class resolution should not use private instances

---
 src/Idris/ElabTerm.hs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Idris/ElabTerm.hs b/src/Idris/ElabTerm.hs
index 0e03f7e51..c30de705e 100644
--- a/src/Idris/ElabTerm.hs
+++ b/src/Idris/ElabTerm.hs
@@ -1375,9 +1375,12 @@ findInstances :: IState -> Term -> [Name]
 findInstances ist t
     | (P _ n _, _) <- unApply t
         = case lookupCtxt n (idris_classes ist) of
-            [CI _ _ _ _ _ ins _] -> ins
+            [CI _ _ _ _ _ ins _] -> filter accessible ins
             _ -> []
     | otherwise = []
+  where accessible n = case lookupDefAccExact n False (tt_ctxt ist) of
+                            Just (_, Hidden) -> False
+                            _ -> True
 
 -- Try again to solve auto implicits
 solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()

From 03b75166a516163dbb82806684b4e27f152eec9b Mon Sep 17 00:00:00 2001
From: Edwin Brady <edwin.brady@gmail.com>
Date: Thu, 19 Mar 2015 19:00:23 +0000
Subject: [PATCH 6/6] Revert "GC check allocation of new heap."

---
 rts/idris_gc.c | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/rts/idris_gc.c b/rts/idris_gc.c
index b52bda96b..77cf65070 100644
--- a/rts/idris_gc.c
+++ b/rts/idris_gc.c
@@ -115,14 +115,6 @@ void idris_gc(VM* vm) {
     char* newheap = malloc(vm->heap.size);
     char* oldheap = vm->heap.heap;
 
-    if (newheap == NULL) {
-        fprintf(stderr,
-                "GC ERROR: Unable to allocate new heap. Requested %zd bytes.\n",
-                vm->heap.size);
-        
-        exit(EXIT_FAILURE);
-    }
-    
     vm->heap.heap = newheap;
 #ifdef FORCE_ALIGNMENT
     if (((i_int)(vm->heap.heap)&1) == 1) {