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

NOTE:Family-Instance-Environment

For some reason, the usual lookup machinery (lookupGhcThing) refuses to properly lookup _imported_ names of family-instance data-constructors. e.g. see testsposExactGADT8.hs and testsposExactGADT9.hs; inside the latter, the lookupGhcThing fails to resolve the name of BlobXVal (but it works just fine when BlobXVal is a plain DataCon as in testsposExactGADT8a.hs To get around this hassle, we also save a map from _family instance_ DataCon-names to the corresponding family instance Tycon in the famEnv field of BareEnv. This map is *created* inside the function FIXME, and *used* inside the function FIXME.

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)