module TcHoleErrors ( findValidHoleFits, tcFilterHoleFits, HoleFit (..)
                    , HoleFitCandidate (..), tcCheckHoleFit, tcSubsumes
                    , withoutUnification ) where

import GhcPrelude

import TcRnTypes
import TcRnMonad
import TcMType
import TcEvidence
import TcType
import Type
import DataCon
import Name
import RdrName ( pprNameProvenance , GlobalRdrElt (..), globalRdrEnvElts )
import PrelNames ( gHC_ERR )
import Id
import VarSet
import VarEnv
import Bag
import ConLike          ( ConLike(..) )
import Util
import TcEnv (tcLookup)
import Outputable
import DynFlags
import Maybes
import FV ( fvVarList, fvVarSet, unionFV, mkFVs, FV )

import Control.Arrow ( (&&&) )

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


import TcSimplify    ( simpl_top, runTcSDeriveds )
import TcUnify       ( tcSubType_NC )

import ExtractDocs ( extractDocs )
import qualified Data.Map as Map
import HsDoc           ( HsDocString, unpackHDS, DeclDocMap(..) )
import HscTypes        ( ModIface(..) )
import LoadIface       ( loadInterfaceForNameMaybe )

import PrelInfo (knownKeyNames)


{-
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 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 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 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 [Nested implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

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 _

The hole will result in the hole constraint:

  [WD] __a1ph {0}:: a0_a1pd[tau:2] (CHoleCan: ExprHole(_))

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 =
              [WD] __a1ph {0}:: a_a1pd[tau:2] (CHoleCan: ExprHole(_))
              [WD] $dShow_a1pe {0}:: Show a_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 information about the skolem
`a_a1pa[sk:2]` fulfills the Show constraint.

The simples are:

  [[WD] __a1ph {0}:: a0_a1pd[tau:2] (CHoleCan: ExprHole(_)),
    [WD] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CNonCanonical)]

I.e. the hole `a0_a1pd[tau:2]` and the constraint that the type of the hole must
fulfill `Show a0_a1pd[tau:2])`.

So when we run the check, we need to make sure that the

  [WD] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CNonCanonical)

Constraint gets solved. When we now check for whether `x :: a0_a1pd[tau:2]` fits
the hole in `tcCheckHoleFit`, the call to `tcSubType` will end up writing 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 =
                  [WD] $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.


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 Trac #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 _

Where the simples will be :

  [[WD] __a1kz {0}:: a0_a1kv[tau:1] (CHoleCan: ExprHole(_)),
    [WD] $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`, and the simple constraints passed to
findValidHoleFits are:

  [[WD] _a_a1pi {0}:: String
                        -> a0_a1pd[tau:2] (CHoleCan: ExprHole(_b)),
    [WD] _b_a1ps {0}:: a1_a1po[tau:2] (CHoleCan: ExprHole(_a)),
    [WD] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CNonCanonical),
    [WD] $dShow_a1pp {0}:: Show a1_a1po[tau:2] (CNonCanonical)]


Here we have the two hole constraints for `_a` and `_b`, but also additional
constraints that these holes must fulfill. When we are looking for a match for
the hole `_a`, we filter the simple constraints to the "Relevant constraints",
by throwing out all hole constraints and 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_a1pp` constraint is solved, since that is
the only non-hole 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.

-}


data HoleFitDispConfig = HFDC { HoleFitDispConfig -> Bool
showWrap :: Bool
                              , HoleFitDispConfig -> Bool
showWrapVars :: Bool
                              , HoleFitDispConfig -> Bool
showType :: Bool
                              , HoleFitDispConfig -> Bool
showProv :: Bool
                              , HoleFitDispConfig -> Bool
showMatches :: Bool }

debugHoleFitDispConfig :: HoleFitDispConfig
debugHoleFitDispConfig :: HoleFitDispConfig
debugHoleFitDispConfig = Bool -> Bool -> Bool -> Bool -> Bool -> HoleFitDispConfig
HFDC Bool
True Bool
True Bool
True Bool
False Bool
False


-- 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 (m :: * -> *) a. Monad m => a -> m a
return HFDC :: Bool -> Bool -> Bool -> Bool -> Bool -> HoleFitDispConfig
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 SortingAlg = NoSorting      -- Do not sort the fits at all
                | BySize         -- Sort them by the size of the match
                | BySubsumption  -- Sort by full subsumption
                deriving (SortingAlg -> SortingAlg -> Bool
(SortingAlg -> SortingAlg -> Bool)
-> (SortingAlg -> SortingAlg -> Bool) -> Eq SortingAlg
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SortingAlg -> SortingAlg -> Bool
$c/= :: SortingAlg -> SortingAlg -> Bool
== :: SortingAlg -> SortingAlg -> Bool
$c== :: SortingAlg -> SortingAlg -> Bool
Eq, Eq SortingAlg
Eq SortingAlg =>
(SortingAlg -> SortingAlg -> Ordering)
-> (SortingAlg -> SortingAlg -> Bool)
-> (SortingAlg -> SortingAlg -> Bool)
-> (SortingAlg -> SortingAlg -> Bool)
-> (SortingAlg -> SortingAlg -> Bool)
-> (SortingAlg -> SortingAlg -> SortingAlg)
-> (SortingAlg -> SortingAlg -> SortingAlg)
-> Ord SortingAlg
SortingAlg -> SortingAlg -> Bool
SortingAlg -> SortingAlg -> Ordering
SortingAlg -> SortingAlg -> SortingAlg
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
min :: SortingAlg -> SortingAlg -> SortingAlg
$cmin :: SortingAlg -> SortingAlg -> SortingAlg
max :: SortingAlg -> SortingAlg -> SortingAlg
$cmax :: SortingAlg -> SortingAlg -> SortingAlg
>= :: SortingAlg -> SortingAlg -> Bool
$c>= :: SortingAlg -> SortingAlg -> Bool
> :: SortingAlg -> SortingAlg -> Bool
$c> :: SortingAlg -> SortingAlg -> Bool
<= :: SortingAlg -> SortingAlg -> Bool
$c<= :: SortingAlg -> SortingAlg -> Bool
< :: SortingAlg -> SortingAlg -> Bool
$c< :: SortingAlg -> SortingAlg -> Bool
compare :: SortingAlg -> SortingAlg -> Ordering
$ccompare :: SortingAlg -> SortingAlg -> Ordering
$cp1Ord :: Eq SortingAlg
Ord)

getSortingAlg :: TcM SortingAlg
getSortingAlg :: TcM SortingAlg
getSortingAlg =
    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.
       ; SortingAlg -> TcM SortingAlg
forall (m :: * -> *) a. Monad m => a -> m a
return (SortingAlg -> TcM SortingAlg) -> SortingAlg -> TcM SortingAlg
forall a b. (a -> b) -> a -> b
$ if Bool -> Bool
not Bool
shouldSort
                    then SortingAlg
NoSorting
                    else if Bool
subsumSort
                         then SortingAlg
BySubsumption
                         else if Bool
sizeSort
                              then SortingAlg
BySize
                              else SortingAlg
NoSorting }


