{-# LANGUAGE FlexibleContexts         #-}


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

import           Prelude                               hiding (error)

import           Liquid.GHC.API       as Ghc  hiding (Located, get, showPpr)

import           Control.Monad                         (zipWithM_)
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 Language.Fixpoint.Types as F
import           Language.Haskell.Liquid.GHC.Misc
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Types.RType
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

-}

-------------------------------------------------------------------------------
-- Renaming Type Variables in Haskell Signatures ------------------------------
-------------------------------------------------------------------------------
runMapTyVars :: Bool -> Type -> SpecType -> (PJ.Doc -> PJ.Doc -> Error) -> Either Error MapTyVarST
runMapTyVars :: Bool
-> Type
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> (Doc -> Doc -> Error)
-> Either Error MapTyVarST
runMapTyVars Bool
allowTC Type
τ RTypeBV Symbol Symbol RTyCon RTyVar RReft
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 (Bool
-> Type
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ RTypeBV Symbol Symbol RTyCon RTyVar RReft
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 :: Bool -> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars :: Bool
-> Type
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC (FunTy { ft_arg :: Type -> Type
ft_arg = Type
τ, ft_res :: Type -> Type
ft_res = Type
τ'}) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
  | Type -> Bool
isErasable Type
τ
  = Bool
-> Type
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ' RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
  where isErasable :: Type -> Bool
isErasable = if Bool
allowTC then Type -> Bool
isEmbeddedDictType else Type -> Bool
isClassPred
mapTyVars Bool
allowTC (FunTy { ft_arg :: Type -> Type
ft_arg = Type
τ, ft_res :: Type -> Type
ft_res = Type
τ'}) (RFun Symbol
_ RFInfo
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RTypeBV Symbol Symbol RTyCon RTyVar RReft
t' RReft
_)
   = Bool
-> Type
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t StateT MapTyVarST (Either Error) ()
-> StateT MapTyVarST (Either Error) ()
-> StateT MapTyVarST (Either Error) ()
forall a b.
StateT MapTyVarST (Either Error) a
-> StateT MapTyVarST (Either Error) b
-> StateT MapTyVarST (Either Error) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool
-> Type
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ' RTypeBV Symbol Symbol RTyCon RTyVar RReft
t'
mapTyVars Bool
allowTC Type
τ (RAllT RTVUBV Symbol Symbol RTyCon RTyVar
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RReft
_)
  = Bool
-> Type
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
mapTyVars Bool
allowTC (TyConApp TyCon
_ [Type]
τs) (RApp RTyCon
_ [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts [RTPropBV Symbol Symbol RTyCon RTyVar RReft]
_ RReft
_)
   = (Type
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> StateT MapTyVarST (Either Error) ())
-> [Type]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> StateT MapTyVarST (Either Error) ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (Bool
-> Type
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC) [Type]
τs ([Type]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
matchKindArgs' [Type]
τs [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts)
mapTyVars Bool
_ (TyVarTy Var
α) (RVar RTyVar
a RReft
_)
   = do s  <- StateT MapTyVarST (Either Error) MapTyVarST
forall s (m :: * -> *). MonadState s m => m s
get
        s' <- mapTyRVar α a s
        put s'
mapTyVars Bool
allowTC Type
τ (RAllP PVUBV Symbol Symbol RTyCon RTyVar
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
  = Bool
-> Type
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
mapTyVars Bool
allowTC Type
τ (RAllE Symbol
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
  = Bool
-> Type
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
mapTyVars Bool
allowTC Type
τ (RRTy [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
_ RReft
_ Oblig
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
  = Bool
-> Type
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
mapTyVars Bool
allowTC Type
τ (REx Symbol
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
  = Bool
-> Type
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
mapTyVars Bool
_ Type
_ (RExprArg Located (ExprBV Symbol Symbol)
_)
  = () -> StateT MapTyVarST (Either Error) ()
forall a. a -> StateT MapTyVarST (Either Error) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
mapTyVars Bool
allowTC (AppTy Type
τ Type
τ') (RAppTy RTypeBV Symbol Symbol RTyCon RTyVar RReft
t RTypeBV Symbol Symbol RTyCon RTyVar RReft
t' RReft
_)
  = do Bool
-> Type
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
       Bool
-> Type
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ' RTypeBV Symbol Symbol RTyCon RTyVar RReft
t'
mapTyVars Bool
_ Type
_ (RHole RReft
_)
  = () -> StateT MapTyVarST (Either Error) ()
forall a. a -> StateT MapTyVarST (Either Error) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
mapTyVars Bool
_ Type
k RTypeBV Symbol Symbol RTyCon RTyVar RReft
_ | Type -> Bool
isKind Type
k
  = () -> StateT MapTyVarST (Either Error) ()
forall a. a -> StateT MapTyVarST (Either Error) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
mapTyVars Bool
allowTC (ForAllTy ForAllTyBinder
_ Type
τ) RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
  = Bool
-> Type
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
mapTyVars Bool
_ Type
hsT RTypeBV Symbol Symbol RTyCon RTyVar RReft
lqT
  = do err <- (MapTyVarST -> Doc -> Doc -> Error)
-> StateT MapTyVarST (Either Error) (Doc -> Doc -> Error)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets MapTyVarST -> Doc -> Doc -> Error
errmsg
       throwError (err (F.pprint hsT) (F.pprint lqT))

isKind :: Kind -> Bool
isKind :: Type -> Bool
isKind Type
k = Type -> Bool
isTYPEorCONSTRAINT Type
k -- TODO:GHC-863 isStarKind k --  typeKind k
          Bool -> Bool -> Bool
|| case Type
k of
                TyVarTy Var
kk -> Var -> Type
varType Var
kk Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
Ghc.liftedTypeKind
                Type
_ -> Bool
False

mapTyRVar :: MonadError Error m
          => Var -> RTyVar -> MapTyVarST -> m MapTyVarST
mapTyRVar :: forall (m :: * -> *).
MonadError Error m =>
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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return MapTyVarST
s
              | Bool
otherwise -> Error -> m MapTyVarST
forall a. Error -> m a
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 a. a -> m a
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]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
matchKindArgs' [Type]
ts1' = [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall a. [a] -> [a]
reverse ([RTypeBV Symbol Symbol RTyCon RTyVar RReft]
 -> [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
-> ([RTypeBV Symbol Symbol RTyCon RTyVar RReft]
    -> [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
go ([Type] -> [Type]
forall a. [a] -> [a]
reverse [Type]
ts1') ([RTypeBV Symbol Symbol RTyCon RTyVar RReft]
 -> [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
-> ([RTypeBV Symbol Symbol RTyCon RTyVar RReft]
    -> [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall a. [a] -> [a]
reverse
  where
    go :: [Type]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
go (Type
_:[Type]
ts1) (RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2:[RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts2) = RTypeBV Symbol Symbol RTyCon RTyVar RReft
t2RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall a. a -> [a] -> [a]
:[Type]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
go [Type]
ts1 [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
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 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r. IsReft r => Type -> RRType r
ofType (Type -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> [Type] -> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts) :: [SpecType]
    go [Type]
_       [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts       = [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts


matchKindArgs :: [SpecType] -> [SpecType] -> [SpecType]
matchKindArgs :: [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
matchKindArgs [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts1' = [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall a. [a] -> [a]
reverse ([RTypeBV Symbol Symbol RTyCon RTyVar RReft]
 -> [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
-> ([RTypeBV Symbol Symbol RTyCon RTyVar RReft]
    -> [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall {a}. [a] -> [a] -> [a]
go ([RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall a. [a] -> [a]
reverse [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
ts1') ([RTypeBV Symbol Symbol RTyCon RTyVar RReft]
 -> [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
-> ([RTypeBV Symbol Symbol RTyCon RTyVar RReft]
    -> [RTypeBV Symbol Symbol RTyCon RTyVar RReft])
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
forall a. [a] -> [a]
reverse
  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 -> ExprBV Symbol Symbol
mkVarExpr Var
v
  | Var -> Bool
isFunVar Var
v = Located Symbol -> [ExprBV Symbol Symbol] -> ExprBV Symbol Symbol
forall v b. Located v -> [ExprBV b v] -> ExprBV b v
F.mkEApp (Var -> Located Symbol
varFunSymbol Var
v) []
  | Bool
otherwise  = Var -> ExprBV Symbol Symbol
forall a. Symbolic a => a -> ExprBV Symbol Symbol
F.eVar Var
v -- EVar (symbol v)

varFunSymbol :: Id -> Located F.Symbol
varFunSymbol :: Var -> Located Symbol
varFunSymbol = Symbol -> Located Symbol
forall a. a -> Located a
dummyLoc (Symbol -> Located Symbol)
-> (Var -> Symbol) -> Var -> Located Symbol
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 a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
αs) Bool -> Bool -> Bool
&& Maybe (FunTyFlag, Type, Type, Type) -> Bool
forall a. Maybe a -> Bool
Mb.isNothing Maybe (FunTyFlag, Type, Type, Type)
tf
  where
    ([Var]
αs, Type
t)  = Type -> ([Var], Type)
splitForAllTyCoVars (Type -> ([Var], Type)) -> Type -> ([Var], Type)
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
v
    tf :: Maybe (FunTyFlag, Type, Type, Type)
tf       = Type -> Maybe (FunTyFlag, Type, 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 :: forall s t. [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 (([Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== Var -> [Char]
forall a. Outputable a => a -> [Char]
showPpr Var
v) ([Char] -> Bool) -> (Var -> [Char]) -> Var -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> [Char]
forall a. Outputable a => a -> [Char]
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
. [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Char] -> Symbol) -> (Var -> [Char]) -> Var -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
forall a. Outputable a => a -> [Char]
showPpr (Name -> [Char]) -> (Var -> Name) -> Var -> [Char]
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 ForAllTyBinder
_ Type
t) = Type -> Bool
hasBoolResult Type
t
hasBoolResult (FunTy { ft_res :: Type -> Type
ft_res = Type
t} )    | HasCallStack => Type -> Type -> Bool
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