"Unbound symbol" when using GADTs

[pacastega]

With the following code

{-# LANGUAGE GADTs #-}
{-@ LIQUID "--reflection" @-}
module TestModule where

data Expr t where
  I :: Int -> Expr Int

  NIL :: Expr [t]
  CONS :: Int -> Expr t -> Expr [t] -> Expr [t]

{-@
data Expr t where
  I :: Int -> Expr Int

  NIL :: Expr {v:[t] | len v = 0}
  CONS :: l:Nat -> head:Expr t -> tail:Expr {v:[t] | len v = l} ->
          Expr {v:[t] | len v = l+1}
@-}

I am getting an error about l being unbound:

    Illegal type specification for `TestModule.$WCONS`
    TestModule.$WCONS :: forall t .
                         x1:GHC.Types.Int -> head##TestModule.CONS:(TestModule.Expr t) -> tail##TestModule.CONS:(TestModule.Expr {VV : [t] | len VV == l##TestModule.CONS}) -> {VV : (TestModule.Expr {VV : [t] | len VV == l##TestModule.CONS + 1}) | is$TestModule.CONS VV
                                                                                                                                                                                                                                                       && not (is$TestModule.I VV)
                                                                                                                                                                                                                                                       && not (is$TestModule.NIL VV)
                                                                                                                                                                                                                                                       && lqdc##$select##TestModule.CONS##1 VV == x1
                                                                                                                                                                                                                                                       && lqdc##$select##TestModule.CONS##2 VV == head##TestModule.CONS
                                                                                                                                                                                                                                                       && lqdc##$select##TestModule.CONS##3 VV == tail##TestModule.CONS}
    Sort Error in Refinement: {VV : [t##X0] | len VV == l##TestModule.CONS}
    Unbound symbol l##TestModule.CONS --- perhaps you meant: TestModule.CONS, is$TestModule.CONS ?
    Just constructor
  |
9 |   CONS :: Int -> Expr t -> Expr [t] -> Expr [t]
  |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[facundominguez]

The error is not helpful, but LH doesn't check the output of GADTs at the moment. See for instance #2090. Even if you could write such a specification, then LH wouldn't check the type of the result.

[nikivazou]

Actually, we have a short discussion with @goldfirere at ICFP about a related issue.

The real problem here is that the GHC and liquid type for the worker types of the GADT worker constructors (e.g., $WCONS) do not match so the refinements are ignored. So, it would be good to understand the GHC rules for the generation of such types and update the generation of the refinement types.