[Agda] This works in Idris by not in agda. (updating the type from the values of the constructor)

[Jesper Cockx]

>
> Is Agda's unifier too eager in this case?


Agda's case splitter requires all unification problems from the previous
case split to be solved before it can start on the next one. In other
words, each set of patterns must correspond to a series of consecutive case
splits.

In this case, it first wants to complete the case split on the argument of
type "Test zero" before it continues with the case split on the argument of
Tost. But for this first case split Agda needs to unify zero with "fn n",
which fails because "fn n" doesn't reduce. It doesn't know yet whether n is
equal to zero or suc because that case split only comes after the current
one.

In this case it would theoretically be possible to postpone the unification
problem and first do the second case split, which would solve the problem.
But in general this would be problematic as the types of the constructor
arguments may change as a result of the unification. So a proper solution
would require interleaving case splitting and unification, allowing
unification problems to persist over multiple case splits.

This is certainly a cool idea, but would require a nontrivial engineering
effort to represent this more general split-and-unify problem. Does someone
have an idea if this is what they do in Idris, or do they have a different
solution to the problem?

Jesper

On Sun, Dec 11, 2016 at 7:50 AM, Roman <effectfully at gmail.com> wrote:

> If you postpone unication a bit, `tn` type checks:
>
> open import Relation.Binary.PropositionalEquality
>
> data Test : ℕ → Set where
>   Tist : Test zero
>   Tostq : ∀ {m} → (n : ℕ) → m ≡ fn n → Test m
>
> pattern Tost n = Tostq n refl
>
> tn : (n : ℕ) → Test (fn n) → ℕ
> tn zero  Tist          = zero
> tn zero (Tost  zero)   = zero
> tn zero (Tost (suc n)) = zero
> tn (suc y) x = {!!}
>
> Is Agda's unifier too eager in this case?
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161211/cfa47ad8/attachment.html