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

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

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
 

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

@@ -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 []

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