Also show types that subsume a hole as valid substitutions for that hole.

This builds on the previous "Valid substitutions include..." functionality,
but add subsumption checking as well, so that the suggested valid substitutions
show not only exact matches, but also identifiers that fit the hole by virtue of
subsuming the type of the hole (i.e. being more general than the type of the
hole).

Building on the previous example, in the given program

```
ps :: String -> IO ()
ps = putStrLn

ps2 :: a -> IO ()
ps2 _ = putStrLn "hello, world"

main :: IO ()
main = _ "hello, world"
```

The results would be something like

```
    • Found hole: _ :: [Char] -> IO ()
    • In the expression: _
      In the expression: _ "hello, world"
      In an equation for ‘main’: main = _ "hello, world"
    • Relevant bindings include main :: IO () (bound at t1.hs:8:1)
      Valid substitutions include
        ps :: String -> IO () (defined at t1.hs:2:1)
        ps2 :: forall a. a -> IO () (defined at t1.hs:5:1)
        putStrLn :: String -> IO ()
          (imported from ‘Prelude’ at t1.hs:1:1
           (and originally defined in ‘System.IO’))
        fail :: forall (m :: * -> *). Monad m => forall a. String -> m a
          (imported from ‘Prelude’ at t1.hs:1:1
           (and originally defined in ‘GHC.Base’))
        mempty :: forall a. Monoid a => a
          (imported from ‘Prelude’ at t1.hs:1:1
           (and originally defined in ‘GHC.Base’))
        print :: forall a. Show a => a -> IO ()
          (imported from ‘Prelude’ at t1.hs:1:1
           (and originally defined in ‘System.IO’))
        (Some substitutions suppressed;
         use -fmax-valid-substitutions=N or -fno-max-valid-substitutions)
```

Signed-off-by: Matthías Páll Gissurarson <mpg@mpg.is>

Modified according to suggestions from Simon PJ

Accept tests that match the expectations, still a few to look better at

Swithced to using tcLookup, after sit down with SPJ at ICFP. Implications are WIP.

Now works with polymorphism and constraints!

We still need to merge the latest master, before we can make a patch.

Wrap the type of the hole, instead of implication shenanigans,

As per SPJs suggestion, this is simpler and feels closer to
what we actually want to do.

Updated tests with the new implementation

Remove debugging trace and update documentation

Reviewers: austin, bgamari

Reviewed By: bgamari

Subscribers: RyanGlScott, rwbarton, thomie

Differential Revision: https://phabricator.haskell.org/D3930

1 files changed, 12 insertions, 0 deletions

diff --git a/testsuite/tests/gadt/T12468.stderr b/testsuite/tests/gadt/T12468.stderr
index 729b5c45b0..6585f663d0 100644
--- a/testsuite/tests/gadt/T12468.stderr
+++ b/testsuite/tests/gadt/T12468.stderr
@@ -4,3 +4,15 @@ T12468.hs:9:7: error:
     • In the expression: _
       In an equation for ‘f’: f I = _
     • Relevant bindings include f :: T a -> a (bound at T12468.hs:9:1)
+      Valid substitutions include
+        maxBound :: forall a. Bounded a => a
+          (imported from ‘Prelude’ at T12468.hs:3:8-13
+           (and originally defined in ‘GHC.Enum’))
+        minBound :: forall a. Bounded a => a
+          (imported from ‘Prelude’ at T12468.hs:3:8-13
+           (and originally defined in ‘GHC.Enum’))
+        undefined :: forall (a :: TYPE r).
+                     GHC.Stack.Types.HasCallStack =>
+                     a
+          (imported from ‘Prelude’ at T12468.hs:3:8-13
+           (and originally defined in ‘GHC.Err’))