Simple liquidhaskell example fails expected behavior

I have recently started playing around with liquid haskell, and from all of the tutorials I could find, I could not find any examples like the following.

data MaybePerson = MaybePerson {                                                                        
  name' :: Maybe String,                                                                                
  age'  :: Maybe Int                                                                                    
}                                                                                                       

data Person = Person {                                                                                  
  name :: String,                                                                                       
  age  :: Int                                                                                           
}                                                                                                       

{-@ measure p :: MaybePerson -> Bool @-}                                                                
p (MaybePerson (Just _) (Just _)) = True                                                                
p _ = False                                                                                             

{-@ type JustPerson = {x:MaybePerson | p x} @-}                                                 

-- Attempts to instantiate a maybe person into a concrete Person                                    
{-@ getPerson :: JustPerson -> Person @-}                                               
getPerson (MaybePerson (Just name) (Just age)) = Person name age                             
getPerson _ = undefined

If I try the following, my module does not type-check, as expected:

test = getPerson (MaybePerson Nothing Nothing)

However, for some reason, the following still does not type check:

test2 = getPerson (MaybePerson (Just "bob") (Just 25))

and I get the error

Error: Liquid Type Mismatch

 36 | test2 = getPerson (MaybePerson (Just "bob") (Just 25))
                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

   Inferred type
     VV : {v : MaybePerson | v == ?a}

   not a subtype of Required type
     VV : {VV : MaybePerson | Blank.p VV}

   In Context
     ?a : MaybePerson

Moreover, if I leave out the getPerson _ = undefined line, I get

Your function is not total: not all patterns are defined.

Even though clearly this function is total because of the precondition specified with liquidhaskell.

What am I doing wrong here? I essentially just want to be able to reason with subtypes of a Maybe a type which are coming from the Just constructor, but I couldn't find any examples anywhere of where to do this properly.

Solution

sorry for the late reply! I should find some way to get notified about questions. Ok, there are two things going on, both of which we should fix!

First, there is something glitchy happening with

{-@ measure p :: MaybePerson -> Bool @-}

The right syntax is just

{-@ measure p @-}
p :: MaybePerson -> Bool

But there was no error message, so there's no way for you to know!

Second, when I change the above I still get some strange error about GHC.Maybe -- I can't recall the exact issue right now, will fix on my laptop, but for illustration, I tweaked your code to:

{-@ LIQUID "--exact-data-cons" @-}

import Prelude hiding (Maybe (..))

data Maybe a = Just a | Nothing

To redefine Maybe. This should not be needed will figure out a fix ASAP

With this, your code works as is, e.g. see here

http://goto.ucsd.edu/liquid/index.html#?demo=permalink%2F1573693313_399.hs

So you can now define

{-@ getPerson :: JustPerson -> Person @-}                                               
getPerson (MaybePerson (Just name) (Just age)) = Person name age

and just remove the equation for the other cases. Further,

test1 = getPerson (MaybePerson Nothing Nothing)         -- error

yields a type error, but the below is safe

test2 = getPerson (MaybePerson (Just "bob") (Just 25))  -- ok

Thanks for pointing this out, will fix!