Cannot reflect GADT definition using DataKinds

[zgrannan]

Minimal example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

data Nat = Z | S Nat

data Op a b where
  Pop  :: Op ('S n) n

{-@
data Op a b where
    Pop  :: Op ('S n) n
@-}

yields the following error:

Op.hs:10:6-8: error:  Bad Data Specification
GHC and Liquid specifications have different numbers of type variables for `Main.Pop`

I suppose this code is to blame but I don't know anything about how Haskell handles GADTs:

https://github.com/ucsd-progsys/liquidhaskell/blob/0808cc61ce7a28fcab47213b03cf6449017a17b2/src/Language/Haskell/Liquid/Bare/Plugged.hs#L107-L108

[zgrannan]

Hmm, maybe this is unrelated, but a similar error also occurs without GADT:

data Op = Foo Op Op

{-@
data Op = Foo Op Op
@-}

yields:

GHC and Liquid specifications have different numbers of fields for `Op.Foo`

[ranjitjhala]

hmm i feel i've seen this before? what's the minimal example with the second case? (data Op = Foo Op Op)

[zgrannan]

@ranjitjhala The above code is in fact a minimal example. Here's a link (not sure what version of LH is used here, but it happens locally on develop for me as well): http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1598510506_12922.hs

I am no longer blocked on this however, because LH is able to use the Foo ADT fine without also putting it in the liquid comments.

[kosmikus]

Sorry, at the moment this is also just speculation, but I know there was a parser bug for data declarations, which should be fixed in my parser PR. So if you could try this with #1704, this would be helpful. But I could understand if that's too much work to try, and I will hopefully get around to it myself eventually.

[kosmikus]

In particular, I believe at least the second one to be caused by #871. Not sure if the first example is also an instance of the same problem.

[nikivazou]

The second one is actually strange (I did not expect the first one to work...) It is not urgent, so @kosmikus when you eventually find the time to work on the new parser you can include it in the tests.

[kosmikus]

@nikivazou IIRC, the problem at least in the second case is that the (old/current) parser incorrectly turns this into data Op = Foo (Op Op).

[nikivazou]

Then the generated error makes sense!

[zgrannan]

@kosmikus I can confirm that https://github.com/ucsd-progsys/liquidhaskell/pull/1704 fixes the second case :)