Serokell’s Work on GHC: Dependent Types, Part 5

This article continues the work of Serokell's GHC team in bringing dependent types to Haskell. Since the last report, there have been significant advancements. Vladislav Zavialov discusses three major contributions and numerous smaller improvements that bring Dependent Haskell closer to becoming a practical reality.

Dependent Haskell, as described in GHC Proposal #378 "Design for Dependent Types", incorporates at least six quantifiers. The most important one is the dependent product, dependent function, or Π-type (Π-type), but it's necessary to address other quantifiers like forall a - ty (visible forall or VDQ).

VDQ design questions were resolved with the acceptance of GHC Proposal #281 "Visible forall in types of terms" in 2021. The latest advancement is the implementation of VDQ in GADTs. With the RequiredTypeArguments extension in GHC 9.14, declarations like Typed Int 42 or Typed String "hello" have a dependently-typed appearance.

However, there are technical challenges in handling visible quantification. Adding proper dependent types requires resolving sytnaxic trivia. The first challenge was updating GHC's AST for constructor patterns to use a mixed-list representation. This improvement led to better error messages and the ability to handle visible forall in constructor signatures.

The type checker was updated to allow foralls of varying visibility in the list of quantifiers. This change necessitated mechanical changes throughout the GHC codebase and resulted in cryptic Core Lint errors. With all challenges resolved, GHC can now handle examples that stress-test this feature.

Future work includes nested quantification in GADTs and VDQ in pattern synonyms. Haskell has two namespaces, and when mixing terms and types with DataKinds and RequiredTypeArguments, context is used to select the namespace and avoid ambiguity. The new .. syntax is introduced for namespace-specified imports, and bugs discovered in the import/export logic were addressed to prepare for this feature.