Question about Chapter 5.3: delmin

[jllang]

The function delmin in Chapter 5.3 seems to have a problem. I get the following error:

~/liquidhaskell-tutorial/src/Tutorial_05_Datatypes.lhs:663:30: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : [GHC.Types.Char] | v ~~ "Don't say I didn't warn ya!"
                                   && len v == strLen "Don't say I didn't warn ya!"
                                   && len v >= 0
                                   && v == "Don't say I didn't warn ya!"}
    .
    is not a subtype of the required type
      VV : {VV : [GHC.Types.Char] | false}
    .
    |
663 | delMin Leaf            = die "Don't say I didn't warn ya!"
    |                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I tried adding this specification {-@ delMin :: (Ord a) => u : {t : BST | t /= Leaf} -> MinPair a @-} but it didn't help. With this specification, I get the following error message:

~/liquidhaskell-tutorial/src/Tutorial_05_Datatypes.lhs:657:15: error:
    • Specified type does not refine Haskell type for `Tutorial_05_Datatypes.delMin` (Plugged Init types old)
The Liquid type
.
    (GHC.Classes.Ord a) -> Tutorial_05_Datatypes.BST -> (Tutorial_05_Datatypes.MinPair a)
.
is inconsistent with the Haskell type
.
    forall a ->
GHC.Classes.Ord a =>
Tutorial_05_Datatypes.BST a -> Tutorial_05_Datatypes.MinPair a
.
defined at src/Tutorial_05_Datatypes.lhs:659:1-6
.
Specifically, the Liquid component
.
    {t : Tutorial_05_Datatypes.BST | t /= Tutorial_05_Datatypes.Leaf}
.
is inconsistent with the Haskell component
.
    (Tutorial_05_Datatypes.BST a)
.

HINT: Use the hole '_' instead of the mismatched component (in the Liquid specification)
    • 
    |
657 | {-@ delMin :: (Ord a) => u : {t : BST | t /= Leaf} -> MinPair a @-}
    |               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

It seems to me that the problem is when delmin is applied to Leaf, so it feels natural to require that the BST we're applying delmin to cannot be a leaf. Why is this specification rejected?

[jllang]

Changing the Leafcase return value to undefined fixes the error, but I feel like that's not the best way to solve this.

[jllang]

Ah, there seems to be a link to another chapter that supposedly helps to fix the problem with delmin. The link doesn't work for me, though.