Derive for inductive types with non-type parameters

[annenkov]

I've stumbled upon the following issue. Derive fails when I try to use it on something like this:

Record D := { Address : Type}.

Inductive msg {d : D} :=
  | send : Address d -> msg.

So, Derive Arbitrary for msg. gives

Error:
In environment
d : Type
mu6_ : Gen d
The term "d" has type "Type" while it is expected to have type "D".

[annenkov]

I think something like this could be generated (just by changing the case when d is a type):

  fun (d : D) (mu9_ : Show (Address d)) =>
    {|
      show := fun x : msg =>
                let
                  fix aux (x' : msg) : string :=
                  match x' with
                  | send p0 => "send " ++ smart_paren (show p0)
                  end in
                aux x |}.