feat: block expects on opaque types

This commit is contained in:
rvcas 2024-03-12 17:31:13 -04:00
parent 1d72838f83
commit 7af4ef53ab
No known key found for this signature in database
GPG Key ID: C09B64E263F7D68C
11 changed files with 112 additions and 8 deletions

View File

@ -1225,6 +1225,7 @@ impl TypedPattern {
} }
pub fn tipo(&self, value: &TypedExpr) -> Option<Rc<Type>> { pub fn tipo(&self, value: &TypedExpr) -> Option<Rc<Type>> {
// expect thing: Wow = thing
match self { match self {
Pattern::Int { .. } => Some(builtins::int()), Pattern::Int { .. } => Some(builtins::int()),
Pattern::Constructor { tipo, .. } => Some(tipo.clone()), Pattern::Constructor { tipo, .. } => Some(tipo.clone()),

View File

@ -1267,6 +1267,7 @@ pub fn prelude_data_types(id_gen: &IdGenerator) -> IndexMap<DataTypeKey, TypedDa
pub fn int() -> Rc<Type> { pub fn int() -> Rc<Type> {
Rc::new(Type::App { Rc::new(Type::App {
public: true, public: true,
opaque: false,
name: INT.to_string(), name: INT.to_string(),
module: "".to_string(), module: "".to_string(),
args: vec![], args: vec![],
@ -1277,6 +1278,7 @@ pub fn int() -> Rc<Type> {
pub fn data() -> Rc<Type> { pub fn data() -> Rc<Type> {
Rc::new(Type::App { Rc::new(Type::App {
public: true, public: true,
opaque: false,
name: DATA.to_string(), name: DATA.to_string(),
module: "".to_string(), module: "".to_string(),
args: vec![], args: vec![],
@ -1288,6 +1290,7 @@ pub fn byte_array() -> Rc<Type> {
Rc::new(Type::App { Rc::new(Type::App {
args: vec![], args: vec![],
public: true, public: true,
opaque: false,
name: BYTE_ARRAY.to_string(), name: BYTE_ARRAY.to_string(),
module: "".to_string(), module: "".to_string(),
alias: None, alias: None,
@ -1297,6 +1300,7 @@ pub fn byte_array() -> Rc<Type> {
pub fn g1_element() -> Rc<Type> { pub fn g1_element() -> Rc<Type> {
Rc::new(Type::App { Rc::new(Type::App {
public: true, public: true,
opaque: false,
module: "".to_string(), module: "".to_string(),
name: G1_ELEMENT.to_string(), name: G1_ELEMENT.to_string(),
args: vec![], args: vec![],
@ -1307,6 +1311,7 @@ pub fn g1_element() -> Rc<Type> {
pub fn g2_element() -> Rc<Type> { pub fn g2_element() -> Rc<Type> {
Rc::new(Type::App { Rc::new(Type::App {
public: true, public: true,
opaque: false,
module: "".to_string(), module: "".to_string(),
name: G2_ELEMENT.to_string(), name: G2_ELEMENT.to_string(),
args: vec![], args: vec![],
@ -1317,6 +1322,7 @@ pub fn g2_element() -> Rc<Type> {
pub fn miller_loop_result() -> Rc<Type> { pub fn miller_loop_result() -> Rc<Type> {
Rc::new(Type::App { Rc::new(Type::App {
public: true, public: true,
opaque: false,
module: "".to_string(), module: "".to_string(),
name: MILLER_LOOP_RESULT.to_string(), name: MILLER_LOOP_RESULT.to_string(),
args: vec![], args: vec![],
@ -1332,6 +1338,7 @@ pub fn bool() -> Rc<Type> {
Rc::new(Type::App { Rc::new(Type::App {
args: vec![], args: vec![],
public: true, public: true,
opaque: false,
name: BOOL.to_string(), name: BOOL.to_string(),
module: "".to_string(), module: "".to_string(),
alias: None, alias: None,
@ -1342,6 +1349,7 @@ pub fn prng() -> Rc<Type> {
Rc::new(Type::App { Rc::new(Type::App {
args: vec![], args: vec![],
public: true, public: true,
opaque: false,
name: PRNG.to_string(), name: PRNG.to_string(),
module: "".to_string(), module: "".to_string(),
alias: None, alias: None,
@ -1355,6 +1363,7 @@ pub fn fuzzer(a: Rc<Type>) -> Rc<Type> {
name: "PRNG".to_string(), name: "PRNG".to_string(),
arguments: vec![], arguments: vec![],
}; };
Rc::new(Type::Fn { Rc::new(Type::Fn {
args: vec![prng()], args: vec![prng()],
ret: option(tuple(vec![prng(), a])), ret: option(tuple(vec![prng(), a])),
@ -1391,6 +1400,7 @@ pub fn fuzzer(a: Rc<Type>) -> Rc<Type> {
pub fn list(t: Rc<Type>) -> Rc<Type> { pub fn list(t: Rc<Type>) -> Rc<Type> {
Rc::new(Type::App { Rc::new(Type::App {
public: true, public: true,
opaque: false,
name: LIST.to_string(), name: LIST.to_string(),
module: "".to_string(), module: "".to_string(),
args: vec![t], args: vec![t],
@ -1402,6 +1412,7 @@ pub fn string() -> Rc<Type> {
Rc::new(Type::App { Rc::new(Type::App {
args: vec![], args: vec![],
public: true, public: true,
opaque: false,
name: STRING.to_string(), name: STRING.to_string(),
module: "".to_string(), module: "".to_string(),
alias: None, alias: None,
@ -1412,6 +1423,7 @@ pub fn void() -> Rc<Type> {
Rc::new(Type::App { Rc::new(Type::App {
args: vec![], args: vec![],
public: true, public: true,
opaque: false,
name: VOID.to_string(), name: VOID.to_string(),
module: "".to_string(), module: "".to_string(),
alias: None, alias: None,
@ -1421,6 +1433,7 @@ pub fn void() -> Rc<Type> {
pub fn option(a: Rc<Type>) -> Rc<Type> { pub fn option(a: Rc<Type>) -> Rc<Type> {
Rc::new(Type::App { Rc::new(Type::App {
public: true, public: true,
opaque: false,
name: OPTION.to_string(), name: OPTION.to_string(),
module: "".to_string(), module: "".to_string(),
args: vec![a], args: vec![a],
@ -1431,6 +1444,7 @@ pub fn option(a: Rc<Type>) -> Rc<Type> {
pub fn ordering() -> Rc<Type> { pub fn ordering() -> Rc<Type> {
Rc::new(Type::App { Rc::new(Type::App {
public: true, public: true,
opaque: false,
name: ORDERING.to_string(), name: ORDERING.to_string(),
module: "".to_string(), module: "".to_string(),
args: vec![], args: vec![],
@ -1448,17 +1462,20 @@ pub fn function(args: Vec<Rc<Type>>, ret: Rc<Type>) -> Rc<Type> {
pub fn generic_var(id: u64) -> Rc<Type> { pub fn generic_var(id: u64) -> Rc<Type> {
let tipo = Rc::new(RefCell::new(TypeVar::Generic { id })); let tipo = Rc::new(RefCell::new(TypeVar::Generic { id }));
Rc::new(Type::Var { tipo, alias: None }) Rc::new(Type::Var { tipo, alias: None })
} }
pub fn unbound_var(id: u64) -> Rc<Type> { pub fn unbound_var(id: u64) -> Rc<Type> {
let tipo = Rc::new(RefCell::new(TypeVar::Unbound { id })); let tipo = Rc::new(RefCell::new(TypeVar::Unbound { id }));
Rc::new(Type::Var { tipo, alias: None }) Rc::new(Type::Var { tipo, alias: None })
} }
pub fn wrapped_redeemer(redeemer: Rc<Type>) -> Rc<Type> { pub fn wrapped_redeemer(redeemer: Rc<Type>) -> Rc<Type> {
Rc::new(Type::App { Rc::new(Type::App {
public: true, public: true,
opaque: false,
module: "".to_string(), module: "".to_string(),
name: REDEEMER_WRAPPER.to_string(), name: REDEEMER_WRAPPER.to_string(),
args: vec![redeemer], args: vec![redeemer],

View File

@ -1793,3 +1793,41 @@ fn backpassing_type_annotation() {
assert!(check(parse(source_code)).is_ok()) assert!(check(parse(source_code)).is_ok())
} }
fn forbid_expect_into_opaque_type_from_data() {
let source_code = r#"
opaque type Thing { inner: Int }
fn bar(n: Data) {
expect a: Thing = n
a
}
"#;
assert!(matches!(
check(parse(source_code)),
Err((_, Error::ExpectOnOpaqueType { .. }))
))
}
#[test]
fn forbid_expect_into_opaque_type_constructor() {
let source_code = r#"
opaque type Thing {
Foo(Int)
Bar(Int)
}
fn bar(n: Thing) {
expect Foo(a) = n
a
}
"#;
assert!(matches!(
check(parse(source_code)),
Err((_, Error::ExpectOnOpaqueType { .. }))
))
}

View File

@ -42,6 +42,7 @@ pub enum Type {
/// ///
App { App {
public: bool, public: bool,
opaque: bool,
module: String, module: String,
name: String, name: String,
args: Vec<Rc<Type>>, args: Vec<Rc<Type>>,
@ -152,12 +153,14 @@ impl Type {
Rc::new(match self { Rc::new(match self {
Type::App { Type::App {
public, public,
opaque,
module, module,
name, name,
args, args,
.. ..
} => Type::App { } => Type::App {
public, public,
opaque,
module, module,
name, name,
args, args,
@ -181,17 +184,13 @@ impl Type {
} }
} }
pub fn is_result_constructor(&self) -> bool { pub fn is_opaque(&self) -> bool {
match self { match self {
Type::Fn { ret, .. } => ret.is_result(), Type::App { opaque, .. } => *opaque,
_ => false, _ => false,
} }
} }
pub fn is_result(&self) -> bool {
matches!(self, Self::App { name, module, .. } if "Result" == name && module.is_empty())
}
pub fn is_unbound(&self) -> bool { pub fn is_unbound(&self) -> bool {
matches!(self, Self::Var { tipo, .. } if tipo.borrow().is_unbound()) matches!(self, Self::Var { tipo, .. } if tipo.borrow().is_unbound())
} }
@ -459,6 +458,7 @@ impl Type {
pub fn get_app_args( pub fn get_app_args(
&self, &self,
public: bool, public: bool,
opaque: bool,
module: &str, module: &str,
name: &str, name: &str,
arity: usize, arity: usize,
@ -481,7 +481,7 @@ impl Type {
Self::Var { tipo, alias } => { Self::Var { tipo, alias } => {
let args: Vec<_> = match tipo.borrow().deref() { let args: Vec<_> = match tipo.borrow().deref() {
TypeVar::Link { tipo } => { TypeVar::Link { tipo } => {
return tipo.get_app_args(public, module, name, arity, environment); return tipo.get_app_args(public, opaque, module, name, arity, environment);
} }
TypeVar::Unbound { .. } => { TypeVar::Unbound { .. } => {
@ -496,6 +496,7 @@ impl Type {
*tipo.borrow_mut() = TypeVar::Link { *tipo.borrow_mut() = TypeVar::Link {
tipo: Rc::new(Self::App { tipo: Rc::new(Self::App {
public, public,
opaque,
name: name.to_string(), name: name.to_string(),
module: module.to_owned(), module: module.to_owned(),
args: args.clone(), args: args.clone(),
@ -650,6 +651,7 @@ pub fn convert_opaque_type(
match t.as_ref() { match t.as_ref() {
Type::App { Type::App {
public, public,
opaque,
module, module,
name, name,
args, args,
@ -662,6 +664,7 @@ pub fn convert_opaque_type(
} }
Type::App { Type::App {
public: *public, public: *public,
opaque: *opaque,
module: module.clone(), module: module.clone(),
name: name.clone(), name: name.clone(),
args: new_args, args: new_args,
@ -736,6 +739,7 @@ pub fn find_and_replace_generics(
Type::App { Type::App {
args, args,
public, public,
opaque,
module, module,
name, name,
alias, alias,
@ -748,6 +752,7 @@ pub fn find_and_replace_generics(
let t = Type::App { let t = Type::App {
args: new_args, args: new_args,
public: *public, public: *public,
opaque: *opaque,
module: module.clone(), module: module.clone(),
name: name.clone(), name: name.clone(),
alias: alias.clone(), alias: alias.clone(),

View File

@ -546,6 +546,7 @@ impl<'a> Environment<'a> {
match t.deref() { match t.deref() {
Type::App { Type::App {
public, public,
opaque,
name, name,
module, module,
args, args,
@ -555,8 +556,10 @@ impl<'a> Environment<'a> {
.iter() .iter()
.map(|t| self.instantiate(t.clone(), ids, hydrator)) .map(|t| self.instantiate(t.clone(), ids, hydrator))
.collect(); .collect();
Rc::new(Type::App { Rc::new(Type::App {
public: *public, public: *public,
opaque: *opaque,
name: name.clone(), name: name.clone(),
module: module.clone(), module: module.clone(),
alias: alias.clone(), alias: alias.clone(),
@ -983,6 +986,7 @@ impl<'a> Environment<'a> {
Definition::DataType(DataType { Definition::DataType(DataType {
name, name,
public, public,
opaque,
parameters, parameters,
location, location,
constructors, constructors,
@ -997,6 +1001,7 @@ impl<'a> Environment<'a> {
let tipo = Rc::new(Type::App { let tipo = Rc::new(Type::App {
public: *public, public: *public,
opaque: *opaque,
module: module.to_owned(), module: module.to_owned(),
name: name.clone(), name: name.clone(),
args: parameters.clone(), args: parameters.clone(),
@ -1856,6 +1861,7 @@ pub(crate) fn generalise(t: Rc<Type>, ctx_level: usize) -> Rc<Type> {
Type::App { Type::App {
public, public,
opaque,
module, module,
name, name,
args, args,
@ -1868,6 +1874,7 @@ pub(crate) fn generalise(t: Rc<Type>, ctx_level: usize) -> Rc<Type> {
Rc::new(Type::App { Rc::new(Type::App {
public: *public, public: *public,
opaque: *opaque,
module: module.clone(), module: module.clone(),
name: name.clone(), name: name.clone(),
args, args,

View File

@ -259,6 +259,13 @@ You can use '{discard}' and numbers to distinguish between similar names.
name: String, name: String,
}, },
#[error("I found an expect assignment involving an opaque type. This is not allowed.\n")]
#[diagnostic(code("illegal::expect_on_opaque"))]
ExpectOnOpaqueType {
#[label]
location: Span,
},
#[error("I found a type definition that has a function type in it. This is not allowed.\n")] #[error("I found a type definition that has a function type in it. This is not allowed.\n")]
#[diagnostic(code("illegal::function_in_type"))] #[diagnostic(code("illegal::function_in_type"))]
#[diagnostic(help( #[diagnostic(help(
@ -1045,6 +1052,7 @@ impl ExtraData for Error {
| Error::IncorrectTestArity { .. } | Error::IncorrectTestArity { .. }
| Error::GenericLeftAtBoundary { .. } | Error::GenericLeftAtBoundary { .. }
| Error::UnexpectedMultiPatternAssignment { .. } | Error::UnexpectedMultiPatternAssignment { .. }
| Error::ExpectOnOpaqueType { .. }
| Error::ValidatorMustReturnBool { .. } => None, | Error::ValidatorMustReturnBool { .. } => None,
Error::UnknownType { name, .. } Error::UnknownType { name, .. }

View File

@ -932,6 +932,7 @@ impl<'a, 'b> ExprTyper<'a, 'b> {
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();
let value_is_opaque = value_typ.is_opaque();
// Check that any type annotation is accurate. // Check that any type annotation is accurate.
let pattern = if let Some(ann) = annotation { let pattern = if let Some(ann) = annotation {
@ -939,6 +940,10 @@ impl<'a, 'b> ExprTyper<'a, 'b> {
.type_from_annotation(ann) .type_from_annotation(ann)
.map(|t| self.instantiate(t, &mut HashMap::new()))?; .map(|t| self.instantiate(t, &mut HashMap::new()))?;
if kind.is_expect() && (ann_typ.is_opaque() || value_is_opaque) {
return Err(Error::ExpectOnOpaqueType { location });
}
self.unify( self.unify(
ann_typ.clone(), ann_typ.clone(),
value_typ.clone(), value_typ.clone(),
@ -975,6 +980,10 @@ impl<'a, 'b> ExprTyper<'a, 'b> {
}); });
} }
if kind.is_expect() && value_is_opaque {
return Err(Error::ExpectOnOpaqueType { location });
}
// Ensure the pattern matches the type of the value // Ensure the pattern matches the type of the value
PatternTyper::new(self.environment, &self.hydrator).unify( PatternTyper::new(self.environment, &self.hydrator).unify(
untyped_pattern.clone(), untyped_pattern.clone(),

View File

@ -202,7 +202,7 @@ impl<'a, 'b> PatternTyper<'a, 'b> {
location, location,
elements, elements,
tail, tail,
} => match tipo.get_app_args(true, "", "List", 1, self.environment) { } => match tipo.get_app_args(true, false, "", "List", 1, self.environment) {
Some(args) => { Some(args) => {
let tipo = args let tipo = args
.first() .first()

View File

@ -368,6 +368,7 @@ mod tests {
module: "whatever".to_string(), module: "whatever".to_string(),
name: "Int".to_string(), name: "Int".to_string(),
public: true, public: true,
opaque: false,
args: vec![], args: vec![],
alias: None alias: None
}, },
@ -378,12 +379,14 @@ mod tests {
module: "".to_string(), module: "".to_string(),
name: "Pair".to_string(), name: "Pair".to_string(),
public: true, public: true,
opaque: false,
alias: None, alias: None,
args: vec![ args: vec![
Rc::new(Type::App { Rc::new(Type::App {
module: "whatever".to_string(), module: "whatever".to_string(),
name: "Int".to_string(), name: "Int".to_string(),
public: true, public: true,
opaque: false,
args: vec![], args: vec![],
alias: None alias: None
}), }),
@ -391,6 +394,7 @@ mod tests {
module: "whatever".to_string(), module: "whatever".to_string(),
name: "Bool".to_string(), name: "Bool".to_string(),
public: true, public: true,
opaque: false,
args: vec![], args: vec![],
alias: None alias: None
}), }),
@ -406,6 +410,7 @@ mod tests {
module: "whatever".to_string(), module: "whatever".to_string(),
name: "Int".to_string(), name: "Int".to_string(),
public: true, public: true,
opaque: false,
alias: None, alias: None,
}), }),
Rc::new(Type::App { Rc::new(Type::App {
@ -413,6 +418,7 @@ mod tests {
module: "whatever".to_string(), module: "whatever".to_string(),
name: "Bool".to_string(), name: "Bool".to_string(),
public: true, public: true,
opaque: false,
alias: None, alias: None,
}), }),
], ],
@ -421,6 +427,7 @@ mod tests {
module: "whatever".to_string(), module: "whatever".to_string(),
name: "Bool".to_string(), name: "Bool".to_string(),
public: true, public: true,
opaque: false,
alias: None, alias: None,
}), }),
alias: None, alias: None,
@ -437,6 +444,7 @@ mod tests {
module: "whatever".to_string(), module: "whatever".to_string(),
name: "Int".to_string(), name: "Int".to_string(),
public: true, public: true,
opaque: false,
}), }),
})), })),
}, },
@ -479,6 +487,7 @@ mod tests {
Type::Fn { Type::Fn {
args: vec![Rc::new(Type::App { args: vec![Rc::new(Type::App {
public: true, public: true,
opaque: false,
module: "".to_string(), module: "".to_string(),
name: "PRNG".to_string(), name: "PRNG".to_string(),
args: vec![], args: vec![],
@ -486,12 +495,14 @@ mod tests {
})], })],
ret: Rc::new(Type::App { ret: Rc::new(Type::App {
public: true, public: true,
opaque: false,
module: "".to_string(), module: "".to_string(),
name: "Option".to_string(), name: "Option".to_string(),
args: vec![Rc::new(Type::Tuple { args: vec![Rc::new(Type::Tuple {
elems: vec![ elems: vec![
Rc::new(Type::App { Rc::new(Type::App {
public: true, public: true,
opaque: false,
module: "".to_string(), module: "".to_string(),
name: "PRNG".to_string(), name: "PRNG".to_string(),
args: vec![], args: vec![],
@ -499,6 +510,7 @@ mod tests {
}), }),
Rc::new(Type::App { Rc::new(Type::App {
public: true, public: true,
opaque: false,
module: "".to_string(), module: "".to_string(),
name: "Bool".to_string(), name: "Bool".to_string(),
args: vec![], args: vec![],
@ -549,6 +561,7 @@ mod tests {
Type::Fn { Type::Fn {
args: vec![Rc::new(Type::App { args: vec![Rc::new(Type::App {
public: true, public: true,
opaque: false,
module: "".to_string(), module: "".to_string(),
name: "PRNG".to_string(), name: "PRNG".to_string(),
args: vec![], args: vec![],
@ -556,12 +569,14 @@ mod tests {
})], })],
ret: Rc::new(Type::App { ret: Rc::new(Type::App {
public: true, public: true,
opaque: false,
module: "".to_string(), module: "".to_string(),
name: "Option".to_string(), name: "Option".to_string(),
args: vec![Rc::new(Type::Tuple { args: vec![Rc::new(Type::Tuple {
elems: vec![ elems: vec![
Rc::new(Type::App { Rc::new(Type::App {
public: true, public: true,
opaque: false,
module: "".to_string(), module: "".to_string(),
name: "PRNG".to_string(), name: "PRNG".to_string(),
args: vec![], args: vec![],

View File

@ -8,6 +8,7 @@ Schema {
breadcrumbs: [ breadcrumbs: [
App { App {
public: true, public: true,
opaque: true,
module: "test_module", module: "test_module",
name: "Rational", name: "Rational",
args: [], args: [],

View File

@ -8,6 +8,7 @@ Schema {
breadcrumbs: [ breadcrumbs: [
App { App {
public: true, public: true,
opaque: true,
module: "test_module", module: "test_module",
name: "Dict", name: "Dict",
args: [ args: [
@ -16,6 +17,7 @@ Schema {
value: Link { value: Link {
tipo: App { tipo: App {
public: false, public: false,
opaque: false,
module: "test_module", module: "test_module",
name: "UUID", name: "UUID",
args: [], args: [],
@ -30,6 +32,7 @@ Schema {
value: Link { value: Link {
tipo: App { tipo: App {
public: true, public: true,
opaque: false,
module: "", module: "",
name: "Int", name: "Int",
args: [], args: [],