Merge pull request #3615 from andrevidela/impTy-refactor

dunhamsteve · web-flow · commit a991795cde7b · 2025-08-18T10:59:39.000-07:00
replace ImpTy
diff --git a/src/Core/WithData.idr b/src/Core/WithData.idr
@@ -109,11 +109,6 @@ setFC : {n : Nat} ->
         WithData fields a -> WithData fields a
 setFC fc = WithData.set "fc" fc @{inRange}
 
-||| Attach binding and file context information to a type
-public export
-FCBind : Type -> Type
-FCBind = WithData [ Bind', FC' ]
-
 ||| A wrapper for a value with a file context.
 public export
 MkFCVal : FC -> ty -> WithFC ty
@@ -194,16 +189,16 @@ public export
 WithName : Type -> Type
 WithName = AddMetadata Name'
 
-||| the "tyname" label containing a `FCBind Name` for metadata records
+||| the "tyname" label containing a `WithFC Name` for metadata records. Typically used for type names.
 public export
 TyName' : KeyVal
-TyName' = "tyname" :-: FCBind Name
+TyName' = "tyname" :-: WithFC Name
 
 ||| Extract the "tyname" value from the metadata record
 export
 (.tyName) : {n : Nat} ->
-            (inRange : NameInRange "tyname" fields === Just (n, FCBind Name)) =>
-            WithData fields a -> FCBind Name
+            (inRange : NameInRange "tyname" fields === Just (n, WithFC Name)) =>
+            WithData fields a -> WithFC Name
 (.tyName) = WithData.get "tyname" @{inRange}
 
 
diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr
@@ -906,7 +906,7 @@ mutual
       = flip Core.traverse (forget names) $ \(doc, n) : (String, WithFC Name) =>
           do addDocString n.val (d ++ doc)
              syn <- get Syn
-             pure $ MkImpTy pty.fc n !(bindTypeNames pty.fc (usingImpl syn)
+             pure $ Mk [pty.fc, n] !(bindTypeNames pty.fc (usingImpl syn)
                                                  ps !(desugar AnyExpr ps ty))
 
   -- Attempt to get the function name from a function pattern. For example,
diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr
@@ -185,7 +185,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
          let impTy = doBind paramBinds initTy
 
          let impTyDecl
-             = IClaim (MkFCVal vfc $ MkIClaimData top vis opts (MkImpTy EmptyFC (NoFC impName) impTy))
+             = IClaim (MkFCVal vfc $ MkIClaimData top vis opts (Mk [EmptyFC, NoFC impName] impTy))
 
          log "elab.implementation" 5 $ "Implementation type: " ++ show impTy
 
@@ -472,7 +472,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
         = do let opts = if isJust $ findTotality opts_in
                           then opts_in
                           else maybe opts_in (\t => Totality t :: opts_in) treq
-             IClaim $ MkFCVal vfc $ MkIClaimData c vis opts $ MkImpTy EmptyFC (NoFC n) mty
+             IClaim $ MkFCVal vfc $ MkIClaimData c vis opts $ Mk [EmptyFC, NoFC n] mty
 
     -- Given the method type (result of topMethType) return the mapping from
     -- top level method name to current implementation's method name
diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr
@@ -51,12 +51,12 @@ namePis i (IBindHere fc m ty) = IBindHere fc m (namePis i ty)
 namePis i ty = ty
 
 getSig : ImpDecl -> Maybe Signature
-getSig (IClaim (MkWithData _ $ MkIClaimData c _ opts (MkImpTy fc n ty)))
+getSig (IClaim (MkWithData _ $ MkIClaimData c _ opts ty))
     = Just $ MkSignature { count    = c
                          , flags    = opts
-                         , name     = n
+                         , name     = ty.tyName
                          , isData   = False
-                         , type     = namePis 0 ty
+                         , type     = namePis 0 ty.val
                          }
 getSig (IData _ _ _ (MkImpLater fc n ty))
     = Just $ MkSignature { count    = erased
@@ -121,7 +121,7 @@ mkIfaceData {vars} ifc def_vis env constraints n conName ps dets meths
           conty = mkTy vfc Implicit (map jname ps) $
                   mkTy vfc AutoImplicit (map bhere constraints) $
                   mkTy vfc Explicit (map bname meths) retty
-          con = MkImpTy vfc (NoFC conName) !(bindTypeNames ifc [] (pNames ++ map fst meths ++ toList vars) conty)
+          con = Mk [vfc, NoFC conName] !(bindTypeNames ifc [] (pNames ++ map fst meths ++ toList vars) conty)
           bound = pNames ++ map fst meths ++ toList vars in
 
           pure $ IData vfc def_vis Nothing {- ?? -}
@@ -189,7 +189,7 @@ getMethToplevel {vars} env vis iname cname constraints allmeths bindNames params
          cn <- traverse inCurrentNS sig.name
          let tydecl = IClaim (MkFCVal vfc $ MkIClaimData sig.count vis (if sig.isData then [Inline, Invertible]
                                             else [Inline])
-                                      (MkImpTy vfc cn ty_imp))
+                                      (Mk [vfc, cn] ty_imp))
          let conapp = apply (IVar vfc cname) (map (IBindVar EmptyFC) bindNames)
          let argns = getExplicitArgs 0 sig.type
          -- eta expand the RHS so that we put implicits in the right place
@@ -250,7 +250,7 @@ getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, co
                            (UN (Basic $ "__" ++ show iname ++ "_" ++ show con))
 
          let tydecl = IClaim (MkFCVal fc $ MkIClaimData top vis [Inline, Hint False]
-                             (MkImpTy EmptyFC (NoFC hintname) ty_imp))
+                             (Mk [EmptyFC, NoFC hintname] ty_imp))
 
          let conapp = apply (impsBind (IVar fc cname) constraints)
                             (map (const (Implicit fc True)) meths)
