Editable typedefs: deletion

[georgefst]

From "not in spec" section of #267:

The deletion of parts of a type definition is harder to handle, since we want to avoid the student losing code that they've written. In addition to the operations outlined above, the following are also possible:

• Delete type
• Delete constructor
• Delete parameter from constructor
• Delete parameter from type
  • Concerns about losing code are somewhat lesser here in practice, but a student could in theory have an arbitrarily-complex type-level expression in a no-longer-required type application.
  • Note that we can only allow this when the parameter does not appear in any constructors. Or at least, we should remove the parameter from any constructors automatically as a first step.

We should consider these alongside other changes which can cause code to disappear. See Saving the student's work when a type changes.

[brprice]

@georgefst Could you update us on the status of this?

IIUC, we support deletions of "unused" types/constructors/parameters-of-ctors/parameters-of-types?

[georgefst]

Yes, we now support deleting parts of unused typedefs. This was implemented in #1063 and got a bit lost in the Zurihac maelstrom.

The check is not as fine-grained as it could be (e.g. we should be able to delete an unused constructor even when its type is in use - #1063 (comment)).

Anyway, we're now intending to just warn about more destructive deletions, instead of banning them. See #1133.

[georgefst]

I consider #1153 to close this issue, since all that now remains is tracked in #1133 and #402.