From 04f8df2a75e74046f1ed697ae3bd2290736a3a99 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Wed, 29 Jan 2025 19:59:31 -0800 Subject: [PATCH 1/6] [ fix ] Don't allow redefinition of empty data --- src/Core/Binary.idr | 2 +- src/Core/Context/Context.idr | 3 ++- src/Core/TTC.idr | 4 +++- src/TTImp/ProcessData.idr | 6 ++++-- 4 files changed, 10 insertions(+), 5 deletions(-) diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index e242cc777b..21e85678b4 100644 --- a/src/Core/Binary.idr +++ b/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_29_00 export checkTTCVersion : String -> Int -> Int -> Core () diff --git a/src/Core/Context/Context.idr b/src/Core/Context/Context.idr index 6abf0e08f8..c096c14b46 100644 --- a/src/Core/Context/Context.idr +++ b/src/Core/Context/Context.idr @@ -51,10 +51,11 @@ record TypeFlags where constructor MkTypeFlags uniqueAuto : Bool -- should 'auto' implicits check for uniqueness external : Bool -- defined externally (e.g. in a C or Scheme library) + forwardDecl : Bool -- is a forward declaration is not yet defined export defaultFlags : TypeFlags -defaultFlags = MkTypeFlags False False +defaultFlags = MkTypeFlags False False False public export record HoleFlags where diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index 41e9a22aec..205e2e975c 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -969,10 +969,12 @@ TTC TypeFlags where toBuf b l = do toBuf b (uniqueAuto l) toBuf b (external l) + toBuf b (forwardDecl l) fromBuf b = do u <- fromBuf b e <- fromBuf b - pure (MkTypeFlags u e) + f <- fromBuf b + pure (MkTypeFlags u e f) export TTC Def where diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr index f2c0942b13..5b391347d4 100644 --- a/src/TTImp/ProcessData.idr +++ b/src/TTImp/ProcessData.idr @@ -425,8 +425,9 @@ 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 + let flags = { forwardDecl := True } defaultFlags tidx <- addDef n (newDef fc n linear vars fullty def_vis - (TCon 0 arity [] [] defaultFlags [] [] Nothing)) + (TCon 0 arity [] [] flags [] [] Nothing)) addMutData (Resolved tidx) defs <- get Ctxt traverse_ (\n => setMutWith fc n (mutData defs)) (mutData defs) @@ -499,10 +500,11 @@ 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 [] _ => case mfullty of Nothing => pure (mw, vis, tot, type ndef) Just fullty => do ok <- convert defs [] fullty (type ndef) + when (not flags.forwardDecl) $ throw (AlreadyDefined fc n) if ok then pure (mw, vis, tot, fullty) else do logTermNF "declare.data" 1 "Previous" [] (type ndef) logTermNF "declare.data" 1 "Now" [] fullty From 7c74f4b9174b672608b71aeb5d3b3a3994d69ec5 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Wed, 29 Jan 2025 20:15:45 -0800 Subject: [PATCH 2/6] [ fix ] don't allow impossible clauses on forward declarations --- src/Core/Coverage.idr | 2 +- tests/idris2/data/data003/Test.idr | 8 ++++++++ tests/idris2/data/data003/Test2.idr | 4 ++++ tests/idris2/data/data003/expected | 18 ++++++++++++++++++ tests/idris2/data/data003/run | 4 ++++ 5 files changed, 35 insertions(+), 1 deletion(-) create mode 100644 tests/idris2/data/data003/Test.idr create mode 100644 tests/idris2/data/data003/Test2.idr create mode 100644 tests/idris2/data/data003/expected create mode 100755 tests/idris2/data/data003/run diff --git a/src/Core/Coverage.idr b/src/Core/Coverage.idr index ee07351cc9..c00008eb7b 100644 --- a/src/Core/Coverage.idr +++ b/src/Core/Coverage.idr @@ -139,7 +139,7 @@ isEmpty defs env (NTCon fc n t a args) | _ => pure False case nty of TCon _ _ _ _ flags _ cons _ - => if not (external flags) + => if not (external flags) && not (forwardDecl flags) then allM (conflict defs env (NTCon fc n t a args)) cons else pure False _ => pure False diff --git a/tests/idris2/data/data003/Test.idr b/tests/idris2/data/data003/Test.idr new file mode 100644 index 0000000000..671481ce0b --- /dev/null +++ b/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 diff --git a/tests/idris2/data/data003/Test2.idr b/tests/idris2/data/data003/Test2.idr new file mode 100644 index 0000000000..dc86b769f7 --- /dev/null +++ b/tests/idris2/data/data003/Test2.idr @@ -0,0 +1,4 @@ +data Bar : Type where + +data Bar : Type where + MkBar : Bar diff --git a/tests/idris2/data/data003/expected b/tests/idris2/data/data003/expected new file mode 100644 index 0000000000..6a57151ee5 --- /dev/null +++ b/tests/idris2/data/data003/expected @@ -0,0 +1,18 @@ +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 + diff --git a/tests/idris2/data/data003/run b/tests/idris2/data/data003/run new file mode 100755 index 0000000000..acbba2c35c --- /dev/null +++ b/tests/idris2/data/data003/run @@ -0,0 +1,4 @@ +. ../../../testutils.sh + +check Test.idr +check Test2.idr From 252b654b52aa3f3112664e7d58ef29fecaa1b8e1 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Wed, 29 Jan 2025 22:02:45 -0800 Subject: [PATCH 3/6] add test for issue 3457 --- tests/idris2/data/data003/Issue3457.idr | 11 +++++++++++ tests/idris2/data/data003/expected | 14 ++++++++++++++ tests/idris2/data/data003/run | 1 + 3 files changed, 26 insertions(+) create mode 100644 tests/idris2/data/data003/Issue3457.idr diff --git a/tests/idris2/data/data003/Issue3457.idr b/tests/idris2/data/data003/Issue3457.idr new file mode 100644 index 0000000000..0a947f21c0 --- /dev/null +++ b/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 diff --git a/tests/idris2/data/data003/expected b/tests/idris2/data/data003/expected index 6a57151ee5..5c4dc8730d 100644 --- a/tests/idris2/data/data003/expected +++ b/tests/idris2/data/data003/expected @@ -16,3 +16,17 @@ 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 _) + diff --git a/tests/idris2/data/data003/run b/tests/idris2/data/data003/run index acbba2c35c..d35ff64b74 100755 --- a/tests/idris2/data/data003/run +++ b/tests/idris2/data/data003/run @@ -2,3 +2,4 @@ check Test.idr check Test2.idr +check Issue3457.idr From 42f61e8c2d8d57629d566fd0c61a0dff8c339cdd Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Thu, 30 Jan 2025 14:53:35 -0800 Subject: [PATCH 4/6] Use `Maybe (List Name)` instead of a `forwardDecl` flag --- src/Core/Binary.idr | 2 +- src/Core/Case/Util.idr | 2 +- src/Core/Context.idr | 12 ++++++++---- src/Core/Context/Context.idr | 5 ++--- src/Core/Context/Data.idr | 2 +- src/Core/Context/Pretty.idr | 4 ++-- src/Core/Coverage.idr | 5 +++-- src/Core/TTC.idr | 4 +--- src/Core/Termination/Positivity.idr | 1 + src/Idris/Doc/String.idr | 2 +- src/TTImp/Elab/App.idr | 2 +- src/TTImp/Elab/Record.idr | 2 +- src/TTImp/Elab/RunElab.idr | 2 +- src/TTImp/Interactive/CaseSplit.idr | 2 +- src/TTImp/Interactive/ExprSearch.idr | 2 +- src/TTImp/Interactive/Intro.idr | 2 +- src/TTImp/ProcessBuiltin.idr | 4 ++-- src/TTImp/ProcessData.idr | 8 +++----- src/TTImp/ProcessRecord.idr | 10 ++++++---- 19 files changed, 38 insertions(+), 35 deletions(-) diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 21e85678b4..b4170d9323 100644 --- a/src/Core/Binary.idr +++ b/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 = 2025_01_29_00 +ttcVersion = 2025_01_30_00 export checkTTCVersion : String -> Int -> Int -> Core () diff --git a/src/Core/Case/Util.idr b/src/Core/Case/Util.idr index da36b57696..d66ce4991a 100644 --- a/src/Core/Case/Util.idr +++ b/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 diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 7f04b35a56..56acf532b2 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -585,9 +585,11 @@ 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 Nothing det) + = pure $ TCon t a ps ds u !(traverse (full gam) ms) Nothing det + full gam (TCon t a ps ds u ms (Just cs) det) = pure $ TCon t a ps ds u !(traverse (full gam) ms) - !(traverse (full gam) cs) det + (Just !(traverse (full gam) cs)) det full gam (BySearch c d def) = pure $ BySearch c d !(full gam def) full gam (Guess tm b cs) @@ -603,9 +605,11 @@ 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 Nothing det) + = pure $ TCon t a ps ds u !(traverse (resolved gam) ms) Nothing det + resolved gam (TCon t a ps ds u ms (Just cs) det) = pure $ TCon t a ps ds u !(traverse (resolved gam) ms) - !(traverse (resolved gam) cs) det + (Just !(traverse (resolved gam) cs)) det resolved gam (BySearch c d def) = pure $ BySearch c d !(resolved gam def) resolved gam (Guess tm b cs) diff --git a/src/Core/Context/Context.idr b/src/Core/Context/Context.idr index c096c14b46..c2fd27e2e8 100644 --- a/src/Core/Context/Context.idr +++ b/src/Core/Context/Context.idr @@ -51,11 +51,10 @@ record TypeFlags where constructor MkTypeFlags uniqueAuto : Bool -- should 'auto' implicits check for uniqueness external : Bool -- defined externally (e.g. in a C or Scheme library) - forwardDecl : Bool -- is a forward declaration is not yet defined export defaultFlags : TypeFlags -defaultFlags = MkTypeFlags False False False +defaultFlags = MkTypeFlags False False public export record HoleFlags where @@ -102,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 diff --git a/src/Core/Context/Data.idr b/src/Core/Context/Data.idr index 97a5dcd2ea..5435fcd363 100644 --- a/src/Core/Context/Data.idr +++ b/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) diff --git a/src/Core/Context/Pretty.idr b/src/Core/Context/Pretty.idr index 068a5b5d74..a7c3f8ff09 100644 --- a/src/Core/Context/Pretty.idr +++ b/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 $ diff --git a/src/Core/Coverage.idr b/src/Core/Coverage.idr index c00008eb7b..55162a8750 100644 --- a/src/Core/Coverage.idr +++ b/src/Core/Coverage.idr @@ -138,8 +138,9 @@ isEmpty defs env (NTCon fc n t a args) = do Just nty <- lookupDefExact n (gamma defs) | _ => pure False case nty of - TCon _ _ _ _ flags _ cons _ - => if not (external flags) && not (forwardDecl flags) + 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 _ => pure False diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index 205e2e975c..41e9a22aec 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -969,12 +969,10 @@ TTC TypeFlags where toBuf b l = do toBuf b (uniqueAuto l) toBuf b (external l) - toBuf b (forwardDecl l) fromBuf b = do u <- fromBuf b e <- fromBuf b - f <- fromBuf b - pure (MkTypeFlags u e f) + pure (MkTypeFlags u e) export TTC Def where diff --git a/src/Core/Termination/Positivity.idr b/src/Core/Termination/Positivity.idr index 403a7272cd..07e51944d1 100644 --- a/src/Core/Termination/Positivity.idr +++ b/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 $ diff --git a/src/Idris/Doc/String.idr b/src/Idris/Doc/String.idr index 4b99d76297..da214d9c72 100644 --- a/src/Idris/Doc/String.idr +++ b/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] => diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index ede3102048..9743018cf3 100644 --- a/src/TTImp/Elab/App.idr +++ b/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 diff --git a/src/TTImp/Elab/Record.idr b/src/TTImp/Elab/Record.idr index 7cae467d75..a4280c3f3c 100644 --- a/src/TTImp/Elab/Record.idr +++ b/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} -> diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr index 457a9b962d..a858c7e3bb 100644 --- a/src/TTImp/Elab/RunElab.idr +++ b/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) diff --git a/src/TTImp/Interactive/CaseSplit.idr b/src/TTImp/Interactive/CaseSplit.idr index e741314556..eef1059d33 100644 --- a/src/TTImp/Interactive/CaseSplit.idr +++ b/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) diff --git a/src/TTImp/Interactive/ExprSearch.idr b/src/TTImp/Interactive/ExprSearch.idr index 36fad55967..96a0a7e1e2 100644 --- a/src/TTImp/Interactive/ExprSearch.idr +++ b/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 diff --git a/src/TTImp/Interactive/Intro.idr b/src/TTImp/Interactive/Intro.idr index 57973f0dcf..ed4c1c3c1e 100644 --- a/src/TTImp/Interactive/Intro.idr +++ b/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) diff --git a/src/TTImp/ProcessBuiltin.idr b/src/TTImp/ProcessBuiltin.idr index e10f30f632..bb274fea1a 100644 --- a/src/TTImp/ProcessBuiltin.idr +++ b/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. diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr index 5b391347d4..f11f473487 100644 --- a/src/TTImp/ProcessData.idr +++ b/src/TTImp/ProcessData.idr @@ -425,9 +425,8 @@ 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 - let flags = { forwardDecl := True } defaultFlags tidx <- addDef n (newDef fc n linear vars fullty def_vis - (TCon 0 arity [] [] flags [] [] Nothing)) + (TCon 0 arity [] [] defaultFlags [] Nothing Nothing)) addMutData (Resolved tidx) defs <- get Ctxt traverse_ (\n => setMutWith fc n (mutData defs)) (mutData defs) @@ -500,11 +499,10 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw o _ => pure $ mbtot <|> declTot case definition ndef of - TCon _ _ _ _ flags 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) - when (not flags.forwardDecl) $ throw (AlreadyDefined fc n) if ok then pure (mw, vis, tot, fullty) else do logTermNF "declare.data" 1 "Previous" [] (type ndef) logTermNF "declare.data" 1 "Now" [] fullty @@ -518,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 diff --git a/src/TTImp/ProcessRecord.idr b/src/TTImp/ProcessRecord.idr index 9d882a1549..668eab635e 100644 --- a/src/TTImp/ProcessRecord.idr +++ b/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 [] + defs <- get Ctxt + -- Create a forward declaration if none exists + 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) + when (isNothing !(lookupTyExact tn (gamma defs))) $ + 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!") From 0ca8bbe355d19a2ec8d3934d941cb1b4f0d876f4 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Fri, 31 Jan 2025 06:59:03 -0800 Subject: [PATCH 5/6] add test of positivity checking --- tests/idris2/data/data003/Positivity.idr | 9 +++++++++ tests/idris2/data/data003/expected | 1 + tests/idris2/data/data003/run | 1 + 3 files changed, 11 insertions(+) create mode 100644 tests/idris2/data/data003/Positivity.idr diff --git a/tests/idris2/data/data003/Positivity.idr b/tests/idris2/data/data003/Positivity.idr new file mode 100644 index 0000000000..15cdcfc95e --- /dev/null +++ b/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 + diff --git a/tests/idris2/data/data003/expected b/tests/idris2/data/data003/expected index 5c4dc8730d..fe751f7e2f 100644 --- a/tests/idris2/data/data003/expected +++ b/tests/idris2/data/data003/expected @@ -30,3 +30,4 @@ Issue3457:6:1--6:20 Missing cases: fun (MkFoo C _) +1/1: Building Positivity (Positivity.idr) diff --git a/tests/idris2/data/data003/run b/tests/idris2/data/data003/run index d35ff64b74..e513c32a12 100755 --- a/tests/idris2/data/data003/run +++ b/tests/idris2/data/data003/run @@ -3,3 +3,4 @@ check Test.idr check Test2.idr check Issue3457.idr +check Positivity.idr From f9f1770193f969e7e3ba2450cbc8c36ed2d590ca Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Wed, 5 Feb 2025 19:59:13 -0800 Subject: [PATCH 6/6] tighten up code and add test --- src/Core/Context.idr | 12 ++++-------- src/TTImp/ProcessRecord.idr | 6 +++--- tests/idris2/data/data003/OopsDef.idr | 10 ++++++++++ tests/idris2/data/data003/OopsRef.idr | 9 +++++++++ tests/idris2/data/data003/expected | 2 ++ tests/idris2/data/data003/run | 1 + 6 files changed, 29 insertions(+), 11 deletions(-) create mode 100644 tests/idris2/data/data003/OopsDef.idr create mode 100644 tests/idris2/data/data003/OopsRef.idr diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 56acf532b2..64cdcf27a5 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -585,11 +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 Nothing det) - = pure $ TCon t a ps ds u !(traverse (full gam) ms) Nothing det - full gam (TCon t a ps ds u ms (Just cs) det) + full gam (TCon t a ps ds u ms mcs det) = pure $ TCon t a ps ds u !(traverse (full gam) ms) - (Just !(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) @@ -605,11 +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 Nothing det) - = pure $ TCon t a ps ds u !(traverse (resolved gam) ms) Nothing det - resolved gam (TCon t a ps ds u ms (Just cs) det) + resolved gam (TCon t a ps ds u ms mcs det) = pure $ TCon t a ps ds u !(traverse (resolved gam) ms) - (Just !(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) diff --git a/src/TTImp/ProcessRecord.idr b/src/TTImp/ProcessRecord.idr index 668eab635e..e34a06ce32 100644 --- a/src/TTImp/ProcessRecord.idr +++ b/src/TTImp/ProcessRecord.idr @@ -147,9 +147,9 @@ elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conNa let dataTy = IBindHere fc (PI erased) !(bindTypeNames fc [] vars (mkDataTy fc params0)) defs <- get Ctxt -- Create a forward declaration if none exists - let dt = MkImpLater fc tn dataTy - log "declare.record" 10 $ "Pre-declare record data type: \{show dt}" - when (isNothing !(lookupTyExact tn (gamma defs))) $ + 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) diff --git a/tests/idris2/data/data003/OopsDef.idr b/tests/idris2/data/data003/OopsDef.idr new file mode 100644 index 0000000000..74b229d7d8 --- /dev/null +++ b/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 + diff --git a/tests/idris2/data/data003/OopsRef.idr b/tests/idris2/data/data003/OopsRef.idr new file mode 100644 index 0000000000..cc59e7423f --- /dev/null +++ b/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 + diff --git a/tests/idris2/data/data003/expected b/tests/idris2/data/data003/expected index fe751f7e2f..a170fc0709 100644 --- a/tests/idris2/data/data003/expected +++ b/tests/idris2/data/data003/expected @@ -31,3 +31,5 @@ Missing cases: fun (MkFoo C _) 1/1: Building Positivity (Positivity.idr) +1/2: Building OopsDef (OopsDef.idr) +2/2: Building OopsRef (OopsRef.idr) diff --git a/tests/idris2/data/data003/run b/tests/idris2/data/data003/run index e513c32a12..de1d73007a 100755 --- a/tests/idris2/data/data003/run +++ b/tests/idris2/data/data003/run @@ -4,3 +4,4 @@ check Test.idr check Test2.idr check Issue3457.idr check Positivity.idr +check OopsRef.idr