Wingman.Judgements.Theta

Documentation

data Evidence

Something we've learned about the type environment.

Instances

Show Evidence

Defined in Wingman.Judgements.Theta

Methods

showsPrec :: Int -> Evidence -> ShowS

show :: Evidence -> String

showList :: [Evidence] -> ShowS

Generic Evidence

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

Defined in Wingman.Judgements.Theta

type Rep Evidence = D1 ('MetaData "Evidence" "Wingman.Judgements.Theta" "hls-tactics-plugin-1.4.0.0-CDY1FtnQAdCF6qnNiOOrMd" '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]

Compute all the Evidence implicitly bound at the given SrcSpan.

mkEvidence :: PredType -> [Evidence]

Given a PredType, pull an Evidence out of it.

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

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

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

Update our knowledge of which types are equal.

evidenceToHypothesis :: Evidence -> Hypothesis CType

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

evidenceToThetaType :: [Evidence] -> Set CType

Build a set of PredTypes from the evidence.

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

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.