I think "would have sufficed" is a strange choice of words in this case. I do consider macros a lot stronger than "deriving", but I am not sure they are entirel

I think "would have sufficed" is a strange choice of words in this case. I do consider macros a lot stronger than "deriving", but I am not sure they are entirely appropriate in a language which is so much rooted in type theory as Haskell is. I think of "deriving" in Haskell as a form of automated theorem proving, and I think it would be beneficial to have better theorem prover integrated in the language (I think it is in languages like Coq). The reason why I think theorem prover would be more appropriate than macros is because with macros you, as a programmer, have to do the proof explicitly, and you're responsible for it being type correct. Whereas with a real theorem prover behind the scenes, this work is not needed. In general, I think it's still quite unclear how to well integrate macro system of Lisp power with type checked language. So risking "moving the goalpost", I am not really satisfied with your answer. Are there some uses cases for macros that do not involve theorem proving (i.e. having compiler build some function automatically based on type signature alone)?