From 04a0f5001f87b531408640ed7edf9bff04e96abd Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Tue, 9 Mar 2021 17:23:05 +0000 Subject: [PATCH] Correct multiplicities when checking Pi binders We've always just used 0, which isn't correct if the function is going to be used in a runtime pattern match. Now calculate correctly so that we're explicit about which type level variables are used at runtime. This might cause some programs to fail to compile, if they use functions that calculate Pi types. The solution is to make those functions explicitly 0 multiplicity. If that doesn't work, you may have been accidentally trying to use compile-time only data at run time! Fixes #1163 --- libs/contrib/Data/Telescope/Fun.idr | 6 +++--- libs/contrib/Data/Telescope/SimpleFun.idr | 4 ++-- src/Core/LinearCheck.idr | 7 +++++-- src/TTImp/Parser.idr | 4 +++- tests/Main.idr | 2 +- tests/idris2/basic013/Implicits.idr | 2 +- tests/idris2/interface003/Do.idr | 2 +- tests/idris2/interface004/Do.idr | 2 +- tests/idris2/interface024/EH.idr | 4 ++-- tests/idris2/reg033/DerivingEq.idr | 2 +- tests/idris2/reg038/Test1.idr | 9 +++++++++ tests/idris2/reg038/Test2.idr | 9 +++++++++ tests/idris2/reg038/expected | 21 +++++++++++++++++++++ tests/idris2/reg038/run | 4 ++++ tests/ttimp/perf003/Id.yaff | 2 +- 15 files changed, 64 insertions(+), 16 deletions(-) create mode 100644 tests/idris2/reg038/Test1.idr create mode 100644 tests/idris2/reg038/Test2.idr create mode 100644 tests/idris2/reg038/expected create mode 100755 tests/idris2/reg038/run diff --git a/libs/contrib/Data/Telescope/Fun.idr b/libs/contrib/Data/Telescope/Fun.idr index 2bd42a021..c6f581c18 100644 --- a/libs/contrib/Data/Telescope/Fun.idr +++ b/libs/contrib/Data/Telescope/Fun.idr @@ -9,9 +9,9 @@ import Data.Telescope.Segment import Data.Telescope.SimpleFun public export -Fun : (env : Left.Environment gamma) -> {n : Nat} -> (0 delta : Segment n gamma) - -> (cod : SimpleFun env delta Type) - -> Type +0 Fun : (env : Left.Environment gamma) -> {n : Nat} -> (0 delta : Segment n gamma) + -> (cod : SimpleFun env delta Type) + -> Type Fun env {n = 0 } [] cod = cod Fun env {n = S n} (ty :: delta) cod = (x : ty env) -> Fun (env ** x) delta (cod x) diff --git a/libs/contrib/Data/Telescope/SimpleFun.idr b/libs/contrib/Data/Telescope/SimpleFun.idr index b0f539823..c6fb21fdd 100644 --- a/libs/contrib/Data/Telescope/SimpleFun.idr +++ b/libs/contrib/Data/Telescope/SimpleFun.idr @@ -10,8 +10,8 @@ import Data.Telescope.Segment ||| An n-ary function whose codomain does not depend on its ||| arguments. The arguments may have dependencies. public export -SimpleFun : (env : Left.Environment gamma) -> {n : Nat} -> (0 delta : Segment n gamma) - -> (cod : Type) -> Type +0 SimpleFun : (env : Left.Environment gamma) -> {n : Nat} -> (0 delta : Segment n gamma) + -> (cod : Type) -> Type SimpleFun env {n = 0 } [] cod = cod SimpleFun env {n = S n} (ty :: delta) cod = (x : ty env) -> SimpleFun (env ** x) delta cod diff --git a/src/Core/LinearCheck.idr b/src/Core/LinearCheck.idr index 44c75fca2..b0783a142 100644 --- a/src/Core/LinearCheck.idr +++ b/src/Core/LinearCheck.idr @@ -287,7 +287,10 @@ mutual where rig : RigCount rig = case b of - Pi _ _ _ _ => erased + Pi _ _ _ _ => + if isErased rig_in + then erased + else top -- checking as if an inspectable run-time type _ => if isErased rig_in then erased else linear @@ -391,7 +394,7 @@ mutual (valv, valt, vs) <- lcheck (rig |*| rigc) erase env val pure (Let fc rigc valv tyv, tyt, vs) lcheckBinder rig erase env (Pi fc c x ty) - = do (tyv, tyt, _) <- lcheck erased erase env ty + = do (tyv, tyt, _) <- lcheck (rig |*| c) erase env ty pure (Pi fc c x tyv, tyt, []) lcheckBinder rig erase env (PVar fc c p ty) = do (tyv, tyt, _) <- lcheck erased erase env ty diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index eadddbf2c..b1431df6d 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -704,9 +704,11 @@ topDecl fname indents visOpts <- many visOpt vis <- getVisibility Nothing visOpts let opts = mapMaybe getRight visOpts + m <- multiplicity + rig <- getMult m claim <- tyDecl fname indents end <- location - pure (IClaim (MkFC fname start end) top vis opts claim) + pure (IClaim (MkFC fname start end) rig vis opts claim) <|> recordDecl fname indents <|> directive fname indents <|> definition fname indents diff --git a/tests/Main.idr b/tests/Main.idr index 951b08ea5..8a6943c29 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -122,7 +122,7 @@ idrisTestsRegression = MkTestPool [] "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021", "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028", "reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035", - "reg036", "reg037"] + "reg036", "reg037", "reg038"] idrisTests : TestPool idrisTests = MkTestPool [] diff --git a/tests/idris2/basic013/Implicits.idr b/tests/idris2/basic013/Implicits.idr index da3b50864..9d6b36c74 100644 --- a/tests/idris2/basic013/Implicits.idr +++ b/tests/idris2/basic013/Implicits.idr @@ -1,6 +1,6 @@ public export interface Do (0 m : Type) where - Next : m -> Type + 0 Next : m -> Type bind : (x : m) -> Next x -- Test that the implicits don't turn into as patterns on the LHS - they diff --git a/tests/idris2/interface003/Do.idr b/tests/idris2/interface003/Do.idr index 3a5e08daf..41c9df478 100644 --- a/tests/idris2/interface003/Do.idr +++ b/tests/idris2/interface003/Do.idr @@ -1,6 +1,6 @@ public export interface Do (0 m : Type) where - Next : (a : Type) -> (b : Type) -> m -> Type + 0 Next : (a : Type) -> (b : Type) -> m -> Type bind : (x : m) -> Next a b x -- This won't actually achieve anything useful, but we're testing whether diff --git a/tests/idris2/interface004/Do.idr b/tests/idris2/interface004/Do.idr index 88c2770fc..108f6d350 100644 --- a/tests/idris2/interface004/Do.idr +++ b/tests/idris2/interface004/Do.idr @@ -1,6 +1,6 @@ public export interface Do (0 m : Type) where - Next : m -> Type + 0 Next : m -> Type bind : (x : m) -> Next x public export diff --git a/tests/idris2/interface024/EH.idr b/tests/idris2/interface024/EH.idr index 348ad9948..a03b2f94c 100644 --- a/tests/idris2/interface024/EH.idr +++ b/tests/idris2/interface024/EH.idr @@ -51,11 +51,11 @@ MultiplicativeStruct m = MkMultiplicative (Mult $ Struct m) (Unit $ Struct m) ----------------------------------------------------- -Commutative : MonoidOver a -> Type +0 Commutative : MonoidOver a -> Type Commutative m = (x,y : a) -> let _ = AdditiveStruct m in x .+. y = y .+. x -Commute : (Additive a, Additive2 a) => Type +0 Commute : (Additive a, Additive2 a) => Type Commute = (x11,x12,x21,x22 : a) -> ((x11 :+: x12) .+. (x21 :+: x22)) diff --git a/tests/idris2/reg033/DerivingEq.idr b/tests/idris2/reg033/DerivingEq.idr index 0340a87b7..4925cb937 100644 --- a/tests/idris2/reg033/DerivingEq.idr +++ b/tests/idris2/reg033/DerivingEq.idr @@ -12,7 +12,7 @@ countArgs _ = 0 -- %logging 5 public export -genEq : Name -> Elab (t -> t -> Bool) +genEq : {t : _} -> Name -> Elab (t -> t -> Bool) genEq typeName = do let pos : FC = MkFC "generated code" (0,0) (0,0) [(n, _)] <- getType typeName diff --git a/tests/idris2/reg038/Test1.idr b/tests/idris2/reg038/Test1.idr new file mode 100644 index 000000000..3f7face8e --- /dev/null +++ b/tests/idris2/reg038/Test1.idr @@ -0,0 +1,9 @@ +data Foo : Nat -> Type where + +G : (0 yv : Nat) -> Type +G yv = Foo yv -> Bool + +partial +f : (0 x : Nat) -> Nat +f x = case G x of + (Foo x' -> _) => x' diff --git a/tests/idris2/reg038/Test2.idr b/tests/idris2/reg038/Test2.idr new file mode 100644 index 000000000..bbe2df5f5 --- /dev/null +++ b/tests/idris2/reg038/Test2.idr @@ -0,0 +1,9 @@ +data Foo : Nat -> Type where + +0 G : (0 yv : Nat) -> Type +G yv = Foo yv -> Bool + +partial +f : (0 x : Nat) -> Nat +f x = case G x of + (Foo x' -> _) => x' diff --git a/tests/idris2/reg038/expected b/tests/idris2/reg038/expected new file mode 100644 index 000000000..76041ca87 --- /dev/null +++ b/tests/idris2/reg038/expected @@ -0,0 +1,21 @@ +1/1: Building Test1 (Test1.idr) +Error: While processing right hand side of G. yv is not accessible in this context. + +Test1.idr:4:12--4:14 + 1 | data Foo : Nat -> Type where + 2 | + 3 | G : (0 yv : Nat) -> Type + 4 | G yv = Foo yv -> Bool + ^^ + +1/1: Building Test2 (Test2.idr) +Error: While processing right hand side of f. Main.G is not accessible in this context. + +Test2.idr:8:12--8:13 + 4 | G yv = Foo yv -> Bool + 5 | + 6 | partial + 7 | f : (0 x : Nat) -> Nat + 8 | f x = case G x of + ^ + diff --git a/tests/idris2/reg038/run b/tests/idris2/reg038/run new file mode 100755 index 000000000..2299026b8 --- /dev/null +++ b/tests/idris2/reg038/run @@ -0,0 +1,4 @@ +$1 --no-color --console-width 0 Test1.idr --check +$1 --no-color --console-width 0 Test2.idr --check + +rm -rf build diff --git a/tests/ttimp/perf003/Id.yaff b/tests/ttimp/perf003/Id.yaff index fe9d3599d..5f81ccdd6 100644 --- a/tests/ttimp/perf003/Id.yaff +++ b/tests/ttimp/perf003/Id.yaff @@ -1,4 +1,4 @@ -IdType : Type +0 IdType : Type IdType = {0 a : Type} -> a -> a id : IdType