diff --git a/Class/Convertible.agda b/Class/Convertible.agda
new file mode 100644
index 00000000..3702c594
--- /dev/null
+++ b/Class/Convertible.agda
@@ -0,0 +1,84 @@
+module Class.Convertible where
+
+open import Function
+open import Class.HasHsType
+open import Class.Core
+open import Class.Functor
+open import Class.Bifunctor
+open import Data.Maybe
+open import Data.Product
+open import Data.Sum
+open import Data.List
+
+record Convertible (A B : Set) : Set where
+  field to   : A → B
+        from : B → A
+open Convertible ⦃...⦄ public
+
+HsConvertible : (A : Set) → ⦃ HasHsType A ⦄ → Set
+HsConvertible A = Convertible A (HsType A)
+
+Convertible-Refl : ∀ {A} → Convertible A A
+Convertible-Refl = λ where .to → id; .from → id
+
+Convertible₁ : (Set → Set) → (Set → Set) → Set₁
+Convertible₁ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible (T A) (U B)
+
+Convertible₂ : (Set → Set → Set) → (Set → Set → Set) → Set₁
+Convertible₂ T U = ∀ {A B} → ⦃ Convertible A B ⦄ → Convertible₁ (T A) (U B)
+
+Functor⇒Convertible : ∀ {F : Type↑} → ⦃ Functor F ⦄ → Convertible₁ F F
+Functor⇒Convertible = λ where
+  .to   → fmap to
+  .from → fmap from
+
+Bifunctor⇒Convertible : ∀ {F} → ⦃ Bifunctor F ⦄ → Convertible₂ F F
+Bifunctor⇒Convertible = λ where
+  .to   → bimap to to
+  .from → bimap from from
+
+_⨾_ : ∀ {A B C} → Convertible A B → Convertible B C → Convertible A C
+(c ⨾ c') .to   = c' .to   ∘ c  .to
+(c ⨾ c') .from = c  .from ∘ c' .from
+
+-- ** instances
+
+open import Foreign.Haskell
+open import Foreign.Haskell.Coerce using (coerce)
+
+open import Data.Nat
+
+instance
+  Convertible-ℕ : Convertible ℕ ℕ
+  Convertible-ℕ = λ where
+    .to   → id
+    .from → id
+
+  Convertible-Maybe : Convertible₁ Maybe Maybe
+  Convertible-Maybe = Functor⇒Convertible
+
+  Convertible-× : Convertible₂ _×_ _×_
+  Convertible-× = Bifunctor⇒Convertible
+
+  Convertible-Pair : Convertible₂ _×_ Pair
+  Convertible-Pair = λ where
+    .to   → coerce ∘ bimap to to
+    .from → bimap from from ∘ coerce
+
+  Convertible-⊎ : Convertible₂ _⊎_ _⊎_
+  Convertible-⊎ = Bifunctor⇒Convertible
+
+  Convertible-Either : Convertible₂ _⊎_ Either
+  Convertible-Either = λ where
+    .to   → coerce ∘ bimap to to
+    .from → bimap from from ∘ coerce
+
+  Convertible-List : Convertible₁ List List
+  Convertible-List = λ where
+    .to   → fmap to
+    .from → fmap from
+
+  Convertible-Fun : ∀ {A A' B B'} → ⦃ Convertible A A' ⦄ → ⦃ Convertible B B' ⦄ → Convertible (A → B) (A' → B')
+  Convertible-Fun = λ where
+    .to   → λ f → to   ∘ f ∘ from
+    .from → λ f → from ∘ f ∘ to
diff --git a/Class/HasHsType.agda b/Class/HasHsType.agda
new file mode 100644
index 00000000..9484f2d7
--- /dev/null
+++ b/Class/HasHsType.agda
@@ -0,0 +1,51 @@
+module Class.HasHsType where
+
+open import Level using (Level)
+open import Data.Bool.Base using (Bool)
+open import Data.Nat.Base using (ℕ)
+open import Data.String.Base using (String)
+open import Data.List.Base using (List)
+open import Data.Maybe.Base using (Maybe)
+open import Data.Sum.Base using (_⊎_)
+open import Data.Product.Base using (_×_)
+open import Data.Unit using (⊤)
+
+open import Foreign.Haskell.Pair using (Pair)
+open import Foreign.Haskell.Either using (Either)
+
+private variable
+  l : Level
+  A B : Set l
+
+record HasHsType (A : Set l) : Set₁ where
+  field
+    HsType : Set
+
+HsType : (A : Set l) → ⦃ HasHsType A ⦄ → Set
+HsType _ ⦃ i ⦄ = i .HasHsType.HsType
+
+MkHsType : (A : Set l) (Hs : Set) → HasHsType A
+MkHsType A Hs .HasHsType.HsType = Hs
+
+instance
+
+  iHsTy-ℕ      = MkHsType ℕ ℕ
+  iHsTy-Bool   = MkHsType Bool Bool
+  iHsTy-⊤      = MkHsType ⊤ ⊤
+  iHsTy-String = MkHsType String String
+
+  -- Could make a macro for these kind of congruence instances.
+  iHsTy-List : ⦃ HasHsType A ⦄ → HasHsType (List A)
+  iHsTy-List {A = A} .HasHsType.HsType = List (HsType A)
+
+  iHsTy-Maybe : ⦃ HasHsType A ⦄ → HasHsType (Maybe A)
+  iHsTy-Maybe {A = A} .HasHsType.HsType = Maybe (HsType A)
+
+  iHsTy-Fun : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A → B)
+  iHsTy-Fun {A = A} {B = B} .HasHsType.HsType = HsType A → HsType B
+
+  iHsTy-Sum : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A ⊎ B)
+  iHsTy-Sum {A = A} {B = B} .HasHsType.HsType = Either (HsType A) (HsType B)
+
+  iHsTy-Pair : ⦃ HasHsType A ⦄ → ⦃ HasHsType B ⦄ → HasHsType (A × B)
+  iHsTy-Pair {A = A} {B = B} .HasHsType.HsType = Pair (HsType A) (HsType B)
diff --git a/Reflection/Utils/Substitute.agda b/Reflection/Utils/Substitute.agda
new file mode 100644
index 00000000..13c9e9be
--- /dev/null
+++ b/Reflection/Utils/Substitute.agda
@@ -0,0 +1,46 @@
+module Reflection.Utils.Substitute where
+
+open import Meta.Prelude
+open import Meta.Init
+
+-- There aren't any nice substitution functions (that I can find) in the standard library or
+-- stdlib-meta. This one is cheating and only works for closed terms at either never gets
+-- applied, or where we can safely throw away the arguments (e.g. `unknown`).
+
+Subst : Set → Set
+Subst A = ℕ → Term → A → A
+
+substTerm : Subst Term
+substArgs : Subst (Args Term)
+substArg  : Subst (Arg Term)
+substAbs  : Subst (Abs Term)
+substSort : Subst Sort
+
+substTerm x s (var y args) =
+  case compare x y of λ where
+    (less _ _)    → var (y ∸ 1) (substArgs x s args)
+    (equal _)     → s  -- cheating and dropping the args!
+    (greater _ _) → var y (substArgs x s args)
+substTerm x s (con c args) = con c (substArgs x s args)
+substTerm x s (def f args) = def f (substArgs x s args)
+substTerm x s (lam v t) = lam v (substAbs x s t)
+substTerm x s (pat-lam cs args₁) = unknown  -- ignoring for now
+substTerm x s (pi a b) = pi (substArg x s a) (substAbs x s b)
+substTerm x s (agda-sort s₁) = agda-sort (substSort x s s₁)
+substTerm x s (lit l) = lit l
+substTerm x s (meta m args) = meta m (substArgs x s args)
+substTerm x s unknown = unknown
+
+substArgs x s [] = []
+substArgs x s (a ∷ as) = substArg x s a ∷ substArgs x s as
+
+substArg x s (arg i t) = arg i (substTerm x s t)
+
+substAbs x s (abs z t) = abs z (substTerm (ℕ.suc x) s t)
+
+substSort x s (set t) = set (substTerm x s t)
+substSort x s (lit n) = lit n
+substSort x s (prop t) = prop (substTerm x s t)
+substSort x s (propLit n) = propLit n
+substSort x s (inf n) = inf n
+substSort x s unknown = unknown
diff --git a/Tactic.agda b/Tactic.agda
index 9a79e205..9f82b280 100644
--- a/Tactic.agda
+++ b/Tactic.agda
@@ -17,3 +17,6 @@ open import Tactic.ReduceDec public
 
 open import Tactic.Derive.DecEq public
 open import Tactic.Derive.Show public
