Zulip Chat Archive

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: Aug 03 2023 at 10:10 UTC