diff --git a/idris.cabal b/idris.cabal
--- a/idris.cabal
+++ b/idris.cabal
@@ -1,5 +1,5 @@
 Name:           idris
-Version:        0.9.20
+Version:        0.9.20.1
 License:        BSD3
 License-file:   LICENSE
 Author:         Edwin Brady
@@ -541,6 +541,14 @@
                        test/interactive010/expected
                        test/interactive010/input
                        test/interactive010/run
+                       test/interactive011/expected
+                       test/interactive011/input
+                       test/interactive011/run
+                       test/interactive011/*.idr
+                       test/interactive012/expected
+                       test/interactive012/input
+                       test/interactive012/run
+                       test/interactive012/*.idr
 
                        test/io001/run
                        test/io001/*.idr
diff --git a/rts/Makefile b/rts/Makefile
--- a/rts/Makefile
+++ b/rts/Makefile
@@ -1,7 +1,8 @@
 include ../config.mk
 
 OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_bitstring.o \
-       idris_opts.o idris_stats.o idris_utf8.o mini-gmp.o getline.o
+       idris_opts.o idris_stats.o idris_utf8.o idris_stdfgn.o mini-gmp.o \
+       getline.o
 HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_bitstring.h \
        idris_opts.h idris_stats.h mini-gmp.h idris_stdfgn.h idris_net.h \
        idris_utf8.h getline.h
@@ -19,10 +20,10 @@
 endif
 
 ifeq ($(OS), windows)
-	OBJS += windows/idris_stdfgn.o windows/idris_net.o windows/win_utils.o
+	OBJS += windows/idris_net.o windows/win_utils.o
 else
 	CFLAGS += -fPIC
-	OBJS += idris_stdfgn.o idris_net.o
+	OBJS += idris_net.o
 endif
 
 LIBTARGET = libidris_rts.a
diff --git a/rts/idris_heap.c b/rts/idris_heap.c
--- a/rts/idris_heap.c
+++ b/rts/idris_heap.c
@@ -7,11 +7,11 @@
 
 
 /* Used for initializing the heap. */
