No kind checking - subrecords can be non-records

[TheSeamau5]

So, apparently if you do this:

type alias Vector a = { a | x : Int }

add : a -> Vector a
add p = 
  { p | x = 1 }

x : Vector Int
x = add 1

you get this awful error which is hall of fame worthy

Used toSrcType on a type that is not well-formed

But the worst part is that if you comment out the type annotation for x

type alias Vector a = { a | x : Int }

add : a -> Vector a
add p = 
  { p | x = 1 }

--x : Vector Int
x = add 1

No compile-time errors. ???

And if you try to show x, you get:

<internal structure>

???

[mgold]

In add, p must be a record, not an arbitrary term as the type a suggests. Define x as this and it compiles:

x : Vector {}
x = add {}

show x produces { x = 1 } as you'd expect.

The type of add needs to be constrained to only accept a record, but the obvious add : {a} -> Vector a is not accepted.

Good find.

[evancz]

This should be a kind error, which currently is not detected.

[TheSeamau5]

Two asides:

1. As asked here: https://groups.google.com/forum/#!topic/elm-discuss/jGA5O0shBU4
   Is there a way to alias the extensible empty record type.

You know, something like this:

type alias Record a = { a | }

Cuz that can at least protect certain APIs from this bug. Concretely, I'd be able to define the add function from above to be:

add : Record a -> Vector (Record a)

And at least here, the error would be less ugly (cuz presumably you'd get the standard error of types being mismatched as opposed to the horribleness you get today).

2. I know that you're interested in the idea, but should we start discussing the possible revamping of the whole record thing or is it too soon?

You know, discuss ideas like merging, disallowing two fields of the same name, multiple extend operations, multiple delete operations, etc...

[tapeinosyne]

Note that, while the example provided by @TheSeamau5 is “evidently” malformed, there are less obvious ways to confuse the typechecker:

type alias X  a =   { a | x : Int }
type alias XY a = X { a | y : Int }
type alias Z  a =   { a | z : Int }
type alias XYZ  =   XY (Z {})
type alias ZXY  =   Z (XY {})

xy : XY {}
xy = { x = 0
     , y = 0 }

xyz : XYZ
xyz = { x = 0
      , y = 0
      , z = 0 }

-- with type annotation, compiler raises `Used toSrcType on a type that is not well-formed`;
-- without, infers the same “apparent” type of `xyz`.
zxy : ZXY
zxy = { x = 1 // 1
      , y = 1 // 1
      , z = 1 // 1 }

[thSoft]

Also happens when the "extended" type is an ADT. Unfortunately, the error message does not even say which type is problematic. :(

[goens]

Sorry, I don't get why it raises a problem on the example shown by @ndr-qef. It's a very nice example, since it shows how subtle this issue is imho (as xy and xyz work just fine). Can you explain what is wrong with it, with zxy? I mean, as far as I understand it resolve to an empty record in the end, right? So how do xyz and xy differ fundamentally from zxy?

In particular, how can you avoid doing something like that yourself? I think I have the same basic problem as you show in the example, but don't quite understand the issue.

[evancz]

Since record extension is going to be removed in 0.16, the root example is no longer reproducible.

It looks like @ndr-qef has found an example that does not require record extension. I'm not sure it's the same thing, but I think it should be broken out into a separate issue of its own.

I have a PR coming in which that code works just fine though, so give me a few hours and I may be able to share that!

[Steve-OH]

The following code gives the same error in 0.16:

type alias Identified a =
    { a | id : String }

type alias Metadata =
    Identified ()

meta : String -> Metadata
meta id =
    { id = id }

Commenting out meta's type declaration causes the error to go away.

I can't tell if this is equivalent to one of the above examples or not.

[sjfloat]

I'm hitting this behavior in 0.17 and I'm not clear about the resolution or why this was closed.

[JoeyEremondi]

We see a similar kind error with type constructors.

type IntRose = 
  Leaf Int 
  | Node List IntRose

compiles without warning.

If we add myRose = Node [Leaf 3], we get a mismatch between List and List IntRose: not exactly helpful. The error is in the type definition, not the use.

Newbies have come across this error more than once.

[evancz]

If you are seeing an error, open an issue with an http://sscce.org/ that follows the checklist. I believe there is already an issue open about adding kind checking though.

[evancz]

Yeah, this is tracked in #1373

[JoeyEremondi]

What's the procedure for the bunched issues? Should the SSSCCE be provided on that issue? Or here?

[evancz]

I think it's only really valuable to have more if we think it is different or the solution is unlikely to catch a particular case.

A good way to do this is to open a new issue with an SSCCE, and when we are sure it is a duplicate, modify the meta issue to point to that issue as well. So I will edit #1373 to have a reference to this one as well.