{-# LANGUAGE FlexibleContexts         #-}

module Language.Haskell.Liquid.Bare.Misc 
  ( freeSymbols
  , joinVar
  , mkVarExpr
  , vmap
  , runMapTyVars
  , matchKindArgs
  , symbolRTyVar
  , simpleSymbolVar
  , hasBoolResult
  , isKind
  ) where

import           Prelude                               hiding (error)

import           Language.Haskell.Liquid.GHC.API       as Ghc  hiding (Located)

import           Control.Monad.Except                  (MonadError, throwError)
import           Control.Monad.State
import qualified Data.Maybe                            as Mb --(fromMaybe, isNothing)

import qualified Text.PrettyPrint.HughesPJ             as PJ 
import qualified Data.List                             as L
import qualified Data.HashMap.Strict                   as M
import           Language.Fixpoint.Misc                as Misc -- (singleton, sortNub)
import qualified Language.Fixpoint.Types as F
import           Language.Haskell.Liquid.GHC.Misc
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Types.Types

-- import           Language.Haskell.Liquid.Bare.Env

-- import           Language.Haskell.Liquid.WiredIn       (dcPrefix)


-- TODO: This is where unsorted stuff is for now. Find proper places for what follows.

{- 
-- WTF does this function do?
makeSymbols :: (Id -> Bool) -> [Id] -> [F.Symbol] -> BareM [(F.Symbol, Var)]
makeSymbols f vs xs
  = do svs <- M.toList <$> gets varEnv
       return $ L.nub ([ (x,v') | (x,v) <- svs, x `elem` xs, let (v',_,_) = joinVar vs (v,x,x)]
                   ++  [ (F.symbol v, v) | v <- vs, f v, isDataConId v, hasBasicArgs $ varType v ])
    where
      -- arguments should be basic so that autogenerated singleton types are well formed
      hasBasicArgs (ForAllTy _ t) = hasBasicArgs t
      hasBasicArgs (FunTy _ tx t)   = isBaseTy tx && hasBasicArgs t
      hasBasicArgs _              = True

-} 

freeSymbols :: (F.Reftable r, F.Reftable r1, F.Reftable r2, TyConable c, TyConable c1, TyConable c2)
            => [F.Symbol]
            -> [(a1, Located (RType c2 tv2 r2))]
            -> [(a, Located (RType c1 tv1 r1))]
            -> [(Located (RType c tv r))]
            -> [LocSymbol]
freeSymbols :: [Symbol]
-> [(a1, Located (RType c2 tv2 r2))]
-> [(a, Located (RType c1 tv1 r1))]
-> [Located (RType c tv r)]
-> [LocSymbol]
freeSymbols [Symbol]
xs' [(a1, Located (RType c2 tv2 r2))]
xts [(a, Located (RType c1 tv1 r1))]
yts [Located (RType c tv r)]
ivs =  [ LocSymbol
lx | LocSymbol
lx <- [LocSymbol] -> [LocSymbol]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([LocSymbol] -> [LocSymbol]) -> [LocSymbol] -> [LocSymbol]
forall a b. (a -> b) -> a -> b
$ [LocSymbol]
zs [LocSymbol] -> [LocSymbol] -> [LocSymbol]
forall a. [a] -> [a] -> [a]
++ [LocSymbol]
zs' [LocSymbol] -> [LocSymbol] -> [LocSymbol]
forall a. [a] -> [a] -> [a]
++ [LocSymbol]
zs'' , Bool -> Bool
not (Symbol -> HashMap Symbol () -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
lx) HashMap Symbol ()
knownM) ]
  where
    knownM :: HashMap Symbol ()
knownM                  = [(Symbol, ())] -> HashMap Symbol ()
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (Symbol
x, ()) | Symbol
x <- [Symbol]
xs' ]
    zs :: [LocSymbol]
zs                      = (Located (RType c2 tv2 r2) -> [LocSymbol])
-> [Located (RType c2 tv2 r2)] -> [LocSymbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Located (RType c2 tv2 r2) -> [LocSymbol]
forall r c tv.
(Reftable r, TyConable c) =>
Located (RType c tv r) -> [LocSymbol]
freeSyms ((a1, Located (RType c2 tv2 r2)) -> Located (RType c2 tv2 r2)
forall a b. (a, b) -> b
snd ((a1, Located (RType c2 tv2 r2)) -> Located (RType c2 tv2 r2))
-> [(a1, Located (RType c2 tv2 r2))] -> [Located (RType c2 tv2 r2)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a1, Located (RType c2 tv2 r2))]
xts)
    zs' :: [LocSymbol]
