Type variables don't unify correctly in top level declarations

[davidcavazos]

Hi, I found an inconsistency while unifying type variables.

SSCCE

This works as expected, the type a unifies with type b and we don't get any errors.

k : Int
k =
  let
    f : a -> Int
    f x = 1

    g : b -> Int
    g = f
  in
  42

However, if the type variable was defined at the top-level declaration, we get a type error.

f : a -> Int
f x =
  let
    g : b -> Int
    g = f
  in
  42

Here's the error:

Something is off with the body of the `g` definition:

8|     g = f
           ^
This `f` value is a:

    a -> Int

But the type annotation on `g` says it should be:

    b -> Int

I think b should be able to unify with a without any problems.

Workaround: creating an "identity" copy of the function.

f : a -> Int
f x =
  42

g : b -> Int
g = f

• Elm: 0.19.1
• Browser: None, just a library while running the tests.
• Operating System: macOS 11.2.3 -- Macbook Pro 2017

Additional Details

That's a pretty stripped down example to reproduce the error, but this issue has been pretty annoying in my code base since I have to be declaring "duplicate" top-level wrapper functions with specialized types to calm down the type checker. Since my functions were recursive, I basically had to create a copy of the function with an underscore suffix and use that. It took a while to strip it down to a single function :)

[github-actions[bot]]

Thanks for reporting this! To set expectations:

• Issues are reviewed in batches, so it can take some time to get a response.
• Ask questions in a community forum. You will get an answer quicker that way!
• If you experience something similar, open a new issue. We like duplicates.

Finally, please be patient with the core team. They are trying their best with limited resources.