Fix a bug in tactics preventing split of split

[isovector]

The auto tactic attempts to prune unhelpful branches in order to avoid an exponential blowup of search space. On one these optimizations is to not build a data constructor if it doesn't result in new types to solve. For example, we're trying to avoid the following pathological example:

data Tree a = Leaf a | Branch (Tree a) (Tree a)

-- given the following hole:
pureTree :: a -> Tree a
pureTree a = _

-- we DO NOT want to fill it with
pureTree a = Branch _ _

The reasoning here is that both goals in Branch _ _ have type Tree a, which is already the type we're trying to solve, so introducing Branch doesn't make any progress.

This check is performed in the splitAuto tactic, but I got it backwards and it wasn't explicitly tested for. The only code which hit it was pure @[] --- but because [] doesn't have any subgoals, this hit a vacuous case and flipped the result of the bad logic. Two wrongs made a hard to find bug.

This PR:

1. Fixes the reversed logic in splitAuto
2. Has a special case for nullary data constructors, fixing the bug cause by vacuousness.
3. Adds property tests ensuring we can auto our way through any permutation of a tuple (which is where we originally noticed the bug)
4. Prevents unsafeRender from crashing when unsafeGlobalDynFlags is unset, such as during testing.
5. Moves tactic solution tracing into the plugin, so it won't run during tests.

[jneira]

LGTM

[jneira]

I guess we are still using lsp-test-0.11.0.4 here

Nooope

https://github.com/isovector/haskell-language-server/blob/26aff7dfc46be78428b0ab58e86510819032eabe/stack-8.8.4.yaml#L32 🤔