Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Types.Fresh

Documentation

class (Applicative m, Monad m) => Freshable m a where Source #

Minimal complete definition

fresh

Methods

fresh :: m a Source #

true :: a -> m a Source #

refresh :: a -> m a Source #

Instances

Instances details

Freshable m Integer => Freshable m RReft Source #
Instance details Defined in Language.Haskell.Liquid.Types.Fresh Methods fresh :: m RReft Source # true :: RReft -> m RReft Source # refresh :: RReft -> m RReft Source #
(Freshable m Integer, Monad m, Applicative m) => Freshable m Reft Source #
Instance details Defined in Language.Haskell.Liquid.Types.Fresh Methods fresh :: m Reft Source # true :: Reft -> m Reft Source # refresh :: Reft -> m Reft Source #
(Freshable m Integer, Monad m, Applicative m) => Freshable m Expr Source #
Instance details Defined in Language.Haskell.Liquid.Types.Fresh Methods fresh :: m Expr Source # true :: Expr -> m Expr Source # refresh :: Expr -> m Expr Source #
(Freshable m Integer, Monad m, Applicative m) => Freshable m Symbol Source #
Instance details Defined in Language.Haskell.Liquid.Types.Fresh Methods fresh :: m Symbol Source # true :: Symbol -> m Symbol Source # refresh :: Symbol -> m Symbol Source #
Freshable CG Integer Source #	This is all hardwiring stuff to CG ----------------------------------------
Instance details Defined in Language.Haskell.Liquid.Constraint.Fresh Methods fresh :: CG Integer Source # true :: Integer -> CG Integer Source # refresh :: Integer -> CG Integer Source #
(Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Fresh Methods fresh :: m (RRType r) Source # true :: RRType r -> m (RRType r) Source # refresh :: RRType r -> m (RRType r) Source #
(Freshable m Integer, Monad m, Applicative m) => Freshable m [Expr] Source #
Instance details Defined in Language.Haskell.Liquid.Types.Fresh Methods fresh :: m [Expr] Source # true :: [Expr] -> m [Expr] Source # refresh :: [Expr] -> m [Expr] Source #

refreshTy :: FreshM m => SpecType -> m SpecType Source #

refreshVV :: FreshM m => SpecType -> m SpecType Source #

refreshArgs :: FreshM m => SpecType -> m SpecType Source #

refreshHoles :: (Symbolic t, Reftable r, TyConable c, Freshable f r) => [(t, RType c tv r)] -> f ([Symbol], [(t, RType c tv r)]) Source #

refreshArgsSub :: FreshM m => SpecType -> m (SpecType, Subst) Source #