Skip to content

Bad interaction between not guessing overloads and first_x_assum #1956

Open
Open
Bad interaction between not guessing overloads and first_x_assum#1956

Description

@dnezam
dnezam
opened on May 8, 2026

If one uses set_trace "guess overloads" 0, one can run into the odd situation where

first_x_assum(qspec_then`INR (LOG2 aa)`mp_tac) >>

fails with the error

Exception- HOL_ERR at Tactical.FIRST_ASSUM: raised

which hides the more relevant error

> ``INR (LOG2 aa)``;
Exception-
   HOL_ERR
     (at Preterm.type-analysis: in compiler-generated text:
          There was more than one resolution of overloaded constants) raised

I am not sure whether there is an elegant way around this.

Activity

  1. mn200 commented on May 17, 2026

    @mn200
    mn200
    on May 17, 2026
    Member

    I'm not sure what the right behaviour should be here. In particular, the quotation is parsed for every possible place where an assumption might be specialised because an assumption with !x. ... might cause the quotation to get type :foo, where the second assumption !y. ... will cause the quotation to get type :bar. This behaviour seems important to preserve, so we can't just parse the argument once before then trying to specialise all the assumptions.

    (Actually, I'm not sure if the quotation has to be repeatedly parsed: we should be able to check the stream of possible parses for compatibility with the desired types, but that's an orthogonal efficiency question.)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions