Merge pull request #979 from aiken-lang/fix_casting_inference

Fix pattern inference and annotation requirements.
This commit is contained in:
Matthias Benkort 2024-07-25 09:40:27 +02:00 committed by GitHub
commit 63863c948f
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
5 changed files with 234 additions and 37 deletions

View File

@ -1404,7 +1404,10 @@ impl<'a> CodeGenerator<'a> {
), ),
) )
} else { } else {
assert!(data_type.constructors.len() == 1); assert!(
data_type.constructors.len() == 1,
"data_type={data_type:#?}"
);
then then
}; };

View File

@ -2024,18 +2024,6 @@ fn forbid_expect_into_opaque_type_from_data() {
)) ))
} }
#[test]
fn allow_expect_into_type_from_data() {
let source_code = r#"
fn bar(n: Data) {
expect a: Option<Int> = n
a
}
"#;
assert!(check(parse(source_code)).is_ok())
}
#[test] #[test]
fn forbid_partial_down_casting() { fn forbid_partial_down_casting() {
let source_code = r#" let source_code = r#"
@ -2075,7 +2063,106 @@ fn forbid_partial_up_casting() {
} }
#[test] #[test]
fn allow_expect_into_type_from_data_2() { fn allow_expect_into_type_from_data() {
let source_code = r#"
fn bar(n: Data) {
expect a: Option<Int> = n
a
}
"#;
assert!(check(parse(source_code)).is_ok())
}
#[test]
fn forbid_casting_into_type_from_data() {
let source_code = r#"
fn bar(n: Data) {
let a: Option<Int> = n
a
}
"#;
assert!(matches!(
check(parse(source_code)),
Err((_, Error::CouldNotUnify { .. }))
))
}
#[test]
fn forbid_casting_into_var_from_data_with_ann() {
let source_code = r#"
fn bar(n: Data) {
let a: Option<Int> = n
a
}
"#;
assert!(matches!(
check(parse(source_code)),
Err((_, Error::CouldNotUnify { .. }))
))
}
#[test]
fn allow_let_rebinding() {
let source_code = r#"
fn bar(n: Data) {
let a = n
a
}
"#;
assert!(check(parse(source_code)).is_ok())
}
#[test]
fn expect_rebinding_requires_annotation() {
let source_code = r#"
fn bar(n: Data) -> Option<Int> {
expect a = n
a
}
"#;
assert!(matches!(
check(parse(source_code)),
Err((_, Error::CastDataNoAnn { .. }))
))
}
#[test]
fn forbid_casting_into_var_from_data_with_ann_indirect() {
let source_code = r#"
fn bar(n: Data) -> Option<Int> {
let a = n
a
}
"#;
assert!(matches!(
check(parse(source_code)),
Err((_, Error::CouldNotUnify { .. }))
))
}
#[test]
fn forbid_casting_into_pattern_from_data() {
let source_code = r#"
fn bar(n: Data) {
let Some(a) = n
a
}
"#;
assert!(matches!(
check(parse(source_code)),
Err((_, Error::CouldNotUnify { .. }))
))
}
#[test]
fn allow_expect_into_monomorphic_type_from_data_with_pattern() {
let source_code = r#" let source_code = r#"
fn bar(n: Data) { fn bar(n: Data) {
expect Some(a): Option<Int> = n expect Some(a): Option<Int> = n
@ -2086,6 +2173,52 @@ fn allow_expect_into_type_from_data_2() {
assert!(check(parse(source_code)).is_ok()) assert!(check(parse(source_code)).is_ok())
} }
#[test]
fn forbid_expect_into_generic_type_from_data_with_pattern() {
let source_code = r#"
fn bar(n: Data) {
expect Some(a) = n
a
}
"#;
assert!(matches!(
check(parse(source_code)),
Err((_, Error::CastDataNoAnn { .. }))
))
}
#[test]
fn allow_generic_expect_without_typecast() {
let source_code = r#"
pub fn unwrap(opt: Option<a>) -> a {
expect Some(a) = opt
a
}
"#;
assert!(check(parse(source_code)).is_ok())
}
#[test]
fn allow_expect_into_custom_type_from_data_no_annotation() {
let source_code = r#"
type OrderDatum {
requested_handle: ByteArray,
amount: Int,
other: Bool,
}
fn foo(datum: Data) {
expect OrderDatum { requested_handle, .. } = datum
requested_handle
}
"#;
assert!(check(parse(source_code)).is_ok())
}
#[test] #[test]
fn forbid_expect_from_arbitrary_type() { fn forbid_expect_from_arbitrary_type() {
let source_code = r#" let source_code = r#"
@ -2110,7 +2243,7 @@ fn forbid_expect_from_arbitrary_type() {
} }
#[test] #[test]
fn forbid_expect_into_opaque_type_constructor_without_typecasting_in_module() { fn allow_expect_into_opaque_type_constructor_without_typecasting_in_module() {
let source_code = r#" let source_code = r#"
opaque type Thing { opaque type Thing {
Foo(Int) Foo(Int)

View File

@ -406,6 +406,21 @@ impl Type {
} }
} }
/// Check whether a given type is fully specialized and has only one possible
/// form. Said differently, this recursively checks if the type still contains
/// unbound or generic variables.
pub fn is_monomorphic(&self) -> bool {
match self {
Self::App { args, .. } => args.iter().all(|arg| arg.is_monomorphic()),
Self::Fn { args, ret, .. } => {
args.iter().all(|arg| arg.is_monomorphic()) && ret.is_monomorphic()
}
Self::Tuple { elems, .. } => elems.iter().all(|arg| arg.is_monomorphic()),
Self::Pair { fst, snd, .. } => [fst, snd].iter().all(|arg| arg.is_monomorphic()),
Self::Var { tipo, .. } => tipo.borrow().is_monomorphic(),
}
}
pub fn is_generic(&self) -> bool { pub fn is_generic(&self) -> bool {
match self { match self {
Self::App { args, .. } => { Self::App { args, .. } => {
@ -931,6 +946,16 @@ pub enum TypeVar {
} }
impl TypeVar { impl TypeVar {
/// Check whether a given type is fully specialized and has only one possible
/// form. Said differently, this recursively checks if the type still contains
/// unbound or generic variables.
pub fn is_monomorphic(&self) -> bool {
match self {
Self::Link { tipo } => tipo.is_monomorphic(),
Self::Unbound { .. } | Self::Generic { .. } => false,
}
}
pub fn is_unbound(&self) -> bool { pub fn is_unbound(&self) -> bool {
matches!(self, Self::Unbound { .. }) matches!(self, Self::Unbound { .. })
} }

View File

@ -1169,12 +1169,13 @@ impl<'a, 'b> ExprTyper<'a, 'b> {
location: Span, location: Span,
) -> Result<TypedExpr, Error> { ) -> Result<TypedExpr, Error> {
let typed_value = self.infer(untyped_value.clone())?; let typed_value = self.infer(untyped_value.clone())?;
let mut value_typ = typed_value.tipo(); let mut value_typ = typed_value.tipo();
let value_is_data = value_typ.is_data(); let value_is_data = value_typ.is_data();
// Check that any type annotation is accurate. // Check that any type annotation is accurate.
let ann_typ = if let Some(ann) = annotation { let pattern = if let Some(ann) = annotation {
let ann_typ = self let ann_typ = self
.type_from_annotation(ann) .type_from_annotation(ann)
.and_then(|t| self.instantiate(t, &mut HashMap::new(), location))?; .and_then(|t| self.instantiate(t, &mut HashMap::new(), location))?;
@ -1188,9 +1189,15 @@ impl<'a, 'b> ExprTyper<'a, 'b> {
value_typ = ann_typ.clone(); value_typ = ann_typ.clone();
Some(ann_typ) // Ensure the pattern matches the type of the value
} else { PatternTyper::new(self.environment, &self.hydrator).unify(
if value_is_data && !untyped_pattern.is_var() && !untyped_pattern.is_discard() { untyped_pattern.clone(),
value_typ.clone(),
Some(ann_typ),
kind.is_let(),
)
} else if value_is_data && !kind.is_let() {
let cast_data_no_ann = || {
let ann = Annotation::Constructor { let ann = Annotation::Constructor {
location: Span::empty(), location: Span::empty(),
module: None, module: None,
@ -1198,28 +1205,57 @@ impl<'a, 'b> ExprTyper<'a, 'b> {
arguments: vec![], arguments: vec![],
}; };
return Err(Error::CastDataNoAnn { Err(Error::CastDataNoAnn {
location, location,
value: UntypedExpr::Assignment { value: UntypedExpr::Assignment {
location, location,
value: untyped_value.into(), value: untyped_value.clone().into(),
patterns: AssignmentPattern::new(untyped_pattern, Some(ann), Span::empty()) patterns: AssignmentPattern::new(
untyped_pattern.clone(),
Some(ann),
Span::empty(),
)
.into(), .into(),
kind, kind,
}, },
}); })
}
None
}; };
if !untyped_pattern.is_var() && !untyped_pattern.is_discard() {
let ann_typ = self.new_unbound_var();
match PatternTyper::new(self.environment, &self.hydrator).unify(
untyped_pattern.clone(),
ann_typ.clone(),
None,
false,
) {
Ok(pattern) if ann_typ.is_monomorphic() => {
self.unify(
ann_typ.clone(),
value_typ.clone(),
typed_value.type_defining_location(),
true,
)?;
value_typ = ann_typ.clone();
Ok(pattern)
}
Ok(..) | Err(..) => cast_data_no_ann(),
}
} else {
cast_data_no_ann()
}
} else {
// Ensure the pattern matches the type of the value // Ensure the pattern matches the type of the value
let pattern = PatternTyper::new(self.environment, &self.hydrator).unify( PatternTyper::new(self.environment, &self.hydrator).unify(
untyped_pattern.clone(), untyped_pattern.clone(),
value_typ.clone(), value_typ.clone(),
ann_typ, None,
kind.is_let(), kind.is_let(),
)?; )
}?;
// If `expect` is explicitly used, we still check exhaustiveness but instead of returning an // If `expect` is explicitly used, we still check exhaustiveness but instead of returning an
// error we emit a warning which explains that using `expect` is unnecessary. // error we emit a warning which explains that using `expect` is unnecessary.

View File

@ -141,11 +141,11 @@ impl<'a, 'b> PatternTyper<'a, 'b> {
pattern: UntypedPattern, pattern: UntypedPattern,
tipo: Rc<Type>, tipo: Rc<Type>,
ann_type: Option<Rc<Type>>, ann_type: Option<Rc<Type>>,
is_let: bool, warn_on_discard: bool,
) -> Result<TypedPattern, Error> { ) -> Result<TypedPattern, Error> {
match pattern { match pattern {
Pattern::Discard { name, location } => { Pattern::Discard { name, location } => {
if is_let { if warn_on_discard {
// Register declaration for the unused variable detection // Register declaration for the unused variable detection
self.environment self.environment
.warnings .warnings