Tactics plugin cannot derive I from combinators S and K in tagless-final style

[siraben]

Consider

class SKIC repr where
  capp :: repr (a -> b) -> repr a -> repr b
  cK :: repr (a -> b -> a)
  cS :: repr ((a -> b -> c) -> (a -> b) -> a -> c)

cI :: SKIC repr => repr (a -> a)
cI = _

The tactics plugin fails to fill the hole. One potential solution would be

cI = cS `capp` cK `capp` cK

This has been tested as of commit 6c14163. I tested to see if this would be the case in the tagless-final HOAS encoding of lambda calculus as well, but it succeeded, i.e.

class Lam repr where
  app :: repr (a -> b) -> repr a -> repr b
  lam :: (repr a -> repr b) -> repr (a -> b)

id_ :: Lam repr => repr (a -> a)
id_ = _

The plugin generates (lam (\ x -> x)) as a solution.

[isovector]

I think the reason the original one fails to solve is that the auto tactic is running out of gas. We limit solutions at depth <= 4 to ensure a speedy search. It's an easy thing to change, but will exponentially slow down the search times:

haskell-language-server/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs

Line 25 in 6c14163

. localTactic (auto' 4)

[jneira]

Time to add some plugin specific configuration? Or the slowness is so bad that it is not an option?

[isovector]

This turns out to not be an issue of gas at all. What's happening is that Wingman tries each method, and ends up with holes of the form repr a for some to-be-unified variable a. But this could be anything, and Wingman tries really hard not to make big search spaces, so it opts out. I'm not sure if there's a satisfactory solution to be had here; any approach I can think of that would make this work would make the search space exponentially big for all other problems.

[Ailrun]

I also think, as your SKI can represent any 0-th order logic proof, and in general SKI can represent any system that untyped lambda calculus can represent, the search space is too big without any case-specific tactic or exposed tactic language.

[isovector]

That sounds like a convincing argument to me. I'd be interested in exposing the tactic language if there were some way to use source-haskell machinery, instead of me needing to write a little language.