invalid datatype declaration, repeated accessor identifier

[RyanGlScott]

These two files give LH a headache:

{-@ LIQUID "--higherorder"        @-}
{-@ LIQUID "--exactdc"            @-}
module Aux where

data U1 p = U1
data Product f g p = Product (f p) (g p)

{-@ LIQUID "--higherorder"        @-}
{-@ LIQUID "--exactdc"            @-}
module Bug where

import Aux
import Language.Haskell.Liquid.ProofCombinators

{-@ axiomatize leqU1 @-}
leqU1 :: U1 p -> U1 p -> Bool
leqU1 _ _ = True

{-@ leqU1Refl :: x:U1 p -> { leqU1 x x } @-}
leqU1Refl :: U1 p -> Proof
leqU1Refl U1 = leqU1 U1 U1 ==. True *** QED

{-@ axiomatize leqProd @-}
leqProd :: Eq (f p)
        => (f p -> f p -> Bool) -> (g p -> g p -> Bool)
        -> Product f g p -> Product f g p -> Bool
leqProd leqFP leqGP (Product x1 y1) (Product x2 y2) =
  if x1 == x2
    then leqGP y1 y2
    else leqFP x1 x2
{-# INLINE leqProd #-}

$ /opt/cabal/head/bin/cabal new-run liquid -- Aux.hs 
Up to date
LiquidHaskell Copyright 2013-17 Regents of the University of California. All Rights Reserved.

**** DONE:  A-Normalization ****************************************************

**** DONE:  Extracted Core using GHC *******************************************

**** DONE:  Transformed Core ***************************************************

**** DONE:  Uniqify & Rename ***************************************************

**** DONE:  Defunctionalize ****************************************************

**** DONE:  Elaborate **********************************************************

**** DONE:  Instantiate ********************************************************

**** DONE:  Worklist Initialize ************************************************

Working -9223372036854775808% []

**** DONE:  annotate ***********************************************************

**** RESULT: SAFE **************************************************************
$ /opt/cabal/head/bin/cabal new-run liquid -- Bug.hs 
Up to date
LiquidHaskell Copyright 2013-17 Regents of the University of California. All Rights Reserved.

**** DONE:  A-Normalization ****************************************************

**** DONE:  Extracted Core using GHC *******************************************

**** DONE:  Transformed Core ***************************************************

**** DONE:  Uniqify & Rename ***************************************************

**** DONE:  Defunctionalize ****************************************************

**** DONE:  Elaborate **********************************************************

**** DONE:  Instantiate ********************************************************

**** DONE:  Worklist Initialize ************************************************

Working 100% [=================================================================]

**** DONE:  annotate ***********************************************************

**** RESULT: ERROR *************************************************************

:1:1-1:1: Error
  crash: SMTLIB2 respSat = Error "line 27 column 19: invalid datatype declaration, repeated accessor identifier 'lqdc$35$$35$$36$select$35$$35$Aux.Product$35$$35$1'"

I'm using liquidhaskell commit a5545e942fca3b106407ec5b2b72c4596ee838ff and liquid-fixpoint commit https://github.com/ucsd-progsys/liquid-fixpoint/commit/1148baa43b3869bf44518879687a956490544162.

[ranjitjhala]

@RyanGlScott are you sure you are rebuilding etc.? I cannot reproduce this.

Also, could be a z3 version thing. which version do you have? Run

z3 --version

[ranjitjhala]

Here's my log

rjhala@borscht ~/r/s/l/t/i/lib (T1117)> more T1117Lib.hs
{-@ LIQUID "--higherorder"        @-}
{-@ LIQUID "--exactdc"            @-}

module T1117Lib where

data U1 p = U1

data Product f g p = Product (f p) (g p)
rjhala@borscht ~/r/s/l/t/i/lib (T1117)> more T1117.hs
{-@ LIQUID "--higherorder"        @-}
{-@ LIQUID "--exactdc"            @-}

module T1117 where

import T1117Lib

import Language.Haskell.Liquid.ProofCombinators

{-@ axiomatize leqU1 @-}
leqU1 :: U1 p -> U1 p -> Bool
leqU1 _ _ = True

{-@ leqU1Refl :: x:U1 p -> { leqU1 x x } @-}
leqU1Refl :: U1 p -> Proof
leqU1Refl U1 = leqU1 U1 U1 ==. True *** QED

{-@ axiomatize leqProd @-}
leqProd :: Eq (f p)
        => (f p -> f p -> Bool) -> (g p -> g p -> Bool)
        -> Product f g p -> Product f g p -> Bool
leqProd leqFP leqGP (Product x1 y1) (Product x2 y2) =
  if x1 == x2
    then leqGP y1 y2
    else leqFP x1 x2
{-# INLINE leqProd #-}
rjhala@borscht ~/r/s/l/t/i/lib (T1117)> stack exec -- liquid T1117Lib.hs
LiquidHaskell Copyright 2013-17 Regents of the University of California. All Rights Reserved.

**** DONE:  A-Normalization ****************************************************

**** DONE:  Extracted Core using GHC *******************************************

**** DONE:  Transformed Core ***************************************************

**** DONE:  Uniqify & Rename ***************************************************

**** DONE:  Defunctionalize ****************************************************

**** DONE:  Elaborate **********************************************************

**** DONE:  Instantiate ********************************************************

**** DONE:  Worklist Initialize ************************************************

Working -9223372036854775808% []

**** DONE:  annotate ***********************************************************

**** RESULT: SAFE **************************************************************
rjhala@borscht ~/r/s/l/t/i/lib (T1117)> stack exec -- liquid T1117.hs
LiquidHaskell Copyright 2013-17 Regents of the University of California. All Rights Reserved.

**** DONE:  A-Normalization ****************************************************

**** DONE:  Extracted Core using GHC *******************************************

**** DONE:  Transformed Core ***************************************************

**** DONE:  Uniqify & Rename ***************************************************

**** DONE:  Defunctionalize ****************************************************

**** DONE:  Elaborate **********************************************************

**** DONE:  Instantiate ********************************************************

**** DONE:  Worklist Initialize ************************************************

Working 100% [=================================================================]

**** DONE:  annotate ***********************************************************

**** RESULT: SAFE **************************************************************
rjhala@borscht ~/r/s/l/t/i/lib (T1117)> z3 --version
Z3 version 4.3.2

[ranjitjhala]

Yes looks like a z3 version thing: the online version complains about the .smt2 file that is generated locally -- and works fine locally... pfft.

[RyanGlScott]

In case it's helpful:

$ z3 --version
Z3 version 4.4.1

[RyanGlScott]

I can confirm that upgrading to z3-4.5.0 resolves the issue for me on Linux, FWIW.

[RyanGlScott]

Sorry, please ignore the comment above. I was testing the wrong files. Testing it on the right files, I still get the same error, even with z3-4.5.0.