Morphir-elm compiler allows runtime polymorphism and type errors

[edwardpeters]

Describe the bug
The type inferencing algorithm used by morphir-elm make handles type variables in a way which allows users to compile polymorphic code.

To Reproduce
The following code compiles and runs:

cast : a -> b
cast x = x

foo : String -> String -> String
foo s1 s2 = String.concat [s1, s2]

bar : Int -> Int -> String
bar i1 i2 = foo (cast i1) (cast i2)

baz : String -> String
baz s = bar (cast s) (cast s)

baaz : a -> b -> String
baaz a b = String.concat[cast a, cast b]

baz runs. baaz also runs, specifically if fed two strings as input - otherwise it results in "Unable to compute", which in this case I believe indicated a runtime type error.

Expected behavior
As defined, cast should be rejected due to a unification error between a and b. (This is the behavior in native elm.)

Desktop (please complete the following information):

• OS: OSX
• Version: 2.89.0

Additional context
I believe this is due to the compiler not distinguishing between generic type variables and free type variables. When inference runs on cast, it therefor tries to unify a with b; as it treats them both as free, it thinks it is able to do so. When inference runs on calling code, it sees them as being independent, and can bind the input and output types to whatever it wants.

This is highly related to #1102 , but demonstrates broader type issues.

[edwardpeters]

@AttilaMihaly This is the issue I mentioned the other week, which I think you felt deserved fixing in the compiler. Just confirmed that it remains in effect on the latest version.