Add check to ensure generics for sorts are correct

crates/flux-fhir-analysis/locales/en-US.ftl

@@ -3,7 +3,6 @@
 fhir_analysis_sort_mismatch =
     mismatched sorts
     .label = expected `{$expected}`, found `{$found}`
-
 fhir_analysis_arg_count_mismatch =
     this {$thing} takes {$expected ->
         [one] {$expected} refinement argument
@@ -201,9 +200,45 @@ fhir_analysis_too_many_generic_args =
         *[other] arguments
     }
 
+fhir_analysis_generics_on_primitive_sort = 
+    primitive sort {$name} expects {$expected -> 
+        [0] no generics
+        [one] exactly one generic argument
+        *[other] exactly {$expected} generic arguments
+    } but found {$found}
+    .label = incorrect generics on primitive sort
+
+fhir_analysis_too_many_generics_on_sort =
+    sorts associated with this {$def_descr} should have {$max ->  
+        [0] no generic arguments
+        [one] at most one generic argument
+        *[other] at most {$max} generic arguments
+    } but {$found} generic {$found ->
+        [one] argument
+        *[other] arguments
+    } supplied
+    .label = expected {$max ->
+        [0] no generic arguments
+        [one] at most one generic argument
+        *[other] at most {$max} generic arguments
+    } on sort
+
+fhir_analysis_generics_on_type_parameter = 
+    type parameter expects no generics but found {$found}
+    .label = found generics on sort type parameter
+
+fhir_analysis_generics_on_self_alias = 
+    type alias Self expects no generics but found {$found}
+    .label = found generics on type `Self`
+
+fhir_analysis_generics_on_opaque_sort = 
+    user defined opaque sorts have no generics but found {$found}
+    .label = found generics on user defined opaque sort
+
 fhir_analysis_refined_unrefinable_type =
     type cannot be refined
 
+
 # Check impl against trait errors
 
 fhir_analysis_incompatible_sort =

crates/flux-fhir-analysis/src/conv/mod.rs

@@ -1961,24 +1961,93 @@
     next_infer_sort: &mut impl FnMut() -> rty::Sort,
 ) -> QueryResult<rty::Sort> {
     let ctor = match path.res {
-        fhir::SortRes::PrimSort(fhir::PrimSort::Int) => return Ok(rty::Sort::Int),
-        fhir::SortRes::PrimSort(fhir::PrimSort::Bool) => return Ok(rty::Sort::Bool),
-        fhir::SortRes::PrimSort(fhir::PrimSort::Real) => return Ok(rty::Sort::Real),
+        fhir::SortRes::PrimSort(fhir::PrimSort::Int) => {
+            if !path.args.is_empty() {
+                return Err(emit_prim_sort_generics_error(genv, path, "int", 0))?;
+            }
+            return Ok(rty::Sort::Int);
+        }
+        fhir::SortRes::PrimSort(fhir::PrimSort::Bool) => {
+            if !path.args.is_empty() {
+                return Err(emit_prim_sort_generics_error(genv, path, "bool", 0))?;
+            }
+            return Ok(rty::Sort::Bool);
+        }
+        fhir::SortRes::PrimSort(fhir::PrimSort::Real) => {
+            if !path.args.is_empty() {
+                return Err(emit_prim_sort_generics_error(genv, path, "real", 0))?;
+            }
+            return Ok(rty::Sort::Real);
+        }
         fhir::SortRes::SortParam(n) => return Ok(rty::Sort::Var(rty::ParamSort::from(n))),
         fhir::SortRes::TyParam(def_id) => {
-            return Ok(rty::Sort::Param(def_id_to_param_ty(genv, def_id)))
+            if !path.args.is_empty() {
+                let err = errors::GenericsOnTyParam::new(
+                    path.segments.last().unwrap().span,
+                    path.args.len(),
+                );
+                return Err(genv.sess().emit_err(err))?;
+            }
+            return Ok(rty::Sort::Param(def_id_to_param_ty(genv, def_id)));
+        }
+        fhir::SortRes::SelfParam { .. } => {
+            if !path.args.is_empty() {
+                let err = errors::GenericsOnSelf::new(
+                    path.segments.last().unwrap().span,
+                    path.args.len(),
+                );
+                return Err(genv.sess().emit_err(err))?;
+            }
+            return Ok(rty::Sort::Param(rty::SELF_PARAM_TY));
         }
-        fhir::SortRes::SelfParam { .. } => return Ok(rty::Sort::Param(rty::SELF_PARAM_TY)),
         fhir::SortRes::SelfAlias { alias_to } => {
+            if !path.args.is_empty() {
+                let err = errors::GenericsOnSelf::new(
+                    path.segments.last().unwrap().span,
+                    path.args.len(),
+                );
+                return Err(genv.sess().emit_err(err))?;
+            }
             return Ok(genv
                 .sort_of_self_ty_alias(alias_to)?
-                .unwrap_or(rty::Sort::Err))
+                .unwrap_or(rty::Sort::Err));
+        }
+        fhir::SortRes::PrimSort(fhir::PrimSort::Set) => {
+            if path.args.len() != 1 {
+                // Has to have one argument
+                return Err(emit_prim_sort_generics_error(genv, path, "Set", 1))?;
+            }
+            rty::SortCtor::Set
+        }
+        fhir::SortRes::PrimSort(fhir::PrimSort::Map) => {
+            if path.args.len() != 2 {
+                // Has to have two arguments
+                return Err(emit_prim_sort_generics_error(genv, path, "Map", 2))?;
+            }
+            rty::SortCtor::Map
+        }
+        fhir::SortRes::User { name } => {
+            if !path.args.is_empty() {
+                let err = errors::GenericsOnUserDefinedOpaqueSort::new(
+                    path.segments.last().unwrap().span,
+                    path.args.len(),
+                );
+                return Err(genv.sess().emit_err(err))?;
+            }
+            rty::SortCtor::User { name }
         }
-        fhir::SortRes::PrimSort(fhir::PrimSort::Set) => rty::SortCtor::Set,
-        fhir::SortRes::PrimSort(fhir::PrimSort::Map) => rty::SortCtor::Map,
-        fhir::SortRes::User { name } => rty::SortCtor::User { name },
         fhir::SortRes::Adt(def_id) => {
             let sort_def = genv.adt_sort_def_of(def_id)?;
+            if path.args.len() > sort_def.param_count() {
+                let err = errors::TooManyGenericsOnSort::new(
+                    genv,
+                    def_id,
+                    path.segments.last().unwrap().span,
+                    path.args.len(),
+                    sort_def.param_count(),
+                );
+                return Err(genv.sess().emit_err(err))?;
+            }
             rty::SortCtor::Adt(sort_def)
         }
     };
@@ -1987,9 +2056,25 @@
         .iter()
         .map(|t| conv_sort(genv, t, next_infer_sort))
         .try_collect()?;
+
     Ok(rty::Sort::app(ctor, args))
 }
 
+fn emit_prim_sort_generics_error(
+    genv: GlobalEnv,
+    path: &fhir::SortPath,
+    name: &'static str,
+    expected: usize,
+) -> ErrorGuaranteed {
+    let err = errors::GenericsOnPrimitiveSort::new(
+        path.segments.last().unwrap().span,
+        name,
+        path.args.len(),
+        expected,
+    );
+    genv.sess().emit_err(err)
+}
+
 fn conv_poly_func_sort(
     genv: GlobalEnv,
     sort: &fhir::PolyFuncSort,
@@ -2192,4 +2277,89 @@
             Self { span }
         }
     }
