compare: unexpected RecIntersect (UnsafeIntersectId 478 478)

[Tritlo]

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]

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

[Tritlo]

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

[Tritlo]

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

[jkoppel]

Awesome!

Sankalp, let's get this merged.

[Tritlo]

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

compare: unexpected RecIntersect (UnsafeIntersectId 478 478) 

to

compare: unexpected RecUnint 0

[sankalpgambhir]

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]

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]

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]

(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]

(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]

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.