fix for ucsd-progsys#2349

Author: nikivazou

liquidhaskell-boot/src/Language/Haskell/Liquid/Types/PredType.hs

@@ -192,8 +192,9 @@ dcWrapSpecType allowTC dc (DataConP _ _ vs ps cs yts rt _ _ _)
     ts'      = map ("" , classRFInfo allowTC , , mempty) cs ++ yts'
     subst    = F.mkSubst [(x, F.EVar y) | (x, y) <- zip as bs]
     rt'      = F.subst subst rt
-    makeVars = zipWith (\v a -> RTVar v (rTVarInfo a :: RTVInfo RSort)) vs (fst $ splitForAllTyCoVars $ dataConRepType dc)
-    makeVars' = map (, mempty) makeVars
+    makeVars = filter (`elem` fvs) $ zipWith (\v a -> RTVar v (rTVarInfo a :: RTVInfo RSort)) vs (fst $ splitForAllTyCoVars $ dataConRepType dc)
+    makeVars' = map (, mempty) makeVars 
+    fvs = freeTyVars $ mkArrow [] ps ts' rt'  
 
 instance PPrint TyConP where
   pprintTidy k tc = "data" <+> pprintTidy k (tcpCon tc)

tests/pos/T2349.hs

@@ -0,0 +1,17 @@
+{-# 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 :: xxxxx:_ -> head:Expr t -> tail:Expr {v:[t] | len v = xxxxx} ->
+          Expr {v:[t] | len v = xxxxx+1}
+@-}