Using irrelevance to get decent code extraction

Irrel.agda

module Irrel where

open import Data.Bool using (if_then_else_)
open import Data.Maybe using (Maybe; just; nothing; map; _>>=_)
open import Data.Nat using (ℕ; suc; zero)
open import Data.Product using (Σ; _,_)
open import Data.String using (String; _==_)
open import Data.Unit using (⊤)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

data Fin : .ℕ → Set where
  zero : ∀ .{n : ℕ} → Fin (suc n)
  suc : ∀ .{n : ℕ} → Fin n → Fin (suc n)

data Vec (A : Set) : .ℕ → Set where
  [] : Vec A zero
  _∷_ : ∀ .{n : ℕ} → A → Vec A n → Vec A (suc n)

data _[_]=_ .{n : ℕ} {A : Set} : .(Vec A n) → .(Fin n) → .A → Set where
  here :
    ∀ .{a : A} .{as : Vec A n} →
    (a ∷ as) [ zero {n} ]= a
  there :
    ∀ .{a b : A} .{as : Vec A n} →
    ∀ .{n : Fin n} →
    as [ n ]= a → (b ∷ as) [ suc n ]= a

data Type : Set where
  TArr : Type → Type → Type
  TUnit : Type

eqType : (t u : Type) → Maybe (t ≡ u)
eqType TUnit TUnit = just refl
eqType (TArr a b) (TArr a' b') with (eqType a a')
eqType (TArr a b) (TArr a' b') | nothing = nothing
eqType (TArr a b) (TArr a' b') | just refl with (eqType b b')
eqType (TArr a b) (TArr a b') | just refl | nothing = nothing
eqType (TArr a b) (TArr a b') | just refl | just refl = just refl
eqType _ _ = nothing

toArrow : (t : Type) → Maybe (Σ Type (λ A → Σ Type (λ B → t ≡ TArr A B)))
toArrow (TArr A B) = just (A , B , refl)
toArrow _ = nothing

data Term : .{n : ℕ} → .(Vec Type n) → .Type → Set where
  Var :
    ∀ .{n : ℕ} .{Γ : Vec Type n} →
    ∀ .{A : Type} →
    (ix : Fin n) →
    .{lookup : Γ [ ix ]= A} →
    Term Γ A
  App :
    ∀ .{n : ℕ} .{Γ : Vec Type n} →
    ∀ .{A B : Type} →
    Term Γ (TArr A B) →
    Term Γ A →
    Term Γ B
  Lam :
    ∀ .{n : ℕ} .{Γ : Vec Type n} →
    ∀ .{A B : Type} →
    Term (A ∷ Γ) B →
    Term Γ (TArr A B)
  Unit :
    ∀ .{n : ℕ} .{Γ : Vec Type n} →
    Term Γ TUnit

data Syntax : Set where
  Var : String → Syntax
  App : Syntax → Syntax → Syntax
  Lam : String → Type → Syntax → Syntax
  Unit : Syntax

record Entry .{n : ℕ} .(Γ : Vec Type n): Set where
  constructor entry
  field
    ix : Fin n
    ty : Type
    .prf : Γ [ ix ]= ty

synth :
  ∀ .{n : ℕ} .{Γ : Vec Type n} →
  (String → Maybe (Entry Γ)) →
  Syntax →
  Maybe (Σ Type (Term Γ))
synth lookup (Var x) =
  map
    (λ { (entry ix ty prf) → (ty , Var ix {lookup = prf}) })
    (lookup x)
synth lookup (App a b) =
  synth lookup a >>= λ { (aTy , a') →
  synth lookup b >>= λ { (bTy , b') →
  toArrow aTy >>= λ { (A , B , refl) →
  map (λ { refl → (B , App a' b') }) (eqType A bTy)
  } } }
synth {n} {Γ} lookup (Lam x t s) =
  synth
    {Γ = t ∷ Γ}
    (λ str →
     if str == x
     then just (entry (zero {n}) t (here {a = t} {as = Γ}))
     else
       map
         (λ { (entry ix u prf) → entry (suc ix) u (there {a = t} {b = u} prf) })
         (lookup str)
    )
    s
synth lookup Unit = just (TUnit , Unit)

-- Why does this type check?
test : (T : Type) → Term [] T → ⊤
test (TArr A B) tm = {!!}
test TUnit (Var ix) = {!!}
test TUnit (App tm tm₁) = {!!}
test TUnit (Lam tm) = {!!}
test TUnit Unit = {!!}