content: {-@ LIQUID "--expect-error-containing=Data constructors in refinement do not match original datatype for `EntityField`" @-}
  {-@ LIQUID "--no-adt"         @-}
  {-@ LIQUID "--exact-data-con" @-}
  
  {-# LANGUAGE ExistentialQuantification, KindSignatures, TypeFamilies, GADTs #-}
  
  module BadData1 where
  
  class PersistEntity record where
      data EntityField record :: * -> *
  
  -- The reason this fails is because the refinement uses 'record'
  -- instead of 'Blob'. Therefore, the lookup for the GHC datatype
  -- will return no constructors, and consequently, LH complains
  -- that our refinement has two.
  --
  instance PersistEntity Blob where
      {-@ data EntityField record typ where
             BlobXVal :: EntityField Blob {v:Int | v >= 0}
             BlobYVal :: EntityField Blob Int
      @-}
      data EntityField Blob typ where
          BlobXVal :: EntityField Blob Int
          BlobYVal :: EntityField Blob Int
  
  
  {-@ data Blob  = B { xVal :: {v:Int | v >= 0}, yVal :: Int } @-}
  data Blob = B { xVal :: Int, yVal :: Int }
  
  {-@ blobXVal :: EntityField Blob {v:Int | v >= 0} @-}
  blobXVal :: EntityField Blob Int
  blobXVal = BlobXVal
  
  -- OK
  -- testUpdateQuery :: () -> Update Blob Int
  -- testUpdateQuery () = createUpdate blobXVal 3
  
  -- BAD
  -- testUpdateQueryFail :: () -> Update Blob Int
  -- testUpdateQueryFail () = createUpdate blobXVal (-1)
  
  main :: IO ()
  main = pure ()
  