diff --git a/Makefile b/Makefile
--- a/Makefile
+++ b/Makefile
@@ -33,6 +33,9 @@
 
 $(EXE): default
 
+install: $(EXE) Setup
+	./Setup install
+
 test tests: $(EXE)
 	@$(SHELL) $(EXAMPLES)/run-tests.sh ./$(EXE) $(EXAMPLES)
 
@@ -63,7 +66,7 @@
 	$(RM) html
 
 
-VERSION = 0.6.3
+VERSION = 0.6.5
 DISTDIR = alms-$(VERSION)
 TARBALL = $(DISTDIR).tar.gz
 
diff --git a/alms.cabal b/alms.cabal
--- a/alms.cabal
+++ b/alms.cabal
@@ -1,5 +1,5 @@
 Name:           alms
-Version:        0.6.3
+Version:        0.6.5
 Copyright:      2011, Jesse A. Tov
 Cabal-Version:  >= 1.8
 License:        BSD3
@@ -54,7 +54,6 @@
   GHC-Options:          -O3
   CPP-Options:          -DALMS_CABAL_BUILD
   Build-Depends:
-                        haskell98,
                         base == 4.*,
                         HUnit >= 1.2,
                         QuickCheck >= 2,
diff --git a/alms.cabal.sh b/alms.cabal.sh
--- a/alms.cabal.sh
+++ b/alms.cabal.sh
@@ -57,7 +57,6 @@
   GHC-Options:          -O3
   CPP-Options:          -DALMS_CABAL_BUILD
   Build-Depends:
-                        haskell98,
                         base == 4.*,
                         HUnit >= 1.2,
                         QuickCheck >= 2,
diff --git a/examples/echoServer.alms b/examples/echoServer.alms
--- a/examples/echoServer.alms
+++ b/examples/echoServer.alms
@@ -1,40 +1,37 @@
 (* Echo server written using state-tracked sockets. *)
 
-#load "libsocketcap"
+#load "libsocketcap3"
 
 module EchoServer = struct
-  open ASocket
+  open SocketCap
 
   (* This is a bit different than the version in the paper, because
    * it uses exceptions. *)
-  let handleClient sock f cap =
-    let rec loop cap =
-      let (str, cap) = recv sock 1024 cap in
-      let cap        = send sock (f str) cap in
-        loop cap
-     in try
-          loop cap
-        with SocketError _ → ()
+  let rec clientLoop f sock !cap =
+    let str = recv sock 1024 cap in
+      send sock (f str) $> cap;
+      clientLoop f sock cap
 
-  let rec acceptLoop sock f cap =
-    let ((clientsock, clientcap), cap) = accept sock cap in
+  let rec acceptLoop f sock !cap =
+    let (clientsock, clientcap) = accept sock cap in
       putStrLn "Opened connection";
-      (Thread.fork :> (unit -A> unit) → Thread.thread)
-        (λ _ → handleClient clientsock f clientcap;
-               putStrLn "Closed connection");
-      acceptLoop sock f cap
+      Thread.fork (λ _ →
+        catchReady (λ _ → clientLoop f clientsock clientcap)
+          (clientsock, λ clientcap →
+            close clientsock clientcap;
+            putStrLn "Closed connection"));
+      acceptLoop f sock cap
 
   let serve port f =
-    let (sock, cap) = socket () in
-    let cap = bind sock port cap in
-    let cap = listen sock cap in
-      acceptLoop sock f cap
+    let (sock, !cap) = socket () in
+    bind sock port $> cap;
+    listen sock $> cap;
+    acceptLoop f sock cap
 end
 
 let serverFun (s: string) = s
 
-let main argv =
-  match argv with
+let main = function
   | [port] → EchoServer.serve (int_of_string port) serverFun
   | _      → failwith "Usage: echoServer.aff PORT\n"
 
diff --git a/examples/ex33-session-types.alms b/examples/ex33-session-types.alms
--- a/examples/ex33-session-types.alms
+++ b/examples/ex33-session-types.alms
@@ -10,12 +10,12 @@
 let server c =
   let (x, c) = recv c in
   let (y, c) = recv c in
-    send c (x + y);
+    send (x + y) c;
     ()
 
 let client c x y =
-  let c = send c x in
-  let c = send c y in
+  let c = send x c in
+  let c = send y c in
   let (r, _) = recv c in
     r
 
diff --git a/examples/ex34-session-types.alms b/examples/ex34-session-types.alms
--- a/examples/ex34-session-types.alms
+++ b/examples/ex34-session-types.alms
@@ -14,17 +14,17 @@
     | Left c ->
         let (x, c) = recv c in
         let (y, c) = recv c in
-          send c (x + y);
+          send (x + y) c;
           ()
     | Right c ->
         let (x, c) = recv c in
-          send c (0 - x);
+          send (0 - x) c;
           ()
 
 let client c x y =
       let c = sel1 c in
-      let c = send c x in
-      let c = send c y in
+      let c = send x c in
+      let c = send y c in
       let (r, _) = recv c in
         r
 
diff --git a/examples/session-types-polygons-3.in b/examples/session-types-polygons-3.in
--- a/examples/session-types-polygons-3.in
+++ b/examples/session-types-polygons-3.in
@@ -11,5 +11,4 @@
 (-1, 3, 3)
 (-1, -1, 3)
 (-1, -1, -1)
-(0, 0, -1)
 
diff --git a/examples/session-types-polygons.alms b/examples/session-types-polygons.alms
--- a/examples/session-types-polygons.alms
+++ b/examples/session-types-polygons.alms
@@ -5,188 +5,192 @@
 
 open SessionType
 
---
--- We first build a tiny 3-D geometry library
---
+(*
+We first build a tiny 3-D geometry library
+*)
+module type GEOMETRY = sig
+  (* Points, planes, and line segments in R³ *)
+  type point   = { x, y, z : float }
+  type plane   = { a, b, c, d : float }
+  type segment = point × point
 
