Skip to content
  • Matthías Páll Gissurarson's avatar
    Also show types that subsume a hole as valid substitutions for that hole. · 1c920832
    Matthías Páll Gissurarson authored and Ben Gamari's avatar Ben Gamari committed
    
    
    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: default avatarMatthí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
    1c920832