diff --git a/idris.cabal b/idris.cabal
--- a/idris.cabal
+++ b/idris.cabal
@@ -1,5 +1,5 @@
 Name:           idris
-Version:        0.9.11.1
+Version:        0.9.11.2
 License:        BSD3
 License-file:   LICENSE
 Author:         Edwin Brady
@@ -55,6 +55,7 @@
                        rts/idris_gmp.h
                        rts/idris_main.c
                        rts/idris_rts.h
+                       rts/idris_net.h
                        rts/idris_stdfgn.h
                        rts/libtest.c
 
diff --git a/libs/base/Network/Socket.idr b/libs/base/Network/Socket.idr
new file mode 100644
--- /dev/null
+++ b/libs/base/Network/Socket.idr
@@ -0,0 +1,246 @@
+-- Time to do this properly.
+-- Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
+-- (C) SimonJF, MIT Licensed, 2014
+module Network.Socket
+
+%include C "idris_net.h"
+%include C "sys/types.h" -- Pushing my luck, might need to re-export everything
+%include C "sys/socket.h" 
+%include C "netdb.h"
+
+%access public
+
+ByteLength : Type
+ByteLength = Int
+
+class ToCode a where
+  toCode : a -> Int
+
+-- Socket Families.
+-- The ones that people might actually use. We're not going to need US Government
+-- proprietary ones...
+data SocketFamily = AF_UNSPEC -- Unspecified
+                  | AF_INET   -- IP / UDP etc. IPv4
+                  | AF_INET6  -- IP / UDP etc. IPv6
+
+instance Show SocketFamily where
+  show AF_UNSPEC = "AF_UNSPEC"
+  show AF_INET   = "AF_INET"
+  show AF_INET6  = "AF_INET4"
+
+instance ToCode SocketFamily where
+  toCode AF_UNSPEC = 0
+  toCode AF_INET   = 2
+  toCode AF_INET6  = 10
+
+getSocketFamily : Int -> Maybe SocketFamily
+getSocketFamily i = Prelude.List.lookup i [(0, AF_UNSPEC), (2, AF_INET), (10, AF_INET6)]
+
+-- Socket Types.
+data SocketType = NotASocket  -- Not a socket, used in certain operations
+                | Stream      -- TCP
+                | Datagram    -- UDP
+                | RawSocket   -- Raw sockets. A guy can dream.
+
+instance Show SocketType where
+  show NotASocket = "Not a socket"
+  show Stream     = "Stream"
+  show Datagram   = "Datagram"
+  show Raw        = "Raw"
+
+instance ToCode SocketType where
+  toCode NotASocket = 0
+  toCode Stream     = 1
+  toCode Datagram   = 2
+  toCode Raw        = 3
+
+-- Protocol Number. Generally good enough to just set it to 0.
+ProtocolNumber : Type
+ProtocolNumber = Int
+
+-- SocketError: Error thrown by a socket operation
+SocketError : Type
+SocketError = Int
+
+-- SocketDescriptor: Native C Socket Descriptor
+SocketDescriptor : Type
+SocketDescriptor = Int
+
+data SocketAddress = IPv4Addr Int Int Int Int
+                   | IPv6Addr -- Not implemented (yet)
+                   | Hostname String
+                   | InvalidAddress -- Used when there's a parse error
+
+instance Show SocketAddress where
+  show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])
+  show IPv6Addr = "NOT IMPLEMENTED YET"
+  show (Hostname host) = host
+  show InvalidAddress = "Invalid"
+
+Port : Type
+Port = Int
+
+-- Backlog used within listen() call -- number of incoming calls
+BACKLOG : Int
+BACKLOG = 20
+
+-- FIXME: This *must* be pulled in from C
+EAGAIN : Int 
+EAGAIN = 11
+
+-- Allocates an amount of memory given by the ByteLength parameter.
+-- Used to allocate a mutable pointer to be given to the Recv functions.
+private
+alloc : ByteLength -> IO Ptr
+alloc bl = mkForeign (FFun "idrnet_malloc" [FInt] FPtr) bl
+
+-- Frees a given pointer
+private
+free : Ptr -> IO ()
+free ptr = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
+
+record Socket : Type where
+  MkSocket : (descriptor : SocketDescriptor) ->
+             (family : SocketFamily) ->
+             (socketType : SocketType) ->
+             (protocolNumber : ProtocolNumber) ->
+             Socket
+
+getErrno : IO Int
+getErrno = mkForeign (FFun "idrnet_errno" [] FInt)
+
+-- Creates a UNIX socket with the given family, socket type and protocol number.
+-- Returns either a socket or an error.
+socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)
+socket sf st pn = do
+  socket_res <- mkForeign (FFun "socket" [FInt, FInt, FInt] FInt) (toCode sf) (toCode st) pn
+  if socket_res == -1 then -- error
+    map Left getErrno
+  else 
+    return $ Right (MkSocket socket_res sf st pn)
+
+
+close : Socket -> IO ()
+close sock = mkForeign (FFun "close" [FInt] FUnit) (descriptor sock)
+
+-- Binds a socket to the given socket address and port.
+-- Returns 0 on success, an error code otherwise.
+bind : Socket -> SocketAddress -> Port -> IO Int
+bind sock addr port = do
+  bind_res <- (mkForeign (FFun "idrnet_bind" [FInt, FInt, FInt, FString, FInt] FInt) 
+                           (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port)
+  if bind_res == (-1) then -- error
+    getErrno
+  else return 0 -- Success
+
+-- Connects to a given address and port.
+-- Returns 0 on success, and an error number on error.
+connect : Socket -> SocketAddress -> Port -> IO Int
+connect sock addr port = do
+  conn_res <- (mkForeign (FFun "idrnet_connect" [FInt, FInt, FInt, FString, FInt] FInt)
+                           (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (show addr) port)
+  if conn_res == (-1) then
+    getErrno
+  else return 0
+
+-- Listens on a bound socket.
+listen : Socket -> IO Int
+listen sock = do
+  listen_res <- mkForeign (FFun "listen" [FInt, FInt] FInt) (descriptor sock) BACKLOG
+  if listen_res == (-1) then
+    getErrno
+  else return 0
+
+-- Parses a textual representation of an IPv4 address into a SocketAddress
+private
+parseIPv4 : String -> SocketAddress
+parseIPv4 str = case splitted of
+                     (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
+                     _ => InvalidAddress
+  where toInt' : String -> Integer
+        toInt' = cast
+        toInt : String -> Int
+        toInt s = fromInteger $ toInt' s
+        splitted : List Int
+        splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
+
+
+-- Retrieves a socket address from a sockaddr pointer
+private
+getSockAddr : Ptr -> IO SocketAddress
+getSockAddr ptr = do
+  addr_family_int <- mkForeign (FFun "idrnet_sockaddr_family" [FPtr] FInt) ptr
+  -- FIXME: Is this really a safe assertion? Depends where the Ptr came
+  -- from!
+  assert_total $ case getSocketFamily addr_family_int of
+    Just AF_INET => do
+      ipv4_addr <- mkForeign (FFun "idrnet_sockaddr_ipv4" [FPtr] FString) ptr
+      return $ parseIPv4 ipv4_addr
+    Just AF_INET6 => return IPv6Addr
+    Just AF_UNSPEC => return IPv6Addr -- FIXME: Horrible hack
+
+-- Accepts a connection from a listening socket.
+accept : Socket -> IO (Either SocketError (Socket, SocketAddress))
+accept sock = do
+  -- We need a pointer to a sockaddr structure. This is then passed into
+  -- idrnet_accept and populated. We can then query it for the SocketAddr and free it.
+  sockaddr_ptr <- mkForeign (FFun "idrnet_create_sockaddr" [] FPtr) 
+  accept_res <- mkForeign (FFun "idrnet_accept" [FInt, FPtr] FInt) (descriptor sock) sockaddr_ptr
+  if accept_res == (-1) then
+    map Left getErrno
+  else do
+    let (MkSocket _ fam ty p_num) = sock
+    sockaddr <- getSockAddr sockaddr_ptr
+    free sockaddr_ptr
+    return $ Right ((MkSocket accept_res fam ty p_num), sockaddr)
+
+send : Socket -> String -> IO (Either SocketError ByteLength)
+send sock dat = do
+  send_res <- mkForeign (FFun "idrnet_send" [FInt, FString] FInt) (descriptor sock) dat
+  if send_res == (-1) then
+    map Left getErrno
+  else
+    return $ Right send_res
+
+private
+freeRecvStruct : Ptr -> IO ()
+freeRecvStruct p = mkForeign (FFun "idrnet_free_recv_struct" [FPtr] FUnit) p
+
+
+recv : Socket -> Int -> IO (Either SocketError (String, ByteLength))
+recv sock len = do
+  -- Firstly make the request, get some kind of recv structure which
+  -- contains the result of the recv and possibly the retrieved payload
+  recv_struct_ptr <- mkForeign (FFun "idrnet_recv" [FInt, FInt] FPtr) (descriptor sock) len
+  recv_res <- mkForeign (FFun "idrnet_get_recv_res" [FPtr] FInt) recv_struct_ptr
+  if recv_res == (-1) then do
+    errno <- getErrno
+    freeRecvStruct recv_struct_ptr
+    return $ Left errno
+  else 
+    if recv_res == 0 then do
+       freeRecvStruct recv_struct_ptr
+       return $ Left 0
+    else do
+       payload <- mkForeign (FFun "idrnet_get_recv_payload" [FPtr] FString) recv_struct_ptr
+       freeRecvStruct recv_struct_ptr
+       return $ Right (payload, recv_res)
+
+
+-- Sends the data in a given memory location
+sendBuf : Socket -> Ptr -> ByteLength -> IO (Either SocketError ByteLength)
+sendBuf sock ptr len = do
+  send_res <- mkForeign (FFun "idrnet_send_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
+  if send_res == (-1) then
+    map Left getErrno
+  else 
+    return $ Right send_res
+
+recvBuf : Socket -> Ptr -> ByteLength -> IO (Either SocketError ByteLength)
+recvBuf sock ptr len = do
+  recv_res <- mkForeign (FFun "idrnet_recv_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
+  if (recv_res == (-1)) then
+    map Left getErrno
+  else
+    return $ Right recv_res
+
diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg
--- a/libs/base/base.ipkg
+++ b/libs/base/base.ipkg
@@ -3,7 +3,7 @@
 opts = "--nobasepkgs --total -i ../prelude"
 modules = System,
 
-          Network.Cgi,
+          Network.Cgi, Network.Socket,
           Debug.Trace,
 
           System.Concurrency.Raw, System.Concurrency.Process,
diff --git a/libs/neweffects/Effects.idr b/libs/neweffects/Effects.idr
--- a/libs/neweffects/Effects.idr
+++ b/libs/neweffects/Effects.idr
@@ -22,10 +22,10 @@
 -- A bit of syntactic sugar ('syntax' is not very flexible so we only go
 -- up to a small number of parameters...)
 
+syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
 syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff] 
        = eff inst (\b => outst)
 syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
-syntax "{" [inst] "}" [eff] = eff inst (\result => inst)
 
 ---- Properties and proof construction
 
@@ -252,13 +252,14 @@
 
 -- yuck :) Haven't got type class instances working nicely in tactic
 -- proofs yet, so just brute force it.
-syntax MkDefaultEnv = (| [], [default], [default, default],
-                         [default, default, default],
-                         [default, default, default, default],
-                         [default, default, default, default, default],
-                         [default, default, default, default, default, default],
-                         [default, default, default, default, default, default, default],
-                         [default, default, default, default, default, default, default, default] |)
+syntax MkDefaultEnv = with Env
+                       (| [], [default], [default, default],
+                          [default, default, default],
+                          [default, default, default, default],
+                          [default, default, default, default, default],
+                          [default, default, default, default, default, default],
+                          [default, default, default, default, default, default, default],
+                          [default, default, default, default, default, default, default, default] |)
 
 run : Applicative m => {default MkDefaultEnv env : Env m xs} -> Eff m a xs xs' -> m a
 run {env} prog = eff env prog (\r, env => pure r)
diff --git a/libs/prelude/Prelude/Strings.idr b/libs/prelude/Prelude/Strings.idr
--- a/libs/prelude/Prelude/Strings.idr
+++ b/libs/prelude/Prelude/Strings.idr
@@ -145,3 +145,16 @@
 
 length : String -> Nat
 length = fromInteger . prim__zextInt_BigInt . prim_lenString
+
+toLower : String -> String
+toLower x with (strM x)
+  strToLower ""             | StrNil = ""
+  strToLower (strCons c cs) | (StrCons c cs) =
+    strCons (toLower c) (toLower (assert_smaller (strCons c cs) cs))
+
+toUpper : String -> String
+toUpper x with (strM x)
+  strToLower ""             | StrNil = ""
+  strToLower (strCons c cs) | (StrCons c cs) =
+    strCons (toUpper c) (toUpper (assert_smaller (strCons c cs) cs ))
+
diff --git a/rts/Makefile b/rts/Makefile
--- a/rts/Makefile
+++ b/rts/Makefile
@@ -1,9 +1,9 @@
 include ../config.mk
 
 OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_stdfgn.o \
-       idris_bitstring.o idris_opts.o idris_stats.o mini-gmp.o
+       idris_bitstring.o idris_net.o idris_opts.o idris_stats.o mini-gmp.o
 HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_stdfgn.h \
-       idris_bitstring.h idris_opts.h idris_stats.h mini-gmp.h
+       idris_bitstring.h idris_net.h idris_opts.h idris_stats.h mini-gmp.h
 CFLAGS:=-fPIC $(CFLAGS)
 CFLAGS += $(GMP_INCLUDE_DIR) $(GMP)
 
diff --git a/rts/idris_net.c b/rts/idris_net.c
new file mode 100644
--- /dev/null
+++ b/rts/idris_net.c
@@ -0,0 +1,143 @@
+// C-Side of the Idris network library
+// (C) Simon Fowler, 2014
+// MIT Licensed. Have fun!
+#include "idris_net.h"
+#include <arpa/inet.h>
+
+void* idrnet_malloc(int size) {
+    return malloc(size);
+}
+
+void idrnet_free(void* ptr) {
+    free(ptr);
+}
+
+int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port) {
+    struct addrinfo hints;
+    struct addrinfo* address_res;
+    // 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;
+    hints.ai_socktype = socket_type;
+
+    // If the length of the hostname is 0 (i.e, it was set to Nothing in Idris)
+    // then we want to instruct the C library to fill in the IP automatically
+    if (strlen(host) == 0) {
+        hints.ai_flags = AI_PASSIVE; // fill in IP automatically
+    }
+
+    int addr_res = getaddrinfo(host, str_port, &hints, &address_res);
+    if (addr_res == -1) {
+        return -1;
+    }
+
+    int bind_res = bind(sockfd, address_res->ai_addr, address_res->ai_addrlen);
+    if (bind_res == -1) {
+        return -1;
+    } 
+
+    return 0;
+}
+
+int idrnet_connect(int sockfd, int family, int socket_type, char* host, int port) {
+    char str_port[8];
+    sprintf(str_port, "%d", port);
+    struct addrinfo hints;
+    struct addrinfo* remote_host;
+
+    // Set up hints structure for getaddrinfo
+    memset(&hints, 0, sizeof(hints));
+    hints.ai_family = family;
+    hints.ai_socktype = socket_type;
+
+    // Get info about the remote host (DNS lookup etc)
+    int addr_res = getaddrinfo(host, str_port, &hints, &remote_host);
+    if (addr_res == -1) {
+        return -1;
+    }
+
+    int connect_res = connect(sockfd, remote_host->ai_addr, remote_host->ai_addrlen);
+    if (connect_res == -1) {
+        return -1;
+    }
+
+    return 0;
+}
+
+
+int idrnet_sockaddr_family(void* sockaddr) {
+    struct sockaddr* addr = (struct sockaddr*) sockaddr;
+    return (int) addr->sa_family;
+}
+
+char* idrnet_sockaddr_ipv4(void* sockaddr) {
+    struct sockaddr_in* addr = (struct sockaddr_in*) addr;
+    char* ip_addr = (char*) malloc(sizeof(char) * INET_ADDRSTRLEN);
+    inet_ntop(AF_INET, &(addr->sin_addr), ip_addr, INET_ADDRSTRLEN);
+    return ip_addr;
+}
+
+void* idrnet_create_sockaddr() {
+    return malloc(sizeof(struct sockaddr_storage));
+}
+
+
+int idrnet_accept(int sockfd, void* sockaddr) {
+    struct sockaddr* addr = (struct sockaddr*) sockaddr;
+    socklen_t addr_size = 0;
+    return accept(sockfd, addr, &addr_size);
+}
+
+int idrnet_send(int sockfd, char* data) {
+    int len = strlen(data); // For now.
+    return send(sockfd, (void*) data, len, 0);
+}
+
+int idrnet_send_buf(int sockfd, void* data, int len) {
+    return send(sockfd, data, len, 0);
+}
+
+void* idrnet_recv(int sockfd, int len) {
+    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
+    }
+    res_struct->payload = (void*) buf;
+    return (void*) res_struct;
+}
+
+int idrnet_recv_buf(int sockfd, void* buf, int len) {
+    return recv(sockfd, buf, len, 0);
+}
+
+int idrnet_get_recv_res(void* res_struct) {
+    return (((idrnet_recv_result*) res_struct)->result);
+}
+
+void* idrnet_get_recv_payload(void* res_struct) {
+    return (((idrnet_recv_result*) res_struct)->payload);
+}
+
+void idrnet_free_recv_struct(void* res_struct) {
+    idrnet_recv_result* i_res_struct = 
+        (idrnet_recv_result*) res_struct;
+    if (i_res_struct->payload != NULL) {
+        free(i_res_struct->payload);
+    }
+    free(res_struct);
+}
+
+int idrnet_errno() {
+    return errno;
+}
+
diff --git a/rts/idris_net.h b/rts/idris_net.h
new file mode 100644
--- /dev/null
+++ b/rts/idris_net.h
@@ -0,0 +1,53 @@
+#ifndef IDRISNET_H
+#define IDRISNET_H
+
+#include <errno.h>
+#include <netdb.h>
+#include <stdbool.h>
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#include <sys/types.h>
+#include <sys/socket.h>
+
+typedef struct idrnet_recv_result {
+    int result;
+    void* payload;
+} idrnet_recv_result;
+
+// Memory management functions
+void* idrnet_malloc(int size);
+void idrnet_free(void* ptr);
+
+// Gets value of errno
+int idrnet_errno(); 
+
+// Bind
+int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port);
+
+// Connect
+int idrnet_connect(int sockfd, int family, int socket_type, char* host, int port);
+
+// Accessor functions for struct_sockaddr
+int idrnet_sockaddr_family(void* sockaddr);
+char* idrnet_sockaddr_ipv4(void* sockaddr);
+void* idrnet_create_sockaddr();
+
+// Accept
+int idrnet_accept(int sockfd, void* sockaddr);
+
+// Send
+int idrnet_send(int sockfd, char* data);
+int idrnet_send_buf(int sockfd, void* data, int len);
+
+// Receive
+// Creates a result structure containing result and payload
+void* idrnet_recv(int sockfd, int len);
+// Receives directly into a buffer
+int idrnet_recv_buf(int sockfd, void* buf, int len);
+
+// Receive structure accessors
+int idrnet_get_recv_res(void* res_struct);
+void* idrnet_get_recv_payload(void* res_struct);
+void idrnet_free_recv_struct(void* res_struct);
+#endif
diff --git a/src/IRTS/CodegenJavaScript.hs b/src/IRTS/CodegenJavaScript.hs
--- a/src/IRTS/CodegenJavaScript.hs
+++ b/src/IRTS/CodegenJavaScript.hs
@@ -20,9 +20,10 @@
 import System.Directory
 
 idrNamespace :: String
