Type checker rewrite

[mrjazzybread]

By popular demand 🙂

We have already discussed this at length offline so I won't talk about
motivation for this pull request or the reasoning for some of the
design decisions. Instead, I'm going to go over some of the ways that
this implementation differs (for the better (mostly)) than the
original.

• Documentation. It exists now.

• I have added an ARCHITECTURE.md file to the root of the project
  explaining the implementation in a very high level way as well as
  detailing how a Gospel spec flows through the program. This is not a
  replacement for inline documentation for each module explaining what
  it does but rather a way to talk about the relationship between the
  most critical modules. I also added a section explaining the testing
  framework since when I started I had no idea how it worked (although
  in hindsight it is quite sensible) and I figured this might help
  anyone going through what I did.

• Typing error messages are less specific 🙁 . Less specific because
  unfortunately, if we have situation like 1 + "" we would want to
  print an error saying "Expected type integer but found type string",
  however in Inferno, when two types are not unified, we don't know
  which was expected, so we would have to print a message saying
  "Mismatch between type string and integer". We still have the
  location so we can point the user to where the error happened (check
  the tests to see how the error messages look), but it will be a
  little less explicit about what actually happened.

• Typing error messages are more specific 🙂 We now have a mechanism
  that traverses the two types and checks the first component that is
  not equal. For example, if we have Sequence.singleton 0 = Sequence.singleton "",
  we will print the message "Mismatch between
  string sequence and integer sequence Type string is incompatible
  with integer". Note that this is not specific to Inferno and it
  could have been done in the previous implementation.

• Generated type variable names are a bit more readable. Before, when
  the Gospel type checker would generate a new name, it would be
  always be 'aN where N would be some number. This would be a bit
  annoying because eventually the N's would get into the hundreds and
  the error messages would become pretty noisy. Additionally, it
  would make translations into Rocq extremely annoying since the names
  of the type variables would change when you added new type
  definitions. Now, names are generated like the OCaml compiler does
  where it starts with 'a then 'b then 'c, etc… This mechanism is
  strong enough to allow for an arbitrary amount of generated type
  variables (although I haven't tested this fully).

• The standard library is now part of the compilation
  chain. Previously, if you made a change that messed up the standard
  library, Gospel would not complain but when you tried to type check
  any file it would complain that the standard library did not
  exists. Now the standard library is type checked whenever we compile
  Gospel and is loaded from a marshalled file at run time.

• Although I haven't changed the testing infrastructure (I made a few
  tweaks to the code but nothing that changed the underlying
  behaviour) I have added my own tests and pretty much abandoned the
  previous ones. Although I have a similar amount of tests that
  current Gospel has (about 200 and something), keep in mind that I
  have only implemented a relatively small fraction of what current
  Gospel has. I wanted to write more but I was already taking too long
  to do this PR 😬.

• If a user writes M1.M2.x, these module accesses will still appear in
  the typed tree. I'm not sure why the previous version of Gospel
  didn't do this but it also made translations into Rocq more annoying
  then they had to be. Additionally, when a user binds some variable
  to some type such as x : M.t1 and M.t1 is an alias for t2, the typed
  AST will contain both the annotation the user wrote (M.t1) as well as
  the alias (t2).

• When typechecking Gospel, we still generate a marshalled file, but
  now I insert it into a _gospel directory. Because of this, I had to
  increase the OCaml version since the mk_dir function only became
  available on 4.14, surprisingly.

And those are the important bits that I have done. As you can see, these
are A LOT of commits so it is impossible to describe in full detail
what I have done, but these are the highlights.

[mariojppereira]

Hello everyone,

First, kudos to @mrjazzybread on this huge effort to rewrite the entire Gospel type-checker!

I am merging this PR, even if the CI is not giving us the green light. But it seems like an internal error. It fails immediately with an obscure error message, so I really believe this one is not on our side.