[Agda] Instance arguments and hole types

[Tillmann Rendel]

Hi,

I'm trying to use Agda's instance arguments to overload the ⟦_⟧ function 
for various different types of syntax, and it works. But it is less 
convenient than I hoped, because sometimes, the Emacs mode shows the 
overloading plumbing instead of inlining it away.

Here's what I have, starting with the overloading apparatus:
> open import Level
>
> record Meaning (Syntax : Set) {ℓ : Level} : Set (suc ℓ) where
>   constructor
>     meaning
>   field
>     Semantics : Set ℓ
>     ⟦_⟧ : Syntax → Semantics
>
> open Meaning {{...}}

Lets define the syntax and semantics of simple types:

> data Type : Set where
>   _⇒_ : (τ₁ τ₂ : Type) → Type
>
> ⟦_⟧Type : Type → Set
> ⟦ τ₁ ⇒ τ₂ ⟧Type = ⟦ τ₁ ⟧Type → ⟦ τ₂ ⟧Type
>
> meaningOfTypes : Meaning Type
> meaningOfTypes = meaning Set ⟦_⟧Type

And for contexts:

> data Context : Set where
>   ∅ : Context
>   _∷_ : Type → Context → Context
>
> data Empty : Set where
>   ∅ : Empty
>
> data Bind (A B : Set) : Set where
>   _∷_ : A → B → Bind A B
>
> ⟦_⟧Context : Context → Set
> ⟦ ∅ ⟧Context = Empty
> ⟦ τ ∷ Γ ⟧Context = Bind ⟦ τ ⟧ ⟦ Γ ⟧Context
>
> meaningOfContexts : Meaning Context
> meaningOfContexts = meaning Set ⟦_⟧Context

Note that in the last equation for ⟦_⟧Context, we can use ⟦ τ ⟧ instead 
of ⟦ τ ⟧Type. That's the point of the exercise, and it seems to work.

We can also define variables as pointers into contexts:

> data Var : Context → Type → Set where
>   this : ∀ {Γ τ} →
>     Var (τ ∷ Γ) τ
>   that : ∀ {Γ τ₁ τ₂} →
>     Var Γ τ₂ →
>     Var (τ₁ ∷ Γ) τ₂
>
> ⟦_⟧Var : ∀ {Γ τ} → Var Γ τ → ⟦ Γ ⟧ → ⟦ τ ⟧
> ⟦ this ⟧Var (v ∷ ρ) = v
> ⟦ that x ⟧Var (v ∷ ρ) = ⟦ x ⟧Var ρ
>
> meaningOfVars : ∀ {Γ τ} → Meaning (Var Γ τ)
> meaningOfVars {Γ} {τ} = meaning (⟦ Γ ⟧ → ⟦ τ ⟧) ⟦_⟧Var

I especially like the type of ⟦_⟧Var. That's what I would write on a 
blackboard.

We can do the same for terms:

> data Term : Context → Type → Set where
>   lam : ∀ {Γ τ₁ τ₂} →
>     Term (τ₁ ∷ Γ) τ₂ →
>     Term Γ (τ₁ ⇒ τ₂)
>   app : ∀ {Γ τ₁ τ₂} →
>     Term Γ (τ₁ ⇒ τ₂) →
>     Term Γ τ₁ →
>     Term Γ τ₂
>   var : ∀ {Γ τ} →
>     Var Γ τ →
>     Term Γ τ
>
> ⟦_⟧Term : ∀ {Γ τ} → Term Γ τ → ⟦ Γ ⟧ → ⟦ τ ⟧
> ⟦ lam t ⟧Term ρ = ?
> ⟦ app t₁ t₂ ⟧Term ρ = ?
> ⟦ var x ⟧Term ρ = ?

Looks good so far, and if we fill the holes correctly, it will typecheck 
just fine:

> ⟦_⟧Term : ∀ {Γ τ} → Term Γ τ → ⟦ Γ ⟧ → ⟦ τ ⟧
> ⟦ lam t ⟧Term ρ = λ v → ⟦ t ⟧Term (v ∷ ρ)
> ⟦ app t₁ t₂ ⟧Term ρ = ⟦ t₁ ⟧Term ρ (⟦ t₂ ⟧Term ρ)
> ⟦ var x ⟧Term ρ = ⟦ x ⟧ ρ
>
> meaningOfTerms : ∀ {Γ τ} → Meaning (Term Γ τ)
> meaningOfTerms {Γ} {τ} = meaning (⟦ Γ ⟧ → ⟦ τ ⟧) ⟦_⟧Term

Note that we can call ⟦ x ⟧ in the last equation of ⟦_⟧Term without 
problems.


But lets see what help the Emacs mode is giving us when filling the 
first hole. The type of the first hole is reported as follows.

> ⟦ .τ₁ ⟧Type → ⟦ .τ₂ ⟧Type

This is fine for me. So lets fill the hole a bit:

> ⟦ lam t ⟧Term ρ = λ v → ⟦ t ⟧Term ?

The Emacs mode reports the following type for the new hole:

> Bind (Meaning.⟦ meaning Set ⟦_⟧Type ⟧ .τ₁) ⟦ .Γ ⟧Context

This is not optimal. I would prefer what I get with C-c C-t:

> Bind ⟦ .τ₁ ⟧Type ⟦ .Γ ⟧Context

What can I do to have the redex (Meaning.⟦ meaning Set ⟦_⟧Type ⟧ .τ₁) 
automatically reduced here?

   Tillmann