diff --git a/GenerateEverything.hs b/GenerateEverything.hs
index b4356c6bf0..4327bf3ba0 100644
--- a/GenerateEverything.hs
+++ b/GenerateEverything.hs
@@ -50,6 +50,9 @@ unsafeModules = map modToFile
   , "Data.Bytestring.IO"
   , "Data.Bytestring.IO.Primitive"
   , "Data.Bytestring.Primitive"
+  , "Data.List.Unsafe.Instances"
+  , "Data.Maybe.Unsafe.Instances"
+  , "Data.Nat.Unsafe.Instances"
   , "Data.Word8.Base"
   , "Data.Word8.Literals"
   , "Data.Word8.Primitive"
@@ -109,6 +112,9 @@ isUnsafeModule fp =
 withKModules :: [FilePath]
 withKModules = map modToFile
   [ "Axiom.Extensionality.Heterogeneous"
+  , "Data.List.Unsafe.Instances"
+  , "Data.Maybe.Unsafe.Instances"
+  , "Data.Nat.Unsafe.Instances"
   , "Data.Star.BoundedVec"
   , "Data.Star.Decoration"
   , "Data.Star.Environment"
diff --git a/src/Data/Integer/Instances.agda b/src/Data/Integer/Instances.agda
index b43ad23e66..683668138e 100644
--- a/src/Data/Integer/Instances.agda
+++ b/src/Data/Integer/Instances.agda
@@ -8,10 +8,21 @@
 
 module Data.Integer.Instances where
 
+open import Data.Integer.Base using (ℤ)
 open import Data.Integer.Properties using (_≡?_; ≤-isDecTotalOrder)
+open import Data.Integer.Show using () renaming (show to showℤ)
+open import Data.List.Base using (_++_)
+open import Data.String.Base using (toList)
 open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
 
+open import Text.Write using (Write)
+
 instance
   ℤ-≡-isDecEquivalence = isDecEquivalence _≡?_
   ℤ-≤-isDecTotalOrder = ≤-isDecTotalOrder
+
+instance
+  open Write
+  IntWrite : Write ℤ
+  IntWrite .writesPrecList _ i str = toList (showℤ i) ++ str
diff --git a/src/Data/List/Instances.agda b/src/Data/List/Instances.agda
index 3f28c89185..cba8597ebc 100644
--- a/src/Data/List/Instances.agda
+++ b/src/Data/List/Instances.agda
@@ -8,7 +8,7 @@
 
 module Data.List.Instances where
 
-open import Data.List.Base using (List; []; _∷_)
+open import Data.List.Base using (List; []; _∷_; foldr)
 open import Data.List.Effectful
   using (functor; applicative; applicativeZero; alternative; monad
         ; monadZero; monadPlus)
@@ -22,6 +22,7 @@ open import Data.List.Relation.Binary.Pointwise
   using (Pointwise)
 open import Data.List.Relation.Binary.Lex.NonStrict
   using (Lex-≤; ≤-isDecTotalOrder)
+open import Data.Nat.Instances using (NatWrite)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
@@ -29,6 +30,7 @@ open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
 open import Relation.Binary.TypeClasses
   using (IsDecTotalOrder; IsDecEquivalence; _≈?_)
+open import Text.Write
 
 private
   variable
@@ -58,3 +60,22 @@ instance
                              → {{IsDecTotalOrder _≈_ _≼_}}
                              → IsDecTotalOrder (Pointwise _≈_) (Lex-≤ _≈_ _≼_)
   List-Lex-≤-isDecTotalOrder {{≼-isDecTotalOrder}} = ≤-isDecTotalOrder ≼-isDecTotalOrder
+
+------------------------------------------------------------------------
+-- List write
+
+open Write {{...}}
+
+instance
+  ListWrite : {{ Write A }} → Write (List A)
+  ListWrite .writesPrecList prec [] str = '[' ∷ (']' ∷ str)
+  ListWrite .writesPrecList prec (x ∷ xs) str = '[' ∷ writesPrecList prec x (listWrite' prec str xs)
+    where
+      -- after the first call, don't prepend '['
+      listWrite' : {{ Write A }} → Precedence → List Char → List A → List Char
+      listWrite' prec str = foldr (λ x str → ',' ∷ writesPrecList prec x str) (']' ∷ str)
+
+-- some examples to write the instances working
+private
+  test[ℕ] : String
+  test[ℕ] = write (5 ∷ 2 ∷ 12 ∷ 42 ∷ [])
diff --git a/src/Data/List/Unsafe/Instances.agda b/src/Data/List/Unsafe/Instances.agda
new file mode 100644
index 0000000000..39ee0cacd1
--- /dev/null
+++ b/src/Data/List/Unsafe/Instances.agda
@@ -0,0 +1,27 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Unsafe instances for List
+------------------------------------------------------------------------
+
+{-# OPTIONS --with-K #-}
+
+module Data.List.Unsafe.Instances where
+
+open import Data.List.Base
+open import Data.Nat.Base
+open import Data.Nat.Instances
+open import Level using (Level)
+open import Text.Write
+open import Text.Pretty 80
+
+private
+  variable
+    a : Level
+    A : Set a
+
+open Pretty {{...}}
+
+instance
+  ListPretty : {{ Pretty A }} → Pretty (List A)
+  ListPretty .pPrintPrec prec xs = parens (commaSep (map (pPrintPrec prec) xs))
diff --git a/src/Data/Maybe/Unsafe/Instances.agda b/src/Data/Maybe/Unsafe/Instances.agda
new file mode 100644
index 0000000000..1011efa9ef
--- /dev/null
+++ b/src/Data/Maybe/Unsafe/Instances.agda
@@ -0,0 +1,24 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Unsafe instances for Maybe
+------------------------------------------------------------------------
+
+{-# OPTIONS --with-K #-}
+
+module Data.Maybe.Unsafe.Instances where
+
+open import Data.Maybe.Base
+open import Text.Pretty 80
+open import Level using (Level)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+instance
+  open Pretty {{...}}
+  MaybePretty : {{ Pretty A }} → Pretty (Maybe A)
+  MaybePretty .pPrintPrec prec (just x) = (text "just") <+> pPrintPrec prec x
+  MaybePretty .pPrintPrec prec nothing = text "nothing"
diff --git a/src/Data/Nat/Instances.agda b/src/Data/Nat/Instances.agda
index efe7e48d3e..245151f83d 100644
--- a/src/Data/Nat/Instances.agda
+++ b/src/Data/Nat/Instances.agda
@@ -8,10 +8,32 @@
 
 module Data.Nat.Instances where
 
+open import Data.Char using (isDigit)
+open import Data.List.Base using (_++_; spanᵇ)
+open import Data.Maybe using (_>>=_; just)
+open import Data.Nat.Base using (ℕ; _≤ᵇ_)
 open import Data.Nat.Properties using (≤-isDecTotalOrder; _≡?_)
+open import Data.Nat.Show using (readMaybe) renaming (show to showℕ)
+open import Data.Product using (_,_)
+open import Data.String.Base using (toList; fromList)
 open import Relation.Binary.PropositionalEquality.Properties
   using (isDecEquivalence)
+open import Text.Read using (Read)
+open import Text.Write using (Write)
 
 instance
   ℕ-≡-isDecEquivalence = isDecEquivalence _≡?_
   ℕ-≤-isDecTotalOrder = ≤-isDecTotalOrder
+
+instance
+  open Write
+  NatWrite : Write ℕ
+  NatWrite .writesPrecList _ n str = (toList (showℕ n)) ++ str
+
+instance
+  open Read {{...}}
+  NatRead : Read ℕ
+  NatRead .readsPrecList prec str = do
+    let (digits , leftover) = spanᵇ isDigit str
+    num ← readMaybe 10 (fromList digits)
+    just (num , leftover)
diff --git a/src/Data/Nat/Unsafe/Instances.agda b/src/Data/Nat/Unsafe/Instances.agda
new file mode 100644
index 0000000000..1b0f89f14f
--- /dev/null
+++ b/src/Data/Nat/Unsafe/Instances.agda
@@ -0,0 +1,18 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Unsafe instances for Nat
+------------------------------------------------------------------------
+
+{-# OPTIONS --with-K #-}
+
+module Data.Nat.Unsafe.Instances where
+
+open import Data.Nat.Base
+open import Data.Nat.Show using (show)
+open import Text.Pretty 80
+
+instance
+  open Pretty {{...}}
+  ℕPretty : Pretty ℕ
+  ℕPretty .pPrintPrec prec n = text (show n)
diff --git a/src/Text/Pretty.agda b/src/Text/Pretty.agda
index a9202b1f82..f305a3f4ec 100644
--- a/src/Text/Pretty.agda
+++ b/src/Text/Pretty.agda
@@ -12,6 +12,7 @@ open import Data.Nat.Base using (ℕ)
 
 module Text.Pretty (width : ℕ) where
 
+open import Agda.Builtin.Reflection using (Precedence) public
 import Level
 open import Data.Char.Base using (Char)
 open import Data.List.Base
@@ -137,3 +138,20 @@ commaSep = foldDoc (λ d e → d <> comma <+> e)
 
 newline : Doc
 newline = flush empty
+
+------------------------------------------------------------------------
+-- Pretty class
+
+private
+  variable
+    a : Level.Level
+
+record Pretty (A : Set a) : Set a where
+  field
+    pPrintPrec : Precedence → A → Doc
+
+  pPrint : A → Doc
+  pPrint = pPrintPrec Precedence.unrelated
+
+  pretty : A → String
+  pretty = render ∘ pPrint
diff --git a/src/Text/Read.agda b/src/Text/Read.agda
new file mode 100644
index 0000000000..99bcde109e
--- /dev/null
+++ b/src/Text/Read.agda
@@ -0,0 +1,41 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Read class
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe  #-}
+
+module Text.Read where
+
+-- should builtin be used?
+open import Agda.Builtin.Reflection using (Precedence) public
+open import Data.Char.Base using (Char) public
+open import Data.List.Base using (List; []; _++_; _∷_)
+open import Data.Maybe.Base using (Maybe; just; nothing; map)
+open import Data.Product.Base using (_×_; _,_; proj₁) renaming (map to map×)
+open import Data.String.Base using (String) public
+open import Data.String.Base using (fromList; toList)
+open import Function.Base using (_∘_; const; _$_; id)
+open import Level using (Level)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+record Read (A : Set a) : Set a where
+  field
+    readsPrecList : Precedence → List Char → Maybe (A × List Char)
+
+  readPrecList : Precedence → List Char → Maybe A
+  readPrecList prec str = map proj₁ (readsPrecList prec str)
+
+  readsPrec : Precedence → String → Maybe (A × String)
+  readsPrec prec str = map (map× id fromList) (readsPrecList prec (toList str))
+
+  readPrec : Precedence → String → Maybe A
+  readPrec prec = (readPrecList prec) ∘ toList
+
+  read : String → Maybe A
+  read = readPrec Precedence.unrelated
diff --git a/src/Text/ReadWrite.agda b/src/Text/ReadWrite.agda
new file mode 100644
index 0000000000..da8fff8cfb
--- /dev/null
+++ b/src/Text/ReadWrite.agda
@@ -0,0 +1,40 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- ReadWrite class
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe  #-}
+
+module Text.ReadWrite where
+
+-- should builtin be used?
+open import Agda.Builtin.Reflection using (Precedence) public
+open import Data.Char.Base using (Char) public
+open import Data.List.Base using (List; []; _++_; _∷_)
+open import Data.Nat.Show using () renaming (show to showℕ)
+open import Data.Maybe.Base using (just)
+open import Data.String.Base using (String) public
+open import Data.String.Base using (fromList; toList)
+open import Function.Base using (_∘_; const; _$_)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Text.Write using (Write)
+open import Text.Read using (Read)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+record ReadWrite (A : Set a) :  Set a where
+  open Read
+  open Write
+
+  field
+    reader : Read A
+    writer : Write A
+
+    readWrite : ∀ {x : A} → read reader (write writer x) ≡ (just x)
+    writeRead : ∀ {x : A} {s : String} → (read reader s) ≡ (just x) → writeMaybe writer (read reader s) ≡ s
+
diff --git a/src/Text/Write.agda b/src/Text/Write.agda
new file mode 100644
index 0000000000..acfdf04866
--- /dev/null
+++ b/src/Text/Write.agda
@@ -0,0 +1,46 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Write class
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe  #-}
+
+module Text.Write where
+
+-- should builtin be used?
+open import Agda.Builtin.Reflection using (Precedence) public
+open import Data.Char.Base using (Char) public
+open import Data.List.Base using (List; []; _++_; _∷_)
+open import Data.Maybe.Base using (Maybe; just; nothing)
+open import Data.Nat.Show using () renaming (show to showℕ)
+open import Data.String.Base using (String) public
+open import Data.String.Base using (fromList; toList)
+open import Function.Base using (_∘_; const; _$_)
+open import Level using (Level)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+record Write (A : Set a) :  Set a where
+  constructor mkWrite
+  field
+    writesPrecList :  Precedence → A → List Char → List Char
+
+  writePrecList : Precedence → A → List Char
+  writePrecList prec x =  writesPrecList prec x []
+
+  writesPrec : Precedence → A → String → String
+  writesPrec prec x str = fromList (writesPrecList prec x (toList str))
+
+  writePrec : Precedence → A → String
+  writePrec prec x = fromList (writesPrecList prec x [])
+
+  write : A → String
+  write = writePrec Precedence.unrelated
+
+  writeMaybe : Maybe A → String
+  writeMaybe nothing = ""
+  writeMaybe (just x) = write x
diff --git a/src/Text/Write/Deriving.agda b/src/Text/Write/Deriving.agda
new file mode 100644
index 0000000000..25a181084c
--- /dev/null
+++ b/src/Text/Write/Deriving.agda
@@ -0,0 +1,467 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Macro for deriving instances of Write
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+-- NOTE: still figuring things out, just pushing to get over to other device
+
+module Text.Write.Deriving where
+
+-- Much understanding and structure taken from
+--   ∙ https://github.com/UlfNorell/agda-prelude/blob/master/src/Tactic/Deriving/Eq.agda
+--   ∙ https://github.com/alhassy/gentle-intro-to-reflection
+
+open import Data.Bool.Base using (Bool; false; true; if_then_else_)
+open import Data.Char.Properties using (_≡?_)
+open import Data.List.Base using (_∷_; []; [_]; List; concat; _++_; zip; wordsBy; length; map)
+open import Data.List.Effectful
+open import Data.Maybe.Base using (just; nothing; fromMaybe; Maybe) renaming (_>>=_ to _>>=Maybe_)
+open import Data.Nat.Base using (ℕ; _+_; ∣_-_∣′)
+open import Data.Nat.Instances
+open TraversableM using (mapM)
+open import Data.String.Base using (toList; fromList; String) renaming (_++_ to _++s_)
+open import Data.Unit using (⊤)
+open import Data.Product.Base using (_×_; _,_; uncurry; proj₁; proj₂)
+open import Function.Base using (_∘_)
+open import Reflection
+open import Reflection.AST.Show using (showName)
+open import Reflection.AST.Term using (Telescope; Clause; unknown; getName)
+open import Reflection.AST.Meta using (showMeta)
+open import Reflection.AST.Name using (_≡ᵇ_)
+open import Reflection.AST.Argument using (iArg; unArg)
+open import Reflection.TCM
+open import Reflection.TCM.Effectful using () renaming (monad to monadTCM)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Text.Write using (Write; Char; Precedence)
+
+open import Level using (Level; suc; zero)
+  
+data Test : Set where
+  a_-_-_ : ℕ → ℕ → ℕ → Test
+  a' : Test
+  a'' : {!!}
+
+{-
+Should this be placed in Tactic.DerivingWrite?
+
+For now, some notes on design:
+
+Should print syntactically correct Agda that can be read by
+an also derived Read instance.
+
+Steps:
+1. Check term is actually a data/record definition, if not throw typecheck error?
+2. Get all parameters and attach required instances to the resulting function type
+
+   only need instances for types within constructors, e.g.
+
+   data {a : Level} {A : Set} → MyData A : Set a where
+     c : A → A → MyData A
+
+   needs to have
+
+   {a : Level} {A : Set} {{ Write A }} → Write (List A)
+
+   NOT
+
+   {a : Level} {A : Set} {{ Write a }} {{ Write A }} → Write (List A)
+
+3. Create a pat-lam for the record field of Write, but use outer de Bruijn indices
+   to fetch write instances
+
+   When writing values of a constructor, recursively call write on them. For
+   other types, use a map of instances for de Bruijn indices. But for the current type
+   (in the case of induction), the name of the defined function must be used.
+
+   NOTE: map return an arg instead of a nat 
+
+4. For data types, create a clause for each constructor and produce a pat-lam out of it
+
+OUTPUT:
+
+For records, print in record syntax (record { x = y, ... }), recursively
+   calling write on fields
+
+For data, get fixity of constructor and recursively call write, intertwining
+   parts of the constructors name in a way that properly aligns with fixity
+
+   (e.g. print x ∷ [] as "x ∷ []", not "_∷_ x []")
+
+Reflection notes:
+- Prelude has a lot of machinery that should be moved over
+- Should derive *own* type so we know the exact order things are in
+- WRONG
+- Clause takes telescope of arguments (i.e. the type of the given function without the return value)
+  AND a list of patterns applied to those arguments. If no pattern matching is applied, just the
+  deBruijin index within a var pattern should be given.
+- Pat lam for pattern matching, lam for normal
+- Instances can't be handled as arguments in pat-lam, but can in lam
+- Recursion can't be done within a lam. Must define a top level name and refer to that
+
+Instance Notes:
+- Recursive calls have to be handled in a helper function, whose type signature
+  is the type of the field in Write. 
+-}
+
+------------------------------------------------------------------------
+-- List Char utils
+
+last : {a : Level} {A : Set a} → A → List A → A
+last x [] = x
+last x (y ∷ ys) = last y ys
+
+unqualify : List Char → List Char
+unqualify str = last str (wordsBy (_≡?_ '.') str)
+
+------------------------------------------------------------------------
+-- Machinery for deriving things
+
+telView : Type → Telescope × Type
+telView (pi x (abs y b)) = ((y , x) ∷ (proj₁ telVb)) , proj₂ telVb
+  where
+    telVb : Telescope × Type
+    telVb = telView b
+{-# CATCHALL #-}
+telView x                = [] , x
+
+getTel : Type → Telescope
+getTel = proj₁ ∘ telView
+
+getCore : Type → Type
+getCore = proj₂ ∘ telView
+
+-- Construct a Type out of a Telescope and Core Type
+telToType : Telescope → Type → Type
+telToType tel core = {!!}
+
+-- Return a list of all types that appear in a list of constructors in order of appearance
+conArgTypes : Type → List Type
+conArgTypes t = map (unArg ∘ proj₂) (getTel t)
+
+instanceArg : Arg Name
+instanceArg = arg (arg-info instance′ defaultModality) (quote Write)
+
+-- Derive the telescope for the type of an instance,
+--
+-- e.g. for Write List this returns
+--      {a : Level} {A : Set a} {{ Write A }}
+instanceTel : Name → Name → TC Telescope
+instanceTel cls inst = {!!}
+
+-- Derive the type of an instance for a given record type,
+-- prepending all required instances to the telescope
+--
+-- e.g. for Write (List), will give
+--      : {{ Write A }} → Write (List A)
+instanceType : Name → Name → TC Type
+instanceType cls inst = do
+  clsT ← getType cls
+  instT ← getType inst
+  tel ← instanceTel cls inst
+  pure (telToType tel {!!})
+
+telStr : Telescope → List ErrorPart
+telStr [] = strErr "[]" ∷ []
+telStr ((nm , arg i t) ∷ xs) = strErr nm ∷ termErr t ∷ (telStr xs)
+
+-- NOTE: a lot of these are likely already defined somewhere
+
+vra : {A : Set} → A → Arg A
+vra = arg (arg-info visible (modality relevant quantity-0))
+
+hra : {A : Set} → A → Arg A
+hra = arg (arg-info hidden (modality relevant quantity-0))
+
+vrv :  ℕ → List (Arg Term) → Arg Term
+vrv n args = arg (arg-info visible (modality relevant quantity-0)) (var n args)
+
+vri : ℕ → Arg Term
+vri n = arg (arg-info instance′ (modality relevant quantity-0)) (var n [])
+
+vrit : {A : Set} → A → Arg A
+vrit = arg (arg-info instance′ (modality relevant quantity-0))
+
+vrv' : ℕ → Arg Term
+vrv' n = vrv n []
+
+------------------------------------------------------------------------
+-- Machinery specific to Write
+
+-- Produce the type for the auxiliary function that does the
+-- actual writing (i.e. has the expanded type)
+--
+-- Example: writeAuxType List
+--          ↦ {a : Set} {A : Set a} → {{ Write A }} → Precedence → List A → List Char → List Char
+writeAuxType : Name → TC Type
+writeAuxType nm = {!!}
+
+-- Produce the type of a Write instance for a given class.
+--
+-- Example: writeType List ↦ {a : Set} {A : Set a} → {{ Write A }} → Write (List A) 
+writeType : Name → TC Type
+writeType nm = {!!}
+
+-- TODO: doc comment can be better
+-- given the telescope for a constructor, produce the whole telescope for
+-- its clause
+-- Precedence → A → List Char → List Char
+conTel : Telescope → Telescope
+conTel tel =  ("str" , (vra (quoteTerm (List Char)))) ∷ (tel ++ ("prec" , (vra (quoteTerm Precedence))) ∷ [])
+
+recTel : Type → Telescope
+recTel rec = conTel [ ("rec" , (vra rec)) ]
+
+------------------------------------------------------------------------
+-- Derive macro for Write
+
+-- NOTE: lots of experimenting
+
+next : List (List Char) → (List Char) × (List (List Char))
+next [] = [] , []
+next (x ∷ xs) = x , xs
+
+-- Take a list of terms and turn it into a term of a list of said terms
+quoteList : List Term → Term
+quoteList [] = con (quote List.[]) []
+quoteList (x ∷ xs) = con (quote _∷_) (vra x ∷ [ (vra (quoteList xs)) ])
+
+padSep : List Char → List Char
+padSep [] = []
+padSep xs@(_ ∷ _) = ' ' ∷ xs ++ [ ' ' ]
+
+open Write {{...}}
+
+-- TODO: probably a better interface/function than this
+--         len ≥ length (tel)
+--         Between values    Inst Map    num vals  tel
+telWrite' : List (List Char) → ℕ → Telescope → List Term
+telWrite' seps len [] = [ con (quote List.[]) [] ]
+telWrite' seps len ((nm , typ) ∷ xs) = sepTerm ∷ pref ∷ 
+                                       (def (quote writesPrecList)
+                                       (prec ∷ conVal ∷ vra suff ∷ [])) ∷
+                                       (telWrite' seps' len xs)
+          where
+
+            sepSeps : List Char × (List (List Char))
+            sepSeps = next seps
+
+            sep : List Char
+            sep = padSep (proj₁ sepSeps)
+
+            -- there must be a better way! maybe we should use strings
+            sepTerm : Term
+            sepTerm = def (quote toList) ((vra (lit (string (fromList sep)))) ∷ [])
+
+            seps' : List (List Char)
+            seps' = proj₂ sepSeps
+            
+            inst : Arg Term
+            inst = arg (arg-info instance′ (modality relevant quantity-0)) unknown
+
+            str : Arg Term
+            str = vrv' (len + 1)
+
+            pref : Term
+            pref = quoteTerm (toList "(")
+
+            suff : Term
+            suff = quoteTerm (toList ")")
+            
+            strBrack : Arg Term
+            strBrack = vra (def (quote _++_) (vra (quoteTerm (toList ") ")) ∷ [ str ]))
+
+            conVal : Arg Term
+            conVal = vrv' (∣ len - (length xs) ∣′)
+
+            prec : Arg Term
+            prec = vrv' 0
+
+telWrite : List (List Char) → ℕ → Telescope → Term
+telWrite seps n tel = def (quote concat) [ (vra (quoteList (telWrite' seps n tel))) ]
+
+varPat : ℕ → Arg Pattern
+varPat n = vra (Pattern.var n)
+
+insPat : ℕ → Arg Pattern
+insPat n = vrit (Pattern.var n)
+
+telToVarPat : ℕ → List (Arg Pattern)
+telToVarPat 0 = []
+telToVarPat (ℕ.suc n) = telToVarPat n ++ (varPat (1 + n)) ∷ []
+
+conNameTerm : Name → Term
+conNameTerm nm = def (quote unqualify) (vra (def (quote toList) (nmLit ∷ [])) ∷ [])
+  where
+    nmLit : Arg Term
+    nmLit = vra (lit (string (showName nm)))
+
+-- get a list of constructor seperators
+-- with an additional empty seperator
+-- if the constructor mixfix starts with a _
+conSeps : List Char → List (List Char)
+conSeps [] = []
+conSeps ('_' ∷ str) = [] ∷ conSeps str
+conSeps str@(_ ∷ _) = wordsBy (_≡?_ '_') str
+
+-- clause when the constructor of a data type is empty
+emptyCons : Name → Clause
+emptyCons nm = Clause.clause (conTel []) ((varPat 0) ∷ conPat ∷ ((varPat 1) ∷ [])) (conNameTerm nm)
+  where
+    conPat : Arg Pattern
+    conPat = vra (Pattern.con nm [])
+
+-- derive the clause for a single constructor
+consClause : Name → Type → Clause
+consClause nm t with telView t
+... | [] , _ = emptyCons nm
+... | tel@(_ ∷ _) , _ = Clause.clause (conTel tel) (varPat 0 ∷ conPat ∷ strPat ∷ []) writeTerm
+  where
+    precPat : Arg Pattern
+    precPat = varPat 0
+
+    telLen : ℕ
+    telLen = Data.List.Base.length tel
+    
+    conPat : Arg Pattern
+    conPat = vra (Pattern.con nm (telToVarPat telLen))
+
+    strPat : Arg Pattern
+    strPat = varPat (telLen + 1)
+
+    nmStr : List Char
+    nmStr = unqualify (toList (showName nm))
+
+    writeTerm : Term
+    writeTerm = telWrite (conSeps nmStr) telLen tel
+
+-- Prec → Rec → LC → LC
+recordOutputs : Name → List (Arg Name) → List Term
+recordOutputs nm [] = [ (quoteTerm (toList "}")) ]
+recordOutputs nm (x ∷ fs) = def (quote toList) [ vra (lit (string fieldName)) ] ∷
+                            (quoteTerm (toList " = ")) ∷
+                            def (quote writesPrecList) (vrv' 0 ∷ fieldArg ∷ vrv' 2 ∷ []) ∷
+                            (quoteTerm (toList "; ")) ∷
+                            recordOutputs nm fs
+  where
+    fieldArg : Arg Term
+    fieldArg = vra (def (unArg x) [ vrv' 1 ])
+
+    fieldName : String
+    fieldName = fromList (unqualify (toList (showName (unArg x))))
+    
+
+recordTerm : Name → List (Arg Name) → Term
+recordTerm nm fs = def (quote concat) [
+                   (vra (quoteList (prefix ∷ outs))) ]
+           where
+             prefix : Term
+             prefix = quoteTerm (toList "record { ")
+
+             outs : List Term
+             outs = recordOutputs nm fs
+
+-- cs in data-type contains actual constructor names
+-- 'name' in data-cons is just name of data type itself
+computeAuxWrite : Definition → TC (List Clause)
+computeAuxWrite (record-type c fs) = do
+  t ← getType c
+  let tel = recTel t
+      pats = varPat 0 ∷ varPat 1 ∷ varPat 2 ∷ []
+      body = recordTerm c fs
+      clause = Clause.clause tel pats body
+  -- typeError [ termErr (pat-lam [ clause ] []) ]
+  pure [ clause ]
+computeAuxWrite (data-type p cs) = do
+  ts ← mapM monadTCM getType cs
+  let tels = Data.List.Base.map telView ts
+  let clauses = (Data.List.Base.map (uncurry consClause) (zip cs ts))
+  -- typeError (termErr (pat-lam clauses []) ∷ [])
+  pure clauses
+{-# CATCHALL #-}
+computeAuxWrite _  = typeError (strErr "Write instances can only be derived for data and record types" ∷ [])
+
+macro
+  deriveWriteDef : Name → Term → TC ⊤
+  deriveWriteDef nm met = do
+    d ← getDefinition nm
+    writeClauses ← computeAuxWrite d
+    unify met (pat-lam writeClauses [])
+
+-- Declare a Write instance with a given name for a given
+-- type.
+--
+-- e.g.
+-- declareWriteInstance 'ListWrite' (quote List)
+-- ↦
+-- ListWrite : {a : Level} {A : Set a} {{Write A}} → Write (List A)
+declareWriteInstance : Name → Name → TC ⊤
+declareWriteInstance fnm class = do
+  t ← writeType class
+  declareDef (iArg fnm) t
+
+-- Define the Write instance of a given name for a given
+-- type.
+--
+-- The instance must already be declared, e.g. via declareWriteInstance.
+-- This also declares another top-level name with the 'expanded' type of Write
+-- (Precedence → A → List Char → List Char), and attaches the 'actual' definition to that.
+-- For a type T, the name of this auxillary function is "write[T]".
+-- 
+-- The instance then simply constructs a record of Write out of it. This is to allow
+-- for the definition to recurse on itself.
+defineWriteInstance : Name → Name → TC ⊤
+defineWriteInstance inm class = do
+  fnm ← freshName ("write[" ++s showName inm ++s "]")
+  ft ← writeAuxType class
+  
+  declareDef (vra fnm) ft
+ 
+  defineFun inm (Clause.clause [] [] (con (quote Text.Write.mkWrite) [ vra (def fnm []) ]) ∷ [])
+
+  classDef ← getDefinition class
+  clauses ← computeAuxWrite classDef
+  defineFun fnm clauses
+  
+  pure _
+
+-- Usage (example for List):
+--  unquoteDecl ListWrite = deriveWriteI ListWrite (quote List)
+deriveWriteI : Name → Name → TC ⊤
+deriveWriteI iname typ = (declareWriteInstance iname typ) >> (defineWriteInstance iname typ)
+
+record Test' : Set where
+  field
+    a : ℕ
+    b : ℕ
+    
+g : Precedence → Test' → List Char → List Char
+g = deriveWriteDef Test'
+
+test' : Test'
+test' .Test'.a = 5
+test' .Test'.b = 99
+f : String
+f = fromList (g unrelated test' [])
+
+{-
+λ { prec (a _ - _ - _) str
+      → concat
+        (toList " a " ∷
+         toList "(" ∷
+         .Write.writesPrecList prec _ (toList ")") ∷
+         concat
+         (toList " - " ∷
+          toList "(" ∷
+          .Write.writesPrecList prec _ (toList ")") ∷
+          concat
+          (toList " - " ∷
+           toList "(" ∷ .Write.writesPrecList prec _ (toList ")") ∷ [] ∷ [])
+          ∷ [])
+         ∷ [])
+  ; prec a' str → unqualify (toList "Text.Write.Deriving.Test.a'")
+  ; prec a'' str → unqualify (toList "Text.Write.Deriving.Test.a''")
+  }
+-}