Following the success of term-level visible type application in letting users specify type arguments in polymorphic function applications, requests were made to extend this to type-level, leading to a GHC proposal. The talk introduces this new language feature – visible kind application – which allows explicit instantiation of kind arguments in kind polymorphic cases in type level programming. I will explain the motivation for this feature, providing examples where it helps produce concise type-checked programs, especially in situations where the ability to use polymorphism or typecheck is hindered by the lack of explicit kind arguments.

There will be an implementation overview as well as design choices made to keep the feature consistent with the current GHC Haskell and Template Haskell. Users can enable visible kind applications by adding TypeApplications in LANGUAGE pragma or flag -XTypeApplications. The syntax is @k where @ is preceded by a white space. This is in line with the current term-level visible type application, and hopefully with visible type application in patterns in the very near future. To conclude the talk, I will share my experience as an undergraduate working with GHC for the first time, hopefully encouraging more new-comers to contribute to GHC.