search

epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

Remove redundant `given Library` leading to compilation error under Scala 3.6 #224

Closed WojciechMazur closed 2 months ago

WojciechMazur commented 2 months ago

This change fixes compilation of project when using Scala 3.6 or later due to change in givens prioritization. The issue was found by the Scala 3 Open Community Build.

Related change in the compiler https://github.com/scala/scala3/pull/19300 New rule stats that:

Instead of requiring an argument to be most specific, we now require it to be most general while still conforming to the formal parameter.

Since Scala 3.5.0 (or under -source:3.5) compiler yields warnings: 

[warn] -- Warning: /Users/wmazur/projects/community-build3/repo/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Untyped.scala:915:99 
[warn] 915 |          have((hIsTheHeightFunction, constructorVarsInDomain(c, term)) |- in(c.term, term)) by Cut(termsHaveHeightForward, lastStep)
[warn]     |                                                                                                   ^
[warn]     |Given search preference for lisa.prooflib.Library between alternatives (lisa.maths.settheory.SetTheory.given_Library :
[warn]     |  => (lisa.SetTheoryLibrary.given_Library² : lisa.prooflib.Library)) and (lisa.maths.settheory.SetTheory.library :
[warn]     |  => (lisa.SetTheoryLibrary.library² : lisa.SetTheoryLibrary.type)) will change
[warn]     |Current choice           : the second alternative
[warn]     |New choice from Scala 3.6: the first alternative
[warn]     |
[warn]     |where:    given_Library  is a given instance in trait Main
[warn]     |          given_Library² is a given instance in trait ProofsHelpers
[warn]     |          library        is a given instance in trait Main
[warn]     |          library²       is a given instance in class Library

The difference in the resolution between 

trait ProofsHelpers:
  library: Library =>
    given Library = library // used under new resolution, more general

and 

abstract class Library extends WithTheorems, ProofsHelpers:
  given library: this.type = this // used before 3.6, more specifc

makes a big difference in function using path-dependent types, eg def foo()(using lib: Library, proof: lib.Proof). When resolved as given Library we're having some Library instance, while Library.this.type is requiring exact dependant value.

The issue can be solved by removing redundant given Library

Fixing this issue would allow Open CB to test this project against the newer version of the compiler.