The Coq mailing list

[Robbert Krebbers <(e29315a54f%hidden_head%e29315a54f)mailinglists(e29315a54f%hidden_at%e29315a54f)robbertkrebbers.nl(e29315a54f%hidden_end%e29315a54f)>]

Hello Cédric and Stéphane,

thanks for the answers!

On 05/09/2012 04:19 PM, AUGER Cédric wrote:
> Do you not see why the strict positivity condition does not hold, or do
> you not see why the strict positivity condition is not fit to allow what
> you wrote and should be refined to allow it ?

Initially both. But after Stéphane's answer, I was clear that the 
definition in the reference manual disallows it due to the implicit 
argument of length.

> For the second point, things are less obvious, and I know there are
> cases where it could be allowed without breaking consistency.

Russell O’Connor's example at #coq

  Inductive val : Type := bad : ((fun X : Type =>  X -> X)  val) -> val

clearly showed me why functions in constructor arguments are unsafe in 
general.

However, Agda allows my definition! But apparently it is non-trivial to 
type check, see [1].

Robbert

[1] https://lists.chalmers.se/pipermail/agda/2012/003992.html