Correctly introduce new openness variables at the union rank

This commit is contained in:
Ayaz Hafiz 2023-04-20 16:56:39 -05:00
parent 71075826ec
commit 190990155e
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
5 changed files with 21 additions and 9 deletions

View file

@ -1331,7 +1331,7 @@ fn solve(
*type_index,
);
open_tag_union(subs, actual);
open_tag_union(subs, pools, actual);
state
}
@ -1571,7 +1571,7 @@ fn solve(
let almost_eq_snapshot = subs.snapshot();
// TODO: turn this on for bidirectional exhaustiveness checking
// open_tag_union(subs, real_var);
open_tag_union(subs, branches_var);
open_tag_union(subs, pools, branches_var);
let almost_eq = matches!(
unify(
&mut UEnv::new(subs),
@ -1901,7 +1901,7 @@ fn compact_lambdas_and_check_obligations(
awaiting_specialization.union(new_awaiting);
}
fn open_tag_union(subs: &mut Subs, var: Variable) {
fn open_tag_union(subs: &mut Subs, pools: &mut Pools, var: Variable) {
let mut stack = vec![var];
while let Some(var) = stack.pop() {
use {Content::*, FlatType::*};
@ -1910,9 +1910,9 @@ fn open_tag_union(subs: &mut Subs, var: Variable) {
match desc.content {
Structure(TagUnion(tags, ext)) => {
if let Structure(EmptyTagUnion) = subs.get_content_without_compacting(ext.var()) {
let new_ext = TagExt::Any(subs.fresh_unnamed_flex_var());
subs.set_rank(new_ext.var(), desc.rank);
let new_union = Structure(TagUnion(tags, new_ext));
let new_ext_var = register(subs, desc.rank, pools, Content::FlexVar(None));
let new_union = Structure(TagUnion(tags, TagExt::Any(new_ext_var)));
subs.set_content(var, new_union);
}

View file

@ -3,6 +3,6 @@ app "test" provides [main] to "./platform"
main =
\x -> when x is
#^ [A [B]w_a [C]w_b]
#^ [A [B]* [C]*]
A B _ -> ""
A _ C -> ""

View file

@ -2,6 +2,6 @@ app "test" provides [main] to "./platform"
main =
\x -> when x is
#^ { a : [A { b : [B]w_a }*]w_b }*
#^ { a : [A { b : [B]* }*]* }*
{ a: A { b: B } } -> ""
_ -> ""

View file

@ -0,0 +1,12 @@
app "test" provides [main] to "./platform"
main =
isCorrectOrder (IsList [IsStr ""])
# ^^^^^^^^^^^^^^ [IsList (List a), IsStr Str]w_b as a -[[isCorrectOrder(1)]]-> Bool
isCorrectOrder = \pair ->
#^^^^^^^^^^^^^^{-1} [IsList (List a)]* as a -[[isCorrectOrder(1)]]-> Bool
when pair is
IsList l -> List.all l isCorrectOrder
_ -> Bool.false

View file

@ -1,6 +1,6 @@
app "test" provides [getInfallible] to "./platform"
getInfallible = \result -> when result is
#^^^^^^^^^^^^^{-1} [Ok a]w_b -[[getInfallible(0)]]-> a
#^^^^^^^^^^^^^{-1} [Ok a]* -[[getInfallible(0)]]-> a
Ok x -> x
_ -> crash "turns out this was fallible"