Merge example (05-datatypes) won't compile #92
Comments
|
This is even harder to explain than your previous q - it’s the “a@“ to
blame. If you replace the a, b with the full pattern it will work fine.
The reason is that the way the type system works (with the constructor and
pattern matching) is that the guard information about x, y “lives” only in
those variables, it is not “back propagated” to the pattern variables
“a”,”b” — I don’t think this is an unsolvable issue but right now you need
to re “pack” the y:ys etc
Does that make sense?
…On Fri, Apr 17, 2020 at 8:50 PM Oisín ***@***.***> wrote:
This may be related to issue #76
<https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/76__;!!Mih3wA!U1Y7UNxKGMVH8pUcLKJ2XcHCFR2ML7bFUIq1FY78U6FB6TFSiB83XxXzAu8Oz5S6$>,
but the (temporary?) workaround listed there didn't help.
Compiling the merge example on the website produces a different error
message about totality, although maybe it is relevant too. I tried invoking
Liquid with the following code:
{-@ data IncList a = Emp
| (:<) { hd :: a, tl :: IncList {v:a | hd <= v}} @-}data IncList a =
Emp
| (:<) { hd :: a, tl :: IncList a }
deriving (Show, Eq)
infixr 9 :<
{-@ merge :: (Ord a) => IncList a -> IncList a -> IncList a @-}merge :: (Ord a) => IncList a -> IncList a -> IncList a
merge xs Emp = xs
merge Emp ys = ys
merge a@(x :< xs) b@(y :< ys)
| x <= y = x :< merge xs b
| otherwise = y :< merge a ys
merge _ _ = Emp
I got this output:
$ liquid --no-termination --no-totality lh-ch5-2.hs
LiquidHaskell Version 0.8.6.0, Git revision 6f29ece (dirty) ***@***.*** (Fri Apr 17 19:03:44 2020 +0200)]
Copyright 2013-19 Regents of the University of California. All Rights Reserved.
Targets: lh-ch5-2.hs
**** DONE: A-Normalization ****************************************************
**** DONE: Extracted Core using GHC *******************************************
**** DONE: Transformed Core ***************************************************
**** DONE: annotate ***********************************************************
**** RESULT: UNSAFE ************************************************************
/home/omf/code/haskell/liquid/ex/lh-ch5-2.hs:15:22-31: Error: Liquid Type Mismatch
15 | | x <= y = x :< merge xs b
^^^^^^^^^^
Inferred type
VV : a
not a subtype of Required type
VV : {VV : a | x <= VV}
In Context
x : a
/home/omf/code/haskell/liquid/ex/lh-ch5-2.hs:16:22-31: Error: Liquid Type Mismatch
16 | | otherwise = y :< merge a ys
^^^^^^^^^^
Inferred type
VV : a
not a subtype of Required type
VV : {VV : a | y <= VV}
In Context
y : a
Shouldn't it infer in these cases that if x <= y, then merge xs (y:ys)
must contain only elements greater or equal to x? Apologies if this is an
obvious understanding fail on my part.
—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
<https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/92__;!!Mih3wA!U1Y7UNxKGMVH8pUcLKJ2XcHCFR2ML7bFUIq1FY78U6FB6TFSiB83XxXzAhI7JmAY$>,
or unsubscribe
<https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OE6MMRHYKN6YJE3XP3RNEPRHANCNFSM4MLF7LDQ__;!!Mih3wA!U1Y7UNxKGMVH8pUcLKJ2XcHCFR2ML7bFUIq1FY78U6FB6TFSiB83XxXzAgKhx7l9$>
.
|
|
Yes that makes sense @ranjitjhala. I was sure I tried that way first, but maybe ran into a different error and then added in the How embarrassing 😀 It does still seem to require either the merge _ _ = EmpI'm not sure why this should be needed, but it's not in the published version of the tutorial site even though it was merged in a while back. Could the site need to be rebuilt / published? |
|
Interesting! I think this is due to some change in how GHC is generating
the Core for the
above example. When I run LH with the file
```
merge (x :< xs) (y :< ys)
| x <= y = x :< merge xs (y :< ys)
| otherwise = y :< merge (x :< xs) ys
merge xs Emp = xs
merge Emp ys = ys
```
I get back core that looks like the below
```
merge = \xlist ylist ->
case xList of
Emp -> yList
(x :< xs) -> case yList of
__DEFAULT ->
case yList of
_DEFAULT -> patternError
Emp -> xList
(y :< ys) -> {- code for merge -}
```
Now the `patternError` tickles the totality error.
Now clearly the above `_DEFAULT` is dead code, I *think* earlier versions
of GHC would eliminate it to produce the simplified (and "total") core below
```
merge = \xlist ylist ->
case xList of
Emp -> yList
(x :< xs) -> case yList of
Emp -> xList
(y :< ys) -> {- code for merge -}
```
Not sure what has changed. Maybe @nikivazou or @adinapoli or @kosmikus know?
At any rate, it _should_ be possible to fix this by either inducing GHC to
generate
the simplified core, or doing some version of the case elimination in LH --
namely,
1. if we have ALREADY matched `yList` against `:<` at an *outer level*, then
2. we should know it cannot be `:<` at an *inner level*.
Many thanks for pointing this out!!! (If you get a chance, can you make an
issue in
the LH repo? Else I will as soon as I resolve my 2FA woes...)
…On Sat, Apr 18, 2020 at 6:19 AM Oisín ***@***.***> wrote:
Yes that makes sense @ranjitjhala
<https://urldefense.com/v3/__https://github.com/ranjitjhala__;!!Mih3wA!XkvUGnBbTNMZesuHSuNbdtzoDkFgr4SoMJdd1PvDQxllmnmXFHFZgF3W4K5MohTg$>.
I was sure I tried that way first, but maybe ran into a different error and
then added in the a@ and b@ references to simplify... then after
eliminating the original problem, forgot to test without those references.
How embarrassing 😀
It does still seem to require either the --no-totality flag to be passed
to Liquid, or the catch-all line shown in issue #76
<https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/76__;!!Mih3wA!XkvUGnBbTNMZesuHSuNbdtzoDkFgr4SoMJdd1PvDQxllmnmXFHFZgF3W4GUTyaKd$>
:
merge _ _ = Emp
I'm not sure why this should be needed, but it's not in the published
version of the tutorial site even though it was merged in a while back.
Could the site need to be rebuilt / published?
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/92*issuecomment-615869896__;Iw!!Mih3wA!XkvUGnBbTNMZesuHSuNbdtzoDkFgr4SoMJdd1PvDQxllmnmXFHFZgF3W4GluhcVk$>,
or unsubscribe
<https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OCDBYZEOHYHERMSL2TRNGSG7ANCNFSM4MLF7LDQ__;!!Mih3wA!XkvUGnBbTNMZesuHSuNbdtzoDkFgr4SoMJdd1PvDQxllmnmXFHFZgF3W4AY0Qn6B$>
.
|
|
Thanks for the analysis @ranjitjhala! I'll open an issue and dump most of your comment into it since the case elimination internals are beyond my current comprehension 😉 |
|
Alright, issue added in the main repo. Could you share the exercise answers repo with me BTW @ranjitjhala? I'm running into issues with almost every exercise and don't want to spam the issue tracker if it's just simple confusion on my part... I'm stuck right now on the |
|
No worries, just gave you access. However, please do ping me if you get too stuck, because that's VERY likely something I haven't explained properly and needs fixing! |
|
btw, looks like that solution for delMin is here: https://github.com/ucsd-progsys/liquidhaskell-tutorial-solutions/blob/master/book/03-datatypes.lhs |
|
btw as a hint: when you remove a node (even it its the "root") you need to replace it with something else. |
|
Thanks @ranjitjhala! I peeked at the |
This may be related to issue #76, but the (temporary?) workaround listed there didn't help.
Compiling the merge example on the website produces a different error message about totality, although maybe it is relevant too. I tried invoking Liquid with the following code:
{-@ data IncList a = Emp | (:<) { hd :: a, tl :: IncList {v:a | hd <= v}} @-} data IncList a = Emp | (:<) { hd :: a, tl :: IncList a } deriving (Show, Eq) infixr 9 :< {-@ merge :: (Ord a) => IncList a -> IncList a -> IncList a @-} merge :: (Ord a) => IncList a -> IncList a -> IncList a merge xs Emp = xs merge Emp ys = ys merge a@(x :< xs) b@(y :< ys) | x <= y = x :< merge xs b | otherwise = y :< merge a ys merge _ _ = EmpI got this output:
Shouldn't it infer in these cases that if
x <= y, thenmerge xs (y :< ys)must contain only elements greater or equal tox? Apologies if this is an obvious understanding fail on my part.The text was updated successfully, but these errors were encountered: