Totality checker is confused by GADTs

[facundominguez]

Verifying the following program fails in the totality check.

{-# LANGUAGE GADTs #-}

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

{-@
data T a where
  T :: Int -> T Int
  TB :: Bool -> T Bool
 @-}
data T a where
  T :: Int -> T Int
  TB :: Bool -> T Bool

{-@ reflect getT @-}
getT :: T Int -> Int
getT (T a) = a

main :: IO ()
main = print ()

The error is

    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : GHC.Prim.Addr# | v == "Test.hs:17:1-14|function getT"}
    .
    is not a subtype of the required type
      VV : {VV : GHC.Prim.Addr# | totalityError "Pattern match(es) are non-exhaustive"}
    .
    Constraint id 18
   |
17 | getT (T a) = a
   | ^^^^^^^^^^^^^^

Is this a bug given that the type of the first parameter of getT doesn't allow the TB data constructor?

[ranjitjhala]

That’s interesting! Surely GHC knows that code is unreachable: why is the case even emitted in the core?

On Tue, Nov 16, 2021 at 1:07 PM Facundo Domínguez @.***> wrote:

Verifying the following program fails in the totality checker.

{-# LANGUAGE GADTs #-}

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

{-@ data T a where T :: Int -> T Int TB :: Bool -> T Bool @-} data T a where T :: Int -> T Int TB :: Bool -> T Bool

{-@ reflect getT @-} getT :: T Int -> Int getT (T a) = a

main :: IO () main = print ()

The error is

Liquid Type Mismatch
.
The inferred type
  VV : {v : GHC.Prim.Addr# | v == "Test.hs:17:1-14|function getT"}
.
is not a subtype of the required type
  VV : {VV : GHC.Prim.Addr# | totalityError "Pattern match(es) are non-exhaustive"}
.
Constraint id 18

| 17 | getT (T a) = a | ^^^^^^^^^^^^^^

Is this a bug given that the type of the first parameter of getT doesn't allow the TB data constructor?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquidhaskell_issues_1905&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=ws62J5tBvOww64uyk8uk27vKCKiQAWGXDghoc4746iiPo-1pKRJcpL-7igkVCAyd&s=SdgBdt8bLK4P3O2ctdY48orzLbJFML8yL6gCNT51Ijs&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OCYGRVDSWY43BL3YF3UMLBZTANCNFSM5IFIIUHA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=ws62J5tBvOww64uyk8uk27vKCKiQAWGXDghoc4746iiPo-1pKRJcpL-7igkVCAyd&s=egbzbaWGilnE1tqxDmA6ngY9sw4BMeZmdo_Od-XLWWc&e= . Triage notifications on the go with GitHub Mobile for iOS https://urldefense.proofpoint.com/v2/url?u=https-3A__apps.apple.com_app_apple-2Dstore_id1477376905-3Fct-3Dnotification-2Demail-26mt-3D8-26pt-3D524675&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=ws62J5tBvOww64uyk8uk27vKCKiQAWGXDghoc4746iiPo-1pKRJcpL-7igkVCAyd&s=j5omrjTBavd5OArX91K6BrteCf9peDff8Hl3bR1se7k&e= or Android https://urldefense.proofpoint.com/v2/url?u=https-3A__play.google.com_store_apps_details-3Fid-3Dcom.github.android-26referrer-3Dutm-5Fcampaign-253Dnotification-2Demail-2526utm-5Fmedium-253Demail-2526utm-5Fsource-253Dgithub&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=ws62J5tBvOww64uyk8uk27vKCKiQAWGXDghoc4746iiPo-1pKRJcpL-7igkVCAyd&s=9rrfs6t-9QbE7Vp5ji_R5bCQSRLDvfq2odFztA88qC4&e=.