Skip to content

Commit

Permalink
fix: apply generic arguments from trait constraints before instantiat…
Browse files Browse the repository at this point in the history
…ing identifiers (#4121)

# Description

## Problem\*

Resolves #4088

## Summary\*

We were calling `instantiate` on identifiers before applying any trait
constraints. So if we have a constraint like `Foo<Field>` (referring to
the trait `trait Foo<T> { ... }`, and an identifier `foo : forall T.
fn(T)`, we need to apply the `T = Field` constraint before instantiating
`foo` to replace `T` with a fresh type variable.

## Additional Context



## Documentation\*

Check one:
- [x] No documentation needed.
- [ ] Documentation included in this PR.
- [ ] **[Exceptional Case]** Documentation to be submitted in a separate
PR.

# PR Checklist\*

- [x] I have tested the changes locally.
- [x] I have formatted the changes with [Prettier](https://prettier.io/)
and/or `cargo fmt` on default settings.

---------

Co-authored-by: Maxim Vezenov <mvezenov@gmail.com>
  • Loading branch information
jfecher and vezenovm authored Jan 23, 2024
1 parent ec36670 commit eb6fc0f
Show file tree
Hide file tree
Showing 5 changed files with 101 additions and 48 deletions.
5 changes: 3 additions & 2 deletions compiler/noirc_frontend/src/hir/resolution/resolver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1746,7 +1746,8 @@ impl<'a> Resolver<'a> {

// This resolves a static trait method T::trait_method by iterating over the where clause
//
// Returns the trait method, object type, and the trait generics.
// Returns the trait method, trait constraint, and whether the impl is assumed from a where
// clause. This is always true since this helper searches where clauses for a generic constraint.
// E.g. `t.method()` with `where T: Foo<Bar>` in scope will return `(Foo::method, T, vec![Bar])`
fn resolve_trait_method_by_named_generic(
&mut self,
Expand Down Expand Up @@ -1789,7 +1790,7 @@ impl<'a> Resolver<'a> {

// Try to resolve the given trait method path.
//
// Returns the trait method, object type, and the trait generics.
// Returns the trait method, trait constraint, and whether the impl is assumed to exist by a where clause or not
// E.g. `t.method()` with `where T: Foo<Bar>` in scope will return `(Foo::method, T, vec![Bar])`
fn resolve_trait_generic_path(
&mut self,
Expand Down
110 changes: 64 additions & 46 deletions compiler/noirc_frontend/src/hir/type_check/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ use crate::{
hir::{resolution::resolver::verify_mutable_reference, type_check::errors::Source},
hir_def::{
expr::{
self, HirArrayLiteral, HirBinaryOp, HirExpression, HirLiteral, HirMethodCallExpression,
HirMethodReference, HirPrefixExpression, ImplKind,
self, HirArrayLiteral, HirBinaryOp, HirExpression, HirIdent, HirLiteral,
HirMethodCallExpression, HirMethodReference, HirPrefixExpression, ImplKind,
},
types::Type,
},
Expand Down Expand Up @@ -46,50 +46,7 @@ impl<'interner> TypeChecker<'interner> {
/// function `foo` to refer to.
pub(crate) fn check_expression(&mut self, expr_id: &ExprId) -> Type {
let typ = match self.interner.expression(expr_id) {
HirExpression::Ident(ident) => {
// An identifiers type may be forall-quantified in the case of generic functions.
// E.g. `fn foo<T>(t: T, field: Field) -> T` has type `forall T. fn(T, Field) -> T`.
// We must instantiate identifiers at every call site to replace this T with a new type
// variable to handle generic functions.
let t = self.interner.id_type_substitute_trait_as_type(ident.id);

// This instantiate's a trait's generics as well which need to be set
// when the constraint below is later solved for when the function is
// finished. How to link the two?
let (typ, bindings) = t.instantiate(self.interner);

// Push any trait constraints required by this definition to the context
// to be checked later when the type of this variable is further constrained.
if let Some(definition) = self.interner.try_definition(ident.id) {
if let DefinitionKind::Function(function) = definition.kind {
let function = self.interner.function_meta(&function);

for mut constraint in function.trait_constraints.clone() {
constraint.apply_bindings(&bindings);
self.trait_constraints.push((constraint, *expr_id));
}
}
}

if let ImplKind::TraitMethod(_, mut constraint, assumed) = ident.impl_kind {
constraint.apply_bindings(&bindings);
if assumed {
let trait_impl = TraitImplKind::Assumed {
object_type: constraint.typ,
trait_generics: constraint.trait_generics,
};
self.interner.select_impl_for_expression(*expr_id, trait_impl);
} else {
// Currently only one impl can be selected per expr_id, so this
// constraint needs to be pushed after any other constraints so
// that monomorphization can resolve this trait method to the correct impl.
self.trait_constraints.push((constraint, *expr_id));
}
}

self.interner.store_instantiation_bindings(*expr_id, bindings);
typ
}
HirExpression::Ident(ident) => self.check_ident(ident, expr_id),
HirExpression::Literal(literal) => {
match literal {
HirLiteral::Array(HirArrayLiteral::Standard(arr)) => {
Expand Down Expand Up @@ -341,6 +298,67 @@ impl<'interner> TypeChecker<'interner> {
typ
}

/// Returns the type of the given identifier
fn check_ident(&mut self, ident: HirIdent, expr_id: &ExprId) -> Type {
let mut bindings = TypeBindings::new();

// Add type bindings from any constraints that were used.
// We need to do this first since otherwise instantiating the type below
// will replace each trait generic with a fresh type variable, rather than
// the type used in the trait constraint (if it exists). See #4088.
if let ImplKind::TraitMethod(_, constraint, _) = &ident.impl_kind {
let the_trait = self.interner.get_trait(constraint.trait_id);
assert_eq!(the_trait.generics.len(), constraint.trait_generics.len());

for (param, arg) in the_trait.generics.iter().zip(&constraint.trait_generics) {
bindings.insert(param.id(), (param.clone(), arg.clone()));
}
}

// An identifiers type may be forall-quantified in the case of generic functions.
// E.g. `fn foo<T>(t: T, field: Field) -> T` has type `forall T. fn(T, Field) -> T`.
// We must instantiate identifiers at every call site to replace this T with a new type
// variable to handle generic functions.
let t = self.interner.id_type_substitute_trait_as_type(ident.id);

// This instantiates a trait's generics as well which need to be set
// when the constraint below is later solved for when the function is
// finished. How to link the two?
let (typ, bindings) = t.instantiate_with_bindings(bindings, self.interner);

// Push any trait constraints required by this definition to the context
// to be checked later when the type of this variable is further constrained.
if let Some(definition) = self.interner.try_definition(ident.id) {
if let DefinitionKind::Function(function) = definition.kind {
let function = self.interner.function_meta(&function);

for mut constraint in function.trait_constraints.clone() {
constraint.apply_bindings(&bindings);
self.trait_constraints.push((constraint, *expr_id));
}
}
}

if let ImplKind::TraitMethod(_, mut constraint, assumed) = ident.impl_kind {
constraint.apply_bindings(&bindings);
if assumed {
let trait_impl = TraitImplKind::Assumed {
object_type: constraint.typ,
trait_generics: constraint.trait_generics,
};
self.interner.select_impl_for_expression(*expr_id, trait_impl);
} else {
// Currently only one impl can be selected per expr_id, so this
// constraint needs to be pushed after any other constraints so
// that monomorphization can resolve this trait method to the correct impl.
self.trait_constraints.push((constraint, *expr_id));
}
}

self.interner.store_instantiation_bindings(*expr_id, bindings);
typ
}

pub fn verify_trait_constraint(
&mut self,
object_type: &Type,
Expand Down
5 changes: 5 additions & 0 deletions test_programs/execution_success/regression_4088/Nargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
[package]
name = "regression_4088"
type = "bin"
authors = [""]
[dependencies]
2 changes: 2 additions & 0 deletions test_programs/execution_success/regression_4088/Prover.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
[note]
value = 0
27 changes: 27 additions & 0 deletions test_programs/execution_success/regression_4088/src/main.nr
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
trait Serialize<N> {
fn serialize(self) -> [Field; N];
}

struct ValueNote {
value: Field,
}

impl Serialize<1> for ValueNote {
fn serialize(self) -> [Field; 1] {
[self.value]
}
}

fn check<N>(serialized_note: [Field; N]) {
assert(serialized_note[0] == 0);
}

fn oopsie<Note, N>(note: Note) where Note: Serialize<N> {
let serialized_note = Note::serialize(note);

check(serialized_note)
}

fn main(mut note: ValueNote) {
oopsie(note);
}

0 comments on commit eb6fc0f

Please sign in to comment.