Safe Haskell	None
Language	Haskell2010

TcHoleErrors

Synopsis

findValidHoleFits :: TidyEnv -> [Implication] -> [Ct] -> Ct -> TcM (TidyEnv, SDoc)
tcFilterHoleFits :: Maybe Int -> TypedHole -> (TcType, [TcTyVar]) -> [HoleFitCandidate] -> TcM (Bool, [HoleFit])
tcCheckHoleFit :: TypedHole -> TcSigmaType -> TcSigmaType -> TcM (Bool, HsWrapper)
tcSubsumes :: TcSigmaType -> TcSigmaType -> TcM Bool
withoutUnification :: FV -> TcM a -> TcM a
fromPureHFPlugin :: HoleFitPlugin -> HoleFitPluginR
hfIsLcl :: HoleFit -> Bool
pprHoleFit :: HoleFitDispConfig -> HoleFit -> SDoc
debugHoleFitDispConfig :: HoleFitDispConfig
data TypedHole = TyH {
- tyHRelevantCts :: Cts
- tyHImplics :: [Implication]
- tyHCt :: Maybe Ct
}
data HoleFit
- = HoleFit {
  - hfId :: Id
  - hfCand :: HoleFitCandidate
  - hfType :: TcType
  - hfRefLvl :: Int
  - hfWrap :: [TcType]
  - hfMatches :: [TcType]
  - hfDoc :: Maybe HsDocString
  }
- | RawHoleFit SDoc
data HoleFitCandidate
- = IdHFCand Id
- | NameHFCand Name
- | GreHFCand GlobalRdrElt
type CandPlugin = TypedHole -> [HoleFitCandidate] -> TcM [HoleFitCandidate]
type FitPlugin = TypedHole -> [HoleFit] -> TcM [HoleFit]
data HoleFitPlugin = HoleFitPlugin {
- candPlugin :: CandPlugin
- fitPlugin :: FitPlugin
}
data HoleFitPluginR = forall s. HoleFitPluginR {
- hfPluginInit :: TcM (TcRef s)
- hfPluginRun :: TcRef s -> HoleFitPlugin
- hfPluginStop :: TcRef s -> TcM ()
}

Documentation

findValidHoleFits Source #

Arguments

:: 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)

tcFilterHoleFits Source #

Arguments

:: Maybe Int	How many we should output, if limited
-> TypedHole	The hole to filter against
-> (TcType, [TcTyVar])	The type to check for fits and a list of refinement variables (free type variables in the type) for emulating additional holes.
-> [HoleFitCandidate]	The candidates to check whether fit.
-> TcM (Bool, [HoleFit])	We return whether or not we stopped due to hitting the limit and the fits we found.

tcFilterHoleFits 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.

tcCheckHoleFit Source #

Arguments

:: TypedHole	The hole to check against
-> TcSigmaType	The type to check against (possibly modified, e.g. refined)
-> TcSigmaType	The type to check whether fits.
-> TcM (Bool, HsWrapper)	Whether it was a match, and the wrapper from hole_ty to ty.

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.

tcSubsumes :: TcSigmaType -> TcSigmaType -> TcM Bool Source #

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.

withoutUnification :: FV -> TcM a -> TcM a Source #

Takes a list of free variables and restores any Flexi type variables in free_vars after the action is run.

fromPureHFPlugin :: HoleFitPlugin -> HoleFitPluginR Source #

Maps a plugin that needs no state to one with an empty one.

hfIsLcl :: HoleFit -> Bool Source #

pprHoleFit :: HoleFitDispConfig -> HoleFit -> SDoc Source #

debugHoleFitDispConfig :: HoleFitDispConfig Source #

data TypedHole Source #

Constructors

TyH
Fields tyHRelevantCts :: Cts Any relevant Cts to the hole tyHImplics :: [Implication] The nested implications of the hole with the innermost implication first. tyHCt :: Maybe Ct The hole constraint itself, if available.

Instances

Instances details

Outputable TypedHole Source #
Instance details Defined in TcHoleFitTypes Methods ppr :: TypedHole -> SDoc Source # pprPrec :: Rational -> TypedHole -> SDoc Source #

