Fortunately, we are doing exactly that! We have a paper that formalizes an extremely big part of GHC Haskell’s typesystem, and we are also developing a typechecker that implements this formalism – Kind of like Practical Type Inference for Arbitrary Rank Types but much bigger
The math is nearly finished, and most of my time is currently dedicated to the implementation.
Here are the extensions that the formalism currently specifies:
- ImpredicativeTypes
- RequiredTypeArguments
- ShallowSubsumption
- DeepSubsumption
- Orpatterns
- PatternSignatures
- ViewPatterns
- PatternSynonyms
- PatternSignatureBinds
- GADTs
- Existentials
- RankNTypes
- PolyKinds
- LambdaCase
- LambdaCases
- TypeApplication
- ScopedTypeVariables
- Modern Scoped Type variables (proposal 448)
Things that will be added soon:
- MonoLocalBinds
- Guards
- Implicit Quantification
- Monomorphism restriction
- Levity Polymorphism
One of the main goals of the implementation is to be in a one-to-one – and when possible, even line-to-line – correspondence with the rules.
The paper doesn’t give an specification for kindchecking datatypes, classes, synonyms, pattern synonyms, and type family declarations. Instead, it assumes that these are already in the environment. Also, if I’m not mistaken, the solver is planned to be able to solve everything GHC solves other than FunctionalDependencies and ImplicitParamters. Additionally we might not support representational equality.
Here is the implementation (WIP): typechecker · master · Artin Ghasivand Ghasivand / haskell · GitLab
And here is the early draft of the paper itself: https://gitlab.haskell.org/Ei30metry/haskell/-/jobs/artifacts/master/raw/haskell.pdf?job=build-pdf