zs'                     = (Located (RType c1 tv1 r1) -> [LocSymbol])
-> [Located (RType c1 tv1 r1)] -> [LocSymbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Located (RType c1 tv1 r1) -> [LocSymbol]
forall r c tv.
(Reftable r, TyConable c) =>
Located (RType c tv r) -> [LocSymbol]
freeSyms ((a, Located (RType c1 tv1 r1)) -> Located (RType c1 tv1 r1)
forall a b. (a, b) -> b
snd ((a, Located (RType c1 tv1 r1)) -> Located (RType c1 tv1 r1))
-> [(a, Located (RType c1 tv1 r1))] -> [Located (RType c1 tv1 r1)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, Located (RType c1 tv1 r1))]
yts)
    zs'' :: [LocSymbol]
zs''                    = (Located (RType c tv r) -> [LocSymbol])
-> [Located (RType c tv r)] -> [LocSymbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Located (RType c tv r) -> [LocSymbol]
forall r c tv.
(Reftable r, TyConable c) =>
Located (RType c tv r) -> [LocSymbol]
freeSyms [Located (RType c tv r)]
ivs



freeSyms :: (F.Reftable r, TyConable c) => Located (RType c tv r) -> [LocSymbol]
freeSyms :: Located (RType c tv r) -> [LocSymbol]
freeSyms Located (RType c tv r)
ty    = [ Located (RType c tv r) -> Symbol -> LocSymbol
forall l b. Loc l => l -> b -> Located b
F.atLoc Located (RType c tv r)
ty Symbol
x | Symbol
x <- [Symbol]
tySyms ]
  where
    tySyms :: [Symbol]
tySyms     = [Symbol] -> [Symbol]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ [[Symbol]] -> [Symbol]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Symbol]] -> [Symbol]) -> [[Symbol]] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ (Symbol -> RType c tv r -> Bool)
-> Bool
-> (c -> [RType c tv r] -> [(Symbol, ())])
-> (RTVar tv (RType c tv ()) -> [(Symbol, ())])
-> (RType c tv r -> ())
-> (SEnv ()
    -> Maybe (RType c tv r) -> r -> [[Symbol]] -> [[Symbol]])
-> (PVar (RType c tv ()) -> SEnv () -> SEnv ())
-> SEnv ()
-> [[Symbol]]
-> RType c tv r
-> [[Symbol]]
forall r c tv a b.
(Reftable r, TyConable c) =>
(Symbol -> RType c tv r -> Bool)
-> Bool
-> (c -> [RType c tv r] -> [(Symbol, a)])
-> (RTVar tv (RType c tv ()) -> [(Symbol, a)])
-> (RType c tv r -> a)
-> (SEnv a -> Maybe (RType c tv r) -> r -> b -> b)
-> (PVar (RType c tv ()) -> SEnv a -> SEnv a)
-> SEnv a
-> b
-> RType c tv r
-> b
efoldReft (\Symbol
_ RType c tv r
_ -> Bool
True) Bool
False (\c
_ [RType c tv r]
_ -> []) (\RTVar tv (RType c tv ())
_ -> []) (() -> RType c tv r -> ()
forall a b. a -> b -> a
const ()) SEnv () -> Maybe (RType c tv r) -> r -> [[Symbol]] -> [[Symbol]]
forall r a p.
Reftable r =>
SEnv a -> p -> r -> [[Symbol]] -> [[Symbol]]
f ((SEnv () -> SEnv ()) -> PVar (RType c tv ()) -> SEnv () -> SEnv ()
forall a b. a -> b -> a
const SEnv () -> SEnv ()
forall a. a -> a
id) SEnv ()
forall a. SEnv a
F.emptySEnv [] (Located (RType c tv r) -> RType c tv r
forall a. Located a -> a
val Located (RType c tv r)
ty)
    f :: SEnv a -> p -> r -> [[Symbol]] -> [[Symbol]]
f SEnv a
γ p
_ r
r [[Symbol]]
xs = let F.Reft (Symbol
v, Expr
_) = r -> Reft
forall r. Reftable r => r -> Reft
F.toReft r
r in
                 [ Symbol
x | Symbol
x <- r -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms r
r, Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= Symbol
v, Bool -> Bool
not (Symbol
x Symbol -> SEnv a -> Bool
forall a. Symbol -> SEnv a -> Bool
`F.memberSEnv` SEnv a
γ)] [Symbol] -> [[Symbol]] -> [[Symbol]]
forall a. a -> [a] -> [a]
: [[Symbol]]
xs

