Add a README file for the implementation

typechecker/README.md

+Implementation of the spec
+==========================
+
+The implementaiton of our specification of GHC's typechecker.
+
+We use several notations to connect different parts of the implementation with the paper.
+
+## Disclaimer
+- The compiler doesn't have a runtime yet. It can only typecheck files.
+- There is no support for modules yet.
+- We can only typecheck value declarations and type signatures. All of the datatypes and classes are hardcoded in the compiler. Look at `./src/Type.hs` and `./src/Initial.hs`.
+
+## Buliding
+Requirements:
+ - ghc 9.10.1
+ - cabal 3.12.1.0 or later
+
+You can either use `make` or `cabal build` to build the project
+
+## Testsuite
+The testsuite uses [golden files](https://ro-che.info/articles/2017-12-04-golden-tests) which are organized into the following directories:
+- `./test/cases/should-typecheck`
+- `./test/cases/should-fail`
+- `./test/cases/parser`
+
+We don't treat the tests we expect fail any differently than those we expect to pass. This is just a convention to navigate tests more conviniently.
+
+### Running the testsuite
+To run all of the tests you can run either of the following:
+- `cabal test`
+- `make run-tests`
+
+To run a specific you can use `cabal test --test-options="-p TESTNAME"`
+
+### Addding tests
+To add a test, add the test-file to one of the test directories, and write the expected output to a file with the same name but with a `.output` extension instead of `.hs`.
+If you don't do this, the testsuite will create the output file and write the generated output to it.
+
+*IMPORTANT*: It is important that the `.output` files don't contain any trailing newlines in them.
+
+## Directory structure
+- Constraint generator: `./src/Tc/Gen/*`
+- Constraint solver:    `./src/Tc/Solver/*`
+- Parser:               `./src/Parser.hs`
+- Tests:                `./test/cases/*`
+
+## Notations
+1. Functions that implement the judgements are always of the form `tcJUDGEMENT`. Exampls
+- `tcMatches`  --> `|-matches`
+- `tcPat`      --> `|-pat`
+- `tcExpr`     --> `|-expr`
+
+2. Equations, or guarded-expressions that implement a cetain rule, are annoated with haddock documents of the form: `-- | Rule: JUDGEMENT-RULE`.
+Examples:
+- Match-Infer  --> `-- | Rule: Match-Infer`
+- Pat-ConCheck --> `-- | Rule: Pat-ConCheck`
+
+3. When referring to a certain part -- where part is either a guarded expression or a pattern match-equation -- of a _function_we refer to that part using the notation `funcname-JUDGEMENT-Rule`.
+Examples:
+- `tcSkolAPats-SkolAPats-Specified`
+- `tcInst-Inst-Infer`
+
+4. Every judgement related function has a header that corresponds to the judgement boxes in our figures.
+
+Example:
+```haskell
+{- *********************************************************************
+*                                                                      *
+*                     Gamma |-expr expr :_delta rho                    *
+*                                                                      *
+********************************************************************* -}
+
+tcExpr :: Gamma -> Expr -> ExpType -> Tc ()
+
+-- | Rule: Expr-App
+tcExpr gamma (TApp head args) expType = do
+  sigma <- tcHeadExpr gamma head
+  traceTc "tcExpr-Expr-App" $
+    vsep [pretty "Application head:" <+> pprHead head <+> pretty ':' <+> (pprSigma sigma)
+         ,pretty "Application args:" <+> pprArgs args]
+  (exprs, phis) <- tcInst gamma sigma args expType
+  mapM_ (uncurry $ tcArg gamma) $ zip exprs phis
+
+-- | Rule: Expr-SuperLambda
+tcExpr gamma (TSuperLambda matches) expType
+  = tcMatches gamma matches expType
+
+-- | Rule: Expr-Let
+tcExpr gamma (TLet valDecls expr) expType = do
+  vars <- tcValDecls gamma valDecls
+  traceTc "tcExpr-Expr-Let" (pprVarBindingsV vars)
+  tcExpr (modifyDelta (modifyVariables (<> vars)) gamma ) expr expType
+
+.
+.
+.
+```

typechecker/test/cases/should-fail/arityMismatch-check.hs

+arityMismatch :: Integer -> Integer -> Integer
+arityMismatch 0 = const 3
+arityMismatch 1 1 = 3

typechecker/test/cases/should-fail/arityMismatch-check.output

+TODO: Fix me
+[InsolubleWC]
+
+wcImplics = []
+wcSimples = []
\ No newline at end of file