Hello friends, I’m working on adding a type infer pass that supports mutually recursive functions in Relay.
However, the type_infer pass seems to use some in-between implementation of Algorithm W and Wand’s Algorithm and isn’t very unintuitive. I made a WIP https://github.com/apache/incubator-tvm/pull/5881, but need some help pointing me in the right direction. Would love some insight!
I don’t know how helpful this will be since it’s old, but I had an ancient abandoned PR that tried to add in mutual recursion. I ran into some unification bugs that I documented in the comments, but maybe those have since been fixed. Seems like it has to do with type variables (the woes of dependent typing).
To understand Relay’s type-checking, I think reading the arxiv paper might help (it uses Hindley-Milner for getting types that don’t involve relations and constraint-solving for the rest).
To be clear, it seems like I was able to get my cludge of a solution to “work” but it required annotating more types than I thought it should. It might be that this is the best we can do, but the lack of graceful errors (again, at the time – I know @jroesch has done a lot of work to improve Relay’s error reporting) made that extremely impractical.
Maybe just encouraging (or even requiring) types to be annotated when mutual recursion is at play will sidestep a lot of issues with checking those.