[ new ] Support arbitrary Name in IBindVar

CHANGELOG_NEXT.md

@@ -129,6 +129,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * Fixed a bug that caused `ttc` size to grow exponentially.
 
+* `IBindVar` supports arbitrary names. `String` in the signature is replaced
+  by `Name`.
+
 ### Backend changes
 
 #### RefC Backend

libs/base/Language/Reflection/TTImp.idr

@@ -57,7 +57,7 @@ mutual
        -- the given binder
        IBindHere : FC -> BindMode -> TTImp -> TTImp
        -- A name which should be implicitly bound
-       IBindVar : FC -> String -> TTImp
+       IBindVar : FC -> Name -> TTImp
        -- An 'as' pattern, valid on the LHS of a clause only
        IAs : FC -> (nameFC : FC) -> UseSide -> Name -> TTImp -> TTImp
        -- A 'dot' pattern, i.e. one which must also have the given value
@@ -676,7 +676,7 @@ mutual
     showPrec d (IRewrite fc s t)
       = showParens (d > Open) "rewrite \{show s} in \{show t}"
     showPrec d (IBindHere fc bm s) = showPrec d s
-    showPrec d (IBindVar fc x) = x
+    showPrec d (IBindVar fc x) = showPrec d x
     showPrec d (IAs fc nameFC side nm s)
       = "\{show nm}@\{showPrec App s}"
     showPrec d (IMustUnify fc dr s) = ".(\{show s})"

src/Core/Binary.idr

@@ -29,7 +29,7 @@ import public Libraries.Utils.Binary
 ||| version number if you're changing the version more than once in the same day.
 export
 ttcVersion : Int
-ttcVersion = 2025_05_09_00
+ttcVersion = 2025_05_21_00
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Core/Core.idr

@@ -65,7 +65,7 @@ data Warning : Type where
      ParserWarning : FC -> String -> Warning
      UnreachableClause : {vars : _} ->
                          FC -> Env Term vars -> Term vars -> Warning
-     ShadowingGlobalDefs : FC -> List1 (String, List1 Name) -> Warning
+     ShadowingGlobalDefs : FC -> List1 (Name, List1 Name) -> Warning
      ||| Soft-breaking change, make an error later.
      ||| @ original Originally declared visibility on forward decl
      ||| @ new      Incompatible new visibility on actual declaration.

src/Idris/Desugar.idr

