ucsd-progsys/liquidhaskell
Voir sur GitHubSpecs not exported from preprocessed source code
Open
#2 132 ouverte le 1 janv. 2023
good first issue
Métriques du dépôt
- Stars
- (1 306 stars)
- Métriques de merge PR
- (Merge moyen 2j 18h) (12 PRs mergées en 30 j)
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)