What is the kind of a hole type? about primer HOT 2 CLOSED

In hackworthltd/vonnegut#291, we introduce a kind hole, to classify type holes. We don't do any fancy smart-holes stuff though.

The following is mostly a rehash of Harry's comment above.

The reason we introduce it is to enable type applications to be formed: consider wanting to write foo : List Bool. We start with foo : ?, and must respect the invariant that whatever type we write has kind KType. We would like to refine the hole to be a type application foo : ?1 ?2, but this requires ?1 to have an arrow kind, rather than KType.

Thus we just say type holes have kind holes, which are consistent with any kind, so ?1 ?2 ∈ KHole ~ KType is fine. We can then fill in ?1 = List and ?2 = Bool.

Another choice could be for every type hole to carry its kind in the AST, so we would start foo : ?#KType, and when doing a type application in a hole ?#kt we would require a kind ks and form ?#(ks->kt) ?#ks. The UI could also offer the choice of giving either the head or the arguments, for example in the hole ?#KType, we could hit type app and get given the options

• [ k ]: ?#(k -> KType) ?#k, where the square brackets denote some sort of "kind inputter"
• List ?#KType, as List has the right kind. In general either 1 option per well-kinded type in scope, or a dropdown or something
• ?#(KType -> KType) Bool, and also for Int (Perhaps a dropdown?)
• ?#((KType -> KType) -> KType) List and also for Maybe (Perhaps part of the previous options)

from primer.

Closing as we made the choice to have kind holes (in the sense of one flavor of kind hole which is consistent with all kinds), and implemented it ages ago. I don't think there is anything else to consider here. Feel free to reopen if I am mistaken!

from primer.