diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index e72d2c245..6e9dd802a 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -27,6 +27,7 @@ beyond work on the language core, are (in no particular order):
     to lex!
 * An alternative, high performance, back end. OCaml seems worth a try.
 * JS and Node back ends would be nice.
+* A Jupyter kernel for Idris, to allow for more industry standard literate programming.
 
 The default Prelude describes the rationale for what gets included and what
 doesn't. Mostly what is there is copied from Idris 1, but it's not impossible
diff --git a/docs/source/reference/index.rst b/docs/source/reference/index.rst
index e84060cca..5e371b0a4 100644
--- a/docs/source/reference/index.rst
+++ b/docs/source/reference/index.rst
@@ -18,6 +18,6 @@ This is a placeholder, to get set up with readthedocs.
 
    packages
    envvars
-   postfixprojs
+   records
    literate
    overloadedlit
diff --git a/docs/source/reference/postfixprojs.rst b/docs/source/reference/postfixprojs.rst
deleted file mode 100644
index 05c485e47..000000000
--- a/docs/source/reference/postfixprojs.rst
+++ /dev/null
@@ -1,196 +0,0 @@
-Postfix projections
-===================
-
-.. role:: idris(code)
-    :language: idris
-
-Postfix projections are syntactic forms that represent postfix application,
-such as ``person.name``. They were originally motivated by the need of dot syntax
-to access fields of records, and generalised also for non-record use cases later.
-
-The more advanced features require ``%language PostfixProjections``,
-at least until it's clear whether they should be present in the language.
-
-Lexical structure
------------------
-
-* ``.foo`` starting with lowercase ``f``, single identifier, and no space after dot,
-  is a valid lexeme, which stands for postfix application of ``foo``
-
-* ``Foo.Bar.baz`` with uppercase ``F`` and ``B`` is one lexeme: a namespaced
-  identifier.
-
-* ``Foo.Bar.baz.boo`` is two lexemes: ``Foo.Bar.baz`` and ``.boo``.
-
-* ``foo.bar.baz`` starting with lowercase ``f`` is three lexemes: ``foo``,
-  ``.bar``, ``.baz``
-
-* ``.foo.bar.baz`` is three lexemes: ``.foo``, ``.bar``, ``.baz``
-
-* ``foo . bar``, as well as ``foo. bar`` is three lexemes: ``foo``, ``.``, ``bar``,
-  and represents function composition as usual
-
-* Beware that ``True.not`` is lexed as "name ``not`` in module ``True``".
-  If you want the postfix application of ``not`` to constructor ``True``,
-  you have to write ``(True).not``.
-
-* Spaces *before* dots are optional; spaces *after* dots are forbidden
-  in postfix projections: ``foo. bar`` is parsed as function composition.
-
-* All module names must start with an uppercase letter.
-
-New syntax of ``simpleExpr``
-----------------------------
-
-Expressions binding tighter than application (``simpleExpr``),
-such as variables or parenthesised expressions, have been renamed to ``simplerExpr``,
-and an extra layer of postfix dot syntax has been inserted in ``simpleExpr``.
-
-.. code-block:: idris
-
-    postfixProj ::= .ident        -- identifiers need not be bracketed
-                  | .(expr)       -- arbitrary expression in brackets
-
-    simpleExpr ::= simplerExpr postfixProj+   -- postfix projection
-                 | (postfixProj+ simpleExpr+) -- section of postfix projection
-                 | simplerExpr                -- (parses as whatever it used to)
-
-Desugaring rules
-----------------
-
-* Postfix projections:
-  ``simpleExpr .proj1 .proj2 .proj3`` desugars to ``(proj3 (proj2 (proj1 simpleExpr))``
-
-* Sections of postfix projections:
-  ``(.proj1 .proj2 .proj3 arg1 arg2)`` desugars to ``(\x => x.proj1.proj2.proj3 arg1 arg2)``
-
-Examples of desugaring:
-
-* ``foo.bar`` desugars as ``bar foo``
-* ``True.not`` is a single lexeme: qualified name
-* ``(True).not`` desugars as ``not True``
-* ``(True).(not . not)`` desugars as ``(not . not) True``
-* ``(not True).(not . not)`` desugars as ``(not . not) (not True)``
-* ``(checkFile fileName).runState initialState`` desugars as ``runState (checkFile fileName) initialState``
-* ``(MkPoint 3 4).x`` desugars as ``x (MkPoint 3 4)``
-
-Examples of desugaring sections:
-
-* bare ``.foo`` is invalid syntax (e.g. in ``f $ .foo``)
-* ``(.foo)`` desugars as ``(\x => x.foo)``, i.e. ``(\x => foo x)``
-* ``(.foo.bar m n)`` desugars as ``(\x => bar (foo x) m n)``
-
-Example code
-------------
-
-.. code-block:: idris
-
-    record Point where
-      constructor MkPoint
-      x : Double
-      y : Double
-
-This record creates two projections:
-
-* ``x : Point -> Double``
-* ``y : Point -> Double``
-
-We add another record:
-
-.. code-block:: idris
-
-    record Rect where
-      constructor MkRect
-      topLeft : Point
-      bottomRight : Point
-
-Let's define some constants:
-
-.. code-block:: idris
-
-    pt : Point
-    pt = MkPoint 4.2 6.6
-
-    rect : Rect
-    rect =
-      MkRect
-        (MkPoint 1.1 2.5)
-        (MkPoint 4.3 6.3)
-
-    squared : Num a => a -> a
-    squared x = x * x
-
-Finally, some examples:
-
-.. code-block:: idris
-
-    main : IO ()
-    main = do
-      -- desugars to (x pt)
-      -- prints 4.2
-      printLn $ pt.x
-
-      -- prints 4.2, too
-      -- maybe we want to make this a parse error?
-      printLn $ pt .x
-
-      -- prints 10.8
-      printLn $ pt.x + pt.y
-
-      -- works fine with namespacing
-      -- both print 4.2
-      printLn $ Main.pt.x
-      printLn $ (Main.pt).x
-
-      -- the LHS can be an arbitrary expression
-      -- prints 4.2
-      printLn $ (MkPoint pt.y pt.x).y
-
-      -- the RHS can be an arbitrary expression, too
-      -- prints 17.64
-      printLn $ (MkPoint pt.y pt.x).(squared . y)
-
-      -- user-defined function
-      -- prints 17.64
-      printLn $ pt.x.squared
-
-      -- prints [1.0, 3.0]
-      printLn $ map (.x) [MkPoint 1 2, MkPoint 3 4]
-
-      -- .topLeft.y desugars to (\x => y (topLeft x))
-      -- prints [2.5, 2.5]
-      printLn $ map (.topLeft.y) [rect, rect]
-
-      -- desugars to (.topLeft.x rect + .bottomRight.y rect)
-      -- prints 7.4
-      printLn $ rect.topLeft.x + rect.bottomRight.y
-
-      -- complex projections
-      -- prints 7.4
-      printLn $ rect.(x . topLeft) + rect.(y . bottomRight)
-
-      -- haskell-style projections
-      printLn $ Main.Point.x pt
-      printLn $ Point.x pt
-      printLn $ (x) pt
-      printLn $ x pt
-
-      -- record update syntax uses dots now
-      -- prints 3.0
-      printLn $ (record { topLeft.x = 3 } rect).topLeft.x
-
-      -- but for compatibility, we support the old syntax, too
-      printLn $ (record { topLeft->x = 3 } rect).topLeft.x
-
-      -- prints 2.1
-      printLn $ (record { topLeft.x $= (+1) } rect).topLeft.x
-      printLn $ (record { topLeft->x $= (+1) } rect).topLeft.x
-
-Parses but does not typecheck:
-
-.. code-block:: idris
-
-  -- parses as: map.x [MkPoint 1 2, MkPoint 3 4]
-  -- maybe we should disallow spaces before dots?
-  --
-  printLn $ map .x [MkPoint 1 2, MkPoint 3 4]
diff --git a/docs/source/reference/records.rst b/docs/source/reference/records.rst
new file mode 100644
index 000000000..b1ed54aa1
--- /dev/null
+++ b/docs/source/reference/records.rst
@@ -0,0 +1,195 @@
+Dot syntax for records
+======================
+
+.. role:: idris(code)
+    :language: idris
+
+Long story short, ``.field`` is a postfix projection operator that binds
+tighter than function application.
+
+Lexical structure
+-----------------
+
+* ``.foo`` is a valid name, which stands for record fields (new ``Name``
+  constructor ``RF "foo"``)
+
+* ``Foo.bar.baz`` starting with uppercase ``F`` is one lexeme, a namespaced
+  identifier: ``DotSepIdent ["baz", "bar", "Foo"]``
+
+* ``foo.bar.baz`` starting with lowercase ``f`` is three lexemes: ``foo``,
+  ``.bar``, ``.baz``
+
+* ``.foo.bar.baz`` is three lexemes: ``.foo``, ``.bar``, ``.baz``
+
+* If you want ``Constructor.field``, you have to write ``(Constructor).field``.
+
+* All module names must start with an uppercase letter.
+
+New syntax of ``simpleExpr``
+----------------------------
+
+Expressions binding tighter than application (``simpleExpr``), such as variables or parenthesised expressions, have been renamed to ``simplerExpr``, and an extra layer of syntax has been inserted.
+
+.. code-block:: idris
+
+    simpleExpr ::= (.field)+               -- parses as PPostfixAppPartial
+                 | simplerExpr (.field)+   -- parses as PPostfixApp
+                 | simplerExpr             -- (parses as whatever it used to)
+
+* ``(.foo)`` is a name, so you can use it to e.g. define a function called
+  ``.foo`` (see ``.squared`` below)
+
+* ``(.foo.bar)`` is a parenthesised expression
+
+Desugaring rules
+----------------
+
+* ``(.field1 .field2 .field3)`` desugars to ``(\x => .field3 (.field2 (.field1
+  x)))``
+
+* ``(simpleExpr .field1 .field2 .field3)`` desugars to ``((.field .field2
+  .field3) simpleExpr)``
+
+Record elaboration
+------------------
+
+* there is a new pragma ``%prefix_record_projections``, which is ``on`` by
+  default
+
+* for every field ``f`` of a record ``R``, we get:
+
+  * projection ``f`` in namespace ``R`` (exactly like now), unless
+    ``%prefix_record_projections`` is ``off``
+
+  * projection ``.f`` in namespace ``R`` with the same definition
+
+Example code
+------------
+
+.. code-block:: idris
+
+    record Point where
+      constructor MkPoint
+      x : Double
+      y : Double
+
+This record creates two projections:
+* ``.x : Point -> Double``
+* ``.y : Point -> Double``
+
+Because ``%prefix_record_projections`` are ``on`` by default, we also get:
+* ``x : Point -> Double``
+* ``y : Point -> Double``
+
+To prevent cluttering the ordinary global name space with short identifiers, we can do this:
+
+.. code-block:: idris
+
+    %prefix_record_projections off
+
+    record Rect where
+      constructor MkRect
+      topLeft : Point
+      bottomRight : Point
+
+For ``Rect``, we don't get the prefix projections:
+
+.. code-block:: idris
+
+    Main> :t topLeft
+    (interactive):1:4--1:11:Undefined name topLeft
+    Main> :t .topLeft
+    \{rec:0} => .topLeft rec : ?_ -> Point
+
+Let's define some constants:
+
+.. code-block:: idris
+
+    pt : Point
+    pt = MkPoint 4.2 6.6
+
+    rect : Rect
+    rect =
+      MkRect
+        (MkPoint 1.1 2.5)
+        (MkPoint 4.3 6.3)
+
+User-defined projections work, too. (Should they?)
+
+.. code-block:: idris
+
+    (.squared) : Double -> Double
+    (.squared) x = x * x
+
+Finally, the examples:
+
+.. code-block:: idris
+
+    main : IO ()
+    main = do
+      -- desugars to (.x pt)
+      -- prints 4.2
+      printLn $ pt.x
+
+      -- prints 4.2, too
+      -- maybe we want to make this a parse error?
+      printLn $ pt .x
+
+      -- prints 10.8
+      printLn $ pt.x + pt.y
+
+      -- works fine with namespacing
+      -- prints 4.2
+      printLn $ (Main.pt).x
+
+      -- the LHS can be an arbitrary expression
+      -- prints 4.2
+      printLn $ (MkPoint pt.y pt.x).y
+
+      -- user-defined projection
+      -- prints 17.64
+      printLn $ pt.x.squared
+
+      -- prints [1.0, 3.0]
+      printLn $ map (.x) [MkPoint 1 2, MkPoint 3 4]
+
+      -- .topLeft.y desugars to (\x => .y (.topLeft x))
+      -- prints [2.5, 2.5]
+      printLn $ map (.topLeft.y) [rect, rect]
+
+      -- desugars to (.topLeft.x rect + .bottomRight.y rect)
+      -- prints 7.4
+      printLn $ rect.topLeft.x + rect.bottomRight.y
+
+      -- qualified names work, too
+      -- all these print 4.2
+      printLn $ Main.Point.(.x) pt
+      printLn $ Point.(.x) pt
+      printLn $ (.x) pt
+      printLn $ .x pt
+
+      -- haskell-style projections work, too
+      printLn $ Main.Point.x pt
+      printLn $ Point.x pt
+      printLn $ (x) pt
+      printLn $ x pt
+
+      -- record update syntax uses dots now
+      -- prints 3.0
+      printLn $ (record { topLeft.x = 3 } rect).topLeft.x
+
+      -- but for compatibility, we support the old syntax, too
+      printLn $ (record { topLeft->x = 3 } rect).topLeft.x
+
+      -- prints 2.1
+      printLn $ (record { topLeft.x $= (+1) } rect).topLeft.x
+      printLn $ (record { topLeft->x $= (+1) } rect).topLeft.x
+
+Parses but does not typecheck:
+
+.. code-block:: idris
+
+  -- parses as: map.x [MkPoint 1 2, MkPoint 3 4]
+  -- maybe we should disallow spaces before dots?
+  --
+  printLn $ map .x [MkPoint 1 2, MkPoint 3 4]
diff --git a/docs/source/tutorial/typesfuns.rst b/docs/source/tutorial/typesfuns.rst
index 2849f53ab..7205f9e67 100644
--- a/docs/source/tutorial/typesfuns.rst
+++ b/docs/source/tutorial/typesfuns.rst
@@ -988,8 +988,8 @@ type. The field names can be used to access the field values:
     "Fred" : String
     *Record> fred.age
     30 : Int
-    *Record> :t firstName
-    firstName : Person -> String
+    *Record> :t (.firstName)
+    Main.Person.(.firstName) : Person -> String
 
 We can use prefix field projections, like in Haskell:
 
@@ -999,6 +999,14 @@ We can use prefix field projections, like in Haskell:
     "Fred" : String
     *Record> age fred
     30 : Int
+    *Record> :t firstName
+    firstName : Person -> String
+
+Prefix field projections can be disabled per record definition
+using pragma ``%prefix_record_projections off``, which makes
+all subsequently defined records generate only dotted projections.
+This pragma has effect until the end of the module
+or until the closest occurrence of ``%prefix_record_projections on``.
 
 We can also use the field names to update a record (or, more
 precisely, produce a copy of the record with the given fields
diff --git a/libs/base/Data/Strings.idr b/libs/base/Data/Strings.idr
index 7c2f2fe29..8c66181f5 100644
--- a/libs/base/Data/Strings.idr
+++ b/libs/base/Data/Strings.idr
@@ -16,11 +16,21 @@ partial
 foldl1 : (a -> a -> a) -> List a -> a
 foldl1 f (x::xs) = foldl f x xs
 
+-- This function runs fast when compiled but won't compute at compile time.
+-- If you need to unpack strings at compile time, use Prelude.unpack.
+%foreign
+  "scheme:string-unpack"
+export
+fastUnpack : String -> List Char
+
 -- This works quickly because when string-concat builds the result, it allocates
 -- enough room in advance so there's only one allocation, rather than lots!
+--
+-- Like fastUnpack, this function won't reduce at compile time.
+-- If you need to concatenate strings at compile time, use Prelude.concat.
 %foreign
-    "scheme:string-concat"
-    "javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
+  "scheme:string-concat"
+  "javascript:lambda:(xs)=>''.concat(...__prim_idris2js_array(xs))"
 export
 fastConcat : List String -> String
 
diff --git a/libs/base/Language/Reflection/TT.idr b/libs/base/Language/Reflection/TT.idr
index a1188604e..810867784 100644
--- a/libs/base/Language/Reflection/TT.idr
+++ b/libs/base/Language/Reflection/TT.idr
@@ -64,6 +64,7 @@ data Name = UN String -- user defined name
           | MN String Int -- machine generated name
           | NS Namespace Name -- name in a namespace
           | DN String Name -- a name and how to display it
+          | RF String -- record field name
 
 export
 Show Name where
@@ -71,6 +72,7 @@ Show Name where
   show (UN x) = x
   show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
   show (DN str y) = str
+  show (RF n) = "." ++ n
 
 public export
 data Count = M0 | M1 | MW
diff --git a/libs/contrib/Data/List/Lazy.idr b/libs/contrib/Data/List/Lazy.idr
new file mode 100644
index 000000000..4bfcdd3c8
--- /dev/null
+++ b/libs/contrib/Data/List/Lazy.idr
@@ -0,0 +1,55 @@
+module Data.List.Lazy
+
+%default total
+
+-- All functions here are public export
+-- because their definitions are pretty much the specification.
+
+public export
+data LazyList : Type -> Type where
+  Nil : LazyList a
+  (::) : (1 x : a) -> (1 xs : Lazy (LazyList a)) -> LazyList a
+
+public export
+Semigroup (LazyList a) where
+  [] <+> ys = ys
+  (x :: xs) <+> ys = x :: (xs <+> ys)
+
+public export
+Monoid (LazyList a) where
+  neutral = []
+
+public export
+Foldable LazyList where
+  foldr op nil [] = nil
+  foldr op nil (x :: xs) = x `op` foldr op nil xs
+
+  foldl op acc [] = acc
+  foldl op acc (x :: xs) = foldl op (acc `op` x) xs
+
+public export
+Functor LazyList where
+  map f [] = []
+  map f (x :: xs) = f x :: map f xs
+
+public export
+Applicative LazyList where
+  pure x = [x]
+  fs <*> vs = concatMap (\f => map f vs) fs
+
+public export
+Alternative LazyList where
+  empty = []
+  (<|>) = (<+>)
+
+public export
+Monad LazyList where
+  m >>= f = concatMap f m
+
+-- There is no Traversable instance for lazy lists.
+-- The result of a traversal will be a non-lazy list in general
+-- (you can't delay the "effect" of an applicative functor).
+public export
+traverse : Applicative f => (a -> f b) -> LazyList a -> f (List b)
+traverse g [] = pure []
+traverse g (x :: xs) = [| g x :: traverse g xs |]
diff --git a/libs/contrib/Data/SortedSet.idr b/libs/contrib/Data/SortedSet.idr
index 1a9eb5911..9346c8816 100644
--- a/libs/contrib/Data/SortedSet.idr
+++ b/libs/contrib/Data/SortedSet.idr
@@ -65,3 +65,11 @@ Ord k => Monoid (SortedSet k) where
 export
 keySet : SortedMap k v -> SortedSet k
 keySet = SetWrapper . map (const ())
+
+export
+singleton : Ord k => k -> SortedSet k
+singleton k = insert k empty
+
+export
+null : SortedSet k -> Bool
+null (SetWrapper m) = SortedMap.null m
diff --git a/libs/contrib/Data/String/Iterator.idr b/libs/contrib/Data/String/Iterator.idr
new file mode 100644
index 000000000..c6066c510
--- /dev/null
+++ b/libs/contrib/Data/String/Iterator.idr
@@ -0,0 +1,74 @@
+module Data.String.Iterator
+
+import public Data.List.Lazy
+
+%default total
+
+-- Backend-dependent string iteration type,
+-- parameterised by the string that it iterates over.
+--
+-- Beware: the index is checked only up to definitional equality.
+-- In theory, you could run `decEq` on two strings
+-- with the same content but allocated in different memory locations
+-- and use the obtained Refl to coerce iterators between them.
+--
+-- The strictly correct solution is to make the iterators independent
+-- from the exact memory location of the string given to `uncons`.
+-- (For example, byte offsets satisfy this requirement.)
+export
+data StringIterator : String -> Type where [external]
+
+-- This function is private
+-- to avoid subverting the linearity guarantees of withString.
+%foreign
+  "scheme:blodwen-string-iterator-new"
+  "javascript:stringIterator:new"
+private
+fromString : (str : String) -> StringIterator str
+
+-- This function uses a linear string iterator
+-- so that backends can use mutating iterators.
+export
+withString : (str : String) -> ((1 it : StringIterator str) -> a) -> a
+withString str f = f (fromString str)
+
+-- We use a custom data type instead of Maybe (Char, StringIterator)
+-- to remove one level of pointer indirection
+-- in every iteration of something that's likely to be a hot loop,
+-- and to avoid one allocation per character.
+--
+-- The Char field of Character is unrestricted for flexibility.
+public export
+data UnconsResult : String -> Type where
+  EOF : UnconsResult str
+  Character : (c : Char) -> (1 it : StringIterator str) -> UnconsResult str
+
+-- We pass the whole string to the uncons function
+-- to avoid yet another allocation per character
+-- because for many backends, StringIterator can be simply an integer
+-- (e.g. byte offset into an UTF-8 string).
+%foreign
+  "scheme:blodwen-string-iterator-next"
+  "javascript:stringIterator:next"
+export
+uncons : (str : String) -> (1 it : StringIterator str) -> UnconsResult str
+
+export
+foldl : (accTy -> Char -> accTy) -> accTy -> String -> accTy
+foldl op acc str = withString str (loop acc)
+  where
+    loop : accTy -> (1 it : StringIterator str) -> accTy
+    loop acc it =
+      case uncons str it of
+        EOF => acc
+        Character c it' => loop (acc `op` c) (assert_smaller it it')
+
+export
+unpack : String -> LazyList Char
+unpack str = withString str unpack'
+  where
+    unpack' : (1 it : StringIterator str) -> LazyList Char
+    unpack' it =
+      case uncons str it of
+        EOF => []
+        Character c it' => c :: Delay (unpack' $ assert_smaller it it')
diff --git a/libs/contrib/Text/Lexer/Core.idr b/libs/contrib/Text/Lexer/Core.idr
index 4144e3353..d17579917 100644
--- a/libs/contrib/Text/Lexer/Core.idr
+++ b/libs/contrib/Text/Lexer/Core.idr
@@ -199,13 +199,13 @@ tokenise pred line col acc tmap str
 export
 lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
 lex tmap str
-    = let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (unpack str) in
+    = let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (fastUnpack str) in
           (ts, (l, c, pack str'))
 
 export
 lexTo : (TokenData a -> Bool) ->
         TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
 lexTo pred tmap str
-    = let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (unpack str) in
+    = let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (fastUnpack str) in
           (ts, (l, c, pack str'))
 
diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg
index c8b0bfa58..8dbf62afa 100644
--- a/libs/contrib/contrib.ipkg
+++ b/libs/contrib/contrib.ipkg
@@ -21,6 +21,7 @@ modules = Control.ANSI,
           Data.List.TailRec,
           Data.List.Equalities,
           Data.List.Reverse,
+          Data.List.Lazy,
           Data.List.Views.Extra,
           Data.List.Palindrome,
 
@@ -48,6 +49,7 @@ modules = Control.ANSI,
           Data.Stream.Extra,
           Data.String.Extra,
           Data.String.Interpolation,
+          Data.String.Iterator,
           Data.String.Parser,
           Data.String.Parser.Expression,
 
diff --git a/libs/network/Network/Socket/Data.idr b/libs/network/Network/Socket/Data.idr
index bc36ca1fc..e4c39b501 100644
--- a/libs/network/Network/Socket/Data.idr
+++ b/libs/network/Network/Socket/Data.idr
@@ -110,14 +110,27 @@ Show SocketFamily where
   show AF_INET   = "AF_INET"
   show AF_INET6  = "AF_INET6"
 
+-- This is a bit of a hack to get the OS-dependent magic constants out of C and
+-- into Idris without having to faff around on the preprocessor on the Idris
+-- side.
+%foreign "C:idrnet_af_unspec,libidris2_support"
+prim__idrnet_af_unspec : PrimIO Int
+
+%foreign "C:idrnet_af_unix,libidris2_support"
+prim__idrnet_af_unix : PrimIO Int
+
+%foreign "C:idrnet_af_inet,libidris2_support"
+prim__idrnet_af_inet : PrimIO Int
+
+%foreign "C:idrnet_af_inet6,libidris2_support"
+prim__idrnet_af_inet6 : PrimIO Int
+
 export
 ToCode SocketFamily where
-  -- Don't know how to read a constant value from C code in idris2...
-  -- gotta to hardcode those for now
-  toCode AF_UNSPEC = 0 -- unsafePerformIO (cMacro "#AF_UNSPEC" Int)
-  toCode AF_UNIX   = 1
-  toCode AF_INET   = 2
-  toCode AF_INET6  = 10
+  toCode AF_UNSPEC = unsafePerformIO $ primIO $ prim__idrnet_af_unspec
+  toCode AF_UNIX   = unsafePerformIO $ primIO $ prim__idrnet_af_unix
+  toCode AF_INET   = unsafePerformIO $ primIO $ prim__idrnet_af_inet
+  toCode AF_INET6  = unsafePerformIO $ primIO $ prim__idrnet_af_inet6
 
 export
 getSocketFamily : Int -> Maybe SocketFamily
diff --git a/src/Compiler/ES/ES.idr b/src/Compiler/ES/ES.idr
index 5ff74859c..71caf7a3a 100644
--- a/src/Compiler/ES/ES.idr
+++ b/src/Compiler/ES/ES.idr
@@ -73,6 +73,28 @@ addSupportToPreamble : {auto c : Ref ESs ESSt} -> String -> String -> Core Strin
 addSupportToPreamble name code =
   addToPreamble name name code
 
+addStringIteratorToPreamble : {auto c : Ref ESs ESSt} -> Core String
+addStringIteratorToPreamble =
+  do
+    let defs = "
+function __prim_stringIteratorNew(str) {
+  return str[Symbol.iterator]();
+}
+function __prim_stringIteratorNext(str, it) {
+  const char = it.next();
+  if (char.done) {
+    return {h: 0}; // EOF
+  } else {
+    return {
+      h: 1, // Character
+      a1: char.value,
+      a2: it
+    };
+  }
+}"
+    let name = "stringIterator"
+    let newName = esName name
+    addToPreamble name newName defs
 
 jsIdent : String -> String
 jsIdent s = concatMap okchar (unpack s)
@@ -92,6 +114,7 @@ jsName (UN n) = keywordSafe $ jsIdent n
 jsName (MN n i) = jsIdent n ++ "_" ++ show i
 jsName (PV n d) = "pat__" ++ jsName n
 jsName (DN _ n) = jsName n
+jsName (RF n) = "rf__" ++ jsIdent n
 jsName (Nested (i, x) n) = "n__" ++ show i ++ "_" ++ show x ++ "_" ++ jsName n
 jsName (CaseBlock x y) = "case__" ++ jsIdent x ++ "_" ++ show y
 jsName (WithBlock x y) = "with__" ++ jsIdent x ++ "_" ++ show y
@@ -311,6 +334,13 @@ makeForeign n x =
           lib_code <- readDataFile ("js/" ++ lib ++ ".js")
           addSupportToPreamble lib lib_code
           pure $ "const " ++ jsName n ++ " = " ++ lib ++ "_" ++ name ++ "\n"
+      "stringIterator" =>
+        do
+          addStringIteratorToPreamble
+          case def of
+            "new" => pure $ "const " ++ jsName n ++ " = __prim_stringIteratorNew;\n"
+            "next" => pure $ "const " ++ jsName n ++ " = __prim_stringIteratorNext;\n"
+            _ => throw (InternalError $ "invalid string iterator function: " ++ def ++ ", supported functions are \"new\", \"next\"")
 
 
       _ => throw (InternalError $ "invalid foreign type : " ++ ty ++ ", supported types are \"lambda\", \"lambdaRequire\", \"support\"")
diff --git a/src/Compiler/Scheme/Common.idr b/src/Compiler/Scheme/Common.idr
index 3bdd3d8a7..85f94058f 100644
--- a/src/Compiler/Scheme/Common.idr
+++ b/src/Compiler/Scheme/Common.idr
@@ -36,6 +36,7 @@ schName (UN n) = schString n
 schName (MN n i) = schString n ++ "-" ++ show i
 schName (PV n d) = "pat--" ++ schName n
 schName (DN _ n) = schName n
+schName (RF n) = "rf--" ++ schString n
 schName (Nested (i, x) n) = "n--" ++ show i ++ "-" ++ show x ++ "-" ++ schName n
 schName (CaseBlock x y) = "case--" ++ schString x ++ "-" ++ show y
 schName (WithBlock x y) = "with--" ++ schString x ++ "-" ++ show y
diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr
index b08eaa222..cd607311b 100644
--- a/src/Core/Binary.idr
+++ b/src/Core/Binary.idr
@@ -31,7 +31,7 @@ import Data.Buffer
 -- TTC files can only be compatible if the version number is the same
 export
 ttcVersion : Int
-ttcVersion = 41
+ttcVersion = 42
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()
diff --git a/src/Core/Context.idr b/src/Core/Context.idr
index 2124123f3..37b115dc0 100644
--- a/src/Core/Context.idr
+++ b/src/Core/Context.idr
@@ -361,7 +361,7 @@ initCtxtS : Int -> Core Context
 initCtxtS s
     = do arr <- coreLift $ newArray s
          aref <- newRef Arr arr
-         pure (MkContext 0 0 empty empty aref 0 empty [partialEvalNS] False False empty)
+         pure $ MkContext 0 0 empty empty aref 0 empty [partialEvalNS] False False empty
 
 export
 initCtxt : Core Context
@@ -1299,6 +1299,8 @@ visibleInAny nss n vis = any (\ns => visibleIn ns n vis) nss
 reducibleIn : Namespace -> Name -> Visibility -> Bool
 reducibleIn nspace (NS ns (UN n)) Export = isParentOf ns nspace
 reducibleIn nspace (NS ns (UN n)) Private = isParentOf ns nspace
+reducibleIn nspace (NS ns (RF n)) Export = isParentOf ns nspace
+reducibleIn nspace (NS ns (RF n)) Private = isParentOf ns nspace
 reducibleIn nspace n _ = True
 
 export
@@ -1806,6 +1808,9 @@ inCurrentNS n@(MN _ _)
 inCurrentNS n@(DN _ _)
     = do defs <- get Ctxt
          pure (NS (currentNS defs) n)
+inCurrentNS n@(RF _)
+    = do defs <- get Ctxt
+         pure (NS (currentNS defs) n)
 inCurrentNS n = pure n
 
 export
@@ -2012,6 +2017,12 @@ setUnboundImplicits a
     = do defs <- get Ctxt
          put Ctxt (record { options->elabDirectives->unboundImplicits = a } defs)
 
+export
+setPrefixRecordProjections : {auto c : Ref Ctxt Defs} -> Bool -> Core ()
+setPrefixRecordProjections b = do
+  defs <- get Ctxt
+  put Ctxt (record { options->elabDirectives->prefixRecordProjections = b } defs)
+
 export
 setDefaultTotalityOption : {auto c : Ref Ctxt Defs} ->
                            TotalReq -> Core ()
@@ -2047,6 +2058,11 @@ isUnboundImplicits
     = do defs <- get Ctxt
          pure (unboundImplicits (elabDirectives (options defs)))
 
+export
+isPrefixRecordProjections : {auto c : Ref Ctxt Defs} -> Core Bool
+isPrefixRecordProjections =
+  prefixRecordProjections . elabDirectives . options <$> get Ctxt
+
 export
 getDefaultTotalityOption : {auto c : Ref Ctxt Defs} ->
                            Core TotalReq
diff --git a/src/Core/Hash.idr b/src/Core/Hash.idr
index a1321bf7c..2fdb291e1 100644
--- a/src/Core/Hash.idr
+++ b/src/Core/Hash.idr
@@ -5,7 +5,9 @@ import Core.TT
 
 import Data.List
 import Data.List1
+import Data.List.Lazy
 import Data.Strings
+import Data.String.Iterator
 
 %default covering
 
@@ -56,15 +58,7 @@ Hashable a => Hashable (Maybe a) where
 
 export
 Hashable String where
-  hashWithSalt h str = hashChars h 0 (cast (length str)) str
-    where
-      hashChars : Int -> Int -> Int -> String -> Int
-      hashChars h p len str
-          = assert_total $
-              if p == len
-                 then h
-                 else hashChars (h * 33 + cast (strIndex str p))
-                                (p + 1) len str
+  hashWithSalt h = String.Iterator.foldl hashWithSalt h
 
 export
 Hashable Namespace where
diff --git a/src/Core/Name.idr b/src/Core/Name.idr
index d22fb364e..2385642ae 100644
--- a/src/Core/Name.idr
+++ b/src/Core/Name.idr
@@ -19,6 +19,7 @@ data Name : Type where
      MN : String -> Int -> Name -- machine generated name
      PV : Name -> Int -> Name -- pattern variable name; int is the resolved function id
      DN : String -> Name -> Name -- a name and how to display it
+     RF : String -> Name  -- record field name
      Nested : (Int, Int) -> Name -> Name -- nested function name
      CaseBlock : String -> Int -> Name -- case block nested in (resolved) name
      WithBlock : String -> Int -> Name -- with block nested in (resolved) name
@@ -57,6 +58,7 @@ userNameRoot : Name -> Maybe String
 userNameRoot (NS _ n) = userNameRoot n
 userNameRoot (UN n) = Just n
 userNameRoot (DN _ n) = userNameRoot n
+userNameRoot (RF n) = Just ("." ++ n)  -- TMP HACK
 userNameRoot _ = Nothing
 
 export
@@ -74,6 +76,7 @@ nameRoot (UN n) = n
 nameRoot (MN n _) = n
 nameRoot (PV n _) = nameRoot n
 nameRoot (DN _ n) = nameRoot n
+nameRoot (RF n) = n
 nameRoot (Nested _ inner) = nameRoot inner
 nameRoot (CaseBlock n _) = "$" ++ show n
 nameRoot (WithBlock n _) = "$" ++ show n
@@ -93,11 +96,13 @@ dropAllNS n = n
 
 export
 Show Name where
+  show (NS ns n@(RF _)) = show ns ++ ".(" ++ show n ++ ")"
   show (NS ns n) = show ns ++ "." ++ show n
   show (UN x) = x
   show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
   show (PV n d) = "{P:" ++ show n ++ ":" ++ show d ++ "}"
   show (DN str n) = str
+  show (RF n) = "." ++ n
   show (Nested (outer, idx) inner)
       = show outer ++ ":" ++ show idx ++ ":" ++ show inner
   show (CaseBlock outer i) = "case block in " ++ outer
@@ -106,11 +111,13 @@ Show Name where
 
 export
 Pretty Name where
+  pretty (NS ns n@(RF _)) = pretty ns <+> dot <+> parens (pretty n)
   pretty (NS ns n) = pretty ns <+> dot <+> pretty n
   pretty (UN x) = pretty x
   pretty (MN x y) = braces (pretty x <+> colon <+> pretty y)
   pretty (PV n d) = braces (pretty 'P' <+> colon <+> pretty n <+> colon <+> pretty d)
   pretty (DN str _) = pretty str
+  pretty (RF n) = "." <+> pretty n
   pretty (Nested (outer, idx) inner) = pretty outer <+> colon <+> pretty idx <+> colon <+> pretty inner
   pretty (CaseBlock outer _) = reflow "case block in" <++> pretty outer
   pretty (WithBlock outer _) = reflow "with block in" <++> pretty outer
@@ -123,6 +130,7 @@ Eq Name where
     (==) (MN x y) (MN x' y') = y == y' && x == x'
     (==) (PV x y) (PV x' y') = x == x' && y == y'
     (==) (DN _ n) (DN _ n') = n == n'
+    (==) (RF n) (RF n') = n == n'
     (==) (Nested x y) (Nested x' y') = x == x' && y == y'
     (==) (CaseBlock x y) (CaseBlock x' y') = y == y' && x == x'
     (==) (WithBlock x y) (WithBlock x' y') = y == y' && x == x'
@@ -135,10 +143,11 @@ nameTag (UN _) = 1
 nameTag (MN _ _) = 2
 nameTag (PV _ _) = 3
 nameTag (DN _ _) = 4
-nameTag (Nested _ _) = 5
-nameTag (CaseBlock _ _) = 6
-nameTag (WithBlock _ _) = 7
-nameTag (Resolved _) = 8
+nameTag (RF _) = 5
+nameTag (Nested _ _) = 6
+nameTag (CaseBlock _ _) = 7
+nameTag (WithBlock _ _) = 8
+nameTag (Resolved _) = 9
 
 export
 Ord Name where
@@ -161,6 +170,7 @@ Ord Name where
                GT => GT
                LT => LT
     compare (DN _ n) (DN _ n') = compare n n'
+    compare (RF n) (RF n') = compare n n'
     compare (Nested x y) (Nested x' y')
         = case compare y y' of
                EQ => compare x x'
@@ -206,6 +216,9 @@ nameEq (DN x t) (DN y t') with (decEq x y)
     nameEq (DN y t) (DN y t) | (Yes Refl) | (Just Refl) = Just Refl
     nameEq (DN y t) (DN y t') | (Yes Refl) | Nothing = Nothing
   nameEq (DN x t) (DN y t') | (No p) = Nothing
+nameEq (RF x) (RF y) with (decEq x y)
+  nameEq (RF y) (RF y) | (Yes Refl) = Just Refl
+  nameEq (RF x) (RF y) | (No contra) = Nothing
 nameEq (Nested x y) (Nested x' y') with (decEq x x')
   nameEq (Nested x y) (Nested x' y') | (No p) = Nothing
   nameEq (Nested x y) (Nested x y') | (Yes Refl) with (nameEq y y')
diff --git a/src/Core/Options.idr b/src/Core/Options.idr
index 7e5b285d0..c85873683 100644
--- a/src/Core/Options.idr
+++ b/src/Core/Options.idr
@@ -101,13 +101,11 @@ public export
 data LangExt
      = ElabReflection
      | Borrowing -- not yet implemented
-     | PostfixProjections
 
 export
 Eq LangExt where
   ElabReflection == ElabReflection = True
   Borrowing == Borrowing = True
-  PostfixProjections == PostfixProjections = True
   _ == _ = False
 
 -- Other options relevant to the current session (so not to be saved in a TTC)
@@ -119,6 +117,11 @@ record ElabDirectives where
   totality : TotalReq
   ambigLimit : Nat
   autoImplicitLimit : Nat
+  --
+  -- produce traditional (prefix) record projections,
+  -- in addition to postfix (dot) projections
+  -- default: yes
+  prefixRecordProjections : Bool
 
 public export
 record Session where
@@ -186,7 +189,7 @@ defaultSession = MkSessionOpts False False False Chez [] defaultLogLevel
 
 export
 defaultElab : ElabDirectives
-defaultElab = MkElabDirectives True True CoveringOnly 3 50
+defaultElab = MkElabDirectives True True CoveringOnly 3 50 True
 
 export
 defaults : Options
diff --git a/src/Core/Reflect.idr b/src/Core/Reflect.idr
index c7a3b3b06..bc91b3e25 100644
--- a/src/Core/Reflect.idr
+++ b/src/Core/Reflect.idr
@@ -272,6 +272,9 @@ Reify Name where
                  => do str' <- reify defs !(evalClosure defs str)
                        n' <- reify defs !(evalClosure defs n)
                        pure (DN str' n')
+             (NS _ (UN "RF"), [str])
+                 => do str' <- reify defs !(evalClosure defs str)
+                       pure (RF str')
              _ => cantReify val "Name"
   reify defs val = cantReify val "Name"
 
@@ -292,6 +295,9 @@ Reflect Name where
       = do str' <- reflect fc defs lhs env str
            n' <- reflect fc defs lhs env n
            appCon fc defs (reflectiontt "DN") [str', n']
+  reflect fc defs lhs env (RF x)
+      = do x' <- reflect fc defs lhs env x
+           appCon fc defs (reflectiontt "RF") [x']
   reflect fc defs lhs env (Resolved i)
       = case !(full (gamma defs) (Resolved i)) of
              Resolved _ => cantReflect fc "Name"
diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr
index b24df1a54..cb87c6baa 100644
--- a/src/Core/TTC.idr
+++ b/src/Core/TTC.idr
@@ -47,9 +47,10 @@ TTC Name where
   toBuf b (MN x y) = do tag 2; toBuf b x; toBuf b y
   toBuf b (PV x y) = do tag 3; toBuf b x; toBuf b y
   toBuf b (DN x y) = do tag 4; toBuf b x; toBuf b y
-  toBuf b (Nested x y) = do tag 5; toBuf b x; toBuf b y
-  toBuf b (CaseBlock x y) = do tag 6; toBuf b x; toBuf b y
-  toBuf b (WithBlock x y) = do tag 7; toBuf b x; toBuf b y
+  toBuf b (RF x) = do tag 5; toBuf b x
+  toBuf b (Nested x y) = do tag 6; toBuf b x; toBuf b y
+  toBuf b (CaseBlock x y) = do tag 7; toBuf b x; toBuf b y
+  toBuf b (WithBlock x y) = do tag 8; toBuf b x; toBuf b y
   toBuf b (Resolved x)
       = throw (InternalError ("Can't write resolved name " ++ show x))
 
@@ -70,12 +71,14 @@ TTC Name where
                      y <- fromBuf b
                      pure (DN x y)
              5 => do x <- fromBuf b
-                     y <- fromBuf b
-                     pure (Nested x y)
+                     pure (RF x)
              6 => do x <- fromBuf b
                      y <- fromBuf b
-                     pure (CaseBlock x y)
+                     pure (Nested x y)
              7 => do x <- fromBuf b
+                     y <- fromBuf b
+                     pure (CaseBlock x y)
+             8 => do x <- fromBuf b
                      y <- fromBuf b
                      pure (WithBlock x y)
              _ => corrupt "Name"
diff --git a/src/Core/UnifyState.idr b/src/Core/UnifyState.idr
index b6b6517a6..cda9cd5bf 100644
--- a/src/Core/UnifyState.idr
+++ b/src/Core/UnifyState.idr
@@ -125,6 +125,7 @@ genMVName : {auto c : Ref Ctxt Defs} ->
             Name -> Core Name
 genMVName (UN str) = genName str
 genMVName (MN str _) = genName str
+genMVName (RF str) = genName str
 genMVName n
     = do ust <- get UST
          put UST (record { nextName $= (+1) } ust)
diff --git a/src/Data/StringMap.idr b/src/Data/StringMap.idr
index 1fc820e81..eee66136f 100644
--- a/src/Data/StringMap.idr
+++ b/src/Data/StringMap.idr
@@ -293,6 +293,13 @@ export
 mergeLeft : StringMap v -> StringMap v -> StringMap v
 mergeLeft x y = mergeWith const x y
 
+export
+adjust : String -> (v -> v) -> StringMap v -> StringMap v
+adjust k f m =
+  case lookup k m of
+    Nothing => m
+    Just v => insert k (f v) m
+
 export
 Show v => Show (StringMap v) where
   show m = show $ map {b=String} (\(k,v) => k ++ "->" ++ show v) $ toList m
diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr
index 9ee7393f8..cc113fe2f 100644
--- a/src/Idris/Desugar.idr
+++ b/src/Idris/Desugar.idr
@@ -351,43 +351,12 @@ mutual
                 desugarB side ps (PApp fc (PApp fc (PRef fc (UN "rangeFromThen")) start) n)
   desugarB side ps (PUnifyLog fc lvl tm)
       = pure $ IUnifyLog fc lvl !(desugarB side ps tm)
-
-  desugarB side ps (PPostfixProjs fc rec projs)
-      = do
-        let isPRef = \case
-              PRef _ _ => True
-              _ => False
-        defs <- get Ctxt
-        when (not (isExtension PostfixProjections defs) && not (all isPRef projs)) $
-          throw (GenericMsg fc "complex postfix projections require %language PostfixProjections")
-
-        desugarB side ps $ foldl (\x, proj => PApp fc proj x) rec projs
-
-  desugarB side ps (PPostfixProjsSection fc projs args)
-      = do
-        let isPRef = \case
-              PRef _ _ => True
-              _ => False
-        defs <- get Ctxt
-
-        when (not (isExtension PostfixProjections defs)) $ do
-          when (not (all isPRef projs)) $
-            throw (GenericMsg fc "complex postfix projections require %language PostfixProjections")
-
-          case args of
-            [] => pure ()
-            _  => throw $ GenericMsg fc "postfix projection sections require %language PostfixProjections"
-
-        desugarB side ps $
+  desugarB side ps (PPostfixApp fc rec projs)
+      = desugarB side ps $ foldl (\x, proj => PApp fc (PRef fc proj) x) rec projs
+  desugarB side ps (PPostfixAppPartial fc projs)
+      = desugarB side ps $
           PLam fc top Explicit (PRef fc (MN "paRoot" 0)) (PImplicit fc) $
-            foldl
-              (\r, arg => PApp fc r arg)
-              (foldl
-                (\r, proj => PApp fc proj r)
-                (PRef fc (MN "paRoot" 0))
-                projs)
-              args
-
+            foldl (\r, proj => PApp fc (PRef fc proj) r) (PRef fc (MN "paRoot" 0)) projs
   desugarB side ps (PWithUnambigNames fc ns rhs)
       = IWithUnambigNames fc ns <$> desugarB side ps rhs
 
@@ -857,6 +826,8 @@ mutual
              UnboundImplicits a => do
                setUnboundImplicits a
                pure [IPragma (\nest, env => setUnboundImplicits a)]
+             PrefixRecordProjections b => do
+               pure [IPragma (\nest, env => setPrefixRecordProjections b)]
              AmbigDepth n => pure [IPragma (\nest, env => setAmbigLimit n)]
              AutoImplicitDepth n => pure [IPragma (\nest, env => setAutoImplicitLimit n)]
              PairNames ty f s => pure [IPragma (\nest, env => setPair fc ty f s)]
diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index f0577d1b2..3215f00ea 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -241,10 +241,9 @@ mutual
            (op, e) <- pure b.val
            pure (PSectionL (boundToFC fname (mergeBounds s b)) op e)
     <|> do  -- (.y.z)  -- section of projection (chain)
-           b <- bounds (MkPair <$> (some $ postfixApp fname indents) <*> (many $ simpleExpr fname indents))
-           (projs, args) <- pure b.val
+           b <- bounds $ some postfixProj
            symbol ")"
-           pure $ PPostfixProjsSection (boundToFC fname b) projs args
+           pure $ PPostfixAppPartial (boundToFC fname b) b.val
       -- unit type/value
     <|> do b <- bounds (continueWith indents ")")
            pure (PUnit (boundToFC fname (mergeBounds s b)))
@@ -340,22 +339,24 @@ mutual
      <|> do end <- bounds (continueWith indents ")")
             pure (PBracketed (boundToFC fname (mergeBounds s end)) e)
 
-  postfixApp : FileName -> IndentInfo -> Rule PTerm
-  postfixApp fname indents
-    = do di <- bounds dotIdent
+  postfixProjection : FileName -> IndentInfo -> Rule PTerm
+  postfixProjection fname indents
+    = do di <- bounds postfixProj
          pure $ PRef (boundToFC fname di) di.val
-    <|> (symbol ".(" *> commit *> expr pdef fname indents <* symbol ")")
 
   simpleExpr : FileName -> IndentInfo -> Rule PTerm
   simpleExpr fname indents
     = do  -- x.y.z
           b <- bounds (do root <- simplerExpr fname indents
-                          projs <- many $ postfixApp fname indents
+                          projs <- many postfixProj
                           pure (root, projs))
           (root, projs) <- pure b.val
           pure $ case projs of
             [] => root
-            _  => PPostfixProjs (boundToFC fname b) root projs
+            _  => PPostfixApp (boundToFC fname b) root projs
+    <|> do
+          b <- bounds (some postfixProj)
+          pure $ PPostfixAppPartial (boundToFC fname b) b.val
 
   simplerExpr : FileName -> IndentInfo -> Rule PTerm
   simplerExpr fname indents
@@ -631,12 +632,13 @@ mutual
     where
       fieldName : Name -> String
       fieldName (UN s) = s
+      fieldName (RF s) = s
       fieldName _ = "_impossible"
 
       -- this allows the dotted syntax .field
       -- but also the arrowed syntax ->field for compatibility with Idris 1
       recFieldCompat : Rule Name
-      recFieldCompat = dotIdent <|> (symbol "->" *> name)
+      recFieldCompat = postfixProj <|> (symbol "->" *> name)
 
   rewrite_ : FileName -> IndentInfo -> Rule PTerm
   rewrite_ fname indents
@@ -932,7 +934,6 @@ onoff
 extension : Rule LangExt
 extension
     = (exactIdent "ElabReflection" *> pure ElabReflection)
-  <|> (exactIdent "PostfixProjections" *> pure PostfixProjections)
   <|> (exactIdent "Borrowing" *> pure Borrowing)
 
 totalityOpt : Rule TotalReq
@@ -964,6 +965,10 @@ directive fname indents
          b <- onoff
          atEnd indents
          pure (UnboundImplicits b)
+  <|> do pragma "prefix_record_projections"
+         b <- onoff
+         atEnd indents
+         pure (PrefixRecordProjections b)
   <|> do pragma "ambiguity_depth"
          lvl <- intLit
          atEnd indents
diff --git a/src/Idris/Pretty.idr b/src/Idris/Pretty.idr
index e26724fe7..d3fd8c481 100644
--- a/src/Idris/Pretty.idr
+++ b/src/Idris/Pretty.idr
@@ -277,10 +277,10 @@ mutual
       go d (PRangeStream _ start (Just next)) =
         brackets (go startPrec start <+> comma <++> go startPrec next <++> pretty "..")
       go d (PUnifyLog _ lvl tm) = go d tm
-      go d (PPostfixProjs fc rec fields) =
-        parenthesise (d > appPrec) $ go startPrec rec <++> dot <+> concatWith (surround dot) (go startPrec <$> fields)
-      go d (PPostfixProjsSection fc fields args) =
-        parens (dot <+> concatWith (surround dot) (go startPrec <$> fields) <+> fillSep (go appPrec <$> args))
+      go d (PPostfixApp fc rec fields) =
+        parenthesise (d > appPrec) $ go startPrec rec <++> dot <+> concatWith (surround dot) (map pretty fields)
+      go d (PPostfixAppPartial fc fields) =
+        parens (dot <+> concatWith (surround dot) (map pretty fields))
       go d (PWithUnambigNames fc ns rhs) = parenthesise (d > appPrec) $ group $ with_ <++> pretty ns <+> line <+> go startPrec rhs
 
 export
diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr
index 58848b7ca..95980c98c 100644
--- a/src/Idris/Syntax.idr
+++ b/src/Idris/Syntax.idr
@@ -93,10 +93,10 @@ mutual
        PRange : FC -> PTerm -> Maybe PTerm -> PTerm -> PTerm
        -- A stream range [x,y..]
        PRangeStream : FC -> PTerm -> Maybe PTerm -> PTerm
-       -- r.x.y, equivalent to (y (x r))
-       PPostfixProjs : FC -> PTerm -> List PTerm -> PTerm
-       -- (.x.y p q), equivalent to (\r => r.x.y p q)
-       PPostfixProjsSection : FC -> List PTerm -> List PTerm -> PTerm
+       -- r.x.y
+       PPostfixApp : FC -> PTerm -> List Name -> PTerm
+       -- .x.y
+       PPostfixAppPartial : FC -> List Name -> PTerm
 
        -- Debugging
        PUnifyLog : FC -> LogLevel -> PTerm -> PTerm
@@ -150,8 +150,8 @@ mutual
   getPTermLoc (PRewrite fc _ _) = fc
   getPTermLoc (PRange fc _ _ _) = fc
   getPTermLoc (PRangeStream fc _ _) = fc
-  getPTermLoc (PPostfixProjs fc _ _) = fc
-  getPTermLoc (PPostfixProjsSection fc _ _) = fc
+  getPTermLoc (PPostfixApp fc _ _) = fc
+  getPTermLoc (PPostfixAppPartial fc _) = fc
   getPTermLoc (PUnifyLog fc _ _) = fc
   getPTermLoc (PWithUnambigNames fc _ _) = fc
 
@@ -237,6 +237,7 @@ mutual
        Overloadable : Name -> Directive
        Extension : LangExt -> Directive
        DefaultTotality : TotalReq -> Directive
+       PrefixRecordProjections : Bool -> Directive
        AutoImplicitDepth : Nat -> Directive
 
   public export
@@ -602,13 +603,10 @@ mutual
     showPrec d (PRangeStream _ start (Just next))
         = "[" ++ showPrec d start ++ ", " ++ showPrec d next ++ " .. ]"
     showPrec d (PUnifyLog _ _ tm) = showPrec d tm
-    showPrec d (PPostfixProjs fc rec fields)
+    showPrec d (PPostfixApp fc rec fields)
         = showPrec d rec ++ concatMap (\n => "." ++ show n) fields
-    showPrec d (PPostfixProjsSection fc fields args)
-        = "("
-            ++ concatMap (\n => "." ++ show n) fields
-            ++ concatMap (\x => " " ++ showPrec App x) args
-            ++ ")"
+    showPrec d (PPostfixAppPartial fc fields)
+        = concatMap (\n => "." ++ show n) fields
     showPrec d (PWithUnambigNames fc ns rhs)
         = "with " ++ show ns ++ " " ++ showPrec d rhs
 
@@ -906,12 +904,11 @@ mapPTermM f = goPTerm where
     goPTerm (PUnifyLog fc k x) =
       PUnifyLog fc k <$> goPTerm x
       >>= f
-    goPTerm (PPostfixProjs fc rec fields) =
-      PPostfixProjs fc <$> goPTerm rec <*> pure fields
-      >>= f
-    goPTerm (PPostfixProjsSection fc fields args) =
-      PPostfixProjsSection fc fields <$> goPTerms args
+    goPTerm (PPostfixApp fc rec fields) =
+      PPostfixApp fc <$> goPTerm rec <*> pure fields
       >>= f
+    goPTerm (PPostfixAppPartial fc fields) =
+      f (PPostfixAppPartial fc fields)
     goPTerm (PWithUnambigNames fc ns rhs) =
       PWithUnambigNames fc ns <$> goPTerm rhs
       >>= f
diff --git a/src/Parser/Rule/Source.idr b/src/Parser/Rule/Source.idr
index 852681419..735f548ff 100644
--- a/src/Parser/Rule/Source.idr
+++ b/src/Parser/Rule/Source.idr
@@ -96,8 +96,8 @@ aDotIdent = terminal "Expected dot+identifier"
 
 
 export
-dotIdent : Rule Name
-dotIdent = UN <$> aDotIdent
+postfixProj : Rule Name
+postfixProj = RF <$> aDotIdent
 
 export
 symbol : String -> Rule ()
@@ -215,12 +215,12 @@ name = opNonNS <|> do
       else pure $ mkNamespacedName ns x
 
   opNonNS : Rule Name
-  opNonNS = symbol "(" *> operator <* symbol ")"
+  opNonNS = symbol "(" *> (operator <|> postfixProj) <* symbol ")"
 
   opNS : Namespace -> Rule Name
   opNS ns = do
     symbol ".("
-    n <- operator
+    n <- (operator <|> postfixProj)
     symbol ")"
     pure (NS ns n)
 
diff --git a/src/TTImp/ProcessRecord.idr b/src/TTImp/ProcessRecord.idr
index 0ef0b60af..10505ca3b 100644
--- a/src/TTImp/ProcessRecord.idr
+++ b/src/TTImp/ProcessRecord.idr
@@ -47,16 +47,21 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
          defs <- get Ctxt
          Just conty <- lookupTyExact conName (gamma defs)
              | Nothing => throw (InternalError ("Adding " ++ show tn ++ "failed"))
+
          -- Go into new namespace, if there is one, for getters
          case newns of
               Nothing =>
-                      elabGetters conName 0 [] [] conty -- make projections
+                   do elabGetters conName 0 [] RF [] conty -- make postfix projections
+                      when !isPrefixRecordProjections $
+                        elabGetters conName 0 [] UN [] conty -- make prefix projections
               Just ns =>
                    do let cns = currentNS defs
                       let nns = nestedNS defs
                       extendNS (mkNamespace ns)
                       newns <- getNS
-                      elabGetters conName 0 [] [] conty -- make projections
+                      elabGetters conName 0 [] RF [] conty -- make postfix projections
+                      when !isPrefixRecordProjections $
+                        elabGetters conName 0 [] UN [] conty -- make prefix projections
                       defs <- get Ctxt
                       -- Record that the current namespace is allowed to look
                       -- at private names in the nested namespace
@@ -122,17 +127,18 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
                   List (Name, RawImp) -> -- names to update in types
                     -- (for dependent records, where a field's type may depend
                     -- on an earlier projection)
+                  (mkProjName : String -> Name) ->
                   Env Term vs -> Term vs ->
                   Core ()
-    elabGetters con done upds tyenv (Bind bfc n b@(Pi _ rc imp ty_chk) sc)
+    elabGetters con done upds mkProjName tyenv (Bind bfc n b@(Pi _ rc imp ty_chk) sc)
         = if (n `elem` map fst params) || (n `elem` vars)
              then elabGetters con
                               (if imp == Explicit && not (n `elem` vars)
                                   then S done else done)
-                              upds (b :: tyenv) sc
+                              upds mkProjName (b :: tyenv) sc
              else
                 do let fldNameStr = nameRoot n
-                   projNameNS <- inCurrentNS (UN fldNameStr)
+                   projNameNS <- inCurrentNS (mkProjName fldNameStr)
 
                    ty <- unelab tyenv ty_chk
                    let ty' = substNames vars upds ty
@@ -173,9 +179,9 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
                    elabGetters con
                                (if imp == Explicit
                                    then S done else done)
-                               upds' (b :: tyenv) sc
+                               upds' mkProjName (b :: tyenv) sc
 
-    elabGetters con done upds _ _ = pure ()
+    elabGetters con done upds _ _ _ = pure ()
 
 export
 processRecord : {vars : _} ->
diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr
index 5c0d6cb49..938028242 100644
--- a/src/TTImp/TTImp.idr
+++ b/src/TTImp/TTImp.idr
@@ -561,6 +561,7 @@ definedInBlock ns decls =
            UN _ => NS ns n
            MN _ _ => NS ns n
            DN _ _ => NS ns n
+           RF _ => NS ns n
            _ => n
 
     defName : Namespace -> ImpDecl -> List Name
@@ -576,11 +577,25 @@ definedInBlock ns decls =
         fldns' : Namespace
         fldns' = maybe ns (\ f => ns <.> mkNamespace f) fldns
 
+        toRF : Name -> Name
+        toRF (UN n) = RF n
+        toRF n = n
+
         fnsUN : List Name
         fnsUN = map getFieldName flds
 
+        fnsRF : List Name
+        fnsRF = map toRF fnsUN
+
+        -- Depending on %prefix_record_projections,
+        -- the record may or may not produce prefix projections (fnsUN).
+        --
+        -- However, since definedInBlock is pure, we can't check that flag
+        -- (and it would also be wrong if %prefix_record_projections appears
+        -- inside the parameter block)
+        -- so let's just declare all of them and some may go unused.
         all : List Name
-        all = expandNS ns n :: map (expandNS fldns') fnsUN
+        all = expandNS ns n :: map (expandNS fldns') (fnsRF ++ fnsUN)
 
     defName _ _ = []
 
diff --git a/src/Text/Lexer/Core.idr b/src/Text/Lexer/Core.idr
index 55a562365..15c007520 100644
--- a/src/Text/Lexer/Core.idr
+++ b/src/Text/Lexer/Core.idr
@@ -171,12 +171,12 @@ tokenise pred line col acc tmap str
 export
 lex : TokenMap a -> String -> (List (WithBounds a), (Int, Int, String))
 lex tmap str
-    = let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (unpack str) in
+    = let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (fastUnpack str) in
           (ts, (l, c, fastPack str'))
 
 export
 lexTo : (WithBounds a -> Bool) ->
         TokenMap a -> String -> (List (WithBounds a), (Int, Int, String))
 lexTo pred tmap str
-    = let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (unpack str) in
+    = let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (fastUnpack str) in
           (ts, (l, c, fastPack str'))
diff --git a/support/c/Makefile b/support/c/Makefile
index 2732627fb..f7831faaa 100644
--- a/support/c/Makefile
+++ b/support/c/Makefile
@@ -52,4 +52,7 @@ cleandep: clean
 
 install: build
 	mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/lib
-	install $(LIBTARGET) $(DYLIBTARGET) *.h ${PREFIX}/idris2-${IDRIS2_VERSION}/lib
+	mkdir -p ${PREFIX}/idris2-${IDRIS2_VERSION}/include
+	install -m 755 $(DYLIBTARGET) ${PREFIX}/idris2-${IDRIS2_VERSION}/lib
+	install -m 644 $(LIBTARGET)   ${PREFIX}/idris2-${IDRIS2_VERSION}/lib
+	install -m 644 *.h            ${PREFIX}/idris2-${IDRIS2_VERSION}/include
diff --git a/support/c/idris_buffer.c b/support/c/idris_buffer.c
index 88fa33f3d..92ff8f18e 100644
--- a/support/c/idris_buffer.c
+++ b/support/c/idris_buffer.c
@@ -4,7 +4,7 @@
 
 typedef struct {
     int size;
-    uint8_t data[0];
+    uint8_t data[];
 } Buffer;
 
 void* idris2_newBuffer(int bytes) {
@@ -46,13 +46,17 @@ void idris2_setBufferByte(void* buffer, int loc, int byte) {
     }
 }
 
-void idris2_setBufferInt(void* buffer, int loc, int val) {
+void idris2_setBufferInt(void* buffer, int loc, int64_t val) {
     Buffer* b = buffer;
     if (loc >= 0 && loc+3 < b->size) {
-        b->data[loc] = val & 0xff;
-        b->data[loc+1] = (val >> 8) & 0xff;
+        b->data[loc  ] =  val        & 0xff;
+        b->data[loc+1] = (val >>  8) & 0xff;
         b->data[loc+2] = (val >> 16) & 0xff;
         b->data[loc+3] = (val >> 24) & 0xff;
+        b->data[loc+4] = (val >> 32) & 0xff;
+        b->data[loc+5] = (val >> 40) & 0xff;
+        b->data[loc+6] = (val >> 48) & 0xff;
+        b->data[loc+7] = (val >> 56) & 0xff;
     }
 }
 
@@ -77,7 +81,7 @@ void idris2_setBufferString(void* buffer, int loc, char* str) {
     }
 }
 
-int idris2_getBufferByte(void* buffer, int loc) {
+uint8_t idris2_getBufferByte(void* buffer, int loc) {
     Buffer* b = buffer;
     if (loc >= 0 && loc < b->size) {
         return b->data[loc];
@@ -86,13 +90,14 @@ int idris2_getBufferByte(void* buffer, int loc) {
     }
 }
 
-int idris2_getBufferInt(void* buffer, int loc) {
+int64_t idris2_getBufferInt(void* buffer, int loc) {
     Buffer* b = buffer;
-    if (loc >= 0 && loc+3 < b->size) {
-        return b->data[loc] +
-               (b->data[loc+1] << 8) +
-               (b->data[loc+2] << 16) +
-               (b->data[loc+3] << 24);
+    if (loc >= 0 && loc+7 < b->size) {
+        int64_t result = 0;
+        for (size_t i=0; i<8; i++) {
+            result |= b->data[loc + i] << (8 * i);
+        }
+        return result;
     } else {
         return 0;
     }
@@ -124,10 +129,10 @@ char* idris2_getBufferString(void* buffer, int loc, int len) {
     return rs;
 }
 
-int idris2_readBufferData(FILE* h, char* buffer, int loc, int max) {
+size_t idris2_readBufferData(FILE* h, char* buffer, size_t loc, size_t max) {
     return fread(buffer+loc, sizeof(uint8_t), (size_t)max, h);
 }
 
-int idris2_writeBufferData(FILE* h, char* buffer, int loc, int len) {
+size_t idris2_writeBufferData(FILE* h, const char* buffer, size_t loc, size_t len) {
     return fwrite(buffer+loc, sizeof(uint8_t), len, h);
 }
diff --git a/support/c/idris_buffer.h b/support/c/idris_buffer.h
index dc20d656f..865c0ba84 100644
--- a/support/c/idris_buffer.h
+++ b/support/c/idris_buffer.h
@@ -11,7 +11,7 @@ void idris2_freeBuffer(void* buf);
 int idris2_getBufferSize(void* buffer);
 
 void idris2_setBufferByte(void* buffer, int loc, int byte);
-void idris2_setBufferInt(void* buffer, int loc, int val);
+void idris2_setBufferInt(void* buffer, int loc, int64_t val);
 void idris2_setBufferDouble(void* buffer, int loc, double val);
 void idris2_setBufferString(void* buffer, int loc, char* str);
 
@@ -19,11 +19,12 @@ void idris2_copyBuffer(void* from, int start, int len,
                        void* to, int loc);
 
 // Reading and writing the raw data, to the pointer in the buffer
-int idris2_readBufferData(FILE* h, char* buffer, int loc, int max);
-int idris2_writeBufferData(FILE* h, char* buffer, int loc, int len);
+size_t idris2_readBufferData(FILE* h, char* buffer, size_t loc, size_t max);
+size_t idris2_writeBufferData(FILE* h, const char* buffer, size_t loc, size_t len);
 
-int idris2_getBufferByte(void* buffer, int loc);
-int idris2_getBufferInt(void* buffer, int loc);
+
+uint8_t idris2_getBufferByte(void* buffer, int loc);
+int64_t idris2_getBufferInt(void* buffer, int loc);
 double idris2_getBufferDouble(void* buffer, int loc);
 char* idris2_getBufferString(void* buffer, int loc, int len);
 
diff --git a/support/c/idris_net.c b/support/c/idris_net.c
index de6f4d4e2..f708254ab 100644
--- a/support/c/idris_net.c
+++ b/support/c/idris_net.c
@@ -76,6 +76,23 @@ int idrnet_socket(int domain, int type, int protocol) {
     return socket(domain, type, protocol);
 }
 
+// Get the address family constants out of C and into Idris
+int idrnet_af_unspec() {
+    return AF_UNSPEC;
+}
+
+int idrnet_af_unix() {
+    return AF_UNIX;
+}
+
+int idrnet_af_inet() {
+    return AF_INET;
+}
+
+int idrnet_af_inet6() {
+    return AF_INET6;
+}
+
 // We call this from quite a few functions. Given a textual host and an int port,
 // populates a struct addrinfo.
 int idrnet_getaddrinfo(struct addrinfo** address_res, char* host, int port,
diff --git a/support/c/idris_net.h b/support/c/idris_net.h
index e600670d8..bf8adf003 100644
--- a/support/c/idris_net.h
+++ b/support/c/idris_net.h
@@ -39,6 +39,12 @@ int idrnet_errno();
 
 int idrnet_socket(int domain, int type, int protocol);
 
+// Address family accessors
+int idrnet_af_unspec(void);
+int idrnet_af_unix(void);
+int idrnet_af_inet(void);
+int idrnet_af_inet6(void);
+
 // Bind
 int idrnet_bind(int sockfd, int family, int socket_type, char* host, int port);
 
diff --git a/support/chez/support.ss b/support/chez/support.ss
index 7bda49eed..0cfbf3dbb 100644
--- a/support/chez/support.ss
+++ b/support/chez/support.ss
@@ -66,8 +66,13 @@
   (if (= (vector-ref xs 0) 0)
     '()
     (cons (vector-ref xs 1) (from-idris-list (vector-ref xs 2)))))
-(define (string-concat xs) (apply string-append (from-idris-list xs)))
 (define (string-pack xs) (apply string (from-idris-list xs)))
+(define (to-idris-list-rev acc xs)
+  (if (null? xs)
+    acc
+    (to-idris-list-rev (vector 1 (car xs) acc) (cdr xs))))
+(define (string-unpack s) (to-idris-list-rev (vector 0) (reverse (string->list s))))
+(define (string-concat xs) (apply string-append (from-idris-list xs)))
 (define string-cons (lambda (x y) (string-append (string x) y)))
 (define get-tag (lambda (x) (vector-ref x 0)))
 (define string-reverse (lambda (x)
@@ -81,6 +86,14 @@
               ""
               (substring s b end))))
 
+(define (blodwen-string-iterator-new s)
+  0)
+
+(define (blodwen-string-iterator-next s ofs)
+  (if (>= ofs (string-length s))
+      (vector 0)  ; EOF
+      (vector 1 (string-ref s ofs) (+ ofs 1))))
+
 (define either-left
   (lambda (x)
     (vector 0 x)))
diff --git a/support/gambit/support.scm b/support/gambit/support.scm
index 76d1e6c28..f5e22d5df 100644
--- a/support/gambit/support.scm
+++ b/support/gambit/support.scm
@@ -72,11 +72,16 @@
   (if (= (vector-ref xs 0) 0)
     '()
     (cons (vector-ref xs 1) (from-idris-list (vector-ref xs 2)))))
-(define-macro (string-concat xs)
-  `(apply string-append (from-idris-list ,xs)))
 
 (define-macro (string-pack xs)
   `(apply string (from-idris-list ,xs)))
+(define (to-idris-list-rev acc xs)
+  (if (null? xs)
+    acc
+    (to-idris-list-rev (vector 1 (car xs) acc) (cdr xs))))
+(define (string-unpack s) (to-idris-list-rev (vector 0) (reverse (string->list s))))
+(define-macro (string-concat xs)
+  `(apply string-append (from-idris-list ,xs)))
 
 (define-macro (string-cons x y)
   `(string-append (string ,x) ,y))
@@ -93,6 +98,14 @@
 
 (define-macro (get-tag x) `(vector-ref ,x 0))
 
+(define (blodwen-string-iterator-new s)
+  0)
+
+(define (blodwen-string-iterator-next s ofs)
+  (if (>= ofs (string-length s))
+      (vector 0)  ; EOF
+      (vector 1 (string-ref s ofs) (+ ofs 1))))
+
 ;; These two are only used in this file
 (define-macro (either-left x) `(vector 0 ,x))
 (define-macro (either-right x) `(vector 1 ,x))
diff --git a/support/racket/support.rkt b/support/racket/support.rkt
index 2865e7b08..eaf7e808a 100644
--- a/support/racket/support.rkt
+++ b/support/racket/support.rkt
@@ -59,7 +59,12 @@
   (if (= (vector-ref xs 0) 0)
     '()
     (cons (vector-ref xs 1) (from-idris-list (vector-ref xs 2)))))
+(define (to-idris-list-rev acc xs)
+  (if (null? xs)
+    acc
+    (to-idris-list-rev (vector 1 (car xs) acc) (cdr xs))))
 (define (string-concat xs) (apply string-append (from-idris-list xs)))
+(define (string-unpack s) (to-idris-list-rev (vector 0) (reverse (string->list s))))
 (define (string-pack xs) (list->string (from-idris-list xs)))
 (define string-cons (lambda (x y) (string-append (string x) y)))
 (define get-tag (lambda (x) (vector-ref x 0)))
@@ -72,6 +77,14 @@
           (end (min l (+ b x))))
           (substring s b end)))
 
+(define (blodwen-string-iterator-new s)
+  0)
+
+(define (blodwen-string-iterator-next s ofs)
+  (if (>= ofs (string-length s))
+      (vector 0)  ; EOF
+      (vector 1 (string-ref s ofs) (+ ofs 1))))
+
 (define either-left
   (lambda (x)
     (vector 0 x)))
diff --git a/tests/ideMode/ideMode001/expected b/tests/ideMode/ideMode001/expected
index 47e53d12e..d6eb41823 100644
--- a/tests/ideMode/ideMode001/expected
+++ b/tests/ideMode/ideMode001/expected
@@ -2,13 +2,13 @@
 000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
 0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:258} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:259}_[]")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:258}_[] ?{_:259}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:295} a)")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:296}_[]")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:295}_[] ?{_:296}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:297}_[] ?{_:296}_[])")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:249}_[] ?{_:248}_[])")))))) 1)
-0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 7)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:239} : (Main.Vect n[0] a[1])) -> ({arg:240} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:7 n[2] m[4]) a[3]))))))")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:286}_[] ?{_:285}_[])")))))) 1)
+0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 7)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:276} : (Main.Vect n[0] a[1])) -> ({arg:277} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:7 n[2] m[4]) a[3]))))))")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
diff --git a/tests/ideMode/ideMode003/expected b/tests/ideMode/ideMode003/expected
index 0d0c9a019..3f8278cfb 100644
--- a/tests/ideMode/ideMode003/expected
+++ b/tests/ideMode/ideMode003/expected
@@ -2,13 +2,13 @@
 000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
 0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:258} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:259}_[]")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:258}_[] ?{_:259}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:295} a)")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:296}_[]")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:295}_[] ?{_:296}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:297}_[] ?{_:296}_[])")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:249}_[] ?{_:248}_[])")))))) 1)
-0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 7)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:239} : (Main.Vect n[0] a[1])) -> ({arg:240} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:7 n[2] m[4]) a[3]))))))")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:286}_[] ?{_:285}_[])")))))) 1)
+0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 7)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:276} : (Main.Vect n[0] a[1])) -> ({arg:277} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:7 n[2] m[4]) a[3]))))))")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
diff --git a/tests/idris2/record004/Main.idr b/tests/idris2/record004/Main.idr
index 5f35e06c4..d014ce86b 100644
--- a/tests/idris2/record004/Main.idr
+++ b/tests/idris2/record004/Main.idr
@@ -6,14 +6,34 @@ record Point where
   y : Double
 
 -- a record creates two projections:
+--
+-- .x : Point -> Double
+-- .y : Point -> Double
+--
+-- because %prefix_record_projections are on by default, we also get:
+--
 -- x : Point -> Double
 -- y : Point -> Double
 
+-- to prevent cluttering the ordinary name space with short identifiers
+%prefix_record_projections off
+
 record Rect where
   constructor MkRect
   topLeft : Point
   bottomRight : Point
 
+-- .topLeft : Rect -> Point
+-- .bottomRight : Rect -> Point
+--
+-- For Rect, we don't get the prefix projections:
+--
+-- Main> :t topLeft
+-- (interactive):1:4--1:11:Undefined name topLeft
+-- Main> :t .topLeft
+-- \{rec:0} => .topLeft rec : ?_ -> Point
+
+
 pt : Point
 pt = MkPoint 4.2 6.6
 
@@ -23,25 +43,46 @@ rect =
     (MkPoint 1.1 2.5)
     (MkPoint 4.3 6.3)
 
--- Foo.bar.baz with uppercase F is one lexeme: DotSepIdent ["baz", "bar", "Foo"]
+-- New lexical structure:
+--
+-- Foo.bar.baz with uppercase F is one lexeme: NSIdent ["baz", "bar", "Foo"]
 -- foo.bar.baz with lowercase f is three lexemes: foo, .bar, .baz
 -- .foo.bar.baz is three lexemes: .foo, .bar, .baz
 --
 -- If you want Constructor.field, you have to write (Constructor).field.
+--
+-- New syntax of simpleExpr:
+--
+-- Expressions binding tighter than application (simpleExpr),
+-- such as variables or parenthesised expressions,
+-- have been renamed to simplerExpr,
+-- and an extra layer of syntax has been inserted.
+-- 
+--   simpleExpr ::= (.field)+               -- parses as PPostfixAppPartial
+--                | simplerExpr (.field)+   -- parses as PPostfixApp
+--                | simplerExpr             -- (parses as whatever it used to)
+--
+-- (.foo) is a name, so you can use it to e.g. define a function called .foo (see .squared below)
+-- (.foo.bar) is a parenthesised expression
+--
+-- New desugaring rules
+--
+-- (.field1 .field2 .field3) desugars to (\x => .field3 (.field2 (.field1 x)))
+-- (simpleExpr .field1 .field2 .field3) desugars to ((.field .field2 .field3) simpleExpr).
+--
+-- There are more details such as namespacing; see below.
 
-add : Num a => a -> a -> a
-add x y = x + y
+-- user-defined projections work, too (should they?)
+(.squared) : Double -> Double
+(.squared) x = x * x
 
-oopFoldl : List a -> b -> (b -> a -> b) -> b
-oopFoldl xs z f = foldl f z xs
 
-bad : Double
-bad = 
-  rect.x.topLeft        -- should not throw errors
-  + rect.(x . topLeft)  -- disallowed without %language PostfixProjections
+-- #649: Forced patterns remain unaffected by postfix projections.
+test649 : (x, y : Bool) -> x = y -> Bool
+test649 .(x) x Refl = x
 
-bad2 : Double
-bad2 = (.oopFoldl 0 (+))  -- disallowed without %language PostfixProjections
 
-%language PostfixProjections
--- from now on, we can use complex projections
+-- #441: Locals do not shadow record projections.
+test441 : (Point -> Double) -> (Point -> Double) -> Point -> Double
+test441 x y pt = pt.x + pt.y
+  -- no ambiguity errors: the locals "x" and "y" are not considered in pt.x and pt.y
diff --git a/tests/idris2/record004/expected b/tests/idris2/record004/expected
index d60fe77d3..0bcedffdb 100644
--- a/tests/idris2/record004/expected
+++ b/tests/idris2/record004/expected
@@ -1,23 +1,10 @@
 1/1: Building Main (Main.idr)
-Error: complex postfix projections require %language PostfixProjections
-
-Main.idr:41:5--41:23
-    |
- 41 |   + rect.(x . topLeft)  -- disallowed without %language PostfixProjections
-    |     ^^^^^^^^^^^^^^^^^^
-
-Error: postfix projection sections require %language PostfixProjections
-
-Main.idr:44:9--44:24
-    |
- 44 | bad2 = (.oopFoldl 0 (+))  -- disallowed without %language PostfixProjections
-    |         ^^^^^^^^^^^^^^^
-
 Main> 4.2
 Main> 4.2
 Main> 10.8
 Main> 4.2
 Main> 4.2
+Main> 17.64
 Main> [1.1, 4.2]
 Main> Error: When unifying (?a -> ?b) -> ?f ?a -> ?f ?b and Point.
 Mismatch between: (?a -> ?b) -> ?f ?a -> ?f ?b and Point.
@@ -28,14 +15,11 @@ Mismatch between: (?a -> ?b) -> ?f ?a -> ?f ?b and Point.
    | ^^^
 
 Main> [2.5, 2.5]
-Main> 8.1
-Main> [8.1, 8.1]
-Main> 6
-Main> [6, 15]
 Main> 7.4
-Main> 7.4
-Main> 7.4
-Main> MkPoint 1.1 2.5
+Main> 4.2
+Main> 4.2
+Main> 4.2
+Main> 4.2
 Main> 4.2
 Main> 4.2
 Main> 4.2
diff --git a/tests/idris2/record004/input b/tests/idris2/record004/input
index a95b898ff..7f88e92eb 100644
--- a/tests/idris2/record004/input
+++ b/tests/idris2/record004/input
@@ -3,17 +3,15 @@ pt .x
 pt.x + pt.y
 (Main.pt).x
 (MkPoint pt.y pt.x).y
+pt.x.squared
 map (.x) [MkPoint 1.1 2.5, MkPoint 4.2 6.3]
 map .x [MkPoint 1 2, MkPoint 3 4]
 map (.topLeft.y) [rect, rect]
-rect.topLeft.x.add 7
-map (.topLeft.x.add 7) [rect, rect]
-[1,2,3].oopFoldl 0 $ \x, y => x + y
-map (.oopFoldl 0 (+)) [[1,2,3],[4,5,6]]
 rect.topLeft.x + rect.bottomRight.y
-rect.(x . topLeft) + rect.(y . bottomRight)
-x rect.topLeft + y rect.bottomRight
-rect.(Rect.topLeft)
+Main.Point.(.x) pt
+Point.(.x) pt
+(.x) pt
+.x pt
 Main.Point.x pt
 Point.x pt
 (x) pt
diff --git a/tests/idris2/reflection004/refdecl.idr b/tests/idris2/reflection004/refdecl.idr
index 7acbfdd3d..c22a65189 100644
--- a/tests/idris2/reflection004/refdecl.idr
+++ b/tests/idris2/reflection004/refdecl.idr
@@ -16,7 +16,7 @@ mkPoint n
     = let type = "Point" ++ show n ++ "D" in
       IRecord emptyFC Public
       (MkRecord emptyFC (NS (MkNS ["Main"]) (UN type)) [] (NS (MkNS ["Main"]) (UN ("Mk" ++ type)))
-        (toList $ map (\axis => MkIField emptyFC MW ExplicitArg (UN axis) `(Double)) (axes n)))
+        (toList $ map (\axis => MkIField emptyFC MW ExplicitArg (RF axis) `(Double)) (axes n)))
 
 logDecls : TTImp -> Elab (Int -> Int)
 logDecls v