liquidhaskell error about merge example

[mhwombat]

Liquidhaskell reports an error with one of the examples:

 /home/amy/liquidhaskell-tutorial/src/05-datatypes.lhs:338:1-5: Error: Liquid Type Mismatch

 338 | merge xs  Emp = xs
       ^^^^^

   Inferred type
     VV : {v : GHC.Prim.Addr# | v == "/home/amy/liquidhaskell-tutorial/src/05-datatypes.lhs:(338,1)-(342,39)|function merge"}

   not a subtype of Required type
     VV : {VV : GHC.Prim.Addr# | 5 < 4}

The code it's complaining about is this:

merge         :: (Ord a) => IncList a -> IncList a -> IncList a
merge xs  Emp = xs    <--- line 338
merge Emp ys  = ys
merge (x :< xs) (y :< ys)
  | x <= y    = x :< merge xs (y :< ys)
  | otherwise = y :< merge (x :< xs) ys

[mhwombat]

You can also see the error on the web page (http://ucsd-progsys.github.io/liquidhaskell-tutorial/05-datatypes.html) if you click the compile button.

[skyzh]

I encountered the same error, but I found that add a line merge _ _ = Emp makes sense. Here's my code:

merge :: (Ord a) => IncList a -> IncList a -> IncList a
merge Emp ys = ys
merge xs Emp = xs
merge (x :< xs) (y :< ys)
    | x <= y    = x :< (merge xs (y :< ys))
    | otherwise = y :< (merge (x :< xs) ys)
merge _ _ = Emp

This may pass liquid haskell safe check.

[ranjitjhala]

Yes this seems like some unfortunate consequence of how new versions of GHC desugar pattern matches. This seems related to the issue #1396 Posted by @wkunkel.

Does the suggested extra case work? If so will update tutorial appropriately.

On Mon, Jan 21, 2019 at 5:03 AM Alex Chi notifications@github.com wrote:

I encountered the same error, but I found that add a line merge = Emp makes sense. Here's my code:

merge :: (Ord a) => IncList a -> IncList a -> IncList a merge Emp ys = ys merge xs Emp = xs merge (x :< xs) (y :< ys) | x <= y = x :< (merge xs (y :< ys)) | otherwise = y :< (merge (x :< xs) ys) merge = Emp

This may pass liquid haskell safe check.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/76#issuecomment-456066773, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOGKB5J6CZPmQGDQ0wE9o00wIXm0Wks5vFbp-gaJpZM4ZyfDi .

[skyzh]

Here's my code, and it passes Travis check.

https://github.com/SkyZH/playground.lhs/blob/master/src/Ex42.hs#L129 https://travis-ci.com/SkyZH/playground.lhs

[ranjitjhala]

Fantastic! Can you send a PR? (If not I can manually do it...)

On Tue, Jan 22, 2019 at 4:41 AM Alex Chi notifications@github.com wrote:

Here's my code, and it passes Travis check.

https://github.com/SkyZH/playground.lhs/blob/master/src/Ex42.hs#L129 https://travis-ci.com/SkyZH/playground.lhs

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/76#issuecomment-456352897, or mute the thread https://github.com/notifications/unsubscribe-auth/ABkuOLaxkEDwhoJ5gIXYT7bBHhCJSgSvks5vFuqXgaJpZM4ZyfDi .

[skyzh]

I've already sent #78 yesterday :) @ranjitjhala