Skip to content

Intersection based gadts #6398

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
abgruszecki merged 9 commits into from
Jun 6, 2019
Merged

Intersection based gadts #6398

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
d25f03c
Rework how GADT constraints are inferred
abgruszecki May 22, 2019
54047ba
Add type-member-based GADT test suite
abgruszecki May 22, 2019
32c4280
Do not rely on subtyping to infer constraints for object patterns
abgruszecki May 22, 2019
483285f
Take HKT injectivity into account when inferring GADT constraints
abgruszecki May 22, 2019
609ee7b
Fix bias in ConstraintHandling#subsumes
abgruszecki May 23, 2019
a85cce4
Remove now untypeable exhaustivity test
abgruszecki May 22, 2019
3902ed2
Improve comments around constrainPatternType
abgruszecki May 23, 2019
7830069
Refactor Mode.GADTFlexible and TypeComparer.frozenGadt
abgruszecki Jun 6, 2019
01096ff
Document ConstraintHandling#subsumes
abgruszecki Jun 6, 2019
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
Improve comments around constrainPatternType
  • Loading branch information
@abgruszecki
abgruszecki committed Jun 5, 2019
commit 3902ed26b53595f6eb03fb77ef9b3268a08089a3
4 changes: 3 additions & 1 deletion compiler/src/dotty/tools/dotc/core/PatternTypeConstrainer.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,9 @@ trait PatternTypeConstrainer { self: TypeComparer =>
/** Derive type and GADT constraints that necessarily follow from a pattern with the given type matching
* a scrutinee of the given type.
*
* We have the following situation in case of a (dynamic) pattern match:
* This function breaks down scrutinee and pattern types into subcomponents between which there must be
* a subtyping relationship, and derives constraints from those relationships. We have the following situation
* in case of a (dynamic) pattern match:
*
* StaticScrutineeType PatternType
* \ /
Expand Down
6 changes: 3 additions & 3 deletions compiler/src/dotty/tools/dotc/typer/Applications.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1095,9 +1095,9 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
fullyDefinedType(unapplyArgType, "pattern selector", tree.span)
selType.dropAnnot(defn.UncheckedAnnot) // need to drop @unchecked. Just because the selector is @unchecked, the pattern isn't.
} else {
// note that we simply ignore whether constraining actually succeeded or not
// in theory, constraining should only fail if the pattern cannot possibly match
// however, during exhaustivity checks, we perform a strictly better check
// We ignore whether constraining the pattern succeeded.
// Constraining only fails if the pattern cannot possibly match,
// but useless pattern checks detect more such cases, so we simply rely on them instead.
ctx.addMode(Mode.GADTflexible).typeComparer.constrainPatternType(unapplyArgType, selType)
val patternBound = maximizeType(unapplyArgType, tree.span, fromScala2x)
if (patternBound.nonEmpty) unapplyFn = addBinders(unapplyFn, patternBound)
Expand Down