Confusing interaction with boot files and --exact-data-cons

[facundominguez]

The following three files make LH fail.

-- ArrayImpl.hs
{-@ LIQUID "--reflection"  @-}
module ArrayImpl where
data Array a = Arr {  lst   :: [a] }

-- Array.hs-boot
module Array where
import ArrayImpl

-- Array.hs
module Array where
import ArrayImpl

$ cabal exec ghc -- -fplugin=LiquidHaskell Array.hs
[2 of 3] Compiling Array[boot]      ( Array.hs-boot, Array.o-boot )
ArrayImpl.hs:3:16: error:
    Illegal type specification for `ArrayImpl.Arr`
    ArrayImpl.Arr :: forall a##aE4 .
                     lqdc##$select##ArrayImpl.Arr##1##ArrayImpl.Arr:[a##aE4] -> {VV : (ArrayImpl.Array a##aE4) | is$ArrayImpl.Arr VV
                                                                                                                 && ArrayImpl.Arr##lqdc##$select##ArrayImpl.Arr##1 VV == lqdc##$select##ArrayImpl.Arr##1##ArrayImpl.Arr}
    Sort Error in Refinement: {VV : (ArrayImpl.Array a##aE4##xo) | is$ArrayImpl.Arr VV
                                                                   && ArrayImpl.Arr##lqdc##$select##ArrayImpl.Arr##1 VV == lqdc##$select##ArrayImpl.Arr##1##ArrayImpl.Arr}
    Unbound symbol is$ArrayImpl.Arr --- perhaps you meant: ArrayImpl.Arr ?
    Just assume
  |
3 | data Array a = Arr {  lst   :: [a] }
  |

Any of the following actions makes LH succeed:

• Remove Array.hs-boot
• Remove {-@ LIQUID "--reflection" @-} from ArrayImpl.hs
• Add {-@ LIQUID "--exact-data-cons" @-} to both Array.hs and Array.hs-boot

This issue probably ties to the others about --exact-data-cons/--exactdc.

Credit to @ulysses4ever for distilling this failing example.