{-# LANGUAGE CPP          #-}
{-# LANGUAGE ViewPatterns #-}

module Wingman.Judgements.Theta
  ( Evidence
  , getEvidenceAtHole
  , mkEvidence
  , evidenceToCoercions
  , evidenceToSubst
  , evidenceToHypothesis
  , evidenceToThetaType
  , allEvidenceToSubst
  ) where

import           Control.Applicative (empty)
import           Control.Lens (preview)
import           Data.Coerce (coerce)
import           Data.Maybe (fromMaybe, mapMaybe, maybeToList)
import           Data.Generics.Sum (_Ctor)
import           Data.Set (Set)
import qualified Data.Set as S
import           Development.IDE.Core.UseStale
import           Development.IDE.GHC.Compat hiding (empty)
import           Generics.SYB hiding (tyConName, empty, Generic)
import           GHC.Generics
import           Wingman.GHC
import           Wingman.Types

#if __GLASGOW_HASKELL__ >= 900
import GHC.Tc.Utils.TcType
#endif


------------------------------------------------------------------------------
-- | Something we've learned about the type environment.
data Evidence
    -- | The two types are equal, via a @a ~ b@ relationship
  = EqualityOfTypes Type Type
    -- | We have an instance in scope
  | HasInstance PredType
  deriving (Int -> Evidence -> ShowS
[Evidence] -> ShowS
Evidence -> String
(Int -> Evidence -> ShowS)
-> (Evidence -> String) -> ([Evidence] -> ShowS) -> Show Evidence
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Evidence] -> ShowS
$cshowList :: [Evidence] -> ShowS
show :: Evidence -> String
$cshow :: Evidence -> String
showsPrec :: Int -> Evidence -> ShowS
$cshowsPrec :: Int -> Evidence -> ShowS
Show, (forall x. Evidence -> Rep Evidence x)
-> (forall x. Rep Evidence x -> Evidence) -> Generic Evidence
forall x. Rep Evidence x -> Evidence
forall x. Evidence -> Rep Evidence x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Evidence x -> Evidence
$cfrom :: forall x. Evidence -> Rep Evidence x
Generic)


------------------------------------------------------------------------------
-- | Given a 'PredType', pull an 'Evidence' out of it.
mkEvidence :: PredType -> [Evidence]
mkEvidence :: PredType -> [Evidence]
mkEvidence (PredType -> Maybe (PredType, PredType)
getEqualityTheta -> Just (PredType
a, PredType
b))
  = Evidence -> [Evidence]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Evidence -> [Evidence]) -> Evidence -> [Evidence]
forall a b. (a -> b) -> a -> b
$ PredType -> PredType -> Evidence
EqualityOfTypes PredType
a PredType
b
mkEvidence inst :: PredType
inst@(PredType -> Maybe TyCon
tcTyConAppTyCon_maybe -> Just (TyCon -> Maybe Class
tyConClass_maybe -> Just Class
cls)) = do
  (TyCon
_, [PredType]
apps) <- Maybe (TyCon, [PredType]) -> [(TyCon, [PredType])]
forall a. Maybe a -> [a]
maybeToList (Maybe (TyCon, [PredType]) -> [(TyCon, [PredType])])
-> Maybe (TyCon, [PredType]) -> [(TyCon, [PredType])]
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
inst
  let tvs :: [TyVar]
tvs     = Class -> [TyVar]
classTyVars Class
cls
      subst :: TCvSubst
subst   = [TyVar] -> [PredType] -> TCvSubst
HasDebugCallStack => [TyVar] -> [PredType] -> TCvSubst
zipTvSubst [TyVar]
tvs [PredType]
apps
  [Evidence]
sc_ev <- (PredType -> [Evidence]) -> [PredType] -> [[Evidence]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (PredType -> [Evidence]
mkEvidence (PredType -> [Evidence])
-> (PredType -> PredType) -> PredType -> [Evidence]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => TCvSubst -> PredType -> PredType
TCvSubst -> PredType -> PredType
substTy TCvSubst
subst) ([PredType] -> [[Evidence]]) -> [PredType] -> [[Evidence]]
forall a b. (a -> b) -> a -> b
$ Class -> [PredType]
classSCTheta Class
cls
  PredType -> Evidence
HasInstance PredType
inst Evidence -> [Evidence] -> [Evidence]
forall a. a -> [a] -> [a]
: [Evidence]
sc_ev
mkEvidence PredType
_ = [Evidence]
forall (f :: * -> *) a. Alternative f => f a
empty


------------------------------------------------------------------------------
-- | Build a set of 'PredType's from the evidence.
evidenceToThetaType :: [Evidence] -> Set CType
evidenceToThetaType :: [Evidence] -> Set CType
evidenceToThetaType [Evidence]
evs = [CType] -> Set CType
forall a. Ord a => [a] -> Set a
S.fromList ([CType] -> Set CType) -> [CType] -> Set CType
forall a b. (a -> b) -> a -> b
$ do
  HasInstance PredType
t <- [Evidence]
evs
  CType -> [CType]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CType -> [CType]) -> CType -> [CType]
forall a b. (a -> b) -> a -> b
$ PredType -> CType
CType PredType
t


------------------------------------------------------------------------------
-- | Compute all the 'Evidence' implicitly bound at the given 'SrcSpan'.
getEvidenceAtHole :: Tracked age SrcSpan -> Tracked age (LHsBinds GhcTc) -> [Evidence]
getEvidenceAtHole :: Tracked age SrcSpan -> Tracked age (LHsBinds GhcTc) -> [Evidence]
getEvidenceAtHole (Tracked age SrcSpan -> SrcSpan
forall (age :: Age) a. Tracked age a -> a
unTrack -> SrcSpan
dst)
  = (PredType -> [Evidence]) -> [PredType] -> [Evidence]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PredType -> [Evidence]
mkEvidence
  ([PredType] -> [Evidence])
-> (Tracked age (LHsBinds GhcTc) -> [PredType])
-> Tracked age (LHsBinds GhcTc)
-> [Evidence]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([PredType] -> [PredType] -> [PredType])
-> GenericQ [PredType] -> GenericQ [PredType]
forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything [PredType] -> [PredType] -> [PredType]
forall a. Semigroup a => a -> a -> a
(<>) (GenericQ [PredType] -> GenericQ [PredType])
-> GenericQ [PredType] -> GenericQ [PredType]
forall a b. (a -> b) -> a -> b
$
        [PredType]
-> (LHsBindLR GhcTc GhcTc -> [PredType]) -> a -> [PredType]
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
mkQ [PredType]
forall a. Monoid a => a
mempty (SrcSpan -> LHsBindLR GhcTc GhcTc -> [PredType]
absBinds SrcSpan
dst) (a -> [PredType])
-> (LHsExpr GhcTc -> [PredType]) -> a -> [PredType]
forall a b q.
(Typeable a, Typeable b) =>
(a -> q) -> (b -> q) -> a -> q
`extQ` SrcSpan -> LHsExpr GhcTc -> [PredType]
wrapperBinds SrcSpan
dst (a -> [PredType])
-> (LMatch GhcTc (LHsExpr GhcTc) -> [PredType]) -> a -> [PredType]
forall a b q.
(Typeable a, Typeable b) =>
(a -> q) -> (b -> q) -> a -> q
`extQ` SrcSpan -> LMatch GhcTc (LHsExpr GhcTc) -> [PredType]
matchBinds SrcSpan
dst)
  (LHsBinds GhcTc -> [PredType])
