Support for GADTs #195
Support for GADTs #195
Conversation
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 |
| @@ -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 | |||
| 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?
| 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
|
Thanks again for the great work, @Meowcolm024! These changes will be useful for future reference, even though they are already obsolete (since we are moving to a new type checker implementation). So I will close this for now as it is not worth fixing the conflicts and cleaning up the history, similarly to #219 By the way, as I told you in person some time ago, you merged some commits on my WIP branch (the "W"-named commits) which were only temporary experimentation changes. These were not intended to be made part of your PR – or at least, not as is. |
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.