(Solved) Invalid function input

#1

My apologies for the beginner question. Why does the following give an “Invalid function input” error?

let TestConfig =
    { THING = {}
    }

let test = \(thing: TestConfig) -> thing

in test

Error Received

Error: Invalid function input

5│            \(thing: TestConfig) -> thing
6│

./test.dhall:5:12
#2

Seems that it won’t compile because I’m not smart.

let TestConfig =
  { THING : {}
  }


let AppConfig_mongo = \(app: TestConfig) -> app

in {=}

Because was conflating a kind (is this the correct name?) and a value here:

THING = {}
#3

@scull7: Yeah, that is correct. { Thing = {} } and { Thing : {} } are two separate things. The former one is a record literal whose values are types and the latter one is a record type whose field is also a record type.

The latter idiom of { Thing : {} } is much more common, but there are two use-cases for the former idiom of { Thing = {} }:

  • First, Dhall packages are records, so you can think of { Thing = {} } as like a Dhall package that exports a type named Thing

  • Second, you can use a record whose fields are types to name type arguments, like this:

    let Map =
      λ(args : { key : Type, value : Type }) →
        List { mapKey : args.key, mapValue : args.value }

in  toMap { foo = 1 } : Map { key = Text, value = Natural }
1 Like