## Stream: general

### Topic: a strange type ascription error

#### Scott Morrison (Jun 22 2018 at 09:28):

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 (Jun 22 2018 at 09:29):

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

#### Scott Morrison (Jun 22 2018 at 09:30):

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

#### Scott Morrison (Jun 22 2018 at 09:33):

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

#### Scott Morrison (Jun 22 2018 at 10:00):

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

#### Reid Barton (Jun 22 2018 at 14:16):

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 (Jun 22 2018 at 14:25):

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

#### Reid Barton (Jun 22 2018 at 14:26):

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.

Last updated: May 07 2021 at 00:30 UTC