Interesting idea. Not sure if the motivation is strong enough, but perhaps it is. I have a few technical questions:

• How does this interact with Qualified do #216? That is, if Qualified do #216 is accepted, then is this proposal unmotivated? You hint at this in the proposal itself, but it looks to me that Qualified do #216 is likely, and so I'd want to know your stance on combining the two.

• The current fail behavior works very well for e.g. Maybe and [] monads. It seems potentially dangerous to specify -XNoFallibleDo for a whole module and then silently cause good uses of incomplete pattern matches in Maybe or [] do-blocks to suddenly throw exceptions.

• How does this interact with -XMonadComprehensions? Right now, a monad comprehension is a direct generalization of a list comprehension. But I normally think of a monad comprehension as alternative syntax for do-notation. Incomplete patterns are vital in list comprehensions, and so it would be very strange if -XNoFallibleDo affected those. So there is something here that doesn't fit.

The current fail behavior works very well for e.g. Maybe and [] monads.

I would say it works well only with MonadZero, which begs some questions. For example, the most convenient thing it automatically does provide line numbers, but those line numbers are only useful for the non-MonadZero case. Awkward...

How does this interact with -XMonadComprehensions?

I believe today Monad comprehensions and List Comprehensions are implemented differently with respect warnings, so there is already some precedent for this. I think we kept MonadComprehensions like do notation (no fail) and ListComprensions like today (yes mzero).

How does this interact with #216?

If we think in backpack terms, (or "meta type class" if one prefers), #216 is about providing the module instantiation (resp. class == meta instance), whereas this is about choosing the signature (resp. meta class).

But frankly, I don't see see this as about making a more flexible do notation, but about fixing a wart in the language. [Disclaimer I might be more extreme than Cale and others.] fail is, to me, a terrible method, and while thankfully it is now quarantined in MonadFail, that doesn't make any less bad, just less damaging.

As the question often goes today, if we didn't have MonadFail.fail today, and someone proposed adding it with its:

• lousy textual interface (I'm willing to pretend it's Text rather than String) for sake of argument

• difficulty of inference https://gitlab.haskell.org/ghc/ghc/issues/15681#note_165441 (whole thread, but that comment especially)

• aforementioned weird relationship to MonadZero

Would we accept this half-baked sugar? Absolutely not, I'd think.

I'm all for having composable, resuable, insert good adjective syntactic sugar for various mathematical structures---way beyond restricted Monads. But I don't think we can get there incrementally based of our current legacy designs---I think it's going to take some meta-programming research not n-year FooBarProposal deprecation cycles.

More -XNo* allows us up to pack up and get ready for some future PhD to lead use out of the wilderness.

Interesting idea. Not sure if the motivation is strong enough, but perhaps it is. I have a few technical questions:

* How does this interact with #216? That is, if #216 is accepted, then is this proposal unmotivated? You hint at this in the proposal itself, but it looks to me that #216 is likely, and so I'd want to know your stance on combining the two.

Yeah, if #216 gets done, then the implementation of fail could be redirected with a qualified do-block in those cases which are presently problematic. I think the explicit qualification is unlikely to be too much of an issue (though I'm not sure, some people might disagree), and the fact that in this case, we want the standard meanings for everything apart from fail means that things are even nicer than the average use of #216. (I was unaware of that proposal before now, or else I'd certainly have mentioned it in the alternatives section!)

I'm looking at this entire proposal as a stopgap measure anyway, so if something that grants more general control over the meaning of the syntax ends up landing in GHC soonish, it should both be easy for MIRI's fork to switch to it, and solve the same problem for everyone else easily enough, so I wouldn't personally have any issue with it.

* The current `fail` behavior works very well for e.g. `Maybe` and `[]` monads. It seems potentially dangerous to specify `-XNoFallibleDo` for a whole module and then silently cause good uses of incomplete pattern matches in `Maybe` or `[]` `do`-blocks to suddenly throw exceptions.

Indeed, you wouldn't want to use NoFallibleDo in modules where the behaviour of fail was indeed important. I'd say probably greater than 95% of the modules I work on involve no use of monads where the fail is anything more than a potential convenient way to get a line number in an error message. But indeed, care would have to be taken by anyone toggling the flag.

