Language.Haskell.Liquid.Types.Fresh

Documentation

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

Minimal complete definition

fresh

Methods

fresh :: m a

true :: a -> m a

refresh :: a -> m a

Instances

Freshable m Integer => Freshable m Strata

Methods

fresh :: m Strata

true :: Strata -> m Strata

refresh :: Strata -> m Strata

Freshable m Integer => Freshable m RReft

Methods

fresh :: m RReft

true :: RReft -> m RReft

refresh :: RReft -> m RReft

(Freshable m Integer, Monad m, Applicative m) => Freshable m Reft

Methods

fresh :: m Reft

true :: Reft -> m Reft

refresh :: Reft -> m Reft

(Freshable m Integer, Monad m, Applicative m) => Freshable m Expr

Methods

fresh :: m Expr

true :: Expr -> m Expr

refresh :: Expr -> m Expr

(Freshable m Integer, Monad m, Applicative m) => Freshable m Symbol

Methods

fresh :: m Symbol

true :: Symbol -> m Symbol

refresh :: Symbol -> m Symbol

Freshable BareM Integer

Methods

fresh :: BareM Integer

true :: Integer -> BareM Integer

refresh :: Integer -> BareM Integer

(Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r)

Methods

fresh :: m (RRType r)

true :: RRType r -> m (RRType r)

refresh :: RRType r -> m (RRType r)

(Freshable m Integer, Monad m, Applicative m) => Freshable m [Expr]

Methods

fresh :: m [Expr]

true :: [Expr] -> m [Expr]

refresh :: [Expr] -> m [Expr]

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

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

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

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

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