ucsd-progsys/liquidhaskell
Ver no GitHubSpecs not exported from preprocessed source code
Open
#2.132 aberto em 1 de jan. de 2023
good first issue
Métricas do repositório
- Stars
- (1.306 stars)
- Métricas de merge de PR
- (Mesclagem média 2d 18h) (12 fundiu PRs em 30d)
Description
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)