Coq Discourse users,
I have a question relating to a problem I have at the intersection of Universe Polymorphism and defining mutually inductive types. In particular definitions failing with the message “Parameters should be syntactically the same for each inductive type.” despite them being so.
I have a work-around for my particular problem but I wanted to make a post as either there is a bug in how coq handles things (very unlikely), or a deficiency in my understanding of how to instantiate mutually inductive types (very likely).
Context
Yesterday evening I was doing the ground work to internalize a reasonably simple type-theory in Coq. I was using Universe Polymorphism because whilst I don’t often need it, the times where I accidentally stumble into needing it without already having already having it on beforehand, which typically ends in a massive headache for me so I have decided to just start using the system from the beginning on new projects of mine.
I also was planning to extend my type theory to add dependent types so I decided to from the get-go define my terms & types together with a mutually inductive type of the form Inductive T@{e y z} {E:Type@{y}} {Y:Type@{y}} :Type@{z} for type INTERNAL_TYPE and INTERNAL_TERM with E being a type of atomic terms and likewise Y a type of atomic types.
(aside a mutually inductive definition for INTERNAL_TYPE and INTERNAL_TERM within said definition there are also a couple of other mutually defined types for other language features that I am playing about with, but they’re not relevant for the discussion)
That mutual definition goes through fine, however I get a problem when I try to use said types in another second mutually inductive definition (in my case for performing typing judgments). Even if I copy-paste parameters exactly I can only ever force the error Parameters should be syntactically the same for each inductive type.
My original problem was tied up heavily with the above problem domain, so I spent some time un-wrangling it, to give the example and problem below:
Question
Consider the following .v that is set-up to mirror how I found my problem initially. It contains many variations on setting up a mutually inductive types S1a, S1b from type T1.
Set Universe Polymorphism.
(*Part Ia*)
Inductive T1@{a c} (A:Type@{a}) :Type@{c} :=
(* defns go here*)
.
(*Failure I*)
Fail Inductive S1a@{a b c d} (A:Type@{a}) (B:Type@{b}) (P : B -> T1@{a c} A) : Type@{d} :=
with S1b (A:Type@{a}) (B:Type@{b}) (P : B -> T1@{a c} A) : Type@{d} :=.
Unset Universe Polymorphism.
(*Working without Uinverse Polymorphism*)
Inductive S1 (A:Type) (B:Type) (P : B -> T1 A) : Type :=
with S1b (A:Type) (B:Type) (P: B-> T1 A) : Type :=.
(*Part Ib*)
Set Universe Polymorphism.
(*Working without Explicit Uinverse Polymorphism*)
Inductive T1' (A:Type) :Type :=.
Inductive S1a' (A:Type) (B:Type) (P : B -> T1' A) : Type :=
with S1b' (A:Type) (B:Type) (P: B-> T1' A) : Type :=.
Print T1'.
Print S1a'.
Note Failure I in Part Ia. This is my initial way of Defining S1a S1b using explicit typing annotations. The message given is:
The command has indeed failed with message: Parameters should be syntactically the same for each inductive type.
However I guaranteed (by copy paste) that the parameters are syntactically the same. Immediately afterwards I try the same but with universe polymorphism turned off and it goes without fail. I surmise from this that there is something going wrong with parameter unification with universes turned on.
In Part Ib I try the same but without any explicit universe levels, leaving Coq to sort out the universe parameters. This works without fail and when you check with the Print command it also correctly verifies that universe parameters / variables are generalized and are how one would expect.
Through messing about with this problem I see that it is the parameter (P : B -> T1 A) that is causing issue as changing T1 A to any other (generic) type makes the failure go away in the case of explicitly setting universe variables. Interestingly it seems that allowing Coq to guess universe levels is an all-or-nothing affair as annotating universe levels for some types and not others does not allow Coq to do unification of levels, but instead triggers an Type-universe unbounded error.
Interestingly I found a workaround to allow me to work-around this issue whilst still explicitly set universe levels. For example:
Section S.
Universe a b c d.
Variable A:Type@{a}.
Variable B:Type@{b}.
Variable P: B -> (T2@{a b c} A B).
Variable T : (T2@{a b c} A B)-> Type@{d}.
Inductive S2a :Type@{d} :=
| intro : forall b (W: T (P b)) , S2a (* random constructor to make sure S2a depends on P*)
with S2b: Type@{d} :=.
End S.
Print S2a.
Print S2a_rect.
Note that by using a section to abstract out the type-parameters in the mutually inductive definition we cause Coq to stop complaining (as there are no type parameters to complain about). This, whilst a little unwieldy allows me to instantiate the types I originally wanted to.
With that example given, my questions are as follows:
-
why does the first failure
(*Failure I*)trigger when the parameters are identical? -
When defining Types, should I just stop explicitly annotating universe levels full stop? I’d rather not do so as setting the layout out the universe variables (to me at least) forms part of the interface for the type when using it in later theories. Thusly leaving that up to the machine looses come control on the layout that interface. One admits that such control can be recovered by defining new type families as wrappers over the original ones like as `Definition newT1’@{a b} := T1’@{a b}', and because no mutually inductive definitions are being made one will also not run into errors this way either. However this is a little unwieldy.
I recognize that my second question is mostly a matter of style, so if anyone has any general comment on how best to layout type definitions (in the mutually inductive and Universe Polymorphic setting) please give them!
Best Wishes