LiquidHaskell: Resolution Pipeline

Something I forgot to mention in my last post is that, once we reach the LHNameResolution.hs module, the modules have already been parsed into a BareSpecParsed: a data type representing a parsed specification, with relevant information for its resolution.

Let us take a look at the resolveLHNames function. From its type signature alone, it’s already kind of scary:

resolveLHNames
  :: Config
  -> GHC.Module
  -> LocalVars
  -> GHC.ImportedMods
  -> GHC.GlobalRdrEnv
  -> BareSpecParsed
  -> TargetDependencies
  -> Either [Error] (BareSpec, LogicNameEnv, LogicMap)

I’ll do my best here to explain what is going on:

  • Config: this is a data type containing all the flags/configuration options passed to the plugin.
  • GHC.Module: the name of the module being resolved.
  • LocalVars: a structure containing maps from variable names to locations where variables with the same name have been declared, and to the actual location of the variable.
  • GHC.ImportedMods: the collection of modules imported in the current module.
  • GHC.GlobalRdrEnv: contains all the information about names in scope and, what they resolve to.
  • BareSpecParsed: as mentioned before, this contains the parsed specification.
  • TargetDependencies: a map from a serializable representation of a module to its lifted specification.
  • (BareSpec, LogicNameEnv, LogicMap): the return type on a successful result is made up of three pieces of data. The BareSpec is the specification after all names have been resolved; LogicNameEnv is a bidirectional mapping between symbols and resolved names; and LogicMap which maps names to their definitions.

I think it should be valuable to understand in better detail the resolveLHNames function. So, I will dedicate the rest of this post to that.

Phase 1: Type alias preparation

The first thing going on in the function is: lift $ fixExpressionArgsOfTypeAliases taliases $ resolveBoundVarsInTypeAliases bareSpec0. This will perform two things:

  1. resolveBoundVarsInTypeAliases: this function looks at the definition of a type alias in an LH spec and resolves the variables in the body of the definition which are bounded by a type argument.
  2. fixExpressionArgsOfTypeAliases: this makes the translation from Types to Expressions.

Consider the following example (taken from the code itself):

type Prop E = {v:_ | prop v = E}

-- Later used in:
Prop (Ev (plus n n))

The first step in this phase will identify that E in the definition of Prop is referring to E in Prop E. And the second step would be in charge of finding type alias usages and converting from types to expressions (using the exprArg function). In the example, Ev (plus n n) would be translated to an expression.

Phase 2: Names resolution

The next step is given by: lift $ mapMLocLHNames (\l -> (<$ l) <$> resolveLHName l) sp0. There are a few things to unpack here, but we can focus exclusively in the resolveLHName function, which is doing the heavy lifting.

This function will resolve names in a specification using the GHC.GlobalRdrEnv which I mentioned before. It will only ignore “logic names”, which are dealt with in the next phase. A logic name is a symbol that exists only in the LH specification, not in Haskell.

Phase 3: Field names resolution

Afterwards, this gets executed:

dataDecls <- lift $ mapM (mapDataDeclFieldNamesM resolveFieldLogicName) (dataDecls sp1)
let sp2 = sp1 {dataDecls}

I won’t pretend to understand it perfectly but, I believe the main thing here is that the code is resolving field names (as in, the ones we get when using record syntax). They must be resolved before resolving measures, because there might be some name collisions (according to the comments in the code).

Phase 4: Logic names resolution

In this final phase, LH will resolve the names of logic names.

let (inScopeEnv, logicNameEnv0, privateReflectNames) =
      makeLogicEnvs impMods thisModule sp2 dependencies

    lmap1 = lmap <> mkLogicMap (HM.fromList $
             [ (F.val $ lhNameToResolvedSymbol <$> k,
                (val <$> v) { lmVar = lhNameToResolvedSymbol <$> k })
             | (k,v) <- defines sp2 ])
sp3 <- lift $ fromBareSpecLHName <$>
            resolveLogicNames
              cfg
              thisModule
              inScopeEnv
              globalRdrEnv
              lmap1
              localVars
              logicNameEnv0
              privateReflectNames
              depsInlinesAndDefines
              sp2

This larger piece of code, but conceptually is not too complicated. The first two lines deal with the construction of the environment to perform the name resolution. Then, lmap1 is creating the LogicMap to be used (I already explained what a LogicMap is). Finally, LH will resolve every missing logic name in the module.

After this, some housekeeping takes place: errors are logged if any and the result to be returned is composed.

Some thoughts

By tracing the execution on the faulty example, I discovered that the error is taking place in phase 4; more precisely in the resolveLogicNames function.

Actually, I didn’t have to do all this exploration to pinpoint exactly where the error was being thrown; I could have obviously just greped the error message and find the location in seconds. But I will need some context if I want to solve the typeclass problem, so this was a good exercise.

I still have quite a lot to analyse. For instance, I should dive deeper into the resolveLogicNames function and also, I should figure out a way to print the maps/envs, so I am able to find out if typeclass methods are even processed at all, and how exactly they could be retrieved.

But I will write about that on the next post.