-> (Tracked age (LHsBinds GhcTc) -> LHsBinds GhcTc)
-> Tracked age (LHsBinds GhcTc)
-> [PredType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tracked age (LHsBinds GhcTc) -> LHsBinds GhcTc
forall (age :: Age) a. Tracked age a -> a
unTrack


mkSubst :: Set TyVar -> Type -> Type -> TCvSubst
mkSubst :: Set TyVar -> PredType -> PredType -> TCvSubst
mkSubst Set TyVar
skolems PredType
a PredType
b =
  let tyvars :: Set TyVar
tyvars = [TyVar] -> Set TyVar
forall a. Ord a => [a] -> Set a
S.fromList ([TyVar] -> Set TyVar) -> [TyVar] -> Set TyVar
forall a b. (a -> b) -> a -> b
$ (PredType -> Maybe TyVar) -> [PredType] -> [TyVar]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe PredType -> Maybe TyVar
getTyVar_maybe [PredType
a, PredType
b]
      -- If we can unify our skolems, at least one is no longer a skolem.
      -- Removing them from this set ensures we can get a subtitution between
      -- the two. But it's okay to leave them in 'ts_skolems' in general, since
      -- they won't exist after running this substitution.
      skolems' :: Set TyVar
skolems' = Set TyVar
skolems Set TyVar -> Set TyVar -> Set TyVar
forall a. Ord a => Set a -> Set a -> Set a
S.\\ Set TyVar
tyvars
   in
  case Set TyVar -> CType -> CType -> Maybe TCvSubst
tryUnifyUnivarsButNotSkolems Set TyVar
skolems' (PredType -> CType
CType PredType
a) (PredType -> CType
CType PredType
b) of
    Just TCvSubst
subst -> TCvSubst
subst
    Maybe TCvSubst
Nothing -> TCvSubst
emptyTCvSubst


