Can't factor out axiomatized definition into a separate module

[RyanGlScott]

LH deems this safe:

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

import Language.Haskell.Liquid.ProofCombinators

data U1 p = U1

{-@ axiomatize compose @-}
compose :: (b -> c) -> (a -> b) -> a -> c
compose f g x = f (g x)

{-@ axiomatize fmapU1 @-}
fmapU1 :: (p -> q) -> U1 p -> U1 q
fmapU1 _ _ = U1

{-@ fmapU1Compose :: f:(q -> r)
                  -> g:(p -> q)
                  -> x:U1 p
                  -> { fmapU1 (compose f g) x == compose (fmapU1 f) (fmapU1 g) x }
@-}
fmapU1Compose :: (q -> r) -> (p -> q)
              -> U1 p -> Proof
fmapU1Compose f g x
  =   fmapU1 (compose f g) x
  ==. U1
  ==. fmapU1 f (fmapU1 g x)
  ==. compose (fmapU1 f) (fmapU1 g) x
  *** QED

But if you try factoring out compose into a separate module:

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

{-@ axiomatize compose @-}
compose :: (b -> c) -> (a -> b) -> a -> c
compose f g x = f (g x)

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

import Compose
import Language.Haskell.Liquid.ProofCombinators

data U1 p = U1

{-@ axiomatize fmapU1 @-}
fmapU1 :: (p -> q) -> U1 p -> U1 q
fmapU1 _ _ = U1

{-@ fmapU1Compose :: f:(q -> r)
                  -> g:(p -> q)
                  -> x:U1 p
                  -> { fmapU1 (compose f g) x == compose (fmapU1 f) (fmapU1 g) x }
@-}
fmapU1Compose :: (q -> r) -> (p -> q)
              -> U1 p -> Proof
fmapU1Compose f g x
  =   fmapU1 (compose f g) x
  ==. U1
  ==. fmapU1 f (fmapU1 g x)
  ==. compose (fmapU1 f) (fmapU1 g) x
  *** QED

Then LH deems it unsafe:

$ stack exec liquid -- Bug.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 ***************************************************

Done solving.
RESULT: Unsafe [Just 4]

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

**** RESULT: UNSAFE ************************************************************

 /home/rgscott/Documents/Hacking/Haskell/verified-instances/generic-proofs/Bug.hs:(23,7)-(27,9): Error: Liquid Type Mismatch
   Inferred type
     VV : ()

   not a subtype of Required type
     VV : {VV : () | Bug.fmapU1 (Compose.compose f g) x == Compose.compose (Bug.fmapU1 f) (Bug.fmapU1 g) x}

   In Context
     x : (U1 a)

[ranjitjhala]

Aargh -- I know what this is. It may shock you that in your case, adding:

{-@ LIQUID "--automatic-instances=liquidinstances" @-}

to the Bug.hs works. In fact, just

{-@ LIQUID "--higherorder"    @-}
{-@ LIQUID "--totality"       @-}
{-@ LIQUID "--exactdc"        @-}
{-@ LIQUID "--automatic-instances=liquidinstances" @-}

module Bug where

import Compose
import Language.Haskell.Liquid.ProofCombinators

data U1 p = U1

{-@ axiomatize fmapU1 @-}
fmapU1 :: (p -> q) -> U1 p -> U1 q
fmapU1 _ _ = U1

{-@ fmapU1Compose :: f:(q -> r)
                  -> g:(p -> q)
                  -> x:U1 p
                  -> { fmapU1 (compose f g) x == compose (fmapU1 f) (fmapU1 g) x }
@-}
fmapU1Compose :: (q -> r) -> (p -> q)
              -> U1 p -> Proof
fmapU1Compose f g x
  = trivial 

works :)

But anyways, will fix this perhaps first thing tomorrow (so your code works properly.)