Using refined data types in separate modules

[Michael Thomas]

I have a question regarding the use of refined data types with liquid haskell.

In one module, I have defined the type MolecularFormula as-

{-@
data MolecularFormula = MolecularFormula {
    getMolecularFormula :: Map ElementSymbol Pos }
@-}
data MolecularFormula = MolecularFormula {
    getMolecularFormula :: Map ElementSymbol Int }
        deriving (Show, Read, Eq, Ord)

In the same module, I put the following definition -

benzene = MolecularFormula {getMolecularFormula = fromList [(H,6),(C,-6)]}

Using the command "stack exec liquid src/Isotope/Base.hs", I get "Error: Liquid Type Mismatch". Great! Liquid haskell has stopped me from doing something stupid. However, if I put the same benzene definition in a separate module, QuasiLiquid, running the command "stack exec liquid src/Isotope/QuasiLiquid.hs" gives the result "SAFE". This is not what I was expecting. Is there something I am doing wrong? I would really like the refined data type to still have the same restrictions when used in separate modules/libraries.

[Niki Vazou]

`liquid` seems to totally ignore your specifications. Run liquid inside the `src` directory: 

    cd src

    stack exec liquid Isotope/QuasiLiquid.hs

Let me know if this works!

Best, 

--
You received this message because you are subscribed to the Google Groups "liquidhaskell" group.
To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskel...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--

Niki Vazou

[Michael Thomas]

That did the trick. Thanks a lot.