Recognize parallel datatypes with args type-level equality

[colin-mcd]

Right now in our Agda implementation, we have a module parameter functor for the span monad, where we use the IO monad when we want to write to send progress updates to the front end, and the id monad when we simply want to check something and get a pure result. This works great, except for when we want to convert from a datatype from a module imported with IO to the same datatype from the same module, but this time imported with id. For example, Agda says that toplevel-state IO is distinct from toplevel-state id, even though the datatypes do not contain anything of type spanM [IO/id].

After having to deal with this annoyance, I think that it would be reasonable to implement a fix for this same problem in Cedille. We would need to check both if two datatypes are essentially the same—just with different constructor names—and also only check that arguments to the datatypes are the same if they occur free somewhere in the constructors (it could happen as well that they do occur free as arguments to some other datatype where they are irrelevant, though, so we'd want to check for this as well?)

[astump]

In general, recognizing that two datatype declarations are the same (up to conversion), and then treating the actual datatypes (D1 and D2, say) as convertible.

Not quite sure, but could be useful.