FA-43496 / Borrow checking / Open access
An absent lifetime occurrence spuriously constrains the generic parameter · case 01
An absent lifetime occurrence spuriously constrains the generic parameter.
ROOT CAUSE
The static analyzer mishandles unused parameter: an absent lifetime occurrence spuriously constrains the generic parameter.
VERIFIED REPAIR
Apply the specified transfer or inference rule at this site: if kind=='unused': return {}.
Unsuccessful approach: The partial repair uses if kind=='unused': return {t[1]:sign}, which still violates the stipulated analysis contract.
Case contract
Infer lifetime parameter variance in a toy type tree. Variance signs are +1 covariant, -1 contravariant, 0 invariant; repeated different signs join to invariant. var(name); ref(lifetime,type) covariant both; mut(lifetime,type) covariant lifetime invariant payload; fn(argument,result) flips argument; tuple(list) joins; cell(type) invariant; phantom(type) covariant; array(type,length) covariant; opaque(parameters) invariant for every listed parameter; unused(name) contributes nothing. Return parameter-to-sign map.
Why this case matters
A finite offline static-analysis model of ownership and borrowing; it does not execute the analyzed program.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(tree):
def walk(t,sign):
kind=t[0]
if kind=='var': return {t[1]:sign}
if kind=='unused': return {t[1]:0}
if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
elif kind=='cell': children=[t[1]]; signs=[0]
elif kind=='phantom': children=[t[1]]; signs=[sign]
elif kind=='array': children=[t[1]]; signs=[sign]
elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
else: return {}
out={}
for child,s in zip(children,signs):
for p,v in walk(child,s).items():
out[p]=v if p not in out or out[p]==v else 0
return out
return walk(tree,1)
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| variable | {'a': 1} | {'a': 1} | Passed |
| unused | {'a': 0} | {} | Failed |
| shared | {'a': 1, 'b': 1} | {'a': 1, 'b': 1} | Passed |
| mutable | {'a': 1, 'b': 0} | {'a': 1, 'b': 0} | Passed |
| function | {'a': -1, 'b': 1} | {'a': -1, 'b': 1} | Passed |
| tuple | {'a': 1, 'b': 1} | {'a': 1, 'b': 1} | Passed |
| cell | {'a': 0} | {'a': 0} | Passed |
| phantom | {'a': 1} | {'a': 1} | Passed |
| opaque | {'a': 0, 'b': 0} | {'a': 0, 'b': 0} | Passed |
| both positions | {'a': 0} | {'a': 0} | Passed |
| array | {'a': 1} | {'a': 1} | Passed |
| variable arity | {'0': 1, '1': 1} | {'0': 1, '1': 1} | Passed |
SHA-256 / 4e6c9a2e2f3a0665e3a34e2ee894f6b699df7a759fb29f77841461e51df22ccd
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(tree):
def walk(t,sign):
kind=t[0]
if kind=='var': return {t[1]:sign}
if kind=='unused': return {t[1]:sign}
if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
elif kind=='cell': children=[t[1]]; signs=[0]
elif kind=='phantom': children=[t[1]]; signs=[sign]
elif kind=='array': children=[t[1]]; signs=[sign]
elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
else: return {}
out={}
for child,s in zip(children,signs):
for p,v in walk(child,s).items():
out[p]=v if p not in out or out[p]==v else 0
return out
return walk(tree,1)
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| variable | {'a': 1} | {'a': 1} | Passed |
| unused | {'a': 1} | {} | Failed |
| shared | {'a': 1, 'b': 1} | {'a': 1, 'b': 1} | Passed |
| mutable | {'a': 1, 'b': 0} | {'a': 1, 'b': 0} | Passed |
| function | {'a': -1, 'b': 1} | {'a': -1, 'b': 1} | Passed |
| tuple | {'a': 1, 'b': 1} | {'a': 1, 'b': 1} | Passed |
| cell | {'a': 0} | {'a': 0} | Passed |
| phantom | {'a': 1} | {'a': 1} | Passed |
| opaque | {'a': 0, 'b': 0} | {'a': 0, 'b': 0} | Passed |
| both positions | {'a': 0} | {'a': 0} | Passed |
| array | {'a': 1} | {'a': 1} | Passed |
| variable arity | {'0': 1, '1': 1} | {'0': 1, '1': 1} | Passed |
SHA-256 / 6b91596308ebea1576e65fa1e3c553611527b3a776b19f1fda7ab1a35e6c0290
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(tree):
def walk(t,sign):
kind=t[0]
if kind=='var': return {t[1]:sign}
if kind=='unused': return {}
if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
elif kind=='cell': children=[t[1]]; signs=[0]
elif kind=='phantom': children=[t[1]]; signs=[sign]
elif kind=='array': children=[t[1]]; signs=[sign]
elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
else: return {}
out={}
for child,s in zip(children,signs):
for p,v in walk(child,s).items():
out[p]=v if p not in out or out[p]==v else 0
return out
return walk(tree,1)
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| variable | {'a': 1} | {'a': 1} | Passed |
| unused | {} | {} | Passed |
| shared | {'a': 1, 'b': 1} | {'a': 1, 'b': 1} | Passed |
| mutable | {'a': 1, 'b': 0} | {'a': 1, 'b': 0} | Passed |
| function | {'a': -1, 'b': 1} | {'a': -1, 'b': 1} | Passed |
| tuple | {'a': 1, 'b': 1} | {'a': 1, 'b': 1} | Passed |
| cell | {'a': 0} | {'a': 0} | Passed |
| phantom | {'a': 1} | {'a': 1} | Passed |
| opaque | {'a': 0, 'b': 0} | {'a': 0, 'b': 0} | Passed |
| both positions | {'a': 0} | {'a': 0} | Passed |
| array | {'a': 1} | {'a': 1} | Passed |
| variable arity | {'0': 1, '1': 1} | {'0': 1, '1': 1} | Passed |
SHA-256 / a1c0aadac82f1b47dd4624fe34dce0cabf2f31e95f3ad2501a6130bc28bed72d
Verification & scope
The explicitly stated toy language is the complete scope; this is not a production compiler or a claim about Rust semantics. This reproducer isolates one failure mechanism. Results cover the supplied fixtures. Variants within a family share a test contract and should remain grouped when constructing evaluation splits. Related mechanisms with a shared evaluation_group must also remain together; these controlled models are not independent production incidents.
Observations recorded using Python 3.12.14 at 2026-09-29T14:44:02.442965+00:00.
Case digest / 14e6eea3078471d96a564ef048d614b972874807379af7024b3f50079ae8aa88