haskell - 単純な LiquidHaskell の例は、期待される動作に失敗します

Question

最近、液体 Haskell をいじり始めましたが、見つけたすべてのチュートリアルから、次のような例を見つけることができませんでした。

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 

次のことを試してみると、モジュールは期待どおりに型チェックを行いません。

test = getPerson (MaybePerson Nothing Nothing) 

ただし、何らかの理由で、以下はまだ型チェックを行いません。

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

エラーが発生します

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

さらに、getPerson _ = undefined行を省略すると、

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

Liquidhaskell で指定された前提条件のために、明らかにこの関数は全体ですが。

ここで何が間違っていますか？Maybe a私は基本的に、コンストラクターから来る型のサブタイプで推論できるようにしたいだけですが、Justこれを適切に行う場所の例はどこにも見つかりませんでした。