[Agda] Strange behaviour of instance search.

[Andreas Abel]

Seems like you want to report an issue or add your description to the 
existing issues.

   https://code.google.com/p/agda/issues/list?q=label%3AInstance

On 01.06.2015 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 `Δ'.
> So I switched to instance arguments:
>
>      postulate
>        _extends_ : Con -> Con -> Set
>
>        instance
>          extends-stop : ∀ {Γ} -> Γ extends Γ
>          extends-skip : ∀ {Γ Δ σ} {{_ : Δ extends Γ}} -> (Δ ▻ σ) extends Γ
>
>        lam : ∀ {Γ σ τ} -> ((∀ {Δ} {{_ : Δ extends (Γ ▻ σ)}} -> Δ ⊢ σ)
> -> Γ ▻ σ ⊢ τ) -> Γ ⊢ σ ⇒ τ
>
>      I : Term (ι ⇒ ι)
>      I = lam λ x -> x
>
>      K : Term (ι ⇒ ι ⇒ ι)
>      K = lam λ x -> lam λ y -> x
>
> So far so good, but when I tried
>
>      A : Term ((ι ⇒ ι) ⇒ ι ⇒ ι)
>      A = lam λ f -> lam λ x -> f · x
>
> Agda just started to consume memory, and I killed the process after it
> had eaten 1+ GB of memory.
>
> But if I provide instance arguments explicitly
>
>      A : Term ((ι ⇒ ι) ⇒ ι ⇒ ι)
>      A = lam λ f -> lam λ x -> f {{extends-skip {{extends-stop}}}} · x
> {{extends-stop}}
>
> Agda happily accepts the definition.
>
> Is it the expected behaviour?
>
> The code: https://github.com/effectfully/random-stuff/blob/master/stuff/TypedJigger.agda
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/