links
links copied to clipboard
equirecursive types should be translated away to isorecursive types in the IR
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.