Language.Haskell.Liquid.Bare.Expand

This module has the code for applying refinement (and) type aliases and the pipeline for "cooking" a BareType into a SpecType. TODO: _only_ export makeRTEnv, cookSpecType and maybe qualifyExpand...

Create alias expansion environment

makeRTEnv :: Env -> ModName -> BareSpec -> ModSpecs -> LogicMap -> BareRTEnv

makeRTEnv initializes the env needed to expand refinements and types, that is, the below needs to be called *before* we use expand

Expand and Qualify

qualifyExpand :: (Expand a, Qualify a) => Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a

qualifyExpand first qualifies names so that we can successfully resolve them during expansion.

Converting BareType to SpecType

cookSpecType :: Env -> SigEnv -> ModName -> PlugTV Var -> LocBareType -> LocSpecType

cookSpecType is the central place where a BareType gets processed, in multiple steps, into a SpecType. See [NOTE:Cooking-SpecType] for details of each of the individual steps.

cookSpecTypeE :: Env -> SigEnv -> ModName -> PlugTV Var -> LocBareType -> Either UserError LocSpecType

specExpandType :: BareRTEnv -> LocSpecType -> LocSpecType

Re-exported for data-constructors

plugHoles :: SigEnv -> ModName -> PlugTV Var -> LocSpecType -> LocSpecType