Initial version of typed holes support under allow-typed-holes flag #2486
Conversation
There was a problem hiding this comment.
Thanks @matheussbernardo. I left some comments. Can we have the feature documented? Maybe it could have a section in docs/mkDocs/docs/options.md.
Also, it would be helpful to have an example of a warning message produced by this implementation for the discussion.
liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs
Outdated
Show resolved
Hide resolved
liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs
Outdated
Show resolved
Hide resolved
liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs
Outdated
Show resolved
Hide resolved
| getSrcSpanFromTick = case genTick of | ||
| SourceNote src _ -> src | ||
| _ -> panic Nothing "Not a Source Note" | ||
| isVarHole = L.isInfixOf "hole" . F.symbolString . F.symbol |
There was a problem hiding this comment.
Will this mistakenly catch variables written by the user that include "hole" in their name? e.g. whole, wholesale, etc.
To make this as precise as possible, I need to understand yet how the variable is bound.
There was a problem hiding this comment.
I updated the implementation. Can you take a second look?
liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Types.hs
Outdated
Show resolved
Hide resolved
| @@ -1,6 +1,6 @@ | |||
| {-@ LIQUID "--expect-error-containing=Hole Found" @-} | |||
| {-@ LIQUID "--exact-data-cons" @-} | |||
| {-@ LIQUID "--allow-typed-holes" @-} | |||
| {-@ LIQUID "--warn-on-term-holes" @-} | |||
There was a problem hiding this comment.
This could be added to the basic-pos testsuite. For scripts/test/test_plugin.sh to pick up the module, it will need to be listed in tests/tests.cabal.
There was a problem hiding this comment.
I just found that it is actually listed in tests.cabal. A separate executable seems overkill for a single test. It would be terser to put it in an existing executable.
There was a problem hiding this comment.
I added more tests to this. I was thinking of adding all my examples to it. But maybe it is a overkill
Based on PR#1140
I am adding a flag --allow-typed-holes
and detecting holes which are bindings with
holeas infix.These holes are currently being saved in the CGInfo and a warning is being presented to the user showing the refinement type.
I added one example in the test that shows how to use this experimental feature.