Empty data declarations are confused with forward data declarations

src/Core/Binary.idr

@@ -29,7 +29,7 @@ import public Libraries.Utils.Binary
 ||| version number if you're changing the version more than once in the same day.
 export
 ttcVersion : Int
-ttcVersion = 2024_10_30_00
+ttcVersion = 2025_01_30_00
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Core/Case/Util.idr

@@ -20,7 +20,7 @@ getCons : {auto c : Ref Ctxt Defs} ->
 getCons defs (NTCon _ tn _ _ _)
     = case !(lookupDefExact tn (gamma defs)) of
            Just (TCon _ _ _ _ _ _ cons _) =>
-                do cs' <- traverse addTy cons
+                do cs' <- traverse addTy (fromMaybe [] cons)
                    pure (catMaybes cs')
            _ => throw (InternalError "Called `getCons` on something that is not a Type constructor")
   where

src/Core/Context.idr

@@ -585,9 +585,9 @@ HasNames Def where
       fullNamesPat (_ ** (env, lhs, rhs))
           = pure $ (_ ** (!(full gam env),
                           !(full gam lhs), !(full gam rhs)))
-  full gam (TCon t a ps ds u ms cs det)
+  full gam (TCon t a ps ds u ms mcs det)
       = pure $ TCon t a ps ds u !(traverse (full gam) ms)
-                                !(traverse (full gam) cs) det
+                                !(traverseOpt (traverse (full gam)) mcs) det
   full gam (BySearch c d def)
       = pure $ BySearch c d !(full gam def)
   full gam (Guess tm b cs)
@@ -603,9 +603,9 @@ HasNames Def where
       resolvedNamesPat (_ ** (env, lhs, rhs))
           = pure $ (_ ** (!(resolved gam env),
                           !(resolved gam lhs), !(resolved gam rhs)))
-  resolved gam (TCon t a ps ds u ms cs det)
+  resolved gam (TCon t a ps ds u ms mcs det)
       = pure $ TCon t a ps ds u !(traverse (resolved gam) ms)
-                                !(traverse (resolved gam) cs) det
+                                !(traverseOpt (traverse (full gam)) mcs) det
   resolved gam (BySearch c d def)
       = pure $ BySearch c d !(resolved gam def)
   resolved gam (Guess tm b cs)

src/Core/Context/Context.idr

@@ -101,7 +101,7 @@ data Def : Type where
            (detpos : List Nat) -> -- determining arguments
            (flags : TypeFlags) -> -- should 'auto' implicits check
            (mutwith : List Name) ->
-           (datacons : List Name) ->
+           (datacons : Maybe (List Name)) ->
            (detagabbleBy : Maybe (List Nat)) ->
                     -- argument positions which can be used for
                     -- detagging, if it's possible (to check if it's

src/Core/Context/Data.idr

@@ -104,7 +104,7 @@ addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons)
                             (TCon tag arity
                                   paramPositions
                                   allPos
-                                  defaultFlags [] (map name datacons) Nothing)
+                                  defaultFlags [] (Just $ map name datacons) Nothing)
          (idx, gam') <- addCtxt tyn tydef (gamma defs)
          gam'' <- addDataConstructors 0 datacons gam'
          put Ctxt ({ gamma := gam'' } defs)

src/Core/Context/Pretty.idr

@@ -57,7 +57,7 @@ namespace Raw
           ([ "tag:" <++> byShow tag
            , "arity:" <++> byShow arity
            , "parameter positions:" <++> byShow ps
-           , "constructors:" <++> enum ((\ nm => annotate (Syntax $ DCon (Just nm)) (pretty0 nm)) <$> cons)
+           , "constructors:" <++> enum ((\ nm => annotate (Syntax $ DCon (Just nm)) (pretty0 nm)) <$> fromMaybe [] cons)
            ] ++ (("mutual with:" <++> enum (pretty0 <$> ms)) <$ guard (not $ null ms))
              ++ (maybe [] (\ pos => ["detaggable by:" <++> byShow pos]) det))
   prettyDef (ExternDef arity) =
@@ -109,7 +109,7 @@ namespace Resugared
           ([ "tag:" <++> byShow tag
            , "arity:" <++> byShow arity
            , "parameter positions:" <++> byShow ps
-           , "constructors:" <++> enum ((\ nm => annotate (Syntax $ DCon (Just nm)) (pretty0 nm)) <$> cons)
+           , "constructors:" <++> enum ((\ nm => annotate (Syntax $ DCon (Just nm)) (pretty0 nm)) <$> fromMaybe [] cons)
            ] ++ (("mutual with:" <++> enum (pretty0 <$> ms)) <$ guard (not $ null ms))
              ++ (maybe [] (\ pos => ["detaggable by:" <++> byShow pos]) det))
   prettyDef (ExternDef arity) = pure $

src/Core/Coverage.idr

@@ -138,7 +138,8 @@ isEmpty defs env (NTCon fc n t a args)
   = do Just nty <- lookupDefExact n (gamma defs)
          | _ => pure False
        case nty of
-            TCon _ _ _ _ flags _ cons _
+            TCon _ _ _ _ flags _ Nothing _ => pure False
+            TCon _ _ _ _ flags _ (Just cons) _
                  => if not (external flags)
                        then allM (conflict defs env (NTCon fc n t a args)) cons
                        else pure False

src/Core/Termination/Positivity.idr

@@ -166,6 +166,7 @@ calcPositive loc n
          logC "totality.positivity" 6 $ do pure $ "Calculating positivity: " ++ show !(toFullNames n)
          case !(lookupDefTyExact n (gamma defs)) of
               Just (TCon _ _ _ _ _ tns dcons _, ty) =>
+                  let dcons = fromMaybe [] dcons in
                   case !(totRefsIn defs ty) of
                        IsTerminating =>
                             do log "totality.positivity" 30 $

src/Idris/Doc/String.idr

@@ -424,7 +424,7 @@ getDocsForName fc n config
            TCon _ _ _ _ _ _ cons _ =>
              do let tot = catMaybes [ showTotal (totality d)
                                     , pure (showVisible (collapseDefault $ visibility d))]
-                cdocs <- traverse (getDConDoc <=< toFullNames) cons
+                cdocs <- traverse (getDConDoc <=< toFullNames) (fromMaybe [] cons)
                 cdoc <- case cdocs of
                   [] => pure (Just "data", [])
                   [doc] =>

src/TTImp/Elab/App.idr

@@ -394,7 +394,7 @@ mutual
                 | Nothing => pure Nothing
                 let (TCon _ _ _ _ _ _ datacons _) = gdef.definition
                 | _ => pure Nothing
-                pure (Just (length datacons))
+                pure (length <$> datacons)
         else pure Nothing
       countConstructors _ = pure Nothing
 

src/TTImp/Elab/Record.idr

@@ -79,7 +79,7 @@ toRHS fc r = snd (toRHS' fc r)
 findConName : Defs -> Name -> Core (Maybe Name)
 findConName defs tyn
     = case !(lookupDefExact tyn (gamma defs)) of
-           Just (TCon _ _ _ _ _ _ [con] _) => pure (Just con)
+           Just (TCon _ _ _ _ _ _ (Just [con]) _) => pure (Just con)
            _ => pure Nothing
 
 findFieldsAndTypeArgs : {auto c : Ref Ctxt Defs} ->

src/TTImp/Elab/RunElab.idr

@@ -311,7 +311,7 @@ elabScript rig fc nest env script@(NDCon nfc nm t ar args) exp
              Just (TCon _ _ _ _ _ _ cons _) <-
                      lookupDefExact cn (gamma defs)
                  | _ => failWith defs $ show cn ++ " is not a type"
-             scriptRet cons
+             scriptRet $ fromMaybe [] cons
     elabCon defs "GetReferredFns" [n]
         = do dn <- reify defs !(evalClosure defs n)
              Just def <- lookupCtxtExact dn (gamma defs)

src/TTImp/Interactive/CaseSplit.idr

@@ -110,7 +110,7 @@ findCons n lhs
                                                ("Not a type constructor " ++
                                                   show res)))
                              pure (OK (fn, !(toFullNames tyn),
-                                           !(traverse toFullNames cons)))
+                                           !(traverse toFullNames $ fromMaybe [] cons)))
 
 findAllVars : Term vars -> List Name
 findAllVars (Bind _ x (PVar _ _ _ _) sc)