@@ -436,7 +436,7 @@ elabInterface {vars} ifc def_vis env nest constraints iname params dets mcon bod
 
              let dtydecl = IClaim $ MkFCVal vdfc
                                   $ MkIClaimData rig (collapseDefault def_vis) []
-                                  $ MkImpTy EmptyFC (NoFC dn) dty_imp
+                                  $ Mk [EmptyFC, NoFC dn] dty_imp
 
              processDecl [] nest env dtydecl
 
diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr
@@ -408,7 +408,7 @@ getItDecls
               let it = UN $ Basic "it" in
               pure [ IClaim
                        (MkFCVal replFC $ MkIClaimData top Private []
-                                       $ MkImpTy replFC (NoFC it) (Implicit replFC False))
+                                       $ Mk [replFC, NoFC it] (Implicit replFC False))
                   , IDef replFC it [PatClause replFC (IVar replFC it) (IVar replFC n)]]
 
 ||| Produce the elaboration of a PTerm, along with its inferred type
diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr
@@ -473,8 +473,8 @@ mutual
   toPTypeDecl : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 ImpTy' KindedName -> Core (PTypeDecl' KindedName)
-  toPTypeDecl (MkImpTy fc n ty)
-      = pure (MkFCVal fc $ MkPTy (pure ("", n)) "" !(toPTerm startPrec ty))
+  toPTypeDecl impTy
+      = pure (MkFCVal impTy.fc $ MkPTy (pure ("", impTy.tyName)) "" !(toPTerm startPrec impTy.val))
 
   toPData : {auto c : Ref Ctxt Defs} ->
             {auto s : Ref Syn SyntaxInfo} ->
diff --git a/src/TTImp/Elab/Local.idr b/src/TTImp/Elab/Local.idr
@@ -99,8 +99,8 @@ localHelper {vars} nest env nestdecls_in func
     -- When we encounter the names in elaboration, we'll update to an
     -- application of the nested name.
     updateTyName : NestedNames vars -> ImpTy -> ImpTy