--- Points and planes in R^3.
-type point = { x, y, z : float }
-type plane = [ `Plane of float * float * float * float ]
+  (*
+    The plane { a, b, c, d } represents the open half-space
+    { (x, y, z) | ax + by + cz + d > 0 }
+  *)
 
--- We use the plane `Plane(a, b, c, d) to represent the open half-space
--- { Point(x, y, z) | ax + by + cz + d > 0 }
+  val string_of_point : point → string
+  val string_of_plane : plane → string
 
-let string_of_point p =
-    "(" ^ string_of p.x ^ ", " ^ string_of p.y ^ ", " ^ string_of p.z ^ ")"
+  val point_of_string : string → point
+  val plane_of_string : string → plane
 
-let string_of_plane (`Plane(a, b, c, d): plane) =
-    string_of a ^ "x + " ^ string_of b ^ "y + " ^
-    string_of c ^ "z + " ^ string_of d ^ " > 0"
+  (* Is the point above the plane?  (i.e., in the semi-space) *)
+  val isPointAbovePlane         : point → plane → bool
 
-(* Some of this should be in the library! *)
-let splitWhile : ('a -> bool) -> 'a list -> 'a list * 'a list
-  = fun pred ->
-      let rec loop (acc: 'a list) (xs: 'a list) : 'a list * 'a list =
-                match xs with
-                | []         -> (rev acc, [])
-                | (x ∷ xs') -> if pred x
-                                   then loop (x ∷ acc) xs'
-                                   else (rev acc, xs)
-       in loop []
+  (* Does the line segment between the two points intersect the plane,
+     and if so, where? *)
+  val intersect       : segment → plane → point option
+end
 
-let not (b: bool) = if b then false else true
+module Geometry : GEOMETRY = struct
+  type point   = { x, y, z : float }
+  type plane   = { a, b, c, d : float }
+  type segment = point × point
 
-let notp (pred: 'a -> bool): 'a -> bool =
-  fun a -> not (pred a)
+  let string_of_point p =
+      "(" ^ string_of p.x ^ ", " ^ string_of p.y ^ ", " ^ string_of p.z ^ ")"
 
-let isSpace (c: char): bool =
-  match c with
-  | ' '  -> true
-  | '\t' -> true
-  | '\n' -> true
-  | '\r' -> true
-  | _    -> false
+  let string_of_plane {a, b, c, d} =
+      string_of a ^ "x + " ^ string_of b ^ "y + " ^
+      string_of c ^ "z + " ^ string_of d ^ " > 0"
 
-let dropSpace (cs : char list) : char list =
-  let (_, result) = splitWhile isSpace cs in result
+  (* Some of this should be in the library! *)
+  let splitWhile pred =
+    let rec loop acc xs =
+              match xs with
+              | []      → (rev acc, [])
+              | x ∷ xs' → if pred x
+                            then loop (x ∷ acc) xs'
+                            else (rev acc, xs)
+     in loop []
 
-let parsePoint (s : string) : point =
-  let foil (x: char list) = float_of_string (implode x) in
-    let cs = explode s in
-    let ('(' ∷ cs) = dropSpace cs in
-    let (x, (_ ∷ cs)) = splitWhile (notp ((==) ',')) (dropSpace cs) in
-    let (y, (_ ∷ cs)) = splitWhile (notp ((==) ',')) (dropSpace cs) in
-    let (z, (_ ∷ cs)) = splitWhile (notp ((==) ')')) (dropSpace cs) in
-      { x = foil x, y = foil y, z = foil z }
+  let notp = compose not
 
-let parsePlane (s: string) : plane =
-  let foil (x: char list) = float_of_string (implode x) in
-    let cs = explode s in
-    let (a, (_ ∷ cs)) = splitWhile (notp ((==) 'x')) (dropSpace cs) in
-    let ('+' ∷ cs)    = dropSpace cs in
-    let (b, (_ ∷ cs)) = splitWhile (notp ((==) 'y')) (dropSpace cs) in
-    let ('+' ∷ cs)    = dropSpace cs in
-    let (c, (_ ∷ cs)) = splitWhile (notp ((==) 'z')) (dropSpace cs) in
-    let ('+' ∷ cs)    = dropSpace cs in
-    let (d, (_ ∷ cs)) = splitWhile (notp ((==) '>')) (dropSpace cs) in
-    let ('0' ∷ cs)    = dropSpace cs in
-      `Plane (foil a, foil b, foil c, foil d)
+  let isSpace = function
+    | ' '  → true
+    | '\t' → true
+    | '\n' → true
+    | '\r' → true
+    | _    → false
 
--- Is the point above the plane?  (i.e., in the semi-space)
-let isPointAbovePlane { x, y, z } (`Plane(a, b, c, d)) =
-  a *. x +. b *. y +. c *. z +. d >. 0.0
+  let dropSpace = compose snd (splitWhile isSpace)
 
--- Does the line segment between the two points intersect the plane,
--- and if so, where?
-let intersect p1 p2 (`Plane(a, b, c, d) as plane) =
- if isPointAbovePlane p1 plane == isPointAbovePlane p2 plane
-   then None
-   else let t = (a *. p1.x +. b *. p1.y +. c *. p1.z +. d) /.
-                (a *. (p1.x -. p2.x) +.
-                 b *. (p1.y -. p2.y) +.
-                 c *. (p1.z -. p2.z)) in
-        let x = p1.x +. (p2.x -. p1.x) *. t in
-        let y = p1.y +. (p2.y -. p1.y) *. t in
-        let z = p1.z +. (p2.z -. p1.z) *. t in
-          Some { x, y, z }
+  let point_of_string s =
+    let foil = compose float_of_string implode in
+      let cs = explode s in
+      let ('(' ∷ cs) = dropSpace cs in
+      let (x, (_ ∷ cs)) = splitWhile (notp ((==) ',')) (dropSpace cs) in
+      let (y, (_ ∷ cs)) = splitWhile (notp ((==) ',')) (dropSpace cs) in
+      let (z, (_ ∷ cs)) = splitWhile (notp ((==) ')')) (dropSpace cs) in
+        { x = foil x, y = foil y, z = foil z }
 
---
--- In sublanguage A, our protocol is to send an unbounded
--- sequence of points:
---
+  let plane_of_string s =
+    let foil = compose float_of_string implode in
+      let cs = explode s in
+      let (a, (_ ∷ cs)) = splitWhile (notp ((==) 'x')) (dropSpace cs) in
+      let ('+' ∷ cs)    = dropSpace cs in
+      let (b, (_ ∷ cs)) = splitWhile (notp ((==) 'y')) (dropSpace cs) in
+      let ('+' ∷ cs)    = dropSpace cs in
+      let (c, (_ ∷ cs)) = splitWhile (notp ((==) 'z')) (dropSpace cs) in
+      let ('+' ∷ cs)    = dropSpace cs in
+      let (d, (_ ∷ cs)) = splitWhile (notp ((==) '>')) (dropSpace cs) in
+      let ('0' ∷ cs)    = dropSpace cs in
+        { a = foil a, b = foil b, c = foil c, d = foil d }
 
-type 'a stream = mu 'x. 1 |&| ?'a; 'x
+  let isPointAbovePlane { x, y, z } { a, b, c, d } =
+    a *. x +. b *. y +. c *. z +. d >. 0.0
 
---
--- Each transducer takes a plane to clip by, and two rendezvous objects,
--- the first on which it expects to receive points, and the second on
--- which it will send points.
---
+  let intersect (p1, p2) ({ a, b, c, d } as plane) =
+   if isPointAbovePlane p1 plane == isPointAbovePlane p2 plane
+     then None
+     else let t = (a *. p1.x +. b *. p1.y +. c *. p1.z +. d) /.
+                  (a *. (p1.x -. p2.x) +.
+                   b *. (p1.y -. p2.y) +.
+                   c *. (p1.z -. p2.z)) in
+          let x = p1.x +. (p2.x -. p1.x) *. t in
+          let y = p1.y +. (p2.y -. p1.y) *. t in
+          let z = p1.z +. (p2.z -. p1.z) *. t in
+            Some { x, y, z }
+end
 
+open Geometry
+
+(*
+Our protocol is to send an unbounded sequence of points:
+*)
+type `a stream = mu 's. 1 |&| ?`a; 's
+
+(*
+Each transducer takes a plane to clip by, and two rendezvous objects,
+the first on which it expects to receive points, and the second on
+which it will send points.
+*)
+
 let clipper (plane: plane)
-               (ic: point stream channel)
-               (oc: point stream dual channel): unit =
+            (ic: point stream channel)
+            (oc: point stream dual channel) =
        let finish (oc: point stream dual channel) =
              sel1 oc; () in
-       let put (oc: point stream dual channel) (pt: point) =
-             send (sel2 oc) pt in
-       let putCross (oc: point stream dual channel)
-                    (p1: point) (p2: point) =
-             match intersect p1 p2 plane with
-             | Some pt -> put oc pt
-             | None    -> oc in
-       let putVisible (oc: point stream dual channel)
-                      (pt: point) =
+       let put pt (oc: point stream dual channel) =
+             send pt (sel2 oc) in
+       let putCross p1 p2 (oc: point stream dual channel) =
+             match intersect (p1, p2) plane with
+             | Some pt → put pt oc
+             | None    → oc in
+       let putVisible pt (oc: point stream dual channel) =
              if isPointAbovePlane pt plane
-               then put oc pt
+               then put pt oc
                else oc in
          match follow ic with
-         | Left _   -> finish oc
-         | Right ic ->
+         | Left _   → finish oc
+         | Right ic →
              let (pt0, ic) = recv ic in
-             let rec loop (ic: point stream channel)
-                          (oc: point stream dual channel)
-                          (pt: point) : unit =
-                       let oc = putVisible oc pt in
+             let rec loop pt
+                          (ic: point stream channel)
+                          (oc: point stream dual channel) =
+                       let oc = putVisible pt oc in
                          match follow ic with
-                         | Left _   -> let oc = putCross oc pt pt0 in
+                         | Left _   → let oc = putCross pt pt0 oc in
                                          finish oc
-                         | Right ic -> let (pt', ic) = recv ic in
-                                       let oc = putCross oc pt pt' in
-                                         loop ic oc pt'
-               in loop ic oc pt0
+                         | Right ic → let (pt', ic) = recv ic in
+                                       let oc = putCross pt pt' oc in
+                                         loop pt' ic oc
+               in loop pt0 ic oc
 
-let printer : point stream channel -> unit =
-  let rec loop (ic: point stream channel): unit =
-            match follow ic with
-            | Left _   -> ()
-            | Right ic -> let (pt, ic) = recv ic in
-                            putStrLn (string_of_point pt);
-                            loop ic
-   in loop
+let rec printer ic =
+  match follow ic with
+  | Left _   → ()
+  | Right ic → let (pt, ic) = recv ic in
+      putStrLn (string_of_point pt);
+      printer ic
 
 -- The main protocol for the program, which lets us split our parser
 -- from our main loop.
-type main_prot = mu 'x. point stream |&| ?plane; 'x
+type main_prot = mu 's. point stream |&| ?plane; 's
 
-let parser : main_prot dual channel -> unit =
-  let rec plane_loop (oc: main_prot dual channel): unit =
+let parser =
+  let rec plane_loop (oc: main_prot dual channel) =
             match getLine () with
-            | "" -> point_loop (sel1 oc)
-            | s  -> let plane = parsePlane s in
-                    let oc    = send (sel2 oc) plane in
+            | "" → point_loop (sel1 oc)
+            | s  → let plane = plane_of_string s in
+                    let oc    = send plane (sel2 oc) in
                       plane_loop oc
-      and point_loop (oc: point stream dual channel): unit =
+      and point_loop (oc: point stream dual channel) =
             match getLine () with
-            | "" -> sel1 oc; ()
-            | s  -> let point = parsePoint s in
-                    let oc    = send (sel2 oc) point in
+            | "" → sel1 oc; ()
+            | s  → let point = point_of_string s in
+                    let oc    = send point (sel2 oc) in
                       point_loop oc
    in plane_loop
 
-let main : unit -> unit =
-  let rec get_planes (acc: plane list) (ic: main_prot channel)
-                     : plane list * point stream channel =
+let main () =
+  let rec get_planes (acc : plane list) (ic: main_prot channel) =
             match follow ic with
-            | Left ic  -> (rev acc, ic)
-            | Right ic -> let (plane, ic) = recv ic in
+            | Left ic  → (rev acc, ic)
+            | Right ic → let (plane, ic) = recv ic in
                             get_planes (plane ∷ acc) ic in
-  let rec connect (planes: plane list)
-                  (ic: point stream channel)
-                  : point stream channel =
+  let rec connect planes (ic : point stream channel) =
             match planes with
-            | []              -> ic
-            | plane ∷ rest ->
-                let outrv : point stream rendezvous = newRendezvous () in
-                  AThread.fork (fun () ->
-                    clipper plane ic (accept outrv));
+            | []           → ic
+            | plane ∷ rest →
+                let outrv = newRendezvous () in
+                  AThread.fork (λ _ → clipper plane ic (accept outrv));
                   connect rest (request outrv) in
-  fun () ->
-    let rv           = newRendezvous () : main_prot rendezvous in
-    let _            = AThread.fork (fun () -> parser (accept rv)) in
-    let (planes, ic) = get_planes [] (request rv) in
-    let ic           = connect planes ic in
-      printer ic
+  let rv           = newRendezvous () in
+  AThread.fork (λ _ → parser (accept rv));
+  let (planes, ic) = get_planes [] (request rv) in
+    printer (connect planes ic)
 
 in
   main ()
diff --git a/examples/session-types-polygons2.alms b/examples/session-types-polygons2.alms
--- a/examples/session-types-polygons2.alms
+++ b/examples/session-types-polygons2.alms
@@ -1,144 +1,156 @@
--- Sutherland-Hodgman (1974) re-entrant polygon clipping
+(* Sutherland-Hodgman (1974) re-entrant polygon clipping *)
 
-#load "libthread"
 #load "libsessiontype2"
 
 open SessionType
 
---
--- We first build a 3-D geometry library in sublanguage C:
---
+(*
+We first build a tiny 3-D geometry library
+*)
+module type GEOMETRY = sig
+  (* Points, planes, and line segments in R³ *)
+  type point   = { x, y, z : float }
+  type plane   = { a, b, c, d : float }
+  type segment = point × point
 
--- Points and planes in R^3.
-type point = Point of float * float * float
-type plane = Plane of float * float * float * float
+  (*
+    The plane { a, b, c, d } represents the open half-space
+    { (x, y, z) | ax + by + cz + d > 0 }
+  *)
 
--- We use the plane Plane(a, b, c, d) to represent the open half-space
--- { Point(x, y, z) | ax + by + cz + d > 0 }
+  val string_of_point : point → string
+  val string_of_plane : plane → string
 
-let string_of_point (Point(x, y, z)) =
-    "(" ^ string_of x ^ ", " ^ string_of y ^ ", " ^ string_of z ^ ")"
+  val point_of_string : string → point
+  val plane_of_string : string → plane
 
-let string_of_plane (Plane(a, b, c, d)) =
-    string_of a ^ "x + " ^ string_of b ^ "y + " ^
-    string_of c ^ "z + " ^ string_of d ^ " > 0"
+  (* Is the point above the plane?  (i.e., in the semi-space) *)
+  val is_point_above_plane         : point → plane → bool
 
-let splitWhile : ('a -> bool) -> 'a list -> 'a list * 'a list
-  = fun pred ->
-      let rec loop (acc: 'a list) (xs: 'a list) : 'a list * 'a list =
-                match xs with
-                | []     -> (rev acc, [])
-                | x ∷ xs' -> if pred x
-                               then loop (x ∷ acc) xs'
-                               else (rev acc, xs)
-       in loop []
+  (* Does the line segment between the two points intersect the plane,
+     and if so, where? *)
+  val intersect       : segment → plane → point option
+end
 
-let notp (pred: 'a -> bool) (x: 'a) = not (pred x)
+module Geometry : GEOMETRY = struct
+  type point   = { x, y, z : float }
+  type plane   = { a, b, c, d : float }
+  type segment = point × point
 
-let isSpace c =
-  match c with
-  | ' '  -> true
-  | '\t' -> true
-  | '\n' -> true
-  | '\r' -> true
-  | _    -> false
+  let string_of_point p =
+      "(" ^ string_of p.x ^ ", " ^ string_of p.y ^ ", " ^ string_of p.z ^ ")"
 
-let dropSpace cs = snd (splitWhile isSpace cs)
+  let string_of_plane {a, b, c, d} =
+      string_of a ^ "x + " ^ string_of b ^ "y + " ^
+      string_of c ^ "z + " ^ string_of d ^ " > 0"
 
-let parsePoint (s : string) : point =
-  let foil (x: char list) = float_of_string (implode x) in
-    let cs = explode s in
-    let '(' ∷ cs = dropSpace cs in
-    let (x, _ ∷ cs) = splitWhile (notp ((==) ',')) (dropSpace cs) in
-    let (y, _ ∷ cs) = splitWhile (notp ((==) ',')) (dropSpace cs) in
-    let (z, _ ∷ cs) = splitWhile (notp ((==) ')')) (dropSpace cs) in
-      Point (foil x, foil y, foil z)
+  (* Some of this should be in the library! *)
+  let splitWhile pred =
+    let rec loop acc xs =
+              match xs with
+              | []      → (rev acc, [])
+              | x ∷ xs' → if pred x
+                            then loop (x ∷ acc) xs'
+                            else (rev acc, xs)
+     in loop []
 
-let parsePlane (s: string) : plane =
-  let foil (x: char list) = float_of_string (implode x) in
-    let cs = explode s in
-    let (a, _ ∷ cs) = splitWhile (notp ((==) 'x')) (dropSpace cs) in
-    let '+' ∷ cs    = dropSpace cs in
-    let (b, _ ∷ cs) = splitWhile (notp ((==) 'y')) (dropSpace cs) in
-    let '+' ∷ cs    = dropSpace cs in
-    let (c, _ ∷ cs) = splitWhile (notp ((==) 'z')) (dropSpace cs) in
-    let '+' ∷ cs    = dropSpace cs in
-    let (d, _ ∷ cs) = splitWhile (notp ((==) '>')) (dropSpace cs) in
-    let '0' ∷ cs    = dropSpace cs in
-      Plane (foil a, foil b, foil c, foil d)
+  let notp = compose not
 
--- Is the point above the plane?  (i.e., in the semi-space)
-let isPointAbovePlane (Point(x, y, z): point)
-                         (Plane(a, b, c, d): plane): bool =
-  a *. x +. b *. y +. c *. z +. d >. 0.0
+  let isSpace = function
+    | ' '  → true
+    | '\t' → true
+    | '\n' → true
+    | '\r' → true
+    | _    → false
 
--- Does the line segment between the two points intersect the plane,
--- and if so, where?
-let intersect (Point(x1, y1, z1) as p1 : point)
-              (Point(x2, y2, z2) as p2 : point)
-              (Plane(a, b, c, d) as plane : plane): point option =
- if isPointAbovePlane p1 plane == isPointAbovePlane p2 plane
-   then None
-   else let t = (a *. x1 +. b *. y1 +. c *. z1 +. d) /.
-                (a *. (x1 -. x2) +.
-                 b *. (y1 -. y2) +.
-                 c *. (z1 -. z2)) in
-        let x = x1 +. (x2 -. x1) *. t in
-        let y = y1 +. (y2 -. y1) *. t in
-        let z = z1 +. (z2 -. z1) *. t in
-          Some (Point (x, y, z))
+  let dropSpace = compose snd (splitWhile isSpace)
 
---
--- In sublanguage A, our protocol is to send an unbounded
--- sequence of points:
---
+  let point_of_string s =
+    let foil = compose float_of_string implode in
+      let cs = explode s in
+      let ('(' ∷ cs) = dropSpace cs in
+      let (x, (_ ∷ cs)) = splitWhile (notp ((==) ',')) (dropSpace cs) in
+      let (y, (_ ∷ cs)) = splitWhile (notp ((==) ',')) (dropSpace cs) in
+      let (z, (_ ∷ cs)) = splitWhile (notp ((==) ')')) (dropSpace cs) in
+        { x = foil x, y = foil y, z = foil z }
 
-type 'a stream = ?->('a step)
- and 'a step   = Done of 1 channel
-               | Next of (?'a; 'a stream) channel
+  let plane_of_string s =
+    let foil = compose float_of_string implode in
+      let cs = explode s in
+      let (a, (_ ∷ cs)) = splitWhile (notp ((==) 'x')) (dropSpace cs) in
+      let ('+' ∷ cs)    = dropSpace cs in
+      let (b, (_ ∷ cs)) = splitWhile (notp ((==) 'y')) (dropSpace cs) in
+      let ('+' ∷ cs)    = dropSpace cs in
+      let (c, (_ ∷ cs)) = splitWhile (notp ((==) 'z')) (dropSpace cs) in
+      let ('+' ∷ cs)    = dropSpace cs in
+      let (d, (_ ∷ cs)) = splitWhile (notp ((==) '>')) (dropSpace cs) in
+      let ('0' ∷ cs)    = dropSpace cs in
+        { a = foil a, b = foil b, c = foil c, d = foil d }
 
---
--- Each transducer takes a plane to clip by, and two rendezvous objects,
--- the first on which it expects to receive points, and the second on
--- which it will send points.
---
+  let is_point_above_plane { x, y, z } { a, b, c, d } =
+    a *. x +. b *. y +. c *. z +. d >. 0.0
 
+  let intersect (p₁, p₂) ({ a, b, c, d } as plane) =
+   if is_point_above_plane p₁ plane == is_point_above_plane p₂ plane
+     then None
+     else let t = (a *. p₁.x +. b *. p₁.y +. c *. p₁.z +. d) /.
+                  (a *. (p₁.x -. p₂.x) +.
+                   b *. (p₁.y -. p₂.y) +.
+                   c *. (p₁.z -. p₂.z)) in
+          let x = p₁.x +. (p₂.x -. p₁.x) *. t in
+          let y = p₁.y +. (p₂.y -. p₁.y) *. t in
+          let z = p₁.z +. (p₂.z -. p₁.z) *. t in
+            Some { x, y, z }
+end
+
+open Geometry
+
+(* The protocol *)
+type `a stream = ?->(`a step)
+ and `a step   = Done of 1 channel
+               | Next of (?`a; `a stream) channel
+
+(*
+  Each transducer takes a plane to clip by and two rendezvous objects,
+  the first on which it expects to receive points, and the second on
+  which it will send points.
+*)
+
 let clipper plane
             !(ic: point stream channel, oc: point stream dual channel) =
-  let finish () =
-    choose Done oc in
-  let put pt =
-    choose Next oc;
-    send pt oc in
-  let putCross p1 p2 =
-    match intersect p1 p2 plane with
-    | Some pt -> put pt
-    | None    -> () in
-  let putVisible pt =
-    if isPointAbovePlane pt plane
-      then put pt
+  let finish () = choose Done oc in
+  let put p     = choose Next oc; send p oc in
+  let putCross p₁ p₂ =
+    match intersect (p₁, p₂) plane with
+    | Some p  → put p
+    | None    → () in
+  let putVisible p =
+    if is_point_above_plane p plane
+      then put p
       else ()
-   in follow ic;
-      match ic with
-      | Done ic -> finish ()
-      | Next ic ->
-        let pt0 = recv ic in
-        let rec loop pt =
-          putVisible pt;
-          follow ic;
-          match ic with
-          | Done ic -> putCross pt pt0;
-                       finish ()
-          | Next ic -> let pt' = recv ic in
-                       putCross pt pt';
-                       loop pt'
-         in loop pt0
+  in follow ic;
+     match ic with
+     | Done ic → finish ()
+     | Next ic →
+       let p₀ = recv ic in
+       let rec loop p =
+         putVisible p;
+         follow ic;
+         match ic with
+         | Done ic →
+             putCross p p₀;
+             finish ()
+         | Next ic →
+             let p′ = recv ic in
+               putCross p p′;
+               loop p′
+       in loop p₀
 
 let rec printer !(ic: point stream channel) =
   follow ic;
   match ic with
-  | Done ic -> ()
-  | Next ic -> putStrLn (string_of_point (recv ic));
+  | Done ic → ()
+  | Next ic → putStrLn (string_of_point (recv ic));
                printer ic
 
 -- The main protocol for the program, which lets us split our parser
@@ -147,44 +159,37 @@
     and main2     = Planes of (?plane; main_prot) channel
                   | Points of point stream channel
 
-let parser (!oc: main_prot dual channel) =
+let parser !(oc: main_prot dual channel) =
   let rec plane_loop () =
             match getLine () with
-            | "" -> choose Points oc;
+            | "" → choose Points oc;
                     point_loop ()
-            | s  -> choose Planes oc;
-                    send (parsePlane s) oc;
+            | s  → choose Planes oc;
+                    send (plane_of_string s) oc;
                     plane_loop ()
       and point_loop () =
             match getLine () with
-            | "" -> choose Done oc
-            | s  -> choose Next oc;
-                    send (parsePoint s) oc;
+            | "" → choose Done oc
+            | s  → choose Next oc;
+                    send (point_of_string s) oc;
                     point_loop ()
    in plane_loop ()
 
-let main =
+let main () =
   let rec get_planes (acc: plane list) !(ic: main_prot channel) =
             follow ic;
             match ic with
-            | Points ic -> rev acc
-            | Planes ic -> get_planes (recv ic ∷ acc) ic in
-  let rec connect (planes: plane list)
-                  (ic: point stream channel)
-                  : point stream channel =
-            match planes with
-            | []              -> ic
-            | plane ∷ rest ->
-                let outrv = newRendezvous () in
-                  AThread.fork
-                    (fun () -> clipper plane (ic, accept outrv); ());
-                  connect rest (request outrv) in
-  fun () ->
-    let rv           = newRendezvous () in
-    let _            = AThread.fork (fun () -> parser (accept rv); ()) in
-    let (planes, ic) = get_planes [] (request rv) in
-    let ic           = connect planes ic in
-      printer ic
+            | Points ic → rev acc
+            | Planes ic → get_planes (recv ic ∷ acc) ic in
+  let connect plane (ic : point stream channel) =
+        let outrv = newRendezvous () in
+          Thread.fork (λ_ → clipper plane (ic, accept outrv); ());
+          request outrv in
+  let rv           = newRendezvous () in
+  let _            = Thread.fork (λ_ → parser (accept rv); ()) in
+  let (planes, ic) = get_planes [] (request rv) in
+  let ic           = foldl connect ic planes
+  in
+    printer ic
 
-in
-  main ()
+in main ()
diff --git a/lib/libbasis.alms b/lib/libbasis.alms
--- a/lib/libbasis.alms
+++ b/lib/libbasis.alms
@@ -96,6 +96,10 @@
   let uncurry f (x, y) = f x y
   let compose f g x    = f (g x)
   let ($) f x          = f x
+
+  (* Useful for implicit threading syntax: *)
+  let ($>) f x         = ((), f x)
+  let ($<) f x         = (f x, ())
 end
 
 open Function
diff --git a/lib/libsessiontype.alms b/lib/libsessiontype.alms
--- a/lib/libsessiontype.alms
+++ b/lib/libsessiontype.alms
@@ -19,16 +19,16 @@
   type 's rendezvous
   type +'s channel qualifier A
 
-  val newRendezvous : all 's. unit -> 's rendezvous
+  val newRendezvous : unit → 's rendezvous
 
-  val request   : all 's. 's rendezvous -> 's channel
-  val accept    : all 's. 's rendezvous -> 's dual channel
+  val request   : 's rendezvous → 's channel
+  val accept    : 's rendezvous → 's dual channel
 
-  val send      : all `a 's. (!`a; 's) channel -> `a -o 's channel
-  val recv      : all `a 's. (?`a; 's) channel -> `a * 's channel
-  val sel1      : all 's 'r. ('s |+| 'r) channel -> 's channel
-  val sel2      : all 's 'r. ('s |+| 'r) channel -> 'r channel
-  val follow    : all 's 'r. ('s |&| 'r) channel -> 's channel + 'r channel
+  val send      : `a → (!`a; 's) channel → 's channel
+  val recv      : (?`a; 's) channel → `a * 's channel
+  val sel1      : ('s |+| 'r) channel → 's channel
+  val sel2      : ('s |+| 'r) channel → 'r channel
+  val follow    : ('s |&| 'r) channel → 's channel + 'r channel
 end
 
 module SessionType : SESSION_TYPE = struct
@@ -47,36 +47,27 @@
      | ('a |+| 'b) dual = 'a dual |&| 'b dual
      | ('a |&| 'b) dual = 'a dual |+| 'b dual
 
-  type rep           = bool C.channel
-  type 's channel    = rep
-  type 's rendezvous = rep C.channel
+  type 's channel    = bool C.channel
+  type 's rendezvous = 's channel C.channel
 
-  let newRendezvous () = C.new ()
+  let newRendezvous = C.new
 
-  let request (r: 's rendezvous) = C.recv r
+  let request = C.recv
 
-  let accept (r: 's rendezvous) =
+  let accept rv =
     let c = C.new () in
-      C.send r c;
+      C.send rv c;
       c
 
-  let send (c: rep) (a: `a) =
-    C.send c (Unsafe.unsafeCoerce a);
-    c
+  let send a c = C.send (Unsafe.unsafeCoerce c) a; c
 
-  let recv (c: rep) =
-    (Unsafe.unsafeCoerce (C.recv c),  c)
+  let recv c = (C.recv (Unsafe.unsafeCoerce c), c)
 
-  let sel1 (c: ('s1 |+| 's2) channel)
-                     : 's1 channel =
-    C.send c true;
-    c
+  let sel1 c = C.send c true; c
 
-  let sel2 (c: rep) =
-    C.send c false;
-    c
+  let sel2 c = C.send c false; c
 
-  let follow (c: rep) =
+  let follow c =
     if C.recv c
       then Left  c
       else Right c
diff --git a/lib/libsessiontype2.alms b/lib/libsessiontype2.alms
--- a/lib/libsessiontype2.alms
+++ b/lib/libsessiontype2.alms
@@ -27,7 +27,7 @@
   val recv      : (?`a; 's) channel → `a * 's channel
 
   val follow    : ?-> `c channel → unit * `c
-  val choose    : ('s channel → `c) → !-> `c channel →
+  val choose    : ('s channel -A> `c) → !-> `c channel →
                     unit * 's dual channel
 end
 
@@ -46,36 +46,23 @@
   type ?-> `c = ?`c; 1
   type !-> `c = !`c; 1
 
-  type rep = int C.channel
-  type 's channel    = rep
-  type 's rendezvous = rep C.channel
+  type 's channel    = bool C.channel
+  type 's rendezvous = 's channel C.channel
 
-  let newRendezvous () = C.new ()
+  let newRendezvous = C.new
 
-  let request (r: unit rendezvous) = C.recv r
+  let request = C.recv
 
-  let accept (r: unit rendezvous) =
+  let accept rv =
     let c = C.new () in
-      C.send r c;
+      C.send rv c;
       c
 
-  let newPair () =
-    let c = C.new () in
-      (c, c)
-
-  let send (a: `a) (c: rep) =
-    C.send c (Unsafe.unsafeCoerce a);
-    ((), c)
-
-  let recv (c: rep) = (Unsafe.unsafeCoerce (C.recv c), c)
-
-  let follow (c: rep) =
-    let (c', _) = recv c in ((), c')
+  let send a c      = (C.send (Unsafe.unsafeCoerce c) a, c)
+  let recv c        = (C.recv (Unsafe.unsafeCoerce c), c)
 
-  let choose (ctor: rep → `c) (c: rep) =
-    let (theirs, mine) = newPair () in
-      send (ctor theirs) c;
-      ((), mine)
+  let follow c      = ((), fst (recv c))
+  let choose ctor c = send (ctor c) c
 end
 
 module SessionType2Test = struct
diff --git a/src/AST/Expr.hs b/src/AST/Expr.hs
--- a/src/AST/Expr.hs
+++ b/src/AST/Expr.hs
@@ -19,7 +19,7 @@
   -- ** Synthetic expression constructors
   exBVar, exBCon,
   exChar, exStr, exInt, exFloat,
-  exSeq,
+  exSeq, exIfThenElse, exOr, exAnd,
   exUnit, exNilRecord,
   exNil, exCons,
   ToExpr(..),
@@ -300,6 +300,16 @@
 
 exSeq :: Tag i => Expr i -> Expr i -> Expr i
 exSeq e1 e2 = exLet paWild e1 e2
+
+exIfThenElse :: Tag i => Expr i -> Expr i -> Expr i -> Expr i
+exIfThenElse ec et ef =
+  exCase ec
+    [ caClause (paCon idTrueValue Nothing) et
+    , caClause (paCon idFalseValue Nothing) ef ]
+
+exOr, exAnd :: Tag i => Expr i -> Expr i -> Expr i
+exOr e1 e2  = exIfThenElse e1 (exCon idTrueValue Nothing) e2
+exAnd e1 e2 = exIfThenElse e1 e2 (exCon idFalseValue Nothing)
 
 exUnit, exNilRecord :: Tag i => Expr i
 exUnit      = exCon idUnitVal Nothing
diff --git a/src/Alt/PrettyPrint.hs b/src/Alt/PrettyPrint.hs
--- a/src/Alt/PrettyPrint.hs
+++ b/src/Alt/PrettyPrint.hs
@@ -30,7 +30,7 @@
 
 import qualified Text.PrettyPrint as P
 import Control.Applicative
-import Data.Monoid
+import Data.Monoid hiding ((<>))
 
 -- Document parameterized by type @e@.
 newtype Doc e = Doc { unDoc :: e -> P.Doc }
diff --git a/src/Basis.hs b/src/Basis.hs
--- a/src/Basis.hs
+++ b/src/Basis.hs
@@ -21,7 +21,7 @@
 import qualified Basis.Array
 import qualified Basis.Row
 
-import qualified IO
+import qualified System.IO as IO
 import qualified System.Environment as Env
 import Data.IORef (IORef, newIORef, readIORef, atomicModifyIORef)
 import System.Random (randomIO)
diff --git a/src/Basis/Channel.hs b/src/Basis/Channel.hs
--- a/src/Basis/Channel.hs
+++ b/src/Basis/Channel.hs
@@ -18,13 +18,13 @@
 
 entries :: [Entry Raw]
 entries  = [
-    dec [sgQ| type 'a channel |],
-    fun "new"  -: [ty| all 'a. unit -> 'a channel |]
+    dec [sgQ| type `a channel |],
+    fun "new"  -: [ty| all `a. unit -> `a channel |]
         -= \() -> Channel `fmap` C.newChan,
-    fun "send" -: [ty| all 'a. 'a channel -> 'a -> unit |]
+    fun "send" -: [ty| all `a. `a channel -> `a -> unit |]
         -= \c a -> do
              C.writeChan (unChannel c) a
              return (),
-    fun "recv" -: [ty| all 'a. 'a channel -> 'a |]
+    fun "recv" -: [ty| all `a. `a channel -> `a |]
         -= \c -> C.readChan (unChannel c)
   ]
diff --git a/src/Basis/IO.hs b/src/Basis/IO.hs
--- a/src/Basis/IO.hs
+++ b/src/Basis/IO.hs
@@ -6,7 +6,7 @@
 import Util
 import Value (Valuable(..), vinjData, vprjDataM)
 
-import qualified IO
+import qualified System.IO as IO
 import Data.Data (Typeable, Data)
 
 instance Valuable IO.Handle where
diff --git a/src/Basis/Thread.hs b/src/Basis/Thread.hs
--- a/src/Basis/Thread.hs
+++ b/src/Basis/Thread.hs
@@ -12,7 +12,7 @@
 entries =  [
     -- Threads
     dec [sgQ| type thread |],
-    fun "fork"  -: [ty| (unit -> unit) -> thread |]
+    fun "fork"  -: [ty| (unit -A> unit) -> thread |]
       -= \f -> Vinj `fmap` CC.forkIO (vapp f () >> return ()),
     fun "kill"  -: [ty| thread -> unit |]
       -= CC.killThread . unVinj,
diff --git a/src/Env.hs b/src/Env.hs
--- a/src/Env.hs
+++ b/src/Env.hs
@@ -36,7 +36,6 @@
 import qualified Data.Map as M
 import qualified Data.Set as S
 import Data.Generics (Typeable, Data)
-import Data.Monoid
 
 infix 6 -:-, -::-, -:+-
 infixl 6 -.-
diff --git a/src/Error.hs b/src/Error.hs
--- a/src/Error.hs
+++ b/src/Error.hs
@@ -28,14 +28,12 @@
 
 import Prelude ()
 import Data.Typeable (Typeable)
-import Control.Applicative
 import Control.Exception (Exception, throwIO, throw, catch)
 
 import qualified Control.Monad.Cont as Cont
 import qualified Control.Monad.Trans.Identity as Identity
 import qualified Control.Monad.Trans.Maybe as Maybe
 import qualified Control.Monad.Trans.List as List
-import qualified Control.Monad.Error as Error
 import qualified Control.Monad.Trans.Reader as Reader
 import qualified Control.Monad.Trans.RWS.Strict as StrictRWS
 import qualified Control.Monad.Trans.RWS.Lazy   as LazyRWS
diff --git a/src/Main.hs b/src/Main.hs
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -36,8 +36,8 @@
 import Data.IORef (IORef)
 import System.Exit (exitFailure, exitSuccess, ExitCode)
 import System.Environment (getArgs, getProgName, withProgName, withArgs)
-import System.IO.Error (ioeGetErrorString, isUserError)
-import IO (hPutStrLn, hFlush, stdout, stderr)
+import System.IO.Error (ioeGetErrorString, isUserError, catchIOError)
+import System.IO (hPutStrLn, hFlush, stdout, stderr)
 import qualified Control.Exception as Exn
 
 #ifdef USE_READLINE
@@ -195,7 +195,7 @@
   repl 1 rs0
   where
     repl row st = do
-      mres <- reader row st
+      mres <- readr row st
       case mres of
         Nothing  -> return ()
         Just (row', ast) -> do
@@ -213,8 +213,8 @@
     say    = if opt Quiet then const (return ()) else printDoc
     getln' = if opt NoLineEdit then getline else readline
     getln  = if opt Quiet then const (getln' "") else getln'
-    reader :: Int -> ReplState -> IO (Maybe (Int, [Decl Raw]))
-    reader row st = loop 1 []
+    readr :: Int -> ReplState -> IO (Maybe (Int, [Decl Raw]))
+    readr row st = loop 1 []
       where
         fixup = unlines . mapTail ("   " ++) . reverse
         loop count acc = do
@@ -225,7 +225,7 @@
               addHistory (fixup (map fst acc))
               hPutStrLn stderr ""
               hPutStrLn stderr (show err)
-              reader (row + count) st
+              readr (row + count) st
             (Just line, _)
               | all isSpace line -> loop count acc
               | otherwise        ->
@@ -383,4 +383,4 @@
 getline s   = do
   putStr s
   hFlush stdout
-  catch (fmap Just getLine) (\_ -> return Nothing)
+  catchIOError (fmap Just getLine) (\_ -> return Nothing)
diff --git a/src/Paths.hs b/src/Paths.hs
--- a/src/Paths.hs
+++ b/src/Paths.hs
@@ -12,6 +12,7 @@
 import System.FilePath
 import System.Directory (doesFileExist, getCurrentDirectory)
 import System.Environment (getEnv)
+import System.IO.Error (catchIOError)
 import Data.Version
 
 #ifdef ALMS_CABAL_BUILD
@@ -22,7 +23,7 @@
 builddir   = $(runIO getCurrentDirectory >>= litE . stringL)
 
 getBuildDir :: IO FilePath
-getBuildDir  = catch (getEnv "alms_builddir") (\_ -> return builddir)
+getBuildDir  = catchIOError (getEnv "alms_builddir") (\_ -> return builddir)
 
 #ifndef ALMS_CABAL_BUILD
 version :: Version
@@ -34,8 +35,8 @@
 datadir    = dropFileName builddir
 
 getBinDir, getDataDir :: IO FilePath
-getBinDir  = catch (getEnv "alms_bindir") (\_ -> return bindir)
-getDataDir = catch (getEnv "alms_datadir") (\_ -> return datadir)
+getBinDir  = catchIOError (getEnv "alms_bindir") (\_ -> return bindir)
+getDataDir = catchIOError (getEnv "alms_datadir") (\_ -> return datadir)
 
 getDataFileName :: FilePath -> IO FilePath
 getDataFileName name = do
@@ -62,7 +63,7 @@
 almsLibPath :: IO [FilePath]
 almsLibPath = do
   user   <- liftM splitSearchPath (getEnv "ALMS_LIB_PATH")
-             `catch` \_ -> return []
+             `catchIOError` \_ -> return []
   system <- liftM (</> "lib") getDataDir
   build  <- liftM (</> "lib") getBuildDir
   return $ user ++ [ system, build ]
diff --git a/src/Statics/Rename.hs b/src/Statics/Rename.hs
--- a/src/Statics/Rename.hs
+++ b/src/Statics/Rename.hs
@@ -19,7 +19,6 @@
 import AST hiding ((&))
 import Data.Loc
 import AST.TypeAnnotation
-import qualified AST.Notable
 import Util
 import Syntax.Ppr (Ppr(..))
 
diff --git a/src/Statics/Sealing.hs b/src/Statics/Sealing.hs
--- a/src/Statics/Sealing.hs
+++ b/src/Statics/Sealing.hs
@@ -248,7 +248,8 @@
     tcGuards tc1 ==! tcGuards tc2       $ "guarded parameters"
     tcQual tc1   ==! tcQual tc2         $ "qualifier"
   (DataType, DataType) → do
-    tcArity tc1  ==! tcArity tc2        $ "number of parameters"
+    length (tcArity tc1)  ==! length (tcArity tc2)
+                                        $ "number of parameters"
     let rhs1 = tcCons tc1
         rhs2 = tcCons tc2
     forM_ (Env.toList rhs1) $ \(k, mσ1) → do
@@ -277,8 +278,9 @@
   where
     (a1 ==! a2) what =
       tAssExp (a1 == a2)
-        [msg| In signature matching, cannot match definition for type
-              $q:tc1 because the $words:what does not match: |]
+        ([msg| In signature matching, cannot match definition for type
+               $q:1 because the $words:what does not match: |]
+         (tcName tc1))
         (pprMsg a1)
         (pprMsg a2)
 
diff --git a/src/Syntax/Construction.hs b/src/Syntax/Construction.hs
--- a/src/Syntax/Construction.hs
+++ b/src/Syntax/Construction.hs
@@ -14,7 +14,7 @@
 import Meta.Quasi
 
 import Prelude ()
-import Data.Map as M
+import Data.Map as M hiding (foldr, foldl')
 import Data.Generics (Data, everywhere, mkT)
 
 -- | Constructs a let expression, but with a special case:
diff --git a/src/Syntax/Lexer.hs b/src/Syntax/Lexer.hs
--- a/src/Syntax/Lexer.hs
+++ b/src/Syntax/Lexer.hs
@@ -46,7 +46,7 @@
     T.identLetter    = alphaNum <|> oneOf "_'′₀₁₂₃₄₅₆₇₈₉⁰¹²³⁴⁵⁶⁷⁸⁹ᵢⱼₐₑₒₓⁱⁿ",
     T.opStart        = satisfy isOpStart <|> plusNoBrace,
     T.opLetter       = satisfy isOpLetter <|> plusNoBrace,
-    T.reservedNames  = ["fun", "λ",
+    T.reservedNames  = ["fun", "λ", "function",
                         "if", "then", "else",
                         "match", "with", "as", "_",
                         "try",
@@ -58,7 +58,8 @@
                         "all", "ex", "mu", "μ", "of",
                         "type", "qualifier" ],
     T.reservedOpNames = ["|", "=", ":", ":>", "->", "→", "⊸",
-                         "∀", "∃", "⋁", "\\/", "...", "…", "::", "∷" ],
+                         "∀", "∃", "⋁", "\\/", "...", "…", "::", "∷",
+                         "&&", "||" ],
     T.caseSensitive = True
   }
   -- 'λ' is not an identifier character, so that we can use it as
diff --git a/src/Syntax/Parser.hs b/src/Syntax/Parser.hs
--- a/src/Syntax/Parser.hs
+++ b/src/Syntax/Parser.hs
@@ -1022,7 +1022,7 @@
            reserved "then"
            caClause (paCon idTrueValue Nothing)
                 <$> exprp
-         clf <- addLoc $ do
+         clf <- option (caClause paWild exUnit) . addLoc $ do
            reserved "else"
            caClause (paCon idFalseValue Nothing)
                 <$> exprp
@@ -1061,6 +1061,11 @@
                 (exApp (exVar (qident "INTERNALS.Exn.raise"))
                        (exVar (qident "e")))
               ],
+      do reserved "function"
+         optional (reservedOp "|")
+         clauses ← flip sepBy1 (reservedOp "|") casealtp
+         return (exAbs (paVar (ident "x."))
+                       (exCase (exBVar (ident "x.")) clauses)),
       lambda *> buildargsp <* arrow <*> exprp,
       next ]
     | p == precExSemi → do
@@ -1095,6 +1100,10 @@
         return (foldr exApp arg ops)
     | p == precCom    →
         foldl1 exPair <$> commaSep1 next
+    | p == precOr     →
+        chainr1last next (exOr <$ reservedOp "||") exprp
+    | p == precAnd    →
+        chainr1last next (exAnd <$ reservedOp "&&") exprp
     | p > precMax     → choice
         [
           exVar <$> qvaridp,
diff --git a/src/Syntax/Ppr.hs b/src/Syntax/Ppr.hs
--- a/src/Syntax/Ppr.hs
+++ b/src/Syntax/Ppr.hs
@@ -382,6 +382,18 @@
     [ex| `$uid:x |]    -> char '`' <> ppr x
     [ex| `$uid:x $e |] -> prec precApp (sep [ char '`' <> ppr x, ppr1 e ])
     [ex| #$uid:x $e |] -> prec precApp (sep [ char '#' <> ppr x, ppr1 e ])
+    [ex| $e1 || $e2 |] ->
+      prec precOr $
+        sep [ ppr1 e1 <+> text "||",
+              nest 2 (ppr e2) ]
+    [ex| $e1 && $e2 |] ->
+      prec precAnd $
+        sep [ ppr1 e1 <+> text "&&",
+              nest 2 (ppr e2) ]
+    [ex| if $ec then $et |] ->
+      prec precDot $
+        sep [ text "if" <+> ppr ec,
+              nest 2 $ text "then" <+> ppr et ]
     [ex| if $ec then $et else $ef |] ->
       prec precDot $
         sep [ text "if" <+> ppr ec,
diff --git a/src/Syntax/Prec.hs b/src/Syntax/Prec.hs
--- a/src/Syntax/Prec.hs
+++ b/src/Syntax/Prec.hs
@@ -7,7 +7,7 @@
   -- * Precedences for reserved operators needed by the parser
   precMin, precStart, precMax, precCast,
   precCom, precDot, precExSemi, precTySemi, precEq, precCaret, precArr,
-  precPlus, precStar, precAt, precApp, precBang, precSel,
+  precOr, precAnd, precPlus, precStar, precAt, precApp, precBang, precSel,
 ) where
 
 import Data.Char
@@ -22,6 +22,11 @@
 precOp ('→':_)        = Right precArr
 precOp ('-':'>':_)    = Right precArr
 precOp ('-':'o':_)    = Right precArr
+precOp ('←':_)        = Right precArr
+precOp ('<':'-':_)    = Right precArr
+precOp (':':'=':_)    = Right precArr
+precOp "||"           = Right precOr
+precOp "&&"           = Right precAnd
 precOp "-[]>"         = Right precArr
 precOp (';':_)        = Right precTySemi
 precOp "⋁"            = Right precTySemi
@@ -46,6 +51,7 @@
 
 precMin, precStart, precMax, precCast,
   precCom, precDot, precExSemi, precTySemi, precEq, precCaret, precArr,
+  precOr, precAnd,
   precPlus, precStar, precAt, precApp, precSel, precBang :: Int
 precMin   = -1
 precCom   = -1 -- ,
@@ -53,17 +59,19 @@
 precDot   =  1 -- in, else, of, .
 precExSemi=  1 -- ;  (expressions only)
 precCast  =  2 -- :>
-precArr   =  3 -- ->
-precEq    =  4 -- != = < > | & $ as
-precCaret =  5 -- ^ : (infixr)
-precPlus  =  6 -- - +
-precStar  =  7 -- % / *
-precTySemi=  8 -- ; "\\/" "⋁" (types only)
-precAt    =  9 -- @ ** (infixr)
-precApp   = 10 -- f x
-precSel   = 11 -- record selection
-precBang  = 12 -- ! ~ ? (prefix)
-precMax   = 12
+precArr   =  3 -- ->… →… <-… ←… :=…
+precOr    =  4 -- ||…
+precAnd   =  5 -- & &&…
+precEq    =  6 -- !=… =… <… >… |… &… $… as…
+precPlus  =  7 -- -… +;…
+precCaret =  8 -- ^… :… ∷… (infixr)
+precStar  =  9 -- %… /… *…
+precTySemi= 10 -- ; "\\/" "⋁" (types only)
+precAt    = 11 -- @… **… (right)
+precApp   = 12 -- f x
+precSel   = 13 -- record selection
+precBang  = 14 -- !… ~… ?… (prefix)
+precMax   = 14
 
 {-# INLINE fixities #-}
 -- To find out the fixity of a precedence level
diff --git a/src/Type/Subst.hs b/src/Type/Subst.hs
--- a/src/Type/Subst.hs
+++ b/src/Type/Subst.hs
@@ -386,9 +386,9 @@
 
 -- | Run in the substitution monad
 runSubstT ∷ Monad m ⇒ SubstState → SubstT r m a → m (a, SubstState)
-runSubstT state0 (SubstT m) = do
-  (result, state, _) ← runRWST m () state0 { stsTrace = 0 }
-  return (result, state)
+runSubstT st0 (SubstT m) = do
+  (result, st, _) ← runRWST m () st0 { stsTrace = 0 }
+  return (result, st)
 
 substState0 ∷ SubstState
 substState0 = SubstState 0 0
diff --git a/src/Util.hs b/src/Util.hs
--- a/src/Util.hs
+++ b/src/Util.hs
@@ -101,7 +101,7 @@
 
 import Data.Char (chr, ord)
 import Data.Maybe
-import Data.Monoid
+import Data.Monoid hiding ((<>))
 import Data.Foldable
 import Data.Function ( on )
 import Data.Traversable
diff --git a/src/Util/MonadRef.hs b/src/Util/MonadRef.hs
--- a/src/Util/MonadRef.hs
+++ b/src/Util/MonadRef.hs
@@ -4,6 +4,7 @@
 ) where
 
 import Control.Monad.ST
+import qualified Control.Monad.ST.Unsafe as C.M.S.U
 import Control.Monad.STM
 
 import Data.IORef
@@ -58,7 +59,7 @@
   writeRef = writeSTRef
 
 instance UnsafeReadRef (STRef s) where
-  unsafeReadRef = unsafePerformIO . unsafeSTToIO . readRef
+  unsafeReadRef = unsafePerformIO . C.M.S.U.unsafeSTToIO . readRef
 
 instance MonadRef TVar STM where
   newRef   = newTVar
diff --git a/src/Util/UndoIO.hs b/src/Util/UndoIO.hs
--- a/src/Util/UndoIO.hs
+++ b/src/Util/UndoIO.hs
@@ -13,8 +13,6 @@
 import Control.Applicative
 import Control.Exception
 import Control.Monad.Error
-import Control.Monad
-import Control.Monad.Trans
 import Data.IORef
 
 -- | A layer on top of the IO monad with an undo facility.