8000 compare: unexpected RecIntersect (UnsafeIntersectId 478 478) · Issue #24 · jkoppel/ecta · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

compare: unexpected RecIntersect (UnsafeIntersectId 478 478) #24

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
Tritlo opened this issue Aug 5, 2023 · 11 comments
Open

compare: unexpected RecIntersect (UnsafeIntersectId 478 478) #24

Tritlo opened this issue Aug 5, 2023 · 11 comments

Comments

@Tritlo
Copy link
Collaborator
Tritlo commented Aug 5, 2023

I'm trying to use ecta via the ecta-plugin, but when I use it for Prelude it complains about

compare: unexpected RecIntersect (UnsafeIntersectId 478 478)

I've made a minimal reproduction here:

https://gist.github.com/Tritlo/405c85003401de9fb481841be7faa940

Of course the issue might be in the plugin itself, but it works for other cases.
I don't know enough about the inner workings of ecta to understand the issue here.
It seems like it is trying to intersect with itself? What does that mean, and what would be the right answer there

This is blocking integration into HLS (haskell/haskell-language-server#3159), so would be great if we could figure it out.
@jkoppel
Copy link
Owner
jkoppel commented Aug 8, 2023

@Tritlo I don't have a working setup of the plugin. Can you turn this into the actual calls to the ecta library?

@Tritlo
Copy link
Collaborator Author
Tritlo commented Aug 8, 2023

The cabal file in the gist installs the plugin, it's all in the stderr, no editor involvement.

@Tritlo
Copy link
Collaborator Author
Tritlo commented Aug 18, 2023

Seems fixed in https://github.com/sankalpgambh 8000 ir/ecta/tree/empty-mu-intersection-fix

@jkoppel
Copy link
Owner
jkoppel commented Aug 18, 2023

Awesome!

Sankalp, let's get this merged.

@Tritlo
Copy link
Collaborator Author
Tritlo commented Aug 18, 2023

Oh wait, it is still broken. The patch changes it from

compare: unexpected RecIntersect (UnsafeIntersectId 478 478)

to

compare: unexpected RecUnint 0

@sankalpgambhir
Copy link
sankalpgambhir commented Sep 24, 2023 •
edited
Loading

The RecUnInt issue seems to be different from the previous one. Extrapolating the previous fix to this case could (read will) break soundness, so it requires some more investigation.

With the patched ecta branch sankalpgambhir/ecta@3a78950 I don't see the same error (testing with Tritlo/ecta-plugin@8ab8b8c) (edit:) and using stack:

(TFun (TVar "a") (TVar "a"),[])
                        
/home/sankalp/projects/ecta/ecta-plugin/TestPlugin/Test.hs:12:5: error:
    • Found hole: _ :: a -> a
      Where: ‘a’ is a rigid type variable bound by
               the type signature for:
                 f :: forall a. a -> a
               at Test.hs:11:1-11
    • In the expression: _
      In an equation for ‘f’: f = _
    • Relevant bindings include f :: a -> a (bound at Test.hs:12:1)
      Valid hole fits include f :: a -> a (bound at Test.hs:12:1)
   |                    
12 | f = _              
   |

I'm not sure if the first line here is expected to be printed, but it looks like a possible substitute (\a -> a).

With Tritlo/ecta-plugin@d21399e:

/home/sankalp/projects/ecta/ecta-plugin/TestPlugin/Test.hs:11:9: error:
    • Found hole: _ :: [a] -> [a] -> Bool
      Where: ‘a’ is a rigid type variable bound by
               the type signature for:
                 equal :: forall a. Eq a => [a] -> [a] -> Bool
               at Test.hs:10:1-35
    • In the expression: _
      In an equation for ‘equal’: equal = _
    • Relevant bindings include
        equal :: [a] -> [a] -> Bool (bound at Test.hs:11:1)
      Constraints include Eq a (from Test.hs:10:1-35)
      Valid hole fits include
        equal :: [a] -> [a] -> Bool (bound at Test.hs:11:1)
        (==) :: forall a. Eq a => a -> a -> Bool
          with (==) @[a]
          (imported from ‘Prelude’ at Test.hs:6:48-55
           (and originally defined in ‘ghc-prim-0.6.1:GHC.Classes’))
   |                    
11 | equal = _          
   |         ^          
                        
/home/sankalp/projects/ecta/ecta-plugin/TestPlugin/Test.hs:15:19: error:
    • Found hole: _ :: [b]
      Where: ‘b’ is a rigid type variable bound by
               the type signature for:
                 myMapMaybe :: forall g b a. (g -> Maybe b) -> [a] -> [b]
               at Test.hs:14:1-42
    • In the expression: _
      In an equation for ‘myMapMaybe’: myMapMaybe f xs = _
    • Relevant bindings include
        xs :: [a] (bound at Test.hs:15:14)
        f :: g -> Maybe b (bound at Test.hs:15:12)
        myMapMaybe :: (g -> Maybe b) -> [a] -> [b] (bound at Test.hs:15:1)
      Valid hole fits include
        [] :: forall a. [a]
          with [] @b    
          (bound at <wired into compiler>)
        (myMapMaybe f) xs
        (myMapMaybe f) []
        reverse ((myMapMaybe f) xs)
        (myMapMaybe f) (reverse xs)
        reverse ((myMapMaybe f) [])
        (myMapMaybe f) (reverse [])
        reverse (reverse ((myMapMaybe f) xs))
        reverse ((myMapMaybe f) (reverse xs))
        (myMapMaybe f) (reverse (reverse xs))
        (myMapMaybe f) ((mapMaybe Just) xs)
        (mapMaybe Just) ((myMapMaybe f) xs)
        reverse (reverse ((myMapMaybe f) []))
        reverse ((myMapMaybe f) (reverse []))
        (mapMaybe Just) ((myMapMaybe f) [])
        (myMapMaybe f) (reverse (reverse []))
        (myMapMaybe f) ((mapMaybe Just) [])
        (myMapMaybe f) ((mapMaybe id) [])
   |                    
15 | myMapMaybe f xs = _
   |

Once again, I don't see the error (going by spotting a "Hectare error:" string).

@sankalpgambhir
Copy link

For completeness, here are the package versions in use with stack:

For ecta, I used a locally cloned version at sankalpgambhir/ecta@3a78950

and for ecta-plugin, Tritlo/ecta-plugin@d21399e and Tritlo/ecta-plugin@8ab8b8c .

$ stack ls dependencies --separator -
Cabal-3.2.1.0
STMonadTrans-0.4.6
StateVar-1.2.2
TestPlugin-1.0.0
adjunctions-4.4
ansi-terminal-0.11.1
array-0.5.4.0
base-4.14.3.0
base-orphans-0.8.6
bifunctors-5.5.11
binary-0.8.8.0
bytestring-0.10.12.0
cabal-doctest-1.0.9
call-stack-0.3.0
clock-0.8.3
cmdargs-0.10.21
colour-2.3.6
comonad-5.0.8
containers-0.6.5.1
contravariant-1.5.5
data-default-class-0.1.2.0
deepseq-1.4.4.0
directory-1.3.6.0
distributive-0.6.2.1
ecta-1.0.0.3
ecta-plugin-0.1.1.3
equivalence-0.4.1
exceptions-0.10.4
extra-1.7.9
fgl-5.7.0.3
filepath-1.4.2.1
free-5.1.7
ghc-8.10.7
ghc-boot-8.10.7
ghc-boot-th-8.10.7
ghc-heap-8.10.7
ghc-prim-0.6.1
ghci-8.10.7
hashable-1.3.0.0
hashtables-1.2.4.2
hpc-0.6.1.0
ilist-0.4.0.1
indexed-traversable-0.1.2
integer-gmp-1.0.3.0
intern-0.9.4
invariant-0.5.5
kan-extensions-5.2.3
keys-3.12.3
language-dot-0.1.1
lens-4.19.2
mmorph-1.1.5
mtl-2.2.2
parallel-3.2.2.0
parsec-3.1.14.0
pipes-4.3.16
pointed-5.0.3
pretty-1.1.3.6
pretty-simple-4.0.0.0
prettyprinter-1.7.1
prettyprinter-ansi-terminal-1.1.3
primitive-0.7.3.0
process-1.6.13.2
profunctors-5.6.2
raw-strings-qq-1.1
reflection-2.1.6
rts-1.0.1
semigroupoids-5.3.7
semigroups-0.19.2
stm-2.5.0.1
tagged-0.8.6.1
template-haskell-2.16.0.0
terminfo-0.4.1.4
text-1.2.4.1
th-abstraction-0.4.3.0
time-1.9.3
transformers-0.5.6.2
transformers-base-0.4.6
transformers-compat-0.6.6
unix-2.7.2.2
unordered-containers-0.2.16.0
vector-0.12.3.1
vector-instances-3.4
void-0.7.3

@Tritlo
Copy link
Collaborator Author
Tritlo commented Sep 24, 2023 •
edited
Loading

Weird that your stack seems to have ecta 1.0.0.3 in there and the plugin as well... are you sure it is using the right versions?

This is what I get from cabal build in TestPlugin using your ecta branch.

[1 of 1] Compiling Test             ( Test.hs, /home/tritlo/ecta-plugin/dist-newstyle/build/x86_64-linux/ghc-8.10.7/TestPlugin-1.0.0/x/test/build/test/test-tmp/Test.o )
(TCons "[]" [TVar "b"],["[]"])
Hectare error:
compare: unexpected RecUnint 0
CallStack (from HasCallStack):
  error, called at src/Data/ECTA/Internal/ECTA/Type.hs:233:31 in ecta-1.0.0.4-inplace:Data.ECTA.Internal.ECTA.Type
(TFun (TCons "[]" [TVar "a"]) (TFun (TCons "[]" [TVar "a"]) (TCons "Bool" [])),["[]"])
Hectare error:
compare: unexpected RecUnint 0
CallStack (from HasCallStack):
  error, called at src/Data/ECTA/Internal/ECTA/Type.hs:233:31 in ecta-1.0.0.4-inplace:Data.ECTA.Internal.ECTA.Type

Test.hs:10:9: error:
    • Found hole: _ :: [a] -> [a] -> Bool
      Where: ‘a’ is a rigid type variable bound by
               the type signature for:
                 equal :: forall a. Eq a => [a] -> [a] -> Bool
               at Test.hs:9:1-35
    • In the expression: _
      In an equation for ‘equal’: equal = _
    • Relevant bindings include
        equal :: [a] -> [a] -> Bool (bound at Test.hs:10:1)
      Constraints include Eq a (from Test.hs:9:1-35)
      Valid hole fits include
        equal :: [a] -> [a] -> Bool (bound at Test.hs:10:1)
        (==) :: forall a. Eq a => a -> a -> Bool
          with (==) @[a]
          (imported from ‘Prelude’ at Test.hs:4:8-11
           (and originally defined in ‘ghc-prim-0.6.1:GHC.Classes’))
        (/=) :: forall a. Eq a => a -> a -> Bool
          with (/=) @[a]
          (imported from ‘Prelude’ at Test.hs:4:8-11
           (and originally defined in ‘ghc-prim-0.6.1:GHC.Classes’))
   |
10 | equal = _
   |         ^

Test.hs:14:19: error:
    • Found hole: _ :: [b]
      Where: ‘b’ is a rigid type variable bound by
               the type signature for:
                 myMapMaybe :: forall g b a. (g -> Maybe b) -> [a] -> [b]
               at Test.hs:13:1-42
    • In the expression: _
      In an equation for ‘myMapMaybe’: myMapMaybe f xs = _
    • Relevant bindings include
        xs :: [a] (bound at Test.hs:14:14)
        f :: g -> Maybe b (bound at Test.hs:14:12)
        myMapMaybe :: (g -> Maybe b) -> [a] -> [b] (bound at Test.hs:14:1)
      Valid hole fits include
        [] :: forall a. [a]
          with [] @b
          (bound at <wired into compiler>)
        mempty :: forall a. Monoid a => a
          with mempty @[b]
          (imported from ‘Prelude’ at Test.hs:4:8-11
           (and originally defined in ‘GHC.Base’))
   |
14 | myMapMaybe f xs = _
   |                   ^
Error: cabal: Failed to build exe:test from TestPlugin-1.0.0.

Are you sure stack is not hiding those errors somehow? Try it again now, I've changed the test-case in TestPlugin/ to not hide the prelude and import everything.

@Tritlo
Copy link
Collaborator Author
Tritlo commented Sep 24, 2023

(if you want to play around with it directly, just clone  git clone https://github.com/sankalpgambhir/ecta directly into the ecta-plugin directory and add ecta/ to the cabal.project so that it uses ecta from there.

@sankalpgambhir
Copy link
sankalpgambhir commented Sep 24, 2023 •
edited
Loading

(if you want to play around with it directly, just clone  git clone https://github.com/sankalpgambhir/ecta directly into the ecta-plugin directory and add ecta/ to the cabal.project so that it uses ecta from there.

That is what I was doing already, but thanks :)

@sankalpgambhir
Copy link

I'll check again to see if stack is hiding something, but I do also see many more hole fit suggestions compared to your output.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@jkoppel @Tritlo @sankalpgambhir
0