-------------------------------------------------------------------------------
-- Renaming Type Variables in Haskell Signatures ------------------------------
-------------------------------------------------------------------------------
runMapTyVars :: Type -> SpecType -> (PJ.Doc -> PJ.Doc -> Error) -> Either Error MapTyVarST
runMapTyVars :: Type
-> SpecType -> (Doc -> Doc -> Error) -> Either Error MapTyVarST
runMapTyVars Type
τ SpecType
t Doc -> Doc -> Error
err = StateT MapTyVarST (Either Error) ()
-> MapTyVarST -> Either Error MapTyVarST
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Type
τ SpecType
t) ([(Var, RTyVar)] -> (Doc -> Doc -> Error) -> MapTyVarST
MTVST [] Doc -> Doc -> Error
err) 

data MapTyVarST = MTVST
  { MapTyVarST -> [(Var, RTyVar)]
vmap   :: [(Var, RTyVar)]
  , MapTyVarST -> Doc -> Doc -> Error
errmsg :: PJ.Doc -> PJ.Doc -> Error
  }

mapTyVars :: Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars :: Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Type
t (RImpF Symbol
_ SpecType
_ SpecType
t' RReft
_)
   = Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Type
t SpecType
t'
mapTyVars (FunTy { ft_arg :: Type -> Type
ft_arg = Type
τ, ft_res :: Type -> Type
ft_res = Type
τ'}) SpecType
t 
  | Type -> Bool
isClassPred Type
τ
  = Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Type
τ' SpecType
t
mapTyVars (FunTy { ft_arg :: Type -> Type
ft_arg = Type
τ, ft_res :: Type -> Type
ft_res = Type
τ'}) (RFun Symbol
_ SpecType
t SpecType
t' RReft
_)
   = Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Type
τ SpecType
t StateT MapTyVarST (Either Error) ()
-> StateT MapTyVarST (Either Error) ()
-> StateT MapTyVarST (Either Error) ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Type
τ' SpecType
t'
mapTyVars Type
τ (RAllT RTVU RTyCon RTyVar
_ SpecType
t RReft
_)
  = Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Type
τ SpecType
t
mapTyVars (TyConApp TyCon
_ [Type]
τs) (RApp RTyCon
_ [SpecType]
ts [RTProp RTyCon RTyVar RReft]
_ RReft
_)
   = (Type -> SpecType -> StateT MapTyVarST (Either Error) ())
-> [Type] -> [SpecType] -> StateT MapTyVarST (Either Error) ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars [Type]
τs ([Type] -> [SpecType] -> [SpecType]
matchKindArgs' [Type]
τs [SpecType]
ts)
mapTyVars (TyVarTy Var
α) (RVar RTyVar
a RReft
_)
   = do MapTyVarST
s  <- StateT MapTyVarST (Either Error) MapTyVarST
forall s (m :: * -> *). MonadState s m => m s
get
        MapTyVarST
s' <- Var
-> RTyVar
-> MapTyVarST
-> StateT MapTyVarST (Either Error) MapTyVarST
forall (m :: * -> *).
MonadError Error m =>
Var -> RTyVar -> MapTyVarST -> m MapTyVarST
mapTyRVar Var
α RTyVar
a MapTyVarST
s
        MapTyVarST -> StateT MapTyVarST (Either Error) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put MapTyVarST
s'
mapTyVars Type
τ (RAllP PVU RTyCon RTyVar
_ SpecType
t)
  = Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Type
τ SpecType
t
mapTyVars Type
τ (RAllE Symbol
_ SpecType
_ SpecType
t)
  = Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Type
τ SpecType
t
mapTyVars Type
τ (RRTy [(Symbol, SpecType)]
_ RReft
_ Oblig
_ SpecType
t)
  = Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Type
τ SpecType
t
mapTyVars Type
τ (REx Symbol
_ SpecType
_ SpecType
t)
  = Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Type
τ SpecType
t
mapTyVars Type
_ (RExprArg Located Expr
_)
  = () -> StateT MapTyVarST (Either Error) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
mapTyVars (AppTy Type
τ Type
τ') (RAppTy SpecType
t SpecType
t' RReft
_)
  = do  Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Type
τ SpecType
t
        Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Type
τ' SpecType
t'
mapTyVars Type
_ (RHole RReft
_)
  = () -> StateT MapTyVarST (Either Error) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
mapTyVars Type
k SpecType
_ | Type -> Bool
isKind Type
k
  = () -> StateT MapTyVarST (Either Error) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
mapTyVars (ForAllTy TyCoVarBinder
_ Type
τ) SpecType
t
  = Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Type
τ SpecType
t
mapTyVars Type
hsT SpecType
lqT
  = do Doc -> Doc -> Error
err <- MapTyVarST -> Doc -> Doc -> Error
errmsg (MapTyVarST -> Doc -> Doc -> Error)
-> StateT MapTyVarST (Either Error) MapTyVarST
-> StateT MapTyVarST (Either Error) (Doc -> Doc -> Error)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT MapTyVarST (Either Error) MapTyVarST
forall s (m :: * -> *). MonadState s m => m s
get
       Error -> StateT MapTyVarST (Either Error) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Doc -> Doc -> Error
err (Type -> Doc
forall a. PPrint a => a -> Doc
F.pprint Type
hsT) (SpecType -> Doc
forall a. PPrint a => a -> Doc
F.pprint SpecType
lqT)) 

isKind :: Kind -> Bool
isKind :: Type -> Bool
isKind = Type -> Bool
classifiesTypeWithValues -- TODO:GHC-863 isStarKind k --  typeKind k


mapTyRVar :: MonadError Error m
          => Var -> RTyVar -> MapTyVarST -> m MapTyVarST
mapTyRVar :: Var -> RTyVar -> MapTyVarST -> m MapTyVarST
mapTyRVar Var
α RTyVar
a s :: MapTyVarST
s@(MTVST [(Var, RTyVar)]
αas Doc -> Doc -> Error
err)
  = case Var -> [(Var, RTyVar)] -> Maybe RTyVar
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
α [(Var, RTyVar)]
αas of
      Just RTyVar
a' | RTyVar
a RTyVar -> RTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== RTyVar
a'   -> MapTyVarST -> m MapTyVarST
forall (m :: * -> *) a. Monad m => a -> m a
return MapTyVarST
s
              | Bool
otherwise -> Error -> m MapTyVarST
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Doc -> Doc -> Error
err (RTyVar -> Doc
forall a. PPrint a => a -> Doc
F.pprint RTyVar
a) (RTyVar -> Doc
forall a. PPrint a => a -> Doc
F.pprint RTyVar
a'))
      Maybe RTyVar
Nothing             -> MapTyVarST -> m MapTyVarST
forall (m :: * -> *) a. Monad m => a -> m a
return (MapTyVarST -> m MapTyVarST) -> MapTyVarST -> m MapTyVarST
forall a b. (a -> b) -> a -> b
$ [(Var, RTyVar)] -> (Doc -> Doc -> Error) -> MapTyVarST
MTVST ((Var
α,RTyVar
a)(Var, RTyVar) -> [(Var, RTyVar)] -> [(Var, RTyVar)]
forall a. a -> [a] -> [a]
:[(Var, RTyVar)]
αas) Doc -> Doc -> Error
err

matchKindArgs' :: [Type] -> [SpecType] -> [SpecType]
matchKindArgs' :: [Type] -> [SpecType] -> [SpecType]
matchKindArgs' [Type]
ts1 [SpecType]
ts2 = [SpecType] -> [SpecType]
forall a. [a] -> [a]
reverse ([SpecType] -> [SpecType]) -> [SpecType] -> [SpecType]
forall a b. (a -> b) -> a -> b
$ [Type] -> [SpecType] -> [SpecType]
go ([Type] -> [Type]
forall a. [a] -> [a]
reverse [Type]
ts1) ([SpecType] -> [SpecType]
forall a. [a] -> [a]
reverse [SpecType]
ts2)
  where
    go :: [Type] -> [SpecType] -> [SpecType]
go (Type
_:[Type]
ts1) (SpecType
t2:[SpecType]
ts2) = SpecType
t2SpecType -> [SpecType] -> [SpecType]
forall a. a -> [a] -> [a]
:[Type] -> [SpecType] -> [SpecType]
go [Type]
ts1 [SpecType]
ts2
    go [Type]
ts      []       | (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
isKind [Type]
ts
                        = (Type -> SpecType
forall r. Monoid r => Type -> RRType r
ofType (Type -> SpecType) -> [Type] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts) :: [SpecType]
    go [Type]
_       [SpecType]
ts       = [SpecType]
ts


matchKindArgs :: [SpecType] -> [SpecType] -> [SpecType]
matchKindArgs :: [SpecType] -> [SpecType] -> [SpecType]
matchKindArgs [SpecType]
ts1 [SpecType]
ts2 = [SpecType] -> [SpecType]
forall a. [a] -> [a]
reverse ([SpecType] -> [SpecType]) -> [SpecType] -> [SpecType]
forall a b. (a -> b) -> a -> b
$ [SpecType] -> [SpecType] -> [SpecType]
forall a. [a] -> [a] -> [a]
go ([SpecType] -> [SpecType]
forall a. [a] -> [a]
reverse [SpecType]
ts1) ([SpecType] -> [SpecType]
forall a. [a] -> [a]
reverse [SpecType]
ts2)
  where
    go :: [a] -> [a] -> [a]
go (a
_:[a]
ts1) (a
t2:[a]
ts2) = a
t2a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a] -> [a] -> [a]
go [a]
ts1 [a]
ts2
    go [a]
ts      []       = [a]
ts
    go [a]
_       [a]
ts       = [a]
ts

mkVarExpr :: Id -> F.Expr
mkVarExpr :: Var -> Expr
mkVarExpr Var
v
  | Var -> Bool
isFunVar Var
v = LocSymbol -> [Expr] -> Expr
F.mkEApp (Var -> LocSymbol
varFunSymbol Var
v) []
  | Bool
otherwise  = Var -> Expr
forall a. Symbolic a => a -> Expr
F.eVar Var
v -- EVar (symbol v)

varFunSymbol :: Id -> Located F.Symbol
varFunSymbol :: Var -> LocSymbol
varFunSymbol = Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (Symbol -> LocSymbol) -> (Var -> Symbol) -> Var -> LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (DataCon -> Symbol) -> (Var -> DataCon) -> Var -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> DataCon
idDataCon

isFunVar :: Id -> Bool
isFunVar :: Var -> Bool
isFunVar Var
v   = Var -> Bool
isDataConId Var
v Bool -> Bool -> Bool
&& Bool -> Bool
not ([Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
αs) Bool -> Bool -> Bool
&& Maybe (Type, Type) -> Bool
forall a. Maybe a -> Bool
Mb.isNothing Maybe (Type, Type)
tf
  where
    ([Var]
αs, Type
t)  = Type -> ([Var], Type)
splitForAllTys (Type -> ([Var], Type)) -> Type -> ([Var], Type)
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
v
    tf :: Maybe (Type, Type)
tf       = Type -> Maybe (Type, Type)
splitFunTy_maybe Type
t

-- the Vars we lookup in GHC don't always have the same tyvars as the Vars
-- we're given, so return the original var when possible.
-- see tests/pos/ResolvePred.hs for an example
joinVar :: [Var] -> (Var, s, t) -> (Var, s, t)
joinVar :: [Var] -> (Var, s, t) -> (Var, s, t)
joinVar [Var]
vs (Var
v,s
s,t
t) = case (Var -> Bool) -> [Var] -> Maybe Var
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Var -> String
forall a. Outputable a => a -> String
showPpr Var
v) (String -> Bool) -> (Var -> String) -> Var -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> String
forall a. Outputable a => a -> String
showPpr) [Var]
vs of
                       Just Var
v' -> (Var
v',s
s,t
t)
                       Maybe Var
Nothing -> (Var
v,s
s,t
t)

simpleSymbolVar :: Var -> F.Symbol
simpleSymbolVar :: Var -> Symbol
simpleSymbolVar  = Symbol -> Symbol
dropModuleNames (Symbol -> Symbol) -> (Var -> Symbol) -> Var -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (String -> Symbol) -> (Var -> String) -> Var -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
forall a. Outputable a => a -> String
showPpr (Name -> String) -> (Var -> Name) -> Var -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Name
forall a. NamedThing a => a -> Name
getName

hasBoolResult :: Type -> Bool
hasBoolResult :: Type -> Bool
hasBoolResult (ForAllTy TyCoVarBinder
_ Type
t) = Type -> Bool
hasBoolResult Type
t
hasBoolResult (FunTy { ft_res :: Type -> Type
ft_res = Type
t} )    | Type -> Type -> Bool
eqType Type
boolTy Type
t = Bool
True
hasBoolResult (FunTy { ft_res :: Type -> Type
ft_res = Type
t} )    = Type -> Bool
hasBoolResult Type
t
hasBoolResult Type
_              = Bool
False