Phantom types

Closes #3314
This commit is contained in:
Ayaz Hafiz 2022-07-05 19:07:41 -04:00
parent e674c33b89
commit fc1617bf17
No known key found for this signature in database
GPG key ID: 0E2A37416A25EF58
3 changed files with 139 additions and 8 deletions

View file

@ -351,15 +351,28 @@ fn canonicalize_alias<'a>(
region: loc_lowercase.region,
});
}
None => {
is_phantom = true;
None => match kind {
AliasKind::Structural => {
is_phantom = true;
env.problems.push(Problem::PhantomTypeArgument {
typ: symbol,
variable_region: loc_lowercase.region,
variable_name: loc_lowercase.value.clone(),
});
}
env.problems.push(Problem::PhantomTypeArgument {
typ: symbol,
variable_region: loc_lowercase.region,
variable_name: loc_lowercase.value.clone(),
});
}
AliasKind::Opaque => {
// Opaques can have phantom types.
can_vars.push(Loc {
value: AliasVar {
name: loc_lowercase.value.clone(),
var: var_store.fresh(),
opt_bound_ability: None,
},
region: loc_lowercase.region,
});
}
},
}
}

View file

@ -7050,4 +7050,55 @@ mod solve_expr {
&["fun : {} -[[thunk(5) [A Str]*, thunk(5) { a : Str }]]-> Str",]
);
}
#[test]
fn check_phantom_type() {
infer_eq_without_problem(
indoc!(
r#"
F a b := b
foo : F Str Str -> F U8 Str
x : F Str Str
foo x
"#
),
"F U8 Str",
);
}
#[test]
fn infer_phantom_type_flow() {
infer_eq_without_problem(
indoc!(
r#"
F a b := b
foo : _ -> F U8 Str
foo = \it -> it
foo
"#
),
"F U8 Str -> F U8 Str",
);
}
#[test]
fn infer_unbound_phantom_type_star() {
infer_eq_without_problem(
indoc!(
r#"
F a b := b
foo = \@F {} -> @F ""
foo
"#
),
"F * {}* -> F * Str",
);
}
}