You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Thinking of a function as a constructive existence proof (if there is an Input, then there is an Output, and here it is), it seems to make sense to say "if there is an instance self of Never, then there is an instance of Never, namely self". Alternatively, it also seems to make sense (by the principle of explosion) to infer the existence of anything at all. It seems like it's a matter of whether or not the coder chooses to make use of the fact that the impossible has happened (so anything goes). So maybe both should be permitted?
Additional Detail from JIRA
md5: 76040ca317b49c0fc1ba64f1a48f8d59
relates to:
return
in functions that take an uninhabited typeIssue Description:
The following code does not compile but should
The diagnostic says
The text was updated successfully, but these errors were encountered: