[GHC] #14273: Typed holes' "valid substitutions" suggestions are oblivious to type class constraints

[GHC]

#14273: Typed holes' "valid substitutions" suggestions are oblivious to type class
constraints
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  Tritlo
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.3
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Poor/confusing    |  Unknown/Multiple
  error message                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #9091, #9479      |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 It's easy to get confused here.  First consider
 {{{
 foo :: [a] -> String
 foo xs = show (_h ++ [])
 }}}
 We end up with this residual constraint
 {{{
 forall a.
   [W]    Show alpha
   [Hole] _h :: [alpha]
 }}}
 where `alpha` is a unification variable, standing for an as-yet-unknown
 type. The
 two unsolved constraints are
 * The `[Hole]` constraint feeds the error-report mechanism, reporting that
 `_h` must be filled vith a value of type `[alpha]`.
 * The `Show alpha` constraint arises from the call of `show`. Initially
 we'd get a `Show [alpha]` constraint, but we use the instance declaration
 `instance Show x => Show [x]` to reduce it to `Show alpha`.

 Now, what can we fill the hole with?  Clearly something of form `[ty]`.
 But once we know what we fill it with, we can set `alpha := ty`, and then
 we want for the rest of the constraints to be soluble, in this case `Show
 alpha`.  So filling with `[Int]` would be fine, but filling with `[Int ->
 Int]` would not.

 Filling with `[a]` would not work either, since we have no way to solve
 `Show a`.

 However, if the original definition had been
 {{{
 foo :: Show a => [a] -> String
 foo xs = show (_h ++ [])
 }}}
 we'd end up with the residual constraint
 {{{
 forall a. Show a =>
   [W]    Show alpha
   [Hole] _h :: [alpha]
 }}}

 then we ''could'' fill `_h` with `xs :: [a]`, because we now do have a
 `Show a` in scope
 from the type signature.

 TL;DR: the real question is this:

 * After filling the hole, can we solve the '''rest of the constraint'''?

 Sadly, that's not a very easy question to answer.

 * The current architecture focuses on the `[Hole]` constraint all by
   itself, but this example shows that it's really all about that
   constraint's peers.

 * There may be many unsolved constraints; filling one hole will not
   nail all of them, so we might erroneously reject a filler.  For example
 {{{
    [W] C alpha beta
    [Hole] _h1 :: alpha
    [Hole] _h2 :: beta
 }}}
   Here we'll never succeed in solving `C alpha beta` until we have
 simultaneously
   filled both holes with compatible types.

 * Operationally, constraint solving may perform unification.  And
 unification
   is (currently) done by side-effect, and not easily undone.  So trying
 successive
   candidates for hole-filling risks prematurely fixing the unification
 variables.

 In full generality this looks too hard.  But I think you might be able to
 do
 a reasonable job for common cases.  For example

 * Given a contraint
 {{{
 forall as1. G1 => ...
    (forall as2. G2 =>
        [Hole] _h :: ty
        C1, ..., Cn
    )...
 }}}
   pick the subset of Ci whose free unification variables are all mentioned
   in `ty`, say D1..Dm

 * Pick a candidate `cand :: cand_ty` to fill `_h`.

 * Clone any free unification variables

 * Try to solve the constraint
 {{{
 forall as1. G1 =>
    (forall as2. G2 =>
        cand_ty <= ty   -- subsumes
        D1, ..., Dm
    )
 }}}

 This isn't perfect, but it'd work in common cases I think.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14273#comment:11>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler