list1 for parameter arguments

src/Idris/Desugar.idr

@@ -1069,28 +1069,30 @@ mutual
   desugarDecl ps (PParameters fc params pds)
       = do
            params' <- getArgs params
-           pds' <- traverse (desugarDecl (ps ++ map fst params')) pds
+           let paramList = forget params'
+           pds' <- traverse (desugarDecl (ps ++ map fst paramList)) pds
            -- Look for implicitly bindable names in the parameters
            pnames <- ifThenElse (not !isUnboundImplicits) (pure [])
              $ map concat
-             $ for (map (Builtin.snd . Builtin.snd . Builtin.snd) params')
-             $ findUniqueBindableNames fc True (ps ++ map Builtin.fst params') []
+             $ for (map (Builtin.snd . Builtin.snd . Builtin.snd) paramList)
+             $ findUniqueBindableNames fc True (ps ++ map Builtin.fst paramList) []
 
            let paramsb = map (\(n, rig, info, tm) =>
                                  (n, rig, info, doBind pnames tm)) params'
            pure [IParameters fc paramsb (concat pds')]
       where
         getArgs : Either (List1 PlainBinder)
-                         (List (Name, RigCount, PiInfo PTerm, PTerm)) ->
-                         Core (List (ImpParameter' Name))
+                         (List1 (Name, RigCount, PiInfo PTerm, PTerm)) ->
+                         Core (List1 (ImpParameter' Name))
         getArgs (Left params)
-          = traverse (\(MkPlainBinder n ty) => do
+          = traverseList1 (\(MkPlainBinder n ty) => do
               ty' <- desugar AnyExpr ps ty
-              pure (n.val, top, Explicit, ty')) (forget params)
+              pure (n.val, top, Explicit, ty')) params
         getArgs (Right params)
-          = traverse (\(n, rig, i, ntm) => do tm' <- desugar AnyExpr ps ntm
-                                              i' <- traverse (desugar AnyExpr ps) i
-                                              pure (n, rig, i', tm')) params
+          = traverseList1 (\(n, rig, i, ntm) => do
+              tm' <- desugar AnyExpr ps ntm
+              i' <- traverse (desugar AnyExpr ps) i
+              pure (n, rig, i', tm')) params
 
   desugarDecl ps (PUsing fc uimpls uds)
       = do syn <- get Syn

src/Idris/Parser.idr

@@ -1885,9 +1885,9 @@ paramDecls fname indents = do
     oldParamDecls
         = parens fname $ sepBy1 (decoratedSymbol fname ",") plainBinder
 
-    newParamDecls : OriginDesc -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
+    newParamDecls : OriginDesc -> IndentInfo -> Rule (List1 (Name, RigCount, PiInfo PTerm, PTerm))
     newParamDecls fname indents
-        = forget <$> map join (some $ typedArg fname indents)
+        = map join (some $ typedArg fname indents)
 
 
 -- topLevelClaim is for claims appearing at the top-level of the file

src/Idris/Resugar.idr

@@ -536,7 +536,7 @@ mutual
   toPDecl (IParameters fc ps ds)
       = do ds' <- traverse toPDecl ds
            pure (Just (PParameters fc
-                        (Right !(traverse (\(n, rig, info, tpe) =>
+                        (Right !(traverseList1 (\(n, rig, info, tpe) =>
                             do info' <- traverse (toPTerm startPrec) info
                                tpe' <- toPTerm startPrec tpe
                                pure (n, rig, info', tpe')) ps))

src/Idris/Syntax.idr

@@ -525,7 +525,7 @@ mutual
                Maybe TotalReq -> PDataDecl' nm -> PDecl' nm
        PParameters : FC ->
                      Either (List1 PlainBinder)
-                            (List (Name, RigCount, PiInfo (PTerm' nm), PTerm' nm)) ->
+                            (List1 (Name, RigCount, PiInfo (PTerm' nm), PTerm' nm)) ->
                      List (PDecl' nm) -> PDecl' nm
        PUsing : FC -> List (Maybe Name, PTerm' nm) ->
                 List (PDecl' nm) -> PDecl' nm

src/TTImp/Elab/Quote.idr

@@ -156,7 +156,7 @@ mutual
       = pure $ IDef fc v !(traverse getUnquoteClause d)
   getUnquoteDecl (IParameters fc ps ds)
       = pure $ IParameters fc
-                           !(traverse unqTuple ps)
+                           !(traverseList1 unqTuple ps)
                            !(traverse getUnquoteDecl ds)
     where
       unqTuple : (Name, RigCount, PiInfo RawImp, RawImp) -> Core (Name, RigCount, PiInfo RawImp, RawImp)

src/TTImp/ProcessDecls.idr

@@ -125,7 +125,7 @@ process eopts nest env (IData fc vis mbtot ddef)
 process eopts nest env (IDef fc fname def)
     = processDef eopts nest env fc fname def
 process eopts nest env (IParameters fc ps decls)
-    = processParams nest env fc ps decls
+    = processParams nest env fc (forget ps) decls
 process eopts nest env (IRecord fc ns vis mbtot rec)
     = processRecord eopts nest env ns vis mbtot rec
 process eopts nest env (IFail fc msg decls)

src/TTImp/TTImp.idr

@@ -10,7 +10,7 @@ import Core.TT
 import Core.Value
 
 import Data.List
-import Data.List1
+import public Data.List1
 import Data.Maybe
 
 import Libraries.Data.SortedSet
@@ -466,7 +466,7 @@ mutual
                Maybe TotalReq -> ImpData' nm -> ImpDecl' nm
        IDef : FC -> Name -> List (ImpClause' nm) -> ImpDecl' nm
        IParameters : FC ->
-                     List (ImpParameter' nm) ->
+                     List1 (ImpParameter' nm) ->
                      List (ImpDecl' nm) -> ImpDecl' nm
        IRecord : FC ->
                  Maybe String -> -- nested namespace

src/TTImp/Utils.idr

@@ -34,7 +34,7 @@ rawImpFromDecl decl = case decl of
         => maybe id (::) tycon $ map type datacons
     IData fc1 y _ (MkImpLater fc2 n tycon) => [tycon]
     IDef fc1 y ys => getFromClause !ys
-    IParameters fc1 ys zs => rawImpFromDecl !zs ++ map getParamTy ys
+    IParameters fc1 ys zs => rawImpFromDecl !zs ++ map getParamTy (forget ys)
     IRecord fc1 y z _ (MkImpRecord fc n params opts conName fields) => do
         (a, b) <- map (snd . snd) params
         getFromPiInfo a ++ [b] ++ getFromIField !fields