Wingman removes functions in where clauses during refine hole

[santiweight]

foo = undefined
  where
    bar :: Maybe a -> b
    bar = _
      where
        pleaseDontHurtMe = undefined

Refine hole on the only hole (bar = _)

You get:

foo = undefined
  where
    bar :: Maybe a -> b
    bar m_a = _we

@isovector why did you hurt my nested where function :(

This might well be an issue with a Wingman dependency, I don't know Wingman's internals well enough to judge...

[isovector]

Confirmed. Dang, this looks like it's going to be hard to fix.

Nested where doesn't appear to be relevant:

foo :: Int -> Bool
foo = _
  where
    pleaseDontHurtMe = undefined

exhibits the same behavior

[santiweight]

Updated the issue - sucks man :(

I'm surprised to hear that this is a complicated fix... If you need any help/review let me know and I can try to help

[isovector]

My guess is that this is a weird interaction between exactprint (which does the AST manipulation for us) and wingman's "agda-split" machinery responsible for splitting case statements into matches.

[isovector]

But also, what SHOULD wingman do here? In the case of binding arguments I guess we can just add them. But what about if there's a case split?

bar :: Maybe a -> b
bar ma = _
  where
    pleaseDontHurtMe = undefined

should this split into an explicit case statement rather than a match? Otherwise the where clause isn't scoped properly anymore.

[santiweight]

In the case of a case split, my expected behaviour would be that a case statement is used - but that is a good point, wingman is caught between a rock and a hard place.

Otherwise, Wingman could either:

1. provide a "insert case of statement"
2. provide an error if such a situation arises, which fixes the bug quickly

I actually quite like option one personally. I'm the type of person who does single-variable pattern matches with a case of statement, and never via function definition pattern matching (I don't know what that syntax is called). i.e. I prefer:

foo = \case
  Just a -> _
  Nothing -> _

and I less-prefer

foo (Just a) = _
foo Nothing = _

Some problems I foresee would be the Wingman suggestion space outgrowing reason, and implementation difficulty.

[isovector]

The easiest fix today would be to disable match generation in the presence of a where clause. This fixes the problem, at the cost of adding a lambda in the original example. Eg, refining this:

foo :: Int -> Bool
foo = _
  where
    pleaseDontHurtMe = undefined

would produce

foo :: Int -> Bool
foo = \n -> _w1
  where
    pleaseDontHurtMe = undefined

It kinda sucks, but it sucks less than trashing the where clause.

[santiweight]

Agreed - if it's that an easy fix, that would be my vote also.

[santiweight]

Also, HLint will probably eventually help fix this back to a lambda case anyway.

[isovector]

Not the best fix, but it's a fix.