Tactics plugin cannot derive program under certain constraints and bindings

[siraben]

Consider

-- succeeds
join_ :: Monad m => m (m a) -> m a
join_ = _

The tactics plugin produces the solution (\ x -> (>>=) x (\ x11 -> x11)). However, now consider

-- fails
fJoin :: (Monad m, Monad f) => f (m (m a)) -> f (m a)
fJoin = fmap _

The type of _ is still m (m a) -> m a (with Monad constraint on m), but the tactics plugin fails to find the solution. I tried moving it into a let binding but it still fails.

-- fails
fJoin :: (Monad m, Monad f) => f (m (m a)) -> f (m a)
fJoin = let f = _ in fmap f

However if we generalize the constraint on f to Functor, the tactics plugin succeeds;

-- succeeds
fJoin :: (Monad m, Functor f) => f (m (m a)) -> f (m a)
fJoin = fmap _

Is solved with _ = (\ x -> (>>=) x (\ x11 -> x11)). However moving it into a let binding again causes a failure!

-- fails
fJoin :: (Monad m, Functor f) => f (m (m a)) -> f (m a)
fJoin = let f = _ in fmap f

This has been tested as of commit 6c14163.

[isovector]

What does fails mean, here? Is it timing out or not finding any solutions? Stderr should tell you.

Please post the reported !!!goal written to stderr for each case as well.

[siraben]

Not finding solutions. I'll update the issue with what stderr reports.

[isovector]

My guess is that this is again caused by overlapping names in the hypothesis. Tactics unpacks a given constraint's methods into specialized arguments in the hypothesis, meaning it can't currently deal with two givens of the same class for different types. One will always overlap the other.

I suspect what's going on between Monad f and Functor f is that it somehow changes the order in which these methods get inserted into the hypothesis set.

[isovector]

I don't have time to work on this in November, but I think it's a pretty easy fix if you'd like to send a PR!

Make this be a map to a container of HyInfos:

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

Line 240 in 6c14163

{ _jHypothesis :: !(Map OccName (HyInfo a))

update these functions to work over that structure:

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

Lines 15 to 17 in 6c14163

	, jHypothesis
	, jEntireHypothesis
	, jPatHypothesis

and

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

Line 226 in 6c14163

methodHypothesis :: PredType -> Maybe [(OccName, HyInfo CType)]

Make this function concatenate when appending:

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

Lines 101 to 103 in 6c14163

	introducing f ns =
	field @"_jHypothesis" <>~ M.fromList (zip [0..] ns <&>
	\(pos, (name, ty)) -> (name, HyInfo (f pos) ty))

and then follow the type errors until everything compiles again.

[Jashweii]

Another example:

fgmap :: (Functor f, Functor g) => (a -> b) -> (f (g a) -> f (g b))
fgmap = _

Based on stderr, it looks like it's exactly as @isovector said, fmap @g has replaced fmap @f in the map, since the key for both is just fmap.

!!!goal: Judgement {_jHypothesis = fromList [(<$,HyInfo {hi_provenance = ClassMethodPrv Functor, hi_type = forall a b. a -> g b -> g a}),(fmap,HyInfo {hi_provenance = ClassMethodPrv Functor, hi_type = forall a b. (a -> b) -> g a -> g b})], _jBlacklistDestruct = False, _jWhitelistSplit = True, _jIsTopHole = True, _jGoal = (a -> b) -> f (g a) -> f (g b)}
!!!ctx: [(fgmap,(a -> b) -> f (g a) -> f (g b))]
!!!skolems: fromList [f,g,a,b]

Is there a reason you don't consider instead not instantiating fmap and leaving type class methods generalised? (i.e. as forall g a b . Functor g => in the above). Then keep track of given constraints rather than given type class methods.

[isovector]

There's no reason, just that we didn't think about it when first implementing this stuff.

In fact, the underlying issue here is that the hypothesis is a map from names to hyinfos. Keying it by name is stupid, results in bugs like this, and provides literally no benefit. We always just iterate over the container anyway. A better solution would be to key by type, but this has issues with currying and generalized variables.

[isovector]

This is fixed as of #1347, with the exception of let-bindings (due to let-generalization.) But it will successfully solve things of the form:

fJoin :: forall f m a. (Monad m, Monad f) => f (m (m a)) -> f (m a)
fJoin =  let f = (_ :: m (m a) -> m) in fmap f

Closing this issue, but I'll add the examples here to the test suite.