Merge pull request #1171 from edwinb/fix1163

Correct multiplicities when checking Pi binders

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)
+0 Fun : (env : Left.Environment gamma) -> {n : Nat} -> (0 delta : Segment n gamma)
-   -> (cod : SimpleFun env delta Type)
+     -> (cod : SimpleFun env delta Type)
-   -> 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)
 

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)
+0 SimpleFun : (env : Left.Environment gamma) -> {n : Nat} -> (0 delta : Segment n gamma)
-         -> (cod : Type) -> Type
+           -> (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
 

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

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

tests/Main.idr

@@ -123,7 +123,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 []

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

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

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

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))

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

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'

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'

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
+                ^
+

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

tests/ttimp/perf003/Id.yaff

@@ -1,4 +1,4 @@
-IdType : Type
+0 IdType : Type
 IdType = {0 a : Type} -> a -> a
 
 id : IdType