src/TTImp/Interactive/ExprSearch.idr

@@ -688,7 +688,7 @@ tryIntermediateRec fc rig opts hints env ty topty (Just rd)
         = isSingleCon defs !(sc defs (toClosure defaultOpts []
                                               (Erased fc Placeholder)))
     isSingleCon defs (NTCon _ n _ _ _)
-        = do Just (TCon _ _ _ _ _ _ [con] _) <- lookupDefExact n (gamma defs)
+        = do Just (TCon _ _ _ _ _ _ (Just [con]) _) <- lookupDefExact n (gamma defs)
                   | _ => pure False
              pure True
     isSingleCon _ _ = pure False

src/TTImp/Interactive/Intro.idr

@@ -50,7 +50,7 @@ parameters
     let TCon _ _ _ _ _ _ cs _ = definition gdef
       | _ => pure []
     let gty = gnf env ty
-    ics <- for cs $ \ cons => do
+    ics <- for (fromMaybe [] cs) $ \ cons => do
       Just gdef <- lookupCtxtExact cons (gamma defs)
         | _ => pure Nothing
       let nargs = lengthExplicitPi $ fst $ snd $ underPis (-1) [] (type gdef)

src/TTImp/ProcessBuiltin.idr

@@ -154,7 +154,7 @@ isNatural fc n = do
         | Nothing => undefinedName EmptyFC n
     let TCon _ _ _ _ _ _ cons _ = gdef.definition
         | _ => pure False
