| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 0000575 | mercury | Bug | public | 2024-07-09 17:18 | 2025-08-13 07:35 | ||||||||
| Reporter | wangp | ||||||||||||
| Assigned To | |||||||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||||||
| Status | new | Resolution | open | ||||||||||
| Product Version | |||||||||||||
| Target Version | Fixed in Version | ||||||||||||
| Summary | 0000575: type qualification scope bug | ||||||||||||
| Description | Explicit type qualification is processed before quantification, leading to variables being given explicit types without taking into account that variables with the same name might be in different scopes. :- module type_qual_bug. :- interface. :- pred bug1 is det. :- pred bug2 is det. :- implementation. :- type foo1 ---> foo(int). :- type foo2 ---> foo(int). bug1 :- % X is assigned the type foo1 due to an explicit type qualification. % Later, when the Xs are renamed apart, the type is copied over to both % new variables. Obviously, the two Xs are not supposed to be related. some [X] ( X = foo(1) : foo1 ), some [X] ( X = foo(2) : foo2 ). bug2 :- % Both X variables end up with type foo2, so this compiles. % But the type of the first X should be ambiguous. some [X] ( X = foo(1) ), some [X] ( X = foo(2) : foo2 ). | ||||||||||||
| Tags | No tags attached. | ||||||||||||
| Attached Files |
| ||||||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
zs (developer) 2025-08-13 07:35 |
To associate the type qualification with the atomic goal in which it occurs and not with the clause as a whole, we need a new goal kind, probably a new kind of shorthand. We can modify maybe_unravel_special_var_functor_unification to record the type qualification in the unravel_info, we can pick it up when we finish processing each atomic goal, and if the atomic goal has a nonempty list of type qualifications, return the atomic goal in the new kind of shorthand that also lists the type qualifications. The typechecker can pick them up before it starts its main job, alerted by a flag in the clauses_info that says "there is at least one explicit type qualification in this predicate or function's clauses". |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2024-07-09 17:18 | wangp | New Issue | |
| 2024-07-09 17:18 | wangp | File Added: type_qual_bug.m | |
| 2025-08-13 07:35 | zs | Note Added: 0001235 | |
| Issue History |