[Agda] Help with stuck unification/intrinsic typing in general

[Neel Krishnaswami]

Dear Daniel.

In general, intrinsically typed representations are definitely the way 
to go when your object language does not have a conversion relation.

If your language does have a conversion or judgemental equality 
relation, then intrinsic representations are enormously harder to work 
with. The basic issue is that the datatype representing typing will have 
proof trees corresponding to derivations of judgemental equality, and 
quotienting by the derivation of convertibility is giant PITA. (This is 
still active research, and I'm not actually up to date on where the 
state of the art here is -- probably Thorsten knows.)

In your particular case, however, it looks like you have a different 
problem. The _._ constructor in your screen shot has the type:

    _·_ : ∀{Δ} {Γ₁ Γ₂ : Context Δ} {A B q}
         → Γ₁ ⊢ A -⟨ q ⟩→ B
         → Γ₂ ⊢ A
         → (q ** Γ₂ ++ Γ₁) ⊢ B

Here, the return type of the function has an index which has function 
calls in it:

         ... → (*q ** Γ₂ ++ Γ₁*) ⊢ B

The Agda type inference algorithm uses unification, and unification 
problems involving calls to arbitrary functions are, in general, 
hopeless. *Unification and pattern match coverage will generally only 
work reliably if the return type's indices contain expressions made only 
from variables and data constructors. *
**

If memory serves, Conor McBride calls indices containing function calls 
"green slime", and warns people never to touch it. The way to keep from 
being contaminated by green slime is to use an explicit equality -- if 
you change your datatype declaration to the following:

    _·_ : ∀{Δ} {Γ₁ Γ₂ Θ : Context Δ} {A B q}
         → Γ₁ ⊢ A -⟨ q ⟩→ B
         → Γ₂ ⊢ A
         → Θ ≡ q ** Γ₂ ++ Γ₁
         → Θ ⊢ B

The case splitter will see the variable Θ and happily introduce a case 
for the _·_ constructor. But in the case branch, you will possess the 
equality Θ ≡ q ** Γ₂ ++ Γ₁ which you can use to do any necessary 
reasoning yourself, thereby sparing the match coverage algorithm from 
having to do arbitrary mathematical reasoning.

Best,
Neel

On 01/10/2020 04:48, Daniel Lee wrote:
> Hi all,
>
> I'm super new to Agda and the Agda community. Hopefully this is the right
> place to ask something like this, but please call me out if it isn't.
>
>
> I'm working on an Agda development for a QTT formalization. I'm trying to
> use an intrinsically typed representation for terms, but run into
> unification issues when trying to define substitution.
>
> Substitution:
> [image: Screen Shot 2020-09-30 at 8.34.38 PM.png]
>
> Error message:
> [image: Screen Shot 2020-09-30 at 8.34.50 PM.png]
>
> Application def:
> [image: Screen Shot 2020-09-30 at 8.35.05 PM.png]
>
> I'm sort of at a loss for how to get around this. Is the issue because of
> the functions in the return type?
>
> More broadly, it seems like intrinsic typing is the Agda way of doing
> things, and gives a lot for free. And it works really well in the STLC
> example given in the PLFA textbook. But for a more complicated type system
> like this, I'm starting to think it might be easier to use extrinsic
> typing? I've also had to rely on the REWRITE pragma which I just learned
> isn't allowed in --safe due to potential non-convergence.
> Does someone maybe have experience with this and could speak to pros/cons
> of using intrinsic vs extrinsic typing here?
>
> Thanks,
> Daniel
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Neel Krishnaswami
nk480 at cl.cam.ac.uk

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201001/9942eff6/attachment.html>