CoreToLogic: and/or embedding is broken

yiyunliu commented 4 years ago

I encountered this issue when trying to reuse coreToLogic to turn the elaborated core expression back to fixpoint expression.

{-@ LIQUID "--reflect" @-}
{-@ reflect bad @-}
bad :: Bool
bad = and [True,False,True]

This file gives back the following error message:

 2 | {-@ reflect bad @-}
                 ^^^

     Main.bad :: {VV : GHC.Types.Bool | VV == bad
                                        && VV == (: true (: false (: true [])))}
     Sort Error in Refinement: {VV : bool | (VV == Main.bad
                                             && VV == (GHC.Types.: true (GHC.Types.: false (GHC.Types.: true GHC.Types.[]))))}
     Expressions GHC.Types.: true (GHC.Types.: false (GHC.Types.: true GHC.Types.[])) should have bool sort, but has [bool]

By examining https://github.com/ucsd-progsys/liquidhaskell/blob/11cc7e31c26d7e4f644397beb9ee808114f48fc9/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs#L387, I figured out why things would go wrong.

Given the expression:

and (True:False:True:[])

splitArgs gives back:

(and,[(True:False:True:[])])

Note that the second element of the pair is not [True, False, True], but a singleton that contains (True:False:True:[]), which has type [Bool].

I suggest that we remove and and or embedding. It is not generally possible. The constructor PAnd takes a list of expressions, rather than one expression. We can't know the form of the list passed to the Haskell function and statically.

ranjitjhala commented 4 years ago

Wow that’s nasty! Your fix sounds reasonable!

On Wed, Feb 5, 2020 at 5:21 PM Yiyun Liu notifications@github.com wrote:

I encountered this issue when trying to reuse coreToLogic to turn the elaborated core expression back to fixpoint expression.

{-@ LIQUID "--reflect" @-} {-@ reflect bad @-}bad :: Bool bad = and [True,False,True]

This file gives back the following error message:

2 | {-@ reflect bad @-} ^^^
 Main.bad :: {VV : GHC.Types.Bool | VV == bad
                                    && VV == (: true (: false (: true [])))}
 Sort Error in Refinement: {VV : bool | (VV == Main.bad
                                         && VV == (GHC.Types.: true (GHC.Types.: false (GHC.Types.: true GHC.Types.[]))))}
 Expressions GHC.Types.: true (GHC.Types.: false (GHC.Types.: true GHC.Types.[])) should have bool sort, but has [bool]
By examining https://github.com/ucsd-progsys/liquidhaskell/blob/11cc7e31c26d7e4f644397beb9ee808114f48fc9/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs#L387 http://url, I figured out why things would go wrong.

Given the expression:

and (True:False:True:[])

splitArgs gives back:

(and,[(True:False:True:[])])

Note that the second element of the pair is not [True, False, True], but a singleton that contains (True:False:True:[]), which has type [Bool].

I suggest that we remove and and or embedding. It is not generally possible. The constructor PAnd takes a list of expressions, rather than one expression. We can't know the form of the list passed to the Haskell function and statically.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1603?email_source=notifications&email_token=AAMS4OHQPLGFUA3PMTFOMD3RBNQYLA5CNFSM4KQU3DI2YY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4ILL6OZQ, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAMS4OCFZXTZAGAN53566PDRBNQYLANCNFSM4KQU3DIQ .

facundominguez commented 3 months ago

I cannot reproduce this failure in the latest LH. But I get s similar failure if I try

{-@ LIQUID "--reflect" @-}
{-@ reflect bad @-}
bad :: [Bool] -> Bool
bad xs = and (True : False : xs)

ucsd-progsys / liquidhaskell

CoreToLogic: and/or embedding is broken #1603