Tactics plugin generates ill-typed term

[siraben]

Given

import Data.Functor.Compose
data Fix f a = Fix (Compose f (Fix f) a)
instance Functor f => Functor (Fix f) where
  fmap f (Fix x) = _

We expect a program equivalent to the following to be synthesized.

instance Functor f => Functor (Fix f) where
  fmap f (Fix x) = Fix (fmap f x)

However the tactics engine produces

instance Functor f => Functor (Fix f) where
  fmap f (Fix x) = (case x of { (Compose x2) -> Compose x2 })

which is ill-typed.

stderr output

!!!goal: Judgement {_jHypothesis = fromList [(f,HyInfo {hi_provenance = UserPrv, hi_type = a -> b}),(x,HyInfo {hi_provenance = UserPrv, hi_type = Compose f (Fix f) a})], _jBlacklistDestruct = False, _jWhitelistSplit = True, _jIsTopHole = True, _jGoal = Fix f b}
!!!ctx: [(fmap,(a -> b) -> Fix f a -> Fix f b)]
!!!skolems: fromList [f,a,b]
!!!solns: [(known fmap
`- homo
   `- destruct x
      `- match Compose {x2}
         `- Compose
            `- assume x2
,case x of { (Compose x2) -> Compose x2 })]

Related to #561.
This has been tested as of commit 6c14163.

[isovector]

I think I know what's going wrong here. Does it work instead if you don't bind the Fix x pattern, or if you change the name of fmap?

[isovector]

Tactics has support for so-called "known" derivations, which use the function name to prune the search and ignore obviously wrong solutions. You're hitting the known fmap case, which runs

  try intros
  overAlgebraicTerms homo
  choice
    [ applying >> auto' 2
    , assumption
    , recursion
    ]

here the only thing to homomorphism over is x, which is what produces the Compose -> Compose case. This can't happen if you don't bind x yourself (it gets a UserPrv provenance in the hypothesis), and should then fail the known case. At that point it should fall back to the usual auto machinery and derive properly.

[jneira]

last wingman changes does not fix it (or at least provide other workaround via metaprograming)?

[isovector]

I think the real bug here is that homo doesn't verify that you can use a data constructor in the hole. Probably an extremely easy fix.