Reconstructing types from erased bidirectional syntax

	{-# OPTIONS --erasure #-}

	module Reconstruct where

	open import Data.Unit
	open import Data.Product

	data Ty : Set where
	Π : Ty → Ty → Ty

	data Con : Set where
	`1 : Con
	_∙_ : Con → Ty → Con

	variable
	Γ : Con
	@0 Γ₀ : Con
	A B : Ty
	@0 A₀ B₀ : Ty

	data Mode : Set where
	chk inf : Mode

	-- Erased annotations
	data Tm : Mode → @0 Con → @0 Ty → Set where
	q : Tm inf (Γ₀ ∙ A₀) A₀
	_[p] : Tm inf Γ₀ A₀ → Tm inf (Γ₀ ∙ B₀) A₀
	lam : Tm chk (Γ₀ ∙ A₀) B₀ → Tm chk Γ₀ (Π A₀ B₀)
	app : Tm inf Γ₀ (Π A₀ B₀) → Tm chk Γ₀ A₀ → Tm inf Γ₀ B₀

	switch : Tm inf Γ₀ A₀ → Tm chk Γ₀ A₀
	ann : (A : Ty) → Tm chk Γ₀ A → Tm inf Γ₀ A

	-- Relevant annotations
	data TmA : Con → Ty → Set where
	qA : TmA (Γ ∙ A) A
	_[p]A : TmA Γ A → TmA (Γ ∙ B) A
	lamA : TmA (Γ ∙ A) B → TmA Γ (Π A B)
	appA : TmA Γ (Π A B) → TmA Γ A → TmA Γ B

	data Rel {A : Set} : @0 A → A → Set where
	rel : (a : A) → Rel a a

	infer : (Γ : Con) → Tm inf Γ A₀ → Σ[ A ∈ Ty ] (Rel A₀ A × TmA Γ A)
	check : (Γ : Con) → (A : Ty) → Tm chk Γ A → TmA Γ A

	check Γ (Π A B) (lam t) = lamA (check (Γ ∙ A) B t)
	check Γ A (switch t) with (infer Γ t)
	... \| A , rel _ , t = t

	infer (Γ ∙ A) q = A , rel A , qA
	infer (Γ ∙ B) (t [p]) with (infer Γ t)
	... \| A , rel _ , t' = A , rel A , t' [p]A
	infer Γ (app t u) with (infer Γ t)
	... \| Π A B , rel _ , t' = B , rel B , appA t' (check Γ A u)
	infer Γ (ann A t) = A , rel A , check Γ A t

参与讨论