Skip to content
  • Matthías Páll Gissurarson's avatar
    Improved Valid Hole Fits · e0b44e2e
    Matthías Páll Gissurarson authored and Ben Gamari's avatar Ben Gamari committed
    I've changed the name from `Valid substitutions` to `Valid hole fits`,
    since "substitution" already has a well defined meaning within the
    theory. As part of this change, the flags and output is reanamed, with
    substitution turning into hole-fit in most cases. "hole fit" was already
    used internally in the code, it's clear and shouldn't cause any
    confusion.
    
    In this update, I've also reworked how we manage side-effects in the
    hole we are considering.
    
    This allows us to consider local bindings such as where clauses and
    arguments to functions, suggesting e.g. `a` for `head (x:xs) where head
    :: [a] -> a`.
    
    It also allows us to find suggestions such as `maximum` for holes of
    type `Ord a => a -> [a]`, and `max` when looking for a match for the
    hole in `g = foldl1 _`, where `g :: Ord a => [a] -> a`.
    
    We also show much improved output for refinement hole fits, and
    fixes #14990. We now show the correct type of the function, but we also
    now show what the arguments to the function should be e.g. `foldl1 (_ ::
    Integer -> Integer -> Integer)` when looking for `[Integer] -> Integer`.
    
    I've moved the bulk of the code from `TcErrors.hs` to a new file,
    `TcHoleErrors.hs`, since it was getting too big to not live on it's own.
    
    This addresses the considerations raised in #14969, and takes proper
    care to set the `tcLevel` of the variables to the right level before
    passing it to the simplifier.
    
    We now also zonk the suggestions properly, which improves the output of
    the refinement hole fits considerably.
    
    This also filters out suggestions from the `GHC.Err` module, since even
    though `error` and `undefined` are indeed valid hole fits, they are
    "trivial", and almost never useful to the user.
    
    We now find the hole fits using the proper manner, namely by solving
    nested implications. This entails that the givens are passed along using
    the implications the hole was nested in, which in turn should mean that
    there will be fewer weird bugs in the typed holes.
    
    I've also added a new sorting method (as suggested by SPJ) and sort by
    the size of the types needed to turn the hole fits into the type of the
    hole. This gives a reasonable approximation to relevance, and is much
    faster than the subsumption check. I've also added a flag to toggle
    whether to use this new sorting algorithm (as is done by default) or the
    subsumption algorithm. This fixes #14969
    
    I've also added documentation for these new flags and update the
    documentation according to the new output.
    
    Reviewers: bgamari, goldfire
    
    Reviewed By: bgamari
    
    Subscribers: simonpj, rwbarton, thomie, carter
    
    GHC Trac Issues: #14969, #14990, #10946
    
    Differential Revision: https://phabricator.haskell.org/D4444
    e0b44e2e