{-# LANGUAGE CPP #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE ExistentialQuantification #-}

module GHC.Tc.Errors.Hole
   ( findValidHoleFits
   , tcCheckHoleFit
   , withoutUnification
   , tcSubsumes
   , isFlexiTyVar
   , tcFilterHoleFits
   , getLocalBindings
   , pprHoleFit
   , addHoleFitDocs
   , getHoleFitSortingAlg
   , getHoleFitDispConfig
   , HoleFitDispConfig (..)
   , HoleFitSortingAlg (..)
   , relevantCtEvidence
   , zonkSubs

   , sortHoleFitsByGraph
   , sortHoleFitsBySize


   -- Re-exported from GHC.Tc.Errors.Hole.Plugin
   , HoleFitPlugin (..), HoleFitPluginR (..)
   )
where

import GHC.Prelude

import GHC.Tc.Errors.Types ( HoleFitDispConfig(..), FitsMbSuppressed(..)
                           , ValidHoleFits(..), noValidHoleFits )
import GHC.Tc.Types
import GHC.Tc.Utils.Monad
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcMType
import GHC.Tc.Types.Evidence
import GHC.Tc.Utils.TcType
import GHC.Tc.Zonk.TcType
import GHC.Core.Type
import GHC.Core.TyCon( TyCon, isGenerativeTyCon )
import GHC.Core.TyCo.Rep( Type(..) )
import GHC.Core.DataCon
import GHC.Core.Predicate( Pred(..), classifyPredType, eqRelRole )
import GHC.Types.Name
import GHC.Types.Name.Reader
import GHC.Builtin.Names ( gHC_ERR, uNSAFE_COERCE )
import GHC.Types.Id
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Types.TyThing
import GHC.Data.Bag
import GHC.Core.ConLike ( ConLike(..) )
import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Tc.Utils.Env (tcLookup)
import GHC.Utils.Outputable
import GHC.Driver.DynFlags
import GHC.Data.Maybe
import GHC.Utils.FV ( fvVarList, fvVarSet, unionFV, mkFVs, FV )

import Control.Arrow ( (&&&) )

import Control.Monad    ( filterM, replicateM, foldM )
import Data.List        ( partition, sort, sortOn, nubBy )
import Data.Graph       ( graphFromEdges, topSort )


import GHC.Tc.Solver    ( simplifyTopWanteds )
import GHC.Tc.Solver.Monad ( runTcSEarlyAbort )
import GHC.Tc.Utils.Unify ( tcSubTypeSigma )

import GHC.HsToCore.Docs ( extractDocs )
import GHC.Hs.Doc
import GHC.Unit.Module.ModIface ( ModIface_(..) )
import GHC.Iface.Load  ( loadInterfaceForName )

import GHC.Builtin.Utils (knownKeyNames)

import GHC.Tc.Errors.Hole.FitTypes
import GHC.Tc.Errors.Hole.Plugin
import qualified Data.Set as Set
import GHC.Types.SrcLoc
import GHC.Data.FastString (NonDetFastString(..))
import GHC.Types.Unique.Map


{-
Note [Valid hole fits include ...]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
`findValidHoleFits` returns the "Valid hole fits include ..." message.
For example, look at the following definitions in a file called test.hs:

   import Data.List (inits)

   f :: [String]
   f = _ "hello, world"

The hole in `f` would generate the message:

  • Found hole: _ :: [Char] -> [String]
  • In the expression: _
    In the expression: _ "hello, world"
    In an equation for ‘f’: f = _ "hello, world"
  • Relevant bindings include f :: [String] (bound at test.hs:6:1)
    Valid hole fits include
      lines :: String -> [String]
        (imported from ‘Prelude’ at mpt.hs:3:8-9
          (and originally defined in ‘base-4.11.0.0:Data.OldList’))
      words :: String -> [String]
        (imported from ‘Prelude’ at mpt.hs:3:8-9
          (and originally defined in ‘base-4.11.0.0:Data.OldList’))
      inits :: forall a. [a] -> [[a]]
        with inits @Char
        (imported from ‘Data.List’ at mpt.hs:4:19-23
          (and originally defined in ‘base-4.11.0.0:Data.OldList’))
      repeat :: forall a. a -> [a]
        with repeat @String
        (imported from ‘Prelude’ at mpt.hs:3:8-9
          (and originally defined in ‘GHC.List’))
      fail :: forall (m :: * -> *). Monad m => forall a. String -> m a
        with fail @[] @String
        (imported from ‘Prelude’ at mpt.hs:3:8-9
          (and originally defined in ‘GHC.Base’))
      return :: forall (m :: * -> *). Monad m => forall a. a -> m a
        with return @[] @String
        (imported from ‘Prelude’ at mpt.hs:3:8-9
          (and originally defined in ‘GHC.Base’))
      pure :: forall (f :: * -> *). Applicative f => forall a. a -> f a
        with pure @[] @String
        (imported from ‘Prelude’ at mpt.hs:3:8-9
          (and originally defined in ‘GHC.Base’))
      read :: forall a. Read a => String -> a
        with read @[String]
        (imported from ‘Prelude’ at mpt.hs:3:8-9
          (and originally defined in ‘Text.Read’))
      mempty :: forall a. Monoid a => a
        with mempty @([Char] -> [String])
        (imported from ‘Prelude’ at mpt.hs:3:8-9
          (and originally defined in ‘GHC.Base’))

Valid hole fits are found by checking top level identifiers and local bindings
in scope for whether their type can be instantiated to the type of the hole.
Additionally, we also need to check whether all relevant constraints are solved
by choosing an identifier of that type as well, see Note [Relevant constraints]

Since checking for subsumption results in the side-effect of type variables
being unified by the simplifier, we need to take care to restore them after
to being flexible type variables after we've checked for subsumption.
This is to avoid affecting the hole and later checks by prematurely having
unified one of the free unification variables.

When outputting, we sort the hole fits by the size of the types we'd need to
apply by type application to the type of the fit to make it fit. This is done
in order to display "more relevant" suggestions first. Another option is to
sort by building a subsumption graph of fits, i.e. a graph of which fits subsume
what other fits, and then outputting those fits which are subsumed by other
fits (i.e. those more specific than other fits) first. This results in the ones
"closest" to the type of the hole to be displayed first.

To help users understand how the suggested fit works, we also display the values
that the quantified type variables would take if that fit is used, like
`mempty @([Char] -> [String])` and `pure @[] @String` in the example above.
If -XTypeApplications is enabled, this can even be copied verbatim as a
replacement for the hole.

Note [Checking hole fits]
~~~~~~~~~~~~~~~~~~~~~~~~~
If we have a hole of type hole_ty, we want to know whether a variable
of type ty is a valid fit for the whole. This is a subsumption check:
we wish to know whether ty <: hole_ty. But, of course, the check
must take into account any givens and relevant constraints.
(See also Note [Relevant constraints]).

For the simplifier to be able to use any givens present in the enclosing
implications to solve relevant constraints, we nest the wanted subsumption
constraints and relevant constraints within the enclosing implications.

As an example, let's look at the following code:

  f :: Show a => a -> String
  f x = show _

Suppose the hole is assigned type a0_a1pd[tau:2].
Here the nested implications are just one level deep, namely:

  [Implic {
      TcLevel = 2
      Skolems = a_a1pa[sk:2]
      No-eqs = True
      Status = Unsolved
      Given = $dShow_a1pc :: Show a_a1pa[sk:2]
      Wanted =
        WC {wc_simple =
              [W] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CDictCan(psc))}
      Binds = EvBindsVar<a1pi>
      Needed inner = []
      Needed outer = []
      the type signature for:
        f :: forall a. Show a => a -> String }]

As we can see, the givens say that the skolem
`a_a1pa[sk:2]` fulfills the Show constraint, and that we must prove
the [W] Show a0_a1pd[tau:2] constraint -- that is, whatever fills the
hole must have a Show instance.

When we now check whether `x :: a_a1pa[sk:2]` fits the hole in
`tcCheckHoleFit`, the call to `tcSubType` will end up unifying the meta type
variable `a0_a1pd[tau:2] := a_a1pa[sk:2]`. By wrapping the wanted constraints
needed by tcSubType_NC and the relevant constraints (see Note [Relevant
constraints] for more details) in the nested implications, we can pass the
information in the givens along to the simplifier. For our example, we end up
needing to check whether the following constraints are soluble.

  WC {wc_impl =
        Implic {
          TcLevel = 2
          Skolems = a_a1pa[sk:2]
          No-eqs = True
          Status = Unsolved
          Given = $dShow_a1pc :: Show a_a1pa[sk:2]
          Wanted =
            WC {wc_simple =
                  [W] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CNonCanonical)}
          Binds = EvBindsVar<a1pl>
          Needed inner = []
          Needed outer = []
          the type signature for:
            f :: forall a. Show a => a -> String }}

But since `a0_a1pd[tau:2] := a_a1pa[sk:2]` and we have from the nested
implications that Show a_a1pa[sk:2] is a given, this is trivial, and we end up
with a final WC of WC {}, confirming x :: a0_a1pd[tau:2] as a match.

To avoid side-effects on the nested implications, we create a new EvBindsVar so
that any changes to the ev binds during a check remains localised to that check.
In addition, we call withoutUnification to reset any unified metavariables; this
call is actually done outside tcCheckHoleFit so that the results can be formatted
for the user before resetting variables.

Note [Valid refinement hole fits include ...]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When the `-frefinement-level-hole-fits=N` flag is given, we additionally look
for "valid refinement hole fits"", i.e. valid hole fits with up to N
additional holes in them.

With `-frefinement-level-hole-fits=0` (the default), GHC will find all
identifiers 'f' (top-level or nested) that will fit in the hole.

With `-frefinement-level-hole-fits=1`, GHC will additionally find all
applications 'f _' that will fit in the hole, where 'f' is an in-scope
identifier, applied to single argument.  It will also report the type of the
needed argument (a new hole).

And similarly as the number of arguments increases

As an example, let's look at the following code:

  f :: [Integer] -> Integer
  f = _

with `-frefinement-level-hole-fits=1`, we'd get:

  Valid refinement hole fits include

    foldl1 (_ :: Integer -> Integer -> Integer)
      with foldl1 @[] @Integer
      where foldl1 :: forall (t :: * -> *).
                      Foldable t =>
                      forall a. (a -> a -> a) -> t a -> a
    foldr1 (_ :: Integer -> Integer -> Integer)
      with foldr1 @[] @Integer
      where foldr1 :: forall (t :: * -> *).
                      Foldable t =>
                      forall a. (a -> a -> a) -> t a -> a
    const (_ :: Integer)
      with const @Integer @[Integer]
      where const :: forall a b. a -> b -> a
    ($) (_ :: [Integer] -> Integer)
      with ($) @'GHC.Types.LiftedRep @[Integer] @Integer
      where ($) :: forall a b. (a -> b) -> a -> b
    fail (_ :: String)
      with fail @((->) [Integer]) @Integer
      where fail :: forall (m :: * -> *).
                    Monad m =>
                    forall a. String -> m a
    return (_ :: Integer)
      with return @((->) [Integer]) @Integer
      where return :: forall (m :: * -> *). Monad m => forall a. a -> m a
    (Some refinement hole fits suppressed;
      use -fmax-refinement-hole-fits=N or -fno-max-refinement-hole-fits)

Which are hole fits with holes in them. This allows e.g. beginners to
discover the fold functions and similar, but also allows for advanced users
to figure out the valid functions in the Free monad, e.g.

  instance Functor f => Monad (Free f) where
      Pure a >>= f = f a
      Free f >>= g = Free (fmap _a f)

Will output (with -frefinment-level-hole-fits=1):
    Found hole: _a :: Free f a -> Free f b
          Where: ‘a’, ‘b’ are rigid type variables bound by
                  the type signature for:
                    (>>=) :: forall a b. Free f a -> (a -> Free f b) -> Free f b
                  at fms.hs:25:12-14
                ‘f’ is a rigid type variable bound by
    ...
    Relevant bindings include
      g :: a -> Free f b (bound at fms.hs:27:16)
      f :: f (Free f a) (bound at fms.hs:27:10)
      (>>=) :: Free f a -> (a -> Free f b) -> Free f b
        (bound at fms.hs:25:12)
    ...
    Valid refinement hole fits include
      ...
      (=<<) (_ :: a -> Free f b)
        with (=<<) @(Free f) @a @b
        where (=<<) :: forall (m :: * -> *) a b.
                      Monad m =>
                      (a -> m b) -> m a -> m b
        (imported from ‘Prelude’ at fms.hs:5:18-22
        (and originally defined in ‘GHC.Base’))
      ...

Where `(=<<) _` is precisely the function we want (we ultimately want `>>= g`).

We find these refinement suggestions by considering hole fits that don't
fit the type of the hole, but ones that would fit if given an additional
argument. We do this by creating a new type variable with `newOpenFlexiTyVar`
(e.g. `t_a1/m[tau:1]`), and then considering hole fits of the type
`t_a1/m[tau:1] -> v` where `v` is the type of the hole.

Since the simplifier is free to unify this new type variable with any type, we
can discover any identifiers that would fit if given another identifier of a
suitable type. This is then generalized so that we can consider any number of
additional arguments by setting the `-frefinement-level-hole-fits` flag to any
number, and then considering hole fits like e.g. `foldl _ _` with two additional
arguments.

To make sure that the refinement hole fits are useful, we check that the types
of the additional holes have a concrete value and not just an invented type
variable. This eliminates suggestions such as `head (_ :: [t0 -> a]) (_ :: t0)`,
and limits the number of less than useful refinement hole fits.

Additionally, to further aid the user in their implementation, we show the
types of the holes the binding would have to be applied to in order to work.
In the free monad example above, this is demonstrated with
`(=<<) (_ :: a -> Free f b)`, which tells the user that the `(=<<)` needs to
be applied to an expression of type `a -> Free f b` in order to match.
If -XScopedTypeVariables is enabled, this hole fit can even be copied verbatim.

