Skip to content

Better utilizing GADT bounds for HKTs #13323

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.

Sign up for GitHub

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

Merged
merged 14 commits into from
Aug 31, 2021
Merged

Better utilizing GADT bounds for HKTs #13323

Show file tree
Hide file tree
Changes from 9 commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
65b171c
Approximate GADT lower bound for HKTs
Linyxus Aug 8, 2021
23f2d75
Properly record the usage of GADT bounds
Linyxus Aug 8, 2021
e4edcea
Fix the injectivity issue
Linyxus Aug 18, 2021
ab6aa68
Add pos testcase
Linyxus Aug 18, 2021
196033e
Add neg test
Linyxus Aug 18, 2021
d551238
Update pos test
Linyxus Aug 18, 2021
7cda5b5
Rename HKGadt state and use primitive boolean
Linyxus Aug 23, 2021
dfbe8d4
Fix touchHKGadt
Linyxus Aug 24, 2021
abb4155
Utilize frozenGadt instead of using a new state variable
Linyxus Aug 25, 2021
28c6381
Remove unused import
Linyxus Aug 25, 2021
2da3c58
Remove workaround
Linyxus Aug 26, 2021
0b323dc
Fix inFrozenGadtIf
Linyxus Aug 25, 2021
8b45a00
Also approximate with HKT's GADT higher bounds
Linyxus Aug 29, 2021
d1a04e2
Remove redundant braces
Linyxus Aug 30, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 14 additions & 0 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ import StdNames.nme
import TypeOps.refineUsingParent
import collection.mutable
import util.Stats
import scala.util.DynamicVariable
import config.Config
import config.Feature.migrateTo3
import config.Printers.{constr, subtyping, gadts, matchTypes, noPrinter}
Expand Down Expand Up @@ -1092,6 +1093,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
val tyconIsInjective =
(tycon1sym.isClass || tycon2sym.isClass)
&& (!touchedGADTs || gadtIsInstantiated)
&& !frozenGadt

inFrozenGadtIf(!tyconIsInjective) {
if tycon1sym == tycon2sym && tycon1sym.isAliasType then
Expand Down Expand Up @@ -1167,13 +1169,25 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
else
fallback(tycon2bounds.lo)

def byGadtBounds: Boolean =
{
tycon2 match
case tycon2: TypeRef =>
val tycon2sym = tycon2.symbol
tycon2sym.onGadtBounds { bounds2 =>
inFrozenGadt { compareLower(bounds2, tyconIsTypeRef = false) }
}
case _ => false
} && { GADTused = true; true }

tycon2 match {
case param2: TypeParamRef =>
isMatchingApply(tp1) ||
canConstrain(param2) && canInstantiate(param2) ||
compareLower(bounds(param2), tyconIsTypeRef = false)
case tycon2: TypeRef =>
isMatchingApply(tp1) ||
byGadtBounds ||
defn.isCompiletimeAppliedType(tycon2.symbol) && compareCompiletimeAppliedType(tp2, tp1, fromBelow = true) || {
tycon2.info match {
case info2: TypeBounds =>
Expand Down
8 changes: 8 additions & 0 deletions tests/neg/gadt-hkt-hi-bounds.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
type Const = [X] =>> Int

trait Expr[-F[_]]
case class ConstExpr() extends Expr[Const]

def foo[F[_], A](e: Expr[F]) = e match
case _: ConstExpr =>
val i: Int = ??? : F[A] // limitation // error
7 changes: 7 additions & 0 deletions tests/pos/gadt-hkt-bounds.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
type Const = [X] =>> Int

trait Expr[+F[_]]
case class ConstExpr() extends Expr[Const]

def foo[F[_], A](e: Expr[F]): F[A] = e match
case _: ConstExpr => 0