Question: how are specs communicated between modules?

[gergoerdi]

I'm looking for an explanation of how LH manages the inter-module flow of information.

For example, suppose I have one module that looks like this:

module Liquid.Prelude where

{-@
embed Bool as bool
assume True  :: {v:Bool | v     }
assume False :: {v:Bool | (~ v) }
@-}

and another one that looks like this:

{-# LANGUAGE LambdaCase #-}
module Liquid.Hello where

import Liquid.Prelude

{-@ foo :: x:Bool -> { v:Bool | x || v } @-}
foo :: Bool -> Bool
foo = \case
    True -> False
    False -> True

For LH to check this second module, it has to have access to the embedding of Bool as the logic type from the first module. How does that work / how is that supposed to work?

My initial suspicion is that everything is put into the typechecked module in serialiseSpec, but then that should mean that anything that works with ModIfaces built from typechecked modules should work. The motivation for my question is that I have a program that uses the GHC API (instead of the GHC executable) to compile Haskell(ish) programs, and the above example fails with:

Source error while processing module Liquid.Hello:
  Liquid.Hello:6:12: error:
      Illegal type specification for `Liquid.Hello.foo`
    Liquid.Hello.foo :: x:GHC.Types.Bool -> {v : GHC.Types.Bool | x
                                                                  || v}
    Sort Error in Refinement: {v : GHC.Types.Bool | x
                                                    || v}
    Expressions x should have bool sort, but has GHC.Types.Bool
    Just

(It does, of course, work when processed with real GHC and the vanilla LH plugin)

[gergoerdi]

Actually, turns out that Liquid.Prelude module doesn't work so well with vanilla LH/GHC either, see #2393...

[facundominguez]

As far as I understand, loadDependencies is getting the annotations from dependencies.

[gergoerdi]

As far as I understand, loadDependencies is getting the annotations from dependencies.

Thanks, this has been helpful. My problem was that when GHC builds the ModDetails that goes into the TypecheckedModule, the annotations are not copied from the TcGblEnv. So if you build a ModIface from that ModDetails, the annotations will be lost.

After copying manually the annotations from tcg_anns into md_anns before converting to ModIface, it seems to work now (modulo #2393 of course).