@@ -1281,7 +1281,7 @@ mutual
                                          (ps ++ fnames ++ paramNames) [])
                                        (map (\(_,_,_,d) => d) params')
                         else []
-           let _ = the (List (String, String)) bnames
+           let _ = the (List (Name, Name)) bnames
 
            let paramsb = map (\ (n, c, p, tm) => (n, c, p, doBind bnames tm)) params'
            let _ = the (List (Name, RigCount, PiInfo RawImp, RawImp)) paramsb

src/Idris/Elab/Implementation.idr

@@ -238,7 +238,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
 
                -- 2. Elaborate top level function types for this interface
                defs <- get Ctxt
-               fns <- topMethTypes [] impName methImps impsp
+               fns <- topMethTypes [] impName methImps (show <$> impsp)
                                       (implParams cdata) (params cdata)
                                       (map name (methods cdata))
                                       (methods cdata)
@@ -248,7 +248,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
                let mtops = map (Builtin.fst . snd) fns
                let con = iconstructor cdata
                let ilhs = impsApply (IVar EmptyFC impName)
-                                    (map (\x => (x, IBindVar vfc (show x)))
+                                    (map (\x => (x, IBindVar vfc x))
                                               (map fst methImps))
                -- RHS is the constructor applied to a search for the necessary
                -- parent constraints, then the method implementations
@@ -363,7 +363,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
               mkLam argns
                     (impsApply
                          (applyTo (IVar EmptyFC n) argns)
-                         (map (\n => (n, IVar vfc (UN (Basic $ show n)))) imps))
+                         (map (\n => (n, IVar vfc n)) imps))
       where
         applyUpdate : (Name, RigCount, PiInfo RawImp) ->
                       (Name, RigCount, PiInfo RawImp)
@@ -410,7 +410,8 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
              -- parameters
              let upds' = !(traverse (applyCon impName) allmeths)
              let mty_in = substNames vars upds' meth.type
-             let (upds, mty_in) = runState Prelude.Nil (renameIBinds impsp (findImplicits mty_in) mty_in)
+             let implicits = show <$> findImplicits mty_in
+             let (upds, mty_in) = runState Prelude.Nil (renameIBinds impsp implicits mty_in)
              -- Finally update the method type so that implicits from the
              -- parameters are passed through to any earlier methods which
              -- appear in the type
@@ -432,7 +433,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
              let mbase = bindImps methImps $
                          bindConstraints vfc AutoImplicit cons $
                          mty_params
-             let ibound = findImplicits mbase
+             let ibound = show <$> findImplicits mbase
 
              mty <- bindTypeNamesUsed ifc ibound vars mbase
 
@@ -448,7 +449,7 @@ elabImplementation {vars} ifc vis opts_in pass env nest is cons iname ps named i
              let ibinds = map fst methImps
              let methupds' = if isNil ibinds then []
                              else [(n, impsApply (IVar vfc n)
-                                     (map (\x => (x, IBindVar vfc (show x))) ibinds))]
+                                     (map (\x => (x, IBindVar vfc x)) ibinds))]
 
              pure ((meth.name, n, upds, meth.count, meth.totalReq, mty), methupds')
 

src/Idris/Elab/Interface.idr

@@ -189,7 +189,7 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params sig
                                             else [Inline])
                                       (MkImpTy vfc cn ty_imp))
          let conapp = apply (IVar vfc cname)
-                            (map (IBindVar EmptyFC) (map bindName allmeths))
+                            (map (IBindVar EmptyFC) (map methName allmeths))
          let argns = getExplicitArgs 0 sig.type
          -- eta expand the RHS so that we put implicits in the right place
          let fnclause = PatClause vfc
@@ -259,7 +259,7 @@ getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, co
          let tydecl = IClaim (MkFCVal fc $ MkIClaimData top vis [Inline, Hint False]
                           (MkImpTy EmptyFC (NoFC hintname) ty_imp))
 
-         let conapp = apply (impsBind (IVar fc cname) (map bindName constraints))
+         let conapp = apply (impsBind (IVar fc cname) (map constName constraints))
                               (map (const (Implicit fc True)) meths)
 
          let fnclause = PatClause fc (IApp fc (IVar fc hintname) conapp)
@@ -275,7 +275,7 @@ getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, co
     constName : Name -> Name
     constName n = UN (Basic $ bindName n)
 
-    impsBind : RawImp -> List String -> RawImp
+    impsBind : RawImp -> List Name -> RawImp
     impsBind fn [] = fn
     impsBind fn (n :: ns)
         = impsBind (IAutoApp fc fn (IBindVar fc n)) ns
@@ -474,8 +474,8 @@ elabInterface {vars} ifc def_vis env nest constraints iname params dets mcon bod
 
         applyParams : RawImp -> List Name -> RawImp
         applyParams tm [] = tm
-        applyParams tm (UN (Basic n) :: ns)
-            = applyParams (INamedApp vdfc tm (UN (Basic n)) (IBindVar vdfc n)) ns
+        applyParams tm (n@(UN (Basic _)) :: ns)
+            = applyParams (INamedApp vdfc tm n (IBindVar vdfc n)) ns
         applyParams tm (_ :: ns) = applyParams tm ns
 
         changeNameTerm : Name -> RawImp -> Core RawImp

src/Idris/Error.idr

@@ -272,7 +272,7 @@ pwarningRaw (ShadowingGlobalDefs fc ns)
    :: map pshadowing (forget ns)
    `snoc` !(ploc fc)
   where
