diff --git a/libs/contrib/Data/Telescope/Fun.idr b/libs/contrib/Data/Telescope/Fun.idr
index 2bd42a021c..c6f581c187 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 b0f539823a..c6fb21fdda 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 44c75fca22..b0783a1426 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 eadddbf2cd..b1431df6d5 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 951b08ea50..8a6943c29f 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 da3b50864c..9d6b36c740 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 3a5e08daf2..41c9df4784 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 88c2770fc6..108f6d350c 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 348ad99487..a03b2f94cc 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 0340a87b7f..4925cb9375 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 0000000000..3f7face8ec
--- /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 0000000000..bbe2df5f59
--- /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 0000000000..76041ca872
--- /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 0000000000..2299026b8c
--- /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 fe9d3599d1..5f81ccdd6a 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