hls-tactics-plugin-1.6.1.0: Wingman plugin for Haskell Language Server
Safe HaskellNone
LanguageHaskell2010

Wingman.Judgements.Theta

Synopsis

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

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.