Tactics plugin returns wrong result for program

[siraben]

Given

safeHead :: [x] -> Maybe x
safeHead = _

We expect a program equivalent to the following to be synthesized (i.e. respects naturality condition)

safeHead :: [x] -> Maybe x
safeHead = \ l_x
  -> case l_x of
       [] -> Nothing
       ((:) x l_x2) -> Just x

And indeed, this is one of the candidate programs as shown in the stderr output below. However the tactics engine produces

safeHead :: [x] -> Maybe x
safeHead = (\ l_x -> Nothing)

stderr output

!!!goal: Judgement {_jHypothesis = fromList [], _jDestructed = fromList [], _jPatternVals = fromList [], _jBlacklistDestruct = False, _jWhitelistSplit = True, _jPositionMaps = fromList [(safeHead,[[]])], _jAncestry = fromList [], _jIsTopHole = True, _jGoal = [x] -> Maybe x}
!!!ctx: [(safeHead,[x] -> Maybe x)]
!!!solns: (auto
`- intros {l_x}
   `- destruct(auto)
      `- destruct l_x
         +- match [] {}
         |  `- split(auto)
         |     `- splitDataCon:Nothing
         |        `- Nothing
         `- match : {x, l_x2}
            `- split(auto)
               `- splitDataCon:Nothing
                  `- Nothing
,\ l_x
  -> case l_x of
       [] -> Nothing
       ((:) x l_x2) -> Nothing)
(auto
`- intros {l_x}
   `- destruct(auto)
      `- destruct l_x
         +- match [] {}
         |  `- split(auto)
         |     `- splitDataCon:Nothing
         |        `- Nothing
         `- match : {x, l_x2}
            `- split(auto)
               `- splitDataCon:Just
                  `- Just
                     `- assume x
,\ l_x
  -> case l_x of
       [] -> Nothing
       ((:) x l_x2) -> Just x)
(auto
`- intros {l_x}
   `- destruct(auto)
      `- destruct l_x
         +- match [] {}
         |  `- split(auto)
         |     `- splitDataCon:Nothing
         |        `- Nothing
         `- match : {x, l_x2}
            `- recursion
               `- apply' safeHead
                  `- assume l_x2
,\ l_x
  -> case l_x of
       [] -> Nothing
       ((:) x l_x2) -> safeHead l_x2)
(auto
`- intros {l_x}
   `- split(auto)
      `- splitDataCon:Nothing
         `- Nothing
,\ l_x -> Nothing)

Subject of the issue

Describe your issue here.

Your environment

• Output of haskell-language-server --probe-tools or haskell-language-server-wrapper --probe-tools
  • This command is available since version >= 0.4.0.0

haskell-language-server --probe-tools
haskell-language-server version: 0.5.1.0 (GHC: 8.8.4) (PATH: /nix/store/ffh2c9zmq8f4nh6ya5v505lb2viyvqsy-haskell-language-server-ghc884/bin/haskell-language-server)
Tool versions found on the $PATH
cabal:		3.2.0.0
stack:		Not found
ghc:		8.8.4

• Which lsp-client do you use
  • emacs
• Describe your project
  • Just a single file Haskell program with the code above.

Steps to reproduce

As above.

[isovector]

I can repro this; debug dump:

!!!goal: Judgement {_jHypothesis = fromList [], _jAmbientHypothesis = fromList [], _jDestructed = fromList [], _jPatternVals = fromList [], _jBlacklistDestruct = False, _jWhitelistSplit = True, _jPositionMaps = fromList [(safeHead,[[]])], _jAncestry = fromList [], _jIsTopHole = True, _jGoal = [a] -> Maybe a}
!!!ctx: [(safeHead,[a] -> Maybe a)]
!!!solns: [
(auto
`- intros {l_a}
   `- destruct(auto)
      `- destruct l_a
         +- match [] {}
         |  `- split(auto)
         |     `- splitDataCon:Nothing
         |        `- Nothing
         `- match : {a, l_a2}
            `- split(auto)
               `- splitDataCon:Nothing
                  `- Nothing
,\ l_a
  -> case l_a of
       [] -> Nothing
       (a : l_a2) -> Nothing)
,(auto           <------------------------------ this is the desired solution
`- intros {l_a}
   `- destruct(auto)
      `- destruct l_a
         +- match [] {}
         |  `- split(auto)
         |     `- splitDataCon:Nothing
         |        `- Nothing
         `- match : {a, l_a2}
            `- split(auto)
               `- splitDataCon:Just
                  `- Just
                     `- assume a
,\ l_a
  -> case l_a of
       [] -> Nothing
      (a : l_a2) -> Just a)
,(auto
`- intros {l_a}
   `- destruct(auto)
      `- destruct l_a
         +- match [] {}
         |  `- split(auto)
         |     `- splitDataCon:Nothing
         |        `- Nothing
         `- match : {a, l_a2}
            `- recursion
               `- apply' safeHead
                  `- assume l_a2
,\ l_a
  -> case l_a of
       [] -> Nothing
       (a : l_a2) -> safeHead l_a2)
,(auto
`- intros {l_a}
   `- split(auto)
      `- splitDataCon:Nothing
         `- Nothing
,\ l_a -> Nothing)]

We're finding the right solution, but for whatever reason, scoreSolution is rating it too low.

[isovector]

A low impact solution here might be to penalize unused top-level position binds immediately after penalizing holes.

EDIT: But we don't have access to the position binds if they were introduced via intros, since this occurs only in the judgement.

@TOTBWF any clever ideas?

[isovector]

The score for the winning solution is (Penalize 0,Reward False,Penalize 1,Reward 0,Penalize 13), vs the desired solution's (Penalize 0,Reward False,Penalize 3,Reward 2,Penalize 126), where the scoring metric is:

       ( Penalize Int  -- number of holes
       , Reward Bool   -- all bindings used
       , Penalize Int  -- number of introduced bindings
       , Reward Int    -- number used bindings
       , Penalize Int  -- size of extract
       )

[wz1000]

What about Reward fraction_of_used_bindings as a replacement for "all bindings used", "number of introduced bindings" and "number of used bindings"?

[wz1000]

another one to consider is Penalize (introduced_bindings - used_bindings)