NOTE: This is a rough, incomplete sketch.

Concrete syntax (roughly)
=========================

D ∷= data x Γ : Set
   | data x γ where
       ⦃c : T⦄
   | record x Γ : Set
   | record x γ where
       constructor c
       field
         ⦃π : T⦄
     open x
   | x : T
   | x ⦃p⦄ = T

p ∷= x | _ | p p

Γ ∷= {x : T} | (x : T)

γ ∷= {x} | x

T, t ∷= x | c | π | t t | λ x → t
      | Set
      | (x : T) → T
      | {x : T} → T
      | t ≡ t | refl | J | K
      | _

Implicit arguments: Only at the start of type signatures for top-level
declarations. J takes three implicit arguments and K two.

Parameter lists in definitions have to match those in declarations.

Constructor names have to be distinct.

Etc…

Intermediate syntax
===================

t ∷= i
   | refl
   | λ x → t
   | c ts
   | _

i ∷= Set
   | (x : t) → t
   | t ≡_t t
   | h es

h ∷= x | f | refl | J | K

e ∷= · t | π ·

Internal syntax
===============

-- Σ should be defined here.

U, u ∷= λ x → u
      | c us
      -- ^ A data or type constructor
      | Set | (x : U) → U
      | u ≡_U u | h es

h ∷= x | f | α | b | refl | J | K

e ∷= · u
   | π ·

b ∷= C ⚷ u
p   | C ⚷ b
   | Γ ⊢ t ⇐ A
   -- ^ Since sometimes we want to have a type checking constraint to
   --   reduce to the checked term afterwards

C ∷= {c₁, …, c_n}  (n ≥ 1)

-- Σ is not present in these constraints since it is global to the
-- type checking.
c ∷= Γ ⊢ A = B ⇐ Set
   | Γ ⊢ t ⇐ A

p ∷= (U, u)
   | C ⚷ (eps >>= λ (U, es) → (U, u))

ep ∷= {Γ ⊢ · t ⇐ B}
    | {Γ ⊢ π · ⇐ B}

eps ∷= ep           >>= λ (U, e) → eps
     | eps          >>= λ (U, es) → eps
     | {Γ ⊢ es ⇐ U} >>= λ (U, es) → eps
     | (U, es)

Weak head normalisation
=======================

The only interesting case:

-------------
 Σ ⊢ f es ⇓ …

All other terms reduce to themselves.

TODO: If we solve a constraint, then we may get β-redexes.

Blocked term reduction
======================

∅ ⚷ u ↝ u

Type checking
=============

Signature changes are propagated in the obvious way.

 Σ := Σ, α : Γ → A
------------------------------------ (α fresh)
 Γ ⊢ _ ⇐ A ↝ α Γ

 Γ ⊢ i ⇒ (A, u)
 Γ ⊢ A = B ⇐ Set ↝ C
----------------------------------------
 Γ ⊢ i ⇐ B ↝ (C ⚷ λ Γ → u) Γ

 Γ ⊢ i ⇒ C ⚷ p
---------------------------------------------------------------------
 Γ ⊢ i ⇐ B ↝ (C ⚷ p >>= λ (A, u) → ({Γ ⊢ A = B ⇐ Set} ⚷ λ Γ → u)) Γ

 Σ ⊢ A ⇓ t₁ ≡_B t₂
 Γ ⊢ t₁ = t₂ ⇐ B ↝ C
-------------------------
 Γ ⊢ refl ⇐ A ↝ C ⚷ refl

 Σ ⊢ A ⇓ C ⚷ B
---------------------------------------
 Γ ⊢ refl ⇐ A ↝ C ⚷ (Γ ⊢ refl ⇐ B)

 Σ ⊢ A ⇓ (x : A₁) → A₂
 Γ, x : A₁ ⊢ t ⇐ A₂ ↝ u
---------------------------
 Γ ⊢ λ x → t ⇐ A ↝ λ x → u

 Σ ⊢ A ⇓ C ⚷ B
---------------------------------------------
 Γ ⊢ λ x → t ⇐ A ↝ C ⚷ (Γ ⊢ λ x → t ⇐ B)

 Σ ⊢ A ⇓ D us
 c : (xs : Ps) → Δ → D xs ∈ Σ
 Γ ⊢ ts ⇐ Δ[×s ≔ us] ↝ vs
