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

[Andreas Abel]

Agda's promise is that everything that is generated by successive splits 
can be type-checked. (That this promise is not always kept is another 
story).

At this point

   tn : (n : ℕ) → Test (fn n) → ℕ
   tn zero    t = {!t!}
   tn (suc n) t = {!!}

there is no way to split on t : Test 0 since it is not clear whether 
Tost is a possible case:

   I'm not sure if there should be a case for the constructor Tost,
   because I get stuck when trying to solve the following unification
   problems (inferred index ≟ expected index):
     fn n ≟ fn zero

What should be the result of splitting on t?  A deep splitting until all 
unification constraints are satisfied??

I am not sure there is a clear story behind this example, except Roman's 
advice: Be careful with function applications in the target type of your 
constructors!

--Andreas

On 11.12.2016 11:29, Jesper Cockx wrote:
>     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
> <mailto: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 <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/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/