-idrNamespace   = "__IDR__"
-idrRTNamespace = "__IDRRT__"
-idrLTNamespace = "__IDRLT__"
+idrNamespace    = "__IDR__"
+idrRTNamespace  = "__IDRRT__"
+idrLTNamespace  = "__IDRLT__"
+idrCTRNamespace = "__IDRCTR__"
 
 
 data JSTarget = Node | JavaScript deriving Eq
@@ -408,16 +409,33 @@
 
 isJSConstant :: JS -> Bool
 isJSConstant js
-  | JSString _ <- js = True
-  | JSChar _   <- js = True
-  | JSNum _    <- js = True
-  | JSType _   <- js = True
-  | JSNull     <- js = True
+  | JSString _   <- js = True
+  | JSChar _     <- js = True
+  | JSNum _      <- js = True
+  | JSType _     <- js = True
+  | JSNull       <- js = True
+  | JSArray vals <- js = all isJSConstant vals
 
   | JSApp (JSIdent "__IDRRT__bigInt") _ <- js = True
+
   | otherwise = False
 
+isJSConstantConstructor :: [String] -> JS -> Bool
+isJSConstantConstructor constants js
+  | isJSConstant js =
+      True
+  | JSArray vals <- js =
+      all (isJSConstantConstructor constants) vals
+  | JSNew "__IDRRT__Con" args <- js =
+      all (isJSConstantConstructor constants) args
+  | JSIndex (JSProj (JSIdent _) "vars") (JSNum _) <- js =
+      True
+  | JSIdent name <- js
+  , name `elem` constants =
+      True
+  | otherwise = False
 
