{-# LANGUAGE CPP #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
module GHC.Tc.Errors.Hole
( findValidHoleFits
, tcCheckHoleFit
, withoutUnification
, tcSubsumes
, isFlexiTyVar
, tcFilterHoleFits
, getLocalBindings
, pprHoleFit
, addHoleFitDocs
, getHoleFitSortingAlg
, getHoleFitDispConfig
, HoleFitDispConfig (..)
, HoleFitSortingAlg (..)
, relevantCts
, zonkSubs
, sortHoleFitsByGraph
, sortHoleFitsBySize
, HoleFitPlugin (..), HoleFitPluginR (..)
)
where
import GHC.Prelude
import GHC.Tc.Types
import GHC.Tc.Utils.Monad
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcMType
import GHC.Tc.Types.Evidence
import GHC.Tc.Utils.TcType
import GHC.Core.Type
import GHC.Core.DataCon
import GHC.Types.Name
import GHC.Types.Name.Reader ( pprNameProvenance , GlobalRdrElt (..)
, globalRdrEnvElts, greMangledName, grePrintableName )
import GHC.Builtin.Names ( gHC_ERR )
import GHC.Types.Id
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Types.TyThing
import GHC.Data.Bag
import GHC.Core.ConLike ( ConLike(..) )
import GHC.Utils.Misc
import GHC.Utils.Panic
import GHC.Tc.Utils.Env (tcLookup)
import GHC.Utils.Outputable
import GHC.Driver.Session
import GHC.Data.Maybe
import GHC.Utils.FV ( fvVarList, fvVarSet, unionFV, mkFVs, FV )
import Control.Arrow ( (&&&) )
import Control.Monad ( filterM, replicateM, foldM )
import Data.List ( partition, sort, sortOn, nubBy )
import Data.Graph ( graphFromEdges, topSort )
import GHC.Tc.Solver ( simplifyTopWanteds, runTcSDeriveds )
import GHC.Tc.Utils.Unify ( tcSubTypeSigma )
import GHC.HsToCore.Docs ( extractDocs )
import qualified Data.Map as Map
import GHC.Hs.Doc ( unpackHDS, DeclDocMap(..) )
import GHC.Unit.Module.ModIface ( ModIface_(..) )
import GHC.Iface.Load ( loadInterfaceForNameMaybe )
import GHC.Builtin.Utils (knownKeyNames)
import GHC.Tc.Errors.Hole.FitTypes
data HoleFitDispConfig = HFDC { HoleFitDispConfig -> Bool
showWrap :: Bool
, HoleFitDispConfig -> Bool
showWrapVars :: Bool
, HoleFitDispConfig -> Bool
showType :: Bool
, HoleFitDispConfig -> Bool
showProv :: Bool
, HoleFitDispConfig -> Bool
showMatches :: Bool }
getHoleFitDispConfig :: TcM HoleFitDispConfig
getHoleFitDispConfig :: TcM HoleFitDispConfig
getHoleFitDispConfig
= do { Bool
sWrap <- forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_ShowTypeAppOfHoleFits
; Bool
sWrapVars <- forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_ShowTypeAppVarsOfHoleFits
; Bool
sType <- forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_ShowTypeOfHoleFits
; Bool
sProv <- forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_ShowProvOfHoleFits
; Bool
sMatc <- forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_ShowMatchesOfHoleFits
; forall (m :: * -> *) a. Monad m => a -> m a
return HFDC{ showWrap :: Bool
showWrap = Bool
sWrap, showWrapVars :: Bool
showWrapVars = Bool
sWrapVars
, showProv :: Bool
showProv = Bool
sProv, showType :: Bool
showType = Bool
sType
, showMatches :: Bool
showMatches = Bool
sMatc } }
data HoleFitSortingAlg = HFSNoSorting
| HFSBySize
| HFSBySubsumption
deriving (HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
$c/= :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
== :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
$c== :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
Eq, Eq HoleFitSortingAlg
HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
HoleFitSortingAlg -> HoleFitSortingAlg -> Ordering
HoleFitSortingAlg -> HoleFitSortingAlg -> HoleFitSortingAlg
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: HoleFitSortingAlg -> HoleFitSortingAlg -> HoleFitSortingAlg
$cmin :: HoleFitSortingAlg -> HoleFitSortingAlg -> HoleFitSortingAlg
max :: HoleFitSortingAlg -> HoleFitSortingAlg -> HoleFitSortingAlg
$cmax :: HoleFitSortingAlg -> HoleFitSortingAlg -> HoleFitSortingAlg
>= :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
$c>= :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
> :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
$c> :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
<= :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
$c<= :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
< :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
$c< :: HoleFitSortingAlg -> HoleFitSortingAlg -> Bool
compare :: HoleFitSortingAlg -> HoleFitSortingAlg -> Ordering
$ccompare :: HoleFitSortingAlg -> HoleFitSortingAlg -> Ordering
Ord)
getHoleFitSortingAlg :: TcM HoleFitSortingAlg
getHoleFitSortingAlg :: TcM HoleFitSortingAlg
getHoleFitSortingAlg =
do { Bool
shouldSort <- forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_SortValidHoleFits
; Bool
subsumSort <- forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_SortBySubsumHoleFits
; Bool
sizeSort <- forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_SortBySizeHoleFits
; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Bool -> Bool
not Bool
shouldSort
then HoleFitSortingAlg
HFSNoSorting
else if Bool
subsumSort
then HoleFitSortingAlg
HFSBySubsumption
else if Bool
sizeSort
then HoleFitSortingAlg
HFSBySize
else HoleFitSortingAlg
HFSNoSorting }
addHoleFitDocs :: [HoleFit] -> TcM [HoleFit]
addHoleFitDocs :: [HoleFit] -> TcM [HoleFit]
addHoleFitDocs [HoleFit]
fits =
do { Bool
showDocs <- forall gbl lcl. GeneralFlag -> TcRnIf gbl lcl Bool
goptM GeneralFlag
Opt_ShowDocsOfHoleFits
; if Bool
showDocs
then do { (Maybe HsDocString
_, DeclDocMap Map Name HsDocString
lclDocs, ArgDocMap
_) <- forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *).
MonadIO m =>
TcGblEnv -> m (Maybe HsDocString, DeclDocMap, ArgDocMap)
extractDocs
; 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 forall (m :: * -> *) a. Monad m => a -> m a
return [HoleFit]
fits }
where
msg :: SDoc
msg = String -> SDoc
text String
"GHC.Tc.Errors.Hole addHoleFitDocs"
lookupInIface :: Name -> ModIface_ phase -> Maybe HsDocString
lookupInIface Name
name (ModIface { mi_decl_docs :: forall (phase :: ModIfacePhase). ModIface_ phase -> DeclDocMap
mi_decl_docs = DeclDocMap Map Name HsDocString
dmap })
= 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 Map Name HsDocString
lclDocs fit :: HoleFit
fit@(HoleFit {hfCand :: HoleFit -> HoleFitCandidate
hfCand = HoleFitCandidate
cand}) =
do { let name :: Name
name = forall a. NamedThing a => a -> Name
getName HoleFitCandidate
cand
; Maybe HsDocString
doc <- if HoleFit -> Bool
hfIsLcl HoleFit
fit
then forall (f :: * -> *) a. Applicative f => a -> f a
pure (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
; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Maybe ModIface
mbIface forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {phase :: ModIfacePhase}.
Name -> ModIface_ phase -> Maybe HsDocString
lookupInIface Name
name }
; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ HoleFit
fit {hfDoc :: Maybe HsDocString
hfDoc = Maybe HsDocString
doc} }
upd Map Name HsDocString
_ HoleFit
fit = forall (m :: * -> *) a. Monad m => a -> m a
return HoleFit
fit
pprHoleFit :: HoleFitDispConfig -> HoleFit -> SDoc
pprHoleFit :: HoleFitDispConfig -> HoleFit -> SDoc
pprHoleFit HoleFitDispConfig
_ (RawHoleFit SDoc
sd) = SDoc
sd
pprHoleFit (HFDC Bool
sWrp Bool
sWrpVars Bool
sTy Bool
sProv Bool
sMs) (HoleFit {Int
[TcType]
Maybe HsDocString
Id
TcType
HoleFitCandidate
hfWrap :: HoleFit -> [TcType]
hfType :: HoleFit -> TcType
hfRefLvl :: HoleFit -> Int
hfMatches :: HoleFit -> [TcType]
hfId :: HoleFit -> Id
hfDoc :: Maybe HsDocString
hfMatches :: [TcType]
hfWrap :: [TcType]
hfRefLvl :: Int
hfType :: TcType
hfCand :: HoleFitCandidate
hfId :: Id
hfDoc :: HoleFit -> Maybe HsDocString
hfCand :: HoleFit -> HoleFitCandidate
..}) =
SDoc -> Int -> SDoc -> SDoc
hang SDoc
display Int
2 SDoc
provenance
where tyApp :: SDoc
tyApp = [SDoc] -> SDoc
sep forall a b. (a -> b) -> a -> b
$ forall a b c. String -> (a -> b -> c) -> [a] -> [b] -> [c]
zipWithEqual String
"pprHoleFit" forall {tv}. Outputable tv => VarBndr tv ArgFlag -> TcType -> SDoc
pprArg [TyCoVarBinder]
vars [TcType]
hfWrap
where pprArg :: VarBndr tv ArgFlag -> TcType -> SDoc
pprArg VarBndr tv ArgFlag
b TcType
arg = case forall tv argf. VarBndr tv argf -> argf
binderArgFlag VarBndr tv ArgFlag
b of
(Invisible Specificity
spec) -> case Specificity
spec of
Specificity
SpecifiedSpec -> String -> SDoc
text String
"@" SDoc -> SDoc -> SDoc
<> TcType -> SDoc
pprParendType TcType
arg
Specificity
InferredSpec -> SDoc
empty
ArgFlag
Required -> forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"pprHoleFit: bad Required"
(forall a. Outputable a => a -> SDoc
ppr VarBndr tv ArgFlag
b SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr TcType
arg)
tyAppVars :: SDoc
tyAppVars = [SDoc] -> SDoc
sep forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
comma forall a b. (a -> b) -> a -> b
$
forall a b c. String -> (a -> b -> c) -> [a] -> [b] -> [c]
zipWithEqual String
"pprHoleFit" (\TyCoVarBinder
v TcType
t -> forall a. Outputable a => a -> SDoc
ppr (forall tv argf. VarBndr tv argf -> tv
binderVar TyCoVarBinder
v) SDoc -> SDoc -> SDoc
<+>
String -> SDoc
text String
"~" SDoc -> SDoc -> SDoc
<+> TcType -> SDoc
pprParendType TcType
t)
[TyCoVarBinder]
vars [TcType]
hfWrap
vars :: [TyCoVarBinder]
vars = TcType -> [TyCoVarBinder]
unwrapTypeVars TcType
hfType
where
unwrapTypeVars :: Type -> [TyCoVarBinder]
unwrapTypeVars :: TcType -> [TyCoVarBinder]
unwrapTypeVars TcType
t = [TyCoVarBinder]
vars forall a. [a] -> [a] -> [a]
++ case TcType -> Maybe (TcType, TcType, TcType)
splitFunTy_maybe TcType
unforalled of
Just (TcType
_, TcType
_, TcType
unfunned) -> TcType -> [TyCoVarBinder]
unwrapTypeVars TcType
unfunned
Maybe (TcType, TcType, TcType)
_ -> []
where ([TyCoVarBinder]
vars, TcType
unforalled) = TcType -> ([TyCoVarBinder], TcType)
splitForAllTyCoVarBinders TcType
t
holeVs :: SDoc
holeVs = [SDoc] -> SDoc
sep forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (SDoc -> SDoc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> SDoc
text String
"_" SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> SDoc
ppr) [TcType]
hfMatches
holeDisp :: SDoc
holeDisp = if Bool
sMs then SDoc
holeVs
else [SDoc] -> SDoc
sep forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Int
length [TcType]
hfMatches) forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"_"
occDisp :: SDoc
occDisp = case HoleFitCandidate
hfCand of
GreHFCand GlobalRdrElt
gre -> forall a. OutputableBndr a => a -> SDoc
pprPrefixOcc (GlobalRdrElt -> Name
grePrintableName GlobalRdrElt
gre)
NameHFCand Name
name -> forall a. OutputableBndr a => a -> SDoc
pprPrefixOcc Name
name
IdHFCand Id
id_ -> forall a. OutputableBndr a => a -> SDoc
pprPrefixOcc Id
id_
tyDisp :: SDoc
tyDisp = Bool -> SDoc -> SDoc
ppWhen Bool
sTy forall a b. (a -> b) -> a -> b
$ SDoc
dcolon SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr TcType
hfType
has :: [a] -> Bool
has = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null
wrapDisp :: SDoc
wrapDisp = Bool -> SDoc -> SDoc
ppWhen (forall {a}. [a] -> Bool
has [TcType]
hfWrap Bool -> Bool -> Bool
&& (Bool
sWrp Bool -> Bool -> Bool
|| Bool
sWrpVars))
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"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 Maybe HsDocString
hfDoc of
Just HsDocString
d -> String -> SDoc
text String
"{-^" SDoc -> SDoc -> SDoc
<>
([SDoc] -> SDoc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map String -> SDoc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsDocString -> String
unpackHDS) HsDocString
d
SDoc -> SDoc -> SDoc
<> String -> SDoc
text String
"-}"
Maybe HsDocString
_ -> SDoc
empty
funcInfo :: SDoc
funcInfo = Bool -> SDoc -> SDoc
ppWhen (forall {a}. [a] -> Bool
has [TcType]
hfMatches Bool -> Bool -> Bool
&& Bool
sTy) forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"where" SDoc -> SDoc -> SDoc
<+> SDoc
occDisp SDoc -> SDoc -> SDoc
<+> SDoc
tyDisp
subDisp :: SDoc
subDisp = SDoc
occDisp SDoc -> SDoc -> SDoc
<+> if forall {a}. [a] -> Bool
has [TcType]
hfMatches then SDoc
holeDisp else SDoc
tyDisp
display :: SDoc
display = SDoc
subDisp SDoc -> SDoc -> SDoc
$$ Int -> SDoc -> SDoc
nest Int
2 (SDoc
funcInfo SDoc -> SDoc -> SDoc
$+$ SDoc
docs SDoc -> SDoc -> SDoc
$+$ SDoc
wrapDisp)
provenance :: SDoc
provenance = Bool -> SDoc -> SDoc
ppWhen Bool
sProv forall a b. (a -> b) -> a -> b
$ SDoc -> SDoc
parens forall a b. (a -> b) -> a -> b
$
case HoleFitCandidate
hfCand of
GreHFCand GlobalRdrElt
gre -> GlobalRdrElt -> SDoc
pprNameProvenance GlobalRdrElt
gre
NameHFCand Name
name -> String -> SDoc
text String
"bound at" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (forall a. NamedThing a => a -> SrcLoc
getSrcLoc Name
name)
IdHFCand Id
id_ -> String -> SDoc
text String
"bound at" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (forall a. NamedThing a => a -> SrcLoc
getSrcLoc Id
id_)
getLocalBindings :: TidyEnv -> CtLoc -> TcM [Id]
getLocalBindings :: TidyEnv -> CtLoc -> TcM [Id]
getLocalBindings TidyEnv
tidy_orig CtLoc
ct_loc
= do { (TidyEnv
env1, CtOrigin
_) <- TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
zonkTidyOrigin TidyEnv
tidy_orig (CtLoc -> CtOrigin
ctLocOrigin CtLoc
ct_loc)
; TidyEnv -> [Id] -> [TcBinder] -> TcM [Id]
go TidyEnv
env1 [] (forall a. HasOccName a => [a] -> [a]
removeBindingShadowing forall a b. (a -> b) -> a -> b
$ TcLclEnv -> [TcBinder]
tcl_bndrs TcLclEnv
lcl_env) }
where
lcl_env :: TcLclEnv
lcl_env = CtLoc -> TcLclEnv
ctLocEnv CtLoc
ct_loc
go :: TidyEnv -> [Id] -> [TcBinder] -> TcM [Id]
go :: TidyEnv -> [Id] -> [TcBinder] -> TcM [Id]
go TidyEnv
_ [Id]
sofar [] = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [a] -> [a]
reverse [Id]
sofar)
go TidyEnv
env [Id]
sofar (TcBinder
tc_bndr : [TcBinder]
tc_bndrs) =
case TcBinder
tc_bndr of
TcIdBndr Id
id TopLevelFlag
_ -> Id -> TcM [Id]
keep_it Id
id
TcBinder
_ -> TcM [Id]
discard_it
where
discard_it :: TcM [Id]
discard_it = TidyEnv -> [Id] -> [TcBinder] -> TcM [Id]
go TidyEnv
env [Id]
sofar [TcBinder]
tc_bndrs
keep_it :: Id -> TcM [Id]
keep_it Id
id = TidyEnv -> [Id] -> [TcBinder] -> TcM [Id]
go TidyEnv
env (Id
idforall a. a -> [a] -> [a]
:[Id]
sofar) [TcBinder]
tc_bndrs
findValidHoleFits :: TidyEnv
-> [Implication]
-> [Ct]
-> Hole
-> TcM (TidyEnv, SDoc)
findValidHoleFits :: TidyEnv -> [Implication] -> [Ct] -> Hole -> TcM (TidyEnv, SDoc)
findValidHoleFits TidyEnv
tidy_env [Implication]
implics [Ct]
simples h :: Hole
h@(Hole { hole_sort :: Hole -> HoleSort
hole_sort = ExprHole HoleExprRef
_
, hole_loc :: Hole -> CtLoc
hole_loc = CtLoc
ct_loc
, hole_ty :: Hole -> TcType
hole_ty = TcType
hole_ty }) =
do { GlobalRdrEnv
rdr_env <- TcRn GlobalRdrEnv
getGlobalRdrEnv
; [Id]
lclBinds <- TidyEnv -> CtLoc -> TcM [Id]
getLocalBindings TidyEnv
tidy_env CtLoc
ct_loc
; Maybe Int
maxVSubs <- DynFlags -> Maybe Int
maxValidHoleFits forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; HoleFitDispConfig
hfdc <- TcM HoleFitDispConfig
getHoleFitDispConfig
; HoleFitSortingAlg
sortingAlg <- TcM HoleFitSortingAlg
getHoleFitSortingAlg
; DynFlags
dflags <- forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; [HoleFitPlugin]
hfPlugs <- TcGblEnv -> [HoleFitPlugin]
tcg_hf_plugins forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv
; let findVLimit :: Maybe Int
findVLimit = if HoleFitSortingAlg
sortingAlg forall a. Ord a => a -> a -> Bool
> HoleFitSortingAlg
HFSNoSorting then forall a. Maybe a
Nothing else Maybe Int
maxVSubs
refLevel :: Maybe Int
refLevel = DynFlags -> Maybe Int
refLevelHoleFits DynFlags
dflags
hole :: TypedHole
hole = TypedHole { th_relevant_cts :: Cts
th_relevant_cts =
forall a. [a] -> Bag a
listToBag (TcType -> [Ct] -> [Ct]
relevantCts TcType
hole_ty [Ct]
simples)
, th_implics :: [Implication]
th_implics = [Implication]
implics
, th_hole :: Maybe Hole
th_hole = forall a. a -> Maybe a
Just Hole
h }
([[HoleFitCandidate] -> TcM [HoleFitCandidate]]
candidatePlugins, [[HoleFit] -> TcM [HoleFit]]
fitPlugins) =
forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\HoleFitPlugin
p-> ((HoleFitPlugin -> CandPlugin
candPlugin HoleFitPlugin
p) TypedHole
hole, (HoleFitPlugin -> FitPlugin
fitPlugin HoleFitPlugin
p) TypedHole
hole)) [HoleFitPlugin]
hfPlugs
; String -> SDoc -> TcRn ()
traceTc String
"findingValidHoleFitsFor { " forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr TypedHole
hole
; String -> SDoc -> TcRn ()
traceTc String
"hole_lvl is:" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr TcLevel
hole_lvl
; String -> SDoc -> TcRn ()
traceTc String
"simples are: " forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr [Ct]
simples
; String -> SDoc -> TcRn ()
traceTc String
"locals are: " forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr [Id]
lclBinds
; let ([GlobalRdrElt]
lcl, [GlobalRdrElt]
gbl) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition GlobalRdrElt -> Bool
gre_lcl (GlobalRdrEnv -> [GlobalRdrElt]
globalRdrEnvElts GlobalRdrEnv
rdr_env)
locals :: [HoleFitCandidate]
locals = forall a. HasOccName a => [a] -> [a]
removeBindingShadowing forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b) -> [a] -> [b]
map Id -> HoleFitCandidate
IdHFCand [Id]
lclBinds forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map GlobalRdrElt -> HoleFitCandidate
GreHFCand [GlobalRdrElt]
lcl
globals :: [HoleFitCandidate]
globals = forall a b. (a -> b) -> [a] -> [b]
map GlobalRdrElt -> HoleFitCandidate
GreHFCand [GlobalRdrElt]
gbl
syntax :: [HoleFitCandidate]
syntax = forall a b. (a -> b) -> [a] -> [b]
map Name -> HoleFitCandidate
NameHFCand [Name]
builtIns
to_check :: [HoleFitCandidate]
to_check = [HoleFitCandidate]
locals forall a. [a] -> [a] -> [a]
++ [HoleFitCandidate]
syntax forall a. [a] -> [a] -> [a]
++ [HoleFitCandidate]
globals
; [HoleFitCandidate]
cands <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
($)) [HoleFitCandidate]
to_check [[HoleFitCandidate] -> TcM [HoleFitCandidate]]
candidatePlugins
; String -> SDoc -> TcRn ()
traceTc String
"numPlugins are:" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr (forall (t :: * -> *) a. Foldable t => t a -> Int
length [[HoleFitCandidate] -> TcM [HoleFitCandidate]]
candidatePlugins)
; (Bool
searchDiscards, [HoleFit]
subs) <-
Maybe Int
-> TypedHole
-> (TcType, [Id])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
tcFilterHoleFits Maybe Int
findVLimit TypedHole
hole (TcType
hole_ty, []) [HoleFitCandidate]
cands
; (TidyEnv
tidy_env, [HoleFit]
tidy_subs) <- TidyEnv -> [HoleFit] -> TcM (TidyEnv, [HoleFit])
zonkSubs TidyEnv
tidy_env [HoleFit]
subs
; [HoleFit]
tidy_sorted_subs <- HoleFitSortingAlg -> [HoleFit] -> TcM [HoleFit]
sortFits HoleFitSortingAlg
sortingAlg [HoleFit]
tidy_subs
; [HoleFit]
plugin_handled_subs <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
($)) [HoleFit]
tidy_sorted_subs [[HoleFit] -> TcM [HoleFit]]
fitPlugins
; let (Bool
pVDisc, [HoleFit]
limited_subs) = Maybe Int -> [HoleFit] -> (Bool, [HoleFit])
possiblyDiscard Maybe Int
maxVSubs [HoleFit]
plugin_handled_subs
vDiscards :: Bool
vDiscards = Bool
pVDisc Bool -> Bool -> Bool
|| Bool
searchDiscards
; [HoleFit]
subs_with_docs <- [HoleFit] -> TcM [HoleFit]
addHoleFitDocs [HoleFit]
limited_subs
; let vMsg :: SDoc
vMsg = Bool -> SDoc -> SDoc
ppUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [HoleFit]
subs_with_docs) forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Valid hole fits include") Int
2 forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat (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
; (TidyEnv
tidy_env, SDoc
refMsg) <- if Maybe Int
refLevel forall a. Ord a => a -> a -> Bool
>= forall a. a -> Maybe a
Just Int
0 then
do { Maybe Int
maxRSubs <- DynFlags -> Maybe Int
maxRefHoleFits forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; let refLvls :: [Int]
refLvls = [Int
1..(forall a. HasCallStack => Maybe a -> a
fromJust Maybe Int
refLevel)]
; [(TcType, [Id])]
ref_tys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Int -> TcM (TcType, [Id])
mkRefTy [Int]
refLvls
; String -> SDoc -> TcRn ()
traceTc String
"ref_tys are" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr [(TcType, [Id])]
ref_tys
; let findRLimit :: Maybe Int
findRLimit = if HoleFitSortingAlg
sortingAlg forall a. Ord a => a -> a -> Bool
> HoleFitSortingAlg
HFSNoSorting then forall a. Maybe a
Nothing
else Maybe Int
maxRSubs
; [(Bool, [HoleFit])]
refDs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b c. (a -> b -> c) -> b -> a -> c
flip (Maybe Int
-> TypedHole
-> (TcType, [Id])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
tcFilterHoleFits Maybe Int
findRLimit TypedHole
hole)
[HoleFitCandidate]
cands) [(TcType, [Id])]
ref_tys
; (TidyEnv
tidy_env, [HoleFit]
tidy_rsubs) <- TidyEnv -> [HoleFit] -> TcM (TidyEnv, [HoleFit])
zonkSubs TidyEnv
tidy_env forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a b. (a, b) -> b
snd [(Bool, [HoleFit])]
refDs
; [HoleFit]
tidy_sorted_rsubs <- HoleFitSortingAlg -> [HoleFit] -> TcM [HoleFit]
sortFits HoleFitSortingAlg
sortingAlg [HoleFit]
tidy_rsubs
; (TidyEnv
tidy_env, TcType
tidy_hole_ty) <- TidyEnv -> TcType -> TcM (TidyEnv, TcType)
zonkTidyTcType TidyEnv
tidy_env TcType
hole_ty
; let hasExactApp :: HoleFit -> Bool
hasExactApp = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (HasDebugCallStack => TcType -> TcType -> Bool
tcEqType TcType
tidy_hole_ty) forall b c a. (b -> c) -> (a -> b) -> a -> c
. HoleFit -> [TcType]
hfWrap
([HoleFit]
exact, [HoleFit]
not_exact) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition HoleFit -> Bool
hasExactApp [HoleFit]
tidy_sorted_rsubs
; [HoleFit]
plugin_handled_rsubs <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
($))
([HoleFit]
not_exact forall a. [a] -> [a] -> [a]
++ [HoleFit]
exact) [[HoleFit] -> TcM [HoleFit]]
fitPlugins
; let (Bool
pRDisc, [HoleFit]
exact_last_rfits) =
Maybe Int -> [HoleFit] -> (Bool, [HoleFit])
possiblyDiscard Maybe Int
maxRSubs forall a b. (a -> b) -> a -> b
$ [HoleFit]
plugin_handled_rsubs
rDiscards :: Bool
rDiscards = Bool
pRDisc Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a b. (a, b) -> a
fst [(Bool, [HoleFit])]
refDs
; [HoleFit]
rsubs_with_docs <- [HoleFit] -> TcM [HoleFit]
addHoleFitDocs [HoleFit]
exact_last_rfits
; forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env,
Bool -> SDoc -> SDoc
ppUnless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [HoleFit]
rsubs_with_docs) forall a b. (a -> b) -> a -> b
$
SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Valid refinement hole fits include") Int
2 forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat (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 forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env, SDoc
empty)
; String -> SDoc -> TcRn ()
traceTc String
"findingValidHoleFitsFor }" SDoc
empty
; forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env, SDoc
vMsg SDoc -> SDoc -> SDoc
$$ SDoc
refMsg) }
where
hole_lvl :: TcLevel
hole_lvl = CtLoc -> TcLevel
ctLocLevel CtLoc
ct_loc
builtIns :: [Name]
builtIns :: [Name]
builtIns = forall a. (a -> Bool) -> [a] -> [a]
filter Name -> Bool
isBuiltInSyntax [Name]
knownKeyNames
mkRefTy :: Int -> TcM (TcType, [TcTyVar])
mkRefTy :: Int -> TcM (TcType, [Id])
mkRefTy Int
refLvl = ([Id] -> TcType
wrapWithVars forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& forall a. a -> a
id) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcM [Id]
newTyVars
where newTyVars :: TcM [Id]
newTyVars = forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
refLvl forall a b. (a -> b) -> a -> b
$ Id -> Id
setLvl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(TcM TcType
newOpenTypeKind forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= TcType -> IOEnv (Env TcGblEnv TcLclEnv) Id
newFlexiTyVar)
setLvl :: Id -> Id
setLvl = forall a b c. (a -> b -> c) -> b -> a -> c
flip Id -> TcLevel -> Id
setMetaTyVarTcLevel TcLevel
hole_lvl
wrapWithVars :: [Id] -> TcType
wrapWithVars [Id]
vars = [TcType] -> TcType -> TcType
mkVisFunTysMany (forall a b. (a -> b) -> [a] -> [b]
map Id -> TcType
mkTyVarTy [Id]
vars) TcType
hole_ty
sortFits :: HoleFitSortingAlg
-> [HoleFit]
-> TcM [HoleFit]
sortFits :: HoleFitSortingAlg -> [HoleFit] -> TcM [HoleFit]
sortFits HoleFitSortingAlg
HFSNoSorting [HoleFit]
subs = forall (m :: * -> *) a. Monad m => a -> m a
return [HoleFit]
subs
sortFits HoleFitSortingAlg
HFSBySize [HoleFit]
subs
= forall a. [a] -> [a] -> [a]
(++) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [HoleFit] -> TcM [HoleFit]
sortHoleFitsBySize (forall a. Ord a => [a] -> [a]
sort [HoleFit]
lclFits)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [HoleFit] -> TcM [HoleFit]
sortHoleFitsBySize (forall a. Ord a => [a] -> [a]
sort [HoleFit]
gblFits)
where ([HoleFit]
lclFits, [HoleFit]
gblFits) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span HoleFit -> Bool
hfIsLcl [HoleFit]
subs
sortFits HoleFitSortingAlg
HFSBySubsumption [HoleFit]
subs
= forall a. [a] -> [a] -> [a]
(++) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [HoleFit] -> TcM [HoleFit]
sortHoleFitsByGraph (forall a. Ord a => [a] -> [a]
sort [HoleFit]
lclFits)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [HoleFit] -> TcM [HoleFit]
sortHoleFitsByGraph (forall a. Ord a => [a] -> [a]
sort [HoleFit]
gblFits)
where ([HoleFit]
lclFits, [HoleFit]
gblFits) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span HoleFit -> Bool
hfIsLcl [HoleFit]
subs
subsDiscardMsg :: SDoc
subsDiscardMsg :: SDoc
subsDiscardMsg =
String -> SDoc
text String
"(Some hole fits suppressed;" SDoc -> SDoc -> SDoc
<+>
String -> SDoc
text String
"use -fmax-valid-hole-fits=N" SDoc -> SDoc -> SDoc
<+>
String -> SDoc
text String
"or -fno-max-valid-hole-fits)"
refSubsDiscardMsg :: SDoc
refSubsDiscardMsg :: SDoc
refSubsDiscardMsg =
String -> SDoc
text String
"(Some refinement hole fits suppressed;" SDoc -> SDoc -> SDoc
<+>
String -> SDoc
text String
"use -fmax-refinement-hole-fits=N" SDoc -> SDoc -> SDoc
<+>
String -> SDoc
text String
"or -fno-max-refinement-hole-fits)"
possiblyDiscard :: Maybe Int -> [HoleFit] -> (Bool, [HoleFit])
possiblyDiscard :: Maybe Int -> [HoleFit] -> (Bool, [HoleFit])
possiblyDiscard (Just Int
max) [HoleFit]
fits = ([HoleFit]
fits forall a. [a] -> Int -> Bool
`lengthExceeds` Int
max, forall a. Int -> [a] -> [a]
take Int
max [HoleFit]
fits)
possiblyDiscard Maybe Int
Nothing [HoleFit]
fits = (Bool
False, [HoleFit]
fits)
findValidHoleFits TidyEnv
env [Implication]
_ [Ct]
_ Hole
_ = forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, SDoc
empty)
relevantCts :: Type -> [Ct] -> [Ct]
relevantCts :: TcType -> [Ct] -> [Ct]
relevantCts TcType
hole_ty [Ct]
simples = if VarSet -> Bool
isEmptyVarSet (FV -> VarSet
fvVarSet FV
hole_fvs) then []
else forall a. (a -> Bool) -> [a] -> [a]
filter Ct -> Bool
isRelevant [Ct]
simples
where ctFreeVarSet :: Ct -> VarSet
ctFreeVarSet :: Ct -> VarSet
ctFreeVarSet = FV -> VarSet
fvVarSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcType -> FV
tyCoFVsOfType forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> TcType
ctPred
hole_fvs :: FV
hole_fvs = TcType -> FV
tyCoFVsOfType TcType
hole_ty
hole_fv_set :: VarSet
hole_fv_set = FV -> VarSet
fvVarSet FV
hole_fvs
anyFVMentioned :: Ct -> Bool
anyFVMentioned :: Ct -> Bool
anyFVMentioned Ct
ct = Ct -> VarSet
ctFreeVarSet Ct
ct VarSet -> VarSet -> Bool
`intersectsVarSet` VarSet
hole_fv_set
isRelevant :: Ct -> Bool
isRelevant Ct
ct = Bool -> Bool
not (VarSet -> Bool
isEmptyVarSet (Ct -> VarSet
ctFreeVarSet Ct
ct))
Bool -> Bool -> Bool
&& Ct -> Bool
anyFVMentioned Ct
ct
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' [HoleFit]
zs TidyEnv
env [] = forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, forall a. [a] -> [a]
reverse [HoleFit]
zs)
zonkSubs' [HoleFit]
zs TidyEnv
env (HoleFit
hf:[HoleFit]
hfs) = do { (TidyEnv
env', HoleFit
z) <- TidyEnv -> HoleFit -> TcM (TidyEnv, HoleFit)
zonkSub TidyEnv
env HoleFit
hf
; [HoleFit] -> TidyEnv -> [HoleFit] -> TcM (TidyEnv, [HoleFit])
zonkSubs' (HoleFit
zforall a. a -> [a] -> [a]
:[HoleFit]
zs) TidyEnv
env' [HoleFit]
hfs }
zonkSub :: TidyEnv -> HoleFit -> TcM (TidyEnv, HoleFit)
zonkSub :: TidyEnv -> HoleFit -> TcM (TidyEnv, HoleFit)
zonkSub TidyEnv
env hf :: HoleFit
hf@RawHoleFit{} = forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, HoleFit
hf)
zonkSub TidyEnv
env hf :: HoleFit
hf@HoleFit{hfType :: HoleFit -> TcType
hfType = TcType
ty, hfMatches :: HoleFit -> [TcType]
hfMatches = [TcType]
m, hfWrap :: HoleFit -> [TcType]
hfWrap = [TcType]
wrp}
= do { (TidyEnv
env, TcType
ty') <- TidyEnv -> TcType -> TcM (TidyEnv, TcType)
zonkTidyTcType TidyEnv
env TcType
ty
; (TidyEnv
env, [TcType]
m') <- TidyEnv -> [TcType] -> TcM (TidyEnv, [TcType])
zonkTidyTcTypes TidyEnv
env [TcType]
m
; (TidyEnv
env, [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'}
; forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env, HoleFit
zFit ) }
sortHoleFitsBySize :: [HoleFit] -> TcM [HoleFit]
sortHoleFitsBySize :: [HoleFit] -> TcM [HoleFit]
sortHoleFitsBySize = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn HoleFit -> TypeSize
sizeOfFit
where sizeOfFit :: HoleFit -> TypeSize
sizeOfFit :: HoleFit -> TypeSize
sizeOfFit = [TcType] -> TypeSize
sizeTypes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy HasDebugCallStack => TcType -> TcType -> Bool
tcEqType forall b c a. (b -> c) -> (a -> b) -> a -> c
. HoleFit -> [TcType]
hfWrap
sortHoleFitsByGraph :: [HoleFit] -> TcM [HoleFit]
sortHoleFitsByGraph :: [HoleFit] -> TcM [HoleFit]
sortHoleFitsByGraph [HoleFit]
fits = [(HoleFit, [HoleFit])] -> [HoleFit] -> TcM [HoleFit]
go [] [HoleFit]
fits
where tcSubsumesWCloning :: TcType -> TcType -> TcM Bool
tcSubsumesWCloning :: TcType -> TcType -> TcM Bool
tcSubsumesWCloning TcType
ht TcType
ty = forall a. FV -> TcM a -> TcM a
withoutUnification FV
fvs (TcType -> TcType -> TcM Bool
tcSubsumes TcType
ht TcType
ty)
where fvs :: FV
fvs = [TcType] -> FV
tyCoFVsOfTypes [TcType
ht,TcType
ty]
go :: [(HoleFit, [HoleFit])] -> [HoleFit] -> TcM [HoleFit]
go :: [(HoleFit, [HoleFit])] -> [HoleFit] -> TcM [HoleFit]
go [(HoleFit, [HoleFit])]
sofar [] = do { String -> SDoc -> TcRn ()
traceTc String
"subsumptionGraph was" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr [(HoleFit, [HoleFit])]
sofar
; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. [a] -> [a] -> [a]
(++) forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> ([a], [a])
partition HoleFit -> Bool
hfIsLcl [HoleFit]
topSorted }
where toV :: (HoleFit, [HoleFit]) -> (HoleFit, Id, [Id])
toV (HoleFit
hf, [HoleFit]
adjs) = (HoleFit
hf, HoleFit -> Id
hfId HoleFit
hf, forall a b. (a -> b) -> [a] -> [b]
map HoleFit -> Id
hfId [HoleFit]
adjs)
(Graph
graph, Int -> (HoleFit, Id, [Id])
fromV, Id -> Maybe Int
_) = forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Int -> (node, key, [key]), key -> Maybe Int)
graphFromEdges forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (HoleFit, [HoleFit]) -> (HoleFit, Id, [Id])
toV [(HoleFit, [HoleFit])]
sofar
topSorted :: [HoleFit]
topSorted = forall a b. (a -> b) -> [a] -> [b]
map ((\(HoleFit
h,Id
_,[Id]
_) -> HoleFit
h) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (HoleFit, Id, [Id])
fromV) forall a b. (a -> b) -> a -> b
$ Graph -> [Int]
topSort Graph
graph
go [(HoleFit, [HoleFit])]
sofar (HoleFit
hf:[HoleFit]
hfs) =
do { [HoleFit]
adjs <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (TcType -> TcType -> TcM Bool
tcSubsumesWCloning (HoleFit -> TcType
hfType HoleFit
hf) 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)forall a. a -> [a] -> [a]
:[(HoleFit, [HoleFit])]
sofar) [HoleFit]
hfs }
tcFilterHoleFits :: Maybe Int
-> TypedHole
-> (TcType, [TcTyVar])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
tcFilterHoleFits :: Maybe Int
-> TypedHole
-> (TcType, [Id])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
tcFilterHoleFits (Just Int
0) TypedHole
_ (TcType, [Id])
_ [HoleFitCandidate]
_ = forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [])
tcFilterHoleFits Maybe Int
limit TypedHole
typed_hole ht :: (TcType, [Id])
ht@(TcType
hole_ty, [Id]
_) [HoleFitCandidate]
candidates =
do { String -> SDoc -> TcRn ()
traceTc String
"checkingFitsFor {" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr TcType
hole_ty
; (Bool
discards, [HoleFit]
subs) <- [HoleFit]
-> VarSet
-> Maybe Int
-> (TcType, [Id])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
go [] VarSet
emptyVarSet Maybe Int
limit (TcType, [Id])
ht [HoleFitCandidate]
candidates
; String -> SDoc -> TcRn ()
traceTc String
"checkingFitsFor }" SDoc
empty
; 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
go :: [HoleFit]
-> VarSet
-> Maybe Int
-> (TcType, [TcTyVar])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
go :: [HoleFit]
-> VarSet
-> Maybe Int
-> (TcType, [Id])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
go [HoleFit]
subs VarSet
_ Maybe Int
_ (TcType, [Id])
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, forall a. [a] -> [a]
reverse [HoleFit]
subs)
go [HoleFit]
subs VarSet
_ (Just Int
0) (TcType, [Id])
_ [HoleFitCandidate]
_ = forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, forall a. [a] -> [a]
reverse [HoleFit]
subs)
go [HoleFit]
subs VarSet
seen Maybe Int
maxleft (TcType, [Id])
ty (HoleFitCandidate
el:[HoleFitCandidate]
elts) =
forall r. TcM r -> TcM r -> TcM r
tryTcDiscardingErrs TcM (Bool, [HoleFit])
discard_it forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcRn ()
traceTc String
"lookingUp" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr HoleFitCandidate
el
; Maybe (Id, TcType)
maybeThing <- HoleFitCandidate -> TcM (Maybe (Id, TcType))
lookup HoleFitCandidate
el
; case Maybe (Id, TcType)
maybeThing of
Just (Id
id, TcType
id_ty) | Id -> Bool
not_trivial Id
id ->
do { Maybe ([TcType], [TcType])
fits <- (TcType, [Id]) -> TcType -> TcM (Maybe ([TcType], [TcType]))
fitsHole (TcType, [Id])
ty TcType
id_ty
; case Maybe ([TcType], [TcType])
fits of
Just ([TcType]
wrp, [TcType]
matches) -> Id -> TcType -> [TcType] -> [TcType] -> TcM (Bool, [HoleFit])
keep_it Id
id TcType
id_ty [TcType]
wrp [TcType]
matches
Maybe ([TcType], [TcType])
_ -> TcM (Bool, [HoleFit])
discard_it }
Maybe (Id, TcType)
_ -> TcM (Bool, [HoleFit])
discard_it }
where
not_trivial :: Id -> Bool
not_trivial Id
id = Name -> Maybe Module
nameModule_maybe (Id -> Name
idName Id
id) forall a. Eq a => a -> a -> Bool
/= forall a. a -> Maybe a
Just Module
gHC_ERR
lookup :: HoleFitCandidate -> TcM (Maybe (Id, Type))
lookup :: HoleFitCandidate -> TcM (Maybe (Id, TcType))
lookup (IdHFCand Id
id) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (Id
id, Id -> TcType
idType Id
id))
lookup HoleFitCandidate
hfc = do { TcTyThing
thing <- Name -> TcM TcTyThing
tcLookup Name
name
; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case TcTyThing
thing of
ATcId {tct_id :: TcTyThing -> Id
tct_id = Id
id} -> forall a. a -> Maybe a
Just (Id
id, Id -> TcType
idType Id
id)
AGlobal (AnId Id
id) -> forall a. a -> Maybe a
Just (Id
id, Id -> TcType
idType Id
id)
AGlobal (AConLike (RealDataCon DataCon
con)) ->
forall a. a -> Maybe a
Just (DataCon -> Id
dataConWrapId DataCon
con, DataCon -> TcType
dataConNonlinearType DataCon
con)
TcTyThing
_ -> forall a. Maybe a
Nothing }
where name :: Name
name = case HoleFitCandidate
hfc of
#if __GLASGOW_HASKELL__ < 901
IdHFCand id -> idName id
#endif
GreHFCand GlobalRdrElt
gre -> GlobalRdrElt -> Name
greMangledName GlobalRdrElt
gre
NameHFCand Name
name -> Name
name
discard_it :: TcM (Bool, [HoleFit])
discard_it = [HoleFit]
-> VarSet
-> Maybe Int
-> (TcType, [Id])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
go [HoleFit]
subs VarSet
seen Maybe Int
maxleft (TcType, [Id])
ty [HoleFitCandidate]
elts
keep_it :: Id -> TcType -> [TcType] -> [TcType] -> TcM (Bool, [HoleFit])
keep_it Id
eid TcType
eid_ty [TcType]
wrp [TcType]
ms = [HoleFit]
-> VarSet
-> Maybe Int
-> (TcType, [Id])
-> [HoleFitCandidate]
-> TcM (Bool, [HoleFit])
go (HoleFit
fitforall a. a -> [a] -> [a]
:[HoleFit]
subs) (VarSet -> Id -> VarSet
extendVarSet VarSet
seen Id
eid)
((\Int
n -> Int
n forall a. Num a => a -> a -> a
- Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
maxleft) (TcType, [Id])
ty [HoleFitCandidate]
elts
where
fit :: HoleFit
fit = HoleFit { hfId :: Id
hfId = Id
eid, hfCand :: HoleFitCandidate
hfCand = HoleFitCandidate
el, hfType :: TcType
hfType = TcType
eid_ty
, hfRefLvl :: Int
hfRefLvl = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a b. (a, b) -> b
snd (TcType, [Id])
ty)
, hfWrap :: [TcType]
hfWrap = [TcType]
wrp, hfMatches :: [TcType]
hfMatches = [TcType]
ms
, hfDoc :: Maybe HsDocString
hfDoc = forall a. Maybe a
Nothing }
unfoldWrapper :: HsWrapper -> [Type]
unfoldWrapper :: HsWrapper -> [TcType]
unfoldWrapper = forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsWrapper -> [TcType]
unfWrp'
where unfWrp' :: HsWrapper -> [TcType]
unfWrp' (WpTyApp TcType
ty) = [TcType
ty]
unfWrp' (WpCompose HsWrapper
w1 HsWrapper
w2) = HsWrapper -> [TcType]
unfWrp' HsWrapper
w1 forall a. [a] -> [a] -> [a]
++ HsWrapper -> [TcType]
unfWrp' HsWrapper
w2
unfWrp' HsWrapper
_ = []
fitsHole :: (TcType, [TcTyVar])
-> TcType
-> TcM (Maybe ([TcType], [TcType]))
fitsHole :: (TcType, [Id]) -> TcType -> TcM (Maybe ([TcType], [TcType]))
fitsHole (TcType
h_ty, [Id]
ref_vars) TcType
ty =
forall a. FV -> TcM a -> TcM a
withoutUnification FV
fvs forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcRn ()
traceTc String
"checkingFitOf {" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr TcType
ty
; (Bool
fits, HsWrapper
wrp) <- TypedHole -> TcType -> TcType -> TcM (Bool, HsWrapper)
tcCheckHoleFit TypedHole
hole TcType
h_ty TcType
ty
; String -> SDoc -> TcRn ()
traceTc String
"Did it fit?" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr Bool
fits
; String -> SDoc -> TcRn ()
traceTc String
"wrap is: " forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr HsWrapper
wrp
; String -> SDoc -> TcRn ()
traceTc String
"checkingFitOf }" SDoc
empty
; [TcType]
z_wrp_tys <- [TcType] -> TcM [TcType]
zonkTcTypes (HsWrapper -> [TcType]
unfoldWrapper HsWrapper
wrp)
; if Bool
fits
then if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Id]
ref_vars
then forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just ([TcType]
z_wrp_tys, []))
else do { let
fvSet :: VarSet
fvSet = FV -> VarSet
fvVarSet FV
fvs
notAbstract :: TcType -> Bool
notAbstract :: TcType -> Bool
notAbstract TcType
t = case TcType -> Maybe Id
getTyVar_maybe TcType
t of
Just Id
tv -> Id
tv Id -> VarSet -> Bool
`elemVarSet` VarSet
fvSet
Maybe Id
_ -> Bool
True
allConcrete :: Bool
allConcrete = 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 = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TcType -> Maybe Id
tcGetTyVar_maybe [TcType]
z_vars
; Bool
allFilled <- Bool -> Bool
not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m Bool
anyM Id -> TcM Bool
isFlexiTyVar [Id]
z_mtvs
; Bool
allowAbstract <- 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 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ([TcType]
z_wrp_tys, [TcType]
z_vars)
else forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing }
else forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing }
where fvs :: FV
fvs = [Id] -> FV
mkFVs [Id]
ref_vars FV -> FV -> FV
`unionFV` FV
hole_fvs FV -> FV -> FV
`unionFV` TcType -> FV
tyCoFVsOfType TcType
ty
hole :: TypedHole
hole = TypedHole
typed_hole { th_hole :: Maybe Hole
th_hole = forall a. Maybe a
Nothing }
isFlexiTyVar :: TcTyVar -> TcM Bool
isFlexiTyVar :: Id -> TcM Bool
isFlexiTyVar Id
tv | Id -> Bool
isMetaTyVar Id
tv = MetaDetails -> Bool
isFlexi forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Id -> TcM MetaDetails
readMetaTyVar Id
tv
isFlexiTyVar Id
_ = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
withoutUnification :: FV -> TcM a -> TcM a
withoutUnification :: forall a. FV -> TcM a -> TcM a
withoutUnification FV
free_vars TcM a
action =
do { [Id]
flexis <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM Id -> TcM Bool
isFlexiTyVar [Id]
fuvs
; a
result <- TcM a
action
; forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Id -> TcRn ()
restore [Id]
flexis
; forall (m :: * -> *) a. Monad m => a -> m a
return a
result }
where restore :: Id -> TcRn ()
restore Id
tv = do { String -> SDoc -> TcRn ()
traceTc String
"withoutUnification: restore flexi" (forall a. Outputable a => a -> SDoc
ppr Id
tv)
; forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
writeTcRef (Id -> IORef MetaDetails
metaTyVarRef Id
tv) MetaDetails
Flexi }
fuvs :: [Id]
fuvs = FV -> [Id]
fvVarList FV
free_vars
tcSubsumes :: TcSigmaType -> TcSigmaType -> TcM Bool
tcSubsumes :: TcType -> TcType -> TcM Bool
tcSubsumes TcType
ty_a TcType
ty_b = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypedHole -> TcType -> TcType -> TcM (Bool, HsWrapper)
tcCheckHoleFit TypedHole
dummyHole TcType
ty_a TcType
ty_b
where dummyHole :: TypedHole
dummyHole = TypedHole { th_relevant_cts :: Cts
th_relevant_cts = forall a. Bag a
emptyBag
, th_implics :: [Implication]
th_implics = []
, th_hole :: Maybe Hole
th_hole = forall a. Maybe a
Nothing }
tcCheckHoleFit :: TypedHole
-> TcSigmaType
-> TcSigmaType
-> TcM (Bool, HsWrapper)
tcCheckHoleFit :: TypedHole -> TcType -> TcType -> TcM (Bool, HsWrapper)
tcCheckHoleFit TypedHole
_ TcType
hole_ty TcType
ty | TcType
hole_ty TcType -> TcType -> Bool
`eqType` TcType
ty
= forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, HsWrapper
idHsWrapper)
tcCheckHoleFit (TypedHole {[Implication]
Maybe Hole
Cts
th_hole :: Maybe Hole
th_implics :: [Implication]
th_relevant_cts :: Cts
th_hole :: TypedHole -> Maybe Hole
th_implics :: TypedHole -> [Implication]
th_relevant_cts :: TypedHole -> Cts
..}) TcType
hole_ty TcType
ty = forall a. TcRn a -> TcRn a
discardErrs forall a b. (a -> b) -> a -> b
$
do {
TcLevel
innermost_lvl <- case [Implication]
th_implics of
[] -> IOEnv (Env TcGblEnv TcLclEnv) TcLevel
getTcLevel
(Implication
imp:[Implication]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Implication -> TcLevel
ic_tclvl Implication
imp)
; (HsWrapper
wrap, WantedConstraints
wanted) <- forall a. TcLevel -> TcM a -> TcM a
setTcLevel TcLevel
innermost_lvl forall a b. (a -> b) -> a -> b
$ forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints forall a b. (a -> b) -> a -> b
$
CtOrigin -> UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
tcSubTypeSigma CtOrigin
orig UserTypeCtxt
ExprSigCtxt TcType
ty TcType
hole_ty
; String -> SDoc -> TcRn ()
traceTc String
"Checking hole fit {" SDoc
empty
; String -> SDoc -> TcRn ()
traceTc String
"wanteds are: " forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr WantedConstraints
wanted
; if WantedConstraints -> Bool
isEmptyWC WantedConstraints
wanted Bool -> Bool -> Bool
&& forall a. Bag a -> Bool
isEmptyBag Cts
th_relevant_cts
then do { String -> SDoc -> TcRn ()
traceTc String
"}" SDoc
empty
; forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, HsWrapper
wrap) }
else do { EvBindsVar
fresh_binds <- TcM EvBindsVar
newTcEvBinds
; Cts
cloned_relevants <- forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Bag a -> m (Bag b)
mapBagM Ct -> TcM Ct
cloneWanted Cts
th_relevant_cts
; let outermost_first :: [Implication]
outermost_first = forall a. [a] -> [a]
reverse [Implication]
th_implics
w_rel_cts :: WantedConstraints
w_rel_cts = WantedConstraints -> Cts -> WantedConstraints
addSimples WantedConstraints
wanted Cts
cloned_relevants
final_wc :: WantedConstraints
final_wc = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (EvBindsVar -> Implication -> WantedConstraints -> WantedConstraints
setWCAndBinds EvBindsVar
fresh_binds) WantedConstraints
w_rel_cts [Implication]
outermost_first
; String -> SDoc -> TcRn ()
traceTc String
"final_wc is: " forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr WantedConstraints
final_wc
; WantedConstraints
rem <- forall a. TcS a -> TcM a
runTcSDeriveds forall a b. (a -> b) -> a -> b
$ WantedConstraints -> TcS WantedConstraints
simplifyTopWanteds WantedConstraints
final_wc
; String -> SDoc -> TcRn ()
traceTc String
"rems was:" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr WantedConstraints
rem
; String -> SDoc -> TcRn ()
traceTc String
"}" SDoc
empty
; forall (m :: * -> *) a. Monad m => a -> m a
return (WantedConstraints -> Bool
isSolvedWC WantedConstraints
rem, HsWrapper
wrap) } }
where
orig :: CtOrigin
orig = Maybe OccName -> CtOrigin
ExprHoleOrigin (Hole -> OccName
hole_occ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Hole
th_hole)
setWCAndBinds :: EvBindsVar
-> Implication
-> WantedConstraints
-> WantedConstraints
setWCAndBinds :: EvBindsVar -> Implication -> WantedConstraints -> WantedConstraints
setWCAndBinds EvBindsVar
binds Implication
imp WantedConstraints
wc
= Bag Implication -> WantedConstraints
mkImplicWC forall a b. (a -> b) -> a -> b
$ forall a. a -> Bag a
unitBag forall a b. (a -> b) -> a -> b
$ Implication
imp { ic_wanted :: WantedConstraints
ic_wanted = WantedConstraints
wc , ic_binds :: EvBindsVar
ic_binds = EvBindsVar
binds }