implement IClaimData reflection

idris-lang · Nov 22, 2024 · 121e494 · 121e494
1 parent 604a04a
commit 121e494
Show file tree

Hide file tree

Showing 12 changed files with 77 additions and 32 deletions.
diff --git a/libs/base/Deriving/Foldable.idr b/libs/base/Deriving/Foldable.idr
@@ -381,7 +381,7 @@ namespace Foldable
 
     -- Define the instance
     check $ ILocal fc
-      [ IClaim fc MW vis [Totality treq] ty
+      [ IClaim (MkFCVal fc (MkIClaimData MW vis [Totality treq] ty))
       , IDef fc foldMapName cls
       ] `(fromFoldMap ~(t) ~(IVar fc foldMapName))
 

diff --git a/libs/base/Deriving/Functor.idr b/libs/base/Deriving/Functor.idr
@@ -392,7 +392,7 @@ namespace Functor
 
     -- Define the instance
     check $ ILocal fc
-      [ IClaim fc MW vis [Totality treq] ty
+      [ IClaim (MkFCVal fc (MkIClaimData MW vis [Totality treq] ty))
       , IDef fc mapName cls
       ] `(MkFunctor {f = ~(t)} ~(IVar fc mapName))
 

diff --git a/libs/base/Deriving/Show.idr b/libs/base/Deriving/Show.idr
@@ -272,7 +272,7 @@ namespace Show
 
     -- Define the instance
     check $ ILocal fc
-      [ IClaim fc MW vis [Totality treq] ty
+      [ IClaim (MkFCVal fc (MkIClaimData MW vis [Totality treq] ty))
       , IDef fc showName cls
       ] `(fromShowPrec ~(IVar fc showName))
 

diff --git a/libs/base/Deriving/Traversable.idr b/libs/base/Deriving/Traversable.idr
@@ -406,7 +406,7 @@ namespace Traversable
 
     -- Define the instance
     check $ ILocal fc
-      [ IClaim fc MW vis [Totality treq] ty
+      [ IClaim (MkFCVal fc (MkIClaimData MW vis [Totality treq] ty))
       , IDef fc traverseName cls
       ] `(MkTraversable {t = ~(t)} ~(IVar fc traverseName))
 

diff --git a/libs/base/Language/Reflection/TT.idr b/libs/base/Language/Reflection/TT.idr
@@ -81,6 +81,18 @@ record WithFC (ty : Type) where
 NoFC : a -> WithFC a
 NoFC = MkFCVal EmptyFC
 
+export
+Functor WithFC where
+  map f = { val $= f}
+
+export
+Foldable WithFC where
+  foldr f i v = f v.val i
+
+export
+Traversable WithFC where
+  traverse f (MkFCVal fc val) = map (MkFCVal fc) (f val)
+
 public export
 data NameType : Type where
      Bound   : NameType

diff --git a/libs/base/Language/Reflection/TTImp.idr b/libs/base/Language/Reflection/TTImp.idr
@@ -202,10 +202,17 @@ mutual
   onWithDefault defHandler _ DefaultedValue     = defHandler
   onWithDefault _ valHandler (SpecifiedValue v) = valHandler v
 
+  public export
+  record IClaimData where
+    constructor MkIClaimData
+    rig : Count
+    vis : Visibility
+    opts : List FnOpt
+    type : ITy
+
   public export
   data Decl : Type where
-       IClaim : FC -> Count -> Visibility -> List FnOpt ->
-                ITy -> Decl
+       IClaim : WithFC IClaimData -> Decl
        IData : FC -> WithDefault Visibility Private -> Maybe TotalReq -> Data -> Decl
        IDef : FC -> Name -> (cls : List Clause) -> Decl
        IParameters : FC -> (params : List (Name, Count, PiInfo TTImp, TTImp)) ->
@@ -429,9 +436,13 @@ parameters {auto eqTTImp : Eq TTImp}
       n == n' && ps == ps' && opts == opts' && cn == cn' && fs == fs'
 
   public export
-  Eq Decl where
-    IClaim _ c v fos t == IClaim _ c' v' fos' t' =
+  Eq IClaimData where
+    MkIClaimData c v fos t == MkIClaimData c' v' fos' t' =
       c == c' && v == v' && fos == fos' && t == t'
+
+  public export
+  Eq Decl where
+    IClaim c == IClaim c' = c.val == c'.val
     IData _ v t d == IData _ v' t' d' =
       v == v' && t == t' && d == d'
     IDef _ n cs == IDef _ n' cs' =
@@ -543,11 +554,14 @@ mutual
   Show ITy where
     show (MkTy fc n ty) = "\{show n.val} : \{show ty}"
 
-  public export
-  Show Decl where
-    show (IClaim fc rig vis xs sig)
+  Show IClaimData where
+    show (MkIClaimData rig vis xs sig)
       = unwords [ show vis
                 , showCount rig (show sig) ]
+
+  public export
+  Show Decl where
+    show (IClaim claim) = show claim.val
     show (IData fc vis treq dt)
       = unwords [ show vis
                 , showTotalReq treq (show dt)
@@ -807,10 +821,13 @@ parameters (f : TTImp -> TTImp)
   mapRecord (MkRecord fc n params opts conName fields)
     = MkRecord fc n (map (map $ map $ bimap mapPiInfo mapTTImp) params) opts conName (map mapIField fields)
 
+  mapIClaimData : IClaimData -> IClaimData
+  mapIClaimData (MkIClaimData rig vis opts ty)
+    = MkIClaimData rig vis (map mapFnOpt opts) (mapITy ty)
+
   public export
   mapDecl : Decl -> Decl
-  mapDecl (IClaim fc rig vis opts ty)
-    = IClaim fc rig vis (map mapFnOpt opts) (mapITy ty)
+  mapDecl (IClaim claim) = IClaim $ map mapIClaimData claim
   mapDecl (IData fc vis mtreq dat) = IData fc vis mtreq (mapData dat)
   mapDecl (IDef fc n cls) = IDef fc n (map mapClause cls)
   mapDecl (IParameters fc params xs) = IParameters fc params (assert_total $ map mapDecl xs)
@@ -933,10 +950,13 @@ parameters {0 m : Type -> Type} {auto apl : Applicative m} (f : (original : TTIm
     <*> pure conName
     <*> traverse mapMIField fields
 
+  mapMIClaimData : IClaimData -> m IClaimData
+  mapMIClaimData (MkIClaimData rig vis opts ty)
+    = MkIClaimData rig vis <$> traverse mapMFnOpt opts <*> mapMITy ty
+
   public export
   mapMDecl : Decl -> m Decl
-  mapMDecl (IClaim fc rig vis opts ty)
-    = IClaim fc rig vis <$> traverse mapMFnOpt opts <*> mapMITy ty
+  mapMDecl (IClaim claim) = IClaim <$> traverse mapMIClaimData claim
   mapMDecl (IData fc vis mtreq dat) = IData fc vis mtreq <$> mapMData dat
   mapMDecl (IDef fc n cls) = IDef fc n <$> traverse mapMClause cls
   mapMDecl (IParameters fc params xs) = IParameters fc params <$> assert_total (traverse mapMDecl xs)

diff --git a/src/Core/Reflect.idr b/src/Core/Reflect.idr
@@ -874,9 +874,7 @@ Reify a => Reify (WithFC a) where
                  pure $ MkFCVal fc val
              (UN (Basic "MkFCVal"), [_, fc, l2]) => do
                  fc' <- reify defs !(evalClosure defs fc)
-                 --val1 <- (evalClosure defs l1)
                  val' <- reify defs !(evalClosure defs l2)
-                 -- cantReify val "MkFCVal wrong arguments: \{show fc} \{show val1} \{show val2}"
                  pure $ MkFCVal fc' val'
              (t, l) => cantReify val "WithFC constructor: \{show t}, args: \{show (length l)}"
   reify defs val = cantReify val "Expected WithFC, found something else"

diff --git a/src/TTImp/Reflect.idr b/src/TTImp/Reflect.idr
@@ -415,16 +415,25 @@ mutual
     reify defs val = cantReify val "Clause"
 
   export
-  Reify ImpDecl where
+  Reify (IClaimData Name) where
     reify defs val@(NDCon _ n _ _ args)
         = case (dropAllNS !(full (gamma defs) n), map snd args) of
-               (UN (Basic "IClaim"), [v,w,x,y,z])
-                    => do v' <- reify defs !(evalClosure defs v)
-                          w' <- reify defs !(evalClosure defs w)
+               (UN (Basic "MkIClaimData"), [w, x, y, z])
+                    => do w' <- reify defs !(evalClosure defs w)
                           x' <- reify defs !(evalClosure defs x)
                           y' <- reify defs !(evalClosure defs y)
                           z' <- reify defs !(evalClosure defs z)
-                          pure (IClaim (MkFCVal v' $ MkIClaimData w' x' y' z'))
+                          pure (MkIClaimData w' x' y' z')
+               _ => cantReify val "IClaimData"
+    reify defs val = cantReify val "IClaimData"
+
+  export
+  Reify ImpDecl where
+    reify defs val@(NDCon _ n _ _ args)
+        = case (dropAllNS !(full (gamma defs) n), map snd args) of
+               (UN (Basic "IClaim"), [v])
+                    => do v' <- reify defs !(evalClosure defs v)
+                          pure (IClaim v')
                (UN (Basic "IData"), [x,y,z,w])
                     => do x' <- reify defs !(evalClosure defs x)
                           y' <- reify defs !(evalClosure defs y)
@@ -763,14 +772,19 @@ mutual
              appCon fc defs (reflectionttimp "ImpossibleClause") [x', y']
 
   export
-  Reflect ImpDecl where
-    reflect fc defs lhs env (IClaim (MkFCVal v $ MkIClaimData w x y z))
-        = do v' <- reflect fc defs lhs env v
-             w' <- reflect fc defs lhs env w
+  Reflect (IClaimData Name) where
+    reflect fc defs lhs env (MkIClaimData w x y z)
+        = do w' <- reflect fc defs lhs env w
              x' <- reflect fc defs lhs env x
              y' <- reflect fc defs lhs env y
              z' <- reflect fc defs lhs env z
-             appCon fc defs (reflectionttimp "IClaim") [v', w', x', y', z']
+             appCon fc defs (reflectionttimp "MkIClaimData") [w', x', y', z']
+
+  export
+  Reflect ImpDecl where
+    reflect fc defs lhs env (IClaim v)
+        = do v' <- reflect fc defs lhs env v
+             appCon fc defs (reflectionttimp "IClaim") [v']
     reflect fc defs lhs env (IData x y z w)
         = do x' <- reflect fc defs lhs env x
              y' <- reflect fc defs lhs env y

diff --git a/tests/idris2/reflection/reflection001/expected b/tests/idris2/reflection/reflection001/expected
@@ -35,7 +35,7 @@ quote:37:1--37:21
 
 Main> IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 17) (3, 18)) (UN (Basic "+"))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 13) (6, 14)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 13) (6, 14)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 13) (6, 14)) (BI 3)))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 18) (6, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 18) (6, 19)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (6, 18) (6, 19)) (BI 4)))
 Main> IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 12) (3, 23)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (3, 17) (3, 18)) (UN (Basic "+"))) (IVar (MkFC (Virtual Interactive) (0, 6) (0, 10)) (UN (Basic "True")))) (IVar (MkFC (Virtual Interactive) (0, 14) (0, 19)) (UN (Basic "False")))