+
 inlineJS :: JS -> JS
 inlineJS (JSReturn (JSApp (JSFunction [] err@(JSError _)) [])) = err
 inlineJS (JSReturn (JSApp (JSFunction ["cse"] body) [val@(JSVar _)])) =
@@ -564,14 +582,14 @@
           where
             replaceHelper :: [Int] -> JS -> JS
             replaceHelper tags (JSNew "__IDRRT__Con" [JSNum (JSInt tag), JSArray []])
-              | tag `elem` tags = JSIdent ("__IDRCTR__" ++ show tag)
+              | tag `elem` tags = JSIdent (idrCTRNamespace ++ show tag)
 
             replaceHelper tags js = transformJS (replaceHelper tags) js
 
 
         createConstant :: Int -> JS
         createConstant tag =
-          JSAlloc ("__IDRCTR__" ++ show tag) (Just (
+          JSAlloc (idrCTRNamespace ++ show tag) (Just (
             JSNew (idrRTNamespace ++ "Con") [JSNum (JSInt tag), JSArray []]
           ))
 
@@ -632,33 +650,11 @@
 
 
     inlineAble :: Int -> String -> [String] -> JS -> Maybe JS
-    inlineAble 1 fun args body
+    inlineAble 1 fun args (JSReturn body)
       | nonRecur fun body =
-          inlineAble' body
-            where
-              inlineAble' :: JS -> Maybe JS
-              inlineAble' (
-                  JSReturn js@(JSNew "__IDRRT__Con" [JSNum _, JSArray vals])
-                )
-                | and $ map (\x -> isJSIdent x || isJSConstant x) vals = Just js
-
-              inlineAble' (
-                  JSReturn js@(JSNew "__IDRRT__Cont" [JSFunction [] (
-                    JSReturn (JSApp (JSIdent _) args)
-                  )])
-                )
-                | and $ map (\x -> isJSIdent x || isJSConstant x) args = Just js
-
-              inlineAble' (
-                  JSReturn js@(JSIndex (JSProj (JSApp (JSIdent _) args) "vars") _)
-                )
-                | and $ map (\x -> isJSIdent x || isJSConstant x) args = Just js
-
-              inlineAble' _ = Nothing
-
-              isJSIdent js
-                | JSIdent _ <- js = True
-                | otherwise       = False
+          if all (<= 1) (map ($ body) (map countIDOccurences args))
+             then Just body
+             else Nothing
 
     inlineAble _ _ _ _ = Nothing
 
@@ -694,6 +690,16 @@
     countAll name js = sum $ map (countInvokations name) js
 
 
+    countIDOccurences :: String -> JS -> Int
+    countIDOccurences name = foldJS match (+) 0
+      where
+        match :: JS -> Int
+        match js
+          | JSIdent ident <- js
+          , name == ident = 1
+          | otherwise     = 0
+
+
     countInvokations :: String -> JS -> Int
     countInvokations name = foldJS match (+) 0
       where
