[Agda] Strange behaviour of instance search.

[Nils Anders Danielsson]

On 2015-06-01 01:31, effectfully wrote:
> Hi. I want to adapt Conor McBride's trick
>
>      https://personal.cis.strath.ac.uk/conor.mcbride/fooling/Jigger.agda
>
> to basic encoding of STLC:
>
>      data _⊢_ Γ : Type -> Set where
>        var : ∀ {σ}   -> σ ∈ Γ     -> Γ ⊢ σ
>        ƛ_  : ∀ {σ τ} -> Γ ▻ σ ⊢ τ -> Γ ⊢ σ ⇒ τ
>        _·_ : ∀ {σ τ} -> Γ ⊢ σ ⇒ τ -> Γ ⊢ σ     -> Γ ⊢ τ
>
> I started from
>
>      _▻▻_ : Con -> Con -> Con
>      Γ ▻▻  ε      = Γ
>      Γ ▻▻ (Δ ▻ σ) = Γ ▻▻ Δ ▻ σ
>
>      postulate
>        naive-lam : ∀ {Γ σ τ} -> ((∀ {Δ} -> Γ ▻ σ ▻▻ Δ ⊢ σ) -> Γ ▻ σ ⊢
> τ) -> Γ ⊢ σ ⇒ τ
>
>      yellow : Term (ι ⇒ ι)
>      yellow = naive-lam λ x -> x
>
> But Agda can't infer `Δ' from (Γ ▻ σ ▻▻ Δ), since there is pattern
> matching on `Δ'.

I once adapted Conor's trick to Kipling (the language in Outrageous but
Meaningful Coincidences). The same approach works here.

The key trick in Jigger.agda seems to be that addition is used with the
arguments "the wrong way around". This is not possible for
contexts/context extensions, but one can index contexts by their length
and use addition with the arguments the wrong way around in the index of
the append operation.

More concretely:

* Make contexts length-indexed, and define them using record types (to
   enable η-equality):

     Con : ℕ -> Set
     Con zero    = ⊤
     Con (suc n) = Con n × Type

     pattern ε       = tt
     pattern _▻_ Γ σ = Γ , σ

* Define append in the following way:

     _▻▻_ : ∀ {m n} -> Con m -> Con n -> Con (m + n)
     _▻▻_         {n = zero}  Γ  ε      = subst Con (m≡m+0 _)              Γ
     _▻▻_ {m = m} {n = suc _} Γ (Δ ▻ σ) = subst Con (1+[m+n]≡m+[1+n] m _) (Γ ▻▻ Δ ▻ σ)

-- 
/NAD