to_additive gives error "can't transport XYZ to itself"

Stream: mathlib4

[Pieter Cuijpers]

I'm trying to define both a multiplicative and an additive version of Quantales using to_additive.
I think I used the definition of Monoid and AddMonoid as an example, but apparently I'm doing something different without knowing it.
I get the error "can't transport XYZ to itself".

Can anyone explain what's wrong?

import Mathlib.Order.CompleteLattice
import Mathlib.Algebra.Group.Defs
import Mathlib.Tactic.ToAdditive

class AddQuantale (α : Type*) extends AddSemigroup α, CompleteLattice α where

  /-- Addition is distributive over join in an additive quantale -/

  protected add_sSup_eq_iSup_add (x : α) (s : Set α) : x + sSup s = ⨆ y ∈ s, x + y

  /-- Addition is distributive over join in an additive quantale -/

  protected sSup_add_eq_iSup_add (s : Set α) (y : α) : sSup s + y = ⨆ x ∈ s, x + y


@[to_additive]

class Quantale (α : Type*) extends Semigroup α, CompleteLattice α where

  /-- Multiplication is distributive over join in a quantale -/

  protected mul_sSup_eq_iSup_mul (x : α) (s : Set α) : x * sSup s = ⨆ y ∈ s, x * y

  /-- Multiplication is distributive over join in a quantale -/

  protected sSup_mul_eq_iSup_mul (s : Set α) (y : α) : sSup s * y = ⨆ x ∈ s, x * y

[Yaël Dillies]

You should add a translation from AddQuantale to Quantale in docs#ToAdditive.nameDict

[Yaël Dillies]

eg add | "quantale"       => ["add", "Quantale"] between L.968 and L.969