<div dir="ltr"><div><div><div>Thank you very much, Andreas, for the explanation.<br></div>Now it's clear to me from where the problem arises.<br><br></div><div>Best regards,<br></div><div>Dmytro <br><br></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">2014-12-06 14:21 GMT+02:00 Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Unfortunately, the order of arguments in the constructor matters for the coverage checker in such delicate cases. I filed an issue derived from your problem:<br>
<br>
<a href="https://code.google.com/p/agda/issues/detail?id=1384" target="_blank">https://code.google.com/p/<u></u>agda/issues/detail?id=1384</a><br>
<br>
If you take look there, putting the equality proof in the constructor earlier works.<br>
<br>
Ideally, every program that is generated by subsequent splits (C-c C-c) should be accepted by Agda. Unfortunately, in the resulting code the split order is no longer visible, and Agda tries to guess an order that works. It does not always.<br>
<br>
Sorry, at the moment you are forced to try and error. Agda logging can be enabled with the -v option, but I am afraid the logs only make sense if you read the source code side by side. There is no user-friendly log where Agda gives an executive summary of what it did. (Contributions welcome!)<br>
<br>
Note that sets of clauses that do not cover all cases are making the problem for the coverage checker even harder! This is why you get the failure when you comment-out the catch-all.<br>
<br>
The following snippet of the CHANGELOG gives a hint on the strategy of the coverage checker:<br>
<br>
<br>
* Improved coverage checker. The coverage checker splits on<br>
arguments that have constructor or literal pattern, committing<br>
to the left-most split that makes progress.<br>
Consider the lookup function for vectors:<br>
<br>
data Fin : Nat → Set where<br>
zero : {n : Nat} → Fin (suc n)<br>
suc : {n : Nat} → Fin n → Fin (suc n)<br>
<br>
data Vec (A : Set) : Nat → Set where<br>
[] : Vec A zero<br>
_∷_ : {n : Nat} → A → Vec A n → Vec A (suc n)<br>
<br>
_!!_ : {A : Set}{n : Nat} → Vec A n → Fin n → A<br>
(x ∷ xs) !! zero = x<br>
(x ∷ xs) !! suc i = xs !! i<br>
<br>
In Agda up to 2.3.0, this definition is rejected unless we add<br>
an absurd clause<br>
<br>
[] !! ()<br>
<br>
This is because the coverage checker committed on splitting<br>
on the vector argument, even though this inevitably lead to<br>
failed coverage, because a case for the empty vector [] is missing.<br>
<br>
The improvement to the coverage checker consists on committing<br>
only on splits that have a chance of covering, since all possible<br>
constructor patterns are present. Thus, Agda will now split<br>
first on the Fin argument, since cases for both zero and suc are<br>
present. Then, it can split on the Vec argument, since the<br>
empty vector is already ruled out by instantiating n to a suc _.<span class=""><br>
<br>
<br>
On 06.12.2014 12:03, Dmytro Starosud wrote:<br>
</span><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">
Sorry :)<br>
One more issue. Please see another gist<br>
<a href="https://gist.github.com/dima-starosud/f27ffd54895822a7db03" target="_blank">https://gist.github.com/dima-<u></u>starosud/f27ffd54895822a7db03</a><br>
Here I (hopefully) did as you proposed.<br>
But I still able to make Agda showing that annoying unification problem<br>
error message.<br>
<br>
Looks like the problem is related to totality checker?<br>
I think the real cause is simply shadowed?<br>
<br>
Please help me understating this.<br>
Is there any way to enable Agda logging or something else to see what<br>
happens behind the scene?<br>
<br>
Thanks a lot,<br>
Dmytro<br>
<br>
<br>
2014-12-06 12:37 GMT+02:00 Dmytro Starosud <<a href="mailto:d.starosud@gmail.com" target="_blank">d.starosud@gmail.com</a><br></span>
<mailto:<a href="mailto:d.starosud@gmail.com" target="_blank">d.starosud@gmail.com</a>>><u></u>:<span class=""><br>
<br>
...and one more question.<br>
<br>
How the way you are proposing differs from "reduce₃"?<br>
<br>
Does not "reduce₃" turn non-pattern indexes to good one?<br>
Since as you can see "reduce₂" doesn't produce error messages.<br>
<br>
Thanks,<br>
Dmytro<br>
<br>
<br>
2014-12-06 12:28 GMT+02:00 Dmytro Starosud <<a href="mailto:d.starosud@gmail.com" target="_blank">d.starosud@gmail.com</a><br></span>
<mailto:<a href="mailto:d.starosud@gmail.com" target="_blank">d.starosud@gmail.com</a>>><u></u>:<span class=""><br>
<br>
Thanks, Andreas,<br>
<br>
I had a kind of similar thoughts, but needed confirmation.<br>
So, the rule is "do not use functional dependencies as a family<br>
indexes, but just constructors".<br>
Please correct if this is not accurate statement.<br>
<br>
What is the root cause (I mean what difficulties in<br>
compiler/theory) which sometimes doesn't allow solving such<br>
unification problems?<br>
<br>
Thanks a lot,<br>
Dmytro<br>
<br>
<br>
2014-12-06 10:57 GMT+02:00 Andreas Abel <<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a><br></span>
<mailto:<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>>>:<span class=""><br>
<br>
The problem is that you are indexing your family Term by<br>
non-patterns in some of the constructor cases. Then Agda<br>
can sometimes not solve the unification constraints involved<br>
in dependent pattern matching, and gives up or produces<br>
error messages. The solution is to use explicit proofs of<br>
equality in your constructors instead.<br>
<br>
Here is a cut-down version of your plight:<br>
<br>
module _ where<br>
<br>
open import Data.Bool<br></span>
open import Relation.Binary.__<u></u>PropositionalEquality<div><div class="h5"><br>
<br>
module NonPatternFamily where<br>
<br>
data Term : Bool → Set where<br>
I : Term false<br>
App : (a b : Bool) → Term a → Term b → Term (a ∨ b)<br>
-- Non-pattern in target of App<br>
-- _∨_ is a defined function, not a constructor.<br>
<br>
fails : Term false → Set<br>
fails (App false false I x) = Bool<br>
fails _ = Bool<br>
<br>
-- a ∨ b != false of type Bool<br>
-- when checking that the pattern App false false I x has<br>
type<br>
-- Term false<br>
<br>
-- Radical fix: no index to Term, just parameter:<br>
<br>
module JustData where<br>
<br>
-- Version with no indices at all, only parameters.<br>
<br>
data Term (i : Bool) : Set where<br>
I : i ≡ false → Term i<br>
App : (a b : Bool) → i ≡ a ∨ b → Term a → Term b → Term i<br>
<br>
test : Term false → Set<br>
test (App false false refl (I refl) x) = Bool<br>
test _ = Bool<br>
<br>
-- Moderate fix: retain the index in harmless (pattern case).<br>
<br>
module PatternFamily where<br>
<br>
-- Version with index,<br>
-- but using equality when non-pattern index would be needed.<br>
<br>
data Term : (i : Bool) → Set where<br>
I : Term false<br>
App : (i a b : Bool) → i ≡ a ∨ b → Term a → Term b → Term i<br>
<br>
test : Term false → Set<br>
test (App .false false false refl I x) = Bool<br>
test _ = Bool<br>
<br>
Hope that helps,<br>
Andreas<br>
<br>
<br>
<br>
On 05.12.2014 22:47, Dmytro Starosud wrote:<br>
<br>
Hello guys,<br>
<br>
I am trying to write a function on indexed types:<br></div></div>
<a href="https://gist.github.com/dima-__starosud/7100947b0e243ea6a034" target="_blank">https://gist.github.com/dima-_<u></u>_starosud/7100947b0e243ea6a034</a><span class=""><br>
<<a href="https://gist.github.com/dima-starosud/7100947b0e243ea6a034" target="_blank">https://gist.github.com/dima-<u></u>starosud/7100947b0e243ea6a034</a>><br>
But I cannot understand the reason of the error messages<br>
shown, and how<br>
to solve issues arisen.<br>
<br>
Please see a gist (link above).<br>
Ideally I wanted "reduce₁". But that didn't compile.<br>
(And I think I can<br>
imagine the reason why)<br>
<br>
Next attempt was "reduce₂". But this would involve a lot<br>
of unnecessary<br>
code on RHSs.<br>
<br>
Than I decided to improve it and got "reduce₃", but it<br>
gave me<br>
completely puzzling error message.<br>
<br>
Please help me to understand all that stuff Agda<br>
communicates to me.<br>
<br>
I would like something really simple (like "reduce₁"),<br>
probably with<br>
help of *pattern*s.<br>
<br>
Thanks in advance,<br>
Dmytro<br>
<br>
<br>
<br></span>
______________________________<u></u>___________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><u></u>><br>
<a href="https://lists.chalmers.se/__mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/__<u></u>mailman/listinfo/agda</a><span class=""><br>
<<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a>><br>
<br>
<br>
<br>
--<br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br></span>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a> <mailto:<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a>><br>
<a href="http://www2.tcs.ifi.lmu.de/~__abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~__<u></u>abel/</a><br>
<<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a>><br>
<br>
<br>
<br>
<br>
</blockquote><div class="HOEnZb"><div class="h5">
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</div></div></blockquote></div><br></div>