Tactics incorrectly synthesizes identity

[isovector]

data Synthesized b a = Synthesized
  { syn_trace :: b
  , syn_val   :: a
  }
  deriving (Eq, Show, Functor, Foldable, Traversable)
  

mapTrace :: (b -> b) -> Synthesized b a -> Synthesized b a
mapTrace = _

Not sure what's going on here; haven't dug in. The real example uses Trace instead of b.

[isovector]

In my currently installed version it produces mapTrace _ sa = sa

[isovector]

[Synthesized {syn_trace = auto
`- intros {frl_crl_c, sa}
   `- destruct(auto)
      `- destruct sa
         `- match Synthesized {rl_c, a}
            `- split(auto)
               `- splitDataCon:Synthesized
                  `- Synthesized
                     `- assume rl_c
, syn_val = \ frl_crl_c sa
  -> case sa of {
       (Synthesized rl_c a)
         -> Synthesized {syn_trace = rl_c, syn_val = a} }},Synthesized {syn_trace = auto
`- intros {frl_crl_c, sa}
   `- assume sa
, syn_val = \ frl_crl_c sa -> sa}]

[isovector]

It's not even trying to apply the function; my guess is that it's a type-synonym problem

[isovector]

It's not a type-synonym problem, and it doesn't appear to be running out of gas --- although I didn't explicitly test it with more gas.

[isovector]

I actually programmed this in intentionally! The offending combinator is requireNewHoles in the apply tactic. In an attempt to prevent infinite regress, we don't apply a function if it doesn't lead to any new holes. This is a good check in general, but should be toned down for locally-bound variables, and make it respect linearity instead.

[isovector]

At the very least, "optimizations" like these should leave a trail somewhere.

[isovector]

The test suite and this failing case both pass after removing requireNewHoles.