ucsd-progsys/liquidhaskell
Vedi su GitHubSpecs not exported from preprocessed source code
Open
#2132 aperta il 1 gen 2023
good first issue
Metriche repository
- Star
- (1306 star)
- Metriche merge PR
- (Merge medio 2g 18h) (12 PR mergiate in 30 g)
Descrizione
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)