On Feb 28, 2021, at 3:25 AM, Ben Franksen <ben.franksen@online.de> wrote:

What are these other GHC features? Does the paper explain this?
Otherwise where can I read more about it?

I think it was data families. But, perhaps more troublesome is the fact that the paper assumes a dependently-typed internal language. Maybe it's possible to do this without dependent types in the internal language, but I'm not sure how to begin to think about that problem.

I was about to write that it might be helpful to have a GHC proposal to implement this paper, which would depend on (and provide further motivation for)  having dependent types... but I'm not actually sure that would be productive at this point.

I have spent some time thinking about how to clear my decks to make more time for implementation work, and I expect to prioritize this more going forward.

Richard