Support for GADTs #195
Draft
Support for GADTs #195
Conversation
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
Hit some pp problems due to incorrect use of TypeBounds; need to rm TBs from typer output & use proper wilcards instead We now type patmat branches inside local polymorphic context; this causes regressions in type simplif and some tests to run out of recursion depth limit
TODO add support for raw type
|
Cool! Will try to take a look later. In the meantime, plz read this again and make sure all the changes are clean: https://github.com/hkust-taco/mlscript/blob/mlscript/CONTRIBUTING.md |
LPTK
reviewed
Mar 4, 2024
| @@ -1147,13 +1147,13 @@ abstract class NewParser(origin: Origin, tokens: Ls[Stroken -> Loc], newDefs: Bo | |||
| } | |||
| val lb = getTypeName("restricts") | |||
| val ub = getTypeName("extends") | |||
|
|
|||
| // TODO update `TypeParamInfo` to use lb and ub | |||
Comment on lines
244
to
251
| ts2.forall { | ||
| case sk: SkolemTag => ts1(sk) | ||
| case tt: TraitTag => ts1(tt) | ||
| case Extruded(pol, sk) => !pol || ts1.exists { // find ? <: bot | ||
| case Extruded(true, _) => true | ||
| case _ => false | ||
| } | ||
| } && rt1 <:< rt2 && |
There was a problem hiding this comment.
This thing looks very fishy. What is going on here? Why don't we use the normal set functions?
LPTK
reviewed
Mar 5, 2024
LPTK
reviewed
Mar 6, 2024
| val cache: MutMap[Level, MutMap[TypeVarOrRigidVar->Bool, TypeVarOrRigidVar]], | ||
| ) { | ||
| private var cycle: Int = 0 | ||
| // TODO maybe find a better way |
There was a problem hiding this comment.
Could you explain what this achieves and why it's needed?
…traint rewritings
Open
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Add support for GADTs
?in type argumentsaskeyword for upcast (same as:)GADT[1-6].mlsingadtdirectory, andAsOp.mlsSome TODOs (added by @LPTK):
local-gadt-wipafter we figure out the new errors??Xtypes into main branch before merging this PRThe PR has become way too big and it's difficult to keep track of what changes cause what results or regressions. Let's split it up and merge each of these things separately:
?in type arguments, useaskeyword for upcast (same as:)App[f, a]); and in this case don't try to refine these type arguments in the scrutinee.