Open Tritlo opened 1 year ago
@Tritlo I don't have a working setup of the plugin. Can you turn this into the actual calls to the ecta library?
The cabal file in the gist installs the plugin, it's all in the stderr, no editor involvement.
Awesome!
Sankalp, let's get this merged.
Oh wait, it is still broken. The patch changes it from
compare: unexpected RecIntersect (UnsafeIntersectId 478 478)
to
compare: unexpected RecUnint 0
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@3a7895086e7d5addb107f280da18145a859d7dd2 I don't see the same error (testing with Tritlo/ecta-plugin@8ab8b8c490d1ec0ed28f48cf7ee233acd2d3c5d8) (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@d21399ed9d3a5247b6f7d75a1af8196622e5f84b:
/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).
For completeness, here are the package versions in use with stack
:
For ecta
, I used a locally cloned version at sankalpgambhir/ecta@3a7895086e7d5addb107f280da18145a859d7dd2
and for ecta-plugin
, Tritlo/ecta-plugin@d21399ed9d3a5247b6f7d75a1af8196622e5f84b and Tritlo/ecta-plugin@8ab8b8c490d1ec0ed28f48cf7ee233acd2d3c5d8 .
$ 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
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.
(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.
(if you want to play around with it directly, just clone
git clone https://github.com/sankalpgambhir/ecta
directly into theecta-plugin
directory and addecta/
to thecabal.project
so that it uses ecta from there.
That is what I was doing already, but thanks :)
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.
I'm trying to use ecta via the ecta-plugin, but when I use it for
Prelude
it complains aboutI'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 (https://github.com/haskell/haskell-language-server/pull/3159), so would be great if we could figure it out.