I'm messing about with a possible new core for Idris. I've got this far. It's surprising what you need to do to get this far...
Conversation
This rather ridiculous example typechecks about 30 times faster than Blodwen, so it's possible I should keep going on this one...
3
20
Any inspiration taken from smalltt?
1
4
Yes, it preserves sharing of metavariables. Also I took the chance to represent global names more sensibly. It might get trickier when I add linearity checking, we'll see.
2
5
Replying to
Cool! Should let know the good news!
I still need to figure out metavariable solving, so I've not run into the fun of these performance problems yet! 😁