From e8d97028ad7f2c5023fa45a69484606f2a2a9813 Mon Sep 17 00:00:00 2001
From: KtorZ <matthias.benkort@gmail.com>
Date: Tue, 1 Oct 2024 18:27:56 +0200
Subject: [PATCH] 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.
---
 CHANGELOG.md                         |  1 +
 crates/aiken-lang/src/tests/check.rs | 51 ++++++++++++++++++++++++++++
 crates/aiken-lang/src/tipo/error.rs  |  2 +-
 crates/aiken-lang/src/tipo/infer.rs  |  4 +++
 4 files changed, 57 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a9999721..00830753 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -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
diff --git a/crates/aiken-lang/src/tests/check.rs b/crates/aiken-lang/src/tests/check.rs
index ed4ae19c..6a525456 100644
--- a/crates/aiken-lang/src/tests/check.rs
+++ b/crates/aiken-lang/src/tests/check.rs
@@ -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());
+}
diff --git a/crates/aiken-lang/src/tipo/error.rs b/crates/aiken-lang/src/tipo/error.rs
index 66655537..849d2571 100644
--- a/crates/aiken-lang/src/tipo/error.rs
+++ b/crates/aiken-lang/src/tipo/error.rs
@@ -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")]
diff --git a/crates/aiken-lang/src/tipo/infer.rs b/crates/aiken-lang/src/tipo/infer.rs
index d69ef03e..6f59bd96 100644
--- a/crates/aiken-lang/src/tipo/infer.rs
+++ b/crates/aiken-lang/src/tipo/infer.rs
@@ -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 {