-    consDefs <- getConsGDef fc cons
+    consDefs <- getConsGDef fc (fromMaybe [] cons)
     pure $ all hasNatFlag consDefs
   where
     isNatFlag : DefFlag -> Bool
@@ -225,7 +225,7 @@ processBuiltinNatural fc name = do
     let TCon _ _ _ _ _ _ dcons _ = gdef.definition
         | def => throw $ GenericMsg fc
             $ "Expected a type constructor, found " ++ showDefType def ++ "."
-    cons <- getConsGDef fc dcons
+    cons <- getConsGDef fc (fromMaybe [] dcons)
     checkNatCons ds.gamma cons n fc
 
 ||| Check a `%builtin NaturalToInteger` pragma is correct.

src/TTImp/ProcessData.idr

@@ -426,7 +426,7 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpLater dfc n_in ty_raw)
 
          -- Add the type constructor as a placeholder
          tidx <- addDef n (newDef fc n linear vars fullty def_vis
-                          (TCon 0 arity [] [] defaultFlags [] [] Nothing))
+                          (TCon 0 arity [] [] defaultFlags [] Nothing Nothing))
          addMutData (Resolved tidx)
          defs <- get Ctxt
          traverse_ (\n => setMutWith fc n (mutData defs)) (mutData defs)
@@ -499,7 +499,7 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw o
                       _ => pure $ mbtot <|> declTot
 
                     case definition ndef of
-                      TCon _ _ _ _ _ mw [] _ => case mfullty of
+                      TCon _ _ _ _ flags mw Nothing _ => case mfullty of
                         Nothing => pure (mw, vis, tot, type ndef)
                         Just fullty =>
                             do ok <- convert defs [] fullty (type ndef)
@@ -516,7 +516,7 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw o
          -- Add the type constructor as a placeholder while checking
          -- data constructors
          tidx <- addDef n (newDef fc n linear vars fullty (specified vis)
-                          (TCon 0 arity [] [] defaultFlags [] [] Nothing))
+                          (TCon 0 arity [] [] defaultFlags [] Nothing Nothing))
          case vis of
               Private => pure ()
               _ => do addHashWithNames n

src/TTImp/ProcessRecord.idr

@@ -26,7 +26,7 @@ import Data.String
 %default covering
 
 -- Used to remove the holes so that we don't end up with "hole is already defined"
--- errors because they've been duplicarted when forming the various types of the
+-- errors because they've been duplicated when forming the various types of the
 -- record constructor, getters, etc.
 killHole : RawImp -> RawImp
 killHole (IHole fc str) = Implicit fc True