substPair :: TCvSubst -> (Type, Type) -> (Type, Type)
substPair :: TCvSubst -> (PredType, PredType) -> (PredType, PredType)
substPair TCvSubst
subst (PredType
ty, PredType
ty') = (HasCallStack => TCvSubst -> PredType -> PredType
TCvSubst -> PredType -> PredType
substTy TCvSubst
subst PredType
ty, HasCallStack => TCvSubst -> PredType -> PredType
TCvSubst -> PredType -> PredType
substTy TCvSubst
subst PredType
ty')


------------------------------------------------------------------------------
-- | 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.
allEvidenceToSubst :: Set TyVar -> [(Type, Type)] -> TCvSubst
allEvidenceToSubst :: Set TyVar -> [(PredType, PredType)] -> TCvSubst
allEvidenceToSubst Set TyVar
_ [] = TCvSubst
emptyTCvSubst
allEvidenceToSubst Set TyVar
skolems ((PredType
a, PredType
b) : [(PredType, PredType)]
evs) =
  let subst :: TCvSubst
subst = Set TyVar -> PredType -> PredType -> TCvSubst
mkSubst Set TyVar
skolems PredType
a PredType
b
   in TCvSubst -> TCvSubst -> TCvSubst
unionTCvSubst TCvSubst
subst
    (TCvSubst -> TCvSubst) -> TCvSubst -> TCvSubst
forall a b. (a -> b) -> a -> b
$ Set TyVar -> [(PredType, PredType)] -> TCvSubst
allEvidenceToSubst Set TyVar
skolems
    ([(PredType, PredType)] -> TCvSubst)
-> [(PredType, PredType)] -> TCvSubst
forall a b. (a -> b) -> a -> b
$ ((PredType, PredType) -> (PredType, PredType))
-> [(PredType, PredType)] -> [(PredType, PredType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TCvSubst -> (PredType, PredType) -> (PredType, PredType)
substPair TCvSubst
subst) [(PredType, PredType)]
evs

------------------------------------------------------------------------------
-- | Given some 'Evidence', get a list of which types are now equal.
evidenceToCoercions :: [Evidence] -> [(CType, CType)]
evidenceToCoercions :: [Evidence] -> [(CType, CType)]
evidenceToCoercions = [(PredType, PredType)] -> [(CType, CType)]
coerce ([(PredType, PredType)] -> [(CType, CType)])
-> ([Evidence] -> [(PredType, PredType)])
-> [Evidence]
-> [(CType, CType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Evidence -> Maybe (PredType, PredType))
-> [Evidence] -> [(PredType, PredType)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Getting (First (PredType, PredType)) Evidence (PredType, PredType)
-> Evidence -> Maybe (PredType, PredType)
forall s (m :: * -> *) a.
MonadReader s m =>
Getting (First a) s a -> m (Maybe a)
preview (Getting (First (PredType, PredType)) Evidence (PredType, PredType)
 -> Evidence -> Maybe (PredType, PredType))
-> Getting
     (First (PredType, PredType)) Evidence (PredType, PredType)
-> Evidence
-> Maybe (PredType, PredType)
forall a b. (a -> b) -> a -> b
$ forall s t a b.
AsConstructor "EqualityOfTypes" s t a b =>
Prism s t a b
forall (ctor :: Symbol) s t a b.
AsConstructor ctor s t a b =>
Prism s t a b
_Ctor @"EqualityOfTypes")

------------------------------------------------------------------------------
-- | Update our knowledge of which types are equal.
evidenceToSubst :: [Evidence] -> TacticState -> TacticState
evidenceToSubst :: [Evidence] -> TacticState -> TacticState
evidenceToSubst [Evidence]
evs TacticState
ts =
  TCvSubst -> TacticState -> TacticState
updateSubst
    (Set TyVar -> [(PredType, PredType)] -> TCvSubst
allEvidenceToSubst (TacticState -> Set TyVar
ts_skolems TacticState
ts) ([(PredType, PredType)] -> TCvSubst)
-> ([(CType, CType)] -> [(PredType, PredType)])
-> [(CType, CType)]
-> TCvSubst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(CType, CType)] -> [(PredType, PredType)]
coerce ([(CType, CType)] -> TCvSubst) -> [(CType, CType)] -> TCvSubst
forall a b. (a -> b) -> a -> b
$ [Evidence] -> [(CType, CType)]
evidenceToCoercions [Evidence]
evs)
    TacticState
ts


------------------------------------------------------------------------------
-- | Get all of the methods that are in scope from this piece of 'Evidence'.
evidenceToHypothesis :: Evidence -> Hypothesis CType
evidenceToHypothesis :: Evidence -> Hypothesis CType
evidenceToHypothesis EqualityOfTypes{} = Hypothesis CType
forall a. Monoid a => a
mempty
evidenceToHypothesis (HasInstance PredType
t) =
  [HyInfo CType] -> Hypothesis CType
forall a. [HyInfo a] -> Hypothesis a
Hypothesis ([HyInfo CType] -> Hypothesis CType)
-> (Maybe [HyInfo CType] -> [HyInfo CType])
-> Maybe [HyInfo CType]
-> Hypothesis CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [HyInfo CType] -> [HyInfo CType]
forall a. [HyInfo a] -> [HyInfo a]
excludeForbiddenMethods ([HyInfo CType] -> [HyInfo CType])
-> (Maybe [HyInfo CType] -> [HyInfo CType])
-> Maybe [HyInfo CType]
-> [HyInfo CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [HyInfo CType] -> Maybe [HyInfo CType] -> [HyInfo CType]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [HyInfo CType] -> Hypothesis CType)
-> Maybe [HyInfo CType] -> Hypothesis CType
forall a b. (a -> b) -> a -> b
$ PredType -> Maybe [HyInfo CType]
methodHypothesis PredType
t


------------------------------------------------------------------------------
-- | Given @a ~ b@ or @a ~# b@, returns @Just (a, b)@, otherwise @Nothing@.
getEqualityTheta :: PredType -> Maybe (Type, Type)
getEqualityTheta :: PredType -> Maybe (PredType, PredType)
getEqualityTheta (HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe -> Just (TyCon
tc, [PredType
_k, PredType
a, PredType
b]))
#if __GLASGOW_HASKELL__ > 806
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
eqTyCon
#else
  | nameRdrName (tyConName tc) == eqTyCon_RDR
#endif
  = (PredType, PredType) -> Maybe (PredType, PredType)
forall a. a -> Maybe a
Just (PredType
a, PredType
b)
getEqualityTheta (HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe -> Just (TyCon
tc, [PredType
_k1, PredType
_k2, PredType
a, PredType
b]))
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
eqPrimTyCon = (PredType, PredType) -> Maybe (PredType, PredType)
forall a. a -> Maybe a
Just (PredType
a, PredType
b)
getEqualityTheta PredType
_ = Maybe (PredType, PredType)
forall a. Maybe a
Nothing


------------------------------------------------------------------------------
-- | Many operations are defined in typeclasses for performance reasons, rather
-- than being a true part of the class. This function filters out those, in
-- order to keep our hypothesis space small.
excludeForbiddenMethods :: [HyInfo a] -> [HyInfo a]
excludeForbiddenMethods :: [HyInfo a] -> [HyInfo a]
excludeForbiddenMethods = (HyInfo a -> Bool) -> [HyInfo a] -> [HyInfo a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (HyInfo a -> Bool) -> HyInfo a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OccName -> Set OccName -> Bool) -> Set OccName -> OccName -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip OccName -> Set OccName -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Set OccName
forbiddenMethods (OccName -> Bool) -> (HyInfo a -> OccName) -> HyInfo a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo a -> OccName
forall a. HyInfo a -> OccName
hi_name)
  where
    forbiddenMethods :: Set OccName
    forbiddenMethods :: Set OccName
forbiddenMethods = (String -> OccName) -> Set String -> Set OccName
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map String -> OccName
mkVarOcc (Set String -> Set OccName) -> Set String -> Set OccName
forall a b. (a -> b) -> a -> b
$ [String] -> Set String
forall a. Ord a => [a] -> Set a
S.fromList
      [ -- monadfail
        String
"fail"
        -- show
      , String
"showsPrec", String
"showList"
        -- functor
      , String
"<$"
        -- applicative
      , String
"liftA2", String
"<*", String
"*>"
        -- monad
      , String
"return", String
">>"
        -- alternative
      , String
"some", String
"many"
        -- foldable
      , String
"foldr1", String
"foldl1", String
"elem", String
"maximum", String
"minimum", String
"sum", String
"product"
        -- traversable
      , String
"sequenceA", String
"mapM", String
"sequence"
        -- semigroup
      , String
"sconcat", String
"stimes"
        -- monoid
      , String
"mconcat"
      ]


------------------------------------------------------------------------------
-- | Extract evidence from 'AbsBinds' in scope.
absBinds ::  SrcSpan -> LHsBindLR GhcTc GhcTc -> [PredType]
#if __GLASGOW_HASKELL__ >= 900
absBinds dst (L src (FunBind w _ _ _))
  | dst `isSubspanOf` src
  = wrapper w
absBinds dst (L src (AbsBinds _ _ h _ _ z _))
#else
absBinds :: SrcSpan -> LHsBindLR GhcTc GhcTc -> [PredType]
absBinds SrcSpan
dst (L SrcSpan
src (AbsBinds XAbsBinds GhcTc GhcTc
_ [TyVar]
_ [TyVar]
h [ABExport GhcTc]
_ [TcEvBinds]
_ LHsBinds GhcTc
_ Bool
_))
#endif
  | SrcSpan
dst SrcSpan -> SrcSpan -> Bool
`isSubspanOf` SrcSpan
src
  = (TyVar -> PredType) -> [TyVar] -> [PredType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyVar -> PredType
idType [TyVar]
h
#if __GLASGOW_HASKELL__ >= 900
    <> foldMap (absBinds dst) z
#endif
absBinds SrcSpan
_ LHsBindLR GhcTc GhcTc
_ = []


------------------------------------------------------------------------------
-- | Extract evidence from 'HsWrapper's in scope
wrapperBinds ::  SrcSpan -> LHsExpr GhcTc -> [PredType]
#if __GLASGOW_HASKELL__ >= 900
wrapperBinds dst (L src (XExpr (WrapExpr (HsWrap h _))))
#else
wrapperBinds :: SrcSpan -> LHsExpr GhcTc -> [PredType]
wrapperBinds SrcSpan
dst (L SrcSpan
src (HsWrap XWrap GhcTc
_ HsWrapper
h HsExpr GhcTc
_))
#endif
  | SrcSpan
dst SrcSpan -> SrcSpan -> Bool
`isSubspanOf` SrcSpan
src
  = HsWrapper -> [PredType]
wrapper HsWrapper
h
wrapperBinds SrcSpan
_ LHsExpr GhcTc
_ = []


------------------------------------------------------------------------------
-- | Extract evidence from the 'ConPatOut's bound in this 'Match'.
matchBinds :: SrcSpan -> LMatch GhcTc (LHsExpr GhcTc) -> [PredType]
matchBinds :: SrcSpan -> LMatch GhcTc (LHsExpr GhcTc) -> [PredType]
matchBinds SrcSpan
dst (L SrcSpan
src (Match XCMatch GhcTc (LHsExpr GhcTc)
_ HsMatchContext (NameOrRdrName (IdP GhcTc))
_ [LPat GhcTc]
pats GRHSs GhcTc (LHsExpr GhcTc)
_))
  | SrcSpan
dst SrcSpan -> SrcSpan -> Bool
`isSubspanOf` SrcSpan
src
  = ([PredType] -> [PredType] -> [PredType])
-> GenericQ [PredType] -> [Located (Pat GhcTc)] -> [PredType]
forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything [PredType] -> [PredType] -> [PredType]
forall a. Semigroup a => a -> a -> a
(<>) ([PredType] -> (Pat GhcTc -> [PredType]) -> a -> [PredType]
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
mkQ [PredType]
forall a. Monoid a => a
mempty Pat GhcTc -> [PredType]
patBinds) [LPat GhcTc]
[Located (Pat GhcTc)]
pats
matchBinds SrcSpan
_ LMatch GhcTc (LHsExpr GhcTc)
_ = []


------------------------------------------------------------------------------
-- | Extract evidence from a 'ConPatOut'.
patBinds ::  Pat GhcTc -> [PredType]
#if __GLASGOW_HASKELL__ >= 900
patBinds (ConPat{ pat_con_ext = ConPatTc { cpt_dicts = dicts }})
#else
patBinds :: Pat GhcTc -> [PredType]
patBinds (ConPatOut { pat_dicts :: forall p. Pat p -> [TyVar]
pat_dicts = [TyVar]
dicts })
#endif
  = (TyVar -> PredType) -> [TyVar] -> [PredType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyVar -> PredType
idType [TyVar]
dicts
patBinds Pat GhcTc
_ = []


------------------------------------------------------------------------------
-- | Extract the types of the evidence bindings in scope.
wrapper ::  HsWrapper -> [PredType]
wrapper :: HsWrapper -> [PredType]
wrapper (WpCompose HsWrapper
h HsWrapper
h2) = HsWrapper -> [PredType]
wrapper HsWrapper
h [PredType] -> [PredType] -> [PredType]
forall a. Semigroup a => a -> a -> a
<> HsWrapper -> [PredType]
wrapper HsWrapper
h2
wrapper (WpEvLam TyVar
v) = [TyVar -> PredType
idType TyVar
v]
wrapper HsWrapper
_ = []