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 :: (PPrint a, Expand a, Qualify a) => Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a

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

When expanding, it's important we pass around a BareRTEnv where the type aliases have been qualified as well. This is subtle, see for example T1761. In that test, we had a type alias "OneTyAlias a = {v:a | oneFunPred v}" where "oneFunPred" was marked inline. However, inlining couldn't happen because the BareRTEnv had an entry for "T1761.oneFunPred", so the relevant expansion of "oneFunPred" couldn't happen. This was because the type alias entry inside BareRTEnv mentioned the tuple ("OneTyAlias", "{v:a | oneFunPred v}") but the snd element needed to be qualified as well, before trying to expand anything.

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 -> Lookup LocSpecType

specExpandType :: BareRTEnv -> LocSpecType -> LocSpecType

Re-exported for data-constructors

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