Skip to content

Conversation

isovector
Copy link
Collaborator

@isovector isovector commented Mar 10, 2021

#1517 made Wingman's evidence search much more robust, but I found some more places that GHC can stick dictionaries. This PR adds a few more sources of evidence, namely from GADT constructors and calls to rank-n functions.

That means now we can solve holes like this:

data X f = Monad f => X

fun1 :: X f -> a -> f a
fun1 X = _

Additionally, Wingman can now use evidence that is synthesized when pattern matching on a GADT.

While testing this feature, I realized that Wingman wasn't rewarding generated solutions for using user-bound variables, so that's also included here.

Fixes #1285
Fixes #1550
Fixes #1551

@isovector isovector marked this pull request as draft March 10, 2021 21:03
@isovector isovector marked this pull request as ready for review March 10, 2021 22:05
@isovector isovector changed the title Pull evidence from HsWrappers and ConPatOut sources Improve how wingman uses evidence Mar 10, 2021
@isovector isovector added the merge me Label to trigger pull request merge label Mar 11, 2021
@mergify mergify bot merged commit 05f25c9 into haskell:master Mar 11, 2021
@isovector isovector deleted the use-evidence branch April 5, 2021 11:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
merge me Label to trigger pull request merge
Projects
None yet
3 participants