-    updateTyName nest (MkImpTy loc' n ty)
-        = MkImpTy loc' (map (mapNestedName nest) n) ty
+    updateTyName nest ty
+        = update "tyname" (map (mapNestedName nest)) ty
 
     updateDataName : NestedNames vars -> ImpData -> ImpData
     updateDataName nest (MkImpData loc' n tycons dopts dcons)
diff --git a/src/TTImp/Elab/Quote.idr b/src/TTImp/Elab/Quote.idr
@@ -104,13 +104,6 @@ mutual
   getUnquoteUpdate (ISetField p t) = pure $ ISetField p !(getUnquote t)
   getUnquoteUpdate (ISetFieldApp p t) = pure $ ISetFieldApp p !(getUnquote t)
 
-  getUnquoteTy : {auto c : Ref Ctxt Defs} ->
-                 {auto q : Ref Unq (List (Name, FC, RawImp))} ->
-                 {auto u : Ref UST UState} ->
-                 ImpTy ->
-                 Core ImpTy
-  getUnquoteTy (MkImpTy fc n t) = pure $ MkImpTy fc n !(getUnquote t)
-
   getUnquoteRecord : {auto c : Ref Ctxt Defs} ->
                      {auto q : Ref Unq (List (Name, FC, RawImp))} ->
                      {auto u : Ref UST UState} ->
@@ -128,7 +121,7 @@ mutual
                    Core ImpData
   getUnquoteData (MkImpData fc n tc opts cs)
       = pure $ MkImpData fc n !(traverseOpt getUnquote tc) opts
-                         !(traverse getUnquoteTy cs)
+                         !(traverse (traverse getUnquote) cs)
   getUnquoteData (MkImpLater fc n tc)
       = pure $ MkImpLater fc n !(getUnquote tc)
 
@@ -138,7 +131,7 @@ mutual
                    ImpDecl ->
                    Core ImpDecl
   getUnquoteDecl (IClaim (MkWithData fc (MkIClaimData c v opts ty)))
-      = pure $ IClaim (MkWithData fc (MkIClaimData c v opts !(getUnquoteTy ty)))
+      = pure $ IClaim (MkWithData fc (MkIClaimData c v opts !(traverse getUnquote ty)))
   getUnquoteDecl (IData fc v mbt d)
       = pure $ IData fc v mbt !(getUnquoteData d)
   getUnquoteDecl (IDef fc v d)
diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr
@@ -501,13 +501,14 @@ mutual
 tyDecl : OriginDesc -> IndentInfo -> Rule ImpTy
 tyDecl fname indents
     = do start <- location
-         n <- name
+         n <- withFC name
          nameEnd <- location
          symbol ":"
          ty <- expr fname indents
          end <- location
          atEnd indents
-         pure (MkImpTy (MkFC fname start end) (MkFCVal (MkFC fname start nameEnd) n) ty)
+         let fc = MkFC fname start end
+         pure (Mk [fc, n] ty)
 
 mutual
   parseRHS : (withArgs : Nat) ->
diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr
@@ -94,9 +94,11 @@ checkCon : {vars : _} ->
            List ElabOpt -> NestedNames vars ->
            Env Term vars -> Visibility -> (orig : Name) -> (resolved : Name) ->
            ImpTy -> Core Constructor
-checkCon {vars} opts nest env vis tn_in tn (MkImpTy fc cn_in ty_raw)
-    = do cn <- inCurrentNS cn_in.val
-         let ty_raw = updateNS tn_in tn ty_raw
+checkCon {vars} opts nest env vis tn_in tn ty_raw
+    = do let cn_in = ty_raw.tyName
+         let fc = ty_raw.fc
+         cn <- inCurrentNS cn_in.val
+         let ty_raw = updateNS tn_in tn ty_raw.val
          log "declare.data.constructor" 5 $ "Checking constructor type " ++ show cn ++ " : " ++ show ty_raw
          log "declare.data.constructor" 10 $ "Updated " ++ show (tn_in, tn)
 
diff --git a/src/TTImp/ProcessDecls.idr b/src/TTImp/ProcessDecls.idr
@@ -171,9 +171,8 @@ processTTImpDecls {vars} nest env decls
          pure True -- TODO: False on error
   where
     bindConNames : ImpTy -> Core ImpTy
-    bindConNames (MkImpTy fc n ty)
-        = do ty' <- bindTypeNames fc [] (toList vars) ty
-             pure (MkImpTy fc n ty')
+    bindConNames ty
+        = traverse (bindTypeNames ty.fc [] (toList vars)) ty
 
     bindDataNames : ImpData -> Core ImpData
     bindDataNames (MkImpData fc n t opts cons)
@@ -186,9 +185,9 @@ processTTImpDecls {vars} nest env decls
 
     -- bind implicits to make raw TTImp source a bit friendlier
     bindNames : ImpDecl -> Core ImpDecl
-    bindNames (IClaim dat@(MkWithData fc (MkIClaimData c vis opts (MkImpTy tfc n ty))))
-        = do ty' <- bindTypeNames dat.fc [] (toList vars) ty
-             pure (IClaim (MkWithData fc (MkIClaimData c vis opts (MkImpTy tfc n ty'))))
+    bindNames (IClaim dat@(MkWithData fc (MkIClaimData c vis opts ty)))
+        = do ty' <- bindTypeNames dat.fc [] (toList vars) ty.val
+             pure (IClaim (MkWithData fc (MkIClaimData c vis opts ({val := ty'} ty))))
     bindNames (IData fc vis mbtot d)
         = do d' <- bindDataNames d
              pure (IData fc vis mbtot d')
diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr
@@ -943,7 +943,7 @@ lookupOrAddAlias eopts nest env fc n [cl@(PatClause _ lhs _)]
        log "declare.def" 5 "Not a misspelling: go ahead and declare it!"
        processType eopts nest env fc top Public []
           -- See #3409
-          $ MkImpTy fc (MkFCVal fc n) $ holeyType (map snd args)
+          $ Mk [fc, MkFCVal fc n] $ holeyType (map snd args)
        defs <- get Ctxt
        lookupCtxtExact n (gamma defs)
 
diff --git a/src/TTImp/ProcessRecord.idr b/src/TTImp/ProcessRecord.idr
@@ -221,7 +221,7 @@ elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conNa
              let conty = mkTy (paramTelescope params) $
                          mkTy (map farg fields) (recTy tn params)
              let boundNames = paramNames params ++ map fname fields ++ (toList vars)
-             let con = MkImpTy (virtualiseFC fc) (NoFC cname)
+             let con = Mk [virtualiseFC fc, NoFC cname]
                        !(bindTypeNames fc [] boundNames conty)
              let dt = MkImpData fc tn Nothing opts [con]
              log "declare.record" 5 $ "Record data type " ++ show dt
@@ -274,7 +274,7 @@ elabRecord {vars} eopts fc env nest newns def_vis mbtot tn_in params0 opts conNa
                                       IPi bfc top Explicit (Just rname) (recTy tn params) ty'
                    let fc' = virtualiseFC fc
                    let mkProjClaim = \ nm =>
-                          let ty = MkImpTy fc' (MkFCVal fc' nm) projTy
+                          let ty = Mk [fc', MkFCVal fc' nm] projTy
                           in IClaim (MkFCVal bfc (MkIClaimData rig isVis [Inline] ty))
 
                    log "declare.record.projection.claim" 5 $
diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr
@@ -145,10 +145,12 @@ processType : {vars : _} ->
               List ElabOpt -> NestedNames vars -> Env Term vars ->
               FC -> RigCount -> Visibility ->
               List FnOpt -> ImpTy -> Core ()
-processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
-    = do n <- inCurrentNS n_in.val
+processType {vars} eopts nest env fc rig vis opts ty_raw
+    = do let typeName = ty_raw.tyName
+         n <- inCurrentNS typeName.val
+         let tfc = ty_raw.fc
 
-         addNameLoc n_in.fc n
+         addNameLoc typeName.fc n
 
          log "declare.type" 1 $ "Processing " ++ show n
          log "declare.type" 5 $ unwords ["Checking type decl:", show rig, show n, ":", show ty_raw]
@@ -163,7 +165,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
          ty <-
              wrapErrorC eopts (InType fc n) $
                    checkTerm idx InType (HolesOkay :: eopts) nest env
-                             (IBindHere fc (PI erased) ty_raw)
+                             (IBindHere fc (PI erased) ty_raw.val)
                              (gType fc u)
          logTermNF "declare.type" 3 ("Type of " ++ show n) Env.empty (abstractFullEnvType tfc env ty)
 
@@ -202,7 +204,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
          addTyDecl fc (Resolved idx) env ty -- for definition generation
 
          log "metadata.names" 7 $ "processType is adding ↓"
-         addNameType n_in.fc (Resolved idx) env ty -- for looking up types
+         addNameType typeName.fc (Resolved idx) env ty -- for looking up types
 
          traverse_ addToSave (keys (getMetas ty))
          addToSave n
@@ -214,5 +216,5 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw)
                  log "module.hash" 15 "Adding hash for type with name \{show n}"
 
          when (showShadowingWarning !getSession) $
-            whenJust (fromList (checkForShadowing StringMap.empty ty_raw))
+            whenJust (fromList (checkForShadowing StringMap.empty ty_raw.val))
                 $ recordWarning . ShadowingLocalBindings fc
diff --git a/src/TTImp/Reflect.idr b/src/TTImp/Reflect.idr
@@ -313,10 +313,10 @@ mutual
     reify defs val@(NDCon _ n _ _ args)
         = case (dropAllNS !(full (gamma defs) n), map snd args) of
                (UN (Basic "MkTy"), [w, y, z])
-                    => do w' <- reify defs !(evalClosure defs w)
-                          y' <- reify defs !(evalClosure defs y)
-                          z' <- reify defs !(evalClosure defs z)
-                          pure (MkImpTy w' y' z')
+                    => do fc' <- reify defs !(evalClosure defs w)
+                          name' <- the (Core (WithFC Name)) (reify defs !(evalClosure defs y))
+                          term' <- reify defs !(evalClosure defs z)
+                          pure (Mk [fc', name'] term')
                _ => cantReify val "ITy"
     reify defs val = cantReify val "ITy"
 
@@ -696,10 +696,10 @@ mutual
 
   export
   Reflect ImpTy where
-    reflect fc defs lhs env (MkImpTy w x z)
-        = do w' <- reflect fc defs lhs env w
-             x' <- reflect fc defs lhs env x
-             z' <- reflect fc defs lhs env z
+    reflect fc defs lhs env ty
+        = do w' <- reflect fc defs lhs env ty.fc
+             x' <- reflect fc defs lhs env ty.tyName
+             z' <- reflect fc defs lhs env ty.val
              appCon fc defs (reflectionttimp "MkTy") [w', x', z']
 
   export
diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr
@@ -311,18 +311,13 @@ mutual
   ImpTy = ImpTy' Name
 
   public export
-  record ImpTy' (nm : Type) where
-      constructor MkImpTy
-      loc : FC
-      name : WithFC Name
-      type : RawImp' nm
-
-  %name ImpTy' ty
+  ImpTy' : Type -> Type
+  ImpTy' = AddMetadata FC' . AddMetadata TyName' . RawImp'
 
   export
   covering
   Show nm => Show (ImpTy' nm) where
-    show (MkImpTy fc n ty) = "(%claim " ++ show n.val ++ " " ++ show ty ++ ")"
+    show ty = "(%claim " ++ show ty.tyName.val ++ " " ++ show ty.val ++ ")"
 
   public export
   ImpData : Type
@@ -813,7 +808,7 @@ definedInBlock ns decls =
     Prelude.toList $ foldl (defName ns) empty decls
   where
     getName : ImpTy -> Name
-    getName (MkImpTy _ n _) = n.val
+    getName = (.tyName.val)
 
     getFieldName : IField -> Name
     getFieldName f = f.name.val
diff --git a/src/TTImp/TTImp/Functor.idr b/src/TTImp/TTImp/Functor.idr
@@ -90,7 +90,7 @@ mutual
   export
   Functor IClaimData where
     map f (MkIClaimData rig vis opts ty)
-      = MkIClaimData rig vis (map (map f) opts) (map f ty)
+      = MkIClaimData rig vis (map (map f) opts) (map (map f) ty)
 
   export
   Functor ImpDecl' where
@@ -133,15 +133,10 @@ mutual
     map f Macro = Macro
     map f (SpecArgs ns) = SpecArgs ns
 
-  export
-  Functor ImpTy' where
-    map f (MkImpTy fc n ty)
-      = MkImpTy fc n (map f ty)
-
   export
   Functor ImpData' where
     map f (MkImpData fc n tycon opts datacons)
-      = MkImpData fc n (map (map f) tycon) opts (map (map f) datacons)
+      = MkImpData fc n (map (map f) tycon) opts (map (map (map f)) datacons)
     map f (MkImpLater fc n tycon)
       = MkImpLater fc n (map f tycon)
 
diff --git a/src/TTImp/TTImp/TTC.idr b/src/TTImp/TTImp/TTC.idr
diff --git a/src/TTImp/TTImp/Traversals.idr b/src/TTImp/TTImp/Traversals.idr
diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr
