Golfing the classy hack

GolfedClassyHack.agda

{-
Conor McBride's "classy hack" for getting HOAS notation for FOAS: https://mazzo.li/epilogue/index.html%3Fp=773.html
The following is a code-golfed version where we observe that by sprinkling some singletons
in the standard FOAS definition of terms, we get an equivalent definition (because singletons are
contractible) which supports HOAS notation directly.
-}

{-# OPTIONS --backtracking-instance-search #-}

open import Relation.Binary.PropositionalEquality
open import Data.Product

infixr 4 _⇒_
data Ty : Set where
  ι   : Ty
  _⇒_ : Ty → Ty → Ty

infixl 3 _▶_
data Con : Set where
  ∙   : Con
  _▶_ : Con → Ty → Con

variable
  Γ Δ : Con
  A B C : Ty

Sing : ∀ {i}{A : Set i} → A → Set i
Sing x = ∃ λ x' → x' ≡ x

data _≤_ : Con → Con → Set where
  instance here  : Γ ≤ Γ
  instance there : ⦃ _ : Γ ≤ Δ ⦄ → Γ ≤ (Δ ▶ A)

data Tm Γ : Ty → Set where
  var : Sing (Δ ▶ A) → ⦃ _ : (Δ ▶ A) ≤ Γ ⦄ → Tm Γ A
  lam : (Sing (Γ ▶ A) → Tm (Γ ▶ A) B) → Tm Γ (A ⇒ B)
  app : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B

ex : Tm ∙ ((ι ⇒ ι ⇒ ι) ⇒ ι ⇒ ι ⇒ ι)
ex = lam λ f → lam λ x → lam λ y → app (app (var f) (var y)) (var x)