Type synonym expansion binds type variables not correctly

[MarvinLira]

Description

The type synonym expansion, which is used when transforming mutually recursive types, does not work correctly.
In the example below it seems like the binding of the type variable a of Foo2 is used to replace occurrences of a in the type bound to b which is not correct.

Steps to Reproduce

Compile the following haskell types.

type Foo2 a b = Foo a b

data Foo a b = FCon (Bar a b)
data Bar a b = BCon (Foo2 b a)

Expected Behavior

The type synonym Foo2 b a gets expanded to Foo b a.

Inductive Bar (Shape : Type) (Pos : Shape -> Type) (a b : Type) : Type
  := bCon : Free Shape Pos (Foo Shape Pos b a) -> Bar Shape Pos a b
with Foo (Shape : Type) (Pos : Shape -> Type) (a b : Type) : Type
  := fCon : Free Shape Pos (Bar Shape Pos a b) -> Foo Shape Pos a b.

Actual Behavior

The type synonym Foo2 b a gets expanded to Foo b b.

Inductive Bar (Shape : Type) (Pos : Shape -> Type) (a b : Type) : Type
  := bCon : Free Shape Pos (Foo Shape Pos b b) -> Bar Shape Pos a b
with Foo (Shape : Type) (Pos : Shape -> Type) (a b : Type) : Type
  := fCon : Free Shape Pos (Bar Shape Pos a b) -> Foo Shape Pos a b.

Versions

• Git commit:
• ghc --version: 8.6.5
• cabal --version:3.2.0.0
• coqc --version: 4.05.0
• OS: ubuntu 18.04.5

Known Workarounds

Additional Information