Type-checking a record with Kind as a field value

#1

This is a follow-up to this question.

Does the spec actually prohibit the following?

$ dhall <<< "{a = Kind}"

Use "dhall --explain" for detailed errors

Error: ❰Sort❱ has no type, kind, or sort

1│ {a = Kind}

I’m running into this in the RecordMixedKinds3 type inference failure test, which my implementation is happy to type check at the moment.

#2

{a = Kind} would have type {a : Sort}, but {a : Sort} does not have a type so this should be an error. The Γ ⊢ { x : T, ts… } : i condition checks that any record type we infer should itself have a valid type.
Note that the type-inference/failure/recordOfKind.dhall test tests for this directly. RecordMixedKinds3 (and a few others) is actually badly constructed because it doesn’t actually fail on what its name says. It’s been on my todo list to fix it.

1 Like
#3

Ah, makes sense—somehow I missed that condition. Thanks.