Tactics plugin doesn't make use of existential or type equality constraints

[Jashweii]

Given the following:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ExistentialQuantification #-}
module Main where
main :: IO ()
main = pure ()

data X f = Monad f => X
data Y a b = a ~ b => Y
data Z a b where Z :: Z a a

The tactics plugin cannot derive any of the following holes:

-- Monad f from X
fun1 :: X f -> a -> f a
fun1 X = _ -- pure
-- a ~ b
fun2 :: (a ~ b) => a -> b
fun2 = _ -- id
-- a ~ b from Y
fun3 :: Y a b -> a -> b
fun3 Y = _ -- id
-- a ~ b from Z
fun4 :: Z a b -> a -> b
fun4 Z = _ -- id

(HLS - current master, GHC 8.10.3)

[isovector]

The first one I think will be hard to nail; right now we only look at the given context for typeclass methods. But admittedly, the typeclass support right now is terrible. So I'll keep this usecase in mind when I rethink how to do it.

The equalities should be easy to tackle.

[Jashweii]

I think you'd have to look at all patterns used that are in scope for the expression and add them to the given constraints, probably by walking up the AST from the hole. For existentials you can bring them into scope as new skolems. For actually solving them when they aren't already in scope, probably a lot more complicated beyond just pattern matching every variable in scope known to have a type with constructors with contexts. I would think you might want to actually consider that for some single constructor types like :~: or Dict though.
Semi related but I think you also don't consider signatures in expressions, e.g.

const () (_ :: forall f a b . Functor f => (a -> b) -> (f a -> f b))

Doesn't consider Functor f as a given, but if it were a top level signature on a binding for a hole it would. This might need to walk up the AST too.

[isovector]

@Jashweii do you have a use case in mind for needing to fill holes like const () (_ :: forall f a b . Functor f => (a -> b) -> (f a -> f b))? I can't think of any reason off the top of my head.

[Jashweii]

@isovector
The way I was thinking about it, it was more to do with being a similar situation in terms of type-checking. For signatures specifically I'm not sure there's much more use than limiting what tactics can do - e.g. if you have Alternative f in scope, you may want to forall f a subexpression with a hole in and limit it to Applicative f, to prevent it using "empty" (while empty or <|> might be used elsewhere outside of that subexpression, so the Alternative is useful just not here). The situation I had more in mind was more arguments to functions that need RankNTypes, where (aside from instantiating vs skolemising) you have the same situation as a signature bringing in extra given constraints for its subexpression, so holes inside exp for (fun :: S -> r) exp and (exp :: S).
There have been a few cases I've had a GADT that reveals more information about its type indices that lets me discharge some assumptions, for a simple example:

-- i have some limited domain of types i am operating on
data RestrictedType a = a ~ Int => I | Bool ~ a => B
-- and i know these constraints for all of those types (in practice this would be (c Int, c Bool) and (c a => r) with c explicitly instantiated at call sites)
withConstraints :: RestrictedType a -> ((Show a, Read a, Ord a) => r) -> r
withConstraints I r = r -- supply int proof to r
withConstraints B r = r -- supply bool proof to r
-- and wish to use them
readR :: RestrictedType a -> String -> a
readR i a = withConstraints i (_ a) -- in practice the hole may be inside a large subexpression, e.g. a do block

GHC correctly suggests read as a valid hole fit, with the constraints listed in the error message for the hole, while tactics doesn't try to make (String -> a) given (Show a, Read a, Ord a) - the same as for a signature.

[isovector]

withConstraints is a good example, thanks. We're pretty limited here by what information the typechecker gives us at that hole, but if it's available, we can probably make this happen.

[isovector]

I just checked, and unfortunately the only type information that GHC gives us at that hole is String -> a :(

[isovector]

As of #1549, this evidence is now collected (and the instance and rank-n examples work.) I've filed #1550 to track that wingman doesn't subsequently use the ~ evidence.