---------------------------------
 Γ ⊢ c ts ⇐ A ↝ c vs

  To type check the list of arguments to the data constructor:

     Γ ⊢ t ⇐ A ↝ u
     Γ ⊢ ts ⇐ Δ[x ≔ t] ↝ us
    ---------------------------
     Γ ⊢ t ts ⇐ (x : A) Δ ↝ u us

    ---------
     Γ ⊢ ε ⇐ ε ↝ ε

 Σ ⊢ A ⇓ C ⚷ B
-------------------------------------
 Γ ⊢ c ts ⇐ A ↝ C ⚷ (Γ ⊢ c ts ⇐ B)

Type inference
==============

----------------------
 Γ ⊢ Set ⇒ (Set, Set)

 Γ ⊢ A ⇐ Set ↝ U
 Γ, x : U ⊢ B ⇐ Set ↝ V
--------------------------------------
 Γ ⊢ (x : A) → B ⇒ (Set, (x : U) → V)

 Γ ⊢ A ⇐ Set ↝ U
 Γ ⊢ t₁ ⇐ U ↝ u₁
 Γ ⊢ t₂ ⇐ U ↝ u₂
----------------------------------
 Γ ⊢ t₁ ≡_A t₂ ⇒ (Set, u₁ ≡_U u₂)

-------------------------------------------------------
 Γ ⊢ J ⇒ ((A : Set) → (x : A) → (y : A) →
          (P : (x y : A) → x ≡_A y → Set) →
          ((x : A) → P x x refl) →
          (eq : x ≡_A y) → P x y eq
         , J
         )

-------------------------------------------
 Γ ⊢ K ⇒ ((A : Set) → (x : A) →
          (P : (x : A) → x ≡_A x → Set) →
          ((x : A) → P x refl) →
          (eq : x ≡_A x) → P x eq
         , K
         )

 h : A ∈ Σ
 Γ ⊢ es ⇐ A ↝ (B, es′)
---------------------
 Γ ⊢ h es ⇒ (B, h es′)

 h : A ∈ Σ
 Γ ⊢ es ⇐ (A, h) ↝ C ⚷ eps
---------------------------------------------
 Γ ⊢ h es ⇒ C ⚷ eps >>= λ (B, es′) → (B, h es′)

  To type check list of eliminators:

     Γ ⊢ e ⇐ (A₁, h) ⇒ (A₂, e′)
     Γ ⊢ es ⇐ (A₂, h e′) ⇒ (A₃, es′)
    ----------------------------
     Γ ⊢ e es ⇐ (A₁, h) ⇒ (A₃, e′ es′)

     Γ ⊢ e ⇐ (A₁, h) ⇒ C ⚷ ep
    --------------------------------------------------------------------
     Γ ⊢ e es ⇐ (A₁, h) ⇒ C ⚷ ep                    >>= λ (A₂, e′) →
                              {Γ ⊢ es ⇐ (A₂, h e′)} >>= λ (A₃, es′) →
                              (A₃, e′ es′)

     Γ ⊢ e ⇐ (A₁, h) ⇒ (A₂, e′)
     Γ ⊢ es ⇐ (A₂, h e′) ⇒ C ⚷ eps
    ----------------------------------------------------
     Γ ⊢ e es ⇐ (A₁, h) ⇒ C ⚷ eps >>= λ (A₃, es′) →
                              (A₃, e′ es′)

    -----------------
     Γ ⊢ ε ⇐ (A, h) ⇒ (A, ε)

  To type check a single eliminator

     Σ ⊢ A ⇓ (x : A₁) → A₂
     Γ ⊢ t ⇐ A₁ ↝ u
    --------------------------------
     Γ ⊢ · t ⇐ (A, h) ⇒ (A₂[x ≔ u], · u)

     Σ ⊢ A ⇓ C ⚷ B
    --------------------------------------------
     Γ ⊢ · t ⇐ (A, h) ⇒ C ⚷ (Γ ⊢ · t ⇐ (B, h))

        Down here you seem to have to carry around the head so that we
        can get the final type for the record projection.

     Σ ⊢ A ⇓ R ts
     π : (xs : Ps) → (r : R xs) → B ∈ Σ
    --------------------------------------------
     Γ ⊢ π · ⇐ (A, h) ⇒ (B[xs ≔ ts, r ≔ h], π ·)

     Σ ⊢ A ⇓ C ⚷ B
    -------------------------------------
     Γ ⊢ π · ⇐ (A, h) ⇒ C ⚷ (Γ ⊢ π · ⇐ (B, h))
