adapt to submodule upgrade

upgrade submodule

In CI, Java upgrade to 11~17, Scala upgrade to 2.13.12

upgrade submodule & adapt

upgrade dependencies

improve scalafix

add:

ExplicitResultTypes {
//  rewriteStructuralTypesToNamedSubclass = false
  skipSimpleDefinitions = false

  onlyImplicits = true
}

but is broken

adapt

upgrade submodules

StaticTuples renamed to Bone

Proto renamed to Backbone

adapt to dependency change

.github/workflows/main-splain.yml

@@ -12,7 +12,7 @@ jobs:
       max-parallel: 2
       fail-fast: false
       matrix:
-        javaVersion: ["1.8", "17"]
+        javaVersion: ["11", "17"]
         scalaVersion: ["2.13.10"]
 
     steps:

.github/workflows/main.yml

@@ -12,8 +12,8 @@ jobs:
       max-parallel: 2
       fail-fast: false
       matrix:
-        javaVersion: ["1.8", "17"]
-        scalaVersion: ["2.13.10"]
+        javaVersion: ["11", "17"]
+        scalaVersion: ["2.13.12"]
 
     steps:
       - uses: actions/checkout@v2

.scalafix.conf

@@ -7,19 +7,21 @@ rules = [
   ProcedureSyntax
   RemoveUnused
   LeakingImplicitClassVal
-//  ExplicitResultTypes
+  ExplicitResultTypes
 ]
 
 RemoveUnused {
   imports = true
   privates = true
-  locals = true
-  // the following 2 are not compatible with scala 2.11
+  locals = false
+  // "locals" is incompatible with `shouldNotCompile`
   patternvars = true
   params = true
 }
 
-//ExplicitResultTypes {
-//  rewriteStructuralTypesToNamedSubclass = false
-//  skipSimpleDefinitions = false
-//}
+ExplicitResultTypes {
+  rewriteStructuralTypesToNamedSubclass = false
+  skipSimpleDefinitions = false
+
+  onlyImplicits = true
+}

core/build.gradle.kts

@@ -2,6 +2,6 @@ val vs: Versions = versions()
 
 dependencies {
 
-    api(project(":macro"))
-    testFixturesApi(testFixtures(project(":macro")))
+    api(project(":macro2"))
+    testFixturesApi(testFixtures(project(":macro2")))
 }

core/src/main/scala/shapesafe/core/AdHocPoly1.scala

@@ -1,117 +1,10 @@
 package shapesafe.core
 
-import shapeless.Poly1
-
-import scala.annotation.implicitNotFound
-
-// TODO: compiler bug?
-//  https://stackoverflow.com/questions/65944627/in-scala-how-could-a-covariant-type-parameter-be-an-upper-bound-of-an-abstract
+import ai.acyclic.prover.commons.function.PreDef
 
 /**
   * Different from dotty's polymorphic function kind, which only supports parametric polymorphic
   */