-void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old) 
+void alloc_heap(Heap * h, size_t heap_size, size_t growth, char * old)
 {
-    char * mem = malloc(heap_size); 
+    char * mem = malloc(heap_size);
     if (mem == NULL) {
-        fprintf(stderr, 
+        fprintf(stderr,
                 "RTS ERROR: Unable to allocate heap. Requested %zd bytes.\n",
                 heap_size);
         exit(EXIT_FAILURE);
@@ -37,8 +37,8 @@
 void free_heap(Heap * h) {
     free(h->heap);
 
-    if (h->old != NULL) { 
-        free(h->old); 
+    if (h->old != NULL) {
+        free(h->old);
     }
 }
 
@@ -47,7 +47,7 @@
 /******************** Heap testing ********************************************/
 void heap_check_underflow(Heap * heap) {
     if (!(heap->heap <= heap->next)) {
-       fprintf(stderr, "RTS ERROR: HEAP UNDERFLOW <bot %p> <cur %p>\n", 
+       fprintf(stderr, "RTS ERROR: HEAP UNDERFLOW <bot %p> <cur %p>\n",
                heap->heap, heap->next);
         exit(EXIT_FAILURE);
     }
@@ -55,7 +55,7 @@
 
 void heap_check_overflow(Heap * heap) {
     if (!(heap->next <= heap->end)) {
-       fprintf(stderr, "RTS ERROR: HEAP OVERFLOW <cur %p> <end %p>\n", 
+       fprintf(stderr, "RTS ERROR: HEAP OVERFLOW <cur %p> <end %p>\n",
                heap->next, heap->end);
         exit(EXIT_FAILURE);
     }
@@ -65,13 +65,13 @@
     return (v != NULL) && !(ISINT(v));
 }
 
-int ref_in_heap(Heap * heap, VAL v) { 
+int ref_in_heap(Heap * heap, VAL v) {
     return ((VAL)heap->heap <= v) && (v < (VAL)heap->next);
 }
 
 // Checks three important properties:
 // 1. Closure.
-//      Check if all pointers in the _heap_ points only to heap. 
+//      Check if all pointers in the _heap_ points only to heap.
 // 2. Unidirectionality. (if compact gc)
 //      All references in the heap should be are unidirectional. In other words,
 //      more recently allocated closure can point only to earlier allocated one.
@@ -79,7 +79,7 @@
 //
 void heap_check_pointers(Heap * heap) {
     char* scan = NULL;
-  
+
     size_t item_size = 0;
     for(scan = heap->heap; scan < heap->next; scan += item_size) {
        item_size = *((size_t*)scan);
@@ -96,7 +96,7 @@
                  if (is_valid_ref(ptr)) {
                      // Check for closure.
                      if (!ref_in_heap(heap, ptr)) {
-                         fprintf(stderr, 
+                         fprintf(stderr,
                                  "RTS ERROR: heap closure broken. "\
                                  "<HEAP %p %p %p> <REF %p>\n",
                                  heap->heap, heap->next, heap->end, ptr);
@@ -105,7 +105,7 @@
 #if 0 // TODO macro
                      // Check for unidirectionality.
                      if (!(ptr < heap_item)) {
-                         fprintf(stderr, 
+                         fprintf(stderr,
                                  "RTS ERROR: heap unidirectionality broken:" \
                                  "<CON %p> <FIELD %p>\n",
                                  heap_item, ptr);
diff --git a/rts/idris_heap.h b/rts/idris_heap.h
--- a/rts/idris_heap.h
+++ b/rts/idris_heap.h
@@ -8,7 +8,7 @@
     char*  heap;   // Point to bottom of heap
     char*  end;    // Point to top of heap
     size_t size;   // Size of _next_ heap. Size of current heap is /end - heap/.
-    size_t growth; // Quantity of heap growth in bytes. 
+    size_t growth; // Quantity of heap growth in bytes.
 
     char* old;
 } Heap;
@@ -23,7 +23,7 @@
 // Should be used _between_ gc's.
 #define HEAP_CHECK(vm) heap_check_all(&(vm->heap));
 #else
-#define HEAP_CHECK(vm) 
+#define HEAP_CHECK(vm)
 #endif // IDRIS_DEBUG
 
 #endif // _IDRIS_HEAP_H
diff --git a/rts/idris_net.c b/rts/idris_net.c
--- a/rts/idris_net.c
+++ b/rts/idris_net.c
@@ -38,15 +38,15 @@
 }
 
 // We call this from quite a few functions. Given a textual host and an int port,
-// populates a struct addrinfo. 
-int idrnet_getaddrinfo(struct addrinfo** address_res, char* host, int port, 
+// populates a struct addrinfo.
+int idrnet_getaddrinfo(struct addrinfo** address_res, char* host, int port,
                        int family, int socket_type) {
 
     struct addrinfo hints;
     // Convert port into string
     char str_port[8];
     sprintf(str_port, "%d", port);
-    
+
     // Set up hints structure
     memset(&hints, 0, sizeof(hints)); // zero out hints
     hints.ai_family = family;
@@ -57,7 +57,7 @@
     if (strlen(host) == 0) {
         hints.ai_flags = AI_PASSIVE; // fill in IP automatically
         return getaddrinfo(NULL, str_port, &hints, address_res);
-    } 
+    }
     return getaddrinfo(host, str_port, &hints, address_res);
 
 }
@@ -75,7 +75,7 @@
         //freeaddrinfo(address_res);
         //printf("Lib err: bind\n");
         return -1;
-    } 
+    }
     return 0;
 }
 
@@ -111,7 +111,7 @@
 
 int idrnet_sockaddr_ipv4_port(void* sockaddr) {
     struct sockaddr_in* addr = (struct sockaddr_in*) sockaddr;
-    return ((int) ntohs(addr->sin_port));  
+    return ((int) ntohs(addr->sin_port));
 }
 
 void* idrnet_create_sockaddr() {
@@ -141,13 +141,13 @@
 }
 
 void* idrnet_recv(int sockfd, int len) {
-    idrnet_recv_result* res_struct = 
+    idrnet_recv_result* res_struct =
         (idrnet_recv_result*) malloc(sizeof(idrnet_recv_result));
     char* buf = malloc(len + 1);
     memset(buf, 0, len + 1);
     int recv_res = recv(sockfd, buf, len, 0);
     res_struct->result = recv_res;
-    
+
     if (recv_res > 0) { // Data was received
         buf[recv_res + 1] = 0x00; // Null-term, so Idris can interpret it
     }
@@ -172,7 +172,7 @@
 }
 
 void idrnet_free_recv_struct(void* res_struct) {
-    idrnet_recv_result* i_res_struct = 
+    idrnet_recv_result* i_res_struct =
         (idrnet_recv_result*) res_struct;
     if (i_res_struct->payload != NULL) {
         free(i_res_struct->payload);
@@ -191,9 +191,9 @@
     int addr_res = idrnet_getaddrinfo(&remote_host, host, port, family, SOCK_DGRAM);
     if (addr_res == -1) {
         return -1;
-    } 
+    }
 
-    int send_res = sendto(sockfd, data, strlen(data), 0, 
+    int send_res = sendto(sockfd, data, strlen(data), 0,
                         remote_host->ai_addr, remote_host->ai_addrlen);
     freeaddrinfo(remote_host);
     return send_res;
@@ -206,11 +206,11 @@
     if (addr_res == -1) {
         //printf("lib err: sendto getaddrinfo \n");
         return -1;
-    } 
+    }
 
     buf_htonl(buf, buf_len);
 
-    int send_res = sendto(sockfd, buf, buf_len, 0, 
+    int send_res = sendto(sockfd, buf, buf_len, 0,
                         remote_host->ai_addr, remote_host->ai_addrlen);
     if (send_res == -1) {
         perror("lib err: sendto \n");
@@ -224,13 +224,13 @@
 void* idrnet_recvfrom(int sockfd, int len) {
 /*
  * int recvfrom(int sockfd, void *buf, int len, unsigned int flags,
-             struct sockaddr *from, int *fromlen); 
+             struct sockaddr *from, int *fromlen);
 */
     // Allocate the required structures, and nuke them
-    struct sockaddr_storage* remote_addr = 
+    struct sockaddr_storage* remote_addr =
         (struct sockaddr_storage*) malloc(sizeof(struct sockaddr_storage));
     char* buf = (char*) malloc(len + 1);
-    idrnet_recvfrom_result* ret = 
+    idrnet_recvfrom_result* ret =
         (idrnet_recvfrom_result*) malloc(sizeof(idrnet_recvfrom_result));
     memset(remote_addr, 0, sizeof(struct sockaddr_storage));
     memset(buf, 0, len + 1);
@@ -240,7 +240,7 @@
     int recv_res = recvfrom(sockfd, buf, len, 0, (struct sockaddr*) remote_addr, &fromlen);
     ret->result = recv_res;
     // Check for failure...
-    if (recv_res == -1) { 
+    if (recv_res == -1) {
         free(buf);
         free(remote_addr);
     } else {
@@ -255,12 +255,11 @@
     return ret;
 }
 
-
 void* idrnet_recvfrom_buf(int sockfd, void* buf, int len) {
     // Allocate the required structures, and nuke them
-    struct sockaddr_storage* remote_addr = 
+    struct sockaddr_storage* remote_addr =
         (struct sockaddr_storage*) malloc(sizeof(struct sockaddr_storage));
-    idrnet_recvfrom_result* ret = 
+    idrnet_recvfrom_result* ret =
         (idrnet_recvfrom_result*) malloc(sizeof(idrnet_recvfrom_result));
     memset(remote_addr, 0, sizeof(struct sockaddr_storage));
     memset(ret, 0, sizeof(idrnet_recvfrom_result));
@@ -269,7 +268,7 @@
     int recv_res = recvfrom(sockfd, buf, len, 0, (struct sockaddr*) remote_addr, &fromlen);
     // Check for failure... But don't free the buffer! Not our job.
     ret->result = recv_res;
-    if (recv_res == -1) { 
+    if (recv_res == -1) {
         free(remote_addr);
     }
     // Payload will be NULL -- since it's been put into the user-specified buffer. We
@@ -298,7 +297,7 @@
 int idrnet_get_recvfrom_port(void* res_struct) {
     idrnet_recvfrom_result* recv_struct = (idrnet_recvfrom_result*) res_struct;
     if (recv_struct->remote_addr != NULL) {
-        struct sockaddr_in* remote_addr_in = 
+        struct sockaddr_in* remote_addr_in =
             (struct sockaddr_in*) recv_struct->remote_addr;
         return ((int) ntohs(remote_addr_in->sin_port));
     }
@@ -316,5 +315,3 @@
         }
     }
 }
-
-
diff --git a/rts/idris_stdfgn.c b/rts/idris_stdfgn.c
--- a/rts/idris_stdfgn.c
+++ b/rts/idris_stdfgn.c
@@ -2,12 +2,18 @@
 #include "idris_rts.h"
 #include "idris_gmp.h"
 #include "idris_gc.h"
-#include <sys/select.h>
+
 #include <fcntl.h>
 #include <errno.h>
 #include <stdio.h>
 #include <time.h>
 
+#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)
+int win_fpoll(void* h);
+#else
+#include <sys/select.h>
+#endif
+
 extern char** environ;
 
 void putStr(char* str) {
@@ -25,13 +31,13 @@
 }
 
 int fileEOF(void* h) {
-  FILE* f = (FILE*)h;
-  return feof(f);
+    FILE* f = (FILE*)h;
+    return feof(f);
 }
 
 int fileError(void* h) {
-  FILE* f = (FILE*)h;
-  return ferror(f);
+    FILE* f = (FILE*)h;
+    return ferror(f);
 }
 
 int idris_writeStr(void* h, char* str) {
@@ -45,6 +51,9 @@
 
 int fpoll(void* h)
 {
+#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)
+    return win_fpoll(h);
+#else
     FILE* f = (FILE*)h;
     fd_set x;
     struct timeval timeout;
@@ -57,6 +66,7 @@
 
     int r = select(fd+1, &x, 0, 0, &timeout);
     return r;
+#endif
 }
 
 void* do_popen(const char* cmd, const char* mode) {
@@ -107,5 +117,5 @@
 }
 
 void idris_forceGC(void* vm) {
-   idris_gc((VM*)vm); 
+    idris_gc((VM*)vm);
 }
diff --git a/rts/windows/idris_net.c b/rts/windows/idris_net.c
--- a/rts/windows/idris_net.c
+++ b/rts/windows/idris_net.c
@@ -12,7 +12,7 @@
 #include <Ws2tcpip.h>
 
 
-// inet_ntop isn't defined in the old mingw delivered with GHC, 
+// inet_ntop isn't defined in the old mingw delivered with GHC,
 // so put the prototype here, cribbed from a newer version of it
 WINSOCK_API_LINKAGE LPCSTR WSAAPI InetNtopA(INT Family, PVOID pAddr,
         LPSTR pStringBuf, size_t StringBufSize);
@@ -50,7 +50,7 @@
     // Convert port into string
     char str_port[8];
     sprintf(str_port, "%d", port);
-    
+
     if (!check_init()) {
         return -1;
     }
@@ -73,7 +73,7 @@
     int bind_res = bind(sockfd, address_res->ai_addr, address_res->ai_addrlen);
     if (bind_res == -1) {
         return -1;
-    } 
+    }
 
     return 0;
 }
@@ -152,13 +152,13 @@
     if (!check_init()) {
         return NULL;
     }
-    idrnet_recv_result* res_struct = 
+    idrnet_recv_result* res_struct =
         (idrnet_recv_result*) malloc(sizeof(idrnet_recv_result));
 
     char* buf = malloc(len + 1);
     int recv_res = recv(sockfd, buf, len, 0);
     res_struct->result = recv_res;
-    
+
     if (recv_res > 0) { // Data was received
         buf[recv_res + 1] = 0x00; // Null-term, so Idris can interpret it
     }
@@ -182,7 +182,7 @@
 }
 
 void idrnet_free_recv_struct(void* res_struct) {
-    idrnet_recv_result* i_res_struct = 
+    idrnet_recv_result* i_res_struct =
         (idrnet_recv_result*) res_struct;
     if (i_res_struct->payload != NULL) {
         free(i_res_struct->payload);
@@ -193,4 +193,3 @@
 int idrnet_errno() {
     return errno;
 }
-
diff --git a/rts/windows/idris_stdfgn.c b/rts/windows/idris_stdfgn.c
deleted file mode 100644
--- a/rts/windows/idris_stdfgn.c
+++ /dev/null
@@ -1,82 +0,0 @@
-#include "../idris_stdfgn.h"
-#include "../idris_rts.h"
-#include "../idris_gc.h"
-
-#include <fcntl.h>
-#include <stdio.h>
-#include <time.h>
-#include <io.h>
-
-extern char** environ;
-
-int win_fpoll(void* h);
-
-void putStr(char* str) {
-    printf("%s", str);
-}
-
-void* fileOpen(char* name, char* mode) {
-    FILE* f = fopen(name, mode);
-    return (void*)f;
-}
-
-void fileClose(void* h) {
-    FILE* f = (FILE*)h;
-    fclose(f);
-}
-
-int fileEOF(void* h) {
-  FILE* f = (FILE*)h;
-  return feof(f);
-}
-
-int fileError(void* h) {
-  FILE* f = (FILE*)h;
-  return ferror(f);
-}
-
-int idris_writeStr(void* h, char* str) {
-    FILE* f = (FILE*)h;
-    if (fputs(str, f)) {
-        return 0;
-    } else {
-        return -1;
-    }
-}
-
-int fpoll(void* h)
-{
-    return win_fpoll(h);
-}
-
-void* do_popen(const char* cmd, const char* mode) {
-    FILE* f = _popen(cmd, mode);
-//    int d = fileno(f);
-//    fcntl(d, F_SETFL, O_NONBLOCK);
-    return f;
-}
-
-int isNull(void* ptr) {
-    return ptr==NULL;
-}
-
-int idris_eqPtr(void* x, void* y) {
-    return x==y;
-}
-
-void* idris_stdin() {
-    return (void*)stdin;
-}
-
-char* getEnvPair(int i) {
-    return *(environ + i);
-}
-
-VAL idris_time() {
-    time_t t = time(NULL);
-    return MKBIGI(t);
-}
-
-void idris_forceGC(void* vm) {
-   idris_gc((VM*)vm);
-}
diff --git a/src/Idris/CaseSplit.hs b/src/Idris/CaseSplit.hs
--- a/src/Idris/CaseSplit.hs
+++ b/src/Idris/CaseSplit.hs
@@ -362,7 +362,7 @@
           -> Idris String
 getClause l fn un fp 
     = do i <- getIState
-         case lookupCtxt fn (idris_classes i) of
+         case lookupCtxt un (idris_classes i) of
               [c] -> return (mkClassBodies i (class_methods c))
               _ -> do ty_in <- getInternalApp fp l
                       let ty = case ty_in of
diff --git a/src/Idris/Core/Elaborate.hs b/src/Idris/Core/Elaborate.hs
--- a/src/Idris/Core/Elaborate.hs
+++ b/src/Idris/Core/Elaborate.hs
@@ -353,6 +353,9 @@
 unifyGoal :: Raw -> Elab' aux ()
 unifyGoal t = processTactic' (UnifyGoal t)
 
+unifyTerms :: Raw -> Raw -> Elab' aux ()
+unifyTerms t1 t2 = processTactic' (UnifyTerms t1 t2)
+
 exact :: Raw -> Elab' aux ()
 exact t = processTactic' (Exact t)
 
@@ -724,7 +727,12 @@
                             focus f
 
 simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
-simple_app infer fun arg str = 
+simple_app infer fun arg str =
+    try (dep_app fun arg str)
+        (infer_app infer fun arg str)
+
+infer_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
+infer_app infer fun arg str =
     do a <- getNameFrom (sMN 0 "__argTy")
        b <- getNameFrom (sMN 0 "__retTy")
        f <- getNameFrom (sMN 0 "f")
@@ -755,8 +763,49 @@
        when (a `elem` hs) $ do movelast a
        when (b `elem` hs) $ do movelast b
        end_unify
- where
-  regretWith err = try regret (lift $ tfail err)
+
+dep_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
+dep_app fun arg str = 
+    do a <- getNameFrom (sMN 0 "__argTy")
+       b <- getNameFrom (sMN 0 "__retTy")
+       fty <- getNameFrom (sMN 0 "__fnTy")
+       f <- getNameFrom (sMN 0 "f")
+       s <- getNameFrom (sMN 0 "s")
+       claim a RType
+       claim fty RType
+       claim f (Var fty)
+       tm <- get_term
+       g <- goal
+       start_unify s
+       claim s (Var a)
+       
+       prep_fill f [s]
+       focus f; attack; fun
+       end_unify
+       fty <- goal
+       solve
+       focus s; attack; 
+       ctxt <- get_context
+       env <- get_env
+       case normalise ctxt env fty of
+            -- if f gives a function type, unify our argument type with
+            -- f's expected argument type
+            Bind _ (Pi _ argty _) _ -> unifyGoal (forget argty)
+            -- Can't infer a type for 'f', so fail here (and drop back to
+            -- simply typed application where we infer the type for f)
+            _ -> fail "Can't make type"
+       end_unify
+       arg
+       solve
+       complete_fill
+
+       -- We don't need a and b in the hole queue any more since they were
+       -- just for checking f, so move them to the end. If they never end up
+       -- getting solved, we'll get an 'Incomplete term' error.
+       hs <- get_holes
+       when (a `elem` hs) $ do movelast a
+       when (b `elem` hs) $ do movelast b
+       end_unify
 
 -- Abstract over an argument of unknown type, giving a name for the hole
 -- which we'll fill with the argument type too.
diff --git a/src/Idris/Core/ProofState.hs b/src/Idris/Core/ProofState.hs
--- a/src/Idris/Core/ProofState.hs
+++ b/src/Idris/Core/ProofState.hs
@@ -91,6 +91,7 @@
             | MatchProblems Bool
             | UnifyProblems
             | UnifyGoal Raw
+            | UnifyTerms Raw Raw
             | ProofState
             | Undo
             | QED
@@ -477,6 +478,13 @@
        return h
 unifyGoal _ _ _ _ = fail "The focus is not a binder."
 
+unifyTerms :: Raw -> Raw -> RunTactic
+unifyTerms tm1 tm2 ctxt env h =
+    do (tm1v, _) <- lift $ check ctxt env tm1
+       (tm2v, _) <- lift $ check ctxt env tm2
+       ns' <- unify' ctxt env (tm1v, Nothing) (tm2v, Nothing)
+       return h
+
 exact :: Raw -> RunTactic
 exact guess ctxt env (Bind x (Hole ty) sc) =
     do (val, valty) <- lift $ check ctxt env guess
@@ -1113,3 +1121,5 @@
          mktac (SetInjective n)  = setinj n
          mktac (MoveLast n)      = movelast n
          mktac (UnifyGoal r)     = unifyGoal r
+         mktac (UnifyTerms x y)  = unifyTerms x y
+
diff --git a/src/Idris/DSL.hs b/src/Idris/DSL.hs
--- a/src/Idris/DSL.hs
+++ b/src/Idris/DSL.hs
@@ -108,7 +108,10 @@
     block b (DoExp fc tm : rest)
         = PApp fc b
             [pexp tm,
-             pexp (PLam fc (sMN 0 "bindx") NoFC Placeholder (block b rest))]
+             pexp (PLam fc (sMN 0 "bindx") NoFC (mkTy tm) (block b rest))]
+        where mkTy (PCase _ _ _) = PRef fc [] unitTy
+              mkTy (PMetavar _ _) = PRef fc [] unitTy
+              mkTy _ = Placeholder
     block b _ = PElabError (Msg "Invalid statement in do block")
 
 expandSugar dsl (PIdiom fc e) = expandSugar dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e
diff --git a/src/Idris/Elab/Clause.hs b/src/Idris/Elab/Clause.hs
--- a/src/Idris/Elab/Clause.hs
+++ b/src/Idris/Elab/Clause.hs
@@ -669,8 +669,6 @@
                                 (erun fc (build i winfo ERHS opts fname rhs))
                         errAt "right hand side of " fname (Just clhsty)
                               (erun fc $ psolve lhs_tm)
-                        hs <- get_holes
-                        mapM_ (elabCaseHole is) hs
                         tt <- get_term
                         aux <- getAux
                         let (tm, ds) = runState (collectDeferred (Just fname) 
@@ -787,27 +785,6 @@
       sepBlocks' ns (b : bs) = let (bf, af) = sepBlocks' ns bs in
                                    (b : bf, af)
       sepBlocks' ns [] = ([], [])
-
-
-    -- if a hole is just an argument/result of a case block, treat it as
-    -- the unit type. Hack to help elaborate case in do blocks.
-    elabCaseHole aux h = do
-        focus h
-        g <- goal
-        case g of
-             TType _ -> when (any (isArg h) aux) $ do apply (Var unitTy) []; solve
-             _ -> return ()
-
-    -- Is the name a pattern argument in the declaration
-    isArg :: Name -> PDecl -> Bool
-    isArg n (PClauses _ _ _ cs) = any isArg' cs
-      where
-        isArg' (PClause _ _ (PApp _ _ args) _ _ _)
-           = any (\x -> case x of
-                          PRef _ _ n' -> n == n'
-                          _ -> False) (map getTm args)
-        isArg' _ = False
-    isArg _ _ = False
 
     -- term is not within "with" block
     isOutsideWith :: PTerm -> Bool
diff --git a/src/Idris/Elab/Term.hs b/src/Idris/Elab/Term.hs
--- a/src/Idris/Elab/Term.hs
+++ b/src/Idris/Elab/Term.hs
@@ -1028,12 +1028,22 @@
                    solve
     elab' ina _ c@(PCase fc scr opts)
         = do attack
+             
              tyn <- getNameFrom (sMN 0 "scty")
              claim tyn RType
              valn <- getNameFrom (sMN 0 "scval")
              scvn <- getNameFrom (sMN 0 "scvar")
              claim valn (Var tyn)
              letbind scvn (Var tyn) (Var valn)
+             
+             -- Start filling in the scrutinee type, if we can work one
+             -- out from the case options
+             let scrTy = getScrType (map fst opts)
+             case scrTy of
+                  Nothing -> return ()
+                  Just ty -> do focus tyn
+                                elabE ina (Just fc) ty
+
              focus valn
              elabE (ina { e_inarg = True }) (Just fc) scr
              -- Solve any remaining implicits - we need to solve as many
@@ -1084,6 +1094,21 @@
                         Just xs@(_:_) -> sNS n xs
                         _ -> n
 
+              getScrType [] = Nothing
+              getScrType (f : os) = maybe (getScrType os) Just (getAppType f)
+
+              getAppType (PRef _ _ n) = 
+                 case lookupTyName n (tt_ctxt ist) of
+                      [(n', ty)] | isDConName n' (tt_ctxt ist) -> 
+                         case unApply (getRetTy ty) of
+                           (P _ tyn _, args) ->
+                               Just (PApp fc (PRef fc [] tyn)
+                                    (map pexp (map (const Placeholder) args)))
+                           _ -> Nothing
+                      _ -> Nothing -- ambiguity is no help to us!
+              getAppType (PApp _ t as) = getAppType t
+              getAppType _ = Nothing
+
               inApp (P _ n _) = [n]
               inApp (App _ f a) = inApp f ++ inApp a
               inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc
@@ -1696,38 +1721,25 @@
 
 collectDeferred :: Maybe Name -> [Name] -> Context ->
                    Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term
-collectDeferred top casenames ctxt (Bind n (GHole i psns t) app) =
-    do ds <- get
-       t' <- collectDeferred top casenames ctxt t
-       when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, tidyArg [] t', psns))])
-       collectDeferred top casenames ctxt app
-  where
-    -- Evaluate the top level functions in arguments, if possible, and if it's
-    -- not a name we're immediately going to define in a case block, so that
-    -- any immediate specialisation of the function applied to constructors 
-    -- can be done
-    tidyArg env (Bind n b@(Pi im t k) sc) 
-        = Bind n (Pi im (tidy ctxt env t) k)
-                 (tidyArg ((n, b) : env) sc)
-    tidyArg env t = tidy ctxt env t
-
-    tidy ctxt env t = normalise ctxt env t
-
-    getFn (Bind n (Lam _) t) = getFn t
-    getFn t | (f, a) <- unApply t = f
-
-collectDeferred top ns ctxt (Bind n b t) 
-     = do b' <- cdb b
-          t' <- collectDeferred top ns ctxt t
-          return (Bind n b' t')
+collectDeferred top casenames ctxt tm = cd [] tm
   where
-    cdb (Let t v)   = liftM2 Let (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)
-    cdb (Guess t v) = liftM2 Guess (collectDeferred top ns ctxt t) (collectDeferred top ns ctxt v)
-    cdb b           = do ty' <- collectDeferred top ns ctxt (binderTy b)
-                         return (b { binderTy = ty' })
-collectDeferred top ns ctxt (App s f a) = liftM2 (App s) (collectDeferred top ns ctxt f) 
-                                                         (collectDeferred top ns ctxt a)
-collectDeferred top ns ctxt t = return t
+    cd env (Bind n (GHole i psns t) app) =
+        do ds <- get
+           t' <- collectDeferred top casenames ctxt t
+           when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t', psns))])
+           cd env app
+    cd env (Bind n b t) 
+         = do b' <- cdb b
+              t' <- cd ((n, b) : env) t
+              return (Bind n b' t')
+      where
+        cdb (Let t v)   = liftM2 Let (cd env t) (cd env v)
+        cdb (Guess t v) = liftM2 Guess (cd env t) (cd env v)
+        cdb b           = do ty' <- cd env (binderTy b)
+                             return (b { binderTy = ty' })
+    cd env (App s f a) = liftM2 (App s) (cd env f) 
+                                        (cd env a)
+    cd env t = return t
 
 case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()
 case_ ind autoSolve ist fn tm = do
diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs
--- a/src/Idris/REPL.hs
+++ b/src/Idris/REPL.hs
@@ -943,7 +943,8 @@
   where
     showMetavarInfo ppo ist n i
          = case lookupTy n (tt_ctxt ist) of
-                (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))
+                (ty:_) -> let ty' = normaliseC (tt_ctxt ist) [] ty in
+                              putTy ppo ist i [] (delab ist (errReverse ist ty'))
     putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
     putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc
     putTy ppo ist i bnd (PPi _ n _ t sc)
diff --git a/test/basic002/test006.idr b/test/basic002/test006.idr
--- a/test/basic002/test006.idr
+++ b/test/basic002/test006.idr
@@ -23,7 +23,7 @@
 ---------- Proofs ----------
 
 Main.parity_lemma_2 = proof {
-    intro;
+    intro j;
     intro;
     rewrite sym (plusSuccRightSucc j j);
     trivial;
diff --git a/test/interactive011/expected b/test/interactive011/expected
new file mode 100644
--- /dev/null
+++ b/test/interactive011/expected
@@ -0,0 +1,3 @@
+    show x = ?Show_rhs_1
+    showPrec d x = ?Show_rhs_2
+append [] _ = ?append_rhs_1
diff --git a/test/interactive011/input b/test/interactive011/input
new file mode 100644
--- /dev/null
+++ b/test/interactive011/input
@@ -0,0 +1,2 @@
+:ac 5 Show
+:ac 7 append
diff --git a/test/interactive011/interactive011.idr b/test/interactive011/interactive011.idr
new file mode 100644
--- /dev/null
+++ b/test/interactive011/interactive011.idr
@@ -0,0 +1,11 @@
+import Data.Vect
+
+data Foo = Bar | Baz
+
+instance Show Foo where
+
+append : Vect n a -> Vect m a -> Vect (n + m) a
+append (x :: xs) ys = ?append_rhs_2
+
+
+
diff --git a/test/interactive011/run b/test/interactive011/run
new file mode 100644
--- /dev/null
+++ b/test/interactive011/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+idris --quiet interactive011.idr < input
+rm -f *.ibc
diff --git a/test/interactive012/expected b/test/interactive012/expected
new file mode 100644
--- /dev/null
+++ b/test/interactive012/expected
@@ -0,0 +1,33 @@
+  x : Int
+--------------------------------------
+mkString_rhs_1 : String
+  x : String
+--------------------------------------
+mkString_rhs_2 : String
+--------------------------------------
+mkThing_rhs_1 : Int
+--------------------------------------
+mkThing_rhs_2 : String
+  str : Bool
+  x : IntString str
+--------------------------------------
+mkString2_rhs : String
+  x : ?what
+--------------------------------------
+mkString3_rhs_1 : String
+  x : ?what
+--------------------------------------
+mkString3_rhs_2 : String
+  a : Type
+  m : Nat
+  ys : Vect m a
+--------------------------------------
+append_rhs_1 : Vect m a
+  a : Type
+  x : a
+  k : Nat
+  xs : Vect k a
+  m : Nat
+  ys : Vect m a
+--------------------------------------
+append_rhs_2 : Vect (S (plus k m)) a
diff --git a/test/interactive012/input b/test/interactive012/input
new file mode 100644
--- /dev/null
+++ b/test/interactive012/input
@@ -0,0 +1,9 @@
+:t mkString_rhs_1
+:t mkString_rhs_2
+:t mkThing_rhs_1
+:t mkThing_rhs_2
+:t mkString2_rhs
+:t mkString3_rhs_1
+:t mkString3_rhs_2
+:t append_rhs_1
+:t append_rhs_2
diff --git a/test/interactive012/interactive012.idr b/test/interactive012/interactive012.idr
new file mode 100644
--- /dev/null
+++ b/test/interactive012/interactive012.idr
@@ -0,0 +1,26 @@
+IntString : Bool -> Type
+IntString False = Int
+IntString True = String
+
+mkString : (str : Bool) -> IntString str -> String
+mkString False x = ?mkString_rhs_1
+mkString True x = ?mkString_rhs_2
+
+mkThing : (str : Bool) -> IntString str
+mkThing False = ?mkThing_rhs_1
+mkThing True = ?mkThing_rhs_2
+
+mkString2 : (str : Bool) -> IntString str -> String
+mkString2 str x = ?mkString2_rhs
+
+mkString3 : (str : Bool) -> ?what -> String
+mkString3 False x = ?mkString3_rhs_1
+mkString3 True x = ?mkString3_rhs_2
+
+data Vect : Nat -> Type -> Type where
+     Nil : Vect Z a
+     (::) : a -> Vect k a -> Vect (S k) a
+
+append : Vect n a -> Vect m a -> Vect (n + m) a
+append [] ys = ?append_rhs_1
+append (x :: xs) ys = ?append_rhs_2
diff --git a/test/interactive012/run b/test/interactive012/run
new file mode 100644
--- /dev/null
+++ b/test/interactive012/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+idris --quiet interactive012.idr < input
+rm -f *.ibc
diff --git a/test/reg001/reg001.idr b/test/reg001/reg001.idr
--- a/test/reg001/reg001.idr
+++ b/test/reg001/reg001.idr
@@ -182,3 +182,29 @@
   
 vecfoo : HVect [String, List Nat, Nat, (Nat, Nat)]
 vecfoo = put (S (S Z)) hVectEx1
+
+foom : Monad m => Int -> m Int
+foom = pure 
+  
+bar : IO ()
+bar = case foom 5 of
+           Nothing => print 42
+           Just n => print n
+
+Max : (Nat -> Type) -> Type
+Max p = (Nat , (k : Nat) -> p k -> Nat)
+    
+maxEquiv : Max p -> (n1 : Nat) -> p n1 -> Nat
+maxEquiv a n1 pr1 = snd a n1 pr1
+
+data Rho = R
+
+rho : Rho -> Rho
+rho r = case r of R => r
+
+data Kappa : (r : Rho) -> Type where K : Kappa r
+
+kappa : Kappa (rho r) -> Kappa (rho r)
+kappa {r} k = k' where -- k' : Kappa (rho r)
+                       k' = k
+
diff --git a/test/tutorial006/run b/test/tutorial006/run
--- a/test/tutorial006/run
+++ b/test/tutorial006/run
@@ -1,4 +1,5 @@
 #!/usr/bin/env bash
 idris --nocolour --consolewidth 80 $@ tutorial006a.idr --check
 idris --nocolour --consolewidth 80 $@ tutorial006b.idr --check
+idris --nocolour --consolewidth 80 $@ tutorial006c.idr -p effects --check
 rm -f *.ibc
diff --git a/test/tutorial006/tutorial006c.idr b/test/tutorial006/tutorial006c.idr
new file mode 100644
--- /dev/null
+++ b/test/tutorial006/tutorial006c.idr
@@ -0,0 +1,20 @@
+import Effects
+import Effect.Exception
+import Effect.StdIO
+import Data.Vect
+
+read_vec : Eff (p ** Vect p Int) [STDIO]
+read_vec = do putStr "Number (-1 when done): "
+              case run (parseNumber (trim !getStr)) of
+                   Nothing => do putStrLn "Input error"
+                                 read_vec
+                   Just v => if (v /= -1)
+                                then do (_ ** xs) <- read_vec
+                                        pure (_ ** v :: xs)
+                                else pure (_ ** [])
+  where
+    parseNumber : String -> Eff Int [EXCEPTION String]
+    parseNumber str
+      = if all (\x => isDigit x || x == '-') (unpack str)
+           then pure (cast str)
+           else raise "Not a number"