derive handlers

Stream: general

[Simon Hudon]

I'm writing a derive handler, and while testing it on my third example, I get the following error:

declaration contains macro with trust-level higher than the one allowed (possible solution: unfold macro, or increase trust-level)

But the term that my handler produces contains no macros that I can see (I'm using expr.fold to enumerate them). Has anyone seen this before?

[Simon Hudon]

Update: I checked a part of the derived term which produces perm_ac and ac_app

[Simon Hudon]

Update 2: I wrote a tactic expand_untrusted that takes care of those macros. It solves the problem. I'm surprised instance_derive_handler doesn't do that by default