<div dir="ltr"><div><div>Right now, Agda considers all arguments of a constructor to be strongly
rigid, even the non-recursive ones (i.e. the ones whose type doesn't mention the datatype). But this is not justified by the
recursion principle for the datatype: you can only recurse on arguments
that are in a recursive position. I don't know how this is enforced in Coq, but here's how I would do it in Agda. First, you need to know for a given constructor which of its arguments are recursive and which ones are not, by looking at the type of the constructor. Then, when you do free variable analysis (in Agda.TypeChecking.Free.Lazy), you only mark variables as strongly rigid if they occur in a *recursive* argument of a constructor. This should be enough to rule out your example (since the argument of c isn't recursive), and I think would also solve the problem in general.<br><br></div>I'm tempted to try to implement this myself, but I probably won't do it until next week. So if you want to try it, go ahead.<br><br></div>-- Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Mar 9, 2017 at 3:35 PM, Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Yes, that's the point. Coq has to be more careful about the structural ordering since it supports impredicativity. (The example is taken from Coquand 1992, Pattern matching with dependent types, where Thierry already points out the problem.)<br>
<br>
Agda is build on the assumption of predicativity, thus<br>
<br>
c f > f args<br>
<br>
is ok with any constructor c, be it recursive or not.<br>
<br>
When you leave the safe ground of predicativity via --type-in-type, things might go wrong in an unexpected way.<br>
<br>
My long term-plan is to replace the structural termination check by type-based termination, which does not exhibit the pathological behavior exploited here. Thus, I am not so pressed to get rid of it.<br>
<br>
However, if someone can point me to the analysis Coq does on its data types for the sake of structural recursion, it may be worthwile to think how to integrate this into Agda.<br>
<br>
Best,<br>
Andreas<span class=""><br>
<br>
On 09.03.2017 05:52, Matthieu Sozeau wrote:<br>
</span><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">
Indeed in Coq we statically compute the possible recursive calls at the<br>
definition of the inductive type, independently of its use. In this case<br>
Agda is "fooled" because it thinks that [f] is a valid subterm (of type<br>
[D]) of [x : D], while Coq simply doesn't categorize [f] as a subterm<br>
when checking the guardedness/structural recursion criterion.<br>
<br>
On Thu, Mar 9, 2017 at 11:37 AM Michael Shulman <<a href="mailto:shulman@sandiego.edu" target="_blank">shulman@sandiego.edu</a><br></span><span class="">
<mailto:<a href="mailto:shulman@sandiego.edu" target="_blank">shulman@sandiego.edu</a>>> wrote:<br>
<br>
Pardon my ignorance, but I don't understand why anyone would accept<br>
the definition of "empty". The datatype D is not recursive; it's<br>
basically of the form<br>
<br>
data D : Set where<br>
c : X -> D<br>
<br>
for some fixed type X, which just happens to be large in this case.<br>
So its induction principle says that we get a map D -> Y whenever we<br>
have a map X -> Y. What justifies any sort of recursive call?<br>
<br>
<br>
On Wed, Mar 8, 2017 at 2:59 PM, Stefan Monnier<br></span><div><div class="h5">
<<a href="mailto:monnier@iro.umontreal.ca" target="_blank">monnier@iro.umontreal.ca</a> <mailto:<a href="mailto:monnier@iro.umontreal.ca" target="_blank">monnier@iro.umontreal.<wbr>ca</a>>> wrote:<br>
<br>
> data D : Set where<br>
> c : (f : (A : Set) → A → A) → D<br>
> -- Structural recursion with f args < c f is no longer valid.<br>
> -- We should not be able to demonstrated that D is empty.<br>
<br>
Coq lets us define this datatype (in Prop).<br>
<br>
> empty : D → ⊥<br>
> empty (c f) = empty (f D (c f))<br>
<br>
But rejects this definition:<br>
<br>
Error:<br>
Recursive definition of empty is ill-formed.<br>
In environment<br>
empty : D -> False<br>
x : D<br>
f : forall A : Prop, A -> A<br>
Recursive call to empty has principal argument equal to<br>
"f D (c f)" instead of a subterm of "x".<br>
Recursive definition is:<br>
"fun x : D => match x with<br>
| c f => empty (f D (c f))<br>
end".<br>
<br>
Not sure exactly what is the rule they use to decide whether a<br>
recursive<br>
call is considered as valid structural recursion. I suspect it<br>
depends<br>
on the notion of a "large inductive type" or something along<br>
these lines.<br>
<br>
<br>
Stefan<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br></div></div>
<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><wbr>><span class=""><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br></span>
<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><wbr>><span class=""><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br>
<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br>
</span></blockquote>
<br><span class="im HOEnZb">
<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://www.cse.chalmers.se/~abela/" rel="noreferrer" target="_blank">http://www.cse.chalmers.se/~ab<wbr>ela/</a><br></span><div class="HOEnZb"><div class="h5">
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>