Chapter 12 Exercise InsertRight

[jllang]

I get errors when I try to define insRsymmetrically to how insLhas been defined above. However, these errors are about insL rather than insR. How can it be? These are the errors I get:

~/liquidhaskell-tutorial/src/Tutorial_12_Case_Study_AVL.lhs:606:42: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : a
    .
    is not a subtype of the required type
      VV : {VV : a | VV < v}
    .
    in the context
      v : a
    |
606 |   | isLeftBig && leftHeavy l'  = balLL v l' r
    |                                          ^^

~/liquidhaskell-tutorial/src/Tutorial_12_Case_Study_AVL.lhs:607:42: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : a
    .
    is not a subtype of the required type
      VV : {VV : a | VV < v}
    .
    in the context
      v : a
    |
607 |   | isLeftBig && rightHeavy l' = balLR v l' r
    |                                          ^^

~/liquidhaskell-tutorial/src/Tutorial_12_Case_Study_AVL.lhs:608:42: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : a
    .
    is not a subtype of the required type
      VV : {VV : a | VV < v}
    .
    in the context
      v : a
    |
608 |   | isLeftBig                  = balL0 v l' r
    |                                          ^^

~/liquidhaskell-tutorial/src/Tutorial_12_Case_Study_AVL.lhs:609:42: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : a
    .
    is not a subtype of the required type
      VV : {VV : a | VV < v}
    .
    in the context
      v : a
    |
609 |   | otherwise                  = node  v l' r
    |                                          ^^

How can it be that modifying one function breaks another independent function?

[ranjitjhala]

1. Can you post a link to your code?
2. Do you have a signature for insL and insR?

[jllang]

Here's the link: https://privatebin.net/?2b64c18c8da919bc#BPts1wpxjXVxaLyzqM9RdhP5Zwtp6E2AqhkxcainToFg

I haven't modified the signatures. My implementation for insR is pretty much the mirror image of insL. If I comment out everything about insR, then these errors go away.

[ranjitjhala]

Hi John, This kind of thing can happen sometimes as an odd consequence of local inference. Suppose you have two "public" functions foo :: Nat -> Nat foo x = incr x bar :: Int -> Int bar x = incr x both of which use a "private" helper function incr :: Int -> Int incr x = 2 * x If you OMIT a signature for `incr`, then LH infers that INCR has the type incr :: Nat -> Nat as it is only called by `foo` with `Nat` inputs. However, if you _add_ the function `bar` into the mix, then LH infers a weaker type for incr, incr :: Int -> Int which is too weak to prove the type of `foo`, thus triggering an error in `foo`. As an example see this http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1627321397_37616.hs So: in your case, check if there is some common helper function who lacks a type signature?

[ranjitjhala]

Or can you send me the full code (in addition to insR) you’re running so I can see if it’s this or something else ? Thanks!

…

On Mon, Jul 26, 2021 at 10:47 AM Ranjit Jhala ***@***.***> wrote: Hi John, This kind of thing can happen sometimes as an odd consequence of local inference. Suppose you have two "public" functions foo :: Nat -> Nat foo x = incr x bar :: Int -> Int bar x = incr x both of which use a "private" helper function incr :: Int -> Int incr x = 2 * x If you OMIT a signature for `incr`, then LH infers that INCR has the type incr :: Nat -> Nat as it is only called by `foo` with `Nat` inputs. However, if you _add_ the function `bar` into the mix, then LH infers a weaker type for incr, incr :: Int -> Int which is too weak to prove the type of `foo`, thus triggering an error in `foo`. As an example see this http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1627321397_37616.hs So: in your case, check if there is some common helper function who lacks a type signature?