Note [Relevant constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
As highlighted by #14273, we need to check any relevant constraints as well
as checking for subsumption. Relevant constraints are the simple constraints
whose free unification variables are mentioned in the type of the hole.

In the simplest case, these are all non-hole constraints in the simples, such
as is the case in

  f :: String
  f = show _

Here, the hole is given type a0_a1kv[tau:1]. Then, the emitted constraint is:

  [W] $dShow_a1kw {0}:: Show a0_a1kv[tau:1] (CNonCanonical)

However, when there are multiple holes, we need to be more careful. As an
example, Let's take a look at the following code:

  f :: Show a => a -> String
  f x = show (_b (show _a))

Here there are two holes, `_a` and `_b`. Suppose _a :: a0_a1pd[tau:2] and
_b :: a1_a1po[tau:2]. Then, the simple constraints passed to
findValidHoleFits are:

  [[W] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CNonCanonical),
    [W] $dShow_a1pp {0}:: Show a1_a1po[tau:2] (CNonCanonical)]

When we are looking for a match for the hole `_a`, we filter the simple
constraints to the "Relevant constraints", by throwing out any constraints
which do not mention a variable mentioned in the type of the hole. For hole
`_a`, we will then only require that the `$dShow_a1pe` constraint is solved,
since that is the only constraint that mentions any free type variables
mentioned in the hole constraint for `_a`, namely `a_a1pd[tau:2]`, and
similarly for the hole `_b` we only require that the `$dShow_a1pe` constraint
is solved.

Note [Leaking errors]
~~~~~~~~~~~~~~~~~~~~~
When considering candidates, GHC believes that we're checking for validity in
actual source. However, As evidenced by #15321, #15007 and #15202, this can
cause bewildering error messages. The solution here is simple: if a candidate
would cause the type checker to error, it is not a valid hole fit, and thus it
is discarded.

Note [Speeding up valid hole-fits]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
To fix #16875 we noted that a lot of time was being spent on unecessary work.

When we'd call `tcCheckHoleFit hole hole_ty ty`, we would end up by generating
a constraint to show that `hole_ty ~ ty`, including any constraints in `ty`. For
example, if `hole_ty = Int` and `ty = Foldable t => (a -> Bool) -> t a -> Bool`,
we'd have `(a_a1pa[sk:1] -> Bool) -> t_t2jk[sk:1] a_a1pa[sk:1] -> Bool ~# Int`
from the coercion, as well as `Foldable t_t2jk[sk:1]`. By adding a flag to
`TcSEnv` and adding a `runTcSEarlyAbort`, we can fail as soon as we hit
an insoluble constraint. Since we don't need the result in the case that it
fails, a boolean `False` (i.e. "it didn't work" from `runTcSEarlyAbort`)
is sufficient.

We also check whether the type of the hole is an immutable type variable (i.e.
a skolem). In that case, the only possible fits are fits of exactly that type,
which can only come from the locals. This speeds things up quite a bit when we
don't know anything about the type of the hole. This also helps with degenerate
fits like (`id (_ :: a)` and `head (_ :: [a])`) when looking for fits of type
`a`, where `a` is a skolem.
-}

-- We read the various -no-show-*-of-hole-fits flags
-- and set the display config accordingly.
getHoleFitDispConfig :: TcM HoleFitDispConfig
getHoleFitDispConfig :: TcM HoleFitDispConfig
getHoleFitDispConfig
  = do { Bool
sWrap <- GeneralFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_ShowTypeAppOfHoleFits
       ; Bool
sWrapVars <- GeneralFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_ShowTypeAppVarsOfHoleFits
       ; Bool
sType <- GeneralFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_ShowTypeOfHoleFits
       ; Bool
sProv <- GeneralFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_ShowProvOfHoleFits
       ; Bool
sMatc <- GeneralFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_ShowMatchesOfHoleFits
       ; HoleFitDispConfig -> TcM HoleFitDispConfig
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return HFDC{ showWrap :: Bool
showWrap = Bool
sWrap, showWrapVars :: Bool
showWrapVars = Bool
sWrapVars
                    , showProv :: Bool
showProv = Bool
sProv, showType :: Bool
showType = Bool
sType
                    , showMatches :: Bool
showMatches = Bool
sMatc } }

-- Which sorting algorithm to use
data HoleFitSortingAlg = HFSNoSorting      -- Do not sort the fits at all
                       | HFSBySize         -- Sort them by the size of the match
                       | HFSBySubsumption  -- Sort by full subsumption
                deriving (HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
(HoleFitSortingAlg -> HoleFitSortingAlg -> Bool)
-> (HoleFitSortingAlg -> HoleFitSortingAlg -> Bool)
-> Eq HoleFitSortingAlg
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
== :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
$c/= :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
/= :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
Eq, Eq HoleFitSortingAlg
Eq HoleFitSortingAlg =>
(HoleFitSortingAlg -> HoleFitSortingAlg -> Ordering)
-> (HoleFitSortingAlg -> HoleFitSortingAlg -> Bool)
-> (HoleFitSortingAlg -> HoleFitSortingAlg -> Bool)
-> (HoleFitSortingAlg -> HoleFitSortingAlg -> Bool)
-> (HoleFitSortingAlg -> HoleFitSortingAlg -> Bool)
-> (HoleFitSortingAlg -> HoleFitSortingAlg -> HoleFitSortingAlg)
-> (HoleFitSortingAlg -> HoleFitSortingAlg -> HoleFitSortingAlg)
-> Ord HoleFitSortingAlg
HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
HoleFitSortingAlg -> HoleFitSortingAlg -> Ordering
HoleFitSortingAlg -> HoleFitSortingAlg -> HoleFitSortingAlg
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: HoleFitSortingAlg -> HoleFitSortingAlg -> Ordering
compare :: HoleFitSortingAlg -> HoleFitSortingAlg -> Ordering
$c< :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
< :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
$c<= :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
<= :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
$c> :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
> :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
$c>= :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
>= :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
$cmax :: HoleFitSortingAlg -> HoleFitSortingAlg -> HoleFitSortingAlg
max :: HoleFitSortingAlg -> HoleFitSortingAlg -> HoleFitSortingAlg
$cmin :: HoleFitSortingAlg -> HoleFitSortingAlg -> HoleFitSortingAlg
min :: HoleFitSortingAlg -> HoleFitSortingAlg -> HoleFitSortingAlg
Ord)

getHoleFitSortingAlg :: TcM HoleFitSortingAlg
getHoleFitSortingAlg :: TcM HoleFitSortingAlg
getHoleFitSortingAlg =
    do { Bool
shouldSort <- GeneralFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_SortValidHoleFits
       ; Bool
subsumSort <- GeneralFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_SortBySubsumHoleFits
       ; Bool
sizeSort <- GeneralFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_SortBySizeHoleFits
       -- We default to sizeSort unless it has been explicitly turned off
       -- or subsumption sorting has been turned on.
       ; HoleFitSortingAlg -> TcM HoleFitSortingAlg
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HoleFitSortingAlg -> TcM HoleFitSortingAlg)
-> HoleFitSortingAlg -> TcM HoleFitSortingAlg
forall a b. (a -> b) -> a -> b
$ if Bool -> Bool
not Bool
shouldSort
                    then HoleFitSortingAlg
HFSNoSorting
                    else if Bool
subsumSort
                         then HoleFitSortingAlg
HFSBySubsumption
                         else if Bool
sizeSort
                              then HoleFitSortingAlg
HFSBySize
                              else HoleFitSortingAlg
HFSNoSorting }

-- If enabled, we go through the fits and add any associated documentation,
-- by looking it up in the module or the environment (for local fits)
addHoleFitDocs :: [HoleFit] -> TcM [HoleFit]
addHoleFitDocs :: [HoleFit] -> TcM [HoleFit]
addHoleFitDocs [HoleFit]
fits =
  do { Bool
showDocs <- GeneralFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_ShowDocsOfHoleFits
     ; if Bool
showDocs
       then do { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
               ; Maybe Docs
mb_local_docs <- DynFlags -> TcGblEnv -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Docs)
forall (m :: * -> *).
MonadIO m =>
DynFlags -> TcGblEnv -> m (Maybe Docs)
extractDocs DynFlags
dflags (TcGblEnv -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Docs))
-> IOEnv (Env TcGblEnv TcLclEnv) TcGblEnv
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Docs)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IOEnv (Env TcGblEnv TcLclEnv) TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv
               ; (Set (Either NonDetFastString Module)
mods_without_docs, [HoleFit]
fits') <- (Set (Either NonDetFastString Module)
 -> HoleFit
 -> IOEnv
      (Env TcGblEnv TcLclEnv)
      (Set (Either NonDetFastString Module), HoleFit))
-> Set (Either NonDetFastString Module)
-> [HoleFit]
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Set (Either NonDetFastString Module), [HoleFit])
forall (m :: * -> *) (t :: * -> *) acc x y.
(Monad m, Traversable t) =>
(acc -> x -> m (acc, y)) -> acc -> t x -> m (acc, t y)
mapAccumLM (Maybe Docs
-> Set (Either NonDetFastString Module)
-> HoleFit
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Set (Either NonDetFastString Module), HoleFit)
upd Maybe Docs
mb_local_docs) Set (Either NonDetFastString Module)
forall a. Set a
Set.empty [HoleFit]
fits
               ; Set (Either NonDetFastString Module)
-> IOEnv (Env TcGblEnv TcLclEnv) ()
forall {a} {b} {f :: * -> *}.
(Outputable a, Outputable b, Applicative f) =>
Set (Either a b) -> f ()
report Set (Either NonDetFastString Module)
mods_without_docs
               ; [HoleFit] -> TcM [HoleFit]
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return [HoleFit]
fits' }
       else [HoleFit] -> TcM [HoleFit]
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return [HoleFit]
fits }
  where
   msg :: SDoc
msg = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"GHC.Tc.Errors.Hole addHoleFitDocs"
   upd :: Maybe Docs
-> Set (Either NonDetFastString Module)
-> HoleFit
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Set (Either NonDetFastString Module), HoleFit)
upd Maybe Docs
mb_local_docs Set (Either NonDetFastString Module)
mods_without_docs fit :: HoleFit
fit@(HoleFit {hfCand :: HoleFit -> HoleFitCandidate
hfCand = HoleFitCandidate
cand}) =
     let name :: Name
name = HoleFitCandidate -> Name
forall a. NamedThing a => a -> Name
getName HoleFitCandidate
cand in
     do { Maybe Docs
mb_docs <- if HoleFit -> Bool
hfIsLcl HoleFit
fit
                     then Maybe Docs -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Docs)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Docs
mb_local_docs
                     else ModIface_ 'ModIfaceFinal -> Maybe Docs
forall (phase :: ModIfacePhase). ModIface_ phase -> Maybe Docs
mi_docs (ModIface_ 'ModIfaceFinal -> Maybe Docs)
-> IOEnv (Env TcGblEnv TcLclEnv) (ModIface_ 'ModIfaceFinal)
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Docs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SDoc
-> Name -> IOEnv (Env TcGblEnv TcLclEnv) (ModIface_ 'ModIfaceFinal)
loadInterfaceForName SDoc
msg Name
name
        ; case Maybe Docs
mb_docs of
            { Maybe Docs
Nothing -> (Set (Either NonDetFastString Module), HoleFit)
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Set (Either NonDetFastString Module), HoleFit)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either NonDetFastString Module
-> Set (Either NonDetFastString Module)
-> Set (Either NonDetFastString Module)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Name -> Either NonDetFastString Module
nameOrigin Name
name) Set (Either NonDetFastString Module)
mods_without_docs, HoleFit
fit)
            ; Just Docs
docs -> do
                { let doc :: Maybe [HsDoc GhcRn]
doc = UniqMap Name [HsDoc GhcRn] -> Name -> Maybe [HsDoc GhcRn]
forall k a. Uniquable k => UniqMap k a -> k -> Maybe a
lookupUniqMap (Docs -> UniqMap Name [HsDoc GhcRn]
docs_decls Docs
docs) Name
name
                ; (Set (Either NonDetFastString Module), HoleFit)
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Set (Either NonDetFastString Module), HoleFit)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Set (Either NonDetFastString Module), HoleFit)
 -> IOEnv
      (Env TcGblEnv TcLclEnv)
      (Set (Either NonDetFastString Module), HoleFit))
-> (Set (Either NonDetFastString Module), HoleFit)
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Set (Either NonDetFastString Module), HoleFit)
forall a b. (a -> b) -> a -> b
$ (Set (Either NonDetFastString Module)
mods_without_docs, HoleFit
fit {hfDoc = map hsDocString <$> doc}) }}}
   upd Maybe Docs
_ Set (Either NonDetFastString Module)
mods_without_docs HoleFit
fit = (Set (Either NonDetFastString Module), HoleFit)
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Set (Either NonDetFastString Module), HoleFit)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set (Either NonDetFastString Module)
mods_without_docs, HoleFit
fit)
   nameOrigin :: Name -> Either NonDetFastString Module
nameOrigin Name
name = case Name -> Maybe Module
nameModule_maybe Name
name of
     Just Module
m  -> Module -> Either NonDetFastString Module
forall a b. b -> Either a b
Right Module
m
     Maybe Module
Nothing ->
       NonDetFastString -> Either NonDetFastString Module
forall a b. a -> Either a b
Left (NonDetFastString -> Either NonDetFastString Module)
-> NonDetFastString -> Either NonDetFastString Module
forall a b. (a -> b) -> a -> b
$ case Name -> SrcLoc
nameSrcLoc Name
name of
         -- Nondeterminism is fine, this is used only to display a warning
         RealSrcLoc RealSrcLoc
r Maybe BufPos
_ -> FastString -> NonDetFastString
NonDetFastString (FastString -> NonDetFastString) -> FastString -> NonDetFastString
forall a b. (a -> b) -> a -> b
$ RealSrcLoc -> FastString
srcLocFile RealSrcLoc
r
         UnhelpfulLoc FastString
s -> FastString -> NonDetFastString
NonDetFastString FastString
s
   report :: Set (Either a b) -> f ()