data HoleFit Source #

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 _ _`).

Constructors

HoleFit
Fields hfId :: Id The elements id in the TcM hfCand :: HoleFitCandidate The candidate that was checked. hfType :: TcType The type of the id, possibly zonked. hfRefLvl :: Int The number of holes in this fit. hfWrap :: [TcType] The wrapper for the match. hfMatches :: [TcType] What the refinement variables got matched with, if anything hfDoc :: Maybe HsDocString Documentation of this HoleFit, if available.
RawHoleFit SDoc	A fit that is just displayed as is. Here so thatHoleFitPlugins can inject any fit they want.

Instances

Instances details

Eq HoleFit Source #
Instance details Defined in TcHoleFitTypes Methods (==) :: HoleFit -> HoleFit -> Bool # (/=) :: HoleFit -> HoleFit -> Bool #
Ord HoleFit Source #
Instance details Defined in TcHoleFitTypes Methods compare :: HoleFit -> HoleFit -> Ordering # (<) :: HoleFit -> HoleFit -> Bool # (<=) :: HoleFit -> HoleFit -> Bool # (>) :: HoleFit -> HoleFit -> Bool # (>=) :: HoleFit -> HoleFit -> Bool # max :: HoleFit -> HoleFit -> HoleFit # min :: HoleFit -> HoleFit -> HoleFit #
Outputable HoleFit Source #
Instance details Defined in TcHoleFitTypes Methods ppr :: HoleFit -> SDoc Source # pprPrec :: Rational -> HoleFit -> SDoc Source #

data HoleFitCandidate Source #

HoleFitCandidates are passed to hole fit plugins and then checked whether they fit a given typed-hole.

Constructors

IdHFCand Id
NameHFCand Name
GreHFCand GlobalRdrElt

Instances

Instances details

Eq HoleFitCandidate Source #
Instance details Defined in TcHoleFitTypes Methods (==) :: HoleFitCandidate -> HoleFitCandidate -> Bool # (/=) :: HoleFitCandidate -> HoleFitCandidate -> Bool #
Ord HoleFitCandidate Source #
Instance details Defined in TcHoleFitTypes Methods compare :: HoleFitCandidate -> HoleFitCandidate -> Ordering # (<) :: HoleFitCandidate -> HoleFitCandidate -> Bool # (<=) :: HoleFitCandidate -> HoleFitCandidate -> Bool # (>) :: HoleFitCandidate -> HoleFitCandidate -> Bool # (>=) :: HoleFitCandidate -> HoleFitCandidate -> Bool # max :: HoleFitCandidate -> HoleFitCandidate -> HoleFitCandidate # min :: HoleFitCandidate -> HoleFitCandidate -> HoleFitCandidate #
Outputable HoleFitCandidate Source #
Instance details Defined in TcHoleFitTypes Methods ppr :: HoleFitCandidate -> SDoc Source # pprPrec :: Rational -> HoleFitCandidate -> SDoc Source #
HasOccName HoleFitCandidate Source #
Instance details Defined in TcHoleFitTypes Methods occName :: HoleFitCandidate -> OccName Source #
NamedThing HoleFitCandidate Source #
Instance details Defined in TcHoleFitTypes Methods getOccName :: HoleFitCandidate -> OccName Source # getName :: HoleFitCandidate -> Name Source #

type CandPlugin = TypedHole -> [HoleFitCandidate] -> TcM [HoleFitCandidate] Source #

A plugin for modifying the candidate hole fits *before* they're checked.

type FitPlugin = TypedHole -> [HoleFit] -> TcM [HoleFit] Source #

A plugin for modifying hole fits *after* they've been found.

data HoleFitPlugin Source #

A HoleFitPlugin is a pair of candidate and fit plugins.

Constructors

HoleFitPlugin
Fields candPlugin :: CandPlugin fitPlugin :: FitPlugin

data HoleFitPluginR Source #

HoleFitPluginR adds a TcRef to hole fit plugins so that plugins can track internal state. Note the existential quantification, ensuring that the state cannot be modified from outside the plugin.

Constructors

forall s. HoleFitPluginR
Fields hfPluginInit :: TcM (TcRef s) Initializes the TcRef to be passed to the plugin hfPluginRun :: TcRef s -> HoleFitPlugin The function defining the plugin itself hfPluginStop :: TcRef s -> TcM () Cleanup of state, guaranteed to be called even on error