refine_struct doesn't work with module

Stream: general

[Scott Morrison]

It seems refine_struct doesn't work with module.

import algebra.module.basic

example {α β : Type} [ring α] [add_comm_group β] : module α β :=
begin
  refine_struct { .. },
end

(says too many constructors).

[Scott Morrison]

@Simon Hudon, any ideas?

[Simon Hudon]

Let's see

[Simon Hudon]

Ok, I have a fix. It's because module is not a structure itself so I need to use whnf before getting the structure name

[Simon Hudon]

#3828