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

Changes from 1 commit
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
Prev Previous commit
Next Next commit
Properly record the usage of GADT bounds
  • Loading branch information
@Linyxus
Linyxus committed Aug 8, 2021
commit 23f2d7591e9c930b6e645bf99522f2ced7ef834c
20 changes: 11 additions & 9 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 @@ -1167,14 +1167,16 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
else
fallback(tycon2bounds.lo)

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

tycon2 match {
case param2: TypeParamRef =>
Expand All @@ -1183,7 +1185,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
compareLower(bounds(param2), tyconIsTypeRef = false)
case tycon2: TypeRef =>
isMatchingApply(tp1) ||
compareTyConGadtBounds ||
byGadtBounds ||
defn.isCompiletimeAppliedType(tycon2.symbol) && compareCompiletimeAppliedType(tp2, tp1, fromBelow = true) || {
tycon2.info match {
case info2: TypeBounds =>
Expand Down