Differing type parameters in mutually recursive types produce invalid Coq code

[MajaRet]

Description

Coq requires that types that depend on each other have syntactically identical type parameters. Since the compiler does not check that, mutually recursive data definitions with differing type parameters are compiled into an invalid Coq program.

Steps to Reproduce

Translate the following mutually recursive data types with the compiler.

data Foo a = FooCons (Bar a) | FooVal a
data Bar b = BarCons (Foo b) | BarVal b

Behavior

The compiler translates the data type as follows:

Inductive Bar (Shape : Type) (Pos : Shape -> Type) (b : Type) : Type
  := barCons : Free Shape Pos (Foo Shape Pos b) -> Bar Shape Pos b
  |  barVal : Free Shape Pos b -> Bar Shape Pos b
with Foo (Shape : Type) (Pos : Shape -> Type) (a : Type) : Type
  := fooCons : Free Shape Pos (Bar Shape Pos a) -> Foo Shape Pos a
  |  fooVal : Free Shape Pos a -> Foo Shape Pos a.

This Coq code is not valid; it produces the error Parameters should be syntactically the same for each inductive type.

On the other hand, the translation of

data Foo a = FooCons (Bar a) | FooVal a
data Bar a = BarCons (Foo a) | BarVal a

is valid in Coq because both Foo and Bar have the same parameters.

The same problem arises when Foo and Bar have a different number of parameters:

data Foo = FooCons (Bar Bool)
data Bar a = BarCons Foo | BarVal a

This definition also leads to invalid Coq code.

Expected Behavior

Compiled programs should always be valid Coq programs. The compiler should therefore try to avoid this error by renaming differing variables so they are the same.
In the case of a different number of type parameters, the compiler should either find a way to make them the same as well, or report an error.

Versions

• Git commit: 0583ff4
• ghc --version: 8.6.5
• cabal --version: 3.2.0.0
• coqc --version: 8.11.0
• OS: Ubuntu 19.10