-Main> ILocal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (11, 29)) [IClaim (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 28)) MW Private [] (MkTy (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 28)) (MkFCVal (UN (Basic "xfn"))) (IPi (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 18) (10, 28)) MW ExplicitArg Nothing (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 18) (10, 21)) (PrT IntType)) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 25) (10, 28)) (PrT IntType)))), IDef (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 29)) (UN (Basic "xfn")) [PatClause (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 15)) (UN (Basic "xfn"))) (IBindVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 16) (11, 19)) "var")) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 26) (11, 27)) (UN (Basic "*"))) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 25)) (UN (Basic "var")))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (12, 12) (12, 22)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (12, 12) (12, 15)) (UN (Basic "xfn"))) (IApp (MkFC (Virtual Interactive) (0, 9) (0, 22)) (IApp (MkFC (Virtual Interactive) (0, 9) (0, 22)) (IVar (MkFC (Virtual Interactive) (0, 9) (0, 12)) (UN (Basic "the"))) (IPrimVal (MkFC (Virtual Interactive) (0, 13) (0, 16)) (PrT IntType))) (IApp (MkFC (Virtual Interactive) (0, 17) (0, 22)) (IVar (MkFC (Virtual Interactive) (0, 17) (0, 22)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (Virtual Interactive) (0, 17) (0, 22)) (BI 99994)))))
-Main> ILocal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (17, 29)) [IClaim (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 28)) MW Private [] (MkTy (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 28)) (MkFCVal (UN (Basic "xfn"))) (IPi (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 18) (16, 28)) MW ExplicitArg Nothing (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 18) (16, 21)) (PrT IntType)) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 25) (16, 28)) (PrT IntType)))), IDef (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 29)) (UN (Basic "xfn")) [PatClause (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 15)) (UN (Basic "xfn"))) (IBindVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 16) (17, 19)) "var")) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 26) (17, 27)) (UN (Basic "*"))) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 25)) (UN (Basic "var")))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (BI 2))))]] (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (18, 12) (18, 43)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (18, 12) (18, 15)) (UN (Basic "xfn"))) (IPrimVal EmptyFC (I 99994)))
+Main> ILocal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (11, 29)) [IClaim (MkFCVal (MkIClaimData MW Private [] (MkTy (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 12) (10, 28)) (MkFCVal (UN (Basic "xfn"))) (IPi (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 18) (10, 28)) MW ExplicitArg Nothing (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 18) (10, 21)) (PrT IntType)) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (10, 25) (10, 28)) (PrT IntType)))))), IDef (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 29)) (UN (Basic "xfn")) [PatClause (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 12) (11, 15)) (UN (Basic "xfn"))) (IBindVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 16) (11, 19)) "var")) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 26) (11, 27)) (UN (Basic "*"))) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 22) (11, 25)) (UN (Basic "var")))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (12, 12) (12, 22)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (12, 12) (12, 15)) (UN (Basic "xfn"))) (IApp (MkFC (Virtual Interactive) (0, 9) (0, 22)) (IApp (MkFC (Virtual Interactive) (0, 9) (0, 22)) (IVar (MkFC (Virtual Interactive) (0, 9) (0, 12)) (UN (Basic "the"))) (IPrimVal (MkFC (Virtual Interactive) (0, 13) (0, 16)) (PrT IntType))) (IApp (MkFC (Virtual Interactive) (0, 17) (0, 22)) (IVar (MkFC (Virtual Interactive) (0, 17) (0, 22)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (Virtual Interactive) (0, 17) (0, 22)) (BI 99994)))))
+Main> ILocal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (17, 29)) [IClaim (MkFCVal (MkIClaimData MW Private [] (MkTy (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 12) (16, 28)) (MkFCVal (UN (Basic "xfn"))) (IPi (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 18) (16, 28)) MW ExplicitArg Nothing (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 18) (16, 21)) (PrT IntType)) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (16, 25) (16, 28)) (PrT IntType)))))), IDef (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 29)) (UN (Basic "xfn")) [PatClause (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 19)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 12) (17, 15)) (UN (Basic "xfn"))) (IBindVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 16) (17, 19)) "var")) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 29)) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 26) (17, 27)) (UN (Basic "*"))) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 22) (17, 25)) (UN (Basic "var")))) (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (UN (Basic "fromInteger"))) (IPrimVal (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (17, 28) (17, 29)) (BI 2))))]] (IApp (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (18, 12) (18, 43)) (IVar (MkFC (PhysicalIdrSrc (MkMI ["quote"])) (18, 12) (18, 15)) (UN (Basic "xfn"))) (IPrimVal EmptyFC (I 99994)))
 Main> [UN (Basic "names"), NS (MkNS ["Prelude"]) (UN (Basic "+"))]
 Main> Bye for now!
