I started programming a Haskell-clone recently (source code).
After basic hindley-milner, problems start to arise. Implementation of data/codata statements seem to ensure my language is breaking up on every front.
At this point I seem to lack foundations for the language. System F introduces kinds, but would it be better to approach theorem provers and pick a different calculus as foundation?
Also looking for overall suggestions for this kind of a project.