Sandy Maguire 9a55a8d0ae Fix a bug in tactics preventing split of split (#520) ... 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: ```haskell 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.		2020-10-20 23:40:58 -07:00
..
config.yml	Fix a bug in tactics preventing split of split (#520)	2020-10-20 23:40:58 -07:00