Safe Haskell	None
Language	Haskell2010

Wingman.Judgements.Theta

Synopsis

data Evidence
getEvidenceAtHole :: Tracked age SrcSpan -> Tracked age (LHsBinds GhcTc) -> [Evidence]
mkEvidence :: PredType -> [Evidence]
evidenceToCoercions :: [Evidence] -> [(CType, CType)]
evidenceToSubst :: [Evidence] -> TacticState -> TacticState
evidenceToHypothesis :: Evidence -> Hypothesis CType
evidenceToThetaType :: [Evidence] -> Set CType
allEvidenceToSubst :: Set TyVar -> [(Type, Type)] -> TCvSubst

Documentation

data Evidence Source #

Something we've learned about the type environment.

Instances

Instances details

Show Evidence Source #
Instance details Defined in Wingman.Judgements.Theta Methods showsPrec :: Int -> Evidence -> ShowS # show :: Evidence -> String # showList :: [Evidence] -> ShowS #
Generic Evidence Source #
Instance details Defined in Wingman.Judgements.Theta Associated Types type Rep Evidence :: Type -> Type # Methods from :: Evidence -> Rep Evidence x # to :: Rep Evidence x -> Evidence #
type Rep Evidence Source #
Instance details Defined in Wingman.Judgements.Theta type Rep Evidence = D1 ('MetaData "Evidence" "Wingman.Judgements.Theta" "hls-tactics-plugin-1.6.1.0-H41kd3uDZThIe8qdfZ8zJi" 'False) (C1 ('MetaCons "EqualityOfTypes" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "HasInstance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PredType)))

getEvidenceAtHole :: Tracked age SrcSpan -> Tracked age (LHsBinds GhcTc) -> [Evidence] Source #

Compute all the Evidence implicitly bound at the given SrcSpan.

mkEvidence :: PredType -> [Evidence] Source #

Given a PredType, pull an Evidence out of it.

evidenceToCoercions :: [Evidence] -> [(CType, CType)] Source #

Given some Evidence, get a list of which types are now equal.

evidenceToSubst :: [Evidence] -> TacticState -> TacticState Source #

Update our knowledge of which types are equal.

evidenceToHypothesis :: Evidence -> Hypothesis CType Source #

Get all of the methods that are in scope from this piece of Evidence.

evidenceToThetaType :: [Evidence] -> Set CType Source #

Build a set of PredTypes from the evidence.

allEvidenceToSubst :: Set TyVar -> [(Type, Type)] -> TCvSubst Source #

Construct a substitution given a list of types that are equal to one another. This is more subtle than it seems, since there might be several equalities for the same type. We must be careful to push the accumulating substitution through each pair of types before adding their equalities.