#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