@@ -145,10 +145,12 @@ elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conNa
     preElabAsData tn
         = do let fc = virtualiseFC fc
              let dataTy = IBindHere fc (PI erased) !(bindTypeNames fc [] vars (mkDataTy fc params0))
-             -- we don't use MkImpLater because users may have already declared the record ahead of time
-             let dt = MkImpData fc tn (Just dataTy) opts []
-             log "declare.record" 10 $ "Pre-declare record data type: \{show dt}"
-             processDecl [] nest env (IData fc def_vis mbtot dt)
+             defs <- get Ctxt
+             -- Create a forward declaration if none exists
+             when (isNothing !(lookupTyExact tn (gamma defs))) $ do
+               let dt = MkImpLater fc tn dataTy
+               log "declare.record" 10 $ "Pre-declare record data type: \{show dt}"
+               processDecl [] nest env (IData fc def_vis mbtot dt)
              defs <- get Ctxt
              Just ty <- lookupTyExact tn (gamma defs)
                | Nothing => throw (InternalError "Missing data type \{show tn}, despite having just declared it!")

tests/idris2/data/data003/Issue3457.idr

@@ -0,0 +1,11 @@
+data Three = A | B | C
+data Bar : Type
+data Foo : Type where
+  MkFoo : Three -> Bar -> Foo
+
+fun : Foo -> String
+fun (MkFoo A y) = ""
+fun (MkFoo B y) = ""
+
+data Bar : Type where
+  MkBar : Bar

tests/idris2/data/data003/OopsDef.idr

@@ -0,0 +1,10 @@
+module OopsDef
+
+%default total
+
+public export
+data Oops : Type
+
+forcePosCheck : Oops -> Oops
+forcePosCheck x = x
+

tests/idris2/data/data003/OopsRef.idr

@@ -0,0 +1,9 @@
+import OopsDef
+
+%default total
+
+failing "Oops is not total, not strictly positive"
+
+  data OopsDef.Oops : Type where
+    MkFix : Not Oops -> Oops
+

tests/idris2/data/data003/Positivity.idr

@@ -0,0 +1,9 @@
+%default total
+
+data Negation : Type -> Type
+
+failing "Absurd is not total, not strictly positive"
+
+  data Absurd : Type -> Type where
+    MkAbsurd : Negation (Absurd a) -> Absurd a
+

tests/idris2/data/data003/Test.idr

@@ -0,0 +1,8 @@
+data Bar : Type
+
+total
+foo : Bar -> a
+foo x impossible
+
+data Bar : Type where
+    MkBar : Bar

tests/idris2/data/data003/Test2.idr

@@ -0,0 +1,4 @@
+data Bar : Type where
+
+data Bar : Type where
+    MkBar : Bar

tests/idris2/data/data003/expected

@@ -0,0 +1,35 @@
+1/1: Building Test (Test.idr)
+Error: foo x is not a valid impossible case.
+
+Test:5:1--5:17
+ 1 | data Bar : Type
+ 2 | 
+ 3 | total
+ 4 | foo : Bar -> a
+ 5 | foo x impossible
+     ^^^^^^^^^^^^^^^^
+
+1/1: Building Test2 (Test2.idr)
+Error: Main.Bar is already defined.
+
+Test2:3:1--4:16
+ 3 | data Bar : Type where
+ 4 |     MkBar : Bar
+
+1/1: Building Issue3457 (Issue3457.idr)
+Error: fun is not covering.
+
+Issue3457:6:1--6:20
+ 2 | data Bar : Type
+ 3 | data Foo : Type where
+ 4 |   MkFoo : Three -> Bar -> Foo
+ 5 | 
+ 6 | fun : Foo -> String
+     ^^^^^^^^^^^^^^^^^^^
+
+Missing cases:
+    fun (MkFoo C _)
+
+1/1: Building Positivity (Positivity.idr)
+1/2: Building OopsDef (OopsDef.idr)
+2/2: Building OopsRef (OopsRef.idr)

tests/idris2/data/data003/run

@@ -0,0 +1,7 @@
+. ../../../testutils.sh
+
+check Test.idr
+check Test2.idr
+check Issue3457.idr
+check Positivity.idr
+check OopsRef.idr