a strange type ascription error

Stream: general

[Scott Morrison]

I am getting an error of the form

invalid type ascription, term has type
  @eq X a b
but is expected to have type
  @eq Y a b

where here X and (especially) Y are quite large expressions.

[Scott Morrison]

But a and b are just names of hypotheses. Any advice on dealing with this sort of thing?

[Scott Morrison]

It seems like merely from the fact that the two terms separately typecheck I should have a proof that X = Y...

[Scott Morrison]

Curiously here, even though the goal prints as a = b, writing show a = b results in show tactic failed.

[Scott Morrison]

... immediate problem solved, (remove a few unnecessary @[reducible] attributes), although I don't really understand what was going wrong.

[Reid Barton]

I have seen a tactic produce a goal which was not well-typed before, and it was very confusing. Sounds like the same sort of issue?

[Reid Barton]

In my case the offending tactic was induction using quotient.ind; from your resolution, it sounds unrelated

[Reid Barton]

I guess the main point is that "the goal in tactic mode is well-typed" is not a 100% iron-clad guarantee, although it surely indicates a bug somewhere if it is violated.