Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 1 commit into from
Jul 22, 2024

Conversation

WojciechMazur
Copy link
Contributor

@WojciechMazur WojciechMazur commented Jul 18, 2024

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 scala/scala3#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.

Copy link
Member

@sankalpgambhir sankalpgambhir left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for checking and fixing this! Looks good.

@sankalpgambhir sankalpgambhir merged commit 70367a6 into epfl-lara:main Jul 22, 2024
1 check passed
@WojciechMazur WojciechMazur deleted the fix/3.6 branch July 22, 2024 09:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants