search

finos / morphir-elm

Tools to work with the Morphir IR in Elm.
https://package.elm-lang.org/packages/finos/morphir-elm/latest
Apache License 2.0
46 stars 65 forks source link

Morphir-elm compiler allows runtime polymorphism and type errors #1146

Open edwardpeters opened 8 months ago

edwardpeters commented 8 months ago

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):

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 https://github.com/finos/morphir-elm/issues/1102 , but demonstrates broader type issues.

edwardpeters commented 4 months ago

@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.