Strengthen check for inference type loops

compiler/qsc/src/interpret/tests.rs

@@ -2230,5 +2230,44 @@ mod given_interpreter {
                 "#]],
             );
         }
+
+        /// Found via fuzzing, see #2426 <https://github.com/microsoft/qsharp/issues/2426>
+        #[test]
+        fn recursive_type_constraint_should_fail() {
+            let sources = SourceMap::new(
+                [(
+                    "test".into(),
+                    r#"operation a(){(foo,bar)->foo+bar=foo->foo"#.into(),
+                )],
+                None,
+            );
+            let (std_id, store) =
+                crate::compile::package_store_with_stdlib(TargetCapabilityFlags::all());
+            match Interpreter::new(
+                sources,
+                PackageType::Lib,
+                TargetCapabilityFlags::all(),
+                LanguageFeatures::default(),
+                store,
+                &[(std_id, None)],
+            ) {
+                Ok(_) => panic!("interpreter should fail with error"),
+                Err(errors) => {
+                    is_error(
+                        &errors,
+                        &expect![[r#"
+                            syntax error: expected `:`, found `{`
+                               [test] [{]
+                            syntax error: expected `}`, found EOF
+                               [test] []
+                            type error: unsupported recursive type constraint
+                               [test] [(foo,bar)->foo+bar]
+                            type error: insufficient type information to infer type
+                               [test] [foo+bar]
+                        "#]],
+                    );
+                }
+            }
+        }
     }
 }

compiler/qsc_frontend/src/typeck.rs

@@ -182,6 +182,12 @@ enum ErrorKind {
     ))]
     #[diagnostic(code("Qsc.TypeCk.TySizeLimitExceeded"))]
     TySizeLimitExceeded(String, #[label] Span),
+    #[error("unsupported recursive type constraint")]
+    #[diagnostic(help(
+        "try using explicit type annotations to avoid this recursive constraint in type inference"
+    ))]
+    #[diagnostic(code("Qsc.TypeCk.RecursiveTypeConstraint"))]
+    RecursiveTypeConstraint(#[label] Span),
 }
 
 impl From<TyConversionError> for Error {

compiler/qsc_frontend/src/typeck/infer.rs

@@ -752,7 +752,7 @@ impl Solver {
                 constraints
             }
             (Ty::Infer(infer1), Ty::Infer(infer2)) if infer1 == infer2 => Vec::new(),
-            (&Ty::Infer(infer), ty) | (ty, &Ty::Infer(infer)) if !contains_infer_ty(infer, ty) => {
+            (&Ty::Infer(infer), ty) | (ty, &Ty::Infer(infer)) => {
                 self.bind_ty(infer, ty.clone(), span)
             }
             (
@@ -822,6 +822,10 @@ impl Solver {
             self.errors
                 .push(Error(ErrorKind::TySizeLimitExceeded(ty.display(), span)));
             return Vec::new();
+        } else if links_to_infer_ty(&self.solution.tys, infer, &ty) {
+            self.errors
+                .push(Error(ErrorKind::RecursiveTypeConstraint(span)));
+            return Vec::new();
         }
         self.solution.tys.insert(infer, ty.clone());
         let mut constraint = vec![Constraint::Eq {
@@ -970,16 +974,28 @@ fn unknown_ty(solved_types: &IndexMap<InferTyId, Ty>, given_type: &Ty) -> Option
     }
 }
 
-fn contains_infer_ty(id: InferTyId, ty: &Ty) -> bool {
+/// Checks whether the given inference type is eventually pointed to by the given type,
+/// indicating a recursive type constraint.
+fn links_to_infer_ty(solution_tys: &IndexMap<InferTyId, Ty>, id: InferTyId, ty: &Ty) -> bool {
     match ty {
         Ty::Err | Ty::Param { .. } | Ty::Prim(_) | Ty::Udt(_, _) => false,
-        Ty::Array(item) => contains_infer_ty(id, item),
+        Ty::Array(item) => links_to_infer_ty(solution_tys, id, item),
         Ty::Arrow(arrow) => {
-            contains_infer_ty(id, &arrow.input.borrow())
-                || contains_infer_ty(id, &arrow.output.borrow())
+            links_to_infer_ty(solution_tys, id, &arrow.input.borrow())
+                || links_to_infer_ty(solution_tys, id, &arrow.output.borrow())
         }
-        Ty::Infer(other_id) => id == *other_id,
-        Ty::Tuple(items) => items.iter().any(|ty| contains_infer_ty(id, ty)),
+        Ty::Infer(other_id) => {
+            // if the other id is the same as the one we are checking, then this is a recursive type
+            id == *other_id
+                // OR if the other id is in the solutions tys, we need to continue the check
+                // through the pointed to type.
+                || solution_tys
+                    .get(*other_id)
+                    .is_some_and(|ty| links_to_infer_ty(solution_tys, id, ty))
+        }
+        Ty::Tuple(items) => items
+            .iter()
+            .any(|ty| links_to_infer_ty(solution_tys, id, ty)),
     }
 }
 

compiler/qsc_frontend/src/typeck/tests.rs

@@ -3209,7 +3209,7 @@ fn infinite() {
             }
         "},
         "",
-        &expect![[r#"
+        &expect![[r##"
             #6 30-32 "()" : Unit
             #8 38-97 "{\n        let x = invalid;\n        let xs = [x, [x]];\n    }" : Unit
             #10 52-53 "x" : ?0
@@ -3220,9 +3220,9 @@ fn infinite() {
             #22 86-89 "[x]" : ?0[]
             #23 87-88 "x" : ?0
             Error(Resolve(NotFound("invalid", Span { lo: 56, hi: 63 })))
-            Error(Type(Error(TyMismatch("?", "?[]", Span { lo: 86, hi: 89 }))))
+            Error(Type(Error(RecursiveTypeConstraint(Span { lo: 86, hi: 89 }))))
             Error(Type(Error(AmbiguousTy(Span { lo: 52, hi: 53 }))))
-        "#]],
+        "##]],
     );
 }
 
@@ -4401,12 +4401,16 @@ fn inference_infinite_recursion_should_fail() {
             #27 102-125 "y : (('T2, 'U2) -> 'T2)" : ((Param<"'T2": 0>, Param<"'U2": 1>) -> Param<"'T2": 0>)
             #40 133-140 "{\n    }" : Unit
             #44 161-163 "()" : Unit
-            #48 170-193 "{\n        A and B\n    }" : (((?1[][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][], ?3) -> ?1[][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][]) -> ?1[][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][])
-            #50 180-187 "A and B" : (((?1[][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][], ?3) -> ?1[][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][]) -> ?1[][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][])
-            #51 180-181 "A" : (((?1[][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][], ?3) -> ?1[][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][]) -> ?1[][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][])
-            #54 186-187 "B" : (((?1[][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][], ?3) -> ?1[][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][]) -> ?2[][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][])
+            #48 170-193 "{\n        A and B\n    }" : (((?2, ?3) -> ?2) -> ?2[])
+            #50 180-187 "A and B" : (((?2, ?3) -> ?2) -> ?2[])
+            #51 180-181 "A" : (((?2, ?3) -> ?2) -> ?2[])
+            #54 186-187 "B" : (((?2, ?3) -> ?2) -> ?2)
             Error(Type(Error(TyMismatch("Unit", "'U1[]", Span { lo: 62, hi: 67 }))))
             Error(Type(Error(TyMismatch("Unit", "'T2", Span { lo: 129, hi: 132 }))))
+            Error(Type(Error(RecursiveTypeConstraint(Span { lo: 186, hi: 187 }))))
+            Error(Type(Error(TyMismatch("Bool", "(((?, ?) -> ?) -> ?[])", Span { lo: 180, hi: 181 }))))
+            Error(Type(Error(TyMismatch("Unit", "(((?, ?) -> ?) -> ?[])", Span { lo: 180, hi: 187 }))))
+            Error(Type(Error(AmbiguousTy(Span { lo: 186, hi: 187 }))))
             Error(Type(Error(AmbiguousTy(Span { lo: 186, hi: 187 }))))
         "##]],
     );