* How does this interact with `-XMonadComprehensions`? Right now, a monad comprehension is a direct generalization of a list comprehension. But I normally think of a monad comprehension as alternative syntax for `do`-notation. Incomplete patterns are vital in list comprehensions, and so it would be very strange if `-XNoFallibleDo` affected those. So there is something here that doesn't fit.

That's actually one of the hanging threads in our implementation at the moment, but I'd probably lean toward the change just having no impact on the translation of MonadComprehensions. I agree that if you are using MonadComprehensions, you probably do want some sort of nicer treatment of failed pattern matches, and this would even leave that syntax open for use in case you discovered need for, I don't know, StateT s [] with some implicit backtracking on pattern match failure in the midst of code that did use NoFallibleDo.

@Ericson2314

I would say it works well only with MonadZero, which begs some questions. For example, the most convenient thing it automatically does provide line numbers, but those line numbers are only useful for the non-MonadFail case. Awkward...

This text seems swapped around, to me. Line numbers are useful only in the non-MonadZero case, right? I just want to make sure I'm understanding you correctly.

Monad comprehensions and List Comprehensions are implemented differently with respect warnings

Do you mean in GHC? Or in your fork?

it is now quarantined in MonadFail, that doesn't make any less bad, just less damaging.

I think a proposal to put fail into Monad would not be viewed kindly. But something fail-like (maybe with a more structured argument) in MonadFail makes sense. Users can always opt out by avoiding a MonadFail constraint. The problem you're trying to address is that you want to use failable patterns but without fail -- because you know, by some reasoning beyond GHC's capabilities at the moment, that the pattern won't fail.

That last observation leads me to suggest a much simpler workaround: lazy patterns. That is, instead of saying

foo = do
  A z <- blah
  ...

say

foo = do
  ~(A z) <- blah
  ...

• Downside: looks closer to line noise. z may be a thunk, and I don't see an easy way to force it without a separate line that forces it.

• Upsides: Works out of the box, no change to GHC required. Visibly signals to readers that the pattern match cannot fail. Local: you can make the decision separately per pattern match. Syntactically lightweight.

What do you think of this workaround?

@goldfirere lazy patterns don't work with GADTs

lazy patterns don't work with GADTs

Silly me. Of course. I've started work on a paper to address that (among other issues), even.

But it actually suggests an alternative design. Instead of marking a whole module as treating pattern-matches in do-notation differently -- and potentially affecting innocuous uses of such a construct -- could we label the pattern-match directly? This is syntactically loud, but what about