+open import Tactic.Derive.Convertible
+open import Tactic.Derive.HsType
+open import Tactic.Derive.HsType.Tests
diff --git a/Tactic/Derive/Convertible.agda b/Tactic/Derive/Convertible.agda
new file mode 100644
index 00000000..09f2b3eb
--- /dev/null
+++ b/Tactic/Derive/Convertible.agda
@@ -0,0 +1,185 @@
+module Tactic.Derive.Convertible where
+
+open import Level
+open import Meta.Prelude
+open import Meta.Init
+
+import Data.List as L
+import Data.List.NonEmpty as NE
+import Data.String as S
+import Data.Product as P
+
+open import Relation.Nullary
+open import Relation.Nullary.Decidable
+
+open import Reflection.Tactic
+open import Reflection.AST.Term
+open import Reflection.AST.DeBruijn
+import Reflection.TCM as R
+open import Reflection.Utils
+open import Reflection.Utils.TCI
+import Function.Identity.Effectful as Identity
+
+open import Class.DecEq
+open import Class.DecEq
+open import Class.Functor
+open import Class.Monad
+open import Class.MonadTC.Instances
+open import Class.Traversable
+open import Class.Show
+open import Class.MonadReader
+
+open import Reflection.Utils.Substitute
+open import Class.Convertible
+open import Class.HasHsType
+open import Tactic.Derive.HsType
+
+private instance
+  _ = Functor-M {TC}
+
+-- TODO: move to agda-stdlib-meta
+liftTC : ∀ {a} {A : Set a} → R.TC A → TC A
+liftTC m _ = m
+
+private
+
+  open MonadReader ⦃...⦄
+
+  variable
+    A B C : Set
+
+  TyViewTel = List (Abs (Arg Type))
+
+  substTel : Subst TyViewTel
+  substTel x s [] = []
+  substTel x s (abs z t ∷ tel) = abs z (substArg x s t) ∷ (substTel (ℕ.suc x) s tel)
+    -- Note: `abs` is abused in TyViewTel and doesn't actually scope over the `t`
+
+  -- Substitute leading level parameters with lzero
+  smashLevels : TyViewTel → ℕ × TyViewTel
+  smashLevels (abs s (arg i (def (quote Level) [])) ∷ tel) =
+    P.map ℕ.suc (substTel 0 (quote 0ℓ ∙)) $ smashLevels tel
+  smashLevels tel = (0 , tel)
+
+  tyViewToTel : TyViewTel → Telescope
+  tyViewToTel = L.map λ where (abs s a) → s , a
+
+  hideTyView : Abs (Arg A) → Abs (Arg A)
+  hideTyView (abs s (arg (arg-info _ m) x)) = abs s (arg (arg-info hidden m) x)
+
+  -- The type of a Convertible instance. For parameterised types adds the appropriate instance
+  -- arguments and instantiates level arguments to lzero. For instance,
+  -- instanceType _⊎_ Hs.Either = {A B : Set} {a b : Set} → ⦃ Convertible A a ⦄ → ⦃ Convertible B b ⦄
+  --                              Convertible (A ⊎ B) (Hs.Either a b)
+  instanceType : (agdaName hsName : Name) → TC TypeView
+  instanceType agdaName hsName = do
+    aLvls , agdaParams ← smashLevels <$> getParamsAndIndices agdaName
+    hLvls , hsParams   ← smashLevels <$> getParamsAndIndices hsName
+    true ← return (length agdaParams == length hsParams)
+      where false → liftTC $ R.typeErrorFmt "%q and %q have different number of parameters" agdaName hsName
+    let n = length agdaParams
+        l₀ = quote 0ℓ ∙
+    agdaTy ← applyWithVisibility agdaName $ L.replicate aLvls l₀ ++ L.map ♯ (take n (downFrom (n + n)))
+    hsTy   ← applyWithVisibility hsName   $ L.replicate hLvls l₀ ++ L.map ♯ (downFrom n)
+    let instHead = weaken n $ quote Convertible ∙⟦ agdaTy ∣ hsTy ⟧
+        tel      = L.map hideTyView (agdaParams ++ hsParams) ++
+                   L.replicate n (abs "_" (iArg (quote Convertible ∙⟦ ♯ (n + n ∸ 1) ∣ ♯ (n ∸ 1) ⟧)))
+    return $ tel , instHead
+
+  -- Compute one clause of the Convertible instance. For instance,
+  -- conversionClause Convertible.to to ((c₁ , _) , (c₂ , _)) generates
+  -- .to (c₁ x₁ .. xn) = c₂ (to x₁) .. (to xn)
+  -- where the xi are the visible constructor arguments.
+  conversionClause : Name → Name → (Name × Type) × (Name × Type) → TC Clause
+  conversionClause prjP prjE ((fromC , fromTy) , (toC , toTy)) = do
+    let isVis   = λ { (abs _ (arg (arg-info visible _) _)) → true; _ → false }
+        fromTel = L.filterᵇ isVis (proj₁ (viewTy fromTy))
+        toTel   = L.filterᵇ isVis (proj₁ (viewTy toTy))
+        n       = length fromTel
+        mkCon  c mkArg = Term.con c    $ L.map (vArg ∘ mkArg ∘ ♯)  (downFrom n)
+        mkConP c mkArg = Pattern.con c $ L.map (vArg ∘ mkArg ∘ `_) (downFrom n)
+    true ← return (n == length toTel)
+      where false → liftTC $ R.typeErrorFmt "%q and %q have different number of arguments" fromC toC
+    return $ clause (tyViewToTel $ L.map (λ where (abs x (arg i _)) → abs x (arg i unknown)) fromTel)
+                    (vArg (proj prjP) ∷ vArg (mkConP fromC id) ∷ [])
+                    (mkCon toC (prjE ∙⟦_⟧))
+
+  -- Compute the clauses of a convertible instance.
+  instanceClauses : (agdaName hsName : Name) → TC (List Clause)
+  instanceClauses agdaName hsName = do
+    agdaCons ← getConstrs agdaName
+    hsCons   ← getConstrs hsName
+    agdaPars ← length <$> getParamsAndIndices agdaName
+    hsPars   ← length <$> getParamsAndIndices hsName
+    true ← return (length agdaCons == length hsCons)
+      where false → liftTC $ R.typeErrorFmt "%q and %q have different number of constructors" agdaName hsName
+    toClauses   ← mapM (conversionClause (quote Convertible.to)   (quote to)  ) (L.zip agdaCons hsCons)
+    fromClauses ← mapM (conversionClause (quote Convertible.from) (quote from)) (L.zip hsCons agdaCons)
+    return $ toClauses ++ fromClauses
+
+  absurdClause : Name → Clause
+  absurdClause prj = absurd-clause (("x" , vArg unknown) ∷ []) (vArg (proj prj) ∷ vArg (absurd 0) ∷ [])
+
+  -- Compute conversion clauses for the current goal and wrap them in a pattern lambda.
+  patternLambda : TC Term
+  patternLambda = do
+    quote Convertible ∙⟦ `A ∣ `B ⟧ ← reduce =<< goalTy
+      where t → liftTC $ R.typeErrorFmt "Expected Convertible A B, got %t" t
+    agdaCons ← getConstrsForType `A
+    hsCons   ← getConstrsForType `B
+    toClauses   ← mapM (conversionClause (quote Convertible.to)   (quote to)  ) (L.zip agdaCons hsCons)
+    fromClauses ← mapM (conversionClause (quote Convertible.from) (quote from)) (L.zip hsCons agdaCons)
+    case toClauses ++ fromClauses of λ where
+      []  → return $ pat-lam (absurdClause (quote Convertible.to) ∷ absurdClause (quote Convertible.from) ∷ []) []
+      cls → return $ pat-lam cls []
+
+doPatternLambda : Term → R.TC Term
+doPatternLambda hole = patternLambda =<< initTCEnvWithGoal hole
+
+-- Deriving a Convertible instance. Usage
+--   unquoteDecl iName = deriveConvertible iName (quote AgdaTy) (quote HsTy)
+deriveConvertible : Name → Name → Name → R.TC ⊤
+deriveConvertible instName agdaName hsName = initUnquoteWithGoal ⦃ defaultTCOptions ⦄ (agda-sort (lit 0)) do
+  agdaDef ← getDefinition agdaName
+  hsDef   ← getDefinition hsName
+  -- instName ← freshName $ "Convertible" S.++ show hsName
+  instTel , instTy ← instanceType agdaName hsName
+  inst    ← declareDef (iArg instName) (tyView (instTel , instTy))
+  clauses ← instanceClauses agdaName hsName
+  defineFun instName clauses
+  return _
+
+-- Macros providing an alternative interface. Usage
+--   iName : ConvertibleType AgdaTy HsTy
+--   iName = autoConvertible
+-- or
+--   iName = autoConvert AgdaTy
+macro
+  ConvertibleType : Name → Name → Tactic
+  ConvertibleType agdaName hsName = initTac ⦃ defaultTCOptions ⦄ $
+    unifyWithGoal ∘ tyView =<< instanceType agdaName hsName
+
+  autoConvertible : Tactic
+  autoConvertible = initTac ⦃ defaultTCOptions ⦄ $
+    unifyWithGoal =<< patternLambda
+
+  autoConvert : Name → Tactic
+  autoConvert d hole = do
+    hsTyMeta ← R.newMeta `Set
+    R.checkType hole $ quote Convertible ∙⟦ d ∙ ∣ hsTyMeta ⟧
+    hsTy ← solveHsType (d ∙)
+    R.unify hsTyMeta hsTy
+    R.unify hole =<< doPatternLambda hole
+
+-- Tests
+
+private
+
+  record Test : Set where
+    field f : ℕ
+          g : Maybe ℕ
+          h : List ℕ
+
+  instance
+    HsTy-Test = autoHsType Test ⊣ withConstructor "MkTest" • fieldPrefix "t"
+    Conv-Test = autoConvert Test
diff --git a/Tactic/Derive/HsType.agda b/Tactic/Derive/HsType.agda
new file mode 100644
index 00000000..81aceb06
--- /dev/null
+++ b/Tactic/Derive/HsType.agda
@@ -0,0 +1,387 @@
+module Tactic.Derive.HsType where
+
+open import Meta.Init hiding (TC; Monad-TC; MonadError-TC)
+
+open import Level using (Level; 0ℓ)
+open import Agda.Builtin.Reflection using (declareData; defineData; pragmaForeign; pragmaCompile;
+                                           solveInstanceConstraints)
+open import Reflection as R hiding (showName; _>>=_; _>>_ ; _≟_)
+open import Reflection.AST hiding (showName)
+open import Reflection.AST.DeBruijn
+open import Data.Maybe using (Maybe; nothing; just; fromMaybe; maybe′; _<∣>_)
+open import Data.Unit using (⊤; tt)
+open import Data.Integer.Base using (ℤ)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.String using (String) renaming (_++_ to _&_)
+open import Data.Product hiding (map; zip; zipWith)
+import Data.String as String
+open import Data.Bool hiding (_≟_)
+open import Data.Nat hiding (_≟_)
+open import Data.List hiding (lookup; fromMaybe)
+open import Data.Char using (toUpper; toLower)
+open import Foreign.Haskell
+open import Function
+open import Text.Printf
+open import Relation.Nullary.Decidable using (¬?)
+
+open import Class.DecEq
+open import Class.Functor
+open import Class.Monad
+open import Class.MonadError
+open import Class.MonadReader
+open import Class.Show
+open import Class.Show.Instances
+open import Class.MonadTC using (TCEnv; dontReduce; defaultTCOptions)
+open import Tactic.Derive.Show using (showName)
+
+open import Reflection.Utils
+open import Reflection.Utils.TCI
+open import Foreign.Haskell.Pair using (Pair)
+open import Class.HasHsType
+
+{-
+Need to generate:
+  - a data type that can be compiled to a Haskell data type
+  - the corresponding Haskell type (in a FOREIGN pragma)
+  - the COMPILE pragma binding them together
+-}
+
+-- TODO: This breaks with:
+-- - mutual data types
+-- - parametrised data types
+-- - maybe more
+
+private variable
+  l : Level
+  A B : Set l
+
+-- TODO: somewhere else
+`Set = agda-sort (Sort.set (quote 0ℓ ∙))
+
+-- * Controlling the names of the generated types
+
+record NameEnv : Set where
+  field
+    customNames : List (Name × String)
+    tName       : Name → Maybe String
+    cName       : Name → Maybe String
+    fName       : Name → Maybe String
+
+private
+  mapHead : (A → A) → List A → List A
+  mapHead f []       = []
+  mapHead f (x ∷ xs) = f x ∷ xs
+
+capitalize : String → String
+capitalize = String.fromList ∘ mapHead toUpper ∘ String.toList
+
+uncapitalize : String → String
+uncapitalize = String.fromList ∘ mapHead toLower ∘ String.toList
+
+private
+  lookup : ⦃ DecEq A ⦄ → A → List (A × B) → Maybe B
+  lookup x xs = proj₂ <$> findᵇ ((x ==_) ∘ proj₁) xs
+
+  lookupEnv : (NameEnv → Name → Maybe String) → NameEnv → Name → Maybe String
+  lookupEnv fn env x = lookup x (NameEnv.customNames env) <∣> fn env x
+
+  lookupTypeName  = lookupEnv NameEnv.tName
+  lookupConName   = lookupEnv NameEnv.cName
+  lookupFieldName = lookupEnv NameEnv.fName
+
+  emptyEnv : NameEnv
+  emptyEnv = record{ customNames = []
+                   ; tName = const nothing
+                   ; cName = const nothing
+                   ; fName = const nothing }
+
+  customName : Name → String → NameEnv
+  customName x s = record emptyEnv { customNames = (x , s) ∷ [] }
+
+onTypes : (String → String) → NameEnv
+onTypes f = record emptyEnv { tName = just ∘ f ∘ showName }
+
+onConstructors : (String → String) → NameEnv
+onConstructors f = record emptyEnv { cName = just ∘ f ∘ showName }
+
+withName : String → NameEnv
+withName t = onTypes (const t)
+
+-- Only use for single constructor types obviously
+withConstructor : String → NameEnv
+withConstructor c = onConstructors (const c)
+
+onFields : (String → String) → NameEnv
+onFields f = record emptyEnv { fName = just ∘ f ∘ showName }
+
+fieldPrefix : String → NameEnv
+fieldPrefix pre = onFields $ (pre String.++_) ∘ capitalize
+
+infixr 5 _•_
+_•_ : NameEnv → NameEnv → NameEnv
+env • env₁ = record
+  { customNames = env.customNames ++ env₁.customNames
+  ; tName       = λ x → env.tName x <∣> env₁.tName x
+  ; cName       = λ x → env.cName x <∣> env₁.cName x
+  ; fName       = λ x → env.fName x <∣> env₁.fName x
+  }
+  where
+    module env  = NameEnv env
+    module env₁ = NameEnv env₁
+
+
+-- * The inner workings
+
+solveHsType : Term → TC Term
+solveHsType tm = do
+  hsTy ← checkType (quote HsType ∙⟦ tm ⟧) `Set
+  solveInstanceConstraints
+  normalise hsTy >>= λ where
+    (def (quote HsType) _) → typeErrorFmt "Failed to solve HsType %t" tm
+    hsTy                   → return hsTy
+
+private
+  debug = debugPrintFmt "tactic.hs-types"
+
+  _‼_ : List A → ℕ → Maybe A
+  []       ‼ i     = nothing
+  (x ∷ xs) ‼ zero  = just x
+  (x ∷ xs) ‼ suc i = xs ‼ i
+
+  specialHsTypes : List (Name × String)
+  specialHsTypes = (quote ⊤      , "()")
+                 ∷ (quote ℕ      , "Integer")
+                 ∷ (quote ℤ      , "Integer")
+                 ∷ (quote Bool   , "Bool")
+                 ∷ (quote List   , "[]")
+                 ∷ (quote Pair   , "(,)")
+                 ∷ (quote Maybe  , "Maybe")
+                 ∷ (quote Either , "Either")
+                 ∷ (quote String , "Data.Text.Text")
+                 ∷ []
+
+  hsTypeName : NameEnv → Name → String
+  hsTypeName env d = fromMaybe (capitalize $ showName d) (lookupTypeName env d)
+
+  freshHsTypeName : NameEnv → Name → TC Name
+  freshHsTypeName env d = freshName (hsTypeName env d)
+
+  hsConName : NameEnv → Name → String
+  hsConName env c = fromMaybe (capitalize $ showName c) (lookupConName env c)
+
+  hsFieldName : NameEnv → Name → String
+  hsFieldName env f = fromMaybe (uncapitalize $ showName f) (lookupFieldName env f)
+
+  freshHsConName : NameEnv → Name → Name → TC Name
+  freshHsConName env tyName c =
+    if showName c == "constructor"
+    then freshName (hsConName env tyName) -- Unnamed record constructor: use type name
+    else freshName (hsConName env c)
+
+  isThis : Name → Term → Bool
+  isThis f (def g _) = f == g
+  isThis _ _ = false
+
+  computeHsType : Name → Name → Term → TC Term
+  computeHsType aThis hThis tm with isThis aThis tm
+  ... | true = pure (hThis ∙)
+  computeHsType aThis hThis (Π[ x ∶ arg (arg-info visible _) a ] b) | false = do
+    dom ← computeHsType aThis hThis a
+    rng ← extendContext x (vArg a) $ computeHsType aThis hThis b
+    pure (vΠ[ x ∶ dom ] rng)
+  computeHsType aThis hThis (Π[ x ∶ a ] b) | false = do
+    ty ← extendContext x a $ computeHsType aThis hThis b
+    just ty′ ← pure (strengthen ty)
+      where nothing → extendContext x a $ typeErrorFmt "%s free in computed HsType %t" x ty
+    pure ty′
+  -- Hack to get recursive occurrences under lists to work
+  computeHsType aThis hThis (def (quote List) (_ ∷ vArg a ∷ [])) | false = do
+    ty ← computeHsType aThis hThis a
+    pure (quote List ∙⟦ ty ⟧)
+  computeHsType _ _ tm | false = do
+    debug 10 "solving HsType %t" tm
+    ty ← solveHsType tm
+    debug 10 "HsType %t = %t" tm ty
+    pure ty
+
+  makeHsCon : NameEnv → Name → Name → Name → TC (Name × Agda.Builtin.Reflection.Quantity × Type)
+  makeHsCon env agdaName hsName c = do
+    debug 10 "Making constructor %q : %q" c agdaName
+    def agdaName' _ ← normalise (def agdaName [])
+      where _ → typeErrorFmt "Failed to compute source type for %q" agdaName
+    hsC  ← freshHsConName env hsName c
+    cTy  ← getType c
+    debug 10 "cTy = %t" cTy
+    hsTy ← computeHsType agdaName' hsName cTy
+    debug 10 "hsTy = %t" hsTy
+    pure (hsC , quantity-ω , hsTy)
+
+  makeHsData : NameEnv → Name → ℕ → List Name → TC Name
+  makeHsData env agdaName nPars constrs = do
+    hsName ← freshHsTypeName env agdaName
+    declareData hsName 0 `Set
+    hsCons ← mapM (makeHsCon env agdaName hsName) constrs
+    defineData hsName hsCons
+    pure hsName
+
+  makeHsType : NameEnv → Name → TC Name
+  makeHsType env d = getDefinition d >>= λ where
+      (data-type pars cs) → makeHsData env d pars cs
+      (record-type c fs)  → makeHsData env d 0 (c ∷ [])
+      _                   → typeErrorFmt "%q is not a data or record type" d
+
+  joinStrings : String → List String → String
+  joinStrings sep ss = foldr _&_ "" $ intersperse sep ss
+
+  removeUnderscore : String → String
+  removeUnderscore s = joinStrings "." $ filter (¬? ∘ ("_" ≟_))
+                        $ map String.fromList $ wordsBy ('.' ≟_) $ String.toList s
+
+  compilePragma : Name → List Name → String
+  compilePragma d cs = printf "= data %s (%s)" (showName d) (joinStrings " | " (map showName cs))
+
+  renderHsTypeName : Name → String
+  renderHsTypeName d = fromMaybe ("MAlonzo.Code." String.++ removeUnderscore (R.showName d)) (lookup d specialHsTypes)
+
+  renderHsType : Term → String
+  renderHsArgs : List (Arg Term) → List String
+
+  renderHsType (def (quote List) (_ ∷ vArg a ∷ [])) = printf "[%s]" (renderHsType a)
+  renderHsType (def (quote Pair) (_ ∷ _ ∷ vArg a ∷ vArg b ∷ [])) = printf "(%s, %s)" (renderHsType a) (renderHsType b)
+  renderHsType (def d []) = renderHsTypeName d
+  renderHsType (def d vs) = printf "(%s %s)" (renderHsTypeName d) (joinStrings " " (renderHsArgs vs))
+  renderHsType (vΠ[ s ∶ a ] x) = printf "(%s -> %s)" (renderHsType a) (renderHsType x)
+  renderHsType t = printf "(TODO: renderHsType %s)" (show t)
+
+  renderHsArgs [] = []
+  renderHsArgs (vArg a ∷ as) = renderHsType a ∷ renderHsArgs as
+  renderHsArgs (_ ∷ as) = renderHsArgs as
+
+  canDeriveInstancesT : Term → Bool
+  canDeriveInstancesA : List (Arg Term) → Bool
+
+  canDeriveInstancesT (def d vs) = canDeriveInstancesA vs
+  canDeriveInstancesT (vΠ[ s ∶ a ] x) = false
+  canDeriveInstancesT t = false
+
+  canDeriveInstancesA [] = true
+  canDeriveInstancesA (vArg a ∷ as) = canDeriveInstancesT a ∧ canDeriveInstancesA as
+  canDeriveInstancesA (_ ∷ as) = canDeriveInstancesA as
+
+  foreignPragma : Name → List Name → TC String
+  foreignPragma d cs = do
+    cons' ← forM cs λ c → do
+            tel , _ ← viewTy <$> getType c
+            let args = map unAbs tel
+            pure (  printf "%s %s" (showName c) (joinStrings " " $ renderHsArgs args)
+                 ,′ canDeriveInstancesA args )
+    let (cons , bs) = unzip cons'
+    pure $ printf "data %s = %s\n  deriving (%sGeneric)"
+                  (showName d) (joinStrings " | " cons)
+                  (if foldl _∧_ true bs then "Show, Eq, " else "" )
+
+  -- Record types
+  foreignPragmaRec : NameEnv → Name → List Name → List Name → TC String
+  foreignPragmaRec _ d [] _ = typeErrorFmt "impossible: %q is a record type with no constructors" d
+  foreignPragmaRec env d (c ∷ _) fs = do
+    tel , _ ← viewTy <$> withNormalisation true (getType c)
+    let fNames = map (hsFieldName env) fs
+    let args = map unAbs tel
+        renderField f ty = printf "%s :: %s" f (renderHsType $ unArg ty)
+        con = printf "%s {%s}" (showName c) (joinStrings ", " $ zipWith renderField fNames args)
+    pure $ printf "data %s = %s\n  deriving (%sGeneric)"
+                  (showName d) con
+                  (if canDeriveInstancesA args then "Show, Eq, " else "")
+
+  hsImports : String
+  hsImports = "import GHC.Generics (Generic)"
+
+  -- Take the name of a simple data type and generate the COMPILE and
+  -- FOREIGN pragmas to bind to Haskell.
+  bindHsType : NameEnv → Name → Name → TC ⊤
+  bindHsType env agdaName hsName = getDefinition hsName >>= λ where
+    (data-type pars cs) → do
+      pragmaForeign "GHC" hsImports
+      pragmaCompile "GHC" hsName $ compilePragma hsName cs
+      getDefinition agdaName >>= λ where
+        (data-type _ _)    → pragmaForeign "GHC" =<< foreignPragma hsName cs
+        (record-type _ fs) → pragmaForeign "GHC" =<< foreignPragmaRec env hsName cs (map unArg fs)
+        _ → typeErrorFmt "%q is not a data or record type" agdaName
+    _ → typeErrorFmt "%q is not a data type (impossible)" hsName
+
+  computeProjections : ℕ → Name → TC (List Term)
+  computeProjections npars c = do
+    argTys , _ ← viewTy <$> getType c
+    let is  = downFrom (length argTys)
+        tel = map (λ where (abs x ty) → x , ty) argTys
+        lhs = vArg (con c (map (λ where (i , abs x (arg info _)) → arg info (var i))
+                               (drop npars (zip is argTys)))) ∷ []
+    return $ map (λ i → pat-lam (clause tel lhs (var i []) ∷ []) []) (drop npars is)
+
+  makeTypeAlias : Name → NameEnv → Term → TC ⊤
+  makeTypeAlias agdaName env hole = do
+    hsTy ← solveHsType (def agdaName [])
+    pragmaForeign "GHC" $ printf "type %s = %s" (hsTypeName env agdaName) (renderHsType hsTy)
+    unify hole (quote return ∙⟦ con (quote tt) [] ⟧)
+
+-- * Exported macros
+
+doAutoHsType : NameEnv → Name → Term → TC Term
+doAutoHsType env d hole = do
+  checkType hole (quote HasHsType ∙⟦ d ∙ ⟧)
+  hs ← makeHsType env d
+  debug 50 "  HsType %q = %q" d hs
+  bindHsType env d hs
+  unify hole (`λ⟦ proj (quote HasHsType.HsType) ⇒ hs ∙ ⟧)
+  pure (hs ∙)
+
+macro
+  autoHsType : Name → Term → TC ⊤
+  autoHsType d hole = _ <$ doAutoHsType emptyEnv d hole
+
+  infix 0 autoHsType_⊣_
+  autoHsType_⊣_ : Name → NameEnv → Term → TC ⊤
+  autoHsType_⊣_ d env hole = _ <$ doAutoHsType env d hole
+
+  infix 9 _↦_
+  _↦_ : Name → String → Term → TC ⊤
+  x ↦ s = unify (quote customName ∙⟦ lit (name x) ∣ lit (string s) ⟧)
+
+  -- Generate a Haskell type synonym for the HsType of the given type
+  -- Usage `unquoteDecl = do hsTypeSynonym Foo; hsTypeSynonym Bar`
+  hsTypeAlias : Name → Term → TC ⊤
+  hsTypeAlias agdaName = makeTypeAlias agdaName emptyEnv
+
+  -- The only NameEnv that's useful here is `withName`.
+  hsTypeAlias_⊣_ : Name → NameEnv → Term → TC ⊤
+  hsTypeAlias agdaName ⊣ env = makeTypeAlias agdaName env
+
+  -- * Macros for constructing and deconstructing generated types
+
+  hsCon : Term → ℕ → Term → TC ⊤
+  hsCon agdaTy i hole = do
+    hsTy@(def hsName _) ← solveHsType agdaTy
+      where _ → typeErrorFmt "Failed to compute HsType of %t" agdaTy
+    cs ← getDefinition hsName >>= λ where
+      (data-type _ cs)  → return cs
+      _ → typeErrorFmt "Expected HsType %t to be a data type, but got %t" agdaTy hsTy
+    c ← maybe′ return  (typeErrorFmt "%q has only %u constructors" hsName (length cs)) (cs ‼ i)
+    unify hole (con c [])
+
+  hsProj : Term → ℕ → Term → TC ⊤
+  hsProj agdaTy i hole = do
+    hsTy@(def hsName _) ← solveHsType agdaTy
+      where _ → typeErrorFmt "Failed to compute HsType of %t" agdaTy
+    prjs ← getDefinition hsName >>= λ where
+      (data-type npars (c ∷ [])) → computeProjections npars c
+      _ → typeErrorFmt "Expected HsType %t to be a single constructor data type, but got %t" agdaTy hsTy
+    prj ← maybe′ return (typeErrorFmt "%q has only %u fields" hsName (length prjs)) (prjs ‼ i)
+    target ← newMeta `Set
+    checkType hole (pi (vArg hsTy) (abs "_" target))
+    unify hole prj
+
+  hsTyName : Term → Term → TC ⊤
+  hsTyName agdaTy hole = do
+    hsTy@(def hsName _) ← solveHsType agdaTy
+      where _ → typeErrorFmt "Failed to compute HsType of %t" agdaTy
+    unify hole (lit (name hsName))
diff --git a/Tactic/Derive/HsType/Tests.agda b/Tactic/Derive/HsType/Tests.agda
new file mode 100644
index 00000000..12fc7cc5
--- /dev/null
+++ b/Tactic/Derive/HsType/Tests.agda
@@ -0,0 +1,33 @@
+
+open import Class.HasHsType
+open import Tactic.Derive.HsType
+open import Tactic.Derive.TestTypes
+
+module Tactic.Derive.HsType.Tests where
+
+{-# FOREIGN GHC
+  {-# LANGUAGE NoImplicitPrelude #-}
+#-}
+{-# FOREIGN GHC import Prelude (Show, Eq, Bool, Integer) #-}
+private
+  HSTy-ℕ : HasHsType ℕ
+  HSTy-ℕ = autoHsType ℕ
+
+  HSTy-ℤ : HasHsType ℤ
+  HSTy-ℤ = autoHsType ℤ
+
+  data X : Set where
+    MkX : (Bool → Bool) → X
+
+  record RecX : Set where
+    field f : (Bool → Bool)
+
+  instance
+    HSTy-E1 : HasHsType E1
+    HSTy-E1 = autoHsType E1
+
+    HSTy-X : HasHsType X
+    HSTy-RecX : HasHsType RecX
+
+    HSTy-X = autoHsType X
+    HSTy-RecX = autoHsType RecX