Hacktoberfest 2026: the issues maintainers tagged for October, open and beginner-friendly. Browse Hacktoberfest issues

Deep imm isn't checked for generic mutabilities and type parameters inside a function

Closed
  • Is something wrong?
#247 0 comments 0 reactions 0 assignees View on GitHub

Maintainers usually reply within 1 day

Nobody has claimed this yet.

Assessment

Difficulty
5/5
Estimated time
Over a week
Newbie friendliness
38/100
Issue type
Bug
Clarity
Mostly clear
Activity status
Active
Tech stack
rust
Domain
compilers, testing-qa

Research direction

Start by reading check_deep_immutability and the mutability constraint logic, including Solver::require_mut; compare those checks with the Lean proof under lean/. Reproduce the two generic-function examples with the evaluator's mutability checks. Done means unknown mutability inside an imm array or struct is constrained to Imm, while mutability and type parameters inside one are rejected; account for the later design described in #243.

Written by the indexing model from the issue text.

Description

bug priority:high scope:types

imm is deep: an imm array or struct can't hold anything mut. The checker enforces it after inference (check_deep_immutability) by looking for a Mut inside an Imm. But inside a generic function, what it holds can have a mutability that's a parameter, or be a value of a type parameter, which is only Mut once the function is called. The check doesn't see that unless the call's own types show it, so an imm value made inside the function can hold a mut one:

fn hide(xs: [i32], f: fn()) -> i32 {
  let w = [xs];            // `imm ['m [i32]]`: accepted
  let before = w[0][0];
  f();
  w[0][0] - before         // 1: `w` is `imm`, and changed
}
let ys = mut [1];
hide(ys, || { ys[0] = 2; });

struct Box[T] { item: T }
fn hide[T](x: T) -> i32 { let b = Box { item: x }; 0 }   // `imm Box[T]`: accepted
hide(mut [1]);             // `b` is an `imm Box` holding a `mut [i32]`

Both stop with "an imm value was made holding a mut one, which the type checker should have ruled out" when run with the evaluator's mutability checks. When the imm value is returned, as in fn wrap(xs: [i32]) = [xs], the caller's types show imm [mut [i32]] and it's reported there, which is why most cases are caught.

How it differs from the proof

The Lean proof (lean/) requires what an imm value holds to be imm exactly (DeepImm), so a mutability parameter or a type parameter inside one is rejected where it's made, whatever the function is called with. The checker only rejects Mut.

Fix

  • Now: an unknown mutability inside an imm array or struct becomes Imm (a constraint, like Solver::require_mut for changes), and a mutability parameter or a type parameter inside one is an error. fn wrap(xs) = [xs] would then be fn(imm [a]) -> imm [imm [a]], and fn wrap(xs: [i32]) = [xs] an error that asks for imm [i32].
  • Later: #243's rule 2 makes deep imm an inequality (T ⊑ μ) that's part of a function's type, which lets wrap stay generic and replaces the check after inference.

Closures already follow the proof here: a closure that captures a value of a type parameter is mut (#244), and one with a parameter's mutability can't be put in an imm struct.

Dominant language
Rust
Stars
54
Forks
3
Avg merge
7m
Merged PRs (30d)
28

Getting set up

This project ships no dev container, Dockerfile or contributing guide, so setting up is up to you: start from its README, and see our first-contribution guide for the general steps.

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from boltlang/Bolt

All issues in boltlang/Bolt

Similar issues

More Rust issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.