@@ -785,10 +791,10 @@
         JSSeq [ JSAlloc "ret" $ Just (
                   JSTernary (
                     (JSIdent "arg0" `jsInstanceOf` jsCon) `jsAnd`
-                    (hasProp "__IDRLT__mEVAL0" "arg0")
+                    (hasProp "__IDRLT__EVAL" "arg0")
                   ) (JSApp
                       (JSIndex
-                        (JSIdent "__IDRLT__mEVAL0")
+                        (JSIdent "__IDRLT__EVAL")
                         (JSProj (JSIdent "arg0") "tag")
                       )
                       [JSIdent "arg0"]
@@ -811,10 +817,10 @@
               , JSAlloc "ret" $ Just (
                   JSTernary (
                     (JSIdent "ev" `jsInstanceOf` jsCon) `jsAnd`
-                    (hasProp "__IDRLT__mAPPLY0" "ev")
+                    (hasProp "__IDRLT__APPLY" "ev")
                   ) (JSApp
                       (JSIndex
-                        (JSIdent "__IDRLT__mAPPLY0")
+                        (JSIdent "__IDRLT__APPLY")
                         (JSProj (JSIdent "ev") "tag")
                       )
                       [JSIdent "fn0", JSIdent "arg0", JSIdent "ev"]
@@ -837,8 +843,8 @@
 
 unfoldLookupTable :: [JS] -> [JS]
 unfoldLookupTable input =
-  let (evals, evalunfold)   = unfoldLT "__IDRLT__mEVAL0" input
-      (applys, applyunfold) = unfoldLT "__IDRLT__mAPPLY0" evalunfold
+  let (evals, evalunfold)   = unfoldLT "__IDRLT__EVAL" input
+      (applys, applyunfold) = unfoldLT "__IDRLT__APPLY" evalunfold
       js                    = applyunfold in
       adaptRuntime $ expandCons evals applys js
   where
@@ -848,12 +854,12 @@
 
 
     adaptApply var = map (jsSubst (
-        JSIndex (JSIdent "__IDRLT__mAPPLY0") (JSProj (JSIdent var) "tag")
+        JSIndex (JSIdent "__IDRLT__APPLY") (JSProj (JSIdent var) "tag")
       ) (JSProj (JSIdent var) "app"))
 
 
     adaptEval = map (jsSubst (
-        JSIndex (JSIdent "__IDRLT__mEVAL0") (JSProj (JSIdent "arg0") "tag")
+        JSIndex (JSIdent "__IDRLT__EVAL") (JSProj (JSIdent "arg0") "tag")
       ) (JSProj (JSIdent "arg0") "eval"))
 
 
@@ -893,8 +899,8 @@
       where
         expandCons' :: JS -> JS
         expandCons' (JSNew "__IDRRT__Con" [JSNum (JSInt tag), JSArray args])
-          | evalid  <- getId "__IDRLT__mEVAL0"  tag evals
-          , applyid <- getId "__IDRLT__mAPPLY0" tag applys =
+          | evalid  <- getId "__IDRLT__EVAL"  tag evals
+          , applyid <- getId "__IDRLT__APPLY" tag applys =
               JSNew "__IDRRT__Con" [ JSNum (JSInt tag)
                                    , maybe JSNull JSIdent evalid
                                    , maybe JSNull JSIdent applyid
@@ -911,8 +917,8 @@
 
 
     ltIdentifier :: String -> Int -> String
-    ltIdentifier "__IDRLT__mEVAL0"  id = idrLTNamespace ++ "EVAL" ++ show id
-    ltIdentifier "__IDRLT__mAPPLY0" id = idrLTNamespace ++ "APPLY" ++ show id
+    ltIdentifier "__IDRLT__EVAL"  id = idrLTNamespace ++ "EVAL" ++ show id
+    ltIdentifier "__IDRLT__APPLY" id = idrLTNamespace ++ "APPLY" ++ show id
 
 
     extractLT :: String -> [JS] -> (JS, [JS])
@@ -1011,6 +1017,158 @@
           | otherwise = js
 
 
+extractLocalConstructors :: [JS] -> [JS]
+extractLocalConstructors js =
+  concatMap extractLocalConstructors' js
+  where
+    globalCons :: [String]
+    globalCons = concatMap (getGlobalCons) js
+
+
+    extractLocalConstructors' :: JS -> [JS]
+    extractLocalConstructors' js@(JSAlloc fun (Just (JSFunction args body))) =
+      map allocCon cons ++ [foldr (uncurry jsSubst) js (reverse cons)]
+      where
+        cons :: [(JS, JS)]
+        cons = zipWith genName (foldJS match (++) [] body) [1..]
+          where
+            genName :: JS -> Int -> (JS, JS)
+            genName js id =
+              (js, JSIdent $ idrCTRNamespace ++ fun ++ "_" ++ show id)
+
+            match :: JS -> [JS]
+            match js
+              | JSNew "__IDRRT__Con" args <- js
+              , all isConstant args = [js]
+              | otherwise           = []
+
+
+        allocCon :: (JS, JS) -> JS
+        allocCon (js, JSIdent name) =
+          JSAlloc name (Just js)
+
+
+        isConstant :: JS -> Bool
+        isConstant js
+          | JSNew "__IDRRT__Con" args <- js
+          , all isConstant args =
+              True
+          | otherwise =
+              isJSConstantConstructor globalCons js
+
+    extractLocalConstructors' js = [js]
+
+
+    getGlobalCons :: JS -> [String]
+    getGlobalCons js = foldJS match (++) [] js
+      where
+        match :: JS -> [String]
+        match js
+          | (JSAlloc name (Just (JSNew "__IDRRT__Con" _))) <- js =
+              [name]
+          | otherwise =
+              []
+
+
+evalCons :: [JS] -> [JS]
+evalCons js =
+  map (collapseCont . collapseTC . expandProj . evalCons') js
+  where
+    cons :: [(String, JS)]
+    cons = concatMap getGlobalCons js
+
+    evalCons' :: JS -> JS
+    evalCons' js = transformJS match js
+      where
+        match :: JS -> JS
+        match (JSApp (JSIdent "__IDRRT__EVALTC") [arg])
+          | JSIdent name                     <- arg
+          , Just (JSNew _ [_, JSNull, _, _]) <- lookupConstructor name cons =
+              arg
+
+        match (JSApp (JSIdent "__IDR__mEVAL0") [arg])
+          | JSIdent name                     <- arg
+          , Just (JSNew _ [_, JSNull, _, _]) <- lookupConstructor name cons =
+              arg
+
+        match js = transformJS match js
+
+
+    lookupConstructor :: String -> [(String, JS)] -> Maybe JS
+    lookupConstructor ctr cons
+      | Just (JSIdent name)  <- lookup ctr cons = lookupConstructor name cons
+      | Just con@(JSNew _ _) <- lookup ctr cons = Just con
+      | otherwise                               = Nothing
+
+
+    expandProj :: JS -> JS
+    expandProj js = transformJS match js
+      where
+        match :: JS -> JS
+        match (
+            JSIndex (
+              JSProj (JSIdent name) "vars"
+            ) (
+              JSNum (JSInt idx)
+            )
+          )
+          | Just (JSNew _ [_, _, _, JSArray args]) <- lookup name cons =
+              args !! idx
+
+        match js = transformJS match js
+
+
+    collapseTC :: JS -> JS
+    collapseTC js = transformJS match js
+      where
+        match :: JS -> JS
+        match (JSApp (JSIdent "__IDRRT__tailcall") [JSFunction [] (
+            JSReturn (JSIdent name)
+          )])
+          | Just _ <- lookup name cons = (JSIdent name)
+
+        match js = transformJS match js
+
+
+    collapseCont :: JS -> JS
+    collapseCont js = transformJS match js
+      where
+        match :: JS -> JS
+        match (JSNew "__IDRRT__Cont" [JSFunction [] (
+            JSReturn ret@(JSNew "__IDRRT__Cont" [JSFunction [] _])
+          )]) = collapseCont ret
+
+
+        match (JSNew "__IDRRT__Cont" [JSFunction [] (
+            JSReturn (JSIdent name)
+          )]) = JSIdent name
+
+        match (JSNew "__IDRRT__Cont" [JSFunction [] (
+            JSReturn ret@(JSNew "__IDRRT__Con" [_, _, _, JSArray args])
+          )])
+          | all collapsable args = ret
+          where
+            collapsable :: JS -> Bool
+            collapsable (JSIdent _) = True
+            collapsable js          = isJSConstantConstructor (map fst cons) js
+
+
+        match js = transformJS match js
+
+
+getGlobalCons :: JS -> [(String, JS)]
+getGlobalCons js = foldJS match (++) [] js
+  where
+    match :: JS -> [(String, JS)]
+    match js
+      | (JSAlloc name (Just con@(JSNew "__IDRRT__Con" _))) <- js =
+          [(name, con)]
+      | (JSAlloc name (Just con@(JSIdent _))) <- js =
+          [(name, con)]
+      | otherwise =
+          []
+
+
 codegenJavaScript
   :: JSTarget
   -> [(Name, SDecl)]
@@ -1067,7 +1225,9 @@
           , map removeInstanceChecks
           , inlineFunctions
           , map reduceContinuations
+          , extractLocalConstructors
           , unfoldLookupTable
+          , evalCons
           ]
 
     prelude :: [JS]
@@ -1227,7 +1387,7 @@
         lookup t = (JSApp
             (JSIndex (JSIdent t) (JSProj (JSIdent lvar) "tag"))
             [JSIdent "fn0", JSIdent "arg0", JSIdent lvar]) in
-        [ lookupTable [(var, "chk")] var cases
+        [ lookupTable "APPLY" [(var, "chk")] var cases
         , jsDecl $ JSFunction ["fn0", "arg0"] (
             JSSeq [ JSAlloc "__var_0" (Just $ JSIdent "fn0")
                   , JSAlloc (translateVariableName var) (
@@ -1235,8 +1395,8 @@
                     )
                   , JSReturn $ (JSTernary (
                        (JSVar var `jsInstanceOf` jsCon) `jsAnd`
-                       (hasProp lookupTableName (translateVariableName var))
-                    ) (lookup lookupTableName) JSNull)
+                       (hasProp (idrLTNamespace ++ "APPLY") (translateVariableName var))
+                    ) (lookup (idrLTNamespace ++ "APPLY")) JSNull)
                   ]
           )
         ]
@@ -1244,13 +1404,13 @@
   | (MN _ ev)            <- name
   , (SChkCase var cases) <- body
   , ev == txt "EVAL" =
-    [ lookupTable [] var cases
+    [ lookupTable "EVAL" [] var cases
     , jsDecl $ JSFunction ["arg0"] (JSReturn $
         JSTernary (
           (JSIdent "arg0" `jsInstanceOf` jsCon) `jsAnd`
-          (hasProp lookupTableName "arg0")
+          (hasProp (idrLTNamespace ++ "EVAL") "arg0")
         ) (JSApp
-            (JSIndex (JSIdent lookupTableName) (JSProj (JSIdent "arg0") "tag"))
+            (JSIndex (JSIdent (idrLTNamespace ++ "EVAL")) (JSProj (JSIdent "arg0") "tag"))
             [JSIdent "arg0"]
         ) (JSIdent "arg0")
       )
@@ -1276,13 +1436,9 @@
     getTag _                      = Nothing
 
 
-    lookupTableName :: String
-    lookupTableName = idrLTNamespace ++ translateName name
-
-
-    lookupTable :: [(LVar, String)] -> LVar -> [SAlt] -> JS
-    lookupTable aux var cases =
-      JSAlloc lookupTableName $ Just (
+    lookupTable :: String -> [(LVar, String)] -> LVar -> [SAlt] -> JS
+    lookupTable table aux var cases =
+      JSAlloc (idrLTNamespace ++ table) $ Just (
         JSApp (JSFunction [] (
           JSSeq $ [
             JSAlloc "t" $ Just (JSArray [])
diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs
--- a/src/Idris/AbsSyntax.hs
+++ b/src/Idris/AbsSyntax.hs
@@ -66,10 +66,13 @@
 addDyLib :: [String] -> Idris (Either DynamicLib String)
 addDyLib libs = do i <- getIState
                    let ls = idris_dynamic_libs i
+                   let importdirs = opt_importdirs (idris_options i)
                    case mapMaybe (findDyLib ls) libs of
                      x:_ -> return (Left x)
                      [] -> do
-                       handle <- lift . lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) $ libs
+                       handle <- lift . lift .
+                                 mapM (\l -> catchIO (tryLoadLib importdirs l)
+                                                     (\_ -> return Nothing)) $ libs
                        case msum handle of
                          Nothing -> return (Right $ "Could not load dynamic alternatives \"" ++
                                                     concat (intersperse "," libs) ++ "\"")
@@ -155,7 +158,77 @@
    = do i <- getIState
         putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }
 
--- | Adds error handlers for a particular function and argument. If names are is ambiguous, all matching handlers are updated.
+addTyInferred :: Name -> Idris ()
+addTyInferred n 
+   = do i <- getIState
+        putIState $ i { idris_tyinfodata =
+                        addDef n TIPartial (idris_tyinfodata i) }
+
+addTyInfConstraints :: FC -> [(Term, Term)] -> Idris ()
+addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts
+                               mapM_ addConstraint ts
+                               return ()
+    where addConstraint (x, y) = findMVApps x y
+
+          findMVApps x y
+             = do let (fx, argsx) = unApply x
+                  let (fy, argsy) = unApply y
+                  if (not (fx == fy)) 
+                     then do
+                       tryAddMV fx y
+                       tryAddMV fy x
+                     else mapM_ addConstraint (zip argsx argsy)
+
+          tryAddMV (P _ mv _) y =
+               do ist <- get
+                  case lookup mv (idris_metavars ist) of
+                       Just _ -> addConstraintRule mv y
+                       _ -> return ()
+          tryAddMV _ _ = return ()
+
+          addConstraintRule :: Name -> Term -> Idris ()
+          addConstraintRule n t 
+             = do ist <- get
+                  logLvl 1 $ "TI constraint: " ++ show (n, t)
+                  case lookupCtxt n (idris_tyinfodata ist) of
+                     [TISolution ts] -> 
+                         do mapM_ (checkConsistent t) ts
+                            let ti' = addDef n (TISolution (t : ts)) 
+                                               (idris_tyinfodata ist)
+                            put $ ist { idris_tyinfodata = ti' }
+                     _ ->  
+                         do let ti' = addDef n (TISolution [t]) 
+                                               (idris_tyinfodata ist)
+                            put $ ist { idris_tyinfodata = ti' }
+
+          -- Check a solution is consistent with previous solutions
+          -- Meaning: If heads are both data types, they had better be the
+          -- same.
+          checkConsistent :: Term -> Term -> Idris ()
+          checkConsistent x y =
+              do let (fx, _) = unApply x
+                 let (fy, _) = unApply y
+                 case (fx, fy) of
+                      (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n) 
+                      (P (TCon _ _) n _, Constant _) -> errWhen True
+                      (Constant _, P (TCon _ _) n' _) -> errWhen True
+                      (P (DCon _ _) n _, P (DCon _ _) n' _) -> errWhen (n/=n) 
+                      _ -> return ()
+
+              where errWhen True 
+                       = throwError (At fc 
+                            (CantUnify False x y (Msg "") [] 0))
+                    errWhen False = return ()
+
+isTyInferred :: Name -> Idris Bool
+isTyInferred n
+   = do i <- getIState
+        case lookupCtxt n (idris_tyinfodata i) of
+             [TIPartial] -> return True
+             _ -> return False
+
+-- | Adds error handlers for a particular function and argument. If names are
+-- ambiguous, all matching handlers are updated.
 addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()
 addFunctionErrorHandlers f arg hs =
  do i <- getIState
@@ -425,14 +498,19 @@
 
 iRender :: Doc a -> Idris (SimpleDoc a)
 iRender d = do w <- getWidth
+               ist <- getIState
+               let ideSlave = case idris_outputmode ist of
+                                IdeSlave _ -> True
+                                _          -> False
                case w of
                  InfinitelyWide -> return $ renderPretty 1.0 1000000000 d
                  ColsWide n -> return $
                                if n < 1
                                  then renderPretty 1.0 1000000000 d
                                  else renderPretty 0.8 n d
-                 AutomaticWidth -> do width <- runIO getScreenWidth
-                                      return $ renderPretty 0.8 width d
+                 AutomaticWidth | ideSlave  -> return $ renderPretty 1.0 1000000000 d
+                                | otherwise -> do width <- runIO getScreenWidth
+                                                  return $ renderPretty 0.8 width d
 
 ihPrintResult :: Handle -> String -> Idris ()
 ihPrintResult h s = do i <- getIState
diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs
--- a/src/Idris/AbsSyntaxTree.hs
+++ b/src/Idris/AbsSyntaxTree.hs
@@ -112,6 +112,7 @@
     idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
     idris_calledgraph :: Ctxt [Name],
     idris_docstrings :: Ctxt String,
+    idris_tyinfodata :: Ctxt TIData,
     idris_totcheck :: [(FC, Name)], -- names to check totality on 
     idris_defertotcheck :: [(FC, Name)], -- names to check at the end
     idris_options :: IOption,
@@ -216,7 +217,7 @@
 idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
                    emptyContext emptyContext emptyContext emptyContext
                    emptyContext emptyContext emptyContext emptyContext
-                   emptyContext
+                   emptyContext emptyContext
                    [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []
                    [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
                    True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty
@@ -811,6 +812,12 @@
 deriving instance NFData ClassInfo
 !-}
 
+-- Type inference data
+
+data TIData = TIPartial -- ^ a function with a partially defined type
+            | TISolution [Term] -- ^ possible solutions to a metavariable in a type 
+    deriving Show
+
 -- An argument is conditionally forceable iff its forceability
 -- depends on the collapsibility of the whole type.
 data Forceability = Conditional | Unconditional deriving (Show, Enum, Bounded, Eq, Ord)
@@ -952,7 +959,10 @@
 getInferTerm (App (App _ _) tm) = tm
 getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
 
-getInferType (Bind n b sc) = Bind n b $ getInferType sc
+getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
+  where toTy (Lam t) = Pi t
+        toTy (PVar t) = PVTy t
+        toTy b = b
 getInferType (App (App _ ty) _) = ty
 
 
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
@@ -466,8 +466,6 @@
     do args <- prepare_apply fn (map fst imps)
        -- _Don't_ solve the arguments we're specifying by hand.
        -- (remove from unified list before calling end_unify)
-       -- HMMM: Actually, if we get it wrong, the typechecker will complain!
-       -- so do nothing
        hs <- get_holes
        ES (p, a) s prev <- get
        let dont = head hs : dontunify p ++
diff --git a/src/Idris/Core/Unify.hs b/src/Idris/Core/Unify.hs
--- a/src/Idris/Core/Unify.hs
+++ b/src/Idris/Core/Unify.hs
@@ -257,7 +257,7 @@
                                  then unifyTmpFail xtm tm
                                  else do sc 1
                                          checkCycle bnames (x, tm)
-        | not (injective xtm) && injective tm = unifyFail xtm tm
+        | not (injective xtm) && injective tm = unifyTmpFail xtm tm
     un' fn bnames tm ytm@(P _ y _)
         | holeIn env y || y `elem` holes
                        = do UI s f <- get
@@ -268,7 +268,7 @@
                                  then unifyTmpFail tm ytm
                                  else do sc 1
                                          checkCycle bnames (y, tm)
-        | not (injective ytm) && injective tm = unifyFail ytm tm
+        | not (injective ytm) && injective tm = unifyTmpFail tm ytm
     un' fn bnames (V i) (P _ x _)
         | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []
     un' fn bnames (P _ x _) (V i)
@@ -379,9 +379,10 @@
                      unArgs vs xs ys
 
             metavarApp tm = let (f, args) = unApply tm in
-                                metavar f &&
-                                all (\x -> metavarApp x) args
-                                   && nub args == args
+                                (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
@@ -413,14 +414,22 @@
 
             rigid (P (DCon _ _) _ _) = True
             rigid (P (TCon _ _) _ _) = True
-            rigid t@(P Ref _ _)      = inenv t
+            rigid t@(P Ref _ _)      = inenv t || globmetavar t
             rigid (Constant _)       = True
             rigid (App f a)          = rigid f && rigid a
-            rigid t                  = not (metavar t)
+            rigid t                  = not (metavar t) || globmetavar t
 
+            globmetavar t = case unApply t  of
+                                (P _ x _, _) ->
+                                   case lookupDef x ctxt of
+                                        [TyDecl _ _] -> True
+                                        _ -> False
+                                _ -> False
+
             metavar t = case t of
-                             P _ x _ -> (x `elem` holes || holeIn env x) &&
-                                        not (x `elem` dont)
+                             P _ x _ -> ((x `elem` holes || holeIn env x) &&
+                                        not (x `elem` dont))
+                                          || globmetavar t
                              _ -> False
             pat t = case t of
                          P _ x _ -> x `elem` holes || patIn env x
diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs
--- a/src/Idris/Delaborate.hs
+++ b/src/Idris/Delaborate.hs
@@ -151,7 +151,7 @@
     _ -> line <> line <> text "Specifically:" <>
          indented (pprintErr' i e) <>
          if (opt_errContext (idris_options i)) then text $ showSc i sc else empty
-pprintErr' i (CantConvert x y env) =
+pprintErr' i (CantConvert x y env) = trace (show (x,y)) $ 
   text "Can't convert" <> indented (pprintTerm i (delab i x)) <$>
   text "with" <> indented (pprintTerm i (delab i y)) <>
   if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty
diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs
--- a/src/Idris/ElabDecls.hs
+++ b/src/Idris/ElabDecls.hs
@@ -49,10 +49,19 @@
          addConstraints fc cs
          return (tm, ty)
 
-checkDef fc ns = do ctxt <- getContext
-                    mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t
-                                                  return (n, (i, top, t'))) ns
 
+checkDef fc ns = checkAddDef False True fc ns
+
+checkAddDef add toplvl fc [] = return []
+checkAddDef add toplvl fc ((n, (i, top, t)) : ns) 
+               = do ctxt <- getContext
+                    (t', _) <- recheckC fc [] t
+                    when add $ addDeferred [(n, (i, top, t, toplvl))]
+                    ns' <- checkAddDef add toplvl fc ns
+                    return ((n, (i, top, t')) : ns')
+--                     mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t
+--                                                   return (n, (i, top, t'))) ns
+
 -- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".
 elabType :: ElabInfo -> SyntaxInfo -> String ->
             FC -> FnOpts -> Name -> PTerm -> Idris Type
@@ -76,9 +85,12 @@
          ((tyT, defer, is), log) <-
                tclift $ elaborate ctxt n (TType (UVal 0)) []
                         (errAt "type of " n (erun fc (build i info False [] n ty)))
-         ds <- checkDef fc defer
-         let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
-         addDeferred ds'
+         ds <- checkAddDef True False fc 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
+--          let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
+--          addDeferred ds'
          mapM_ (elabCaseBlock info opts) is
          ctxt <- getContext
          logLvl 5 $ "Rechecking"
@@ -630,7 +642,7 @@
 
          -- Elaborate the provider term to TT and check that the type matches
          (e, et) <- elabVal toplevel False tm
-         unless (isProviderOf ty' et) $
+         unless (isProviderOf (normalise ctxt [] ty') et) $
            ifail $ "Expected provider type IO (Provider (" ++
                    show ty' ++ "))" ++ ", got " ++ show et ++ " instead."
 
@@ -1262,6 +1274,7 @@
         -- Build the LHS as an "Infer", and pull out its type and
         -- pattern bindings
         i <- getIState
+        inf <- isTyInferred fname
         -- get the parameters first, to pass through to any where block
         let fn_ty = case lookupTy fname (tt_ctxt i) of
                          [t] -> t
@@ -1275,16 +1288,25 @@
         logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)
         logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
 
-        ((lhs', dlhs, []), _) <-
+        (((lhs', dlhs, []), probs), _) <-
             tclift $ elaborate ctxt (sMN 0 "patLHS") infP []
-                     (errAt "left hand side of " fname
-                       (erun fc (buildTC i info True opts fname (infTerm lhs))))
+                     (do res <- errAt "left hand side of " fname
+                                  (erun fc (buildTC i info True opts fname (infTerm lhs)))
+                         probs <- get_probs
+                         return (res, probs))
+
+        when inf $ addTyInfConstraints fc (map (\(x,y,_,_) -> (x,y)) probs)
+
         let lhs_tm = orderPats (getInferTerm lhs')
         let lhs_ty = getInferType lhs'
         logLvl 3 ("Elaborated: " ++ show lhs_tm)
         logLvl 3 ("Elaborated type: " ++ show lhs_ty)
 
-        (clhs_c, clhsty) <- recheckC fc [] lhs_tm
+        -- 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
+                               else return (lhs_tm, lhs_ty)
         let clhs = normalise ctxt [] clhs_c
         
         logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))
@@ -1319,7 +1341,7 @@
         logLvl 2 $ "RHS: " ++ showTmImpls rhs
         ctxt <- getContext -- new context with where block added
         logLvl 5 "STARTING CHECK"
-        ((rhs', defer, is), _) <-
+        ((rhs', defer, is, probs), _) <-
            tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty []
                     (do pbinds lhs_tm
                         setNextName 
@@ -1332,7 +1354,11 @@
                         mapM_ (elabCaseHole aux) hs
                         tt <- get_term
                         let (tm, ds) = runState (collectDeferred (Just fname) tt) []
-                        return (tm, ds, is))
+                        probs <- get_probs
+                        return (tm, ds, is, probs))
+
+        when inf $ addTyInfConstraints fc (map (\(x,y,_,_) -> (x,y)) probs)
+
         logLvl 5 "DONE CHECK"
         logLvl 2 $ "---> " ++ show rhs'
         when (not (null defer)) $ iLOG $ "DEFERRED " ++ show (map fst defer)
@@ -1352,7 +1378,9 @@
         ctxt <- getContext
         logLvl 5 $ "Rechecking"
         logLvl 6 $ " ==> " ++ show (forget rhs')
-        (crhs, crhsty) <- recheckC fc [] rhs'
+        (crhs, crhsty) <- if not inf 
+                             then recheckC fc [] rhs'
+                             else return (rhs', clhsty)
         logLvl 6 $ " ==> " ++ show crhsty ++ "   against   " ++ show clhsty
         case  converts ctxt [] clhsty crhsty of
             OK _ -> return ()
diff --git a/src/Idris/ElabTerm.hs b/src/Idris/ElabTerm.hs
--- a/src/Idris/ElabTerm.hs
+++ b/src/Idris/ElabTerm.hs
@@ -11,6 +11,7 @@
 import Idris.Core.Elaborate hiding (Tactic(..))
 import Idris.Core.TT
 import Idris.Core.Evaluate
+import Idris.Core.Unify
 import Idris.Core.Typecheck (check)
 
 import Control.Applicative ((<$>))
@@ -46,6 +47,10 @@
          ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
 build ist info pattern opts fn tm
     = do elab ist info pattern opts fn tm
+         let tmIn = tm
+         let inf = case lookupCtxt fn (idris_tyinfodata ist) of
+                        [TIPartial] -> True
+                        _ -> False
          ivs <- get_instances
          hs <- get_holes
          ptm <- get_term
@@ -70,7 +75,8 @@
          probs <- get_probs
          case probs of
             [] -> return ()
-            ((_,_,_,e):es) -> lift (Error e)
+            ((_,_,_,e):es) -> if inf then return ()
+                                     else lift (Error e)
          is <- getAux
          tt <- get_term
          let (tm, ds) = runState (collectDeferred (Just fn) tt) []
@@ -87,13 +93,18 @@
 buildTC ist info pattern opts fn tm
     = do -- set name supply to begin after highest index in tm
          let ns = allNamesIn tm
+         let tmIn = tm
+         let inf = case lookupCtxt fn (idris_tyinfodata ist) of
+                        [TIPartial] -> True
+                        _ -> False
          initNextNameFrom ns
          elab ist info pattern opts fn tm
          probs <- get_probs
          tm <- get_term
          case probs of
             [] -> return ()
-            ((_,_,_,e):es) -> lift (Error e)
+            ((_,_,_,e):es) -> if inf then return ()
+                                     else lift (Error e)
          is <- getAux
          tt <- get_term
          let (tm, ds) = runState (collectDeferred (Just fn) tt) []
@@ -841,7 +852,8 @@
                    Term -> State [(Name, (Int, Maybe Name, Type))] Term
 collectDeferred top (Bind n (GHole i t) app) =
     do ds <- get
-       when (not (n `elem` map fst ds)) $ put ((n, (i, top, t)) : ds)
+       t' <- collectDeferred top t
+       when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t'))])
        collectDeferred top app
 collectDeferred top (Bind n b t) = do b' <- cdb b
                                       t' <- collectDeferred top t
diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs
--- a/src/Idris/IBC.hs
+++ b/src/Idris/IBC.hs
@@ -26,7 +26,7 @@
 
 
 ibcVersion :: Word8
-ibcVersion = 58
+ibcVersion = 59
 
 
 data IBCFile = IBCFile { ver :: Word8,
@@ -1650,6 +1650,10 @@
                                    put x1
                 PNoImplicits x1 -> do putWord8 36
                                       put x1
+                PDisamb x1 x2 -> do putWord8 37
+                                    put x1
+                                    put x2
+
         get
           = do i <- getWord8
                case i of
@@ -1759,6 +1763,9 @@
                             return (PUnifyLog x1)
                    36 -> do x1 <- get
                             return (PNoImplicits x1)
+                   37 -> do x1 <- get
+                            x2 <- get
+                            return (PDisamb x1 x2)
                    _ -> error "Corrupted binary data for PTerm"
 
 instance (Binary t) => Binary (PTactic' t) where
diff --git a/src/Idris/ParseExpr.hs b/src/Idris/ParseExpr.hs
--- a/src/Idris/ParseExpr.hs
+++ b/src/Idris/ParseExpr.hs
@@ -70,8 +70,14 @@
       |   InternalExpr;
 @
  -}
-expr' :: SyntaxInfo -> IdrisParser PTerm
-expr' syn =     try (externalExpr syn)
+expr' syn = doexpr' syn
+--    = do l <- restOfLine
+--         f <- getFC
+--         e <- trace (show (f, l)) $ doexpr' syn
+--         return e
+
+doexpr' :: SyntaxInfo -> IdrisParser PTerm
+doexpr' syn =     try (externalExpr syn)
             <|> internalExpr syn
             <?> "expression"
 
@@ -181,6 +187,7 @@
   | Let
   | RewriteTerm
   | Pi
+  | CaseExpr
   | DoBlock
   ;
 @
@@ -199,6 +206,7 @@
      <|> rewriteTerm syn
      <|> try(pi syn)
      <|> doBlock syn
+     <|> caseExpr syn
      <|> simpleExpr syn
      <?> "expression"
 
@@ -263,7 +271,6 @@
   | 'refl' ('{' Expr '}')?
   | ProofExpr
   | TacticsExpr
-  | CaseExpr
   | FnName
   | List
   | Comprehension
@@ -290,7 +297,6 @@
         <|> do reserved "elim_for"; fc <- getFC; t <- fnName; return (PRef fc (SN $ ElimN t))
         <|> proofExpr syn
         <|> tacticsExpr syn
-        <|> caseExpr syn
         <|> do reserved "Type"; return PType
         <|> try (do c <- constant
                     fc <- getFC
diff --git a/src/Idris/ParseHelpers.hs b/src/Idris/ParseHelpers.hs
--- a/src/Idris/ParseHelpers.hs
+++ b/src/Idris/ParseHelpers.hs
@@ -260,7 +260,8 @@
 -- | Parses an operator
 operator :: MonadicParsing m => m String
 operator = do op <- token . some $ operatorLetter
-              when (op == ":") $ fail "(:) is not a valid operator"
+              when (op `elem` [":", "=>", "->", "<-", "=", "?="]) $ 
+                   fail $ op ++ " is not a valid operator"
               return op
 
 {- * Position helpers -}
diff --git a/src/Idris/ParseOps.hs b/src/Idris/ParseOps.hs
--- a/src/Idris/ParseOps.hs
+++ b/src/Idris/ParseOps.hs
@@ -39,7 +39,7 @@
       [[backtick],
        [binary "$" (\fc x y -> PApp fc x [pexp y]) AssocRight],
        [binary "="  PEq AssocLeft],
-       [binary "->" (\fc x y -> PPi expl (sMN 42 "__pi_arg") x y) AssocRight]]
+       [binary "->" (\fc x y -> PPi expl (sUN "__pi_arg") x y) AssocRight]]
 
 -- | Calculates table for fixtiy declarations
 toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm
diff --git a/src/Idris/ProofSearch.hs b/src/Idris/ProofSearch.hs
--- a/src/Idris/ProofSearch.hs
+++ b/src/Idris/ProofSearch.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE PatternGuards #-}
+
 module Idris.ProofSearch(trivial, proofSearch) where
 
 import Idris.Core.Elaborate hiding (Tactic(..))
@@ -36,9 +38,20 @@
 
 proofSearch :: (PTerm -> ElabD ()) -> Maybe Name -> Name -> [Name] ->
                IState -> ElabD ()
-proofSearch elab fn nroot hints ist = psRec maxDepth
+proofSearch elab fn nroot hints ist 
+       = case lookupCtxt nroot (idris_tyinfodata ist) of
+              [TISolution ts] -> findInferredTy ts
+              _ -> psRec maxDepth
   where
     maxDepth = 6
+
+    findInferredTy (t : _) = elab (delab ist (toUN t)) 
+
+    toUN t@(P nt (MN i n) ty) 
+       | ('_':xs) <- str n = t
+       | otherwise = P nt (UN n) ty
+    toUN (App f a) = App (toUN f) (toUN a)
+    toUN t = t
 
     psRec 0 = do attack; defer nroot; solve --fail "Maximum depth reached"
     psRec d = try' (trivial elab ist)
diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs
--- a/src/Idris/REPL.hs
+++ b/src/Idris/REPL.hs
@@ -8,6 +8,7 @@
 import Idris.ElabDecls
 import Idris.ElabTerm
 import Idris.Error
+import Idris.ErrReverse
 import Idris.Delaborate
 import Idris.Prover
 import Idris.Parser
@@ -486,7 +487,7 @@
   where
     showMetavarInfo imp ist n i
          = case lookupTy n (tt_ctxt ist) of
-                (ty:_) -> putTy imp ist i [] (delab ist ty)
+                (ty:_) -> putTy imp ist i [] (delab ist (errReverse ist ty))
     putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
     putTy imp ist 0 bnd sc = putGoal imp ist bnd sc
     putTy imp ist i bnd (PPi _ n t sc)
@@ -894,8 +895,9 @@
                   _ -> iPrintError $ "Ambiguous name"
 process h fn (DynamicLink l)
                            = do i <- getIState
-                                let lib = trim l
-                                handle <- lift . lift $ tryLoadLib lib
+                                let importdirs = opt_importdirs (idris_options i)
+                                    lib = trim l
+                                handle <- lift . lift $ tryLoadLib importdirs lib
                                 case handle of
                                   Nothing -> iPrintError $ "Could not load dynamic lib \"" ++ l ++ "\""
                                   Just x -> do let libs = idris_dynamic_libs i
diff --git a/src/Util/DynamicLinker.hs b/src/Util/DynamicLinker.hs
--- a/src/Util/DynamicLinker.hs
+++ b/src/Util/DynamicLinker.hs
@@ -1,7 +1,7 @@
 -- | Platform-specific dynamic linking support. Add new platforms to this file
 -- through conditional compilation.
 {-# LANGUAGE ExistentialQuantification, CPP #-}
-module Util.DynamicLinker where
+module Util.DynamicLinker (ForeignFun(..), DynamicLib(..), tryLoadLib, tryLoadFn) where
 
 #ifdef IDRIS_FFI
 import Foreign.LibFFI
@@ -9,11 +9,13 @@
 import System.Directory
 #ifndef WINDOWS
 import System.Posix.DynamicLinker
+import System.FilePath.Posix ((</>))
 #else
 import qualified Control.Exception as Exception (catch, IOException)
 import System.Win32.DLL
 import System.Win32.Types
 type DL = HMODULE
+import System.FilePath.Windows ((</>))
 #endif
 
 hostDynamicLibExt :: String
@@ -45,14 +47,27 @@
 instance Eq DynamicLib where
     (Lib a _) == (Lib b _) = a == b
 
+firstExisting :: [FilePath] -> IO (Maybe FilePath)
+firstExisting [] = return Nothing
+firstExisting (f:fs) = do exists <- doesFileExist f
+                          if exists
+                            then return (Just f)
+                            else firstExisting fs
+
+libFileName :: [FilePath] -> String -> IO String
+libFileName dirs lib = do let names = [lib, lib ++ "." ++ hostDynamicLibExt]
+                          cwd <- getCurrentDirectory
+                          found <- firstExisting $
+                                   map ("."</>) names ++ [d </> f | d <- cwd:dirs, f <- names]
+                          return $ maybe (lib ++ "." ++ hostDynamicLibExt) id found
+
 #ifndef WINDOWS
-tryLoadLib :: String -> IO (Maybe DynamicLib)
-tryLoadLib lib = do exactName <- doesFileExist lib
-                    let filename = if exactName then lib else lib ++ "." ++ hostDynamicLibExt
-                    handle <- dlopen filename [RTLD_NOW, RTLD_GLOBAL]
-                    if undl handle == nullPtr
-                      then return Nothing
-                      else return . Just $ Lib lib handle
+tryLoadLib :: [FilePath] -> String -> IO (Maybe DynamicLib)
+tryLoadLib dirs lib = do filename <- libFileName dirs lib
+                         handle <- dlopen filename [RTLD_NOW, RTLD_GLOBAL]
+                         if undl handle == nullPtr
+                           then return Nothing
+                           else return . Just $ Lib lib handle
 
 
 tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun)
@@ -61,13 +76,12 @@
                                then return Nothing
                                else return . Just $ Fun fn cFn
 #else
-tryLoadLib :: String -> IO (Maybe DynamicLib)
-tryLoadLib lib = do exactName <- doesFileExist lib
-                    let filename = if exactName then lib else lib ++ "." ++ hostDynamicLibExt
-                    handle <- Exception.catch (loadLibrary filename) nullPtrOnException
-                    if handle == nullPtr
-                        then return Nothing
-                        else return . Just $ Lib lib handle
+tryLoadLib :: [FilePath] -> String -> IO (Maybe DynamicLib)
+tryLoadLib dirs lib = do filename <- libFileName dirs lib
+                         handle <- Exception.catch (loadLibrary filename) nullPtrOnException
+                         if handle == nullPtr
+                             then return Nothing
+                             else return . Just $ Lib lib handle
   where nullPtrOnException :: Exception.IOException -> IO DL
         nullPtrOnException e = return nullPtr
         -- `show e` will however give broken error message
@@ -86,11 +100,17 @@
                       }
     deriving Eq
 
-tryLoadLib :: String -> IO (Maybe DynamicLib)
-tryLoadLib lib = do putStrLn $ "WARNING: Cannot load '" ++ lib ++ "' at compile time because Idris was compiled without libffi support."
-                    return Nothing
+data ForeignFun = forall a. Fun { fun_name :: String
+                                , fun_handle :: ()
+                                }
 
+tryLoadLib :: [FilePath] -> String -> IO (Maybe DynamicLib)
+tryLoadLib fps lib = do putStrLn $ "WARNING: Cannot load '" ++ lib ++ "' at compile time because Idris was compiled without libffi support."
+                        return Nothing
 
+tryLoadFn :: String -> DynamicLib -> IO (Maybe ForeignFun)
+tryLoadFn fn lib = do putStrLn $ "WARNING: Cannot load '" ++ fn ++ "' at compile time because Idris was compiled without libffi support."
+                      return Nothing
 #endif
 
 
diff --git a/test/dsl002/run b/test/dsl002/run
--- a/test/dsl002/run
+++ b/test/dsl002/run
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 idris $@ test014.idr -o test014
 ./test014
-rm -f test014 resimp.ibc test014.ibc
+rm -f test014 Resimp.ibc test014.ibc
diff --git a/test/proof003/run b/test/proof003/run
--- a/test/proof003/run
+++ b/test/proof003/run
@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 idris $@ test015.idr -o test015
 ./test015
-rm -f test015 parity.ibc test015.ibc
+rm -f test015 Parity.ibc test015.ibc