The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Jelle wrote:
> Hello,
>
> When running Coq with "-impredicative-set" I would have expected the
> following to work:
>
>   Record foo : Set := mkFoo { bar : Set }.
>   foo is defined
>   foo_ind is defined
>   foo_rec is defined
>
> But the projection is not defined:
>
>   Warning: bar cannot be defined because it is large and foo is not.
>
> Trying this manually gives:
>
>   Definition bar (x : foo) := match x with mkFoo b =>  b end.
>
>   Error: Incorrect elimination of "x" in the inductive type "foo":
>   the return type has sort "Type" while it should be "Prop" or "Set".
>
>   Elimination of an inductive object of sort Set is not allowed on a
>   predicate in sort Type because strong elimination on non-small
>   inductive types leads to paradoxes.
>
> What is going on here? -impredicative-set doesn't work with records?
> And what exactly is strong elimination?
>    

Strong elimination (usually called large elimination, actually) is a 
[match] whose result type doesn't have type [Set] or [Prop].  Less 
formally, it's a [match] returning a type.  A large inductive type 
definition has at least one constructor whose type contains a 
"polymorphic" [forall], quantifying over types.  Your [foo] is certainly 
one such type, since the type of [mkFoo] includes quantification over [Set].

To preserve consistency, large elimination on large inductive 
definitions in impredicative [Set] must be disallowed.  The details of 
this I am not familiar with.