Wingman won't apply return-type-polymorphic functions, even if they're the only things that would typecheck

[isovector]

@masaeedu reports:

module Foo where

newtype Flip t a b = Flip { unFlip :: t b a }

newtype Co b f = Co { runCo :: forall r. b (Compose (Flip (->) r) f) -> r }

-- Records or products, pick one

data Something f = TheInt (f Int) | TheString (f String)

getTheInt :: Co Something f -> f Int
getTheInt (Co f) = f $ TheInt $ Compose $ Flip id

getTheString :: Co Something f -> f String
getTheString (Co f) = f $ TheString $ Compose $ Flip id

buildSomething :: (x -> f Int) -> (x -> f String) -> x -> Co Something f
buildSomething f g x = Co $ \case
  TheInt (Compose (Flip fi)) -> fi $ f x
  TheString (Compose (Flip fs)) -> fs $ g x

data SomethingElse f = SomethingElse { theInt :: f Int, theString :: f String }

buildAnInt :: f Int -> Co SomethingElse f
buildAnInt i = Co $ \SomethingElse { theInt = Compose (Flip x) } -> x i

buildAString :: f String -> Co SomethingElse f
buildAString s = Co $ \SomethingElse { theString = Compose (Flip x) } -> x s

matchSomethingElse :: (f Int -> r) -> (f String -> r) -> Co SomethingElse f -> r
matchSomethingElse f g (Co c) = c $ SomethingElse
  { theInt = Compose $ Flip f
  , theString = Compose $ Flip g
  }

fwd :: Co (Co Something) f -> Something f
fwd (Co c) = c $ Co $ \case
  TheInt (Compose (Flip fi)) -> fi $ Compose $ Flip TheInt
  TheString (Compose (Flip fs)) -> fs $ Compose $ Flip TheString

bwd :: Something f -> Co (Co Something) f
bwd = \case
  TheInt fi -> Co $ \(Co c) -> c $ TheInt $ Compose $ Flip $ \(Compose (Flip f)) -> f fi
  TheString fs -> Co $ \(Co c) -> c $ TheString $ Compose $ Flip $ \(Compose (Flip f)) -> f fs

Wingman should be able to produce fwd and bwd if given enough gas, but it doesn't! It gets stuck applying c, failing with a TooPolymorphic error. This appears to be caused by the call to requireConcreteHole in apply, which doesn't allow return-type-polymorphic calls. I've forgotten the original impetus for this, but it appears to be related to #534, and presumably to prevent Wingman from wasting its time solving holes via read and unsafeCoerce.

But there's another bug corresponding to requireConcreteHole:

haskell-language-server/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs

Lines 64 to 65 in 1e47c75

	-- TODO(sandy): This tactic doesn't fire for the @AutoThetaFix@ golden test,
	-- presumably due to running afoul of 'requireConcreteHole'. Look into this!

which suggests we're barking up the entirely wrong tree with this check.

I think it's reasonable to requireConcreteHoles when applying non-local definitions, which would still rule out read and unsafeCoerce, but will allow recursion and application.