Serokell publica la quinta entrega de su serie sobre tipos dependientes en Haskell, centrada en el trabajo que Vladislav Zavialov y su equipo desarrollan en el compilador GHC. El artículo detalla tres contribuciones principales y varias mejoras secundarias que acercan Dependent Haskell a una realidad práctica.
El eje de la actualización es la incorporación de forall visible (VDQ) en los GADTs a partir de GHC 9.14. Esto permite que un constructor de datos declare argumentos de tipo seguidos de argumentos de término, como Typed :: forall a -> a -> T a, de modo que expresiones como Typed Int 42 o Typed String "hello" sean válidas. Aunque el argumento de tipo sigue siendo borrado y no puede aparecer en pattern matching, la sintaxis elimina obstáculos técnicos de cara a futuros tipos dependientes plenos. Los autores explican los tres retos resueltos: refactorizar la representación del AST para mezclar argumentos de tipo y de término, permitir forall visible en las signaturas de constructores y actualizar la representación Core para soportar cuantificadores de visibilidad variable.
La segunda gran aportación son los imports con espacio de nombres explícito, regulados por la propuesta #581 de GHC. La sintaxis import Data.Monoid as M.Type (type ..) o import Data.Monoid as M (data ..) permite importar selectivamente nombres del espacio de tipos o de datos y resolver ambigüedades que aparecen al combinar términos y tipos con DataKinds y RequiredTypeArguments.
El texto también cubre otras mejoras: instancias de tipo en kind checking, unificación de HsType y HsExpr, sintaxis de estrella en argumentos requeridos, detección de puns y nuevas type families (Tuple, Constraints, Tuple#, Sum#).