Zulip Chat Archive

Stream: general

Topic: a strange type ascription error


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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