-    pshadowing : (String, List1 Name) -> Doc IdrisAnn
+    pshadowing : (Name, List1 Name) -> Doc IdrisAnn
     pshadowing (n, ns) = indent 2 $ hsep $
                            pretty0 n
                         :: reflow "is shadowing"

src/Idris/Parser.idr

@@ -76,7 +76,7 @@ decoratedDataConstructorName : OriginDesc -> Rule Name
 decoratedDataConstructorName fname = decorate fname Data dataConstructorName
 
 decoratedSimpleBinderUName : OriginDesc -> Rule Name
-decoratedSimpleBinderUName fname = decorate fname Bound (UN . Basic <$> unqualifiedName)
+decoratedSimpleBinderUName fname = decorate fname Bound userName
 
 decoratedSimpleNamedArg : OriginDesc -> Rule String
 decoratedSimpleNamedArg fname
@@ -1627,10 +1627,7 @@ parameters {auto fname : OriginDesc} {auto indents : IndentInfo}
            commit
            decoratedSymbol fname "("
            us <- sepBy (decoratedSymbol fname ",")
-                       (do n <- optional $ do
-                                      x <- unqualifiedName
-                                      decoratedSymbol fname ":"
-                                      pure (UN $ Basic x)
+                       (do n <- optional $ userName <* decoratedSymbol fname ":"
                            ty <- typeExpr pdef fname indents
                            pure (n, ty))
            decoratedSymbol fname ")"

src/Idris/Resugar.idr

@@ -287,11 +287,11 @@ mutual
                       else toPTerm p ret
     where
       needsBind : Maybe Name -> Bool
-      needsBind (Just nm@(UN (Basic t)))
+      needsBind (Just nm@(UN (Basic _)))
           = let ret = map rawName ret
                 ns = findBindableNames False [] [] ret
                 allNs = findAllNames [] ret in
-                (nm `elem` allNs) && not (t `elem` (map Builtin.fst ns))
+                (nm `elem` allNs) && not (nm `elem` (map Builtin.fst ns))
       needsBind _ = False
   toPTerm p (IPi fc rig pt n arg ret)
       = do arg' <- toPTerm appPrec arg
@@ -375,9 +375,8 @@ mutual
   toPTerm p (IPrimVal fc c) = pure (PPrimVal fc c)
   toPTerm p (IHole fc str) = pure (PHole fc False str)
   toPTerm p (IType fc) = pure (PType fc)
-  toPTerm p (IBindVar fc v)
-    = let nm = UN (Basic v) in
-      pure (PRef fc (MkKindedName (Just Bound) nm nm))
+  toPTerm p (IBindVar fc nm)
+    = pure (PRef fc (MkKindedName (Just Bound) nm nm))
   toPTerm p (IBindHere fc _ tm) = toPTerm p tm
   toPTerm p (IAs fc nameFC _ n pat) = pure (PAs fc nameFC n !(toPTerm argPrec pat))
   toPTerm p (IMustUnify fc r pat) = pure (PDotted fc !(toPTerm argPrec pat))

src/Parser/Rule/Source.idr

@@ -347,6 +347,10 @@ export
 unqualifiedName : Rule String
 unqualifiedName = identPart
 
+export
+userName : Rule Name
+userName = UN . Basic <$> unqualifiedName
+
 export
 holeName : Rule String
 holeName

src/TTImp/BindImplicits.idr

@@ -68,30 +68,28 @@ renameIBinds rs us (IAlternative fc u alts)
     renameAlt : AltType -> State (List (String, String)) AltType
     renameAlt (UniqueDefault t) = pure $ UniqueDefault !(renameIBinds rs us t)
     renameAlt u = pure u
-renameIBinds rs us (IBindVar fc n)
+renameIBinds rs us (IBindVar fc nm@(UN (Basic n)))
     = if n `elem` rs
          then do let n' = genUniqueStr (rs ++ us) n
                  upds <- get
                  put ((n, n') :: upds)
-                 pure $ IBindVar fc n'
-         else pure $ IBindVar fc n
+                 pure $ IBindVar fc (UN (Basic n'))
+         else pure $ IBindVar fc nm
 renameIBinds rs us tm = pure $ tm
 
 export
-doBind : List (String, String) -> RawImp -> RawImp
+doBind : List (Name, Name) -> RawImp -> RawImp
 doBind [] tm = tm
-doBind ns (IVar fc nm@(UN (Basic n)))
-    = maybe (IVar fc nm)
-            (IBindVar fc)
-            (lookup n ns)
+doBind ns (IVar fc nm)
+    = maybe (IVar fc nm) (IBindVar fc) (lookup nm ns)
 doBind ns (IPi fc rig p mn aty retty)
     = let ns' = case mn of
-                     Just (UN (Basic n)) => filter (\x => fst x /= n) ns
+                     Just nm => filter (\x => fst x /= nm) ns
                      _ => ns in
           IPi fc rig p mn (doBind ns' aty) (doBind ns' retty)
 doBind ns (ILam fc rig p mn aty sc)
     = let ns' = case mn of
-                     Just (UN (Basic n)) => filter (\x => fst x /= n) ns
+                     Just nm => filter (\x => fst x /= nm) ns
                      _ => ns in
           ILam fc rig p mn (doBind ns' aty) (doBind ns' sc)
 doBind ns (IApp fc fn av)
@@ -129,7 +127,7 @@ bindNames arg tm
     = if !isUnboundImplicits
          then do let ns = nub (findBindableNames arg [] [] tm)
                  log "elab.bindnames" 10 $ "Found names :" ++ show ns
-                 pure (map (UN . Basic) (map snd ns), doBind ns tm)
+                 pure (map snd ns, doBind ns tm)
          else pure ([], tm)
 
 -- if the name is part of the using decls, add the relevant binder for it:
@@ -196,8 +194,8 @@ piBindNames loc env tm
     = do ns <- findUniqueBindableNames loc True env [] tm
          pure $ piBind (map fst ns) tm
   where
-    piBind : List String -> RawImp -> RawImp
+    piBind : List Name -> RawImp -> RawImp
     piBind [] ty = ty
     piBind (n :: ns) ty
-       = IPi loc erased Implicit (Just (UN $ Basic n)) (Implicit loc False)
+       = IPi loc erased Implicit (Just n) (Implicit loc False)
        $ piBind ns ty

src/TTImp/Elab/Ambiguity.idr

@@ -36,7 +36,7 @@ expandAmbigName : {vars : _} ->
                   RawImp -> Maybe (Glued vars) -> Core RawImp
 expandAmbigName (InLHS _) nest env orig args (IBindVar fc n) exp
     = do est <- get EST
-         if UN (Basic n) `elem` lhsPatVars est
+         if n `elem` lhsPatVars est
             then pure $ IMustUnify fc NonLinearVar orig
             else pure $ orig
 expandAmbigName mode nest env orig args (IVar fc x) exp

src/TTImp/Elab/Case.idr

@@ -335,7 +335,7 @@ caseBlock {vars} rigc elabinfo fc nest env opts scr scrtm scrty caseRig alts exp
     -- Names used in the pattern we're matching on, so don't bind them
     -- in the generated case block
     usedIn : RawImp -> List Name
-    usedIn (IBindVar _ n) = [UN $ Basic n]
+    usedIn (IBindVar _ n) = [n]
     usedIn (IApp _ f a) = usedIn f ++ usedIn a
     usedIn (IAs _ _ _ n a) = n :: usedIn a
     usedIn (IAlternative _ _ alts) = concatMap usedIn alts

src/TTImp/Elab/ImplicitBind.idr

@@ -423,20 +423,20 @@ checkBindVar : {vars : _} ->
                {auto o : Ref ROpts REPLOpts} ->
                RigCount -> ElabInfo ->
                NestedNames vars -> Env Term vars ->
-               FC -> UserName -> -- username is base of the pattern name
+               FC -> Name ->
                Maybe (Glued vars) ->
                Core (Term vars, Glued vars)
-checkBindVar rig elabinfo nest env fc str topexp
+checkBindVar rig elabinfo nest env fc nm topexp
     = do let elabmode = elabMode elabinfo
          -- In types, don't rebind if the name is already in scope;
          -- Below, return True if we don't need to implicitly bind the name
          let False = case implicitMode elabinfo of
-                          PI _ => maybe False (const True) (defined (UN str) env)
+                          PI _ => maybe False (const True) (defined nm env)
                           _ => False
-               | _ => check rig elabinfo nest env (IVar fc (UN str)) topexp
+               | _ => check rig elabinfo nest env (IVar fc nm) topexp
          est <- get EST
-         let n = PV (UN str) (defining est)
-         noteLHSPatVar elabmode (UN str)
+         let n = PV nm (defining est)
+         noteLHSPatVar elabmode nm
          notePatVar n
          est <- get EST
 
@@ -459,20 +459,20 @@ checkBindVar rig elabinfo nest env fc str topexp
                                 toBind $= ((n, NameBinding fc rig Explicit tm bty) :: ) }
 
                    log "metadata.names" 7 $ "checkBindVar is adding ↓"
-                   addNameType fc (UN str) env exp
-                   addNameLoc fc (UN str)
+                   addNameType fc nm env exp
+                   addNameLoc fc nm
 
                    checkExp rig elabinfo env fc tm (gnf env exp) topexp
               Just bty =>
                 do -- Check rig is consistent with the one in bty, and
                    -- update if necessary
-                   combine (UN str) rig (bindingRig bty)
+                   combine nm rig (bindingRig bty)
                    let tm = bindingTerm bty
                    let ty = bindingType bty
 
                    log "metadata.names" 7 $ "checkBindVar is adding ↓"
-                   addNameType fc (UN str) env ty
-                   addNameLoc fc (UN str)
+                   addNameType fc nm env ty
+                   addNameLoc fc nm
 
                    checkExp rig elabinfo env fc tm (gnf env ty) topexp
   where

src/TTImp/Elab/Record.idr

@@ -59,7 +59,7 @@ Show Rec where
 toLHS' : FC -> Rec -> (Maybe Name, RawImp)
 toLHS' loc (Field mn@(Just _) n _)
     = (mn, IAs loc (virtualiseFC loc) UseRight (UN $ Basic n) (Implicit loc True))
-toLHS' loc (Field mn n _) = (mn, IBindVar (virtualiseFC loc) n)
+toLHS' loc (Field mn n _) = (mn, IBindVar (virtualiseFC loc) (UN $ Basic n))
 toLHS' loc (Constr mn con args)
     = let args' = map (toLHS' loc . snd) args in
           (mn, gapply (IVar loc con) args')

src/TTImp/Elab/Term.idr

@@ -185,7 +185,7 @@ checkTerm rig elabinfo nest env (ICoerced fc tm) exp
 checkTerm rig elabinfo nest env (IBindHere fc binder sc) exp
     = checkBindHere rig elabinfo nest env fc binder sc exp
 checkTerm rig elabinfo nest env (IBindVar fc n) exp
-    = checkBindVar rig elabinfo nest env fc (Basic n) exp
+    = checkBindVar rig elabinfo nest env fc n exp
 checkTerm rig elabinfo nest env (IAs fc nameFC side n_in tm) exp
     = checkAs rig elabinfo nest env fc nameFC side n_in tm exp
 checkTerm rig elabinfo nest env (IMustUnify fc reason tm) exp

src/TTImp/Interactive/CaseSplit.idr

@@ -144,7 +144,7 @@ expandCon fc usedvars con
          Just ty <- lookupTyExact con (gamma defs)
               | Nothing => undefinedName fc con
          pure (apply (IVar fc con)
-                (map (IBindVar fc)
+                (map (IBindVar fc . UN . Basic)
                      !(getArgNames defs [] usedvars []
                                    !(nf defs [] ty))))