1. 28 Nov, 2019 1 commit
  2. 16 Oct, 2019 1 commit
    • Richard Eisenberg's avatar
      Break up TcRnTypes, among other modules. · 51fad9e6
      Richard Eisenberg authored
      This introduces three new modules:
      
       - basicTypes/Predicate.hs describes predicates, moving
         this logic out of Type. Predicates don't really exist
         in Core, and so don't belong in Type.
      
       - typecheck/TcOrigin.hs describes the origin of constraints
         and types. It was easy to remove from other modules and
         can often be imported instead of other, scarier modules.
      
       - typecheck/Constraint.hs describes constraints as used in
         the solver. It is taken from TcRnTypes.
      
      No work other than module splitting is in this patch.
      
      This is the first step toward homogeneous equality, which will
      rely more strongly on predicates. And homogeneous equality is the
      next step toward a dependently typed core language.
      51fad9e6
  3. 01 Oct, 2019 1 commit
    • Ömer Sinan Ağacan's avatar
      Refactor iface file generation: · f3cb8c7c
      Ömer Sinan Ağacan authored
      This commit refactors interface file generation to allow information
      from the later passed (NCG, STG) to be stored in interface files.
      
      We achieve this by splitting interface file generation into two parts:
      * Partial interfaces, built based on the result of the core pipeline
      * A fully instantiated interface, which also contains the final
      fingerprints and can optionally contain information produced by the backend.
      
      This change is required by !1304 and !1530.
      
      -dynamic-too handling is refactored too: previously when generating code
      we'd branch on -dynamic-too *before* code generation, but now we do it
      after.
      
      (Original code written by @AndreasK in !1530)
      
      Performance
      ~~~~~~~~~~~
      
      Before this patch interface files where created and immediately flushed
      to disk which made space leaks impossible.
      With this change we instead use NFData to force all iface related data
      structures to avoid space leaks.
      
      In the process of refactoring it was discovered that the code in the
      ToIface Module allocated a lot of thunks which were immediately forced
      when writing/forcing the interface file. So we made this module more
      strict to avoid creating many of those thunks.
      
      Bottom line is that allocations go down by about ~0.1% compared to
      master.
      Residency is not meaningfully different after this patch.
      Runtime was not benchmarked.
      Co-Authored-By: Andreas Klebinger's avatarAndreas Klebinger <klebinger.andreas@gmx.at>
      Co-Authored-By: Ömer Sinan Ağacan's avatarÖmer Sinan Ağacan <omer@well-typed.com>
      f3cb8c7c
  4. 20 Sep, 2019 1 commit
  5. 21 Jun, 2019 1 commit
    • Matthías Páll Gissurarson's avatar
      Add HoleFitPlugins and RawHoleFits · c311277b
      Matthías Páll Gissurarson authored
      This patch adds a new kind of plugin, Hole fit plugins. These plugins
      can change what candidates are considered when looking for valid hole
      fits, and add hole fits of their own. The type of a plugin is relatively
      simple,
      
      ```
      type FitPlugin = TypedHole -> [HoleFit] -> TcM [HoleFit]
      type CandPlugin = TypedHole -> [HoleFitCandidate] -> TcM [HoleFitCandidate]
      data HoleFitPlugin = HoleFitPlugin { candPlugin :: CandPlugin
                                         , fitPlugin :: FitPlugin }
      
      data TypedHole = TyH { tyHRelevantCts :: Cts
                             -- ^ Any relevant Cts to the hole
                           , tyHImplics :: [Implication]
                             -- ^ The nested implications of the hole with the
                             --   innermost implication first.
                           , tyHCt :: Maybe Ct
                             -- ^ The hole constraint itself, if available.
                           }
      
      This allows users and plugin writers to interact with the candidates and
      fits as they wish, even going as far as to allow them to reimplement the
      current functionality (since `TypedHole` contains all the relevant
      information).
      
      As an example, consider the following plugin:
      
      ```
      module HolePlugin where
      
      import GhcPlugins
      
      import TcHoleErrors
      
      import Data.List (intersect, stripPrefix)
      import RdrName (importSpecModule)
      
      import TcRnTypes
      
      import System.Process
      
      plugin :: Plugin
      plugin = defaultPlugin { holeFitPlugin = hfp, pluginRecompile = purePlugin }
      
      hfp :: [CommandLineOption] -> Maybe HoleFitPluginR
      hfp opts = Just (fromPureHFPlugin $ HoleFitPlugin (candP opts) (fp opts))
      
      toFilter :: Maybe String -> Maybe String
      toFilter = flip (>>=) (stripPrefix "_module_")
      
      replace :: Eq a => a -> a -> [a] -> [a]
      replace match repl str = replace' [] str
        where
          replace' sofar (x:xs) | x == match = replace' (repl:sofar) xs
          replace' sofar (x:xs) = replace' (x:sofar) xs
          replace' sofar [] = reverse sofar
      
      -- | This candidate plugin filters the candidates by module,
      --   using the name of the hole as module to search in
      candP :: [CommandLineOption] -> CandPlugin
      candP _ hole cands =
        do let he = case tyHCt hole of
                      Just (CHoleCan _ h) -> Just (occNameString $ holeOcc h)
                      _ -> Nothing
           case toFilter he of
              Just undscModName -> do let replaced = replace '_' '.' undscModName
                                      let res = filter (greNotInOpts [replaced]) cands
                                      return $ res
              _ -> return cands
        where greNotInOpts opts (GreHFCand gre)  = not $ null $ intersect (inScopeVia gre) opts
              greNotInOpts _ _ = True
              inScopeVia = map (moduleNameString . importSpecModule) . gre_imp
      
      -- Yes, it's pretty hacky, but it is just an example :)
      searchHoogle :: String -> IO [String]
      searchHoogle ty = lines <$> (readProcess "hoogle" [(show ty)] [])
      
      fp :: [CommandLineOption] -> FitPlugin
      fp ("hoogle":[]) hole hfs =
          do dflags <- getDynFlags
             let tyString = showSDoc dflags . ppr . ctPred <$> tyHCt hole
             res <- case tyString of
                      Just ty -> liftIO $ searchHoogle ty
                      _ -> return []
             return $ (take 2 $ map (RawHoleFit . text . ("Hoogle says: " ++)) res) ++ hfs
      fp _ _ hfs = return hfs
      
      ```
      
      with this plugin available, you can compile the following file
      
      ```
      {-# OPTIONS -fplugin=HolePlugin -fplugin-opt=HolePlugin:hoogle #-}
      module Main where
      
      import Prelude hiding (head, last)
      
      import Data.List (head, last)
      
      t :: [Int] -> Int
      t = _module_Prelude
      
      g :: [Int] -> Int
      g = _module_Data_List
      
      main :: IO ()
      main = print $ t [1,2,3]
      ```
      
      and get the following output:
      
      ```
      Main.hs:14:5: error:
          • Found hole: _module_Prelude :: [Int] -> Int
            Or perhaps ‘_module_Prelude’ is mis-spelled, or not in scope
          • In the expression: _module_Prelude
            In an equation for ‘t’: t = _module_Prelude
          • Relevant bindings include
              t :: [Int] -> Int (bound at Main.hs:14:1)
            Valid hole fits include
              Hoogle says: GHC.List length :: [a] -> Int
              Hoogle says: GHC.OldList length :: [a] -> Int
              t :: [Int] -> Int (bound at Main.hs:14:1)
              g :: [Int] -> Int (bound at Main.hs:17:1)
              length :: forall (t :: * -> *) a. Foldable t => t a -> Int
                with length @[] @Int
                (imported from ‘Prelude’ at Main.hs:5:1-34
                 (and originally defined in ‘Data.Foldable’))
              maximum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
                with maximum @[] @Int
                (imported from ‘Prelude’ at Main.hs:5:1-34
                 (and originally defined in ‘Data.Foldable’))
              (Some hole fits suppressed; use -fmax-valid-hole-fits=N or -fno-max-valid-hole-fits)
         |
      14 | t = _module_Prelude
         |     ^^^^^^^^^^^^^^^
      
      Main.hs:17:5: error:
          • Found hole: _module_Data_List :: [Int] -> Int
            Or perhaps ‘_module_Data_List’ is mis-spelled, or not in scope
          • In the expression: _module_Data_List
            In an equation for ‘g’: g = _module_Data_List
          • Relevant bindings include
              g :: [Int] -> Int (bound at Main.hs:17:1)
            Valid hole fits include
              Hoogle says: GHC.List length :: [a] -> Int
              Hoogle says: GHC.OldList length :: [a] -> Int
              g :: [Int] -> Int (bound at Main.hs:17:1)
              head :: forall a. [a] -> a
                with head @Int
                (imported from ‘Data.List’ at Main.hs:7:19-22
                 (and originally defined in ‘GHC.List’))
              last :: forall a. [a] -> a
                with last @Int
                (imported from ‘Data.List’ at Main.hs:7:25-28
                 (and originally defined in ‘GHC.List’))
         |
      17 | g = _module_Data_List
      
      ```
      
      This relatively simple plugin has two functions, as an example of what
      is possible to do with hole fit plugins. The candidate plugin starts by
      filtering the candidates considered by module, indicated by the name of
      the hole (`_module_Data_List`). The second function is in the fit
      plugin, where the plugin invokes a local hoogle instance to search by
      the type of the hole.
      
      By adding the `RawHoleFit` type, we can also allow these completely free
      suggestions, used in the plugin above to display fits found by Hoogle.
      
      Additionally, the `HoleFitPluginR` wrapper can be used for plugins to
      maintain state between invocations, which can be used to speed up
      invocation of plugins that have expensive initialization.
      
      ```
      -- | HoleFitPluginR adds a TcRef to hole fit plugins so that plugins can
      -- track internal state. Note the existential quantification, ensuring that
      -- the state cannot be modified from outside the plugin.
      data HoleFitPluginR = forall s. HoleFitPluginR
        { hfPluginInit :: TcM (TcRef s)
          -- ^ Initializes the TcRef to be passed to the plugin
        , hfPluginRun :: TcRef s -> HoleFitPlugin
          -- ^ The function defining the plugin itself
        , hfPluginStop :: TcRef s -> TcM ()
          -- ^ Cleanup of state, guaranteed to be called even on error
        }
      ```
      
      Of course, the syntax here is up for debate, but hole fit plugins allow
      us to experiment relatively easily with ways to interact with
      typed-holes without having to dig deep into GHC.
      
      Reviewers: bgamari
      
      Subscribers: rwbarton, carter
      
      Differential Revision: https://phabricator.haskell.org/D5373
      c311277b
  6. 29 May, 2019 1 commit
  7. 15 Mar, 2019 1 commit
  8. 24 Feb, 2019 1 commit
    • Simon Peyton Jones's avatar
      Add AnonArgFlag to FunTy · 6cce36f8
      Simon Peyton Jones authored
      The big payload of this patch is:
      
        Add an AnonArgFlag to the FunTy constructor
        of Type, so that
          (FunTy VisArg   t1 t2) means (t1 -> t2)
          (FunTy InvisArg t1 t2) means (t1 => t2)
      
      The big payoff is that we have a simple, local test to make
      when decomposing a type, leading to many fewer calls to
      isPredTy. To me the code seems a lot tidier, and probably
      more efficient (isPredTy has to take the kind of the type).
      
      See Note [Function types] in TyCoRep.
      
      There are lots of consequences
      
      * I made FunTy into a record, so that it'll be easier
        when we add a linearity field, something that is coming
        down the road.
      
      * Lots of code gets touched in a routine way, simply because it
        pattern matches on FunTy.
      
      * I wanted to make a pattern synonym for (FunTy2 arg res), which
        picks out just the argument and result type from the record. But
        alas the pattern-match overlap checker has a heart attack, and
        either reports false positives, or takes too long.  In the end
        I gave up on pattern synonyms.
      
        There's some commented-out code in TyCoRep that shows what I
        wanted to do.
      
      * Much more clarity about predicate types, constraint types
        and (in particular) equality constraints in kinds.  See TyCoRep
        Note [Types for coercions, predicates, and evidence]
        and Note [Constraints in kinds].
      
        This made me realise that we need an AnonArgFlag on
        AnonTCB in a TyConBinder, something that was really plain
        wrong before. See TyCon Note [AnonTCB InivsArg]
      
      * When building function types we must know whether we
        need VisArg (mkVisFunTy) or InvisArg (mkInvisFunTy).
        This turned out to be pretty easy in practice.
      
      * Pretty-printing of types, esp in IfaceType, gets
        tidier, because we were already recording the (->)
        vs (=>) distinction in an ad-hoc way.  Death to
        IfaceFunTy.
      
      * mkLamType needs to keep track of whether it is building
        (t1 -> t2) or (t1 => t2).  See Type
        Note [mkLamType: dictionary arguments]
      
      Other minor stuff
      
      * Some tidy-up in validity checking involving constraints;
        Trac #16263
      6cce36f8
  9. 22 Nov, 2018 1 commit
    • David Eichmann's avatar
      Fix unused-import warnings · 6353efc7
      David Eichmann authored
      This patch fixes a fairly long-standing bug (dating back to 2015) in
      RdrName.bestImport, namely
      
         commit 9376249b
         Author: Simon Peyton Jones <simonpj@microsoft.com>
         Date:   Wed Oct 28 17:16:55 2015 +0000
      
         Fix unused-import stuff in a better way
      
      In that patch got the sense of the comparison back to front, and
      thereby failed to implement the unused-import rules described in
        Note [Choosing the best import declaration] in RdrName
      
      This led to Trac #13064 and #15393
      
      Fixing this bug revealed a bunch of unused imports in libraries;
      the ones in the GHC repo are part of this commit.
      
      The two important changes are
      
      * Fix the bug in bestImport
      
      * Modified the rules by adding (a) in
           Note [Choosing the best import declaration] in RdrName
        Reason: the previosu rules made Trac #5211 go bad again.  And
        the new rule (a) makes sense to me.
      
      In unravalling this I also ended up doing a few other things
      
      * Refactor RnNames.ImportDeclUsage to use a [GlobalRdrElt] for the
        things that are used, rather than [AvailInfo]. This is simpler
        and more direct.
      
      * Rename greParentName to greParent_maybe, to follow GHC
        naming conventions
      
      * Delete dead code RdrName.greUsedRdrName
      
      Bumps a few submodules.
      
      Reviewers: hvr, goldfire, bgamari, simonmar, jrtc27
      
      Subscribers: rwbarton, carter
      
      Differential Revision: https://phabricator.haskell.org/D5312
      6353efc7
  10. 01 Nov, 2018 1 commit
    • Matthías Páll Gissurarson's avatar
      Add built-in syntax suggestions, and refactor to allow library use · 1c92f193
      Matthías Páll Gissurarson authored
      Summary:
      This change to the valid hole fits adds built-in syntax candidates (like (:) and []),
      so that they are checked in addition to what is in scope.
      
      The rest is merely a refactor and export of the functions used to find the valid
      hole fits, since there was interest at ICFP to use the valid hole fit machinery for
      additional uses. By exporting the `tcFilterHoleFits` function, this can now be done
      without having to rely on parsing the actual error message.
      
      Test Plan: Test for built-in syntax included
      
      Reviewers: bgamari
      
      Reviewed By: bgamari
      
      Subscribers: RyanGlScott, rwbarton, carter
      
      Differential Revision: https://phabricator.haskell.org/D5227
      1c92f193
  11. 25 Jul, 2018 1 commit
    • Simon Peyton Jones's avatar
      Fix and document cloneWC · 857ef25e
      Simon Peyton Jones authored
      The cloneWC, cloneWanted, cloneImplication family are used by
        * TcHoleErrors
        * TcRule
      to clone the /bindings/ in a constraint, so that solving the
      constraint will not add bindings to the program. The idea is only
      to affect unifications.
      
      But I had it wrong -- I failed to clone the EvBindsVar of an
      implication.  That gave an assert failure, I think, as well as
      useless dead code.
      
      The fix is easy.  I'm not adding a test case.
      
      In the type 'TcEvidence.EvBindsVar', I also renamed the
      'NoEvBindsVar' constructor to 'CoEvBindsVar'.  It's not that we
      have /no/ evidence bindings, just that we can only have coercion
      bindings, done via HoleDest.
      857ef25e
  12. 24 Jul, 2018 1 commit
  13. 21 Jul, 2018 1 commit
  14. 12 Jul, 2018 1 commit
    • Matthías Páll Gissurarson's avatar
      Add flag to show docs of valid hole fits · c4d98341
      Matthías Páll Gissurarson authored
      One issue with valid hole fits is that the function names can often be
      opaque for the uninitiated, such as `($)`. This diff adds a new flag,
      `-fshow-docs-of-hole-fits` that adds the documentation of the identifier
      in question to the message, using the same mechanism as the `:doc`
      command.
      
      As an example, with this flag enabled, the valid hole fits for `_ ::
      [Int] -> Int` will include:
      
      ```
      Valid hole fits include
        head :: forall a. [a] -> a
          {-^ Extract the first element of a list, which must be non-empty.-}
          with head @Int
          (imported from ‘Prelude’ (and originally defined in ‘GHC.List’))
      ```
      
      And one of the refinement hole fits, `($) _`, will read:
      
      ```
      Valid refinement hole fits include
        ...
        ($) (_ :: [Int] -> Int)
            where ($) :: forall a b. (a -> b) -> a -> b
            {-^ Application operator.  This operator is redundant, since ordinary
                application @(f x)@ means the same as @(f '$' x)@. However, '$' has
                low, right-associative binding precedence, so it sometimes allows
                parentheses to be omitted; for example:
      
                > f $ g $ h x  =  f (g (h x))
      
                It is also useful in higher-order situations, such as @'map' ('$' 0) xs@,
                or @'Data.List.zipWith' ('$') fs xs@.
      
                Note that @($)@ is levity-polymorphic in its result type, so that
                    foo $ True    where  foo :: Bool -> Int#
                is well-typed-}
            with ($) @'GHC.Types.LiftedRep @[Int] @Int
            (imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))
      
      ```
      
      Another example of where documentation can come in very handy, is when
      working with the `lens` library.
      
      When you compile
      ```
      {-# OPTIONS_GHC -fno-show-provenance-of-hole-fits -fshow-docs-of-hole-fits #-}
      module LensDemo where
      
      import Control.Lens
      import Control.Monad.State
      
      newtype Test = Test { _value :: Int } deriving (Show)
      
      value :: Lens' Test Int
      value f (Test i) = Test <$> f i
      
      updTest :: Test -> Test
      updTest t = t &~ do
          _ value (1 :: Int)
      ```
      
      You get:
      ```
        Valid hole fits include
          (#=) :: forall s (m :: * -> *) a b.
                  MonadState s m =>
                  ALens s s a b -> b -> m ()
            {-^ A version of ('Control.Lens.Setter..=') that works on 'ALens'.-}
            with (#=) @Test @(StateT Test Identity) @Int @Int
          (<#=) :: forall s (m :: * -> *) a b.
                   MonadState s m =>
                   ALens s s a b -> b -> m b
            {-^ A version of ('Control.Lens.Setter.<.=') that works on 'ALens'.-}
            with (<#=) @Test @(StateT Test Identity) @Int @Int
          (<*=) :: forall s (m :: * -> *) a.
                   (MonadState s m, Num a) =>
                   LensLike' ((,) a) s a -> a -> m a
            {-^ Multiply the target of a numerically valued 'Lens' into your 'Monad''s
                state and return the result.
      
                When you do not need the result of the multiplication,
                ('Control.Lens.Setter.*=') is more flexible.
      
                @
                ('<*=') :: ('MonadState' s m, 'Num' a) => 'Lens'' s a -> a -> m a
                ('<*=') :: ('MonadState' s m, 'Num' a) => 'Control.Lens.Iso.Iso'' s a -> a -> m a
                @-}
            with (<*=) @Test @(StateT Test Identity) @Int
          (<+=) :: forall s (m :: * -> *) a.
                   (MonadState s m, Num a) =>
                   LensLike' ((,) a) s a -> a -> m a
            {-^ Add to the target of a numerically valued 'Lens' into your 'Monad''s state
                and return the result.
      
                When you do not need the result of the addition,
                ('Control.Lens.Setter.+=') is more flexible.
      
                @
                ('<+=') :: ('MonadState' s m, 'Num' a) => 'Lens'' s a -> a -> m a
                ('<+=') :: ('MonadState' s m, 'Num' a) => 'Control.Lens.Iso.Iso'' s a -> a -> m a
                @-}
            with (<+=) @Test @(StateT Test Identity) @Int
          (<-=) :: forall s (m :: * -> *) a.
                   (MonadState s m, Num a) =>
                   LensLike' ((,) a) s a -> a -> m a
            {-^ Subtract from the target of a numerically valued 'Lens' into your 'Monad''s
                state and return the result.
      
                When you do not need the result of the subtraction,
                ('Control.Lens.Setter.-=') is more flexible.
      
                @
                ('<-=') :: ('MonadState' s m, 'Num' a) => 'Lens'' s a -> a -> m a
                ('<-=') :: ('MonadState' s m, 'Num' a) => 'Control.Lens.Iso.Iso'' s a -> a -> m a
                @-}
            with (<-=) @Test @(StateT Test Identity) @Int
          (<<*=) :: forall s (m :: * -> *) a.
                    (MonadState s m, Num a) =>
                    LensLike' ((,) a) s a -> a -> m a
            {-^ Modify the target of a 'Lens' into your 'Monad''s state by multipling a value
                and return the /old/ value that was replaced.
      
                When you do not need the result of the operation,
                ('Control.Lens.Setter.*=') is more flexible.
      
                @
                ('<<*=') :: ('MonadState' s m, 'Num' a) => 'Lens'' s a -> a -> m a
                ('<<*=') :: ('MonadState' s m, 'Num' a) => 'Iso'' s a -> a -> m a
                @-}
            with (<<*=) @Test @(StateT Test Identity) @Int
          (Some hole fits suppressed; use -fmax-valid-hole-fits=N or -fno-max-valid-hole-fits)
      
      ```
      
      Which allows you to see at a glance what opaque operators like `(<<*=)`
      and `(<#=)` do.
      
      Reviewers: bgamari, sjakobi
      
      Reviewed By: sjakobi
      
      Subscribers: sjakobi, alexbiehl, rwbarton, thomie, carter
      
      Differential Revision: https://phabricator.haskell.org/D4848
      c4d98341
  15. 04 Jul, 2018 1 commit
    • Matthías Páll Gissurarson's avatar
      Fix errors caused by invalid candidates leaking from hole fits · 39de4e3d
      Matthías Páll Gissurarson authored
      This is a one line fix (and a note) that fixes four tickets, #15007,
       #15321 and #15202, #15314
      
      The issue was that errors caused by illegal candidates (according to GHC
      stage or being internal names) were leaking to the user, causing
      bewildering error messages. If a candidate causes the type checker to
      error, it is not a valid hole fit, and should be discarded.
      
      As mentioned in #15321, this can cause a pattern of omissions, which
      might be hard to discover. A better approach would be to gather the
      error messages, and ask users to report them as GHC bugs. This will be
      implemented in a subsequent change.
      
      Reviewers: bgamari, simonpj
      
      Reviewed By: simonpj
      
      Subscribers: simonpj, rwbarton, thomie, carter
      
      GHC Trac Issues: #15007, #15321, #15202, #15314
      
      Differential Revision: https://phabricator.haskell.org/D4909
      39de4e3d
  16. 30 May, 2018 1 commit
    • Matthías Páll Gissurarson's avatar
      Improved Valid Hole Fits · e0b44e2e
      Matthías Páll Gissurarson authored
      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