Tactics plugin generates ill-typed term

[siraben]

Given

foo :: Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
foo f g a = _

We expect a program equivalent to the following to be synthesized.

foo :: Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
foo f g a = f a >>= g

However the tactics engine produces

foo :: Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
foo f g a = (f a)

which is ill-typed.

stderr output

!!!goal: Judgement {_jHypothesis = fromList [(a,a),(f,a -> m b),(g,b -> m c)], _jAmbientHypothesis = fromList [(*>,forall a b. m a -> m b -> m b),(<$,forall a b. a -> m b -> m a),(<*,forall a b. m a -> m b -> m a),(<*>,forall a b. m (a -> b) -> m a -> m b),(>>,forall a b. m a -> m b -> m b),(>>=,forall a b. m a -> (a -> m b) -> m b),(fmap,forall a b. (a -> b) -> m a -> m b),(liftA2,forall a b c. (a -> b -> c) -> m a -> m b -> m c),(pure,forall a. a -> m a),(return,forall a. a -> m a)], _jDestructed = fromList [], _jPatternVals = fromList [], _jBlacklistDestruct = False, _jWhitelistSplit = True, _jPositionMaps = fromList [(foo,[[f,g,a]])], _jAncestry = fromList [], _jIsTopHole = True, _jGoal = m c}
!!!ctx: [(foo,(a -> m b) -> (b -> m c) -> a -> m c)]
!!!solns: [(auto
`- apply' *>
   +- assume a
   `- apply' g
      `- assume *>
,(*>) a (g (*>))),(auto
`- apply' >>=
   +- assume a
   `- assume g
,(>>=) a g),(auto
`- apply' g
   `- assume a
,g a),(auto
`- apply' f
   `- assume g
,f g),(auto
`- apply' f
   `- assume a
,f a)]

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]

😱

[isovector]

Interestingly, this behavior requires having bound the parameters yourself. Tactics will fail to find a solution if it does intros itself. Which probably means the position mapping is using variables that aren't the skolems we have in scope.

[isovector]

Fixed in #542; I was doing something dumb when tracking skolems.