report Set (Either a b)
mods = do
     { let warning :: SDoc
warning =
             String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"WARNING: Couldn't find any documentation for the following modules:" SDoc -> SDoc -> SDoc
$+$
             Int -> SDoc -> SDoc
nest Int
2
                  ((Either a b -> SDoc) -> [Either a b] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas ((a -> SDoc) -> (b -> SDoc) -> Either a b -> SDoc
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> SDoc
forall a. Outputable a => a -> SDoc
ppr b -> SDoc
forall a. Outputable a => a -> SDoc
ppr) (Set (Either a b) -> [Either a b]
forall a. Set a -> [a]
Set.toList Set (Either a b)
mods) SDoc -> SDoc -> SDoc
$+$
                   String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Make sure the modules are compiled with '-haddock'.")
     ; Bool -> String -> SDoc -> f () -> f ()
forall a. HasCallStack => Bool -> String -> SDoc -> a -> a
warnPprTrace (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set (Either a b) -> Bool
forall a. Set a -> Bool
Set.null Set (Either a b)
mods) String
"addHoleFitDocs" SDoc
warning (() -> f ()
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
     }

-- For pretty printing hole fits, we display the name and type of the fit,
-- with added '_' to represent any extra arguments in case of a non-zero
-- refinement level.
pprHoleFit :: HoleFitDispConfig -> HoleFit -> SDoc
pprHoleFit :: HoleFitDispConfig -> HoleFit -> SDoc
pprHoleFit HoleFitDispConfig
_ (RawHoleFit SDoc
sd) = SDoc
sd
pprHoleFit (HFDC Bool
sWrp Bool
sWrpVars Bool
sTy Bool
sProv Bool
sMs) (HoleFit {Int
[TcType]
Maybe [HsDocString]
Id
TcType
HoleFitCandidate
hfCand :: HoleFit -> HoleFitCandidate
hfDoc :: HoleFit -> Maybe [HsDocString]
hfId :: Id
hfCand :: HoleFitCandidate
hfType :: TcType
hfRefLvl :: Int
hfWrap :: [TcType]
hfMatches :: [TcType]
hfDoc :: Maybe [HsDocString]
hfMatches :: HoleFit -> [TcType]
hfWrap :: HoleFit -> [TcType]
hfRefLvl :: HoleFit -> Int
hfType :: HoleFit -> TcType
hfId :: HoleFit -> Id
..}) =
 SDoc -> Int -> SDoc -> SDoc
hang SDoc
display Int
2 SDoc
provenance
 where tyApp :: SDoc
tyApp = [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ String
-> (VarBndr Id ForAllTyFlag -> TcType -> SDoc)
-> [VarBndr Id ForAllTyFlag]
-> [TcType]
-> [SDoc]
forall a b c.
HasDebugCallStack =>
String -> (a -> b -> c) -> [a] -> [b] -> [c]
zipWithEqual String
"pprHoleFit" VarBndr Id ForAllTyFlag -> TcType -> SDoc
forall {tv}.
Outputable tv =>
VarBndr tv ForAllTyFlag -> TcType -> SDoc
pprArg [VarBndr Id ForAllTyFlag]
vars [TcType]
hfWrap
         where pprArg :: VarBndr tv ForAllTyFlag -> TcType -> SDoc
pprArg VarBndr tv ForAllTyFlag
b TcType
arg = case VarBndr tv ForAllTyFlag -> ForAllTyFlag
forall tv argf. VarBndr tv argf -> argf
binderFlag VarBndr tv ForAllTyFlag
b of
                                ForAllTyFlag
Specified -> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"@" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> TcType -> SDoc
pprParendType TcType
arg
                                  -- Do not print type application for inferred
                                  -- variables (#16456)
                                ForAllTyFlag
Inferred  -> SDoc
forall doc. IsOutput doc => doc
empty
                                ForAllTyFlag
Required  -> String -> SDoc -> SDoc
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"pprHoleFit: bad Required"
                                                         (VarBndr tv ForAllTyFlag -> SDoc
forall a. Outputable a => a -> SDoc
ppr VarBndr tv ForAllTyFlag
b SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
arg)
       tyAppVars :: SDoc
tyAppVars = [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
forall doc. IsLine doc => doc -> [doc] -> [doc]
punctuate SDoc
forall doc. IsLine doc => doc
comma ([SDoc] -> [SDoc]) -> [SDoc] -> [SDoc]
forall a b. (a -> b) -> a -> b
$
           String
-> (VarBndr Id ForAllTyFlag -> TcType -> SDoc)
-> [VarBndr Id ForAllTyFlag]
-> [TcType]
-> [SDoc]
forall a b c.
HasDebugCallStack =>
String -> (a -> b -> c) -> [a] -> [b] -> [c]
zipWithEqual String
"pprHoleFit" (\VarBndr Id ForAllTyFlag
v TcType
t -> Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr (VarBndr Id ForAllTyFlag -> Id
forall tv argf. VarBndr tv argf -> tv
binderVar VarBndr Id ForAllTyFlag
v) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+>
                                               String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"~" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
pprParendType TcType
t)
           [VarBndr Id ForAllTyFlag]
vars [TcType]
hfWrap

       vars :: [VarBndr Id ForAllTyFlag]
vars = TcType -> [VarBndr Id ForAllTyFlag]
unwrapTypeVars TcType
hfType
         where
           -- Attempts to get all the quantified type variables in a type,
           -- e.g.
           -- return :: forall (m :: * -> *) Monad m => (forall a . a -> m a)
           -- into [m, a]
           unwrapTypeVars :: Type -> [ForAllTyBinder]
           unwrapTypeVars :: TcType -> [VarBndr Id ForAllTyFlag]
unwrapTypeVars TcType
t = [VarBndr Id ForAllTyFlag]
vars [VarBndr Id ForAllTyFlag]
-> [VarBndr Id ForAllTyFlag] -> [VarBndr Id ForAllTyFlag]
forall a. [a] -> [a] -> [a]
++ case TcType -> Maybe (FunTyFlag, TcType, TcType, TcType)
splitFunTy_maybe TcType
unforalled of
                               Just (FunTyFlag
_, TcType
_, TcType
_, TcType
unfunned) -> TcType -> [VarBndr Id ForAllTyFlag]
unwrapTypeVars TcType
unfunned
                               Maybe (FunTyFlag, TcType, TcType, TcType)
_ -> []
             where ([VarBndr Id ForAllTyFlag]
vars, TcType
unforalled) = TcType -> ([VarBndr Id ForAllTyFlag], TcType)
splitForAllForAllTyBinders TcType
t
       holeVs :: SDoc
holeVs = [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ (TcType -> SDoc) -> [TcType] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (SDoc -> SDoc) -> (TcType -> SDoc) -> TcType -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"_" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+>) (SDoc -> SDoc) -> (TcType -> SDoc) -> TcType -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr) [TcType]
hfMatches
       holeDisp :: SDoc
holeDisp = if Bool
sMs then SDoc
holeVs
                  else [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ Int -> SDoc -> [SDoc]
forall a. Int -> a -> [a]
replicate ([TcType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TcType]
hfMatches) (SDoc -> [SDoc]) -> SDoc -> [SDoc]
forall a b. (a -> b) -> a -> b
$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"_"
       occDisp :: SDoc
occDisp = case HoleFitCandidate
hfCand of
                   GreHFCand GlobalRdrElt
gre   -> Name -> SDoc
forall a. OutputableBndr a => a -> SDoc
pprPrefixOcc (GlobalRdrElt -> Name
forall info. GlobalRdrEltX info -> Name
greName GlobalRdrElt
gre)
                   NameHFCand Name
name -> Name -> SDoc
forall a. OutputableBndr a => a -> SDoc
pprPrefixOcc Name
name
                   IdHFCand Id
id_    -> Id -> SDoc
forall a. OutputableBndr a => a -> SDoc
pprPrefixOcc Id
id_
       tyDisp :: SDoc
tyDisp = Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppWhen Bool
sTy (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
hfType
       has :: [a] -> Bool
has = Bool -> Bool
not (Bool -> Bool) -> ([a] -> Bool) -> [a] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null
       wrapDisp :: SDoc
wrapDisp = Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppWhen ([TcType] -> Bool
forall a. [a] -> Bool
has [TcType]
hfWrap Bool -> Bool -> Bool
&& (Bool
sWrp Bool -> Bool -> Bool
|| Bool
sWrpVars))
                   (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"with" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> if Bool
sWrp Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
sTy
                                     then SDoc
occDisp SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
tyApp
                                     else SDoc
tyAppVars
       docs :: SDoc
docs = case Maybe [HsDocString]
hfDoc of
                Just [HsDocString]
d -> [HsDocString] -> SDoc
pprHsDocStrings [HsDocString]
d
                Maybe [HsDocString]
_ -> SDoc
forall doc. IsOutput doc => doc
empty
       funcInfo :: SDoc
funcInfo = Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppWhen ([TcType] -> Bool
forall a. [a] -> Bool
has [TcType]
hfMatches Bool -> Bool -> Bool
&& Bool
sTy) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                    String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"where" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
occDisp SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
tyDisp
       subDisp :: SDoc
subDisp = SDoc
occDisp SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> if [TcType] -> Bool
forall a. [a] -> Bool
has [TcType]
hfMatches then SDoc
holeDisp else SDoc
tyDisp
       display :: SDoc
display =  SDoc
subDisp SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Int -> SDoc -> SDoc
nest Int
2 (SDoc
funcInfo SDoc -> SDoc -> SDoc
$+$ SDoc
docs SDoc -> SDoc -> SDoc
$+$ SDoc
wrapDisp)
       provenance :: SDoc
provenance = Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppWhen Bool
sProv (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
             case HoleFitCandidate
hfCand of
                 GreHFCand GlobalRdrElt
gre -> GlobalRdrElt -> SDoc
forall info. GlobalRdrEltX info -> SDoc
pprNameProvenance GlobalRdrElt
gre
                 NameHFCand Name
name -> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"bound at" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SrcLoc -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Name -> SrcLoc
forall a. NamedThing a => a -> SrcLoc
getSrcLoc Name
name)
                 IdHFCand Id
id_ -> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"bound at" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SrcLoc -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Id -> SrcLoc
forall a. NamedThing a => a -> SrcLoc
getSrcLoc Id
id_)

getLocalBindings :: TidyEnv -> CtLoc -> TcM [Id]
getLocalBindings :: TidyEnv -> CtLoc -> TcM [Id]
getLocalBindings TidyEnv
tidy_orig CtLoc
ct_loc
 = do { (TidyEnv
env1, CtOrigin
_) <- ZonkM (TidyEnv, CtOrigin) -> TcM (TidyEnv, CtOrigin)
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM (TidyEnv, CtOrigin) -> TcM (TidyEnv, CtOrigin))
-> ZonkM (TidyEnv, CtOrigin) -> TcM (TidyEnv, CtOrigin)
forall a b. (a -> b) -> a -> b
$ TidyEnv -> CtOrigin -> ZonkM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
tidy_orig (CtLoc -> CtOrigin
ctLocOrigin CtLoc
ct_loc)
      ; TidyEnv -> [Id] -> [TcBinder] -> TcM [Id]
go TidyEnv
env1 [] ([TcBinder] -> [TcBinder]
forall a. HasOccName a => [a] -> [a]
removeBindingShadowing ([TcBinder] -> [TcBinder]) -> [TcBinder] -> [TcBinder]
forall a b. (a -> b) -> a -> b
$ CtLocEnv -> [TcBinder]
ctl_bndrs CtLocEnv
lcl_env) }
  where
    lcl_env :: CtLocEnv
lcl_env = CtLoc -> CtLocEnv
ctLocEnv CtLoc
ct_loc

    go :: TidyEnv -> [Id] -> [TcBinder] -> TcM [Id]
    go :: TidyEnv -> [Id] -> [TcBinder] -> TcM [Id]
go TidyEnv
_ [Id]
sofar [] = [Id] -> TcM [Id]
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Id] -> [Id]
forall a. [a] -> [a]
reverse [Id]
sofar)
    go TidyEnv
env [Id]
sofar (TcBinder
tc_bndr : [TcBinder]
tc_bndrs) =
        case TcBinder
tc_bndr of
          TcIdBndr Id
id TopLevelFlag
_ -> Id -> TcM [Id]
keep_it Id
id
          TcBinder
_ -> TcM [Id]
discard_it
     where
        discard_it :: TcM [Id]
discard_it = TidyEnv -> [Id] -> [TcBinder] -> TcM [Id]
go TidyEnv
env [Id]
sofar [TcBinder]
tc_bndrs
        keep_it :: Id -> TcM [Id]
keep_it Id
id = TidyEnv -> [Id] -> [TcBinder] -> TcM [Id]
go TidyEnv
env (Id
idId -> [Id] -> [Id]
forall a. a -> [a] -> [a]
:[Id]
sofar) [TcBinder]
tc_bndrs



-- See Note [Valid hole fits include ...]
findValidHoleFits :: TidyEnv        -- ^ The tidy_env for zonking
                  -> [Implication]  -- ^ Enclosing implications for givens
                  -> [CtEvidence]
                  -- ^ The  unsolved simple constraints in the implication for
                  -- the hole.
                  -> Hole
                  -> TcM (TidyEnv, ValidHoleFits)
findValidHoleFits :: TidyEnv
-> [Implication]
-> [CtEvidence]
-> Hole
-> TcM (TidyEnv, ValidHoleFits)
findValidHoleFits TidyEnv
tidy_env [Implication]
implics [CtEvidence]
simples h :: Hole
h@(Hole { hole_sort :: Hole -> HoleSort
hole_sort = ExprHole HoleExprRef
_
                                                   , hole_loc :: Hole -> CtLoc
hole_loc  = CtLoc
ct_loc
                                                   , hole_ty :: Hole -> TcType
hole_ty   = TcType
hole_ty }) =
  do { GlobalRdrEnv
rdr_env <- TcRn GlobalRdrEnv
getGlobalRdrEnv
     ; [Id]
lclBinds <- TidyEnv -> CtLoc -> TcM [Id]
getLocalBindings TidyEnv
tidy_env CtLoc
ct_loc
     ; Maybe Int
maxVSubs <- DynFlags -> Maybe Int
maxValidHoleFits (DynFlags -> Maybe Int)
-> IOEnv (Env TcGblEnv TcLclEnv) DynFlags
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
     ; HoleFitSortingAlg
sortingAlg <- TcM HoleFitSortingAlg
getHoleFitSortingAlg
     ; DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
     ; [HoleFitPlugin]
hfPlugs <- TcGblEnv -> [HoleFitPlugin]
tcg_hf_plugins (TcGblEnv -> [HoleFitPlugin])
-> IOEnv (Env TcGblEnv TcLclEnv) TcGblEnv
-> IOEnv (Env TcGblEnv TcLclEnv) [HoleFitPlugin]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOEnv (Env TcGblEnv TcLclEnv) TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv
     ; let findVLimit :: Maybe Int
findVLimit = if HoleFitSortingAlg
sortingAlg HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
forall a. Ord a => a -> a -> Bool
> HoleFitSortingAlg
HFSNoSorting then Maybe Int
forall a. Maybe a
Nothing else Maybe Int
maxVSubs
           refLevel :: Maybe Int
refLevel = DynFlags -> Maybe Int
refLevelHoleFits DynFlags
dflags
           hole :: TypedHole
hole = TypedHole { th_relevant_cts :: Bag CtEvidence
th_relevant_cts =
                                [CtEvidence] -> Bag CtEvidence
forall a. [a] -> Bag a
listToBag (TcType -> [CtEvidence] -> [CtEvidence]
relevantCtEvidence TcType
hole_ty [CtEvidence]
simples)
                            , th_implics :: [Implication]
th_implics      = [Implication]
implics
                            , th_hole :: Maybe Hole
th_hole         = Hole -> Maybe Hole
forall a. a -> Maybe a
Just Hole
h }
           ([[HoleFitCandidate] -> TcM [HoleFitCandidate]]
candidatePlugins, [[HoleFit] -> TcM [HoleFit]]
fitPlugins) =
             [([HoleFitCandidate] -> TcM [HoleFitCandidate],
  [HoleFit] -> TcM [HoleFit])]
-> ([[HoleFitCandidate] -> TcM [HoleFitCandidate]],
    [[HoleFit] -> TcM [HoleFit]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([([HoleFitCandidate] -> TcM [HoleFitCandidate],
   [HoleFit] -> TcM [HoleFit])]
 -> ([[HoleFitCandidate] -> TcM [HoleFitCandidate]],
     [[HoleFit] -> TcM [HoleFit]]))
-> [([HoleFitCandidate] -> TcM [HoleFitCandidate],
     [HoleFit] -> TcM [HoleFit])]
-> ([[HoleFitCandidate] -> TcM [HoleFitCandidate]],
    [[HoleFit] -> TcM [HoleFit]])
forall a b. (a -> b) -> a -> b
$ (HoleFitPlugin
 -> ([HoleFitCandidate] -> TcM [HoleFitCandidate],
     [HoleFit] -> TcM [HoleFit]))
-> [HoleFitPlugin]
-> [([HoleFitCandidate] -> TcM [HoleFitCandidate],
     [HoleFit] -> TcM [HoleFit])]
forall a b. (a -> b) -> [a] -> [b]
map (\HoleFitPlugin
p-> ((HoleFitPlugin -> CandPlugin
candPlugin HoleFitPlugin
p) TypedHole
hole, (HoleFitPlugin -> FitPlugin
fitPlugin HoleFitPlugin
p) TypedHole
hole)) [HoleFitPlugin]
hfPlugs
     ; String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"findingValidHoleFitsFor { " (SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ TypedHole -> SDoc
forall a. Outputable a => a -> SDoc
ppr TypedHole
hole
     ; String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"hole_lvl is:" (SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
hole_lvl
     ; String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"simples are: " (SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ [CtEvidence] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [CtEvidence]
simples
     ; String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"locals are: " (SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ [Id] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
lclBinds
     ; let ([GlobalRdrElt]
lcl, [GlobalRdrElt]
gbl) = (GlobalRdrElt -> Bool)
-> [GlobalRdrElt] -> ([GlobalRdrElt], [GlobalRdrElt])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition GlobalRdrElt -> Bool
forall info. GlobalRdrEltX info -> Bool
gre_lcl (GlobalRdrEnv -> [GlobalRdrElt]
forall info. GlobalRdrEnvX info -> [GlobalRdrEltX info]
globalRdrEnvElts GlobalRdrEnv
rdr_env)
           -- We remove binding shadowings here, but only for the local level.
           -- this is so we e.g. suggest the global fmap from the Functor class
           -- even though there is a local definition as well, such as in the
           -- Free monad example.
           locals :: [HoleFitCandidate]
locals = [HoleFitCandidate] -> [HoleFitCandidate]
forall a. HasOccName a => [a] -> [a]
removeBindingShadowing ([HoleFitCandidate] -> [HoleFitCandidate])
-> [HoleFitCandidate] -> [HoleFitCandidate]
forall a b. (a -> b) -> a -> b
$
                      (Id -> HoleFitCandidate) -> [Id] -> [HoleFitCandidate]
forall a b. (a -> b) -> [a] -> [b]
map Id -> HoleFitCandidate
IdHFCand [Id]
lclBinds [HoleFitCandidate] -> [HoleFitCandidate] -> [HoleFitCandidate]
forall a. [a] -> [a] -> [a]
++ (GlobalRdrElt -> HoleFitCandidate)
-> [GlobalRdrElt] -> [HoleFitCandidate]
forall a b. (a -> b) -> [a] -> [b]
map GlobalRdrElt -> HoleFitCandidate
GreHFCand [GlobalRdrElt]
lcl
           globals :: [HoleFitCandidate]
globals = (GlobalRdrElt -> HoleFitCandidate)
-> [GlobalRdrElt] -> [HoleFitCandidate]
forall a b. (a -> b) -> [a] -> [b]
map GlobalRdrElt -> HoleFitCandidate
GreHFCand [GlobalRdrElt]
gbl
           syntax :: [HoleFitCandidate]
syntax = (Name -> HoleFitCandidate) -> [Name] -> [HoleFitCandidate]
forall a b. (a -> b) -> [a] -> [b]
map Name -> HoleFitCandidate
NameHFCand [Name]
builtIns
           -- If the hole is a rigid type-variable, then we only check the
           -- locals, since only they can match the type (in a meaningful way).
           only_locals :: Bool
only_locals = (Id -> Bool) -> Maybe Id -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Id -> Bool
isImmutableTyVar (Maybe Id -> Bool) -> Maybe Id -> Bool
forall a b. (a -> b) -> a -> b
$ TcType -> Maybe Id
getTyVar_maybe TcType
hole_ty
           to_check :: [HoleFitCandidate]
to_check = if Bool
only_locals then [HoleFitCandidate]
locals
                      else [HoleFitCandidate]
locals [HoleFitCandidate] -> [HoleFitCandidate] -> [HoleFitCandidate]
forall a. [a] -> [a] -> [a]
++ [HoleFitCandidate]
syntax [HoleFitCandidate] -> [HoleFitCandidate] -> [HoleFitCandidate]
forall a. [a] -> [a] -> [a]
++ [HoleFitCandidate]
globals
     ; [HoleFitCandidate]
cands <- ([HoleFitCandidate]
 -> ([HoleFitCandidate] -> TcM [HoleFitCandidate])
 -> TcM [HoleFitCandidate])
-> [HoleFitCandidate]
-> [[HoleFitCandidate] -> TcM [HoleFitCandidate]]
-> TcM [HoleFitCandidate]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((([HoleFitCandidate] -> TcM [HoleFitCandidate])
 -> [HoleFitCandidate] -> TcM [HoleFitCandidate])
-> [HoleFitCandidate]
-> ([HoleFitCandidate] -> TcM [HoleFitCandidate])
-> TcM [HoleFitCandidate]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ([HoleFitCandidate] -> TcM [HoleFitCandidate])
-> [HoleFitCandidate] -> TcM [HoleFitCandidate]
forall a b. (a -> b) -> a -> b
($)) [HoleFitCandidate]
to_check [[HoleFitCandidate] -> TcM [HoleFitCandidate]]
candidatePlugins
     ; String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"numPlugins are:" (SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([[HoleFitCandidate] -> TcM [HoleFitCandidate]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[HoleFitCandidate] -> TcM [HoleFitCandidate]]
candidatePlugins)
     ; (Bool
searchDiscards, [HoleFit]
subs) <-
        Maybe Int
-> TypedHole
-> (TcType, [Id])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
tcFilterHoleFits Maybe Int
findVLimit TypedHole
hole (TcType
hole_ty, []) [HoleFitCandidate]
cands
     ; (TidyEnv
tidy_env, [HoleFit]
tidy_subs) <- ZonkM (TidyEnv, [HoleFit]) -> TcM (TidyEnv, [HoleFit])
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM (TidyEnv, [HoleFit]) -> TcM (TidyEnv, [HoleFit]))
-> ZonkM (TidyEnv, [HoleFit]) -> TcM (TidyEnv, [HoleFit])
forall a b. (a -> b) -> a -> b
$ TidyEnv -> [HoleFit] -> ZonkM (TidyEnv, [HoleFit])
zonkSubs TidyEnv
tidy_env [HoleFit]
subs
     ; [HoleFit]
tidy_sorted_subs <- HoleFitSortingAlg -> [HoleFit] -> TcM [HoleFit]
sortFits HoleFitSortingAlg
sortingAlg [HoleFit]
tidy_subs
     ; [HoleFit]
plugin_handled_subs <- ([HoleFit] -> ([HoleFit] -> TcM [HoleFit]) -> TcM [HoleFit])
-> [HoleFit] -> [[HoleFit] -> TcM [HoleFit]] -> TcM [HoleFit]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((([HoleFit] -> TcM [HoleFit]) -> [HoleFit] -> TcM [HoleFit])
-> [HoleFit] -> ([HoleFit] -> TcM [HoleFit]) -> TcM [HoleFit]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ([HoleFit] -> TcM [HoleFit]) -> [HoleFit] -> TcM [HoleFit]
forall a b. (a -> b) -> a -> b
($)) [HoleFit]
tidy_sorted_subs [[HoleFit] -> TcM [HoleFit]]
fitPlugins
     ; let (Bool
pVDisc, [HoleFit]
limited_subs) = Maybe Int -> [HoleFit] -> (Bool, [HoleFit])
possiblyDiscard Maybe Int
maxVSubs [HoleFit]
plugin_handled_subs
           vDiscards :: Bool
vDiscards = Bool
pVDisc Bool -> Bool -> Bool
|| Bool
searchDiscards
     ; [HoleFit]
subs_with_docs <- [HoleFit] -> TcM [HoleFit]
addHoleFitDocs [HoleFit]
limited_subs
     ; let subs :: FitsMbSuppressed
subs = [HoleFit] -> Bool -> FitsMbSuppressed
Fits [HoleFit]
subs_with_docs Bool
vDiscards
     -- Refinement hole fits. See Note [Valid refinement hole fits include ...]
     ; (TidyEnv
tidy_env, FitsMbSuppressed
rsubs) <-
       if Maybe Int
refLevel Maybe Int -> Maybe Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0
       then
         do { Maybe Int
maxRSubs <- DynFlags -> Maybe Int
maxRefHoleFits (DynFlags -> Maybe Int)
-> IOEnv (Env TcGblEnv TcLclEnv) DynFlags
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
            -- We can use from just, since we know that Nothing >= _ is False.
            ; let refLvls :: [Int]
refLvls = [Int
1..(Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust Maybe Int
refLevel)]
            -- We make a new refinement type for each level of refinement, where
            -- the level of refinement indicates number of additional arguments
            -- to allow.
            ; [(TcType, [Id])]
ref_tys <- (Int -> IOEnv (Env TcGblEnv TcLclEnv) (TcType, [Id]))
-> [Int] -> IOEnv (Env TcGblEnv TcLclEnv) [(TcType, [Id])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Int -> IOEnv (Env TcGblEnv TcLclEnv) (TcType, [Id])
mkRefTy [Int]
refLvls
            ; String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"ref_tys are" (SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ [(TcType, [Id])] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(TcType, [Id])]
ref_tys
            ; let findRLimit :: Maybe Int
findRLimit = if HoleFitSortingAlg
sortingAlg HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
forall a. Ord a => a -> a -> Bool
> HoleFitSortingAlg
HFSNoSorting then Maybe Int
forall a. Maybe a
Nothing
                                                            else Maybe Int
maxRSubs
            ; [(Bool, [HoleFit])]
refDs <- ((TcType, [Id]) -> TcM (Bool, [HoleFit]))
-> [(TcType, [Id])]
-> IOEnv (Env TcGblEnv TcLclEnv) [(Bool, [HoleFit])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (((TcType, [Id]) -> [HoleFitCandidate] -> TcM (Bool, [HoleFit]))
-> [HoleFitCandidate] -> (TcType, [Id]) -> TcM (Bool, [HoleFit])
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Maybe Int
-> TypedHole
-> (TcType, [Id])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
tcFilterHoleFits Maybe Int
findRLimit TypedHole
hole)
                              [HoleFitCandidate]
cands) [(TcType, [Id])]
ref_tys
            ; (TidyEnv
tidy_env, [HoleFit]
tidy_rsubs) <- ZonkM (TidyEnv, [HoleFit]) -> TcM (TidyEnv, [HoleFit])
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM (TidyEnv, [HoleFit]) -> TcM (TidyEnv, [HoleFit]))
-> ZonkM (TidyEnv, [HoleFit]) -> TcM (TidyEnv, [HoleFit])
forall a b. (a -> b) -> a -> b
$ TidyEnv -> [HoleFit] -> ZonkM (TidyEnv, [HoleFit])
zonkSubs TidyEnv
tidy_env ([HoleFit] -> ZonkM (TidyEnv, [HoleFit]))
-> [HoleFit] -> ZonkM (TidyEnv, [HoleFit])
forall a b. (a -> b) -> a -> b
$ ((Bool, [HoleFit]) -> [HoleFit])
-> [(Bool, [HoleFit])] -> [HoleFit]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Bool, [HoleFit]) -> [HoleFit]
forall a b. (a, b) -> b
snd [(Bool, [HoleFit])]
refDs
            ; [HoleFit]
tidy_sorted_rsubs <- HoleFitSortingAlg -> [HoleFit] -> TcM [HoleFit]
sortFits HoleFitSortingAlg
sortingAlg [HoleFit]
tidy_rsubs
            -- For refinement substitutions we want matches
            -- like id (_ :: t), head (_ :: [t]), asTypeOf (_ :: t),
            -- and others in that vein to appear last, since these are
            -- unlikely to be the most relevant fits.
            ; (TidyEnv
tidy_env, TcType
tidy_hole_ty) <- ZonkM (TidyEnv, TcType) -> TcM (TidyEnv, TcType)
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM (TidyEnv, TcType) -> TcM (TidyEnv, TcType))
-> ZonkM (TidyEnv, TcType) -> TcM (TidyEnv, TcType)
forall a b. (a -> b) -> a -> b
$ TidyEnv -> TcType -> ZonkM (TidyEnv, TcType)
zonkTidyTcType TidyEnv
tidy_env TcType
hole_ty
            ; let hasExactApp :: HoleFit -> Bool
hasExactApp = (TcType -> Bool) -> [TcType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (HasDebugCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
tcEqType TcType
tidy_hole_ty) ([TcType] -> Bool) -> (HoleFit -> [TcType]) -> HoleFit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HoleFit -> [TcType]
hfWrap
                  ([HoleFit]
exact, [HoleFit]
not_exact) = (HoleFit -> Bool) -> [HoleFit] -> ([HoleFit], [HoleFit])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition HoleFit -> Bool
hasExactApp [HoleFit]
tidy_sorted_rsubs
            ; [HoleFit]
plugin_handled_rsubs <- ([HoleFit] -> ([HoleFit] -> TcM [HoleFit]) -> TcM [HoleFit])
-> [HoleFit] -> [[HoleFit] -> TcM [HoleFit]] -> TcM [HoleFit]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((([HoleFit] -> TcM [HoleFit]) -> [HoleFit] -> TcM [HoleFit])
-> [HoleFit] -> ([HoleFit] -> TcM [HoleFit]) -> TcM [HoleFit]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ([HoleFit] -> TcM [HoleFit]) -> [HoleFit] -> TcM [HoleFit]
forall a b. (a -> b) -> a -> b
($))
                                        ([HoleFit]
not_exact [HoleFit] -> [HoleFit] -> [HoleFit]
forall a. [a] -> [a] -> [a]
++ [HoleFit]
exact) [[HoleFit] -> TcM [HoleFit]]
fitPlugins
            ; let (Bool
pRDisc, [HoleFit]
exact_last_rfits) =
                    Maybe Int -> [HoleFit] -> (Bool, [HoleFit])
possiblyDiscard Maybe Int
maxRSubs ([HoleFit] -> (Bool, [HoleFit])) -> [HoleFit] -> (Bool, [HoleFit])
forall a b. (a -> b) -> a -> b
$ [HoleFit]
plugin_handled_rsubs
                  rDiscards :: Bool
rDiscards = Bool
pRDisc Bool -> Bool -> Bool
|| ((Bool, [HoleFit]) -> Bool) -> [(Bool, [HoleFit])] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool, [HoleFit]) -> Bool
forall a b. (a, b) -> a
fst [(Bool, [HoleFit])]
refDs
            ; [HoleFit]
rsubs_with_docs <- [HoleFit] -> TcM [HoleFit]
addHoleFitDocs [HoleFit]
exact_last_rfits
            ; (TidyEnv, FitsMbSuppressed)
-> IOEnv (Env TcGblEnv TcLclEnv) (TidyEnv, FitsMbSuppressed)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env, [HoleFit] -> Bool -> FitsMbSuppressed
Fits [HoleFit]
rsubs_with_docs Bool
rDiscards) }
       else (TidyEnv, FitsMbSuppressed)
-> IOEnv (Env TcGblEnv TcLclEnv) (TidyEnv, FitsMbSuppressed)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env, [HoleFit] -> Bool -> FitsMbSuppressed
Fits [] Bool
False)
     ; String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"findingValidHoleFitsFor }" SDoc
forall doc. IsOutput doc => doc
empty
     ; let hole_fits :: ValidHoleFits
hole_fits = FitsMbSuppressed -> FitsMbSuppressed -> ValidHoleFits
ValidHoleFits FitsMbSuppressed
subs FitsMbSuppressed
rsubs
     ; (TidyEnv, ValidHoleFits) -> TcM (TidyEnv, ValidHoleFits)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env, ValidHoleFits
hole_fits) }
  where
    -- We extract the TcLevel from the constraint.
    hole_lvl :: TcLevel
hole_lvl = CtLoc -> TcLevel
ctLocLevel CtLoc
ct_loc

    -- BuiltInSyntax names like (:) and []
    builtIns :: [Name]
    builtIns :: [Name]
builtIns = (Name -> Bool) -> [Name] -> [Name]
forall a. (a -> Bool) -> [a] -> [a]
filter Name -> Bool
isBuiltInSyntax [Name]
knownKeyNames

    -- We make a refinement type by adding a new type variable in front
    -- of the type of t h hole, going from e.g. [Integer] -> Integer
    -- to t_a1/m[tau:1] -> [Integer] -> Integer. This allows the simplifier
    -- to unify the new type variable with any type, allowing us
    -- to suggest a "refinement hole fit", like `(foldl1 _)` instead
    -- of only concrete hole fits like `sum`.
    mkRefTy :: Int -> TcM (TcType, [TcTyVar])
    mkRefTy :: Int -> IOEnv (Env TcGblEnv TcLclEnv) (TcType, [Id])
mkRefTy Int
refLvl = ([Id] -> TcType
wrapWithVars ([Id] -> TcType) -> ([Id] -> [Id]) -> [Id] -> (TcType, [Id])
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& [Id] -> [Id]
forall a. a -> a
id) ([Id] -> (TcType, [Id]))
-> TcM [Id] -> IOEnv (Env TcGblEnv TcLclEnv) (TcType, [Id])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcM [Id]
newTyVars
      where newTyVars :: TcM [Id]
newTyVars = Int -> IOEnv (Env TcGblEnv TcLclEnv) Id -> TcM [Id]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
refLvl (IOEnv (Env TcGblEnv TcLclEnv) Id -> TcM [Id])
-> IOEnv (Env TcGblEnv TcLclEnv) Id -> TcM [Id]
forall a b. (a -> b) -> a -> b
$ Id -> Id
setLvl (Id -> Id)
-> IOEnv (Env TcGblEnv TcLclEnv) Id
-> IOEnv (Env TcGblEnv TcLclEnv) Id
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOEnv (Env TcGblEnv TcLclEnv) Id
newOpenFlexiTyVar
            setLvl :: Id -> Id
setLvl = (Id -> TcLevel -> Id) -> TcLevel -> Id -> Id
forall a b c. (a -> b -> c) -> b -> a -> c
flip Id -> TcLevel -> Id
setMetaTyVarTcLevel TcLevel
hole_lvl
            wrapWithVars :: [Id] -> TcType
wrapWithVars [Id]
vars = [TcType] -> TcType -> TcType
mkVisFunTysMany ((Id -> TcType) -> [Id] -> [TcType]
forall a b. (a -> b) -> [a] -> [b]
map Id -> TcType
mkTyVarTy [Id]
vars) TcType
hole_ty

    sortFits :: HoleFitSortingAlg    -- How we should sort the hole fits
             -> [HoleFit]     -- The subs to sort
             -> TcM [HoleFit]
    sortFits :: HoleFitSortingAlg -> [HoleFit] -> TcM [HoleFit]
sortFits HoleFitSortingAlg
HFSNoSorting [HoleFit]
subs = [HoleFit] -> TcM [HoleFit]
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return [HoleFit]
subs
    sortFits HoleFitSortingAlg
HFSBySize [HoleFit]
subs
        = [HoleFit] -> [HoleFit] -> [HoleFit]
forall a. [a] -> [a] -> [a]
(++) ([HoleFit] -> [HoleFit] -> [HoleFit])
-> TcM [HoleFit]
-> IOEnv (Env TcGblEnv TcLclEnv) ([HoleFit] -> [HoleFit])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [HoleFit] -> TcM [HoleFit]
sortHoleFitsBySize ([HoleFit] -> [HoleFit]
forall a. Ord a => [a] -> [a]
sort [HoleFit]
lclFits)
               IOEnv (Env TcGblEnv TcLclEnv) ([HoleFit] -> [HoleFit])
-> TcM [HoleFit] -> TcM [HoleFit]
forall a b.
IOEnv (Env TcGblEnv TcLclEnv) (a -> b)
-> IOEnv (Env TcGblEnv TcLclEnv) a
-> IOEnv (Env TcGblEnv TcLclEnv) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [HoleFit] -> TcM [HoleFit]
sortHoleFitsBySize ([HoleFit] -> [HoleFit]
forall a. Ord a => [a] -> [a]
sort [HoleFit]
gblFits)
        where ([HoleFit]
lclFits, [HoleFit]
gblFits) = (HoleFit -> Bool) -> [HoleFit] -> ([HoleFit], [HoleFit])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span HoleFit -> Bool
hfIsLcl [HoleFit]
subs
    -- To sort by subsumption, we invoke the sortByGraph function, which
    -- builds the subsumption graph for the fits and then sorts them using a
    -- graph sort.  Since we want locals to come first anyway, we can sort
    -- them separately. The substitutions are already checked in local then
    -- global order, so we can get away with using span here.
    -- We use (<*>) to expose the parallelism, in case it becomes useful later.
    sortFits HoleFitSortingAlg
HFSBySubsumption [HoleFit]
subs
        = [HoleFit] -> [HoleFit] -> [HoleFit]
forall a. [a] -> [a] -> [a]
(++) ([HoleFit] -> [HoleFit] -> [HoleFit])
-> TcM [HoleFit]
-> IOEnv (Env TcGblEnv TcLclEnv) ([HoleFit] -> [HoleFit])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [HoleFit] -> TcM [HoleFit]
sortHoleFitsByGraph ([HoleFit] -> [HoleFit]
forall a. Ord a => [a] -> [a]
sort [HoleFit]
lclFits)
               IOEnv (Env TcGblEnv TcLclEnv) ([HoleFit] -> [HoleFit])
-> TcM [HoleFit] -> TcM [HoleFit]
forall a b.
IOEnv (Env TcGblEnv TcLclEnv) (a -> b)
-> IOEnv (Env TcGblEnv TcLclEnv) a
-> IOEnv (Env TcGblEnv TcLclEnv) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [HoleFit] -> TcM [HoleFit]
sortHoleFitsByGraph ([HoleFit] -> [HoleFit]
forall a. Ord a => [a] -> [a]
sort [HoleFit]
gblFits)
        where ([HoleFit]
lclFits, [HoleFit]
gblFits) = (HoleFit -> Bool) -> [HoleFit] -> ([HoleFit], [HoleFit])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span HoleFit -> Bool
hfIsLcl [HoleFit]
subs

    -- Based on the flags, we might possibly discard some or all the
    -- fits we've found.
    possiblyDiscard :: Maybe Int -> [HoleFit] -> (Bool, [HoleFit])
    possiblyDiscard :: Maybe Int -> [HoleFit] -> (Bool, [HoleFit])
possiblyDiscard (Just Int
max) [HoleFit]
fits = ([HoleFit]
fits [HoleFit] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthExceeds` Int
max, Int -> [HoleFit] -> [HoleFit]
forall a. Int -> [a] -> [a]
take Int
max [HoleFit]
fits)
    possiblyDiscard Maybe Int
Nothing [HoleFit]
fits = (Bool
False, [HoleFit]
fits)


-- We don't (as of yet) handle holes in types, only in expressions.
findValidHoleFits TidyEnv
env [Implication]
_ [CtEvidence]
_ Hole
_ = (TidyEnv, ValidHoleFits) -> TcM (TidyEnv, ValidHoleFits)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, ValidHoleFits
noValidHoleFits)

-- See Note [Relevant constraints]
relevantCtEvidence :: Type -> [CtEvidence] -> [CtEvidence]
relevantCtEvidence :: TcType -> [CtEvidence] -> [CtEvidence]
relevantCtEvidence TcType
hole_ty [CtEvidence]
simples
  = if VarSet -> Bool
isEmptyVarSet (FV -> VarSet
fvVarSet FV
hole_fvs)
    then []
    else (CtEvidence -> Bool) -> [CtEvidence] -> [CtEvidence]
forall a. (a -> Bool) -> [a] -> [a]
filter CtEvidence -> Bool
isRelevant [CtEvidence]
simples
  where hole_fvs :: FV
hole_fvs = TcType -> FV
tyCoFVsOfType TcType
hole_ty
        hole_fv_set :: VarSet
hole_fv_set = FV -> VarSet
fvVarSet FV
hole_fvs
        -- We filter out those constraints that have no variables (since
        -- they won't be solved by finding a type for the type variable
        -- representing the hole) and also other holes, since we're not
        -- trying to find hole fits for many holes at once.
        isRelevant :: CtEvidence -> Bool
isRelevant CtEvidence
ctev = Bool -> Bool
not (VarSet -> Bool
isEmptyVarSet VarSet
fvs) Bool -> Bool -> Bool
&&
                          (VarSet
fvs VarSet -> VarSet -> Bool
`intersectsVarSet` VarSet
hole_fv_set)
          where fvs :: VarSet
fvs = CtEvidence -> VarSet
tyCoVarsOfCtEv CtEvidence
ctev

-- We zonk the hole fits so that the output aligns with the rest
-- of the typed hole error message output.
zonkSubs :: TidyEnv -> [HoleFit] -> ZonkM (TidyEnv, [HoleFit])
zonkSubs :: TidyEnv -> [HoleFit] -> ZonkM (TidyEnv, [HoleFit])
zonkSubs = [HoleFit] -> TidyEnv -> [HoleFit] -> ZonkM (TidyEnv, [HoleFit])
zonkSubs' []
  where zonkSubs' :: [HoleFit] -> TidyEnv -> [HoleFit] -> ZonkM (TidyEnv, [HoleFit])
zonkSubs' [HoleFit]
zs TidyEnv
env [] = (TidyEnv, [HoleFit]) -> ZonkM (TidyEnv, [HoleFit])
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, [HoleFit] -> [HoleFit]
forall a. [a] -> [a]
reverse [HoleFit]
zs)
        zonkSubs' [HoleFit]
zs TidyEnv
env (HoleFit
hf:[HoleFit]
hfs) = do { (TidyEnv
env', HoleFit
z) <- TidyEnv -> HoleFit -> ZonkM (TidyEnv, HoleFit)
zonkSub TidyEnv
env HoleFit
hf
                                        ; [HoleFit] -> TidyEnv -> [HoleFit] -> ZonkM (TidyEnv, [HoleFit])
zonkSubs' (HoleFit
zHoleFit -> [HoleFit] -> [HoleFit]
forall a. a -> [a] -> [a]
:[HoleFit]
zs) TidyEnv
env' [HoleFit]
hfs }

        zonkSub :: TidyEnv -> HoleFit -> ZonkM (TidyEnv, HoleFit)
        zonkSub :: TidyEnv -> HoleFit -> ZonkM (TidyEnv, HoleFit)
zonkSub TidyEnv
env hf :: HoleFit
hf@RawHoleFit{} = (TidyEnv, HoleFit) -> ZonkM (TidyEnv, HoleFit)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, HoleFit
hf)
        zonkSub TidyEnv
env hf :: HoleFit
hf@HoleFit{hfType :: HoleFit -> TcType
hfType = TcType
ty, hfMatches :: HoleFit -> [TcType]
hfMatches = [TcType]
m, hfWrap :: HoleFit -> [TcType]
hfWrap = [TcType]
wrp}
            = do { (TidyEnv
env, TcType
ty') <- TidyEnv -> TcType -> ZonkM (TidyEnv, TcType)
zonkTidyTcType TidyEnv
env TcType
ty
                ; (TidyEnv
env, [TcType]
m')   <- TidyEnv -> [TcType] -> ZonkM (TidyEnv, [TcType])
zonkTidyTcTypes TidyEnv
env [TcType]
m
                ; (TidyEnv
env, [TcType]
wrp') <- TidyEnv -> [TcType] -> ZonkM (TidyEnv, [TcType])
zonkTidyTcTypes TidyEnv
env [TcType]
wrp
                ; let zFit :: HoleFit
zFit = HoleFit
hf {hfType = ty', hfMatches = m', hfWrap = wrp'}
                ; (TidyEnv, HoleFit) -> ZonkM (TidyEnv, HoleFit)
forall a. a -> ZonkM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, HoleFit
zFit ) }

-- | Sort by size uses as a measure for relevance the sizes of the different
-- types needed to instantiate the fit to the type of the hole.
-- This is much quicker than sorting by subsumption, and gives reasonable
-- results in most cases.
sortHoleFitsBySize :: [HoleFit] -> TcM [HoleFit]
sortHoleFitsBySize :: [HoleFit] -> TcM [HoleFit]
sortHoleFitsBySize = [HoleFit] -> TcM [HoleFit]
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([HoleFit] -> TcM [HoleFit])
-> ([HoleFit] -> [HoleFit]) -> [HoleFit] -> TcM [HoleFit]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HoleFit -> TypeSize) -> [HoleFit] -> [HoleFit]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn HoleFit -> TypeSize
sizeOfFit
  where sizeOfFit :: HoleFit -> TypeSize
        sizeOfFit :: HoleFit -> TypeSize
sizeOfFit = [TcType] -> TypeSize
sizeTypes ([TcType] -> TypeSize)
-> (HoleFit -> [TcType]) -> HoleFit -> TypeSize
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TcType -> TcType -> Bool) -> [TcType] -> [TcType]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy HasDebugCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
tcEqType ([TcType] -> [TcType])
-> (HoleFit -> [TcType]) -> HoleFit -> [TcType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  HoleFit -> [TcType]
hfWrap

-- Based on a suggestion by phadej on #ghc, we can sort the found fits
-- by constructing a subsumption graph, and then do a topological sort of
-- the graph. This makes the most specific types appear first, which are
-- probably those most relevant. This takes a lot of work (but results in
-- much more useful output), and can be disabled by
-- '-fno-sort-valid-hole-fits'.
sortHoleFitsByGraph :: [HoleFit] -> TcM [HoleFit]
sortHoleFitsByGraph :: [HoleFit] -> TcM [HoleFit]
sortHoleFitsByGraph [HoleFit]
fits = [(HoleFit, [HoleFit])] -> [HoleFit] -> TcM [HoleFit]
go [] [HoleFit]
fits
  where tcSubsumesWCloning :: TcType -> TcType -> TcM Bool
        tcSubsumesWCloning :: TcType -> TcType -> TcRnIf TcGblEnv TcLclEnv Bool
tcSubsumesWCloning TcType
ht TcType
ty = FV
-> TcRnIf TcGblEnv TcLclEnv Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall a. FV -> TcM a -> TcM a
withoutUnification FV
fvs (TcType -> TcType -> TcRnIf TcGblEnv TcLclEnv Bool
tcSubsumes TcType
ht TcType
ty)
          where fvs :: FV
fvs = [TcType] -> FV
tyCoFVsOfTypes [TcType
ht,TcType
ty]
        go :: [(HoleFit, [HoleFit])] -> [HoleFit] -> TcM [HoleFit]
        go :: [(HoleFit, [HoleFit])] -> [HoleFit] -> TcM [HoleFit]
go [(HoleFit, [HoleFit])]
sofar [] = do { String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"subsumptionGraph was" (SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ [(HoleFit, [HoleFit])] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(HoleFit, [HoleFit])]
sofar
                         ; [HoleFit] -> TcM [HoleFit]
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([HoleFit] -> TcM [HoleFit]) -> [HoleFit] -> TcM [HoleFit]
forall a b. (a -> b) -> a -> b
$ ([HoleFit] -> [HoleFit] -> [HoleFit])
-> ([HoleFit], [HoleFit]) -> [HoleFit]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [HoleFit] -> [HoleFit] -> [HoleFit]
forall a. [a] -> [a] -> [a]
(++) (([HoleFit], [HoleFit]) -> [HoleFit])
-> ([HoleFit], [HoleFit]) -> [HoleFit]
forall a b. (a -> b) -> a -> b
$ (HoleFit -> Bool) -> [HoleFit] -> ([HoleFit], [HoleFit])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition HoleFit -> Bool
hfIsLcl [HoleFit]
topSorted }
          where toV :: (HoleFit, [HoleFit]) -> (HoleFit, Id, [Id])
toV (HoleFit
hf, [HoleFit]
adjs) = (HoleFit
hf, HoleFit -> Id
hfId HoleFit
hf, (HoleFit -> Id) -> [HoleFit] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map HoleFit -> Id
hfId [HoleFit]
adjs)
                (Graph
graph, Int -> (HoleFit, Id, [Id])
fromV, Id -> Maybe Int
_) = [(HoleFit, Id, [Id])]
-> (Graph, Int -> (HoleFit, Id, [Id]), Id -> Maybe Int)
forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Int -> (node, key, [key]), key -> Maybe Int)
graphFromEdges ([(HoleFit, Id, [Id])]
 -> (Graph, Int -> (HoleFit, Id, [Id]), Id -> Maybe Int))
-> [(HoleFit, Id, [Id])]
-> (Graph, Int -> (HoleFit, Id, [Id]), Id -> Maybe Int)
forall a b. (a -> b) -> a -> b
$ ((HoleFit, [HoleFit]) -> (HoleFit, Id, [Id]))
-> [(HoleFit, [HoleFit])] -> [(HoleFit, Id, [Id])]
forall a b. (a -> b) -> [a] -> [b]
map (HoleFit, [HoleFit]) -> (HoleFit, Id, [Id])
toV [(HoleFit, [HoleFit])]
sofar
                topSorted :: [HoleFit]
topSorted = (Int -> HoleFit) -> [Int] -> [HoleFit]
forall a b. (a -> b) -> [a] -> [b]
map ((\(HoleFit
h,Id
_,[Id]
_) -> HoleFit
h) ((HoleFit, Id, [Id]) -> HoleFit)
-> (Int -> (HoleFit, Id, [Id])) -> Int -> HoleFit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (HoleFit, Id, [Id])
fromV) ([Int] -> [HoleFit]) -> [Int] -> [HoleFit]
forall a b. (a -> b) -> a -> b
$ Graph -> [Int]
topSort Graph
graph
        go [(HoleFit, [HoleFit])]
sofar (HoleFit
hf:[HoleFit]
hfs) =
          do { [HoleFit]
adjs <- (HoleFit -> TcRnIf TcGblEnv TcLclEnv Bool)
-> [HoleFit] -> TcM [HoleFit]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (TcType -> TcType -> TcRnIf TcGblEnv TcLclEnv Bool
tcSubsumesWCloning (HoleFit -> TcType
hfType HoleFit
hf) (TcType -> TcRnIf TcGblEnv TcLclEnv Bool)
-> (HoleFit -> TcType) -> HoleFit -> TcRnIf TcGblEnv TcLclEnv Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HoleFit -> TcType
hfType) [HoleFit]
fits
             ; [(HoleFit, [HoleFit])] -> [HoleFit] -> TcM [HoleFit]
go ((HoleFit
hf, [HoleFit]
adjs)(HoleFit, [HoleFit])
-> [(HoleFit, [HoleFit])] -> [(HoleFit, [HoleFit])]
forall a. a -> [a] -> [a]
:[(HoleFit, [HoleFit])]
sofar) [HoleFit]
hfs }

-- | tcFilterHoleFits filters the candidates by whether, given the implications
-- and the relevant constraints, they can be made to match the type by
-- running the type checker. Stops after finding limit matches.
tcFilterHoleFits :: Maybe Int
               -- ^ How many we should output, if limited
               -> TypedHole -- ^ The hole to filter against
               -> (TcType, [TcTyVar])
               -- ^ The type to check for fits and a list of refinement
               -- variables (free type variables in the type) for emulating
               -- additional holes.
               -> [HoleFitCandidate]
               -- ^ The candidates to check whether fit.
               -> TcM (Bool, [HoleFit])
               -- ^ We return whether or not we stopped due to hitting the limit
               -- and the fits we found.
tcFilterHoleFits :: Maybe Int
-> TypedHole
-> (TcType, [Id])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
tcFilterHoleFits (Just Int
0) TypedHole
_ (TcType, [Id])
_ [HoleFitCandidate]
_ = (Bool, [HoleFit]) -> TcM (Bool, [HoleFit])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, []) -- Stop right away on 0
tcFilterHoleFits Maybe Int
limit TypedHole
typed_hole ht :: (TcType, [Id])
ht@(TcType
hole_ty, [Id]
_) [HoleFitCandidate]
candidates =
  do { String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"checkingFitsFor {" (SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
hole_ty
     ; (Bool
discards, [HoleFit]
subs) <- [HoleFit]
-> VarSet
-> Maybe Int
-> (TcType, [Id])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
go [] VarSet
emptyVarSet Maybe Int
limit (TcType, [Id])
ht [HoleFitCandidate]
candidates
     ; String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"checkingFitsFor }" SDoc
forall doc. IsOutput doc => doc
empty
     ; (Bool, [HoleFit]) -> TcM (Bool, [HoleFit])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
discards, [HoleFit]
subs) }
  where
    hole_fvs :: FV
    hole_fvs :: FV
hole_fvs = TcType -> FV
tyCoFVsOfType TcType
hole_ty
    -- Kickoff the checking of the elements.
    -- We iterate over the elements, checking each one in turn for whether
    -- it fits, and adding it to the results if it does.
    go :: [HoleFit]           -- What we've found so far.
       -> VarSet              -- Ids we've already checked
       -> Maybe Int           -- How many we're allowed to find, if limited
       -> (TcType, [TcTyVar]) -- The type, and its refinement variables.
       -> [HoleFitCandidate]  -- The elements we've yet to check.
       -> TcM (Bool, [HoleFit])
    go :: [HoleFit]
-> VarSet
-> Maybe Int
-> (TcType, [Id])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
go [HoleFit]
subs VarSet
_ Maybe Int
_ (TcType, [Id])
_ [] = (Bool, [HoleFit]) -> TcM (Bool, [HoleFit])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [HoleFit] -> [HoleFit]
forall a. [a] -> [a]
reverse [HoleFit]
subs)
    go [HoleFit]
subs VarSet
_ (Just Int
0) (TcType, [Id])
_ [HoleFitCandidate]
_ = (Bool, [HoleFit]) -> TcM (Bool, [HoleFit])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [HoleFit] -> [HoleFit]
forall a. [a] -> [a]
reverse [HoleFit]
subs)
    go [HoleFit]
subs VarSet
seen Maybe Int
maxleft (TcType, [Id])
ty (HoleFitCandidate
el:[HoleFitCandidate]
elts) =
        -- See Note [Leaking errors]
        TcM (Bool, [HoleFit])
-> TcM (Bool, [HoleFit]) -> TcM (Bool, [HoleFit])
forall r. TcM r -> TcM r -> TcM r
tryTcDiscardingErrs TcM (Bool, [HoleFit])
discard_it (TcM (Bool, [HoleFit]) -> TcM (Bool, [HoleFit]))
-> TcM (Bool, [HoleFit]) -> TcM (Bool, [HoleFit])
forall a b. (a -> b) -> a -> b
$
        do { String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"lookingUp" (SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ HoleFitCandidate -> SDoc
forall a. Outputable a => a -> SDoc
ppr HoleFitCandidate
el
           ; Maybe (Id, TcType)
maybeThing <- HoleFitCandidate -> TcM (Maybe (Id, TcType))
lookup HoleFitCandidate
el
           ; case Maybe (Id, TcType)
maybeThing of
               Just (Id
id, TcType
id_ty) | Id -> Bool
not_trivial Id
id ->
                       do { Maybe ([TcType], [TcType])
fits <- (TcType, [Id]) -> TcType -> TcM (Maybe ([TcType], [TcType]))
fitsHole (TcType, [Id])
ty TcType
id_ty
                          ; case Maybe ([TcType], [TcType])
fits of
                              Just ([TcType]
wrp, [TcType]
matches) -> Id -> TcType -> [TcType] -> [TcType] -> TcM (Bool, [HoleFit])
keep_it Id
id TcType
id_ty [TcType]
wrp [TcType]
matches
                              Maybe ([TcType], [TcType])
_ -> TcM (Bool, [HoleFit])
discard_it }
               Maybe (Id, TcType)
_ -> TcM (Bool, [HoleFit])
discard_it }
        where
          -- We want to filter out undefined and the likes from GHC.Err (#17940)
          not_trivial :: Id -> Bool
not_trivial Id
id = Name -> Maybe Module
nameModule_maybe (Id -> Name
idName Id
id) Maybe Module -> [Maybe Module] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Module -> Maybe Module
forall a. a -> Maybe a
Just Module
gHC_ERR, Module -> Maybe Module
forall a. a -> Maybe a
Just Module
uNSAFE_COERCE]

          lookup :: HoleFitCandidate -> TcM (Maybe (Id, Type))
          lookup :: HoleFitCandidate -> TcM (Maybe (Id, TcType))
lookup (IdHFCand Id
id) = Maybe (Id, TcType) -> TcM (Maybe (Id, TcType))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Id, TcType) -> Maybe (Id, TcType)
forall a. a -> Maybe a
Just (Id
id, Id -> TcType
idType Id
id))
          lookup HoleFitCandidate
hfc = do { TcTyThing
thing <- Name -> TcM TcTyThing
tcLookup Name
name
                          ; Maybe (Id, TcType) -> TcM (Maybe (Id, TcType))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Id, TcType) -> TcM (Maybe (Id, TcType)))
-> Maybe (Id, TcType) -> TcM (Maybe (Id, TcType))
forall a b. (a -> b) -> a -> b
$ case TcTyThing
thing of
                                       ATcId {tct_id :: TcTyThing -> Id
tct_id = Id
id} -> (Id, TcType) -> Maybe (Id, TcType)
forall a. a -> Maybe a
Just (Id
id, Id -> TcType
idType Id
id)
                                       AGlobal (AnId Id
id)   -> (Id, TcType) -> Maybe (Id, TcType)
forall a. a -> Maybe a
Just (Id
id, Id -> TcType
idType Id
id)
                                       AGlobal (AConLike (RealDataCon DataCon
con)) ->
                                           (Id, TcType) -> Maybe (Id, TcType)
forall a. a -> Maybe a
Just (DataCon -> Id
dataConWrapId DataCon
con, DataCon -> TcType
dataConNonlinearType DataCon
con)
                                       TcTyThing
_ -> Maybe (Id, TcType)
forall a. Maybe a
Nothing }
            where name :: Name
name = case HoleFitCandidate
hfc of
#if __GLASGOW_HASKELL__ < 901
                           IdHFCand id     -> idName id
#endif
                           GreHFCand GlobalRdrElt
gre   -> GlobalRdrElt -> Name
forall info. GlobalRdrEltX info -> Name
greName GlobalRdrElt
gre
                           NameHFCand Name
name -> Name
name
          discard_it :: TcM (Bool, [HoleFit])
discard_it = [HoleFit]
-> VarSet
-> Maybe Int
-> (TcType, [Id])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
go [HoleFit]
subs VarSet
seen Maybe Int
maxleft (TcType, [Id])
ty [HoleFitCandidate]
elts
          keep_it :: Id -> TcType -> [TcType] -> [TcType] -> TcM (Bool, [HoleFit])
keep_it Id
eid TcType
eid_ty [TcType]
wrp [TcType]
ms = [HoleFit]
-> VarSet
-> Maybe Int
-> (TcType, [Id])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
go (HoleFit
fitHoleFit -> [HoleFit] -> [HoleFit]
forall a. a -> [a] -> [a]
:[HoleFit]
subs) (VarSet -> Id -> VarSet
extendVarSet VarSet
seen Id
eid)
                                 ((\Int
n -> Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
maxleft) (TcType, [Id])
ty [HoleFitCandidate]
elts
            where
              fit :: HoleFit
fit = HoleFit { hfId :: Id
hfId = Id
eid, hfCand :: HoleFitCandidate
hfCand = HoleFitCandidate
el, hfType :: TcType
hfType = TcType
eid_ty
                            , hfRefLvl :: Int
hfRefLvl = [Id] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((TcType, [Id]) -> [Id]
forall a b. (a, b) -> b
snd (TcType, [Id])
ty)
                            , hfWrap :: [TcType]
hfWrap = [TcType]
wrp, hfMatches :: [TcType]
hfMatches = [TcType]
ms
                            , hfDoc :: Maybe [HsDocString]
hfDoc = Maybe [HsDocString]
forall a. Maybe a
Nothing }




    unfoldWrapper :: HsWrapper -> [Type]
    unfoldWrapper :: HsWrapper -> [TcType]
unfoldWrapper = [TcType] -> [TcType]
forall a. [a] -> [a]
reverse ([TcType] -> [TcType])
-> (HsWrapper -> [TcType]) -> HsWrapper -> [TcType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsWrapper -> [TcType]
unfWrp'
      where unfWrp' :: HsWrapper -> [TcType]
unfWrp' (WpTyApp TcType
ty) = [TcType
ty]
            unfWrp' (WpCompose HsWrapper
w1 HsWrapper
w2) = HsWrapper -> [TcType]
unfWrp' HsWrapper
w1 [TcType] -> [TcType] -> [TcType]
forall a. [a] -> [a] -> [a]
++ HsWrapper -> [TcType]
unfWrp' HsWrapper
w2
            unfWrp' HsWrapper
_ = []


    -- The real work happens here, where we invoke the type checker using
    -- tcCheckHoleFit to see whether the given type fits the hole.
    fitsHole :: (TcType, [TcTyVar]) -- The type of the hole wrapped with the
                                    -- refinement variables created to simulate
                                    -- additional holes (if any), and the list
                                    -- of those variables (possibly empty).
                                    -- As an example: If the actual type of the
                                    -- hole (as specified by the hole
                                    -- constraint CHoleExpr passed to
                                    -- findValidHoleFits) is t and we want to
                                    -- simulate N additional holes, h_ty will
                                    -- be  r_1 -> ... -> r_N -> t, and
                                    -- ref_vars will be [r_1, ... , r_N].
                                    -- In the base case with no additional
                                    -- holes, h_ty will just be t and ref_vars
                                    -- will be [].
             -> TcType -- The type we're checking to whether it can be
                       -- instantiated to the type h_ty.
             -> TcM (Maybe ([TcType], [TcType])) -- If it is not a match, we
                                                 -- return Nothing. Otherwise,
                                                 -- we Just return the list of
                                                 -- types that quantified type
                                                 -- variables in ty would take
                                                 -- if used in place of h_ty,
                                                 -- and the list types of any
                                                 -- additional holes simulated
                                                 -- with the refinement
                                                 -- variables in ref_vars.
    fitsHole :: (TcType, [Id]) -> TcType -> TcM (Maybe ([TcType], [TcType]))
fitsHole (TcType
h_ty, [Id]
ref_vars) TcType
ty =
    -- We wrap this with the withoutUnification to avoid having side-effects
    -- beyond the check, but we rely on the side-effects when looking for
    -- refinement hole fits, so we can't wrap the side-effects deeper than this.
      FV
-> TcM (Maybe ([TcType], [TcType]))
-> TcM (Maybe ([TcType], [TcType]))
forall a. FV -> TcM a -> TcM a
withoutUnification FV
fvs (TcM (Maybe ([TcType], [TcType]))
 -> TcM (Maybe ([TcType], [TcType])))
-> TcM (Maybe ([TcType], [TcType]))
-> TcM (Maybe ([TcType], [TcType]))
forall a b. (a -> b) -> a -> b
$
      do { String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"checkingFitOf {" (SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty
         ; (Bool
fits, HsWrapper
wrp) <- TypedHole -> TcType -> TcType -> TcM (Bool, HsWrapper)
tcCheckHoleFit TypedHole
hole TcType
h_ty TcType
ty
         ; String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"Did it fit?" (SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
fits
         ; String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"wrap is: " (SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ HsWrapper -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsWrapper
wrp
         ; String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"checkingFitOf }" SDoc
forall doc. IsOutput doc => doc
empty
         -- We'd like to avoid refinement suggestions like `id _ _` or
         -- `head _ _`, and only suggest refinements where our all phantom
         -- variables got unified during the checking. This can be disabled
         -- with the `-fabstract-refinement-hole-fits` flag.
         -- Here we do the additional handling when there are refinement
         -- variables, i.e. zonk them to read their final value to check for
         -- abstract refinements, and to report what the type of the simulated
         -- holes must be for this to be a match.
         ; if Bool
fits then do {
              -- Zonking is expensive, so we only do it if required.
              [TcType]
z_wrp_tys <- ZonkM [TcType] -> TcM [TcType]
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM [TcType] -> TcM [TcType]) -> ZonkM [TcType] -> TcM [TcType]
forall a b. (a -> b) -> a -> b
$ [TcType] -> ZonkM [TcType]
zonkTcTypes (HsWrapper -> [TcType]
unfoldWrapper HsWrapper
wrp)
            ; if [Id] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
ref_vars
              then Maybe ([TcType], [TcType]) -> TcM (Maybe ([TcType], [TcType]))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (([TcType], [TcType]) -> Maybe ([TcType], [TcType])
forall a. a -> Maybe a
Just ([TcType]
z_wrp_tys, []))
              else do { let -- To be concrete matches, matches have to
                            -- be more than just an invented type variable.
                            fvSet :: VarSet
fvSet = FV -> VarSet
fvVarSet FV
fvs
                            notAbstract :: TcType -> Bool
                            notAbstract :: TcType -> Bool
notAbstract TcType
t = case TcType -> Maybe Id
getTyVar_maybe TcType
t of
                                              Just Id
tv -> Id
tv Id -> VarSet -> Bool
`elemVarSet` VarSet
fvSet
                                              Maybe Id
_ -> Bool
True
                            allConcrete :: Bool
allConcrete = (TcType -> Bool) -> [TcType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TcType -> Bool
notAbstract [TcType]
z_wrp_tys
                      ; [TcType]
z_vars  <- ZonkM [TcType] -> TcM [TcType]
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM [TcType] -> TcM [TcType]) -> ZonkM [TcType] -> TcM [TcType]
forall a b. (a -> b) -> a -> b
$ [Id] -> ZonkM [TcType]
zonkTcTyVars [Id]
ref_vars
                      ; let z_mtvs :: [Id]
z_mtvs = (TcType -> Maybe Id) -> [TcType] -> [Id]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TcType -> Maybe Id
getTyVar_maybe [TcType]
z_vars
                      ; Bool
allFilled <- Bool -> Bool
not (Bool -> Bool)
-> TcRnIf TcGblEnv TcLclEnv Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Id -> TcRnIf TcGblEnv TcLclEnv Bool)
-> [Id] -> TcRnIf TcGblEnv TcLclEnv Bool
forall (m :: * -> *) (f :: * -> *) a.
(Monad m, Foldable f) =>
(a -> m Bool) -> f a -> m Bool
anyM Id -> TcRnIf TcGblEnv TcLclEnv Bool
isFlexiTyVar [Id]
z_mtvs
                      ; Bool
allowAbstract <- GeneralFlag -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_AbstractRefHoleFits
                      ; if Bool
allowAbstract Bool -> Bool -> Bool
|| (Bool
allFilled Bool -> Bool -> Bool
&& Bool
allConcrete )
                        then Maybe ([TcType], [TcType]) -> TcM (Maybe ([TcType], [TcType]))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([TcType], [TcType]) -> TcM (Maybe ([TcType], [TcType])))
-> Maybe ([TcType], [TcType]) -> TcM (Maybe ([TcType], [TcType]))
forall a b. (a -> b) -> a -> b
$ ([TcType], [TcType]) -> Maybe ([TcType], [TcType])
forall a. a -> Maybe a
Just ([TcType]
z_wrp_tys, [TcType]
z_vars)
                        else Maybe ([TcType], [TcType]) -> TcM (Maybe ([TcType], [TcType]))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([TcType], [TcType])
forall a. Maybe a
Nothing }}
           else Maybe ([TcType], [TcType]) -> TcM (Maybe ([TcType], [TcType]))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([TcType], [TcType])
forall a. Maybe a
Nothing }
     where fvs :: FV
fvs = [Id] -> FV
mkFVs [Id]
ref_vars FV -> FV -> FV
`unionFV` FV
hole_fvs FV -> FV -> FV
`unionFV` TcType -> FV
tyCoFVsOfType TcType
ty
           hole :: TypedHole
hole = TypedHole
typed_hole { th_hole = Nothing }



-- | Checks whether a MetaTyVar is flexible or not.
isFlexiTyVar :: TcTyVar -> TcM Bool
isFlexiTyVar :: Id -> TcRnIf TcGblEnv TcLclEnv Bool
isFlexiTyVar Id
tv | Id -> Bool
isMetaTyVar Id
tv = MetaDetails -> Bool
isFlexi (MetaDetails -> Bool)
-> IOEnv (Env TcGblEnv TcLclEnv) MetaDetails
-> TcRnIf TcGblEnv TcLclEnv Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Id -> IOEnv (Env TcGblEnv TcLclEnv) MetaDetails
forall (m :: * -> *). MonadIO m => Id -> m MetaDetails
readMetaTyVar Id
tv
isFlexiTyVar Id
_ = Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- | Takes a list of free variables and restores any Flexi type variables in
-- free_vars after the action is run.
withoutUnification :: FV -> TcM a -> TcM a
withoutUnification :: forall a. FV -> TcM a -> TcM a
withoutUnification FV
free_vars TcM a
action =
  do { [Id]
flexis <- (Id -> TcRnIf TcGblEnv TcLclEnv Bool) -> [Id] -> TcM [Id]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM Id -> TcRnIf TcGblEnv TcLclEnv Bool
isFlexiTyVar [Id]
fuvs
     ; a
result <- TcM a
action
          -- Reset any mutated free variables
     ; (Id -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> [Id] -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Id -> IOEnv (Env TcGblEnv TcLclEnv) ()
restore [Id]
flexis
     ; a -> TcM a
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
result }
  where restore :: Id -> IOEnv (Env TcGblEnv TcLclEnv) ()
restore Id
tv = do { String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"withoutUnification: restore flexi" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
tv)
                        ; TcRef MetaDetails
-> MetaDetails -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall (m :: * -> *) a. MonadIO m => TcRef a -> a -> m ()
writeTcRef (Id -> TcRef MetaDetails
metaTyVarRef Id
tv) MetaDetails
Flexi }
        fuvs :: [Id]
fuvs = FV -> [Id]
fvVarList FV
free_vars

-- | Reports whether first type (ty_a) subsumes the second type (ty_b),
-- discarding any errors. Subsumption here means that the ty_b can fit into the
-- ty_a, i.e. `tcSubsumes a b == True` if b is a subtype of a.
tcSubsumes :: TcSigmaType -> TcSigmaType -> TcM Bool
tcSubsumes :: TcType -> TcType -> TcRnIf TcGblEnv TcLclEnv Bool
tcSubsumes TcType
ty_a TcType
ty_b = (Bool, HsWrapper) -> Bool
forall a b. (a, b) -> a
fst ((Bool, HsWrapper) -> Bool)
-> TcM (Bool, HsWrapper) -> TcRnIf TcGblEnv TcLclEnv Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypedHole -> TcType -> TcType -> TcM (Bool, HsWrapper)
tcCheckHoleFit TypedHole
dummyHole TcType
ty_a TcType
ty_b
  where dummyHole :: TypedHole
dummyHole = TypedHole { th_relevant_cts :: Bag CtEvidence
th_relevant_cts = Bag CtEvidence
forall a. Bag a
emptyBag
                              , th_implics :: [Implication]
th_implics      = []
                              , th_hole :: Maybe Hole
th_hole         = Maybe Hole
forall a. Maybe a
Nothing }

-- | A tcSubsumes which takes into account relevant constraints, to fix trac
-- #14273. This makes sure that when checking whether a type fits the hole,
-- the type has to be subsumed by type of the hole as well as fulfill all
-- constraints on the type of the hole.
tcCheckHoleFit :: TypedHole   -- ^ The hole to check against
               -> TcSigmaType
               -- ^ The type of the hole to check against (possibly modified,
               -- e.g. refined with additional holes for refinement hole-fits.)
               -> TcSigmaType -- ^ The type to check whether fits.
               -> TcM (Bool, HsWrapper)
               -- ^ Whether it was a match, and the wrapper from hole_ty to ty.
tcCheckHoleFit :: TypedHole -> TcType -> TcType -> TcM (Bool, HsWrapper)
tcCheckHoleFit TypedHole
_ TcType
hole_ty TcType
ty | TcType
hole_ty TcType -> TcType -> Bool
`eqType` TcType
ty
    = (Bool, HsWrapper) -> TcM (Bool, HsWrapper)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, HsWrapper
idHsWrapper)
tcCheckHoleFit (TypedHole {[Implication]
Maybe Hole
Bag CtEvidence
th_relevant_cts :: TypedHole -> Bag CtEvidence
th_implics :: TypedHole -> [Implication]
th_hole :: TypedHole -> Maybe Hole
th_relevant_cts :: Bag CtEvidence
th_implics :: [Implication]
th_hole :: Maybe Hole
..}) TcType
hole_ty TcType
ty = TcM (Bool, HsWrapper) -> TcM (Bool, HsWrapper)
forall a. TcRn a -> TcRn a
discardErrs (TcM (Bool, HsWrapper) -> TcM (Bool, HsWrapper))
-> TcM (Bool, HsWrapper) -> TcM (Bool, HsWrapper)
forall a b. (a -> b) -> a -> b
$
  do { -- We wrap the subtype constraint in the implications to pass along the
       -- givens, and so we must ensure that any nested implications and skolems
       -- end up with the correct level. The implications are ordered so that
       -- the innermost (the one with the highest level) is first, so it
       -- suffices to get the level of the first one (or the current level, if
       -- there are no implications involved).
       TcLevel
innermost_lvl <- case [Implication]
th_implics of
                          [] -> IOEnv (Env TcGblEnv TcLclEnv) TcLevel
getTcLevel
                          -- imp is the innermost implication
                          (Implication
imp:[Implication]
_) -> TcLevel -> IOEnv (Env TcGblEnv TcLclEnv) TcLevel
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Implication -> TcLevel
ic_tclvl Implication
imp)
     ; (HsWrapper
wrap, WantedConstraints
wanted) <- TcLevel
-> TcM (HsWrapper, WantedConstraints)
-> TcM (HsWrapper, WantedConstraints)
forall a. TcLevel -> TcM a -> TcM a
setTcLevel TcLevel
innermost_lvl (TcM (HsWrapper, WantedConstraints)
 -> TcM (HsWrapper, WantedConstraints))
-> TcM (HsWrapper, WantedConstraints)
-> TcM (HsWrapper, WantedConstraints)
forall a b. (a -> b) -> a -> b
$ TcM HsWrapper -> TcM (HsWrapper, WantedConstraints)
forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints (TcM HsWrapper -> TcM (HsWrapper, WantedConstraints))
-> TcM HsWrapper -> TcM (HsWrapper, WantedConstraints)
forall a b. (a -> b) -> a -> b
$
                         CtOrigin -> UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
tcSubTypeSigma CtOrigin
orig (ReportRedundantConstraints -> UserTypeCtxt
ExprSigCtxt ReportRedundantConstraints
NoRRC) TcType
ty TcType
hole_ty
     ; String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"Checking hole fit {" SDoc
forall doc. IsOutput doc => doc
empty
     ; String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"wanteds are: " (SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
wanted
     ; if | WantedConstraints -> Bool
isEmptyWC WantedConstraints
wanted, Bag CtEvidence -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag CtEvidence
th_relevant_cts
          -> do { String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"}" SDoc
forall doc. IsOutput doc => doc
empty
                ; (Bool, HsWrapper) -> TcM (Bool, HsWrapper)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, HsWrapper
wrap) }

          | WantedConstraints -> Bool
checkInsoluble WantedConstraints
wanted -- See Note [Fast path for tcCheckHoleFit]
          -> (Bool, HsWrapper) -> TcM (Bool, HsWrapper)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, HsWrapper
wrap)

          | Bool
otherwise
          -> do { EvBindsVar
fresh_binds <- TcM EvBindsVar
newTcEvBinds
                 -- The relevant constraints may contain HoleDests, so we must
                 -- take care to clone them as well (to avoid #15370).
                ; Bag CtEvidence
cloned_relevants <- (CtEvidence -> IOEnv (Env TcGblEnv TcLclEnv) CtEvidence)
-> Bag CtEvidence -> IOEnv (Env TcGblEnv TcLclEnv) (Bag CtEvidence)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM CtEvidence -> IOEnv (Env TcGblEnv TcLclEnv) CtEvidence
cloneWantedCtEv Bag CtEvidence
th_relevant_cts
                  -- We wrap the WC in the nested implications, for details, see
                  -- Note [Checking hole fits]
                ; let wrapInImpls :: WantedConstraints -> WantedConstraints
wrapInImpls WantedConstraints
cts = (WantedConstraints -> Implication -> WantedConstraints)
-> WantedConstraints -> [Implication] -> WantedConstraints
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Implication -> WantedConstraints -> WantedConstraints)
-> WantedConstraints -> Implication -> WantedConstraints
forall a b c. (a -> b -> c) -> b -> a -> c
flip (EvBindsVar -> Implication -> WantedConstraints -> WantedConstraints
setWCAndBinds EvBindsVar
fresh_binds)) WantedConstraints
cts [Implication]
th_implics
                      final_wc :: WantedConstraints
final_wc  = WantedConstraints -> WantedConstraints
wrapInImpls (WantedConstraints -> WantedConstraints)
-> WantedConstraints -> WantedConstraints
forall a b. (a -> b) -> a -> b
$ WantedConstraints -> Bag Ct -> WantedConstraints
addSimples WantedConstraints
wanted (Bag Ct -> WantedConstraints) -> Bag Ct -> WantedConstraints
forall a b. (a -> b) -> a -> b
$
                                  (CtEvidence -> Ct) -> Bag CtEvidence -> Bag Ct
forall a b. (a -> b) -> Bag a -> Bag b
mapBag CtEvidence -> Ct
mkNonCanonical Bag CtEvidence
cloned_relevants
                  -- We add the cloned relevants to the wanteds generated
                  -- by the call to tcSubType_NC, for details, see
                  -- Note [Relevant constraints]. There's no need to clone
                  -- the wanteds, because they are freshly generated by the
                  -- call to`tcSubtype_NC`.
                ; String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"final_wc is: " (SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
final_wc
                  -- See Note [Speeding up valid hole-fits]
                ; (Maybe WantedConstraints
rem, Messages TcRnMessage
_) <- TcRn WantedConstraints
-> TcRn (Maybe WantedConstraints, Messages TcRnMessage)
forall a. TcRn a -> TcRn (Maybe a, Messages TcRnMessage)
tryTc (TcRn WantedConstraints
 -> TcRn (Maybe WantedConstraints, Messages TcRnMessage))
-> TcRn WantedConstraints
-> TcRn (Maybe WantedConstraints, Messages TcRnMessage)
forall a b. (a -> b) -> a -> b
$ TcS WantedConstraints -> TcRn WantedConstraints
forall a. TcS a -> TcM a
runTcSEarlyAbort (TcS WantedConstraints -> TcRn WantedConstraints)
-> TcS WantedConstraints -> TcRn WantedConstraints
forall a b. (a -> b) -> a -> b
$ WantedConstraints -> TcS WantedConstraints
simplifyTopWanteds WantedConstraints
final_wc
                ; String -> SDoc -> IOEnv (Env TcGblEnv TcLclEnv) ()
traceTc String
"}" SDoc
forall doc. IsOutput doc => doc
empty
                ; (Bool, HsWrapper) -> TcM (Bool, HsWrapper)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((WantedConstraints -> Bool) -> Maybe WantedConstraints -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any WantedConstraints -> Bool
isSolvedWC Maybe WantedConstraints
rem, HsWrapper
wrap) } }
  where
    orig :: CtOrigin
orig = Maybe RdrName -> CtOrigin
ExprHoleOrigin (Hole -> RdrName
hole_occ (Hole -> RdrName) -> Maybe Hole -> Maybe RdrName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Hole
th_hole)

    setWCAndBinds :: EvBindsVar         -- Fresh ev binds var.
                  -> Implication        -- The implication to put WC in.
                  -> WantedConstraints  -- The WC constraints to put implic.
                  -> WantedConstraints  -- The new constraints.
    setWCAndBinds :: EvBindsVar -> Implication -> WantedConstraints -> WantedConstraints
setWCAndBinds EvBindsVar
binds Implication
imp WantedConstraints
wc
      = Bag Implication -> WantedConstraints
mkImplicWC (Bag Implication -> WantedConstraints)
-> Bag Implication -> WantedConstraints
forall a b. (a -> b) -> a -> b
$ Implication -> Bag Implication
forall a. a -> Bag a
unitBag (Implication -> Bag Implication) -> Implication -> Bag Implication
forall a b. (a -> b) -> a -> b
$ Implication
imp { ic_wanted = wc , ic_binds = binds }

{- Note [Fast path for tcCheckHoleFit]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In `tcCheckHoleFit` we compare (with `tcSubTypeSigma`) the type of the hole
with the type of zillions of in-scope functions, to see which would "fit".
Most of these checks fail!  They generate obviously-insoluble constraints.
For these very-common cases we don't want to crank up the full constraint
solver.  It's much more efficient to do a quick-and-dirty check for insolubility.

Now, `tcSubTypeSigma` uses the on-the-fly unifier in GHC.Tc.Utils.Unify,
it has already done the dirt-simple unification. So our quick-and-dirty
check can simply look for constraints like (Int ~ Bool).  We don't need
to worry about (Maybe Int ~ Maybe Bool).

The quick-and-dirty check is in `checkInsoluble`. It can make a big
difference: For test hard_hole_fits, compile-time allocation goes down by 37%!
-}


checkInsoluble :: WantedConstraints -> Bool
-- See Note [Fast path for tcCheckHoleFit]
checkInsoluble :: WantedConstraints -> Bool
checkInsoluble (WC { wc_simple :: WantedConstraints -> Bag Ct
wc_simple = Bag Ct
simples })
  = (Ct -> Bool) -> Bag Ct -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Ct -> Bool
is_insol Bag Ct
simples
  where
    is_insol :: Ct -> Bool
is_insol Ct
ct = case TcType -> Pred
classifyPredType (Ct -> TcType
ctPred Ct
ct) of
                    EqPred EqRel
r TcType
t1 TcType
t2 -> Role -> TcType -> TcType -> Bool
definitelyNotEqual (EqRel -> Role
eqRelRole EqRel
r) TcType
t1 TcType
t2
                    Pred
_              -> Bool
False

definitelyNotEqual :: Role -> TcType -> TcType -> Bool
-- See Note [Fast path for tcCheckHoleFit]
-- Specifically, does not need to recurse under type constructors
definitelyNotEqual :: Role -> TcType -> TcType -> Bool
definitelyNotEqual Role
r TcType
t1 TcType
t2
  = TcType -> TcType -> Bool
go TcType
t1 TcType
t2
  where
    go :: TcType -> TcType -> Bool
go TcType
t1 TcType
t2
      | Just TcType
t1' <- TcType -> Maybe TcType
coreView TcType
t1 = TcType -> TcType -> Bool
go TcType
t1' TcType
t2
      | Just TcType
t2' <- TcType -> Maybe TcType
coreView TcType
t2 = TcType -> TcType -> Bool
go TcType
t1 TcType
t2'

    go (TyConApp TyCon
tc [TcType]
_) TcType
t2 | TyCon -> Role -> Bool
isGenerativeTyCon TyCon
tc Role
r = TyCon -> TcType -> Bool
go_tc TyCon
tc TcType
t2
    go TcType
t1 (TyConApp TyCon
tc [TcType]
_) | TyCon -> Role -> Bool
isGenerativeTyCon TyCon
tc Role
r = TyCon -> TcType -> Bool
go_tc TyCon
tc TcType
t1
    go (FunTy {ft_af :: TcType -> FunTyFlag
ft_af = FunTyFlag
af1}) (FunTy {ft_af :: TcType -> FunTyFlag
ft_af = FunTyFlag
af2}) = FunTyFlag
af1 FunTyFlag -> FunTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
/= FunTyFlag
af2
    go TcType
_ TcType
_ = Bool
False

    go_tc :: TyCon -> TcType -> Bool
    -- The TyCon is generative, and is not a saturated FunTy
    go_tc :: TyCon -> TcType -> Bool
go_tc TyCon
tc1 (TyConApp TyCon
tc2 [TcType]
_) | TyCon -> Role -> Bool
isGenerativeTyCon TyCon
tc2 Role
r = TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
/= TyCon
tc2
    go_tc TyCon
_ (FunTy {})    = Bool
True
    go_tc TyCon
_ (ForAllTy {}) = Bool
True
    go_tc TyCon
_ TcType
_ = Bool
False