I was reading this http://adam.chlipala.net/cpdt/html/Universes.html

And it gives me this example, which was supposed to be rejected by Coq but is accepted, is there any heuristics going on that I'm not aware of?

```
Inductive exp : Set -> Set :=
| Const : forall T : Set, T -> exp T
| Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2)
| Eq : forall T, exp T -> exp T -> exp bool.
```

Also he says *This definition is large in the sense that at least one of its constructors takes an argument whose type has type Type.* But I don't see what constructor takes a type here, I tried the example expecting to get the problematic constructor highlighted in the PG but no, it's just accepted

It is rejected for me on 8.15.1

Maybe I have a flag enabled that I'm not aware of

Can you do `Print exp.`

and show the output?

```
Inductive exp : Set -> Set :=
Const : forall T : Set, T -> exp T
| Pair : forall T1 T2 : Set, exp T1 -> exp T2 -> exp (T1 * T2)
| Eq : forall T : Set, exp T -> exp T -> exp bool.
Arguments exp _%type_scope
Arguments Const _%type_scope _
Arguments Pair (_ _)%type_scope _ _
Arguments Eq _%type_scope _ _
```

fails for me

Okay, I suspect you do have some flag enabled. I was hoping Coq had just replaced `-> Set`

with `-> Type`

(it does that for `Prop`

sometimes) but the output looks exactly the same as the definition so it can't be that.

@Daniel Hilst Selli this is large because `Const`

takes a `Set`

can you test this in a standalone file?

Okay, is something in my editor :

```
coqc /tmp/Foo.v
File "/tmp/Foo.v", line 1, characters 0-168:
Error: Large non-propositional inductive types must be in Type.
```

The 3 constructors are taking arguments in Type (or rather in `Set`

). For your definition to be accepted I guess Set is set to be impredicative in some way (for instance with the option `-impredicative-set`

) ?

you might be using some library that disables universe checking, _or_ some setting in `_CoqProject`

@Kenji Maillard no, this is too impredicative

impredicative strong sums break strong normalization

you can use `-type-in-type`

:-)

(or however that's called in Coq)

this is accepted with impredicative-set, but squashed

This work though:

```
Inductive exp : Prop -> Prop :=
Const : forall T : Prop, T -> exp T
| Pair : forall T1 T2 : Prop, exp T1 -> exp T2 -> exp (T1 /\ T2)
| Eq : forall T : Prop, exp T -> exp T -> exp True.
```

I spoke too quickly: the problem is with _injective_ constructors.

Okay, I was using PG for a long time in the same living emacs process I closed emacs, start it again, and open the file with the example and now it rejects on the editor too, so I suspect that there is some configuration getting persisted which I don't know why but at last I know how to work around it, thanks, guys!

So about the question, because in the Const `forall T : Set, T`

type is `Set`

and `exp`

type is `Set -> Set`

this is considered *large*, right?

Basically yes. Another large datatype, working but squashed with `-impredicative-set`

— here we can define it but can't extract the `T`

out of it:

```
Inductive exp : Set :=
| Const : forall T : Set, T -> exp.
(* | Const : forall T : Set, T -> exp T. *)
(* | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2)
| Eq : forall T, exp T -> exp T -> exp bool. *)
Definition f (e : exp) : Set.
Proof.
Fail destruct e.
```

Daniel Hilst Selli said:

So about the question, because in the Const

`forall T : Set, T`

type is`Set`

and`exp`

type is`Set -> Set`

this is consideredlarge, right?

there is no `forall T : Set, T`

, it's parenthesized as `forall T : Set, (T -> exp T)`

it's large because the argument of Const `T : Set`

is large ie because its type `Set`

is in `Type > Set`

Oh I was reading it as `(forall T : Set, T) -> exp`

So, is it correct to say that I cannot parameterize a `Set`

by another `Set`

?

no, you can do eg `Inductive prod (A B : Set) : Set := pair : A -> B -> prod A B.`

without problem

note here that A and B are parameters of the inductive (on the left of the `:`

) not just arguments to the constructor

Last updated: Jun 16 2024 at 03:41 UTC