[ fix ] Forward data declarations are linear

src/TTImp/ProcessData.idr

@@ -425,7 +425,7 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpLater dfc n_in ty_raw)
          arity <- getArity defs [] fullty
 
          -- Add the type constructor as a placeholder
-         tidx <- addDef n (newDef fc n linear vars fullty def_vis
+         tidx <- addDef n (newDef fc n top vars fullty def_vis
                           (TCon 0 arity [] [] defaultFlags [] Nothing Nothing))
          addMutData (Resolved tidx)
          defs <- get Ctxt

tests/idris2/data/data005/Issue1204.idr

@@ -0,0 +1,8 @@
+data Tm = Foo Nat
+
+mutual
+  Env : Type
+  Env = List Clos
+
+  data Clos : Type where
+    Cl : Tm -> Env -> Clos

tests/idris2/data/data005/Issue586.idr

@@ -0,0 +1,9 @@
+mutual
+  public export
+  ListT : (m : Type -> Type) -> (a : Type) -> Type
+  ListT m a = m (ListStruct m a)
+
+  public export
+  data ListStruct : (m : Type -> Type) -> (a : Type) -> Type where
+    Nil  : ListStruct m a
+    (::) : a -> ListT m a -> ListStruct m a

tests/idris2/data/data005/Issue586b.idr

@@ -0,0 +1,5 @@
+data X : Type
+data Y : Type -> Type
+
+f : Type
+f = Y X

tests/idris2/data/data005/expected

@@ -0,0 +1,3 @@
+1/1: Building Issue586 (Issue586.idr)
+1/1: Building Issue586b (Issue586b.idr)
+1/1: Building Issue1204 (Issue1204.idr)

tests/idris2/data/data005/run

@@ -0,0 +1,5 @@
+. ../../../testutils.sh
+
+check Issue586.idr
+check Issue586b.idr
+check Issue1204.idr