Fix generic inference by instantiating annotations and storing inferred types

[abs0luty]

• Closes Unbound type variable in top level definition after type inference #2533
• Closes Type inference issue expected Test(a) but found Test(a) #2550

💡 Explanation

pub type Test(a) {
  Test(a)
}

pub fn it(value: Test(a)) {
  it2(value)
}

pub fn it2(value: Test(a)) -> Test(a) {
  it(value)
}

pub fn main() {
  it(Test(1))
}

Before the patch the compiler registered a generic "sketch" for each function, then tried to compare the sketch directly to the inferred body types. That made the generic variables act rigid in the check and produced a false mismatch in mutually recursive code.

startup
  |
  v
preregister function sketches in env
  it  : fn(Test(a)) -> Test(a)
  it2 : fn(Test(a)) -> Test(a)

main()
  |
  v
Test(1) : Test(Int)
  |
  v
call it(Test(Int))
  |
  v
type of it looked up from env  -----------------------------> fn(Test(a)) -> Test(a)
  |                                                           (generic, rigid at check)
  v
inside it body, call it2(value)
  |
  v
finish it2
  |
  v
last expr type from body ----------------------------------> Test(Int)
  |
  v
direct compare without instantiation ----------------------> expected: Test(a)
                                                             found:    Test(Int)
                                                             result:   a behaves rigid
                                                                       unification fails
Environment remains with preregistered sketches
Error bubbles as false mismatch

Now the compiler instantiates annotations and preregistered types before unification, and it records the inferred result in the environment so later checks see the concrete shape.

startup
  |
  v
preregister sketches in env
  it  : fn(Test(a)) -> Test(a)
  it2 : fn(Test(a)) -> Test(a)

main()
  |
  v
Test(1) : Test(Int)
  |
  v
need type of it(Test(Int))  ------------------------------+
  |                                                       |
  v                                                       |
infer it body                                             |
  |                                                       |
  v                                                       |
call it2(value)                                           |
  |                                                       |
  v                                                       |
flow back provisional result from use of value -----------+--> Test(Int)
  |                                                       |
  v                                                       |
inferred type for it becomes -----------------------------+--> fn(Test(Int)) -> Test(Int)
  |                                                       |
  v                                                       |
store inferred type in env (overwrite sketch) ------------+--> it : fn(Test(Int)) -> Test(Int)

infer it2
  |
  v
last expr is it(value)
  |
  v
from env, type of it(value) -------------------------------> Test(Int)
  |
  v
check it2 return annotation
  |
  v
instantiate annotation Test(a) ----------------------------> Test(a₁)
  |
  v
unify Test(a₁) with Test(Int)  ============================= a₁ := Int, success
  |
  v
store inferred type in env --------------------------------> it2 : fn(Test(Int)) -> Test(Int)

finish main
  |
  v
it(Test(1)) : Test(Int)

no mismatch, because:
- comparisons use instantiated annotations
- recursion observes concrete env entries rather than generic sketches
- typed AST keeps the inferred return type