Add test for unsound generalization

And fix the error expectation for `TypecheckError::VarLevelMismatch` that still had the old longer name `VariableLevelMismatch`.
tweag · Jul 24, 2023 · d7294e9 · d7294e9
1 parent 3649a12
commit d7294e9
Show file tree

Hide file tree

Showing 6 changed files with 39 additions and 9 deletions.
diff --git a/core/tests/integration/main.rs b/core/tests/integration/main.rs
@@ -163,10 +163,12 @@ enum ErrorExpectation {
     TypecheckExtraDynTail,
     #[serde(rename = "TypecheckError::MissingDynTail")]
     TypecheckMissingDynTail,
+    #[serde(rename = "TypecheckError::ArrowTypeMismatch")]
+    TypecheckArrowTypeMismatch { sub_error: Box<ErrorExpectation> },
     #[serde(rename = "TypecheckError::FlatTypeInTermPosition")]
     TypecheckFlatTypeInTermPosition,
-    #[serde(rename = "TypecheckError::VariableLevelMismatch")]
-    TypecheckVariableLevelMismatch { type_var: String },
+    #[serde(rename = "TypecheckError::VarLevelMismatch")]
+    TypecheckVarLevelMismatch { type_var: String },
     #[serde(rename = "ParseError")]
     AnyParseError,
     #[serde(rename = "ParseError::DuplicateIdentInRecordPattern")]
@@ -287,11 +289,20 @@ impl PartialEq<Error> for ErrorExpectation {
                 _ => false,
             },
             (
-                TypecheckVariableLevelMismatch { type_var: ident },
+                TypecheckVarLevelMismatch { type_var: ident },
                 Error::TypecheckError(TypecheckError::VarLevelMismatch {
                     type_var: constant, ..
                 }),
             ) => ident == constant.label(),
+            // The clone is not ideal, but currently we can't compare `TypecheckError` directly
+            // with an ErrorExpectation. Ideally, we would implement `eq` for all error subtypes,
+            // and have the eq with `Error` just dipsatch to those sub-eq functions.
+            (
+                TypecheckArrowTypeMismatch {
+                    sub_error: sub_error1,
+                },
+                Error::TypecheckError(TypecheckError::ArrowTypeMismatch(_, _, _, sub_error2, _)),
+            ) => sub_error1.as_ref() == &Error::TypecheckError((**sub_error2).clone()),
             (_, _) => false,
         }
     }
@@ -352,9 +363,12 @@ impl std::fmt::Display for ErrorExpectation {
             }
             TypecheckExtraDynTail => "TypecheckError::ExtraDynTail".to_owned(),
             TypecheckMissingDynTail => "TypecheckError::MissingDynTail".to_owned(),
+            TypecheckArrowTypeMismatch { sub_error } => {
+                format!("TypecheckError::ArrowTypeMismatch{sub_error})")
+            }
             TypecheckFlatTypeInTermPosition => "TypecheckError::FlatTypeInTermPosition".to_owned(),
-            TypecheckVariableLevelMismatch { type_var: ident } => {
-                format!("TypecheckError::VariableLevelMismatch({ident})")
+            TypecheckVarLevelMismatch { type_var: ident } => {
+                format!("TypecheckError::VarLevelMismatch({ident})")
             }
             SerializeNumberOutOfRange => "ExportError::NumberOutOfRange".to_owned(),
         };

diff --git a/core/tests/integration/typecheck/fail/unsound_generalization_enum_rows.ncl b/core/tests/integration/typecheck/fail/unsound_generalization_enum_rows.ncl
@@ -2,7 +2,7 @@
 # eval = 'typecheck'
 #
 # [test.metadata]
-# error = 'TypecheckError::VariableLevelMismatch'
+# error = 'TypecheckError::VarLevelMismatch'
 #
 # [test.metadata.expectation]
 # type_var = 'tail'

diff --git a/core/tests/integration/typecheck/fail/unsound_generalization_fun.ncl b/core/tests/integration/typecheck/fail/unsound_generalization_fun.ncl
@@ -2,7 +2,7 @@
 # eval = 'typecheck'
 #
 # [test.metadata]
-# error = 'TypecheckError::VariableLevelMismatch'
+# error = 'TypecheckError::VarLevelMismatch'
 #
 # [test.metadata.expectation]
 # type_var = 'c'

diff --git a/core/tests/integration/typecheck/fail/unsound_generalization_monomorphic_id.ncl b/core/tests/integration/typecheck/fail/unsound_generalization_monomorphic_id.ncl
@@ -0,0 +1,16 @@
+# test.type = 'error'
+# eval = 'typecheck'
+# 
+# [test.metadata]
+# error = 'TypecheckError::ArrowTypeMismatch'
+#
+# [test.metadata.expectation.sub_error]
+# error = 'TypecheckError::VarLevelMismatch'
+#
+# [test.metadata.expectation.sub_error.expectation]
+# type_var = 'b'
+(let eval : forall a. (forall b. b -> b) -> a -> a = fun f x => f x
+# because g isn't annotated, it doesn't get a polymorphic type, but a
+# monomorphic _a -> _a
+in let g = fun x => x
+in eval g) : _
diff --git a/core/tests/integration/typecheck/fail/unsound_generalization_record_rows.ncl b/core/tests/integration/typecheck/fail/unsound_generalization_record_rows.ncl
@@ -2,7 +2,7 @@
 # eval = 'typecheck'
 #
 # [test.metadata]
-# error = 'TypecheckError::VariableLevelMismatch'
+# error = 'TypecheckError::VarLevelMismatch'
 #
 # [test.metadata.expectation]
 # type_var = 'tail'

diff --git a/core/tests/integration/typecheck/fail/unsound_generalization_simple.ncl b/core/tests/integration/typecheck/fail/unsound_generalization_simple.ncl
@@ -2,7 +2,7 @@
 # eval = 'typecheck'
 #
 # [test.metadata]
-# error = 'TypecheckError::VariableLevelMismatch'
+# error = 'TypecheckError::VarLevelMismatch'
 #
 # [test.metadata.expectation]
 # type_var = 'a'