Complex list types are not interpreted as lists for the purposes of type-annotating empty lists

[ari-becker]

working.dhall

let RebadgedText = Text : Type
in {
  emptyList = [] : List RebadgedText
}

The working.dhall passes the type checker and produces an empty list.

broken.dhall

let RebadgedTextList = (List Text): Type
in {
  emptyList = [] : RebadgedTextList
}

The broken.dhall produces an error: An empty list requires a type annotation.

Expected behavior: broken.dhall should pass the type checker and produce an empty list.

Using: dhall-to-yaml v1.2.4 (still latest available on Homebrew)

[ocharles]

[] : List T is a single syntactic element, while [] : RebadgedText is actually three - an annotation node with a (syntactically incomplete) empty list and the type 'RebadgedText' as children. With the current grammar, it's not possible to do what you want unfortunately. ([] : List Text) : RebadgedText should work, but is likely not what you want!

…

On Sun, 30 Dec 2018, 2:30 pm Ari Becker ***@***.*** wrote: working.dhall let RebadgedText = Text : Type in { emptyList = [] : List RebadgedText } The working.dhall passes the type checker and produces an empty list. broken.dhall let RebadgedTextList = (List Text): Type in { emptyList = [] : RebadgedTextList } The broken.dhall produces an error: An empty list requires a type annotation. Expected behavior: broken.dhall should pass the type checker and produce an empty list. Using: dhall-to-yaml v1.2.4 (still latest available on Homebrew) — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#770>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AABRjuTL0Kp-GJrxMl2RhGU4AvFLMFxlks5u-M3sgaJpZM4Zk9DD> .

[oded-dd]

+1

[f-f]

@ari-becker this is a known issue, you might find more info/details in #414

There is also a FAQ entry about this behaviour