+
+    #[derive(Diagnostic)]
+    #[diag(fhir_analysis_generics_on_primitive_sort, code = E0999)]
+    pub(super) struct GenericsOnPrimitiveSort {
+        #[primary_span]
+        #[label]
+        span: Span,
+        name: &'static str,
+        found: usize,
+        expected: usize,
+    }
+
+    impl GenericsOnPrimitiveSort {
+        pub(super) fn new(span: Span, name: &'static str, found: usize, expected: usize) -> Self {
+            Self { span, found, expected, name }
+        }
+    }
+
+    #[derive(Diagnostic)]
+    #[diag(fhir_analysis_too_many_generics_on_sort, code = E0999)]
+    pub(super) struct TooManyGenericsOnSort {
+        #[primary_span]
+        #[label]
+        span: Span,
+        found: usize,
+        max: usize,
+        def_descr: &'static str,
+    }
+
+    impl TooManyGenericsOnSort {
+        pub(super) fn new(
+            genv: GlobalEnv,
+            def_id: DefId,
+            span: Span,
+            found: usize,
+            max: usize,
+        ) -> Self {
+            Self { span, found, max, def_descr: genv.tcx().def_descr(def_id) }
+        }
+    }
+
+    #[derive(Diagnostic)]
+    #[diag(fhir_analysis_generics_on_type_parameter, code = E0999)]
+    pub(super) struct GenericsOnTyParam {
+        #[primary_span]
+        #[label]
+        span: Span,
+        found: usize,
+    }
+
+    impl GenericsOnTyParam {
+        pub(super) fn new(span: Span, found: usize) -> Self {
+            Self { span, found }
+        }
+    }
+
+    #[derive(Diagnostic)]
+    #[diag(fhir_analysis_generics_on_self_alias, code = E0999)]
+    pub(super) struct GenericsOnSelf {
+        #[primary_span]
+        #[label]
+        span: Span,
+        found: usize,
+    }
+
+    impl GenericsOnSelf {
+        pub(super) fn new(span: Span, found: usize) -> Self {
+            Self { span, found }
+        }
+    }
+
+    #[derive(Diagnostic)]
+    #[diag(fhir_analysis_generics_on_opaque_sort, code = E0999)]
+    pub(super) struct GenericsOnUserDefinedOpaqueSort {
+        #[primary_span]
+        #[label]
+        span: Span,
+        found: usize,
+    }
+
+    impl GenericsOnUserDefinedOpaqueSort {
+        pub(super) fn new(span: Span, found: usize) -> Self {
+            Self { span, found }
+        }
+    }
 }

crates/flux-middle/src/rty/mod.rs

@@ -141,6 +141,11 @@ impl AdtSortDef {
             .map(|i| Sort::Var(ParamSort::from(i)))
             .collect()
     }
+
+    /// Gives the number of sort variables bound by this definition.
+    pub fn param_count(&self) -> usize {
+        self.0.params.len()
+    }
 }
 
 #[derive(Debug, Clone, Default, Encodable, Decodable)]

tests/tests/neg/error_messages/conv/mismatched_generics.rs

@@ -0,0 +1,54 @@
+use flux_rs::*;
+
+#[refined_by(n: int)]
+struct S {
+    #[field(i32[n])]
+    f: i32,
+}
+
+defs! {
+    fn foo(s: S<int>) -> int { //~ Error sorts associated with this struct should have no generic arguments but 1 generic argument supplied
+        s.n
+    }
+
+    fn foo2(x: int<bool>) -> int { //~ Error primitive sort int expects no generics but found 1
+        1
+    }
+
+    fn foo3(x: Map<int>) -> int { //~ Error primitive sort Map expects exactly 2 generic arguments but found 1
+        1
+    } 
+
+    fn foo4(x: Map) -> int { //~ Error primitive sort Map expects exactly 2 generic arguments but found 0
+        1
+    }
+
+    fn foo5(x: Set<int, int>) -> int { //~ Error primitive sort Set expects exactly one generic argument but found 2
+        1
+    }
+
+    fn foo6(x: real<bool>) -> real { //~ Error primitive sort real expects no generics but found 1
+        1
+    }
+
+    fn foo7(x: bool<int>) -> real { //~ Error primitive sort bool expects no generics but found 1
+        1
+    }
+}
+
+#[flux::refined_by(f: T<int>)] //~ Error type parameter expects no generics but found 1
+struct X<T> { 
+    #[flux::field(T[f])]
+    f: T 
+}
+
+#[flux::assoc(fn foo(x: Self<int>) -> int)] //~ Error type alias Self expects no generics but found 1
+trait MyTrait {}
+
+flux_rs::defs! {
+    opaque sort MyOpaqueSort;
+}
+
+#[flux_rs::opaque]
+#[flux_rs::refined_by(f: MyOpaqueSort<int>)] //~ Error user defined opaque sorts have no generics but found 1
+struct Y {}