diff --git a/tests/idris2/reflection/reflection004/refdecl.idr b/tests/idris2/reflection/reflection004/refdecl.idr
@@ -27,7 +27,7 @@ mkPoint n
 
 logDecls : TTImp -> Elab (Int -> Int)
 logDecls v
-    = do declare [IClaim EmptyFC MW Public []
+    = do declare [IClaim $ MkFCVal EmptyFC $ MkIClaimData MW Public []
                  (MkTy EmptyFC (MkFCVal EmptyFC `{ Main.foo })
                                `(Int -> Int -> Int) )]
 

diff --git a/tests/idris2/reflection/reflection017/CanElabType.idr b/tests/idris2/reflection/reflection017/CanElabType.idr
@@ -14,7 +14,7 @@ desiredType = IApp EmptyFC (IVar EmptyFC `{CanElabType.T}) `(3)
 
 elabDecl : Name -> Elab Unit
 elabDecl n = declare [
-    IClaim EmptyFC MW Public [] $ MkTy EmptyFC (MkFCVal EmptyFC n) desiredType
+    IClaim $ MkFCVal EmptyFC $ MkIClaimData MW Public [] $ MkTy EmptyFC (MkFCVal EmptyFC n) desiredType
   ]
 
 %runElab elabDecl `{x1}

diff --git a/tests/idris2/reflection/reflection021/QuoteSearch.idr b/tests/idris2/reflection/reflection021/QuoteSearch.idr
@@ -15,7 +15,8 @@ defy = do
     logTerm "" 0 "Quoted term:" val
 
     declare [
-        IClaim fc MW Private [] (MkTy fc (MkFCVal fc (UN (Basic "y"))) (IVar fc (UN (Basic "Nat")))),
+        IClaim (MkFCVal fc (MkIClaimData MW Private []
+          (MkTy fc (MkFCVal fc (UN (Basic "y"))) (IVar fc (UN (Basic "Nat")))))),
         IDef fc (UN (Basic "y")) [PatClause fc (IVar fc (UN (Basic "y"))) (IApp fc (IApp fc (IVar fc (UN (Basic "+"))) val) val)]
     ]