LH regression: Ambiguous specification symbol

[RyanGlScott]

This is a regression that seems to have arisen somewhere between 27bc088c4f8b29fd9866e5589233e97e22e314c4 (where this bug does not occur) and 259ebc254472918e6275c44099c56d7ff019ea9f (where it does). First, consider these two files:

{-# LANGUAGE TypeFamilies #-}
module Generic where

import Language.Haskell.Liquid.ProofCombinators

class Generic a where
  type Rep a :: * -> *
  from :: a -> Rep a x
  to   :: Rep a x -> a

{-@ LIQUID "--higherorder"        @-}
{-@ LIQUID "--totality"           @-}
{-@ LIQUID "--exactdc"            @-}
module Iso where

import Language.Haskell.Liquid.ProofCombinators

{-@ data Iso a b = Iso { to   :: a -> b
                       , from :: b -> a
                       , tof  :: y:b -> { to (from y) == y }
                       , fot  :: x:a -> { from (to x) == x }
                       }
@-}
data Iso a b = Iso { to   :: a -> b
                   , from :: b -> a
                   , tof  :: b -> Proof
                   , fot  :: a -> Proof
                   }

If you try to check them with LH with either commit (I'll use the later one, 259ebc254472918e6275c44099c56d7ff019ea9f, as an example):

$ stack exec liquid -- Generic.hs                                                                                                      LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

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

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

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

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

Working -9223372036854775808% []

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

**** RESULT: SAFE **************************************************************
$ stack exec liquid -- Iso.hs
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

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

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

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

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

Working -9223372036854775808% []

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

**** RESULT: SAFE **************************************************************

Then they're safe, as expected (although the percentage is quite off, for some reason...)

However, if you combine these files:

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

import Language.Haskell.Liquid.ProofCombinators
import Iso
import Generic

Then with commit 27bc088c4f8b29fd9866e5589233e97e22e314c4, it's safe. But with commit 259ebc254472918e6275c44099c56d7ff019ea9f, it's unsafe:

$ stack exec liquid -- Bug.hs
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

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

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

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

 /home/rgscott/Documents/Hacking/Haskell/verified-instances/generic-proofs/Iso.hs:8:10: Error: Ambiguous specification symbol `to`

 8 | {-@ data Iso a b = Iso { to   :: a -> b
              ^
     Could refer to any of the names

     * - Generic.to

     * - Iso.to

This error is confusing for a number of reasons, since:

1. It shows the error as originating in Iso.hs, but that can't be the case, as checking Iso worked!
2. Why should LH be confused here? The only to whose definition was reflected was that of Iso.

[ranjitjhala]

This is my doing; will look into it soon!

In the meantime One workaround is to rename ISO's record name if possible?

[ranjitjhala]

This is my doing; will look into it soon!

In the meantime One workaround is to rename ISO's record name if possible?

[RyanGlScott]

Renaming the records does seem to work around the issue, yes.

[ranjitjhala]

By the way, the names are unqualified now so this should work even without renaming the fields. Can you try that?

[RyanGlScott]

I made this comment since I encountered this very issue (on the latest LH commit, 68370a4c5ae9c0dc2fa70e9373dd7da7d4a3a793) elsewhere. But I can try this minimized example again too.

[RyanGlScott]

I'm afraid that I experience the same error on 68370a4c5ae9c0dc2fa70e9373dd7da7d4a3a793 (after removing the --totality flag from Iso and Bug, of course).

[ranjitjhala]

Ok, so another work around is to make the imports qualified, i.e.

import qualified Iso
import qualified Generic

but really, we ought to just save the "qualified"-DataCtor (see qualifyDataCtor) in the lifted spec. Unfortunately, the qualifying happens long after the lifting, so this is quite a difficult piece of surgery :(