-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fix match type instantiation when not approximating
When not approximating parameters, keep the constraint entries in a Range, so it can propagate through instantiateParams's ApproximatingTypeMap.
- Loading branch information
Showing
19 changed files
with
129 additions
and
54 deletions.
There are no files selected for viewing
This file contains 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
This file contains 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
This file contains 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
This file contains 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
This file contains 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
This file contains 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
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file contains 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
This file contains 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
This file contains 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
This file contains 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
This file contains 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
This file contains 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
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,2 @@ | ||
def toList: List[Int] = | ||
(1, 1).toList |
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,21 @@ | ||
sealed trait Nat | ||
final case class Zero() extends Nat | ||
final case class Succ[+N <: Nat]() extends Nat | ||
|
||
final case class Neg[+N <: Succ[Nat]]() | ||
|
||
type Sum[X, Y] = Y match | ||
case Zero => X | ||
case Succ[y] => Sum[Succ[X], y] | ||
|
||
type IntSum[A, B] = B match | ||
case Neg[b] => IntSumNeg[A, b] | ||
|
||
type IntSumNeg[A, B] = A match | ||
case Neg[a] => Neg[Sum[a, B]] | ||
|
||
type One = Succ[Zero] | ||
type Two = Succ[One] | ||
|
||
class Test: | ||
def test() = summon[IntSum[Neg[One], Neg[One]] =:= Neg[Two]] |
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,19 @@ | ||
sealed trait Nat | ||
final case class Zero() extends Nat | ||
final case class Succ[+N <: Nat]() extends Nat | ||
|
||
final case class Neg[+N <: Succ[Nat]]() | ||
|
||
type Sum[X, Y] = Y match | ||
case Zero => X | ||
case Succ[y] => Sum[Succ[X], y] | ||
|
||
type IntSum[A, B] = B match | ||
case Neg[b] => A match | ||
case Neg[a] => Neg[Sum[a, b]] | ||
|
||
type One = Succ[Zero] | ||
type Two = Succ[One] | ||
|
||
class Test: | ||
def test() = summon[IntSum[Neg[One], Neg[One]] =:= Neg[Two]] |
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,27 @@ | ||
@main def main(): Unit = | ||
println(summon[Sum[Minus[Succ[Zero]], Minus[Succ[Zero]]] =:= Minus[Succ[Succ[Zero]]]]) | ||
|
||
sealed trait IntT | ||
sealed trait NatT extends IntT | ||
final case class Zero() extends NatT | ||
final case class Succ[+N <: NatT](n: N) extends NatT | ||
final case class Minus[+N <: Succ[NatT]](n: N) extends IntT | ||
|
||
type NatSum[X <: NatT, Y <: NatT] <: NatT = Y match | ||
case Zero => X | ||
case Succ[y] => NatSum[Succ[X], y] | ||
|
||
type NatDif[X <: NatT, Y <: NatT] <: IntT = Y match | ||
case Zero => X | ||
case Succ[y] => X match | ||
case Zero => Minus[Y] | ||
case Succ[x] => NatDif[x, y] | ||
|
||
type Sum[X <: IntT, Y <: IntT] <: IntT = Y match | ||
case Zero => X | ||
case Minus[y] => X match | ||
case Minus[x] => Minus[NatSum[x, y]] | ||
case _ => NatDif[X, y] | ||
case _ => X match | ||
case Minus[x] => NatDif[Y, x] | ||
case _ => NatSum[X, Y] |
This file contains 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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
type Ext[S <: Seq[_]] = S match { | ||
case Seq[t] => t | ||
} | ||
|
||
def test = implicitly[Ext[Seq[Int]] =:= Int] |