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?