Importing refinements leads to "redundant" imports

[RyanGlScott]

This is a minor issue I ran into when combining Template Haskell with Liquid Haskell:

-- A.hs                                                                                   
{-@ LIQUID "--higherorder"    @-}                                                         
{-@ LIQUID "--totality"       @-}                                                         
{-@ LIQUID "--exactdc"        @-}                                                         
{-# LANGUAGE TemplateHaskell #-}                                                          
module A (genSimple) where                                                                

import Language.Haskell.Liquid.ProofCombinators                                           
import Language.Haskell.TH                                                                

genSimple :: Q [Dec]                                                                      
genSimple = [d| simple :: Proof; simple = trivial |]

-- B.hs                                                                                   
{-@ LIQUID "--higherorder"    @-}                                                         
{-@ LIQUID "--totality"       @-}                                                         
{-@ LIQUID "--exactdc"        @-}                                                         
{-# LANGUAGE TemplateHaskell #-}                                                          
{-# OPTIONS_GHC -Wall #-}
module B where

import A
import Language.Haskell.Liquid.ProofCombinators

{-@ simple :: { 1 == 1 } @-}
$(genSimple)

B.hs compiles, and LH deems it safe. But unfortunately, it's not warning-free:

$ stack --docker exec ghci -- B.hs
GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
[1 of 2] Compiling A                ( A.hs, interpreted )
[2 of 2] Compiling B                ( B.hs, interpreted )

B.hs:10:1: Warning:
    The import of ‘Language.Haskell.Liquid.ProofCombinators’ is redundant
      except perhaps to import instances from ‘Language.Haskell.Liquid.ProofCombinators’
    To import instances alone, use: import Language.Haskell.Liquid.ProofCombinators()
Ok, modules loaded: B, A.

From GHC's perspective, this makes sense, since it isn't aware that LH is making use of the import Language.Haskell.Liquid.ProofCombinators. I attempted to squash this warning by changing B.hs like so:

import Language.Haskell.Liquid.ProofCombinators ()

Unfortunately, LH doesn't like this:

$ stack --docker exec liquid -- B.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/.stack-work/install/x86_64-linux-dkc06df8944aa1430a10f19c84f6dae333/lts-6.27/7.10.3/share/x86_64-linux-ghc-7.10.3/liquidhaskell-0.7.0.0/include/Language/Haskell/Liquid/ProofCombinators.hs:210:23: Error: GHC Error

 210 | {-@ instance OptGt a (Proof -> b) where
                             ^

     Not in scope: type constructor or class ` Proof '

Is there a reason why the refinements for Proof require a full-blown import Language.Haskell.Liquid.ProofCombinators? As thing stand currently, it's impossible for me to simultaneously be -Wall-clean and have LH work properly in this scenario.

[nikivazou]

What id you replace Proof with () in the instance declaration?

[RyanGlScott]

That would work around that particular issue, but this isn't really the full extent of the sort of thing I want to do with Template Haskell. Let's tweak the original example:

module Foo (Foo(..)) where

data Foo = Foo

-- A.hs
{-@ LIQUID "--higherorder"    @-}
{-@ LIQUID "--totality"       @-}
{-@ LIQUID "--exactdc"        @-}
{-# LANGUAGE TemplateHaskell #-}
module A (genSimple) where

import Foo (Foo(..))

import Language.Haskell.Liquid.ProofCombinators
import Language.Haskell.TH

genSimple :: Q [Dec]
genSimple = [d| simple :: Foo -> Foo -> Proof; simple x@Foo y@Foo = x ==. y *** QED  |]

-- B.hs
{-@ LIQUID "--higherorder"    @-}
{-@ LIQUID "--totality"       @-}
{-@ LIQUID "--exactdc"        @-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wall #-}
module B where

import A
import Foo (Foo(..))
import Language.Haskell.Liquid.ProofCombinators

{-@ simple :: x:Foo -> y:Foo ->  { x == y } @-}
$(genSimple)

Running liquid on B works, but if you compile B, you get:

$ stack --docker exec ghci -- B.hs
GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
[1 of 3] Compiling Foo              ( Foo.hs, interpreted )
[2 of 3] Compiling A                ( A.hs, interpreted )
[3 of 3] Compiling B                ( B.hs, interpreted )

B.hs:10:1: Warning:
    The import of ‘Foo’ is redundant
      except perhaps to import instances from ‘Foo’
    To import instances alone, use: import Foo()

B.hs:11:1: Warning:
    The import of ‘Language.Haskell.Liquid.ProofCombinators’ is redundant
      except perhaps to import instances from ‘Language.Haskell.Liquid.ProofCombinators’
    To import instances alone, use: import Language.Haskell.Liquid.ProofCombinators()

And similarly, you can't just comment out the redunant Foo import, since LH relies on it:

$ stack --docker exec liquid -- B.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/B.hs:13:17: Error: GHC Error

 13 | {-@ simple :: x:Foo -> y:Foo ->  { x == y } @-}
                      ^

     Not in scope: type constructor or class ` Foo '

[nikivazou]

Can't you make genSimple generate the comments with the code? That way the specification will get created in the same module as the function definition

[RyanGlScott]

Sadly, Template Haskell currently has no representation of comments, so that's not feasible at the moment.

[nikivazou]

So, what happens if you edit genSimple to

genSimple = [d|{-@ simple :: x:Foo -> y:Foo ->  { x == y } @-} simple :: Proof; simple = trivial |]

Well, this issue will be closed when Template Haskell supports comment generation, since it is just a warning I do not think I can fix it :(

[RyanGlScott]

Adding a comment to a Template Haskell splice is simply ignored with how TH currently operates.

Well, this issue will be closed when Template Haskell supports comment generation, since it is just a warning I do not think I can fix it

Let me be clear here, since I believe the problem is on LH's end, not GHC's. GHC is perfectly justified in claiming that import Foo is redundant. It's LH that is being too picky about where it gets its refinements for the Foo datatype. It demands that you have:

import Foo

Whereas if you have

import Foo ()

LH will refuse to find the refinements. I claim that this is too conservative of an approach. Why should LH not discover the refinements for Foo in the latter case? It's silly to not find them if you selective your imports with parentheses, since you can't selectively import refinements in the first place!

I propose that whenever LH sees an import of a module, regardless of whether it is qualified or not, that it automatically brings in all refinements defined in that module, as well as the ones transitively imported from that module. That is, make refinements work more like typeclass instances. That would resolve this issue and avoid the need to hack GHC directly.

[nikivazou]

This makes sense!

But my counter suggestion is to make Template Haskell generate comments when it generates code that has comments. Then, the spec for simple will live in module A with its definition and ghc will not complain!