foo = do
  {-# COMPLETE #-} A z <- blah
  ...

I'm abusing the idea of COMPLETE here. But it wouldn't conflict with {-# COMPLETE ... #-}'s current usage, and it seems to have the right intuition. Maybe some different syntactic marker would be better.

How common are these matches in practice?

This text seems swapped around, to me. Line numbers are useful only in the non-MonadZero case, right? I just want to make sure I'm understanding you correctly.

Yes indeed, sorry about that.

Do you mean in GHC? Or in your fork?

I mean in GHC.

The problem you're trying to address is that you want to use failable patterns but without fail -- because you know, by some reasoning beyond GHC's capabilities at the moment, that the pattern won't fail.

Well to be clear, I always intend to use at least -Werror=incomplete-patterns and -Werror=incomplete-uni-patterns. I don't think anyone should be throwing and catching PatternMatchFail, but we figured that would be way to make this the most like other patterns.

foo = do
  {-# COMPLETE #-} A z <- blah
  ...

I suppose this works, but this seems awfully heavyweight, and "anti huffman". In general, complete pattern matches definitely should be norm and path of least resistance, while the incomplete ones should be the weird ones with the many loud capital letters. Kinda like how C having const rather than mut is a perverse incentive.

I never ever want MonadFail, so I am fine to just doing

foo = do
  before...
  n <- blah >>= \case
    A n -> pure n
    _ -> manualErrorHandling
  rest...

or

foo = do
  before...
  n <- blah >>= \case
    A n -> do
      rest...
    _ -> manualErrorHandling

If there is any sugar I'd want, it would be some way to mark a "default case" to avoid repeating bound variables or rightward drift. Something like:

foo = do
  before...
  case A n <- blah of
    _ -> manualErrorHandling
  rest...

I'm perfectly happy to call fail throw or Left myself; that was never the annoying part.

I appreciate your observation about incentivizing good behavior.

But I'm thrown off the scent now: if you're happy to do the manual error-handling yourself, why do you want this new extension?

I'm also confused now about -Wincomplete-uni-patterns. It turns out that this flag does not warn about incomplete uni-patterns in do-blocks, quite possibly because incomplete uni-patterns in do-blocks are sometimes very appropriate. So I don't see how your promise to use -Wincomplete-uni-patterns interacts with this proposal.

I was thinking, briefly, of suggesting that -Werror=incomplete-uni-patterns could allow GHC to use error instead of fail, because the code would be dead regardless. (That's poor design, having a warning flag affect the typing rules. So I don't really mean it. But the idea of configuring GHC to make a certain construct illegal and then avoid fail does have merit.) But with incomplete-uni-patterns not working with do means that this approach is dead, too.

@goldfirere I'm only speculating, but I'm quite sure Obsidian folks have problems with
https://hackage.haskell.org/package/some-1.0.1/docs/Data-Some-Newtype.html

newtype Some tag = UnsafeSome (tag Any)

{-# COMPLETE Some #-}
pattern Some :: tag a -> Some tag
pattern Some x <- UnsafeSome x
  where Some x = UnsafeSome ((unsafeCoerce :: tag a -> tag Any) x)

See https://gitlab.haskell.org/ghc/ghc/issues/1965

Where with GADT variant one could write

do Some x <- foo
   Some y <- bar
   doSomethingWith x y

and refinement would work, with above cheat-performant implementation of
Some one would need to use

-- this is in fact safe.
withSome :: Some tag -> (forall a. tag a -> b) -> b
withSome (UnsafeSome thing) some = some (unsafeCoerce thing)

withSomeM :: Monad m => m (Some tag) -> (forall a. tag a -> m r) -> m r
withSomeM m k = m >>= \s -> withSome s k

so the code would look like

do withSomeM foo $ \x ->
   withSomeM bar $ \y ->
   doSomethingWith x y

i.e. no benefit of do notation at all.

Personally I think it is not that bad, that I would rather use NoFallibleDo. I do use Maybe monad often in the same files, e.g. Just Refl <- ... stuff for type equalities.

TL;DR this is the gist of https://gitlab.haskell.org/ghc/ghc/issues/15681

The proposal would benefit from more clearer and "real" motivational examples. Also from links to GHC issues it allows to work around.

The motivation for our work on this came from MIRI hiring us to come up with and implement some solution to the issues mentioned in the Motivation section (and on the GHC issue that @phadej already linked to), rather than anything internal to Obsidian Systems, so for this one I don't actually have practical examples handy from my own usage of the language. Despite using Some quite a lot, I hadn't run into any issues with pattern matching completeness there (but it makes sense that I could eventually run into it). This proposal mostly exists because this is work that is happening regardless, so that people can decide if it would be a desirable inclusion into GHC proper. My own impression is that I could go either way on it, though I do have some sympathy for @Ericson2314 's view of gradually enabling a very cut-down version of Haskell via various language extensions. It seems probable to me that #216 would see more actual use though.

I entirely agree that practical examples would be nice to have. It also would have been good motivation for our role in this, but the code which induced them to pay us to make this change presumably isn't open source. Perhaps we can get someone from over there to comment on this proposal in any case though.

@goldfirere

But I'm thrown off the scent now: if you're happy to do the manual error-handling yourself, why do you want this new extension?

I'm also confused now about -Wincomplete-uni-patterns. It turns out that this flag does not warn about incomplete uni-patterns in do-blocks, quite possibly because incomplete uni-patterns in do-blocks are sometimes very appropriate. So I don't see how your promise to use -Wincomplete-uni-patterns interacts with this proposal.

Ah so we have a rather buried sentence on this we should bring to the fore:

Moreover, when the -Wincomplete-uni-patterns warning flag is enabled alongside NoFallibleDo, we will warn about the incomplete pattern match.

Here's my train of thought:

1. Partial pattern matching is bad
2. We have effective means to catch it today
3. Partial pattern matching in do blocks is also bad because fail is bad
4. For consistency, fix the fail problem just like we do with the other unintended pattern fallibility.
   • Throw PatternMatchFailure to avoid type inference + exhaustiveness checking Gordian knot
   • -Werror=... will catch, like everything else which throws PatternMatchFailure
   • idiomatic Haskell as always doesn't throw PatternMatchFailure in practice

So one could disparage the PatternMatchFailure as this straw-man intermediate step that's solely down for consistency.

One idea that this conversation has led me to: imagine that #216 is adopted. We might like to implement fail via throw in some module so that QualifiedDo syntax could basically implement this proposal here. This would however leave out the potentially useful warning when GHC failed to verify that your pattern matches were complete. But why should it have to? We have custom type errors, but why not custom warnings?

If, by way of analogy with the existing

type family TypeError (msg :: ErrorMessage) :: k

we had

type family Warning (msg :: ErrorMessage) :: Constraint

which is a constraint that is trivially solvable by printing a warning message, then we could have:

fail :: Warning (Text "Incomplete pattern match in do-expression") => String -> m ()
fail s = throw (PatternMatchFailure s)

alongside a re-export of ordinary (>>=), and that would then behave quite similarly to this proposal, only at the expression-level rather than the module-level.

To be clear, #216 on it's own is not enough, because once again you are at the mercy of the compiler as to when M.fail is used, just as today you are for fail.

@Ericson2314 Um, but you're at the mercy of the compiler as to when the case expression involving throw gets generated with this proposal as well... it's just that we've selected an expression that has less of an impact on the type signature, as M.fail might do as well.

And with #216 you can say noFail.do ..., and then that do-block can use error instead of fail -- exactly as proposed here. As I see it, the only difference between this proposal and using #216 to accomplish the same goal is that with #216, you have to annotate each do separately, instead of declaring it all at the top of the module.

@goldfirere there are some subtleties in that only post type checking can we properly decide what's fallible, so we have to make sure that the the errors can be freely added and remove without influencing the types of the adjacent time. The old Monad.fail had that property. Throwing exceptions "purely", and -Werror making any residual throws into compile-time errors, also both have that properly.

#216 however, which is essentially qualified rebindable syntax IIUC, certainly doesn't. Maybe certain instances do like Cale's example, but modifying the desugaring based on whether the user-passed identifers pass a sort of subsumption check sounds quite complex.

I think I might go over the motivation and alternatives to clear up some of these things from the discussion; each change in the proposal is rather simple, but the sum total of their interactions certainly isn't.

I should clarify: When I'm thinking that #216 solves this problem, I mean to have it in concert with an ability to report warnings for incomplete pattern matches in do-blocks, above and beyond what -Wincomplete-uni-patterns does now. So we have a noFail.do block which inserts error instead of fail (without any change to typing), but we also have a way for GHC to report whether any matches fails. I had not quite realized this was what I was thinking, and the change to the warning system would indeed be a new feature. And, for it to work best, it would have to be somehow controlled by the noFail prefix to the do block.

Here's an idea: what if we have something like

data NoFail m = NoFail { bind :: forall a b. m a -> (a -> m b) -> m b, then :: ..., fail :: TypeError "incomplete pattern match" => String -> m a }

I'm not sure if the current setup around TypeError is the right one that will work here, but the idea is to have a constraint that reports an error if and only if it is used outside of dead code. Such a constraint would be useful well beyond this proposal. But I think if we had it (and maybe TypeError is this -- not sure), then I think we'd be able to address the motivations of this proposal nicely (with #216).

I still think trying to use some sort of magic constraint is disingenuous. There's two routes:

1. The fail term is considered during type checking, but we make the type checker ignore the constraint (or it's trivially globally given)

2. The desugarer special cases this constraint and emits errors rather than dictionary args, if the exhaustiveness checker didn't remove it already.

3. The fail term is ignored during type checking

4. The desugarer places the term anywhere it cannot prove exhaustiveness. The constraint is again ignored (doesn't become a dictionary) and instead errors are emitted.

In both cases, the "constraint" precisely never is handled like other constraints in any meaningful way. I think it would be more honest to just have a magic term: "blow up if this makes throw the desugarer". I know I've wanted a similar "blow up if this isn't optimized away" in the past.

Still, I think that given most Haskellers are against "syntactically silent" partiality, the sort of "grand plan" I'd hope for is:

1. NoFallibleDo

2. (Optional) New sugar

   case A n <- blah of
     pat0 -> manualErrorHandling0
     ...

3. (Optional) A MonadZeroDo controlled by a either zdo (like mdo), or some Qualified do #216-like mechanism. Also would be used my list comprehensions, and maybe monad comprehensions. Unlike today, there would be no heuristics in the type checker re exhaustiveness: type checking simply always requires MonadZero for these blocks.

4. -Werror=incomplete-patterns and -Werror=incomplete-uni-patterns is on by default. -fdefer-exhaustivness-errors, analogous to -fdefer-type-error gets us back the old behavior. Flipping the default indicates that both -fdefer-* are slap-dash tricks to do during the development process, and not idiomatic.

5. NoFallibleDo on by default in future language standard.

I think this because

• Respects reader's desire to know at a glance where code may blow up without extra care from the author
• Avoids heuristics duplicating other logic (type checker fake exhaustiveness check)
• Avoids String in desugaring
• The nice MonadZero case for lightweight failure fail still is syntactically explicit---but on the block level rather than individual bind level in order to stay lightweight.

I'm afraid I don't understand #319 (comment) without examples. :(

The "new sugar" is well approximated by e.g.

foo = do
  x <- blah
  y <- blah2 x >>= \case
    pat1 -> ...
    pat2 -> ...
  ...

That's a bit ugly, granted, but I'm not sure it's worth sugaring over.

Happy to consider making pattern-match incompleteness a hard error.

I have to say it sounds more and more that what you want is just to stop GHC from accepting incomplete pattern matches in do blocks altogether. That is: don't replace fail with error; just issue a type error if there is a failible pattern match. If that were the case, and you did want to really match, you could manually write a case.

I'm afraid I don't understand #319 (comment) without examples. :(

I am not sure what example to write, since this deals with the internals of the compiler and it's many intermediate representations rather than the surface syntax? But I could point in our PR out the key points in GHC whose behavior determines which flavor of this proposal or the discussion's proposals is implemented. Alternatively, I'd be happy to hop on IRC and just explain and reference those spots it in real time. (I think the latter might be more efficient, if you don't mind.)

The "new sugar" is

I edited in an "(Optional)" for "new sugar" part. I do like it, but for the sake of this argument it is a palliative for not having the fail desugar, not essential.

I have to say it sounds more and more that what you want is just to stop GHC from accepting incomplete pattern matches in do blocks altogether. That is: don't replace fail with error; just issue a type error if there is a fallible pattern match. If that were the case, and you did want to really match, you could manually write a case.

Yes that is true. All that business with the PatternMatchFailure was just done for consistency with -Werror=incompete-patterns -Werror=incompete-uni-patterns being the current way to ban incomplete patterns, not because anyone I know likes PatternMatchFailure.

We could "jump ahead" in the grand plan to just banning them outright with -XNoFallibleDo, assuming long term something like the -fdefer-exhaustivness-errors change would fix the inconsistency of different knobs (-Werror=.. vs -XNoFallibleDo) effecting whether incomplete patterns are allowed .

I remain unconvinced -- but perhaps I've been too loud. Let's hear from other voices, while I take a step back from this proposal. Happy to take another look if this is revised or submitted to the committee.

I think you are saying that...

All I meant is it appears we must have either #327 or %FallibleDo to get this accepted. I must admit I would prefer to land and then figure out exactly what we want, as #327/%FallibleDo has plenty to bikeshed while this alone does not, but landing this without a concrete #327/%FallibleDo plan (which is what I was calling the "opt-in", perhaps to loosely) was deemed too fork-like.

Conversely, just a local, opt-in %NoFallibleDo would get annoying pretty quickly (I certainly would forget to decorate all my do blocks with it) and we'll probably see demand for a module-wide flag like -XNoFallibleDo anyway after we have #327.

:) Agree completely.

It seems like everyone can have their cake and eat it, too.

...

What do we think?

Sorry, I just came back from vacation, and I'm getting back to my sepherding tasks.

Honestly, I think that is too complicated, since there's a very subtle interaction between default modes (which can be enabled via Cabal files and at the top of the module) and possible modifiers. Furthermore, we are somehow overriding the usual behavior of -XNoSomething, because -XFallibleDo seems to be different than dropping -XNoFallibleDo.

I also got the feeling that the proponents are too keen on breaking backwards compatibility. However, I think the proposal is not strong enough on that respect; and this doesn't seem (in my very subjective view) something the community has complained too much about.

I'm not sure what to do then, the above seems like a fundamental impasse

However, I think the proposal is not strong enough on that respect; and this doesn't seem (in my very subjective view) something the community has complained too much about.

To me, this proposal feels like the sort of unglamorous maintaincence work that isn't super noticable or widely desired, but is nonetheless important to keep things working smoothly (in this case reining in accumulated complexity).

We have a situation where small decisions over time have created something very weird and out of step with the our general principals — and ad-hoc approximation of a type directed desugaring. In fixing this we affirm our values and reclaim our complexity budget for other things in this area.

Furthermore, we are somehow overriding the usual behavior of -XNoSomething, because -XFallibleDo seems to be different than dropping -XNoFallibleDo.

May I ask why that is the case? If -XFallibleDo is enabled by default (and retains the current behavior), as suggested in the proposal, then I wonder how we could observe a difference if code or cmd flags never mention FallibleDo.

Genuine questions popping into my head:

1. Maybe you are thinking of cabal's other-extension field? I'm not completely familiar with how relevant that is
2. Is there a flag -fdeactivate-all-extensions that makes the behavior observable?
3. I think the procedure has precedent in -XNoStarIsType (part of Embrace (Type :: Type) #83, I believe). Why was it OK there? Did -XNoStarIsType cause back compat issues (well, apart from the migration plan in conjunction with -XTypeOperators)?
4. Note that this proposal is not about migrating to -XNoFallibleDo as the default, I think. Would it be better if we reversed and said -XNonFallibleDo to opt in? With -XNoNonFallibleDo being the default. I think the proposal wants to avoid the double negative, but then again we already have something similar with -XNondecreasingIndentation...

I do admit the strictly speaking, the implicit fail or pattern match failure are not compatible extensions of the other, and only compatible extensions against regime where incomplete bind patterns are rejected at compile time (so the extensions just allow previously rejected programs). But we would need the recently rejected -XNoIncomplete to fully formalize that at the language extension level!

@cgibbard @Ericson2314 I've realized that there has been some time since we last discussed about this. Is the linked version the latest one? Do you want to re-apply for Committee review?

We could do another round, but I am not sure we've meaningfully moved on form the old impasse. If I understand correctly:

1. @goldfirere proposed compromise of modifiers and changeable "default".
2. You would like to see just the modifier, and think modifier + different default is too fork-like or too many knobs.
3. @sgraf812 and I think this is a worthy cleanup even without and modifier escape hatch, and while we are willing to oblige your/the commitee's desire for an escape hatch, we think WIP: Case bind #327 (which works for individual binds, and allows decently succinctly but also explicitly saying exactly what one wants) is a better feature than a do-block-wide modifier.

@serras has called for a vote on this (thanks, @serras), and I have voted to reject, for the following reasons:

• The current proposal suggests too global a change: a full module is a big thing, and contains many do expressions. We should not have a file-sized switch apply to all such expressions. (Yes, we have other such switches, but I hate all of them, and recent proposals have, piece by piece, tried to localize them.)
• This proposal does seem (almost) subsumed by Qualified do #216, with the new addition of Unsatisfiable #433. Qualified do #216 (accepted, implemented, released) proposes -XQualifiedDo that allows a user to change the symbols used in desugaring do. It would be easy to have a fail :: Unsatisfiable (Text ...) => String -> m a (and I could support having a base module export the right symbols to make this easy). This would allow users to choose the desugaring per do. The only problem is one highlighted in the proposal as an Alternative: the heuristic insertion of fail might cause Unsatisfiable errors spuriously. But I think there's an easy solution to that: just amend Unsatisfiable #433 to say that an Unsatisfiable constraint in inaccessible code does not produce an error. (In fact, I'm quite surprised Unsatisfiable #433 doesn't already say that, and have looked several times but can't find it. @adamgundry?)
• Failing that, there is always WIP: Case bind #327, which would allow for a syntax where the behavior on a failing match is made explicit. Pairing that with a warning (in -Weverything only) every time GHC inserts a fail, and I think we're in good shape.

I'm sympathetic to the goals here, but I think there are more compelling ways to achieve those goals than what's proposed here.

But I think there's an easy solution to that: just amend Unsatisfiable #433 to say that an Unsatisfiable constraint in inaccessible code does not produce an error. (In fact, I'm quite surprised Unsatisfiable #433 doesn't already say that, and have looked several times but can't find it. @adamgundry?)

Unsatisfiable doesn't do this as far as I can remember. And I'm not convinced we want this to be specific to Unsatisfiable: after all, couldn't one equally well say that inaccessible code is not type-checked at all, and should never produce any type errors? https://gitlab.haskell.org/ghc/ghc/-/issues/17543 is relevant.

Dear authors: the Committee has agreed to reject this proposal. Several of us see #327 as a better solution to this problem, so we encourage collaboration in that regard.

I...didn't know this was in the committee review state? If #327 got finished, my plan was return to this, as I viewed it as a complementary not an alternative. I thought the impasse was mainly #327 vs modifiers vs punt, so doing #327 would make this potentially viable.

Would it be possible to reopen the proposal in some fashion if #327 we're accepted?

(Reading the committee emails I see

case C x1 … xn <- u of {}

as the reason #327 could do this on it's own. I didn't think of that before, and seeing it now, I do see why #327 could, strictly speaking, serve as an alternative. But, I doubt that is practical given how much more verbose it is. A core philosophical point with this stuff is that total binds are the common case, and therefore they deserve the concise syntax to steer people in the right direction.)

Ah in particular, @serras asked

I've realized that there has been some time since we last discussed about this. Is the linked version the latest one? Do you want to re-apply for Committee review?

And my reply not clear. I meant to say "I think we are still at this impasse: ..., let's hold off until something changes", but what came across is probably more "grrr I have nothing more to say, let's just go to a vote".

Sorry I only wrote the "this is the impasse" part and didn't answer the second part, and sorry I missed the earlier calling for a vote.

Apologies if there was a miscommunication. The rejection of course applies to this proposal, so if something changes (the proposed change, or other related assumptions that led to the rejection), we can discuss it of course again.

@Ericson2314 sorry on my side, I indeed interpreted your comment as marking the proposal as ready for another round of review. As @nomeata says, we are open to discussing the proposal again.

Thanks for the replies.

I suppose I am also curious on the criteria for proposals.

Reading the emails from last month, it seems a big issue was that it was too late to change the nature of do notation. However I earlier had seen my #285 accepted, of which -XNoImplicitForAll is a far more invasive break from Haskell. While it will be practically necessary for pun-free Dependent Haskell, I don't see it having a route to being on by default later.

That one is still not implemented, but living on as #448 where it is important to help put some of the principles in context. I might add that while -XScopedTypeVariables at least isn't on by default, switching from it to the new better version proposed in #448 will, as a practical matter, also take a lot of work.

My experience with #285 taught me that there was some appetite or at least allowance for "restriction of Haskell" extensions that might never be able to become the default, but would be very useful for groups of people trying to code in a certain style. And in general, the entire experience with #378 that eventually went through led me to believe there was some willingness allow certain "vanguard" groups to rethink old parts of Haskell to explore what might be the best ideom.

Without sounding too bitter, is the steering committee now of a new opinion on these things? Or does these seem different than those in some key ways I am missing?

If it helps, I am not just hoping to relitigate proposals like this one. I would like to keep on writing -XNo proposals like https://twitter.com/kmett/status/1479314977626505218 so as to continue to enforce (subjectively) good style, cutting the marble block down into language I wish we had. But if there is no appetite for more -XNo..., then it would be good to know before taking the time to write such proposals.

Talking just on my name (not on behalf of the Committee), there were several reasons that weighted in.

• First of all, I consider that we can allow more in the type level, where Haskell is still quite exploratory, than in the term level.
• I tend to see patterns such as Just x <- f x as bad code style. My personal preference is to pattern match and then made the outcome explicit, whereas it is an exception or any other problem. This extension makes me chose between a call to fail and a "pattern match fail" exception, but those are still only two options. This is why want WIP: Case bind #327.
• Finally, I think that the proposal as it stands is too global. In this regard we are trying to move from "an extension changes the whole file" to more localized pragmas (as we have now for overlapping instances, and has been proposed for qualified do's or ambiguous type signatures.)

@serras

Thanks for responding to me on these things.

First of all, I consider that we can allow more in the type level, where Haskell is still quite exploratory, than in the term level.

OK this make sense.

I tend to see patterns such as Just x <- f x as bad code style.

Oh, I somehow did not realize that. Me too! hat is also part of my motivation.

Quite on the contrary, the impression I got was you thought it was a fine thing to do.

Finally, I think that the proposal as it stands is too global.

How does this square with the above for you? For me, it is precisely because I view Just x <- f y as bad style that fine-grained configuration wasn't attractive to me. Being fine-grained to me says "oh this is fine style in some situations", which isn't a very clear moral message.

"pattern match fail" exception

The pattern match fail exception was written with -XNoIncomplete (#351) in mind, but that proposal was rejected. If this proposal went back to making pattern match failure an error, would that make a difference for you? E.g. might it send a clearer message that Just x <- f x is just bad and we don't want it?

(I am still conscientious of the incongruity of making just one thing in the language require complete patterns. And the complaint in #351 that pattern match exhaustiveness is too under-specified to be part of a language extension would equally apply here. But I think I have a path to making a new better specified version of -XNoIncomplete that would require absurd patterns (or really "absurd alternatives"). I would then have the option of making -XNoFallibleDo require -XNoIncomplete, which would avoid both the weird pattern match failure business and introducing design incongruity.)

Speaking for myself (like @serras, not for the committee), I have an appetite for more -XNo proposals.

Maybe this would have been different for me if the proposal stated loudly that Just x <- f y was an antipattern. We could decide whether we agreed with that statement (it's certainly not an antipattern for me in a list or monad comprehension... though I sometimes use it in a Maybe-do) and then decided whether banning the construct was a good idea. Without the overarching statement that such matches are an antipattern, it seems odd to switch it off for an entire file. That, really, was my biggest complaint: that this proposal was too global, affecting the whole file -- and without any way to override the change locally. If we want to just say that Just x <- f y is a misfeature (or, rather, the interpretation of such a pattern-match as a potential call to fail) and that we should remove the misfeature, that's a different conversation.

As stated, the motivation is to give programmers the option of how to treat a Just x <- f y match. That choice should be per-do, where it is more adequately handled (in my opinion) by e.g. -XQualifiedDo.

Do keep the proposals coming, though. I know it is frustrating to put time into these to have them rejected. I do think that, generally, you (@Ericson2314) and I want similar things for the language -- we just have to figure out how to get the design right.

Yeah this sounds increasingly like there was mainly a messaging issue here where I just didn't write down the big subjective "Just x <- f y, is bad, y'all!", focusing too much on all the objective reasons it was unwieldy without getting down the the punchline.

That's actually reassuring! It leads me to think the "V2" I outlined above would at least spur a very different conversation.

@goldfirere

Just x <- f y is a misfeature (or, rather, the interpretation of such a pattern-match as a potential call to fail)

I'd say that's a misfeature in the do-notation.

Though, it is a feature in list comprehensions.
Our problem is that these two things have been conceived as the same concept historically. And since we can implement list comprehensions withdo-notation, it is hard to get rid of the misfeature easily. Still, I would have thought that a by-default-off-language extension NoFallibleDo could have been the way to proceed.
One would have to be careful while switching it on. Maybe some warning or linting tool could help find do-blocks that could be meant as List/Maybe comprehensions with partial matches, and warn about them.

P.S.: When I write Just x <- f y I want to say that I reasoned that Nothing is impossible.