-trait AdHocPoly1[IUB, OUB] {
-
-  final type _IUB = IUB
-  final type _OUB = OUB
-
-  trait Case[-I <: IUB] {
-
-    type Out <: OUB
-
-    def apply(v: I): Out
-  }
-
-  class =>>[
-      -I <: IUB,
-      O <: OUB
-  ](val toOut: I => O)
-      extends Case[I] {
-
-    final type Out = O
-
-    override def apply(v: I): O = toOut(v)
-  }
-
-  object Auxs {
-
-    final type =>>[
-        I <: IUB,
-        O <: OUB
-    ] = Case[I] {
-      type Out = O
-    }
-
-    final type =>>:<[
-        I <: IUB,
-        O <: OUB
-    ] = Case[I] {
-      type Out <: O
-    }
-  }
-
-  object AuxsWithNotFoundMsg {
-
-    @implicitNotFound(
-      "${I}\t =/=>> \t??? <: ${OUB}"
-    )
-    final type Case[I <: IUB] = AdHocPoly1.this.Case[I]
-
-    @implicitNotFound(
-      "${I}\t =/=>> \t${O}"
-    )
-    final type =>>[
-        I <: IUB,
-        O <: OUB
-    ] = Case[I] {
-      type Out = O
-    }
-
-    // only use as an implicit type parameter if Output type doesn't depends on O!
-    @implicitNotFound(
-      "${I}\t =/=>> \t??? <: ${O}"
-    )
-    final type =>>:<[
-        I <: IUB,
-        O <: OUB
-    ] = Case[I] {
-      type Out <: O
-    }
-  }
-
-  def forAll[I <: IUB] = new ForAll[I]() // same as `at` in Poly1?
-
-  protected class ForAll[I <: IUB]() {
-
-    def =>>[O <: OUB](fn: I => O): I =>> O = new (I =>> O)(fn)
-  }
-
-  def summon[I <: IUB](
-      implicit
-      _case: Case[I]
-  ): _case.type = _case
-
-  def summonFor[I <: IUB](v: I)(
-      implicit
-      _case: Case[I]
-  ): _case.type = _case
-
-  def apply[I <: IUB](v: I)(
-      implicit
-      _case: Case[I]
-  ): _case.Out = _case.apply(v)
-
-  object AsShapelessPoly1 extends Poly1 {
-
-    val outer: AdHocPoly1[IUB, OUB] = AdHocPoly1.this
-
-    implicit def delegate[I <: IUB, O <: OUB](
-        implicit
-        from: I =>> O
-    ): Case.Aux[I, O] = at[I].apply { ii =>
-      from.apply(ii)
-    }
-  }
-}
+trait AdHocPoly1 extends PreDef.Poly {}
 
 object AdHocPoly1 {}

core/src/main/scala/shapesafe/core/arity/ConstArity.scala

@@ -1,12 +1,12 @@
 package shapesafe.core.arity
 
-import ai.acyclic.prover.commons.Same
+import ai.acyclic.prover.commons.same.Same
 import shapeless.Witness
 import shapesafe.core.XInt
 import shapesafe.core.arity.Utils.Op
 import singleton.ops.{==, Require}
 
-trait ConstArity[S] extends LeafArity with Same.ByEquality.Facade {
+trait ConstArity[S] extends LeafArity with Same.ByEquality.IWrapper {
 
   type SS = S
   def singleton: S

core/src/main/scala/shapesafe/core/arity/binary/Op2_Imp0.scala

@@ -1,5 +1,6 @@
 package shapesafe.core.arity.binary
 
+import shapesafe.core.arity.ProveArity.|-
 import shapesafe.core.arity._
 
 trait Op2_Imp0 extends Op2Like_Imp0 {
@@ -11,7 +12,7 @@ trait Op2_Imp0 extends Op2Like_Imp0 {
   ](
       implicit
       domain: UncheckedDomain[A1, A2]
-  ) = {
+  ): OP#On[A1, A2] |- Unchecked = {
     domain.forOp2[OP]
   }
 }

core/src/main/scala/shapesafe/core/axis/Axis.scala

@@ -1,6 +1,6 @@
 package shapesafe.core.axis
 
-import ai.acyclic.prover.commons.Same
+import ai.acyclic.prover.commons.same.Same
 import shapeless.Witness
 import shapeless.labelled.FieldType
 import shapesafe.core.arity.{Arity, ArityType, ConstArity}
@@ -9,7 +9,7 @@ import shapesafe.core.{XInt, XString}
 
 import scala.language.implicitConversions
 
-trait Axis extends AxisLike with Same.ByEquality.Facade with CanPeek {
+trait Axis extends AxisLike with Same.ByEquality.IWrapper with CanPeek {
   // TODO:; can be a subclass of shapeless KeyTag
 
   final type Field = FieldType[Name, _ArityType]

core/src/main/scala/shapesafe/core/axis/NewNameAppender.scala

@@ -19,7 +19,7 @@ trait NewNameAppender extends RecordUpdater {
       isNew: NotContainsConstraint[OLDNS, N]
   ): (OLD, N ->> A1) =>> ((N ->> A1) :: OLD) = {
 
-    forAll[(OLD, N ->> A1)].=>> {
+    at[(OLD, N ->> A1)].defining {
       case (old, field) =>
         field :: old
     }

core/src/main/scala/shapesafe/core/axis/OldNameUpdaters.scala

@@ -27,7 +27,7 @@ class OldNameUpdaters[OP <: Op2Like](val op: OP) {
         lemma: op.On[A1, A2] |- O
     ): (OLD, N ->> A2) =>> ((N ->> O) :: OLD) = {
 
-      forAll[(OLD, N ->> A2)].=>> {
+      at[(OLD, N ->> A2)].defining {
 
         case (old, field) =>
           import shapeless.record._
@@ -64,7 +64,7 @@ class OldNameUpdaters[OP <: Op2Like](val op: OP) {
         modifier: Modifier[OLD, N, A1, O]
     ): (OLD, N ->> A2) =>> modifier.Out = {
 
-      forAll[(OLD, N ->> A2)].=>> {
+      at[(OLD, N ->> A2)].defining {
 
         case (old, field) =>
           val a2 = field: A2

core/src/main/scala/shapesafe/core/axis/RecordUpdater.scala

@@ -1,6 +1,5 @@
 package shapesafe.core.axis
 
 import shapesafe.core.AdHocPoly1
-import shapeless.HList
 
-trait RecordUpdater extends AdHocPoly1[(HList, Axis.UB_->>), HList] {}
+trait RecordUpdater extends AdHocPoly1 {}

core/src/main/scala/shapesafe/core/debugging/ExpressionType.scala

@@ -1,7 +1,7 @@
 package shapesafe.core.debugging
 
 import ai.acyclic.prover.commons.graph.local.Local
-import ai.acyclic.prover.commons.meta2.ProductDiscovery
+import ai.acyclic.prover.commons.meta.ProductDiscovery
 
 trait ExpressionType extends CanPeek {}
 

core/src/main/scala/shapesafe/core/debugging/ProofWithReasoning.scala

@@ -12,10 +12,10 @@ trait ProofWithReasoning extends ProofSystem with Reporters {
     type Goal <: CanPeek
 
     object Peek extends PeekReporter[CanPeek, Goal]
-    type Peek[I <: CanPeek] = Peek.Case[I]
+    type Peek[I <: CanPeek] = Peek.CaseFrom[I]
 
     object Interrupt extends InterruptReporter[CanPeek, Goal]
-    type Interrupt[I <: CanPeek] = Interrupt.Case[I]
+    type Interrupt[I <: CanPeek] = Interrupt.CaseFrom[I]
 
     trait ReasoningMixin {
       self: Proof[_, _] =>
@@ -27,7 +27,7 @@ trait ProofWithReasoning extends ProofSystem with Reporters {
 
       implicit def reason[I <: CanPeek, P <: Consequent](
           implicit
-          reporter: Peek.Case[I],
+          reporter: Peek.CaseFrom[I],
           prove: Proof[I, P]
       ): Proof[I, P] with ReasoningMixin = {
 

core/src/main/scala/shapesafe/core/debugging/Refutes.scala

@@ -10,18 +10,18 @@ trait Refutes {
 
   type WHEN_PROVING
 
-  type Refute0[SELF <: CanRefute, O] = Refute0.Auxs.=>>[SELF, O]
+  type Refute0[SELF <: CanRefute, O] = Refute0.=>>[SELF, O]
 
-  object Refute0 extends AdHocPoly1[CanRefute, Any] {
+  object Refute0 extends AdHocPoly1 {
 
-    implicit def get[I <: _IUB, V <: String](
+    implicit def get[I <: CanRefute, V <: String](
         implicit
         expr2Str: PeekCTAux[I#Notation, V]
     ): I =>> (
       I#RefuteTxt +
         WHEN_PROVING +
         V
-    ) = forAll[I].=>> { _ =>
+    ) = at[I].defining { _ =>
       null
     }
   }