Specs not exported from preprocessed source code

[mboes]

Consider the following example, where the source for the A module is preprocessed with hsc2hs:

# A.hsc
module A where

{-@ type Foo = { v : Int | v = 5 } @-}

# B.hs
module B where

import A

{-@ foo :: Foo @-}
foo = 5

LH fails with the following error:

[1 of 2] Compiling A

**** LIQUID: SAFE (0 constraints checked) **************************************
[2 of 2] Compiling B
ghc: panic! (the 'impossible' happened)
  (GHC version 8.10.7:
	[src/B.hs:5:12-14 Unknown type constructor `Foo`
                     matchTyCon: Foo]

If A.hsc is renamed to A.hs instead, then everything works fine. This problem might be hsc2hs-specific, but I suspect it's a more general problem with preprocessed source code.

Version of LH used: 0.8.10.7 (latest release on Hackage at time of writing)

[facundominguez]

I can't reproduce in the latest version of LH from github. Also, the program needs to add a type signature for foo, otherwise GHC infers Integer instead of Int.

[mboes]

I'm not claiming that the code satisfies the spec, but I'm claiming that the spec is not made available to downstream modules. I can reproduce even with HEAD. See https://github.com/mboes/liquidhaskell-issue-2132.

[facundominguez]

I'm reproducing with the OPTIONS_GHC pragma.

# A.hsc
{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
module A where
{-@ type Foo = { v : Integer | v = 5 } @-}

# B.hs
{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
module B where
import A
{-@ foo :: Foo @-}
foo = 5

#hsctest.cabal
cabal-version:      2.4
name:               hsctest
version:            0.1
synopsis:           Test for LiquidHaskell + hsc2hs
build-type:         Simple

library
  exposed-modules:    A B

  build-depends:      base                 >= 4.11.1.0 && < 5,
                      liquidhaskell        == 0.9.8.1
  default-language:   Haskell98
  ghc-options:        -Wall

hsc2hs produces the following file

{-# LINE 1 "hsctest/A.hs" #-}
{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
module A where

{-@ type Foo = { v : Integer | v = 5 } @-}

Removing the LINE pragma causes the definition of Foo to be found.