From a74c07c97bebab3639c35fa26835c72638ff68e8 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Thu, 31 Oct 2024 14:50:16 -0300 Subject: [PATCH 01/13] Introduce DeclatedType --- pil-analyzer/src/pil_analyzer.rs | 29 ++++--- pil-analyzer/src/type_inference.rs | 128 ++++++++++++++++++++--------- 2 files changed, 107 insertions(+), 50 deletions(-) diff --git a/pil-analyzer/src/pil_analyzer.rs b/pil-analyzer/src/pil_analyzer.rs index 8b141328b5..fab2b56053 100644 --- a/pil-analyzer/src/pil_analyzer.rs +++ b/pil-analyzer/src/pil_analyzer.rs @@ -14,7 +14,7 @@ use powdr_ast::parsed::asm::{ use powdr_ast::parsed::types::Type; use powdr_ast::parsed::visitor::{AllChildren, Children}; use powdr_ast::parsed::{ - self, FunctionKind, LambdaExpression, PILFile, PilStatement, SymbolCategory, + self, FunctionKind, LambdaExpression, PILFile, PilStatement, SourceReference, SymbolCategory, TraitImplementation, TypedExpression, }; use powdr_number::{FieldElement, GoldilocksField}; @@ -29,7 +29,7 @@ use powdr_parser_util::Error; use crate::traits_resolver::TraitsResolver; use crate::type_builtins::constr_function_statement_type; -use crate::type_inference::infer_types; +use crate::type_inference::{infer_types, DeclaredType}; use crate::{side_effect_checker, AnalysisDriver}; use crate::statement_processor::{Counters, PILItem, StatementProcessor}; @@ -303,19 +303,21 @@ impl PILAnalyzer { ) }) .flat_map(|(name, (symbol, value))| { - let (type_scheme, expr) = match (symbol.kind, value) { + let (declared_type, expr) = match (symbol.kind, value) { (SymbolKind::Poly(PolynomialType::Committed), Some(value)) => { // Witness column, move its value (query function) into the expressions to be checked separately. - let type_scheme = type_from_definition(symbol, &None); let FunctionValueDefinition::Expression(TypedExpression { e, .. }) = value else { panic!("Invalid value for query function") }; - + let source = e.source_reference().clone(); expressions.push((e, query_type.clone().into())); - (type_scheme, None) + let declared_type = type_from_definition(symbol, &None) + .map(|ts| ts.into()) + .map(|dec: DeclaredType| dec.with_source(source)); + (declared_type, None) } ( _, @@ -323,19 +325,26 @@ impl PILAnalyzer { type_scheme, e, })), - ) => (type_scheme.clone(), Some(e)), + ) => { + let source = e.source_reference(); + let declared_type = type_scheme + .clone() + .map(|ts| ts.into()) + .map(|dec: DeclaredType| dec.with_source(source.clone())); + (declared_type, Some(e)) + } (_, value) => { - let type_scheme = type_from_definition(symbol, value); + let declared_type = type_from_definition(symbol, value).map(|ts| ts.into()); if let Some(FunctionValueDefinition::Array(items)) = value { // Expect all items in the arrays to be field elements. expressions.extend(items.children_mut().map(|e| (e, Type::Fe.into()))); } - (type_scheme, None) + (declared_type, None) } }; - Some((name.clone(), (type_scheme, expr))) + Some((name.clone(), (declared_type, expr))) }) .collect(); for expr in &mut self.proof_items { diff --git a/pil-analyzer/src/type_inference.rs b/pil-analyzer/src/type_inference.rs index 82ee2c8a47..0450aa815e 100644 --- a/pil-analyzer/src/type_inference.rs +++ b/pil-analyzer/src/type_inference.rs @@ -29,7 +29,7 @@ use crate::{ /// Sets the generic arguments for references and the literal types in all expressions. /// Returns the types for symbols without explicit type. pub fn infer_types( - definitions: HashMap, Option<&mut Expression>)>, + definitions: HashMap, Option<&mut Expression>)>, expressions: &mut [(&mut Expression, ExpectedType)], ) -> Result, Vec> { TypeChecker::new().infer_types(definitions, expressions) @@ -60,13 +60,60 @@ impl From for ExpectedType { } } +#[derive(Debug, Clone)] +pub struct DeclaredType { + pub source: SourceRef, + pub vars: TypeBounds, + pub ty: DeclaredTypeKind, +} + +impl DeclaredType { + fn scheme(&self) -> TypeScheme { + match &self.ty { + DeclaredTypeKind::Struct(ty, _) | DeclaredTypeKind::Type(ty) => TypeScheme { + vars: self.vars.clone(), + ty: ty.clone(), + }, + } + } + + fn type_mut(&mut self) -> &mut Type { + match &mut self.ty { + DeclaredTypeKind::Struct(ty, _) => ty, + DeclaredTypeKind::Type(ty) => ty, + } + } + + pub fn with_source(mut self, source: SourceRef) -> Self { + self.source = source; + self + } +} + +#[derive(Debug, Clone)] +pub enum DeclaredTypeKind { + #[allow(dead_code)] // Remove when #1910 is merged + Struct(Type, HashMap), + Type(Type), +} + +impl From for DeclaredType { + fn from(scheme: TypeScheme) -> Self { + Self { + source: SourceRef::unknown(), + vars: scheme.vars.clone(), + ty: DeclaredTypeKind::Type(scheme.ty.clone()), + } + } +} + struct TypeChecker { /// Types for local variables, might contain type variables. local_var_types: Vec, /// Declared types for all symbols and their source references. /// Contains the unmodified type scheme for symbols with generic types and newly /// created type variables for symbols without declared type. - declared_types: HashMap, + declared_types: HashMap, /// Current mapping of declared type vars to type. Reset before checking each definition. declared_type_vars: HashMap, unifier: Unifier, @@ -89,7 +136,7 @@ impl TypeChecker { /// returns the types for symbols without explicit type. pub fn infer_types( mut self, - mut definitions: HashMap, Option<&mut Expression>)>, + mut definitions: HashMap, Option<&mut Expression>)>, expressions: &mut [(&mut Expression, ExpectedType)], ) -> Result, Vec> { let type_var_mapping = self @@ -100,11 +147,11 @@ impl TypeChecker { .into_iter() .filter(|(_, (ty, _))| ty.is_none()) .map(|(name, _)| { - let (_, mut scheme) = self.declared_types.remove(&name).unwrap(); - assert!(scheme.vars.is_empty()); - self.substitute(&mut scheme.ty); - assert!(scheme.ty.is_concrete_type()); - (name, scheme.ty) + let mut declared_type = self.declared_types.remove(&name).unwrap(); + assert!(declared_type.vars.is_empty()); + self.substitute(declared_type.type_mut()); + assert!(declared_type.scheme().ty.is_concrete_type()); + (name, declared_type.scheme().ty) }) .collect()) } @@ -113,7 +160,7 @@ impl TypeChecker { /// the type variables used by the type checker to those used in the declaration. fn infer_types_inner( &mut self, - definitions: &mut HashMap, Option<&mut Expression>)>, + definitions: &mut HashMap, Option<&mut Expression>)>, expressions: &mut [(&mut Expression, ExpectedType)], ) -> Result>, Error> { // TODO in order to fix type inference on recursive functions, we need to: @@ -145,10 +192,10 @@ impl TypeChecker { continue; }; - let (_, declared_type) = self.declared_types[&name].clone(); + let declared_type = self.declared_types[&name].clone(); if declared_type.vars.is_empty() { self.declared_type_vars.clear(); - self.process_concrete_symbol(declared_type.ty.clone(), value)?; + self.process_concrete_symbol(declared_type.scheme().ty.clone(), value)?; } else { self.declared_type_vars = declared_type .vars @@ -168,13 +215,13 @@ impl TypeChecker { // Now we check for all symbols that are not declared as a type scheme that they // can resolve to a concrete type. - for (name, (source_ref, declared_type)) in &self.declared_types { + for (name, declared_type) in &self.declared_types { if declared_type.vars.is_empty() { // It is not a type scheme, see if we were able to derive a concrete type. - let inferred = self.type_into_substituted(declared_type.ty.clone()); + let inferred = self.type_into_substituted(declared_type.scheme().ty.clone()); if !inferred.is_concrete_type() { let inferred_scheme = self.to_type_scheme(inferred); - return Err(source_ref.with_error( + return Err(declared_type.source.with_error( format!( "Could not derive a concrete type for symbol {name}.\nInferred type scheme: {}\n", format_type_scheme_around_name( @@ -197,38 +244,39 @@ impl TypeChecker { /// Fills self.declared_types and checks that declared builtins have the correct type. fn setup_declared_types( &mut self, - definitions: &mut HashMap, Option<&mut Expression>)>, + definitions: &mut HashMap, Option<&mut Expression>)>, ) { // Add types from declarations. Type schemes are added without instantiating. self.declared_types = definitions .iter() - .map(|(name, (type_scheme, value))| { - let source_ref = value - .as_ref() - .map(|v| v.source_reference()) - .cloned() - .unwrap_or_default(); - // Check if it is a builtin symbol. - let ty = match (builtin_schemes().get(name), type_scheme) { + .map(|(name, (declared_type, _))| { + let declared_type = match (builtin_schemes().get(name), declared_type) { (Some(builtin), declared) => { - if let Some(declared) = declared { + if let Some(declared_inner) = declared { + let declared_scheme = declared_inner.scheme(); assert_eq!( - builtin, - declared, + *builtin, + declared_scheme, "Invalid type for built-in scheme. Got {} but expected {}", - format_type_scheme_around_name(name, &Some(declared.clone())), + format_type_scheme_around_name( + name, + &Some(declared_scheme.clone()) + ), format_type_scheme_around_name(name, &Some(builtin.clone())) ); }; - builtin.clone() + builtin.clone().into() } // Store an (uninstantiated) type scheme for symbols with a declared polymorphic type. - (None, Some(type_scheme)) => type_scheme.clone(), + (None, Some(declared_type)) => declared_type.clone(), // Store a new (unquantified) type variable for symbols without declared type. // This forces a single concrete type for them. - (None, None) => self.unifier.new_type_var().into(), + (None, None) => { + let scheme: TypeScheme = self.unifier.new_type_var().into(); + scheme.into() + } }; - (name.clone(), (source_ref, ty)) + (name.clone(), declared_type) }) .collect(); @@ -237,7 +285,7 @@ impl TypeChecker { for (name, scheme) in builtin_schemes() { self.declared_types .entry(name.clone()) - .or_insert_with(|| (SourceRef::unknown(), scheme.clone())); + .or_insert_with(|| Into::::into(scheme.clone())); definitions.remove(name); } } @@ -327,7 +375,7 @@ impl TypeChecker { /// the type variable names used by the type checker to those from the declaration. fn update_type_args( &mut self, - definitions: &mut HashMap, Option<&mut Expression>)>, + definitions: &mut HashMap, Option<&mut Expression>)>, expressions: &mut [(&mut Expression, ExpectedType)], type_var_mapping: &HashMap>, ) -> Result<(), Vec> { @@ -523,7 +571,7 @@ impl TypeChecker { ) => { let (ty, args) = self .unifier - .instantiate_scheme(self.declared_types[name].1.clone()); + .instantiate_scheme(self.declared_types[name].scheme().clone()); if let Some(requested_type_args) = type_args { if requested_type_args.len() != args.len() { return Err(source_ref.with_error(format!( @@ -858,7 +906,7 @@ impl TypeChecker { // is not helpful because the type is obvious from the value. let (ty, _generic_args) = self .unifier - .instantiate_scheme(self.declared_types[&name.to_string()].1.clone()); + .instantiate_scheme(self.declared_types[&name.to_string()].scheme().clone()); let ty = type_for_reference(&ty); match data { @@ -913,18 +961,18 @@ impl TypeChecker { inferred_types: HashMap, ) -> Result>, Error> { inferred_types.into_iter().map(|(name, inferred_type)| { - let (source_ref, declared_type) = self.declared_types[&name].clone(); + let declared_type = self.declared_types[&name].clone(); let inferred_type = self.type_into_substituted(inferred_type.clone()); let inferred = self.to_type_scheme(inferred_type.clone()); - let declared = declared_type.clone().simplify_type_vars(); + let declared = declared_type.scheme().clone().simplify_type_vars(); if inferred != declared { - return Err(source_ref.with_error(format!( + return Err(declared_type.source.with_error(format!( "Inferred type scheme for symbol {name} does not match the declared type.\nInferred: let{}\nDeclared: let{}", format_type_scheme_around_name(&name, &Some(inferred)), - format_type_scheme_around_name(&name, &Some(declared_type), + format_type_scheme_around_name(&name, &Some(declared), )))); } - let declared_type_vars = declared_type.ty.contained_type_vars(); + let declared_type_vars = declared.ty.contained_type_vars(); let inferred_type_vars = inferred_type.contained_type_vars(); Ok((name.clone(), inferred_type_vars From 611a4fb2b856aff6db25fdf0d8b953c64bb057eb Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Fri, 1 Nov 2024 10:57:47 -0300 Subject: [PATCH 02/13] Fix introduced bug in verify_type_scheme --- pil-analyzer/src/type_inference.rs | 35 ++++++++++++++++++++++-------- 1 file changed, 26 insertions(+), 9 deletions(-) diff --git a/pil-analyzer/src/type_inference.rs b/pil-analyzer/src/type_inference.rs index 0450aa815e..3b455d500b 100644 --- a/pil-analyzer/src/type_inference.rs +++ b/pil-analyzer/src/type_inference.rs @@ -84,6 +84,12 @@ impl DeclaredType { } } + fn declared_type(&self) -> &Type { + match &self.ty { + DeclaredTypeKind::Struct(ty, _) | DeclaredTypeKind::Type(ty) => ty, + } + } + pub fn with_source(mut self, source: SourceRef) -> Self { self.source = source; self @@ -176,6 +182,14 @@ impl TypeChecker { ); self.setup_declared_types(definitions); + // After we setup declared types, every definition + // related with a Struct Declaration is not nedded any more + let mut definitions: HashMap<_,_> = definitions + .into_iter() + .filter(|(_, (ty, _))| { + !matches!(ty, Some(declared) if matches!(declared.ty, DeclaredTypeKind::Struct(_, _))) + }) + .collect(); // These are the inferred types for symbols that are declared // as type schemes. They are compared to the declared types @@ -195,7 +209,7 @@ impl TypeChecker { let declared_type = self.declared_types[&name].clone(); if declared_type.vars.is_empty() { self.declared_type_vars.clear(); - self.process_concrete_symbol(declared_type.scheme().ty.clone(), value)?; + self.process_concrete_symbol(declared_type.declared_type().clone(), value)?; } else { self.declared_type_vars = declared_type .vars @@ -218,7 +232,7 @@ impl TypeChecker { for (name, declared_type) in &self.declared_types { if declared_type.vars.is_empty() { // It is not a type scheme, see if we were able to derive a concrete type. - let inferred = self.type_into_substituted(declared_type.scheme().ty.clone()); + let inferred = self.type_into_substituted(declared_type.declared_type().clone()); if !inferred.is_concrete_type() { let inferred_scheme = self.to_type_scheme(inferred); return Err(declared_type.source.with_error( @@ -569,9 +583,7 @@ impl TypeChecker { source_ref, Reference::Poly(PolynomialReference { name, type_args }), ) => { - let (ty, args) = self - .unifier - .instantiate_scheme(self.declared_types[name].scheme().clone()); + let (ty, args) = self.instantiate_scheme_by_declared_name(name); if let Some(requested_type_args) = type_args { if requested_type_args.len() != args.len() { return Err(source_ref.with_error(format!( @@ -904,9 +916,8 @@ impl TypeChecker { Pattern::Enum(source_ref, name, data) => { // We just ignore the generic args here, storing them in the pattern // is not helpful because the type is obvious from the value. - let (ty, _generic_args) = self - .unifier - .instantiate_scheme(self.declared_types[&name.to_string()].scheme().clone()); + let (ty, _generic_args) = + self.instantiate_scheme_by_declared_name(&name.to_string()); let ty = type_for_reference(&ty); match data { @@ -972,7 +983,8 @@ impl TypeChecker { format_type_scheme_around_name(&name, &Some(declared), )))); } - let declared_type_vars = declared.ty.contained_type_vars(); + let declared_ty = declared_type.scheme().ty; + let declared_type_vars = declared_ty.contained_type_vars(); let inferred_type_vars = inferred_type.contained_type_vars(); Ok((name.clone(), inferred_type_vars @@ -1025,6 +1037,11 @@ impl TypeChecker { pub fn local_var_type(&self, id: u64) -> Type { self.local_var_types[id as usize].clone() } + + fn instantiate_scheme_by_declared_name(&mut self, name: &str) -> (Type, Vec) { + self.unifier + .instantiate_scheme(self.declared_types[&name.to_string()].scheme().clone()) + } } fn update_type_if_literal( From 84439d8c34279f8bd3f3b4264b8f4c505ed0fe47 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Fri, 1 Nov 2024 11:05:20 -0300 Subject: [PATCH 03/13] clippy --- pil-analyzer/src/type_inference.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pil-analyzer/src/type_inference.rs b/pil-analyzer/src/type_inference.rs index 3b455d500b..9d77bfc958 100644 --- a/pil-analyzer/src/type_inference.rs +++ b/pil-analyzer/src/type_inference.rs @@ -185,7 +185,7 @@ impl TypeChecker { // After we setup declared types, every definition // related with a Struct Declaration is not nedded any more let mut definitions: HashMap<_,_> = definitions - .into_iter() + .iter_mut() .filter(|(_, (ty, _))| { !matches!(ty, Some(declared) if matches!(declared.ty, DeclaredTypeKind::Struct(_, _))) }) From 93d050753dcd0b7fe1d4d73e37ca4c9673a14c27 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gast=C3=B3n=20Zanitti?= Date: Fri, 1 Nov 2024 11:37:56 -0300 Subject: [PATCH 04/13] Update pil-analyzer/src/type_inference.rs Co-authored-by: chriseth --- pil-analyzer/src/type_inference.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pil-analyzer/src/type_inference.rs b/pil-analyzer/src/type_inference.rs index 9d77bfc958..72e7f4f202 100644 --- a/pil-analyzer/src/type_inference.rs +++ b/pil-analyzer/src/type_inference.rs @@ -1040,7 +1040,7 @@ impl TypeChecker { fn instantiate_scheme_by_declared_name(&mut self, name: &str) -> (Type, Vec) { self.unifier - .instantiate_scheme(self.declared_types[&name.to_string()].scheme().clone()) + .instantiate_scheme(self.declared_types[name].scheme().clone()) } } From 44949c11868ef5bfcb4e1b1c22738924818adae8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gast=C3=B3n=20Zanitti?= Date: Fri, 1 Nov 2024 13:54:44 -0300 Subject: [PATCH 05/13] Update pil-analyzer/src/type_inference.rs Co-authored-by: chriseth --- pil-analyzer/src/type_inference.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/pil-analyzer/src/type_inference.rs b/pil-analyzer/src/type_inference.rs index 72e7f4f202..5466f48105 100644 --- a/pil-analyzer/src/type_inference.rs +++ b/pil-analyzer/src/type_inference.rs @@ -1038,6 +1038,7 @@ impl TypeChecker { self.local_var_types[id as usize].clone() } + /// Returns a new type scheme for the given name. fn instantiate_scheme_by_declared_name(&mut self, name: &str) -> (Type, Vec) { self.unifier .instantiate_scheme(self.declared_types[name].scheme().clone()) From f56ad9bc1dbb2a4d302345f11fab36cc4dbec88e Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Fri, 1 Nov 2024 14:23:00 -0300 Subject: [PATCH 06/13] new verify_type_schemes + compare_type_schemes --- pil-analyzer/src/type_inference.rs | 70 ++++++++++++++++++++---------- 1 file changed, 46 insertions(+), 24 deletions(-) diff --git a/pil-analyzer/src/type_inference.rs b/pil-analyzer/src/type_inference.rs index 5466f48105..a6c2b7fc48 100644 --- a/pil-analyzer/src/type_inference.rs +++ b/pil-analyzer/src/type_inference.rs @@ -971,29 +971,51 @@ impl TypeChecker { &self, inferred_types: HashMap, ) -> Result>, Error> { - inferred_types.into_iter().map(|(name, inferred_type)| { - let declared_type = self.declared_types[&name].clone(); - let inferred_type = self.type_into_substituted(inferred_type.clone()); - let inferred = self.to_type_scheme(inferred_type.clone()); - let declared = declared_type.scheme().clone().simplify_type_vars(); - if inferred != declared { - return Err(declared_type.source.with_error(format!( - "Inferred type scheme for symbol {name} does not match the declared type.\nInferred: let{}\nDeclared: let{}", - format_type_scheme_around_name(&name, &Some(inferred)), - format_type_scheme_around_name(&name, &Some(declared), - )))); - } - let declared_ty = declared_type.scheme().ty; - let declared_type_vars = declared_ty.contained_type_vars(); - let inferred_type_vars = inferred_type.contained_type_vars(); - Ok((name.clone(), - inferred_type_vars - .into_iter() - .cloned() - .zip(declared_type_vars.into_iter().map(|tv| Type::TypeVar(tv.clone()))) - .collect(), - )) - }).collect::>() + inferred_types + .into_iter() + .map(|(name, inferred_type)| { + let declared_type = self.declared_types[&name].clone(); + let inferred_type = self.type_into_substituted(inferred_type.clone()); + + self.compare_type_schemes(&name, inferred_type, declared_type.scheme().clone()) + .map_err(|err| { + declared_type + .source + .with_error(format!("For symbol {name}: {err}")) + }) + .map(|mapping| (name, mapping)) + }) + .collect() + } + + /// Compares two type schemes and returns a mapping from inferred type vars to declared type vars if they match + fn compare_type_schemes( + &self, + name: &str, + inferred_type: Type, + declared_scheme: TypeScheme, + ) -> Result, String> { + let inferred = self.to_type_scheme(inferred_type.clone()); + let declared = declared_scheme.clone().simplify_type_vars(); + + if inferred != declared { + return Err(format!( + "Inferred type scheme does not match the declared type.\nInferred: let{}\nDeclared: let{}", + format_type_scheme_around_name(&name, &Some(inferred)), + format_type_scheme_around_name(&name, &Some(declared)) + )); + } + + Ok(inferred_type + .contained_type_vars() + .cloned() + .zip( + declared_scheme + .ty + .contained_type_vars() + .map(|tv| Type::TypeVar(tv.clone())), + ) + .collect()) } fn type_into_substituted(&self, mut ty: Type) -> Type { @@ -1038,7 +1060,7 @@ impl TypeChecker { self.local_var_types[id as usize].clone() } - /// Returns a new type scheme for the given name. + /// Returns a new type scheme as a tuple (type, generic args) for the given name. fn instantiate_scheme_by_declared_name(&mut self, name: &str) -> (Type, Vec) { self.unifier .instantiate_scheme(self.declared_types[name].scheme().clone()) From 61fa85b8808c5d5303dfe62998c2500e535b8596 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Mon, 4 Nov 2024 12:58:26 -0300 Subject: [PATCH 07/13] get names after structs removal --- pil-analyzer/src/type_inference.rs | 70 ++++++++++++++++++------------ 1 file changed, 42 insertions(+), 28 deletions(-) diff --git a/pil-analyzer/src/type_inference.rs b/pil-analyzer/src/type_inference.rs index a6c2b7fc48..843b7b9764 100644 --- a/pil-analyzer/src/type_inference.rs +++ b/pil-analyzer/src/type_inference.rs @@ -1,3 +1,4 @@ +use core::panic; use std::collections::{BTreeSet, HashMap}; use itertools::Itertools; @@ -174,13 +175,6 @@ impl TypeChecker { // - analyze each such group in an environment, where their type schemes // are instantiated once at the start and not anymore for the symbol lookup. - // Sort the names such that called names occur first. - let names = sort_called_first( - definitions - .iter() - .map(|(n, (_, v))| (n.as_str(), v.as_deref())), - ); - self.setup_declared_types(definitions); // After we setup declared types, every definition // related with a Struct Declaration is not nedded any more @@ -191,6 +185,13 @@ impl TypeChecker { }) .collect(); + // Sort the names such that called names occur first. + let names = sort_called_first( + definitions + .iter() + .map(|(n, (_, v))| (n.as_str(), v.as_deref())), + ); + // These are the inferred types for symbols that are declared // as type schemes. They are compared to the declared types // at the end. @@ -206,12 +207,12 @@ impl TypeChecker { continue; }; - let declared_type = self.declared_types[&name].clone(); - if declared_type.vars.is_empty() { + let declared_type_scheme = self.type_scheme_from_declared_type(&name); + if declared_type_scheme.vars.is_empty() { self.declared_type_vars.clear(); - self.process_concrete_symbol(declared_type.declared_type().clone(), value)?; + self.process_concrete_symbol(declared_type_scheme.ty.clone(), value)?; } else { - self.declared_type_vars = declared_type + self.declared_type_vars = declared_type_scheme .vars .vars() .map(|v| (v.clone(), self.unifier.new_type_var())) @@ -229,23 +230,25 @@ impl TypeChecker { // Now we check for all symbols that are not declared as a type scheme that they // can resolve to a concrete type. - for (name, declared_type) in &self.declared_types { - if declared_type.vars.is_empty() { - // It is not a type scheme, see if we were able to derive a concrete type. - let inferred = self.type_into_substituted(declared_type.declared_type().clone()); - if !inferred.is_concrete_type() { - let inferred_scheme = self.to_type_scheme(inferred); - return Err(declared_type.source.with_error( - format!( - "Could not derive a concrete type for symbol {name}.\nInferred type scheme: {}\n", - format_type_scheme_around_name( - name, - &Some(inferred_scheme), - ) - ))); - } - } - } + self.declared_types + .iter() + .filter(|(_, declared_type)| declared_type.vars.is_empty()) + // It is not a type scheme, see if we were able to derive a concrete type. + .map(|(name, declared_type)| { + ( + name, + declared_type.source.clone(), + self.type_into_substituted(declared_type.declared_type().clone()), + ) + }) + .filter(|(_, _, inferred)| !inferred.is_concrete_type()) + .try_for_each(|(name, source, inferred)| { + let inferred_scheme = self.to_type_scheme(inferred); + Err(source.with_error(format!( + "Could not derive a concrete type for symbol {name}.\nInferred type scheme: {}\n", + format_type_scheme_around_name(name, &Some(inferred_scheme)) + ))) + })?; // We check type schemes last, because only at this point do we know // that other types that should be concrete do not occur as type variables in the @@ -255,6 +258,17 @@ impl TypeChecker { self.verify_type_schemes(inferred_types) } + fn type_scheme_from_declared_type(&mut self, name: &String) -> TypeScheme { + let declared_type = self.declared_types[name].clone(); + + match declared_type.ty { + DeclaredTypeKind::Struct(_, _) => { + unreachable!("Struct declarations should be removed") + } + DeclaredTypeKind::Type(_) => declared_type.scheme(), + } + } + /// Fills self.declared_types and checks that declared builtins have the correct type. fn setup_declared_types( &mut self, From 5a62af6b0803f993a9fe512a7d28927aa0048ce6 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Mon, 4 Nov 2024 13:04:56 -0300 Subject: [PATCH 08/13] better msg --- pil-analyzer/src/type_inference.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pil-analyzer/src/type_inference.rs b/pil-analyzer/src/type_inference.rs index 843b7b9764..cfa70f8894 100644 --- a/pil-analyzer/src/type_inference.rs +++ b/pil-analyzer/src/type_inference.rs @@ -263,7 +263,7 @@ impl TypeChecker { match declared_type.ty { DeclaredTypeKind::Struct(_, _) => { - unreachable!("Struct declarations should be removed") + unreachable!("Struct declarations should have been removed at this point") } DeclaredTypeKind::Type(_) => declared_type.scheme(), } From 89eedb17c758e3474261cdee1fb12af880dba035 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Mon, 4 Nov 2024 13:05:28 -0300 Subject: [PATCH 09/13] better msg --- pil-analyzer/src/type_inference.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pil-analyzer/src/type_inference.rs b/pil-analyzer/src/type_inference.rs index cfa70f8894..8f292cc954 100644 --- a/pil-analyzer/src/type_inference.rs +++ b/pil-analyzer/src/type_inference.rs @@ -263,7 +263,7 @@ impl TypeChecker { match declared_type.ty { DeclaredTypeKind::Struct(_, _) => { - unreachable!("Struct declarations should have been removed at this point") + unreachable!("Declared types for Structs should have been removed at this point") } DeclaredTypeKind::Type(_) => declared_type.scheme(), } From 2b298f74d7dd509a42a020d0dc411cd8e68f3ee2 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Mon, 4 Nov 2024 14:09:24 -0300 Subject: [PATCH 10/13] names --- pil-analyzer/src/type_inference.rs | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/pil-analyzer/src/type_inference.rs b/pil-analyzer/src/type_inference.rs index 8f292cc954..8222eadc0e 100644 --- a/pil-analyzer/src/type_inference.rs +++ b/pil-analyzer/src/type_inference.rs @@ -175,6 +175,13 @@ impl TypeChecker { // - analyze each such group in an environment, where their type schemes // are instantiated once at the start and not anymore for the symbol lookup. + // Sort the names such that called names occur first. + let names = sort_called_first( + definitions + .iter() + .map(|(n, (_, v))| (n.as_str(), v.as_deref())), + ); + self.setup_declared_types(definitions); // After we setup declared types, every definition // related with a Struct Declaration is not nedded any more @@ -185,13 +192,6 @@ impl TypeChecker { }) .collect(); - // Sort the names such that called names occur first. - let names = sort_called_first( - definitions - .iter() - .map(|(n, (_, v))| (n.as_str(), v.as_deref())), - ); - // These are the inferred types for symbols that are declared // as type schemes. They are compared to the declared types // at the end. From 5e8384c778c5a15d51149ca31a40b979b8a9a182 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Sun, 10 Nov 2024 22:31:57 -0300 Subject: [PATCH 11/13] is_concrete --- pil-analyzer/src/type_inference.rs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/pil-analyzer/src/type_inference.rs b/pil-analyzer/src/type_inference.rs index 8222eadc0e..c324859909 100644 --- a/pil-analyzer/src/type_inference.rs +++ b/pil-analyzer/src/type_inference.rs @@ -95,6 +95,10 @@ impl DeclaredType { self.source = source; self } + + fn is_concrete(&self) -> bool { + self.vars.is_empty() + } } #[derive(Debug, Clone)] @@ -155,7 +159,7 @@ impl TypeChecker { .filter(|(_, (ty, _))| ty.is_none()) .map(|(name, _)| { let mut declared_type = self.declared_types.remove(&name).unwrap(); - assert!(declared_type.vars.is_empty()); + assert!(declared_type.is_concrete()); self.substitute(declared_type.type_mut()); assert!(declared_type.scheme().ty.is_concrete_type()); (name, declared_type.scheme().ty) @@ -232,7 +236,7 @@ impl TypeChecker { // can resolve to a concrete type. self.declared_types .iter() - .filter(|(_, declared_type)| declared_type.vars.is_empty()) + .filter(|(_, declared_type)| declared_type.is_concrete()) // It is not a type scheme, see if we were able to derive a concrete type. .map(|(name, declared_type)| { ( @@ -313,7 +317,7 @@ impl TypeChecker { for (name, scheme) in builtin_schemes() { self.declared_types .entry(name.clone()) - .or_insert_with(|| Into::::into(scheme.clone())); + .or_insert_with(|| DeclaredType::from(scheme.clone())); definitions.remove(name); } } From 5589f47e1aa40b5a0bc50127c629f664752a117b Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Wed, 13 Nov 2024 10:13:19 -0300 Subject: [PATCH 12/13] remove pub --- pil-analyzer/src/type_inference.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/pil-analyzer/src/type_inference.rs b/pil-analyzer/src/type_inference.rs index c324859909..7d7b3013a4 100644 --- a/pil-analyzer/src/type_inference.rs +++ b/pil-analyzer/src/type_inference.rs @@ -63,9 +63,9 @@ impl From for ExpectedType { #[derive(Debug, Clone)] pub struct DeclaredType { - pub source: SourceRef, - pub vars: TypeBounds, - pub ty: DeclaredTypeKind, + source: SourceRef, + vars: TypeBounds, + ty: DeclaredTypeKind, } impl DeclaredType { @@ -102,7 +102,7 @@ impl DeclaredType { } #[derive(Debug, Clone)] -pub enum DeclaredTypeKind { +enum DeclaredTypeKind { #[allow(dead_code)] // Remove when #1910 is merged Struct(Type, HashMap), Type(Type), From 975ed04913ecfedb7bb4f3cc446b22f37ffea6d6 Mon Sep 17 00:00:00 2001 From: Gaston Zanitti Date: Wed, 13 Nov 2024 11:28:10 -0300 Subject: [PATCH 13/13] compare_inferred_type_to_declared --- pil-analyzer/src/type_inference.rs | 22 ++++++++-------------- 1 file changed, 8 insertions(+), 14 deletions(-) diff --git a/pil-analyzer/src/type_inference.rs b/pil-analyzer/src/type_inference.rs index 7d7b3013a4..37d968b69c 100644 --- a/pil-analyzer/src/type_inference.rs +++ b/pil-analyzer/src/type_inference.rs @@ -992,36 +992,30 @@ impl TypeChecker { inferred_types .into_iter() .map(|(name, inferred_type)| { - let declared_type = self.declared_types[&name].clone(); - let inferred_type = self.type_into_substituted(inferred_type.clone()); - - self.compare_type_schemes(&name, inferred_type, declared_type.scheme().clone()) - .map_err(|err| { - declared_type - .source - .with_error(format!("For symbol {name}: {err}")) - }) + self.compare_inferred_type_to_declared(&name, inferred_type) .map(|mapping| (name, mapping)) }) .collect() } /// Compares two type schemes and returns a mapping from inferred type vars to declared type vars if they match - fn compare_type_schemes( + fn compare_inferred_type_to_declared( &self, name: &str, inferred_type: Type, - declared_scheme: TypeScheme, - ) -> Result, String> { + ) -> Result, Error> { + let declared_type = self.declared_types[name].clone(); + let declared_scheme = declared_type.scheme(); + let inferred_type = self.type_into_substituted(inferred_type.clone()); let inferred = self.to_type_scheme(inferred_type.clone()); let declared = declared_scheme.clone().simplify_type_vars(); if inferred != declared { - return Err(format!( + return Err(declared_type.source.with_error(format!( "Inferred type scheme does not match the declared type.\nInferred: let{}\nDeclared: let{}", format_type_scheme_around_name(&name, &Some(inferred)), format_type_scheme_around_name(&name, &Some(declared)) - )); + ))); } Ok(inferred_type