-- | HoleFitCandidates are passed to the filter and checked whether they can be
-- made to fit.
data HoleFitCandidate = IdHFCand Id             -- An id, like locals.
                      | NameHFCand Name         -- A name, like built-in syntax.
                      | GreHFCand GlobalRdrElt  -- A global, like imported ids.
                      deriving (HoleFitCandidate -> HoleFitCandidate -> Bool
(HoleFitCandidate -> HoleFitCandidate -> Bool)
-> (HoleFitCandidate -> HoleFitCandidate -> Bool)
-> Eq HoleFitCandidate
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HoleFitCandidate -> HoleFitCandidate -> Bool
$c/= :: HoleFitCandidate -> HoleFitCandidate -> Bool
== :: HoleFitCandidate -> HoleFitCandidate -> Bool
$c== :: HoleFitCandidate -> HoleFitCandidate -> Bool
Eq)
instance Outputable HoleFitCandidate where
  ppr :: HoleFitCandidate -> SDoc
ppr = HoleFitCandidate -> SDoc
pprHoleFitCand

pprHoleFitCand :: HoleFitCandidate -> SDoc
pprHoleFitCand :: HoleFitCandidate -> SDoc
pprHoleFitCand (IdHFCand id :: Id
id) = String -> SDoc
text "Id HFC: " SDoc -> SDoc -> SDoc
<> Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
id
pprHoleFitCand (NameHFCand name :: Name
name) = String -> SDoc
text "Name HFC: " SDoc -> SDoc -> SDoc
<> Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
name
pprHoleFitCand (GreHFCand gre :: GlobalRdrElt
gre) = String -> SDoc
text "Gre HFC: " SDoc -> SDoc -> SDoc
<> GlobalRdrElt -> SDoc
forall a. Outputable a => a -> SDoc
ppr GlobalRdrElt
gre

instance HasOccName HoleFitCandidate where
  occName :: HoleFitCandidate -> OccName
occName hfc :: HoleFitCandidate
hfc = case HoleFitCandidate
hfc of
                  IdHFCand id :: Id
id -> Id -> OccName
forall name. HasOccName name => name -> OccName
occName Id
id
                  NameHFCand name :: Name
name -> Name -> OccName
forall name. HasOccName name => name -> OccName
occName Name
name
                  GreHFCand gre :: GlobalRdrElt
gre -> Name -> OccName
forall name. HasOccName name => name -> OccName
occName (GlobalRdrElt -> Name
gre_name GlobalRdrElt
gre)

-- | HoleFit is the type we use for valid hole fits. It contains the
-- element that was checked, the Id of that element as found by `tcLookup`,
-- and the refinement level of the fit, which is the number of extra argument
-- holes that this fit uses (e.g. if hfRefLvl is 2, the fit is for `Id _ _`).
data HoleFit =
  HoleFit { HoleFit -> Id
hfId   :: Id       -- The elements id in the TcM
          , HoleFit -> HoleFitCandidate
hfCand :: HoleFitCandidate  -- The candidate that was checked.
          , HoleFit -> TcType
hfType :: TcType -- The type of the id, possibly zonked.
          , HoleFit -> Int
hfRefLvl :: Int  -- The number of holes in this fit.
          , HoleFit -> [TcType]
hfWrap :: [TcType] -- The wrapper for the match.
          , HoleFit -> [TcType]
hfMatches :: [TcType]  -- What the refinement variables got matched
                                   -- with, if anything
          , HoleFit -> Maybe HsDocString
hfDoc :: Maybe HsDocString } -- Documentation of this HoleFit, if
                                         -- available.


hfName :: HoleFit -> Name
hfName :: HoleFit -> Name
hfName hf :: HoleFit
hf = case HoleFit -> HoleFitCandidate
hfCand HoleFit
hf of
              IdHFCand id :: Id
id -> Id -> Name
idName Id
id
              NameHFCand name :: Name
name -> Name
name
              GreHFCand gre :: GlobalRdrElt
gre -> GlobalRdrElt -> Name
gre_name GlobalRdrElt
gre

hfIsLcl :: HoleFit -> Bool
hfIsLcl :: HoleFit -> Bool
hfIsLcl hf :: HoleFit
hf = case HoleFit -> HoleFitCandidate
hfCand HoleFit
hf of
               IdHFCand _    -> Bool
True
               NameHFCand _  -> Bool
False
               GreHFCand gre :: GlobalRdrElt
gre -> GlobalRdrElt -> Bool
gre_lcl GlobalRdrElt
gre

-- We define an Eq and Ord instance to be able to build a graph.
instance Eq HoleFit where
   == :: HoleFit -> HoleFit -> Bool
