Add README.md to extra-doc-files.

Bump versions.

Directly parse types to TypeTLen, not Mod NameTy.

Remove dependency on ghc-prim.

Bump versions.

Move the Cabal description to Markdown.

Integrate types to the module system.

Remove unused GHC extensions.

Rename inj_* -> *Inj.

Rename source -> withSource, and g_*.

Polish comments.

Remove Proxy in Sym instances.

Polish for publication.

Add make target %/fast.

Add display exception for the list type [].

Fix Dim.

Use symantic-document to write docType.

Add replicate.

Fix handling of Fixity in showType.

Add Config_showType.

Use AllowAmbiguousTypes to avoid Proxy uses.

Change Term to be a GADT, to avoid type applications and allow TypeOf Term.

Fix symantic-lib tests.

Fix symantic-grammar test.

Put symantic-document before symantic and symantic-lib.

Remove debugging entry map_f.

Fix description.

Bump versions.

Add symantic-document.

Add some Eq and Show instances.

Improve dynamic insertion of terms (via CtxTy or Modules).

Clarification : Megaparsec integration.

Clarification : eqKi -> eqKind.

Improve the module system.

Improve handling of metadata in grammars.

Support directories as targets in GNUmakefile.

Massive rewrite to better support rank-1 polymorphic types.

Try the new Type and Term design against the actual needs.

Improve Show of Type.

Archive old attempt to remove proto tokens without polymorphic types.

Cleanup dead-end attempts.

Complexify the type system to support rank-1 polymorphic types and terms.

With polymorphic types now expressible,
the proto token workaround should be removable,
since every token should now be able to directly have a Type/Term,
thus no longer needing to be applied to a few others before having it.

As a consequence of merging Type and Term,
the symantic machinery will have to be moved to TeSym,
and thus also carried by Type. WIP.

Try to implement polymorphic types.

Fix prefix/postfix operators wrt. term application.

Add compileWithTyCtx.

Add support for (>=>).

Add GNUmakefile rule : tag.

Fix Mono{Foldable,Functor} and {Semi,Is}Sequence constraints.

Cleaner to support the constraints
in the various data types' Proj_TyConC
instead of the constraints'.
For instance, this avoids to require the IO TyConst
when using MonoFunctor.

Add withContext.

Fix stack clean.

Rename grammar rules, prefixing them with g_.

Rename Term_Name -> TeName

Add IsString instances.

Fix time&space explosion of GHC's typechecker.

Add Lib.{Bounded,Enum,Ratio,Rational,Real,Semigroup}.

Fix comment typo.

Fix lexeme to progress over indented lines.

Renaming Constants -> TyConsts.

Cosmetic cleanup of GHC flags.

Add GNUmakefile.

Cosmetic cleanup.

Fix Inj_ConstP -> Inj_TyConstP.

Use AllowAmbiguousTypes to avoid using Proxy.

Cosmetic cleanup.

Fix empty and eoi.

Backtrack (try) the grammar only when necessary to get better error messages.

Gather type declarations and infix declarations.

Reduce compile time of tests with -O0 -fmax-simplifier-iterations=0.

Split into symantic{,-grammar,-lib}.

Bump version.

Renames.

Polish doc.

Add optional.

Add stack.yaml.

Update doc.

Fix Lib.Ord : Ordering.

Fix module including.

Use more TypeApplications.

Remove Alternative uses in grammars.

Fix Lib.Text.

Move libraries in Lib.

Add Gram_Term.

Add Parsing.Grammar.

Fix comment typo.

Add Compiling.Alternative.

Renaming textI_app* to textI*.

Clarify names, and add commentaries (bis).

Clarify names, and add commentaries.

Add Compiling.Show.

Add Parsing.Token.

Add Compiling.Sequences.

Add Compiling.NonNull.

Add Compiling.MonoFoldable.

Add Typing.Family and Compiling.MonoFunctor.

Add tests for Compiling.

Fix lambda application.

Use GHC-8.0.1's TypeInType to handle kinds better, and migrate Compiling.

Add Compiling, Interpreting and Transforming.

Simplify the Constraint projection

Revamp the type system.

This is definitively much more correct, simple and powerful this way:
kinds are now properly handled,
type constraints capture is now quite neat,
and usable type variables should be possible.

Though the current code may seem obvious and natural
for the task at hand, it required
first to know that this was indeed this task that has to be done…

Indeed I was previously much more focused on the symantics part,
but this happened when I decided to put a day or two
to check if type inferencing would indeed be possible with the previous type system,
I rapidly convinced myself that I couldn't handle type variables as required,
so I then put aside the previous type system to work anew
from the main (mono)type of Top,
which also appears in Write You a Haskell:

data Type
 =   TVar TVar
 |   TCon String
 |   TArr Type Type

As in the previous type system,
I first tried to have Type indexing an Haskell type (h)
by using the usual GADTs way,
which was surprisingly possible for every kind:
once I realized this could be done through Proxy
(this definitively is a very important type
to compute with GHC's type system),
and found that the type application could be handled
with a type family, which could effectively let me build types
from an AST, the type family's result just stays abstract,
and GADTs put constraints in scope with it in them.

The Index GADT of GLambda was my inspiration to handle type constants
through a type list of them, and thus drop the previous approach
which was indexing types (and not type constants)
and required much more code.

I then tried to have Type always well-formed through GADTs,
my first attempt was (stupidly) to only check the arity,
then I realized it was not enough and introduced a Kind type.

At this point I was able to kindcheck an AST of a type,
but failed to replicate the previous approach to capture a Constraint,
hopefully I then tried (without much hope it would work)
to do the "obvious thing" (since this is what GHC does),
that is to add a type constraint kind into Kind,
which proved itself quite rewarding.
Surprisingly I've quickly found that introducing UnProxy
enables to capture Constraints which need to work on abstract types,
like (Eq a) to prove (Eq (Maybe a)).

Work ahead is to try to update the previous approach
to build expressions with symantics.
Then later to try again type inferencing.

Cheers :-)