Prevent constant evaluating to generic/unbound functions
Constants are like tiny programs, so they are bound by the same rules as validators and other programs. In fact, functions are slightly more flexible in that they allow generic constant expressions like `List<a>`. Yet, there is no way to contain such generic structure that contain inhabitants in a way that satisfies the type-checker. In the example of `List<a>`, the only inhabitant of that type that we can construct is the empty list. Anything else would require holding onto some generic value. In addition, we can't force literal values into generic annotation, as something like: ``` const foo: List<a> = [1, 2, 3] ``` wouldn't type-check either since the right-side would unify to `List<Int>`. And again, the only right-hand side that can type-check is the empty list without any inhabitant. The added restriction on generic function is necessary because while we allow constants to return lambda, we cannot (easily) generate UPLC that is generic in its argument. By the time we generate UPLC, the underlying types have to be known.
This commit is contained in:
parent
51b6b77db8
commit
e8d97028ad
|
@ -8,6 +8,7 @@
|
|||
|
||||
### Changed
|
||||
|
||||
- **aiken-lang**: Forbid constants evaluating to generic or unbound functions. Same restrictions as for validators or any exported UPLC programs apply here. @KtorZ & @MicroProofs
|
||||
- **aiken-lang**: Fix compiler crash on trace + expect as last expression of a clause. See #1029. @KtorZ
|
||||
- **aiken-lang**: Fix redundant warning on introduced identifiers when destructuring validator params. @KtorZ
|
||||
- **aiken-lsp**: Compile project using verbose tracing, to avoid having the language server complain about unused imports. @KtorZ
|
||||
|
|
|
@ -3394,3 +3394,54 @@ fn destructuring_validator_params_record() {
|
|||
"should be empty: {warnings:#?}"
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn constant_generic_lambda() {
|
||||
let source_code = r#"const foo: fn(a) -> List<a> = fn(x: a) { [x] }"#;
|
||||
assert!(matches!(
|
||||
check(parse(source_code)),
|
||||
Err((_, Error::GenericLeftAtBoundary { .. }))
|
||||
))
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn constant_generic_mismatch() {
|
||||
let source_code = r#"const foo: List<a> = [42]"#;
|
||||
assert!(matches!(
|
||||
check(parse(source_code)),
|
||||
Err((_, Error::CouldNotUnify { .. }))
|
||||
))
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn constant_generic_inferred_1() {
|
||||
let source_code = r#"const foo = [42]"#;
|
||||
assert!(check(parse(source_code)).is_ok());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn constant_generic_inferred_2() {
|
||||
let source_code = r#"
|
||||
const foo = fn(x) { [x] }(42)
|
||||
|
||||
test my_test() {
|
||||
foo == [42]
|
||||
}
|
||||
"#;
|
||||
assert!(check(parse(source_code)).is_ok());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn constant_generic_inferred_3() {
|
||||
let source_code = r#"const foo: List<a> = fn(x) { [x] }(42)"#;
|
||||
assert!(matches!(
|
||||
check(parse(source_code)),
|
||||
Err((_, Error::CouldNotUnify { .. }))
|
||||
))
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn constant_generic_empty() {
|
||||
let source_code = r#"const foo: List<a> = []"#;
|
||||
assert!(check_validator(parse(source_code)).is_ok());
|
||||
}
|
||||
|
|
|
@ -1044,7 +1044,7 @@ The best thing to do from here is to remove it."#))]
|
|||
#[error("I choked on a generic type left in an outward-facing interface.\n")]
|
||||
#[diagnostic(code("illegal::generic_in_abi"))]
|
||||
#[diagnostic(help(
|
||||
"Functions of the outer-most parts of a project, such as a validator or a property-based test, must be fully instantiated. That means they can no longer carry unbound generic variables. The type must be fully-known at this point since many structural validation must occur to ensure a safe boundary between the on-chain and off-chain worlds."
|
||||
"Elements of the outer-most parts of a project, such as a validator, constants or a property-based test, must be fully instantiated. That means they can no longer carry unbound or generic variables. The type must be fully-known at this point since many structural validation must occur to ensure a safe boundary between the on-chain and off-chain worlds."
|
||||
))]
|
||||
GenericLeftAtBoundary {
|
||||
#[label("unbound generic at boundary")]
|
||||
|
|
|
@ -655,6 +655,10 @@ fn infer_definition(
|
|||
|
||||
let tipo = typed_expr.tipo();
|
||||
|
||||
if tipo.is_function() && !tipo.is_monomorphic() {
|
||||
return Err(Error::GenericLeftAtBoundary { location });
|
||||
}
|
||||
|
||||
let variant = ValueConstructor {
|
||||
public,
|
||||
variant: ValueConstructorVariant::ModuleConstant {
|
||||
|
|
Loading…
Reference in New Issue