(==) = Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Id -> Id -> Bool) -> (HoleFit -> Id) -> HoleFit -> HoleFit -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` HoleFit -> Id
hfId

-- We compare HoleFits by their name instead of their Id, since we don't
-- want our tests to be affected by the non-determinism of `nonDetCmpVar`,
-- which is used to compare Ids. When comparing, we want HoleFits with a lower
-- refinement level to come first.
instance Ord HoleFit where
  compare :: HoleFit -> HoleFit -> Ordering
compare a :: HoleFit
a b :: HoleFit
b = HoleFit -> HoleFit -> Ordering
cmp HoleFit
a HoleFit
b
    where cmp :: HoleFit -> HoleFit -> Ordering
cmp  = if HoleFit -> Int
hfRefLvl HoleFit
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== HoleFit -> Int
hfRefLvl HoleFit
b
                 then Name -> Name -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Name -> Name -> Ordering)
-> (HoleFit -> Name) -> HoleFit -> HoleFit -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` HoleFit -> Name
hfName
                 else Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (HoleFit -> Int) -> HoleFit -> HoleFit -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` HoleFit -> Int
hfRefLvl

instance Outputable HoleFit where
    ppr :: HoleFit -> SDoc
ppr = HoleFitDispConfig -> HoleFit -> SDoc
pprHoleFit HoleFitDispConfig
debugHoleFitDispConfig

-- 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)
addDocs :: [HoleFit] -> TcM [HoleFit]
addDocs :: [HoleFit] -> TcM [HoleFit]
addDocs fits :: [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 { (_, DeclDocMap lclDocs :: Map Name HsDocString
lclDocs, _) <- TcGblEnv -> (Maybe HsDocString, DeclDocMap, ArgDocMap)
extractDocs (TcGblEnv -> (Maybe HsDocString, DeclDocMap, ArgDocMap))
-> IOEnv (Env TcGblEnv TcLclEnv) TcGblEnv
-> IOEnv
     (Env TcGblEnv TcLclEnv) (Maybe HsDocString, DeclDocMap, ArgDocMap)
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
               ; (HoleFit -> IOEnv (Env TcGblEnv TcLclEnv) HoleFit)
-> [HoleFit] -> TcM [HoleFit]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Map Name HsDocString
-> HoleFit -> IOEnv (Env TcGblEnv TcLclEnv) HoleFit
upd Map Name HsDocString
lclDocs) [HoleFit]
fits }
       else [HoleFit] -> TcM [HoleFit]
forall (m :: * -> *) a. Monad m => a -> m a
return [HoleFit]
fits }
  where
   msg :: SDoc
msg = String -> SDoc
text "TcHoleErrors addDocs"
   lookupInIface :: Name -> ModIface -> Maybe HsDocString
lookupInIface name :: Name
name (ModIface { mi_decl_docs :: ModIface -> DeclDocMap
mi_decl_docs = DeclDocMap dmap :: Map Name HsDocString
dmap })
     = Name -> Map Name HsDocString -> Maybe HsDocString
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
name Map Name HsDocString
dmap
   upd :: Map Name HsDocString
-> HoleFit -> IOEnv (Env TcGblEnv TcLclEnv) HoleFit
upd lclDocs :: Map Name HsDocString
lclDocs fit :: HoleFit
fit =
     let name :: Name
name = HoleFit -> Name
hfName HoleFit
fit in
     do { Maybe HsDocString
doc <- if HoleFit -> Bool
hfIsLcl HoleFit
fit
                 then Maybe HsDocString
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe HsDocString)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Map Name HsDocString -> Maybe HsDocString
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
name Map Name HsDocString
lclDocs)
                 else do { Maybe ModIface
mbIface <- SDoc -> Name -> TcRn (Maybe ModIface)
loadInterfaceForNameMaybe SDoc
msg Name
name
                         ; Maybe HsDocString
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe HsDocString)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe HsDocString
 -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe HsDocString))
-> Maybe HsDocString
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe HsDocString)
forall a b. (a -> b) -> a -> b
$ Maybe ModIface
mbIface Maybe ModIface
-> (ModIface -> Maybe HsDocString) -> Maybe HsDocString
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> ModIface -> Maybe HsDocString
lookupInIface Name
name }
        ; HoleFit -> IOEnv (Env TcGblEnv TcLclEnv) HoleFit
forall (m :: * -> *) a. Monad m => a -> m a
return (HoleFit -> IOEnv (Env TcGblEnv TcLclEnv) HoleFit)
-> HoleFit -> IOEnv (Env TcGblEnv TcLclEnv) HoleFit
forall a b. (a -> b) -> a -> b
$ HoleFit
fit {hfDoc :: Maybe HsDocString
hfDoc = Maybe HsDocString
doc} }

-- 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 (HFDC sWrp :: Bool
sWrp sWrpVars :: Bool
sWrpVars sTy :: Bool
sTy sProv :: Bool
sProv sMs :: Bool
sMs) hf :: HoleFit
hf = SDoc -> Int -> SDoc -> SDoc
hang SDoc
display 2 SDoc
provenance
    where name :: Name
name = HoleFit -> Name
hfName HoleFit
hf
          ty :: TcType
ty = HoleFit -> TcType
hfType HoleFit
hf
          matches :: [TcType]
matches =  HoleFit -> [TcType]
hfMatches HoleFit
hf
          wrap :: [TcType]
wrap = HoleFit -> [TcType]
hfWrap HoleFit
hf
          tyApp :: SDoc
tyApp = [SDoc] -> SDoc
sep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ (TcType -> SDoc) -> [TcType] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> SDoc
text "@" SDoc -> SDoc -> SDoc
<>) (SDoc -> SDoc) -> (TcType -> SDoc) -> TcType -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcType -> SDoc
pprParendType) [TcType]
wrap
          tyAppVars :: SDoc
tyAppVars = [SDoc] -> SDoc
sep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
comma ([SDoc] -> [SDoc]) -> [SDoc] -> [SDoc]
forall a b. (a -> b) -> a -> b
$
              ((Id, TcType) -> SDoc) -> [(Id, TcType)] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (\(v :: Id
v,t :: TcType
t) -> Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
v SDoc -> SDoc -> SDoc
<+> String -> SDoc
text "~" SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
pprParendType TcType
t) ([(Id, TcType)] -> [SDoc]) -> [(Id, TcType)] -> [SDoc]
forall a b. (a -> b) -> a -> b
$
                [Id] -> [TcType] -> [(Id, TcType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Id]
vars [TcType]
wrap
            where
              vars :: [Id]
vars = TcType -> [Id]
unwrapTypeVars TcType
ty
              -- 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 -> [TyVar]
              unwrapTypeVars :: TcType -> [Id]
unwrapTypeVars t :: TcType
t = [Id]
vars [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ case TcType -> Maybe (TcType, TcType)
splitFunTy_maybe TcType
unforalled of
                                  Just (_, unfunned :: TcType
unfunned) -> TcType -> [Id]
unwrapTypeVars TcType
unfunned
                                  _ -> []
                where (vars :: [Id]
vars, unforalled :: TcType
unforalled) = TcType -> ([Id], TcType)
splitForAllTys TcType
t
          holeVs :: SDoc
holeVs = [SDoc] -> SDoc
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
parens (SDoc -> SDoc) -> (TcType -> SDoc) -> TcType -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> SDoc
text "_" SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+>) (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]
matches
          holeDisp :: SDoc
holeDisp = if Bool
sMs then SDoc
holeVs
                     else [SDoc] -> SDoc
sep ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ Int -> SDoc -> [SDoc]
forall a. Int -> a -> [a]
replicate ([TcType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TcType]
matches) (SDoc -> [SDoc]) -> SDoc -> [SDoc]
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text "_"
          occDisp :: SDoc
occDisp = Name -> SDoc
forall a. OutputableBndr a => a -> SDoc
pprPrefixOcc Name
name
          tyDisp :: SDoc
tyDisp = Bool -> SDoc -> SDoc
ppWhen Bool
sTy (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty
          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 (t :: * -> *) a. Foldable t => t a -> Bool
null
          wrapDisp :: SDoc
wrapDisp = Bool -> SDoc -> SDoc
ppWhen ([TcType] -> Bool
forall a. [a] -> Bool
has [TcType]
wrap Bool -> Bool -> Bool
&& (Bool
sWrp Bool -> Bool -> Bool
|| Bool
sWrpVars))
                      (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text "with" SDoc -> SDoc -> SDoc
<+> if Bool
sWrp Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
sTy
                                        then SDoc
occDisp SDoc -> SDoc -> SDoc
<+> SDoc
tyApp
                                        else SDoc
tyAppVars
          docs :: SDoc
docs = case HoleFit -> Maybe HsDocString
hfDoc HoleFit
hf of
                   Just d :: HsDocString
d -> String -> SDoc
text "{-^" SDoc -> SDoc -> SDoc
<>
                             ([SDoc] -> SDoc
vcat ([SDoc] -> SDoc) -> (HsDocString -> [SDoc]) -> HsDocString -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> SDoc) -> [String] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map String -> SDoc
text ([String] -> [SDoc])
-> (HsDocString -> [String]) -> HsDocString -> [SDoc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines (String -> [String])
-> (HsDocString -> String) -> HsDocString -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsDocString -> String
unpackHDS) HsDocString
d
                             SDoc -> SDoc -> SDoc
<> String -> SDoc
text "-}"
                   _ -> SDoc
empty
          funcInfo :: SDoc
funcInfo = Bool -> SDoc -> SDoc
ppWhen ([TcType] -> Bool
forall a. [a] -> Bool
has [TcType]
matches Bool -> Bool -> Bool
&& Bool
sTy) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                       String -> SDoc
text "where" SDoc -> SDoc -> SDoc
<+> SDoc
occDisp SDoc -> SDoc -> SDoc
<+> SDoc
tyDisp
          subDisp :: SDoc
subDisp = SDoc
occDisp SDoc -> SDoc -> SDoc
<+> if [TcType] -> Bool
forall a. [a] -> Bool
has [TcType]
matches then SDoc
holeDisp else SDoc
tyDisp
          display :: SDoc
display =  SDoc
subDisp SDoc -> SDoc -> SDoc
$$ Int -> SDoc -> SDoc
nest 2 (SDoc
funcInfo SDoc -> SDoc -> SDoc
$+$ SDoc
docs SDoc -> SDoc -> SDoc
$+$ SDoc
wrapDisp)
          provenance :: SDoc
provenance = Bool -> SDoc -> SDoc
ppWhen Bool
sProv (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> SDoc
parens (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                case HoleFit -> HoleFitCandidate
hfCand HoleFit
hf of
                    GreHFCand gre :: GlobalRdrElt
gre -> GlobalRdrElt -> SDoc
pprNameProvenance GlobalRdrElt
gre
                    _ -> String -> SDoc
text "bound at" SDoc -> SDoc -> SDoc
<+> SrcLoc -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Name -> SrcLoc
forall a. NamedThing a => a -> SrcLoc
getSrcLoc Name
name)

getLocalBindings :: TidyEnv -> Ct -> TcM [Id]
getLocalBindings :: TidyEnv -> Ct -> TcM [Id]
getLocalBindings tidy_orig :: TidyEnv
tidy_orig ct :: Ct
ct
 = do { (env1 :: TidyEnv
env1, _) <- TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
tidy_orig (CtLoc -> CtOrigin
ctLocOrigin CtLoc
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
$ TcLclEnv -> [TcBinder]
tcl_bndrs TcLclEnv
lcl_env) }
  where
    loc :: CtLoc
loc     = CtEvidence -> CtLoc
ctEvLoc (Ct -> CtEvidence
ctEvidence Ct
ct)
    lcl_env :: TcLclEnv
lcl_env = CtLoc -> TcLclEnv
ctLocEnv CtLoc
loc

    go :: TidyEnv -> [Id] -> [TcBinder] -> TcM [Id]
    go :: TidyEnv -> [Id] -> [TcBinder] -> TcM [Id]
go _ sofar :: [Id]
sofar [] = [Id] -> TcM [Id]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Id] -> [Id]
forall a. [a] -> [a]
reverse [Id]
sofar)
    go env :: TidyEnv
env sofar :: [Id]
sofar (tc_bndr :: TcBinder
tc_bndr : tc_bndrs :: [TcBinder]
tc_bndrs) =
        case TcBinder
tc_bndr of
          TcIdBndr id :: Id
id _ -> Id -> TcM [Id]
keep_it Id
id
          _ -> 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
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
                  -> [Ct]
                  -- ^ The  unsolved simple constraints in the implication for
                  -- the hole.
                  -> Ct -- ^ The hole constraint itself
                  -> TcM (TidyEnv, SDoc)
findValidHoleFits :: TidyEnv -> [Implication] -> [Ct] -> Ct -> TcM (TidyEnv, SDoc)
findValidHoleFits tidy_env :: TidyEnv
tidy_env implics :: [Implication]
implics simples :: [Ct]
simples ct :: Ct
ct | Ct -> Bool
isExprHoleCt Ct
ct =
  do { GlobalRdrEnv
rdr_env <- TcRn GlobalRdrEnv
getGlobalRdrEnv
     ; [Id]
lclBinds <- TidyEnv -> Ct -> TcM [Id]
getLocalBindings TidyEnv
tidy_env Ct
ct
     ; 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
     ; HoleFitDispConfig
hfdc <- TcM HoleFitDispConfig
getHoleFitDispConfig
     ; SortingAlg
sortingAlg <- TcM SortingAlg
getSortingAlg
     ; let findVLimit :: Maybe Int
findVLimit = if SortingAlg
sortingAlg SortingAlg -> SortingAlg -> Bool
forall a. Ord a => a -> a -> Bool
> SortingAlg
NoSorting then Maybe Int
forall a. Maybe a
Nothing else Maybe Int
maxVSubs
     ; Maybe Int
refLevel <- DynFlags -> Maybe Int
refLevelHoleFits (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
     ; String -> SDoc -> TcRn ()
traceTc "findingValidHoleFitsFor { " (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct
     ; String -> SDoc -> TcRn ()
traceTc "hole_lvl is:" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
hole_lvl
     ; String -> SDoc -> TcRn ()
traceTc "implics are: " (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ [Implication] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Implication]
implics
     ; String -> SDoc -> TcRn ()
traceTc "simples are: " (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ [Ct] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Ct]
simples
     ; String -> SDoc -> TcRn ()
traceTc "locals are: " (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ [Id] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
lclBinds
     ; let (lcl :: [GlobalRdrElt]
lcl, gbl :: [GlobalRdrElt]
gbl) = (GlobalRdrElt -> Bool)
-> [GlobalRdrElt] -> ([GlobalRdrElt], [GlobalRdrElt])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition GlobalRdrElt -> Bool
gre_lcl (GlobalRdrEnv -> [GlobalRdrElt]
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
           to_check :: [HoleFitCandidate]
to_check = [HoleFitCandidate]
locals [HoleFitCandidate] -> [HoleFitCandidate] -> [HoleFitCandidate]
forall a. [a] -> [a] -> [a]
++ [HoleFitCandidate]
syntax [HoleFitCandidate] -> [HoleFitCandidate] -> [HoleFitCandidate]
forall a. [a] -> [a] -> [a]
++ [HoleFitCandidate]
globals
     ; (searchDiscards :: Bool
searchDiscards, subs :: [HoleFit]
subs) <-
        Maybe Int
-> [Implication]
-> [Ct]
-> (TcType, [Id])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
tcFilterHoleFits Maybe Int
findVLimit [Implication]
implics [Ct]
relevantCts (TcType
hole_ty, []) [HoleFitCandidate]
to_check
     ; (tidy_env :: TidyEnv
tidy_env, tidy_subs :: [HoleFit]
tidy_subs) <- TidyEnv -> [HoleFit] -> TcM (TidyEnv, [HoleFit])
zonkSubs TidyEnv
tidy_env [HoleFit]
subs
     ; [HoleFit]
tidy_sorted_subs <- SortingAlg -> [HoleFit] -> TcM [HoleFit]
sortFits SortingAlg
sortingAlg [HoleFit]
tidy_subs
     ; let (pVDisc :: Bool
pVDisc, limited_subs :: [HoleFit]
limited_subs) = Maybe Int -> [HoleFit] -> (Bool, [HoleFit])
possiblyDiscard Maybe Int
maxVSubs [HoleFit]
tidy_sorted_subs
           vDiscards :: Bool
vDiscards = Bool
pVDisc Bool -> Bool -> Bool
|| Bool
searchDiscards
     ; [HoleFit]
subs_with_docs <- [HoleFit] -> TcM [HoleFit]
addDocs [HoleFit]
limited_subs
     ; let vMsg :: SDoc
vMsg = Bool -> SDoc -> SDoc
ppUnless ([HoleFit] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [HoleFit]
subs_with_docs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                    SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Valid hole fits include") 2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                      [SDoc] -> SDoc
vcat ((HoleFit -> SDoc) -> [HoleFit] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (HoleFitDispConfig -> HoleFit -> SDoc
pprHoleFit HoleFitDispConfig
hfdc) [HoleFit]
subs_with_docs)
                        SDoc -> SDoc -> SDoc
$$ Bool -> SDoc -> SDoc
ppWhen Bool
vDiscards SDoc
subsDiscardMsg
     -- Refinement hole fits. See Note [Valid refinement hole fits include ...]
     ; (tidy_env :: TidyEnv
tidy_env, refMsg :: SDoc
refMsg) <- 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 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 = [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)
mapM Int -> IOEnv (Env TcGblEnv TcLclEnv) (TcType, [Id])
mkRefTy [Int]
refLvls
            ; String -> SDoc -> TcRn ()
traceTc "ref_tys are" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
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 SortingAlg
sortingAlg SortingAlg -> SortingAlg -> Bool
forall a. Ord a => a -> a -> Bool
> SortingAlg
NoSorting 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)
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
-> [Implication]
-> [Ct]
-> (TcType, [Id])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
tcFilterHoleFits Maybe Int
findRLimit [Implication]
implics
                                     [Ct]
relevantCts) [HoleFitCandidate]
to_check) [(TcType, [Id])]
ref_tys
            ; (tidy_env :: TidyEnv
tidy_env, tidy_rsubs :: [HoleFit]
tidy_rsubs) <- TidyEnv -> [HoleFit] -> TcM (TidyEnv, [HoleFit])
zonkSubs TidyEnv
tidy_env ([HoleFit] -> TcM (TidyEnv, [HoleFit]))
-> [HoleFit] -> TcM (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 <- SortingAlg -> [HoleFit] -> TcM [HoleFit]
sortFits SortingAlg
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.
            ; (tidy_env :: TidyEnv
tidy_env, tidy_hole_ty :: TcType
tidy_hole_ty) <- TidyEnv -> TcType -> TcM (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
                  (exact :: [HoleFit]
exact, not_exact :: [HoleFit]
not_exact) = (HoleFit -> Bool) -> [HoleFit] -> ([HoleFit], [HoleFit])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition HoleFit -> Bool
hasExactApp [HoleFit]
tidy_sorted_rsubs
                  (pRDisc :: Bool
pRDisc, exact_last_rfits :: [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]
not_exact [HoleFit] -> [HoleFit] -> [HoleFit]
forall a. [a] -> [a] -> [a]
++ [HoleFit]
exact
                  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]
addDocs [HoleFit]
exact_last_rfits
            ; (TidyEnv, SDoc) -> TcM (TidyEnv, SDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env,
                Bool -> SDoc -> SDoc
ppUnless ([HoleFit] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [HoleFit]
rsubs_with_docs) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                  SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Valid refinement hole fits include") 2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                  [SDoc] -> SDoc
vcat ((HoleFit -> SDoc) -> [HoleFit] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (HoleFitDispConfig -> HoleFit -> SDoc
pprHoleFit HoleFitDispConfig
hfdc) [HoleFit]
rsubs_with_docs)
                    SDoc -> SDoc -> SDoc
$$ Bool -> SDoc -> SDoc
ppWhen Bool
rDiscards SDoc
refSubsDiscardMsg) }
       else (TidyEnv, SDoc) -> TcM (TidyEnv, SDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env, SDoc
empty)
     ; String -> SDoc -> TcRn ()
traceTc "findingValidHoleFitsFor }" SDoc
empty
     ; (TidyEnv, SDoc) -> TcM (TidyEnv, SDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env, SDoc
vMsg SDoc -> SDoc -> SDoc
$$ SDoc
refMsg) }
  where
    -- We extract the type, the tcLevel and the types free variables
    -- from from the constraint.
    hole_ty :: TcPredType
    hole_ty :: TcType
hole_ty = Ct -> TcType
ctPred Ct
ct
    hole_fvs :: FV
    hole_fvs :: FV
hole_fvs = TcType -> FV
tyCoFVsOfType TcType
hole_ty
    hole_lvl :: TcLevel
hole_lvl = CtLoc -> TcLevel
ctLocLevel (CtLoc -> TcLevel) -> CtLoc -> TcLevel
forall a b. (a -> b) -> a -> b
$ CtEvidence -> CtLoc
ctEvLoc (CtEvidence -> CtLoc) -> CtEvidence -> CtLoc
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct

    -- 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 refLvl :: Int
refLvl = ([Id] -> TcType
wrapWithVars ([Id] -> TcType) -> ([Id] -> [Id]) -> [Id] -> (TcType, [Id])
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
<$>
                            (TcM TcType
newOpenTypeKind TcM TcType
-> (TcType -> IOEnv (Env TcGblEnv TcLclEnv) Id)
-> IOEnv (Env TcGblEnv TcLclEnv) Id
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TcType -> IOEnv (Env TcGblEnv TcLclEnv) Id
newFlexiTyVar)
            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 vars :: [Id]
vars = [TcType] -> TcType -> TcType
mkFunTys ((Id -> TcType) -> [Id] -> [TcType]
forall a b. (a -> b) -> [a] -> [b]
map Id -> TcType
mkTyVarTy [Id]
vars) TcType
hole_ty

    sortFits :: SortingAlg    -- How we should sort the hole fits
             -> [HoleFit]     -- The subs to sort
             -> TcM [HoleFit]
    sortFits :: SortingAlg -> [HoleFit] -> TcM [HoleFit]
sortFits NoSorting subs :: [HoleFit]
subs = [HoleFit] -> TcM [HoleFit]
forall (m :: * -> *) a. Monad m => a -> m a
return [HoleFit]
subs
    sortFits BySize subs :: [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]
sortBySize ([HoleFit] -> [HoleFit]
forall a. Ord a => [a] -> [a]
sort [HoleFit]
lclFits)
               IOEnv (Env TcGblEnv TcLclEnv) ([HoleFit] -> [HoleFit])
-> TcM [HoleFit] -> TcM [HoleFit]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [HoleFit] -> TcM [HoleFit]
sortBySize ([HoleFit] -> [HoleFit]
forall a. Ord a => [a] -> [a]
sort [HoleFit]
gblFits)
        where (lclFits :: [HoleFit]
lclFits, gblFits :: [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 BySubsumption subs :: [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]
sortByGraph ([HoleFit] -> [HoleFit]
forall a. Ord a => [a] -> [a]
sort [HoleFit]
lclFits)
               IOEnv (Env TcGblEnv TcLclEnv) ([HoleFit] -> [HoleFit])
-> TcM [HoleFit] -> TcM [HoleFit]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [HoleFit] -> TcM [HoleFit]
sortByGraph ([HoleFit] -> [HoleFit]
forall a. Ord a => [a] -> [a]
sort [HoleFit]
gblFits)
        where (lclFits :: [HoleFit]
lclFits, gblFits :: [HoleFit]
gblFits) = (HoleFit -> Bool) -> [HoleFit] -> ([HoleFit], [HoleFit])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span HoleFit -> Bool
hfIsLcl [HoleFit]
subs

    -- See Note [Relevant Constraints]
    relevantCts :: [Ct]
    relevantCts :: [Ct]
relevantCts = if VarSet -> Bool
isEmptyVarSet (FV -> VarSet
fvVarSet FV
hole_fvs) then []
                  else (Ct -> Bool) -> [Ct] -> [Ct]
forall a. (a -> Bool) -> [a] -> [a]
filter Ct -> Bool
isRelevant [Ct]
simples
      where ctFreeVarSet :: Ct -> VarSet
            ctFreeVarSet :: Ct -> VarSet
ctFreeVarSet = FV -> VarSet
fvVarSet (FV -> VarSet) -> (Ct -> FV) -> Ct -> VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcType -> FV
tyCoFVsOfType (TcType -> FV) -> (Ct -> TcType) -> Ct -> FV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> TcType
ctPred
            hole_fv_set :: VarSet
hole_fv_set = FV -> VarSet
fvVarSet FV
hole_fvs
            anyFVMentioned :: Ct -> Bool
            anyFVMentioned :: Ct -> Bool
anyFVMentioned ct :: Ct
ct = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ VarSet -> Bool
isEmptyVarSet (VarSet -> Bool) -> VarSet -> Bool
forall a b. (a -> b) -> a -> b
$
                                  Ct -> VarSet
ctFreeVarSet Ct
ct VarSet -> VarSet -> VarSet
`intersectVarSet` VarSet
hole_fv_set
            -- 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 :: Ct -> Bool
isRelevant ct :: Ct
ct = Bool -> Bool
not (VarSet -> Bool
isEmptyVarSet (Ct -> VarSet
ctFreeVarSet Ct
ct))
                            Bool -> Bool -> Bool
&& Ct -> Bool
anyFVMentioned Ct
ct
                            Bool -> Bool -> Bool
&& Bool -> Bool
not (Ct -> Bool
isHoleCt Ct
ct)

    -- We zonk the hole fits so that the output aligns with the rest
    -- of the typed hole error message output.
    zonkSubs :: TidyEnv -> [HoleFit] -> TcM (TidyEnv, [HoleFit])
    zonkSubs :: TidyEnv -> [HoleFit] -> TcM (TidyEnv, [HoleFit])
zonkSubs = [HoleFit] -> TidyEnv -> [HoleFit] -> TcM (TidyEnv, [HoleFit])
zonkSubs' []
      where zonkSubs' :: [HoleFit] -> TidyEnv -> [HoleFit] -> TcM (TidyEnv, [HoleFit])
zonkSubs' zs :: [HoleFit]
zs env :: TidyEnv
env [] = (TidyEnv, [HoleFit]) -> TcM (TidyEnv, [HoleFit])
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, [HoleFit] -> [HoleFit]
forall a. [a] -> [a]
reverse [HoleFit]
zs)
            zonkSubs' zs :: [HoleFit]
zs env :: TidyEnv
env (hf :: HoleFit
hf:hfs :: [HoleFit]
hfs) = do { (env' :: TidyEnv
env', z :: HoleFit
z) <- TidyEnv
-> HoleFit -> IOEnv (Env TcGblEnv TcLclEnv) (TidyEnv, HoleFit)
zonkSub TidyEnv
env HoleFit
hf
                                           ; [HoleFit] -> TidyEnv -> [HoleFit] -> TcM (TidyEnv, [HoleFit])
zonkSubs' (HoleFit
zHoleFit -> [HoleFit] -> [HoleFit]
forall a. a -> [a] -> [a]
:[HoleFit]
zs) TidyEnv
env' [HoleFit]
hfs }
            zonkSub :: TidyEnv
-> HoleFit -> IOEnv (Env TcGblEnv TcLclEnv) (TidyEnv, HoleFit)
zonkSub env :: 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 { (env :: TidyEnv
env, ty' :: TcType
ty') <- TidyEnv -> TcType -> TcM (TidyEnv, TcType)
zonkTidyTcType TidyEnv
env TcType
ty
                   ; (env :: TidyEnv
env, m' :: [TcType]
m') <- TidyEnv -> [TcType] -> TcM (TidyEnv, [TcType])
zonkTidyTcTypes TidyEnv
env [TcType]
m
                   ; (env :: TidyEnv
env, wrp' :: [TcType]
wrp') <- TidyEnv -> [TcType] -> TcM (TidyEnv, [TcType])
zonkTidyTcTypes TidyEnv
env [TcType]
wrp
                   ; let zFit :: HoleFit
zFit = HoleFit
hf {hfType :: TcType
hfType = TcType
ty', hfMatches :: [TcType]
hfMatches = [TcType]
m', hfWrap :: [TcType]
hfWrap = [TcType]
wrp'}
                   ; (TidyEnv, HoleFit)
-> IOEnv (Env TcGblEnv TcLclEnv) (TidyEnv, HoleFit)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, HoleFit
zFit ) }

    -- 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 max :: Int
max) fits :: [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 Nothing fits :: [HoleFit]
fits = (Bool
False, [HoleFit]
fits)

    -- 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.
    sortBySize :: [HoleFit] -> TcM [HoleFit]
    sortBySize :: [HoleFit] -> TcM [HoleFit]
sortBySize = [HoleFit] -> TcM [HoleFit]
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'.
    sortByGraph :: [HoleFit] -> TcM [HoleFit]
    sortByGraph :: [HoleFit] -> TcM [HoleFit]
sortByGraph fits :: [HoleFit]
fits = [(HoleFit, [HoleFit])] -> [HoleFit] -> TcM [HoleFit]
go [] [HoleFit]
fits
      where tcSubsumesWCloning :: TcType -> TcType -> TcM Bool
            tcSubsumesWCloning :: TcType -> TcType -> TcRnIf TcGblEnv TcLclEnv Bool
tcSubsumesWCloning ht :: TcType
ht ty :: 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 sofar :: [(HoleFit, [HoleFit])]
sofar [] = do { String -> SDoc -> TcRn ()
traceTc "subsumptionGraph was" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ [(HoleFit, [HoleFit])] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(HoleFit, [HoleFit])]
sofar
                             ; [HoleFit] -> TcM [HoleFit]
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 (hf :: HoleFit
hf, adjs :: [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
graph, fromV :: Int -> (HoleFit, Id, [Id])
fromV, _) = [(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 ((\(h :: HoleFit
h,_,_) -> 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 sofar :: [(HoleFit, [HoleFit])]
sofar (hf :: HoleFit
hf:hfs :: [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 }

-- We don't (as of yet) handle holes in types, only in expressions.
findValidHoleFits env :: TidyEnv
env _ _ _ = (TidyEnv, SDoc) -> TcM (TidyEnv, SDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, SDoc
empty)


-- | 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
               -> [Implication]
               -- ^ Enclosing implications for givens
               -> [Ct]
               -- ^ Any relevant unsolved simple constraints
               -> (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
-> [Implication]
-> [Ct]
-> (TcType, [Id])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
tcFilterHoleFits (Just 0) _ _ _ _ = (Bool, [HoleFit]) -> TcM (Bool, [HoleFit])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, []) -- Stop right away on 0
tcFilterHoleFits limit :: Maybe Int
limit implics :: [Implication]
implics relevantCts :: [Ct]
relevantCts ht :: (TcType, [Id])
ht@(hole_ty :: TcType
hole_ty, _) candidates :: [HoleFitCandidate]
candidates =
  do { String -> SDoc -> TcRn ()
traceTc "checkingFitsFor {" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
hole_ty
     ; (discards :: Bool
discards, subs :: [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 -> TcRn ()
traceTc "checkingFitsFor }" SDoc
empty
     ; (Bool, [HoleFit]) -> TcM (Bool, [HoleFit])
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 subs :: [HoleFit]
subs _ _ _ [] = (Bool, [HoleFit]) -> TcM (Bool, [HoleFit])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [HoleFit] -> [HoleFit]
forall a. [a] -> [a]
reverse [HoleFit]
subs)
    go subs :: [HoleFit]
subs _ (Just 0) _ _ = (Bool, [HoleFit]) -> TcM (Bool, [HoleFit])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [HoleFit] -> [HoleFit]
forall a. [a] -> [a]
reverse [HoleFit]
subs)
    go subs :: [HoleFit]
subs seen :: VarSet
seen maxleft :: Maybe Int
maxleft ty :: (TcType, [Id])
ty (el :: HoleFitCandidate
el:elts :: [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 -> TcRn ()
traceTc "lookingUp" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ HoleFitCandidate -> SDoc
forall a. Outputable a => a -> SDoc
ppr HoleFitCandidate
el
           ; Maybe Id
maybeThing <- HoleFitCandidate -> TcM (Maybe Id)
lookup HoleFitCandidate
el
           ; case Maybe Id
maybeThing of
               Just id :: Id
id | Id -> Bool
not_trivial Id
id ->
                       do { Maybe ([TcType], [TcType])
fits <- (TcType, [Id]) -> TcType -> TcM (Maybe ([TcType], [TcType]))
fitsHole (TcType, [Id])
ty (Id -> TcType
idType Id
id)
                          ; case Maybe ([TcType], [TcType])
fits of
                              Just (wrp :: [TcType]
wrp, matches :: [TcType]
matches) -> Id -> [TcType] -> [TcType] -> TcM (Bool, [HoleFit])
keep_it Id
id [TcType]
wrp [TcType]
matches
                              _ -> TcM (Bool, [HoleFit])
discard_it }
               _ -> TcM (Bool, [HoleFit])
discard_it }
        where
          -- We want to filter out undefined and the likes from GHC.Err
          not_trivial :: Id -> Bool
not_trivial id :: Id
id = Name -> Maybe Module
nameModule_maybe (Id -> Name
idName Id
id) Maybe Module -> Maybe Module -> Bool
forall a. Eq a => a -> a -> Bool
/= Module -> Maybe Module
forall a. a -> Maybe a
Just Module
gHC_ERR

          lookup :: HoleFitCandidate -> TcM (Maybe Id)
          lookup :: HoleFitCandidate -> TcM (Maybe Id)
lookup (IdHFCand id :: Id
id) = Maybe Id -> TcM (Maybe Id)
forall (m :: * -> *) a. Monad m => a -> m a
return (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
id)
          lookup hfc :: HoleFitCandidate
hfc = do { TcTyThing
thing <- Name -> TcM TcTyThing
tcLookup Name
name
                          ; Maybe Id -> TcM (Maybe Id)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Id -> TcM (Maybe Id)) -> Maybe Id -> TcM (Maybe Id)
forall a b. (a -> b) -> a -> b
$ case TcTyThing
thing of
                                       ATcId {tct_id :: TcTyThing -> Id
tct_id = Id
id} -> Id -> Maybe Id
forall a. a -> Maybe a
Just Id
id
                                       AGlobal (AnId id :: Id
id)   -> Id -> Maybe Id
forall a. a -> Maybe a
Just Id
id
                                       AGlobal (AConLike (RealDataCon con :: DataCon
con)) ->
                                           Id -> Maybe Id
forall a. a -> Maybe a
Just (DataCon -> Id
dataConWrapId DataCon
con)
                                       _ -> Maybe Id
forall a. Maybe a
Nothing }
            where name :: Name
name = case HoleFitCandidate
hfc of
                           IdHFCand id :: Id
id -> Id -> Name
idName Id
id
                           GreHFCand gre :: GlobalRdrElt
gre -> GlobalRdrElt -> Name
gre_name GlobalRdrElt
gre
                           NameHFCand name :: 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] -> TcM (Bool, [HoleFit])
keep_it eid :: Id
eid wrp :: [TcType]
wrp ms :: [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)
                                 ((\n :: Int
n -> Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 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 :: Id
-> HoleFitCandidate
-> TcType
-> Int
-> [TcType]
-> [TcType]
-> Maybe HsDocString
-> HoleFit
HoleFit { hfId :: Id
hfId = Id
eid, hfCand :: HoleFitCandidate
hfCand = HoleFitCandidate
el, hfType :: TcType
hfType = (Id -> TcType
idType Id
eid)
                            , hfRefLvl :: Int
hfRefLvl = [Id] -> 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 ty :: TcType
ty) = [TcType
ty]
            unfWrp' (WpCompose w1 :: HsWrapper
w1 w2 :: HsWrapper
w2) = HsWrapper -> [TcType]
unfWrp' HsWrapper
w1 [TcType] -> [TcType] -> [TcType]
forall a. [a] -> [a] -> [a]
++ HsWrapper -> [TcType]
unfWrp' HsWrapper
w2
            unfWrp' _ = []


    -- 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 (h_ty :: TcType
h_ty, ref_vars :: [Id]
ref_vars) ty :: 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 -> TcRn ()
traceTc "checkingFitOf {" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty
         ; (fits :: Bool
fits, wrp :: HsWrapper
wrp) <- Cts -> [Implication] -> TcType -> TcType -> TcM (Bool, HsWrapper)
tcCheckHoleFit ([Ct] -> Cts
forall a. [a] -> Bag a
listToBag [Ct]
relevantCts) [Implication]
implics TcType
h_ty TcType
ty
         ; String -> SDoc -> TcRn ()
traceTc "Did it fit?" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
fits
         ; String -> SDoc -> TcRn ()
traceTc "wrap is: " (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ HsWrapper -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsWrapper
wrp
         ; String -> SDoc -> TcRn ()
traceTc "checkingFitOf }" SDoc
empty
         ; [TcType]
z_wrp_tys <- [TcType] -> TcM [TcType]
zonkTcTypes (HsWrapper -> [TcType]
unfoldWrapper HsWrapper
wrp)
         -- 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 if [Id] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
ref_vars
                then Maybe ([TcType], [TcType]) -> TcM (Maybe ([TcType], [TcType]))
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 t :: TcType
t = case TcType -> Maybe Id
getTyVar_maybe TcType
t of
                                                Just tv :: Id
tv -> Id
tv Id -> VarSet -> Bool
`elemVarSet` VarSet
fvSet
                                                _ -> 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  <- [Id] -> TcM [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
tcGetTyVar_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 :: * -> *) a. Monad m => (a -> m Bool) -> [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 (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 (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 (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


subsDiscardMsg :: SDoc
subsDiscardMsg :: SDoc
subsDiscardMsg =
    String -> SDoc
text "(Some hole fits suppressed;" SDoc -> SDoc -> SDoc
<+>
    String -> SDoc
text "use -fmax-valid-hole-fits=N" SDoc -> SDoc -> SDoc
<+>
    String -> SDoc
text "or -fno-max-valid-hole-fits)"

refSubsDiscardMsg :: SDoc
refSubsDiscardMsg :: SDoc
refSubsDiscardMsg =
    String -> SDoc
text "(Some refinement hole fits suppressed;" SDoc -> SDoc -> SDoc
<+>
    String -> SDoc
text "use -fmax-refinement-hole-fits=N" SDoc -> SDoc -> SDoc
<+>
    String -> SDoc
text "or -fno-max-refinement-hole-fits)"


-- | Checks whether a MetaTyVar is flexible or not.
isFlexiTyVar :: TcTyVar -> TcM Bool
isFlexiTyVar :: Id -> TcRnIf TcGblEnv TcLclEnv Bool
isFlexiTyVar tv :: 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
readMetaTyVar Id
tv
isFlexiTyVar _ = Bool -> TcRnIf TcGblEnv TcLclEnv Bool
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 :: FV -> TcM a -> TcM a
withoutUnification free_vars :: FV
free_vars action :: 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 -> TcRn ()) -> [Id] -> TcRn ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Id -> TcRn ()
forall gbl lcl. Id -> TcRnIf gbl lcl ()
restore [Id]
flexis
     ; a -> TcM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
result }
  where restore :: Id -> TcRnIf gbl lcl ()
restore = (TcRef MetaDetails -> MetaDetails -> TcRnIf gbl lcl ())
-> MetaDetails -> TcRef MetaDetails -> TcRnIf gbl lcl ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip TcRef MetaDetails -> MetaDetails -> TcRnIf gbl lcl ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
writeTcRef MetaDetails
Flexi (TcRef MetaDetails -> TcRnIf gbl lcl ())
-> (Id -> TcRef MetaDetails) -> Id -> TcRnIf gbl lcl ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> TcRef MetaDetails
metaTyVarRef
        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 ty_a :: TcType
ty_a ty_b :: 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
<$> Cts -> [Implication] -> TcType -> TcType -> TcM (Bool, HsWrapper)
tcCheckHoleFit Cts
forall a. Bag a
emptyBag [] TcType
ty_a TcType
ty_b


-- | 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.
-- Note: The simplifier may perform unification, so make sure to restore any
-- free type variables to avoid side-effects.
tcCheckHoleFit :: Cts                   -- ^  Any relevant Cts to the hole.
               -> [Implication]
               -- ^ The nested implications of the hole with the innermost
               -- implication first.
               -> TcSigmaType           -- ^ The type of the hole.
               -> TcSigmaType           -- ^ The type to check whether fits.
               -> TcM (Bool, HsWrapper)
               -- ^ Whether it was a match, and the wrapper from hole_ty to ty.
tcCheckHoleFit :: Cts -> [Implication] -> TcType -> TcType -> TcM (Bool, HsWrapper)
tcCheckHoleFit _ _ hole_ty :: TcType
hole_ty ty :: TcType
ty | TcType
hole_ty TcType -> TcType -> Bool
`eqType` TcType
ty
    = (Bool, HsWrapper) -> TcM (Bool, HsWrapper)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, HsWrapper
idHsWrapper)
tcCheckHoleFit relevantCts :: Cts
relevantCts implics :: [Implication]
implics hole_ty :: TcType
hole_ty 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]
implics of
                          [] -> TcM TcLevel
getTcLevel
                          -- imp is the innermost implication
                          (imp :: Implication
imp:_) -> TcLevel -> TcM TcLevel
forall (m :: * -> *) a. Monad m => a -> m a
return (Implication -> TcLevel
ic_tclvl Implication
imp)
     ; (wrp :: HsWrapper
wrp, wanted :: 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
$
                          UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
tcSubType_NC UserTypeCtxt
ExprSigCtxt TcType
ty TcType
hole_ty
     ; String -> SDoc -> TcRn ()
traceTc "Checking hole fit {" SDoc
empty
     ; String -> SDoc -> TcRn ()
traceTc "wanteds are: " (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
wanted
     ; if WantedConstraints -> Bool
isEmptyWC WantedConstraints
wanted Bool -> Bool -> Bool
&& Cts -> Bool
forall a. Bag a -> Bool
isEmptyBag Cts
relevantCts
       then String -> SDoc -> TcRn ()
traceTc "}" SDoc
empty TcRn () -> TcM (Bool, HsWrapper) -> TcM (Bool, HsWrapper)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Bool, HsWrapper) -> TcM (Bool, HsWrapper)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, HsWrapper
wrp)
       else 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).
               ; Cts
cloned_relevants <- (Ct -> IOEnv (Env TcGblEnv TcLclEnv) Ct)
-> Cts -> IOEnv (Env TcGblEnv TcLclEnv) Cts
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM Ct -> IOEnv (Env TcGblEnv TcLclEnv) Ct
cloneWanted Cts
relevantCts
                 -- We wrap the WC in the nested implications, see
                 -- Note [Nested Implications]
               ; let outermost_first :: [Implication]
outermost_first = [Implication] -> [Implication]
forall a. [a] -> [a]
reverse [Implication]
implics
                     setWC :: Implication -> WantedConstraints -> WantedConstraints
setWC = EvBindsVar -> Implication -> WantedConstraints -> WantedConstraints
setWCAndBinds EvBindsVar
fresh_binds
                    -- We add the cloned relevants to the wanteds generated by
                    -- the call to tcSubType_NC, see Note [Relevant Constraints]
                    -- There's no need to clone the wanteds, because they are
                    -- freshly generated by `tcSubtype_NC`.
                     w_rel_cts :: WantedConstraints
w_rel_cts = WantedConstraints -> Cts -> WantedConstraints
addSimples WantedConstraints
wanted Cts
cloned_relevants
                     w_givens :: WantedConstraints
w_givens = (Implication -> WantedConstraints -> WantedConstraints)
-> WantedConstraints -> [Implication] -> WantedConstraints
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Implication -> WantedConstraints -> WantedConstraints
setWC WantedConstraints
w_rel_cts [Implication]
outermost_first
               ; String -> SDoc -> TcRn ()
traceTc "w_givens are: " (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
w_givens
               ; WantedConstraints
rem <- TcS WantedConstraints -> TcM WantedConstraints
forall a. TcS a -> TcM a
runTcSDeriveds (TcS WantedConstraints -> TcM WantedConstraints)
-> TcS WantedConstraints -> TcM WantedConstraints
forall a b. (a -> b) -> a -> b
$ WantedConstraints -> TcS WantedConstraints
simpl_top WantedConstraints
w_givens
               -- We don't want any insoluble or simple constraints left, but
               -- solved implications are ok (and neccessary for e.g. undefined)
               ; String -> SDoc -> TcRn ()
traceTc "rems was:" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ WantedConstraints -> SDoc
forall a. Outputable a => a -> SDoc
ppr WantedConstraints
rem
               ; String -> SDoc -> TcRn ()
traceTc "}" SDoc
empty
               ; (Bool, HsWrapper) -> TcM (Bool, HsWrapper)
forall (m :: * -> *) a. Monad m => a -> m a
return (WantedConstraints -> Bool
isSolvedWC WantedConstraints
rem, HsWrapper
wrp) } }
     where
       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 binds :: EvBindsVar
binds imp :: Implication
imp wc :: WantedConstraints
wc
         = WC :: Cts -> Bag Implication -> WantedConstraints
WC { wc_simple :: Cts
wc_simple = Cts
forall a. Bag a
emptyBag
              , wc_impl :: Bag Implication
wc_impl = 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 :: WantedConstraints
ic_wanted = WantedConstraints
wc , ic_binds :: EvBindsVar
ic_binds = EvBindsVar
binds } }