Merge example (05-datatypes) won't compile

[DestyNova]

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 _ _ = Emp

I got this output:

$ liquid --no-termination --no-totality lh-ch5-2.hs

LiquidHaskell Version 0.8.6.0, Git revision 6f29ece8f61483f0546d052308882c8abef6da78 (dirty) [develop@6f29ece8f61483f0546d052308882c8abef6da78 (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.

[ranjitjhala]

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 notifications@github.com 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 6f29ece8f61483f0546d052308882c8abef6da78 (dirty) [develop@6f29ece8f61483f0546d052308882c8abef6da78 (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$ .

[DestyNova]

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 a@ and b@ references to simplify... then after eliminating the original problem, forgot to test without those references.

How embarrassing :grinning:

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:

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?

[ranjitjhala]

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 notifications@github.com 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$ .

[DestyNova]

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 :wink:

[DestyNova]

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 del problem in chapter 5 and can't see how it could possibly done by calling delMin (i.e. what if del is called with the value of the root node? calling delMin would just walk down the tree and do something we don't want) :thinking:

[ranjitjhala]

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!

[ranjitjhala]

btw, looks like that solution for delMin is here:

https://github.com/ucsd-progsys/liquidhaskell-tutorial-solutions/blob/master/book/03-datatypes.lhs

[ranjitjhala]

btw as a hint: when you remove a node (even it its the "root") you need to replace it with something else. delMin is useful to find that "replacement" ...

[DestyNova]

Thanks @ranjitjhala! I peeked at the del solution and facepalmed straight away. I had the following comment in my notes... should have followed the train of thought a few steps further :grin:

-- del k' t@(Node k l r) = case compare k' k of
--                           LT -> Node k (del k' l) r
--                           GT -> Node k l (del k' r)
--                           _ -> ... wait what? if we delete a middle node, we need to rewrite the tree by hoisting one of the children up :-/