Changes between Initial Version and Version 1 of Ticket #12119, comment 9


Ignore:
Timestamp:
Oct 23, 2018 11:03:23 PM (14 months ago)
Author:
sheaf
Comment:

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #12119, comment 9

    initial v1  
    1 I understand that the type family is injective if I remove the type error. However I would prefer a custom error message, as opposed to the user getting some confusing error about stuck type families.
     1I understand that the type family is injective if I remove the type error.\\
     2However I would prefer a custom error message, as opposed to the user getting some confusing error about a stuck type family application. In my opinion, one of the advantages of injectivity annotation is that internal use of the type family doesn't end up leaking into the front-end.