Skip to content

Commit

Permalink
Check for types aliasing uni T values
Browse files Browse the repository at this point in the history
When lowering to MIR, we check for types that aren't fully inferred.
This commit extends this check to also check for `uni ref T` and
`uni mut T` values stored inside other types, producing an error when
encountering such types. This ensures that one can't violate the
uniqueness constraints through e.g. a generic method, without
complicating the type system (e.g. by adding a `T: ref` bound).

This fixes #713.

Changelog: fixed
  • Loading branch information
yorickpeterse committed Dec 3, 2024
1 parent 45e116b commit 26070da
Show file tree
Hide file tree
Showing 4 changed files with 127 additions and 20 deletions.
18 changes: 18 additions & 0 deletions compiler/src/diagnostics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -845,6 +845,24 @@ impl Diagnostics {
);
}

pub(crate) fn type_containing_uni_alias(
&mut self,
name: String,
file: PathBuf,
location: Location,
) {
self.error(
DiagnosticId::InvalidType,
format!(
"the type of this expression ('{}') is invalid because it \
contains an 'uni ref T' or 'uni mut T' value",
name,
),
file,
location,
);
}

pub(crate) fn string_literal_too_large(
&mut self,
limit: usize,
Expand Down
29 changes: 19 additions & 10 deletions compiler/src/mir/passes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,9 @@ use types::format::format_type;
use types::module_name::ModuleName;
use types::{
self, Block as _, ClassId, ConstantId, Inline, MethodId, ModuleId, Symbol,
TypeBounds, TypeRef, EQ_METHOD, FIELDS_LIMIT, OPTION_NONE, OPTION_SOME,
RESULT_CLASS, RESULT_ERROR, RESULT_MODULE, RESULT_OK,
TypeBounds, TypeRef, VerificationError, EQ_METHOD, FIELDS_LIMIT,
OPTION_NONE, OPTION_SOME, RESULT_CLASS, RESULT_ERROR, RESULT_MODULE,
RESULT_OK,
};

const SELF_NAME: &str = "self";
Expand Down Expand Up @@ -2048,15 +2049,23 @@ impl<'a> LowerMethod<'a> {
}

fn check_inferred(&mut self, typ: TypeRef, location: Location) {
if typ.is_inferred(self.db()) {
return;
match typ.verify_type(self.db(), 0) {
Ok(()) => {}
Err(VerificationError::Incomplete) => {
self.state.diagnostics.cant_infer_type(
format_type(self.db(), typ),
self.file(),
location,
);
}
Err(VerificationError::UniViolation) => {
self.state.diagnostics.type_containing_uni_alias(
format_type(self.db(), typ),
self.file(),
location,
);
}
}

self.state.diagnostics.cant_infer_type(
format_type(self.db(), typ),
self.file(),
location,
);
}

fn input_expression(
Expand Down
57 changes: 57 additions & 0 deletions std/fixtures/diagnostics/uni_aliasing.inko
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
class User {
let @name: String
}

class Box[T] {
let @value: Option[T]
let @borrow: Option[ref T]

fn mut store(value: T) {
@value = Option.Some(value)
}
}

fn example1 {
let a = [recover User('Alice')]

a.opt(0)
}

fn example2 {
let a = recover User('Alice')
let b = Option.Some(a)

b.as_ref
}

fn example3 {
let a = recover User('Alice')

Box(value: Option.Some(a), borrow: Option.None)
}

fn example4 {
let a = recover User('Alice')
let b = Box(value: Option.None, borrow: Option.None)

b.value = Option.Some(a)
}

fn example5 {
let a = recover User('Alice')
let b = Box(value: Option.None, borrow: Option.None)

b.store(a)
}

fn example6 {
let a = recover User('Alice')

ref a
}

# uni_aliasing.inko:17:3 error(invalid-type): the type of this expression ('Option[uni ref User]') is invalid because it contains an 'uni ref T' or 'uni mut T' value
# uni_aliasing.inko:24:3 error(invalid-type): the type of this expression ('Option[uni ref User]') is invalid because it contains an 'uni ref T' or 'uni mut T' value
# uni_aliasing.inko:30:38 error(invalid-type): the type of this expression ('Option[uni ref User]') is invalid because it contains an 'uni ref T' or 'uni mut T' value
# uni_aliasing.inko:35:43 error(invalid-type): the type of this expression ('Option[uni ref User]') is invalid because it contains an 'uni ref T' or 'uni mut T' value
# uni_aliasing.inko:42:43 error(invalid-type): the type of this expression ('Option[uni ref User]') is invalid because it contains an 'uni ref T' or 'uni mut T' value
43 changes: 33 additions & 10 deletions types/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3888,6 +3888,15 @@ impl Shape {
}
}

#[derive(Copy, Clone)]
pub enum VerificationError {
/// The type isn't fully inferred.
Incomplete,

/// The type contains one or more aliases to an `uni T` type.
UniViolation,
}

/// A reference to a type.
#[derive(Debug, PartialEq, Eq, Clone, Copy, Hash)]
pub enum TypeRef {
Expand Down Expand Up @@ -4928,8 +4937,19 @@ impl TypeRef {
}
}

pub fn is_inferred(self, db: &Database) -> bool {
pub fn verify_type(
self,
db: &Database,
depth: usize,
) -> Result<(), VerificationError> {
match self {
// `uni ref T` and `uni mut T` are valid as an outer-most type, as
// we can't assign such types to anything or store them anywhere.
// This in turn allows them to be used as e.g. the receiver of
// methods in certain cases.
TypeRef::UniRef(_) | TypeRef::UniMut(_) if depth > 0 => {
Err(VerificationError::UniViolation)
}
TypeRef::Owned(id)
| TypeRef::Uni(id)
| TypeRef::Ref(id)
Expand All @@ -4944,7 +4964,7 @@ impl TypeRef {
.unwrap()
.mapping
.values()
.all(|v| v.is_inferred(db))
.try_for_each(|v| v.verify_type(db, depth + 1))
}
TypeId::TraitInstance(ins)
if ins.instance_of.is_generic(db) =>
Expand All @@ -4953,20 +4973,23 @@ impl TypeRef {
.unwrap()
.mapping
.values()
.all(|v| v.is_inferred(db))
.try_for_each(|v| v.verify_type(db, depth + 1))
}
TypeId::Closure(id) => {
id.arguments(db)
.into_iter()
.all(|arg| arg.value_type.is_inferred(db))
&& id.return_type(db).is_inferred(db)
id.arguments(db).into_iter().try_for_each(|arg| {
arg.value_type.verify_type(db, depth + 1)
})?;

id.return_type(db).verify_type(db, depth + 1)
}
_ => true,
_ => Ok(()),
},
TypeRef::Placeholder(id) => {
id.value(db).map_or(false, |v| v.is_inferred(db))
id.value(db).map_or(Err(VerificationError::Incomplete), |v| {
v.verify_type(db, depth + 1)
})
}
_ => true,
_ => Ok(()),
}
}

Expand Down

0 comments on commit 26070da

Please sign in to comment.