DRAFT Scala 3: implement the compile-time refinement macros - #1453
Open
lgmyrek wants to merge 3 commits into
Open
DRAFT Scala 3: implement the compile-time refinement macros#1453lgmyrek wants to merge 3 commits into
lgmyrek wants to merge 3 commits into
Conversation
lgmyrek
marked this pull request as draft
July 15, 2026 15:31
Contributor
|
Tick the box to add this pull request to the merge queue (same as
|
Author
|
@fthomas RFC |
lgmyrek
marked this pull request as ready for review
July 24, 2026 11:53
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
DRAFT Scala 3: implement the compile-time refinement macros (via Hearth)
Summary
The Scala 3 build of refined-core has so far shipped without the compile-time
macro layer —
auto.autoRefineV/autoInfer,refineMV,RefType.refineM/applyRefM,and the compile-checked
RefinedTypeOps.applydidn't exist on Scala 3. This PRimplements them, porting the behavior of the Scala 2
scala-reflectmacros to Scala 3with Hearth
0.4.1— using itsExpr.semiEvalcompile-time evaluator + the
cross-quotesDSL rather than hand-writtenscala.quotedmacros.
All changes are confined to
scala-3.0+sources; Scala 2.12/2.13 are untouched.What's added
Public API — Scala 3 now matches Scala 2 apart from the
@@(shapeless tag) carrier:auto.autoRefineV,auto.autoInfer— implicit compile-time conversionsrefineMV[P](t)— package-levelRefType[F].refineM[P](t)RefType.applyRefM[FTP](t)RefinedTypeOps.apply—object PosInt extends RefinedTypeOps[PosInt, Int]; PosInt(5)Internals:
macros/Macros.scala,macros/RefinedMacro.scala— the Hearth-based macro impls(validate via
semiEval; emitRefined.unsafeApply/unsafeWrap/upcast)macros/RefinedTypeOpsM.scala,internal/RefineMPartiallyApplied.scala,internal/ApplyRefMPartiallyApplied.scala— the partially-applied buildersinternal/WitnessAs.scala—singletonWitnessAsroutes on whether the base typeBis a singleton (see difference Do not use Scala's collection hierarchy for collection predicates #5)
build.sbt— Hearth dependency +-Xpluginwiring for thecross-quotescompilerplugin (JVM-published, reused across platforms, pulled in
Provided)Tests: all 20
scala-3.0-specs ported toscala-3.0+, with a Scala 3illTypedshim(
test/ScalaVersionSpecific.scala) built onscala.compiletime.testing.typeCheckErrors.Validation
Full Scala 3 platform matrix, green on stable Hearth 0.4.1:
validateJVM30(clean + all modules)validateJS30validateNative30Scala 2.12 / 2.13
coreJVM/Test/compile: unchanged and green. This confirms thecross-quotes/semiEvalmacros run at compile time across JVM, JS, and Native.Differences from the Scala 2 implementation
Macro engine. Scala 2 uses
scala-reflectblackbox macros with literal matchers(
Literal(Constant(_)),BigDecimalMatcher, …). Scala 3 uses Hearth'ssemiEval,which reflectively evaluates the expression tree at compile time. This is strictly
more capable — it evaluates
List(1,2,3),BigInt("1"), method calls, etc. So afew values Scala 2 rejected as "not a compile-time constant" now succeed at
compile time (the ported
BigLiterals/RefineM"non-literal" cases had to switch togenuinely non-evaluable inputs to still fail).
No
@@(shapeless tag) carrier. NotagRefTypeon Scala 3, sorefineMT,refineMF, and the@@variants ofapplyRefM/RefinedTypeOpsdon't exist;refineMV/refineM/applyRefMtargetRefinedonly.Refinedis an opaque type (erases to its base type), unlike the Scala 2 valueclass:
Refined.unsafeApply(1).equals(1)istrue, there is no.copy, etc.(
RefinedSpec.equalsadjusted accordingly.)hypotheticalSyllogism(transitivity) is omitted from the Scala 3Inferencerules — see Concerns. Two-hop chains like
Last[P] ==> NonEmpty(viaExists[P])are therefore not derivable on Scala 3.
Equal[SomeObject.type](object-singleton predicates) works viaValueOfratherthan
constValueinWitnessAs.constValuerejects a non-literal singleton ("not aconstant type");
ValueOfaccepts both.singletonWitnessAsroutes on whether thebase
Bhas aValueOf: object singletons take theValueOfbranch (exercised onlyat runtime, via
isValid), while everything else stays onconstValue(whichsemiEvalreduces natively). KeepingValueOfoff the compile-time path is why astable Hearth release suffices.
Cosmetic: some
Inference.showstrings differ (e.g.greaterInferenceIntvsgreaterInference).Not a difference: the point-free/curried builder forms behave the same as Scala 2 —
refineMV(t),refineMV[P][T](t),refineV(t),RefType[Refined].refineM(t)all inferthe predicate
Pfrom the expected type (a case-class field, avalascription, amethod parameter). Only a fully-standalone
val x = refineMV(5)(no expected type) needsan explicit
refineMV[P](5)— exactly as on Scala 2. The ported specs mirror this (barewhere the original was bare, explicit only where there is no expected type, e.g. inside
illTyped("…")snippets).Concerns / open items (please review)
🟠
hypotheticalSyllogismremoval weakens inference for all Scala 3 users, notjust tests. Its intermediate
Boccurs only in the premises, so resolving a goalthrough it spawns an ambiguous free-RHS subgoal
A ==> ?B(unifying withminimalTautology,disjunctionIntroduction{L,R}, …) that Scala 3's implicit searchreports as an ambiguity aborting the whole search — including otherwise-derivable goals
such as
Size[Interval.Closed[1,n]] ==> NonEmpty. Dropping it keeps the commonsingle-step and conjunction-elimination inferences working, at the cost of transitive
two-hop chains. Priority-tweaking was tried and is whack-a-mole; a proper fix likely
needs goal-directed resolution. (Whether Scala 3.7's given-prioritization change helps
is unclear — likely not, since the root cause is an under-constrained search, not a
priority tie.)
🟠 New third-party macro-engine dependency. Hearth becomes a (necessary) transitive
dependency of refined-core on Scala 3 — downstream users get it on their compile
classpath for macro expansion.
cross-quotesis a compiler plugin, wired as aProvideddep via-Xplugin(only needed to compile refined-core itself).🟡 Test diagnostics via the auto-conversion path. A real compile of
val x: Char Refined Equal['0'] = '1'correctly reportsPredicate failed: (1 == 0).But
scala.compiletime.testing.typeCheckErrors(the only in-process compile-check API,used by the test shim) suppresses a macro abort raised while trying an implicit
conversion and exposes only the resulting type mismatch. Net: the "Predicate failed"
message is asserted on direct
refineMV[…]calls (RefineMSpec), whileauto*conversion negatives assert only rejection (type mismatch). Real user-facing
diagnostics are unaffected/good.
🟡
-Xpluginjar resolution picks the first compile-classpath entry whose pathcontains
hearth-cross-quotes, andsys.errors if absent. Robust today; slightlyfragile against future artifacts with a matching name.
Intentionally not ported
@@-tag cases (refineMT,RefTypeSpecTag,Min/Max @@,autoRefineT,refineT/refineMTsyntax),OneOf(noValidateon Scala 3), the<:!<subtypingtest, and the transitive
Last ==> NonEmptyinference — each documented in-file with thereason.
Credits
All credits to @kubuszok for https://github.com/kubuszok/hearth and https://github.com/kubuszok/refined-compat, I am but a man with claude