Wingman doesn't case split on forall-quantified values

[isovector]

@ssbothwell reports:

import Data.Functor.Contravariant

class Semigroupal cat t1 t2 to f where
  combine :: cat (to (f x y) (f x' y')) (f (t1 x x') (t2 y y'))

comux :: forall p a b c d. Semigroupal Op (,) (,) (,) p => p (a, c) (b, d) -> (p a b, p c d)
comux = _

Wingman can't write this function, even though the implementation is just getOp combine.

[isovector]

But this is odd, because combine is in the hypothesis:

HyInfo 
  { hi_name = combine
  , hi_provenance = ClassMethodPrv Semigroupal
  , hi_type = forall x y x' y'. Op (p x y, p x' y') (p (x, x') (y, y'))
  }

Thus I'd expect Wingman to try destruct combine, resulting in

case combine of
  Op { getOp = x } -> _

and then solve the hole immediately via assumption.

[isovector]

But the desired goal in comux has type p (a, c) (b, d) -> (p a b, p c d), so maybe there's an issue here where either:

1. values with forall types can't be destructed
2. there's a problem unifying the skolemized goal with the forall'd type of x... or is it skolemized here with different skolems? Unclear how the pattern match would/should behave.

[isovector]

Spitting depends on tacticsGetDataCons:

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

Line 61 in 868e476

case tacticsGetDataCons $ unCType t of

which doesn't peek through forall types neither here:

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

Lines 94 to 99 in 868e476

	tacticsGetDataCons ty | Just _ <- algebraicTyCon ty =
	splitTyConApp_maybe ty <&> \(tc, apps) ->
	( filter (not . dataConCannotMatch apps) $ tyConDataCons tc
	, apps
	)
	tacticsGetDataCons _ = Nothing

nor here:

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

Line 135 in 868e476

algebraicTyCon (splitTyConApp_maybe -> Just (tycon, _))

Mystery solved!