links icon indicating copy to clipboard operation
links copied to clipboard

equirecursive types should be translated away to isorecursive types in the IR

Open jamescheney opened this issue 5 years ago • 0 comments

As discussed in today's group meeting, recursive types are currently represented (in source and IR typechecking) as cyclic data structures using references. It is desirable to translate all such cyclic types to isorecursive types when generating IR code (or before). This would be good because the IR can easily be extended to handle isorecursive types, but simply ignores any occurrences of equirecusrive types (e.g. type equality gives up and defaults to "true").

Alternatively, the IR type equality checker should be extended to handle equirecursive types using coinduction, as is done (in a more complicated way than needed here) in the source typechecker/type inference code.

jamescheney avatar Jul 02 '20 15:07 jamescheney