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
X and (especially)
Y are quite large expressions.
Scott Morrison (Jun 22 2018 at 09:29):
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