Skip to content

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

Open
@edwardpeters

Description

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.

Metadata

Assignees

No one assigned

    Labels

    taskTask level project item

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions