Unions don't seem to be typechecked correctly

[majk-p]

In the following Dhall expression:

let Package =
      < GitHub : { repository : Text, revision : Text }
      >

in [ Package.GitHub { repository = {} } ]

We should get a type error because of repository not being a Text, and revision being missing. Dhall's editor on the website says:

Error: Wrong type of function argument

{ - revision : …
,   repository : - Text
                 + Type
}

5│      Package.GitHub { repository = {} }

(input):5:6

Instead, if I try to normalize this expression and encode it as JSON using the circe encoder:

import $ivy.`org.dhallj::dhall-scala:0.8.0-M1`
import $ivy.`org.dhallj::dhall-circe:0.8.0-M1`

import org.dhallj.parser.DhallParser._

val input = """
let Package =
      < GitHub : { repository : Text, revision : Text }
      >

in [ Package.GitHub { repository = {} } ]
"""

import org.dhallj.circe.Converter

println(parse(input))
println(parse(input).normalize)
println(Converter(parse(input).normalize))

The last line prints:

Some([
  {
    
  }
])

The result of normalization prints as [(<GitHub : {repository : Text, revision : Text}>.GitHub) {repository = {}}].

If I skip repository = {} completely, I get Some([\n]).

If Package is just a record and not a union, it works as expected.

[travisbrown]

What you're describing is 100% intended behavior, since the conversion operations provided by Dhall for Java do not type-check their inputs. For example [1, True] is a Dhall expression that does not type-check:

scala> import org.dhallj.syntax._
import org.dhallj.syntax._

scala> val Right(expr) = "[1, True]".parseExpr
val expr: org.dhallj.core.Expr = [1, True]

scala> expr.typeCheck
val res1: Either[org.dhallj.core.typechecking.TypeCheckFailure,org.dhallj.core.Expr] = Left(org.dhallj.core.typechecking.TypeCheckFailure: List elements should all have the same type)

You can still do many things with it, though:

scala> expr.normalize
val res1: org.dhallj.core.Expr = [1, True]

scala> expr.diff(expr)
val res2: Option[(Option[org.dhallj.core.Expr], Option[org.dhallj.core.Expr])] = None

scala> import org.dhallj.circe.Converter
import org.dhallj.circe.Converter

scala> Converter(expr)
val res3: Option[io.circe.Json] =
Some([
  1,
  true
])

This approach isn't specific to Dhall for Java. If you pipe [1, True] to the standard dhall CLI, you'll get a type-check error, but if you pipe it to dhall encode --json, for example, you'll get a JSON representation of the CBOR encoding of the Dhall expression, with no warning, even though it's not well-typed. This also works for your example:

$ echo "let Package = < GitHub : { repository : Text, revision : Text } > in [ Package.GitHub { repository = {} } ]" | dhall encode --json
[
    25,
    "Package",
    null,
    [
    ...
                        "repository": [
                        7,
                        {}
                    ]
    ...
]

There's no indication that the {} part doesn't have a valid type.

It's even possible to construct Dhall expressions that are ill-typed but become well-typed after normalization (e.g. let foo = bar in 1). If you want the tooling you're building to indicate these failures to the user, you'll have to type-check before normalization.

The idea in general is that components like Converter are intended to be parts of larger tools, where it's up to you as the tool implementer to decide whether you need to type-check the Expr inputs or not. If you do, you can include a call to typeCheck in the pipeline, and it'll fail as expected:

scala> val bad = "let Package = < GitHub : { repository : Text, revision : Text } > in [ Package.GitHub { repository = {} } ]"
val bad: String = let Package = < GitHub : { repository : Text, revision : Text } > in [ Package.GitHub { repository = {} } ]

scala> val Right(badExpr) = bad.parseExpr
val badExpr: org.dhallj.core.Expr = let Package = <GitHub : {repository : Text, revision : Text}> in [(Package.GitHub) {repository = {}}]

scala> badExpr.typeCheck
val res4: Either[org.dhallj.core.typechecking.TypeCheckFailure,org.dhallj.core.Expr] = Left(org.dhallj.core.typechecking.TypeCheckFailure: Wrong type of function argument)

It's possible this could be better documented, either here or in the general Dhall documentation, but the behavior itself won't change, so I'm closing this issue.

[majk-p]

Thank you for the detailed explanation, my Dhall knowledge is far from perfect. Definitely doesn't look like bug in dhallj then 👍