LH chokes on type / constructor that is only used in spec, not in terms

[gergoerdi]

As of d5e4003, given the following module:

{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE CPP #-}
module Liquid.Prelude () where

import GHC.Types(Bool(..))

{-@
embed Bool as bool
assume True  :: {v:Bool | v     }
assume False :: {v:Bool | (~ v) }
@-}

#if ADD_BOGUS_TERM
_x = True
#else

This fails as-is, but passes with -DADD_BOGUS_TERM:

[mi@scbbox liquidhaskell.upstream]$ cabal exec -- ghc -fforce-recomp -fplugin=LiquidHaskellBoot input/Liquid/Prelude.hs
Loaded package environment from /home/mi/prog/liquidhaskell.upstream/dist-newstyle/tmp/environment.-34699/.ghc.environment.x86_64-linux-9.10.1
[1 of 1] Compiling Liquid.Prelude   ( input/Liquid/Prelude.hs, input/Liquid/Prelude.o )
input/Liquid/Prelude.hs:10:8: error:
    Unknown variable `False`
    resolveAsmVar-True
   |
10 | assume False :: {v:Bool | (~ v) }
   |        ^^^^^^

[mi@scbbox liquidhaskell.upstream]$ cabal exec -- ghc -fforce-recomp -fplugin=LiquidHaskellBoot -DADD_BOGUS_TERM input/Liquid/Prelude.hs
Loaded package environment from /home/mi/prog/liquidhaskell.upstream/dist-newstyle/tmp/environment.-34720/.ghc.environment.x86_64-linux-9.10.1
[1 of 1] Compiling Liquid.Prelude   ( input/Liquid/Prelude.hs, input/Liquid/Prelude.o )

**** LIQUID: SAFE (0 constraints checked) **************************************

[gergoerdi]

You don't even have to use the constructors, just using the type is enough of a workaround:

{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE CPP #-}
module Liquid.Prelude () where

import GHC.Types(Bool(..))

{-@
embed Bool as bool
assume True  :: {v:Bool | v     }
assume False :: {v:Bool | (~ v) }
@-}

#if ADD_BOGUS_TERM
_f :: Bool -> Bool
_f x = x
#endif