Dependently-typed Core

[christiaanb]

At the moment, the internal Core language of clash is a simple polymorphic calculus, with support for existential types, impredicative types, and higher-rank polymorphism. This is however insufficient to handle GADT pattern matching that is a available in GHC's Core language.

In the long run, we want to have a dependently typed Core language, with dependent pattern matching. That way, we can properly support e.g. GADT pattern matching. We can then also succesfully support translating idris to VHDL.

[Ericson2314]

Might be interesting to to do this in conjunction with https://github.com/goldfirere/ghc/tree/nokinds .

[Ericson2314]

Was this closed by mistake? Ah yes this is a very annoying part of merging repos with github, sigh. Someday I hope some git hoster service thinks of this when designing their issue tracker.

[christiaanb]

Yeah... because I merged the prelude....