Restate type alias raises errors

[sankalpgambhir]

A comment here mentions that the type alias is equivalent, but there seems to be some weird casting happening in the background.

lisa/lisa-utils/src/main/scala/lisa/utils/tactics/SimpleDeducedSteps.scala

Line 26 in 657acdd

def apply(using proof: Library#Proof)(premise: proof.ProofStep | proof.OutsideFact | Int)(bot: Sequent): proof.ProofTacticJudgement =

Consider the following:

val testThm = makeTHM("'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('x))") {
    ...
}

val test1 = makeTHM("'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('x))") {
    have("'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('x))") by Rewrite(thm"testThm")
}

val test2 = makeTHM("'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('x))") {
    have("'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('x))") by Restate(thm"testThm")
}

test1 compiles and checks through the kernel, while test2 raises a type error:

[error] -- [E134] Type Error: /home/sankalp/projects/lisa/lisa-working2/lisa-examples/src/main/scala/Exercise.scala:31:57 
[error] 31 |    have("'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('x))") by Restate(thm"testThm")
[error]    |                                                         ^^^^^^^
[error]    |None of the overloaded alternatives of method apply in object Restate with types
[error]    | (using proof: lisa.utils.Library#Proof)
[error]    |  (premise: proof.ProofStep | proof.OutsideFact | Int)
[error]    |    (bot: lisa.kernel.proof.SequentCalculus.Sequent): proof.ProofTacticJudgement
[error]    | (using proof: lisa.utils.Library#Proof)
[error]    |  (bot: lisa.kernel.proof.SequentCalculus.Sequent): proof.ProofTacticJudgement
[error]    |match arguments (lisa.settheory.SetTheoryLibrary.theory.Theorem)
[error] one error found

For reference, here is the type signature of Rewrite:

lisa/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala

Line 36 in 657acdd

def apply(using proof: Library#Proof)(premise: proof.Fact)(bot: Sequent): proof.ProofTacticJudgement = {

[SimonGuilloud]

That's a scala 3 bug. Not much to do about it except finding a work arround.

[sankalpgambhir]

Despite the closing of #120, this one continues to struggle (just tried).