Anomaly when name mangling is enabled

[RalfJung]

When using Equations with name mangling enabled, I am seeing the following error:

Error:
Anomaly "Uncaught exception Failure("Could not generate a permutation")."
Please report at http://coq.inria.fr/bugs/.

This is deep inside a large development, I'll see if I can extract something self-contained.

[RalfJung]

Here is a self-contained example demonstrating the problem:

From Equations Require Import Equations.
From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8.
From Coq Require Import Permutation.
Export ListNotations.
From Coq.Program Require Export Basics Syntax.
From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
From Coq Require Import QArith Qcanon.

Set Mangle Names.

Declare Scope stdpp_scope.
Global Open Scope stdpp_scope.
Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1").
Notation "p .2" := (snd p) (at level 2, left associativity, format "p .2").

Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B.
Global Arguments mbind {_ _ _ _} _ !_ / : assert.
Global Instance: Params (@mbind) 4 := {}.
Global Hint Mode MBind ! : typeclass_instances.

Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope.
Notation "x ← y ; z" := (y ≫= (λ x : _, z))
  (at level 20, y at level 100, z at level 200, only parsing) : stdpp_scope.
Notation "' x ← y ; z" := (y ≫= (λ x : _, z))
  (at level 20, x pattern, y at level 100, z at level 200, only parsing) : stdpp_scope.

Global Instance option_bind: MBind option := λ A B f mx,
  match mx with Some x => f x | None => None end.

Definition block : Set := positive.
Definition loc : Set := block * Z.

Inductive type :=
  | Product (Ts: list type)
  .

Section def.
Context {A: Type}.
Equations visit_freeze_sensitive'
  (l: loc) (f: A → loc → nat → bool → option A)
  (a: A) (last cur_dist: nat) (T: type) : option (A * (nat * nat)) :=
  visit_freeze_sensitive' l f a last cur_dist (Product Ts) :=
      visit_LR a last cur_dist Ts
        where visit_LR (a: A) (last cur_dist: nat) (Ts: list type)
          : option (A * (nat * nat)) :=
          { visit_LR a last cur_dist [] := Some (a, (last, cur_dist)) ;
            visit_LR a last cur_dist (T' :: Ts') :=
              alc ← visit_freeze_sensitive' l f a last cur_dist T' ;
              visit_LR alc.1 alc.2.1 alc.2.2 Ts' }
  .
End def.