@@ -175,8 +175,8 @@ elabRecordFunctions :: ElabInfo
175175elabRecordFunctions info rsyn fc tyn params fields dconName target
176176 = do logElab 1 $ "Elaborating helper functions for record " ++ show tyn
177177
178− logElab 1 $ "Fields: " ++ show fieldNames
179− logElab 1 $ "Params: " ++ show paramNames
178+ logElab 3 $ "Fields: " ++ show fieldNames
179+ logElab 3 $ "Params: " ++ show paramNames
180180 -- The elaborated constructor type for the data declaration
181181 i <- getIState
182182 ttConsTy <-
@@ -186,8 +186,8 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target
186186
187187 -- The arguments to the constructor
188188 let constructorArgs = getArgTys ttConsTy
189− logElab 1 $ "Cons args: " ++ show constructorArgs
190− logElab 1 $ "Free fields: " ++ show (filter (not . isFieldOrParam') constructorArgs)
189+ logElab 3 $ "Cons args: " ++ show constructorArgs
190+ logElab 3 $ "Free fields: " ++ show (filter (not . isFieldOrParam') constructorArgs)
191191 -- If elaborating the constructor has resulted in some new implicit fields we make projection functions for them.
192192 let freeFieldsForElab = map (freeField i) (filter (not . isFieldOrParam') constructorArgs)
193193
@@ -201,16 +201,16 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target
201201 -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.
202202 let projectors = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (freeFieldsForElab ++ paramsForElab ++ userFieldsForElab) [0..]]
203203 -- Build and elaborate projection functions
204− elabProj dconName projectors
204+ elabProj dconName paramNames projectors
205205
206− logElab 1 $ "Dependencies: " ++ show fieldDependencies
206+ logElab 3 $ "Dependencies: " ++ show fieldDependencies
207207
208− logElab 1 $ "Depended on: " ++ show dependedOn
208+ logElab 3 $ "Depended on: " ++ show dependedOn
209209
210210 -- All things we need to elaborate update functions for, together with a number denoting their position in the constructor.
211211 let updaters = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (paramsForElab ++ userFieldsForElab) [0..]]
212212 -- Build and elaborate update functions
213− elabUp dconName updaters
213+ elabUp dconName paramNames updaters
214214 where
215215 -- | Creates a PArg from a plicity and a name where the term is a Placeholder.
216216 placeholderArg :: Plicity -> Name -> PArg
@@ -270,20 +270,22 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target
270270 paramName n = n
271271
272272 -- | Elaborate the projection functions.
273− elabProj :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()
274− elabProj cn fs = let phArgs = map (uncurry placeholderArg) [(p, n) | (n, _, p, _, _, _) <- fs]
273+ elabProj :: Name -> [Name] -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()
274+ elabProj cn paramnames fs
275+ = let phArgs = map (uncurry placeholderArg) [(p, n) | (n, _, p, _, _, _) <- fs]
275276 elab = \(n, n', p, t, doc, i) ->
276277 -- Use projections in types
277278 do let t' = projectInType [(m, m') | (m, m', _, _, _, _) <- fs
278279 -- Parameters are already in scope, so just use them
279280 , not (m `elem` paramNames)] t
280− elabProjection info n n' p t' doc rsyn fc target cn phArgs fieldNames i
281+ elabProjection info n paramnames n' p t' doc rsyn fc target cn phArgs fieldNames i
281282 in mapM_ elab fs
282283
283284 -- | Elaborate the update functions.
284− elabUp :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()
285− elabUp cn fs = let args = map (uncurry asPRefArg) [(p, n) | (n, _, p, _, _, _) <- fs]
286− elab = \(n, n', p, t, doc, i) -> elabUpdate info n n' p t doc rsyn fc target cn args fieldNames i (optionalSetter n)
285+ elabUp :: Name -> [Name] -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()
286+ elabUp cn paramnames fs
287+ = let args = map (uncurry asPRefArg) [(p, n) | (n, _, p, _, _, _) <- fs]
288+ elab = \(n, n', p, t, doc, i) -> elabUpdate info n paramnames n' p t doc rsyn fc target cn args fieldNames i (optionalSetter n)
287289 in mapM_ elab fs
288290
289291 -- | Decides whether a setter should be generated for a field or not.
@@ -313,6 +315,7 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target
313315-- | Creates and elaborates a projection function.
314316elabProjection :: ElabInfo
315317 -> Name -- ^ Name of the argument in the constructor
318+ -> [Name] -- ^ Parameter names
316319 -> Name -- ^ Projection Name
317320 -> Plicity -- ^ Projection Plicity
318321 -> PTerm -- ^ Projection Type
@@ -324,7 +327,7 @@ elabProjection :: ElabInfo
324327 -> [Name] -- ^ All Field Names
325328 -> Int -- ^ Argument Index
326329 -> Idris ()
327−elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs fnames index
330+elabProjection info cname paramnames pname plicity projTy pdoc psyn fc targetTy cn phArgs fnames index
328331 = do logElab 1 $ "Generating Projection for " ++ show pname
329332
330333 let ty = generateTy
@@ -343,7 +346,11 @@ elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs f
343346 -- | The type of the projection function.
344347 generateTy :: PDecl
345348 generateTy = PTy pdoc [] psyn fc [] pname NoFC $
346− PPi expl recName NoFC targetTy projTy
349+ bindParams paramnames $
350+ PPi expl recName NoFC targetTy projTy
351+
352+ bindParams [] t = t
353+ bindParams (n : ns) ty = PPi impl n NoFC Placeholder (bindParams ns ty)
347354
348355 -- | The left hand side of the projection function.
349356 generateLhs :: PTerm
@@ -370,6 +377,7 @@ elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs f
370377-- If 'optional' is true, we will not fail if we can't elaborate the update function.
371378elabUpdate :: ElabInfo
372379 -> Name -- ^ Name of the argument in the constructor
380+ -> [Name] -- ^ Parameter names
373381 -> Name -- ^ Field Name
374382 -> Plicity -- ^ Field Plicity
375383 -> PTerm -- ^ Field Type
@@ -382,7 +390,7 @@ elabUpdate :: ElabInfo
382390 -> Int -- ^ Argument Index
383391 -> Bool -- ^ Optional
384392 -> Idris ()
385−elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i optional
393+elabUpdate info cname paramnames pname plicity pty pdoc psyn fc sty cn args fnames i optional
386394 = do logElab 1 $ "Generating Update for " ++ show pname
387395
388396 let ty = generateTy
@@ -406,10 +414,14 @@ elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i option
406414 -- | The type of the update function.
407415 generateTy :: PDecl
408416 generateTy = PTy pdoc [] psyn fc [] set_pname NoFC $
409− PPi expl (nsroot pname) NoFC pty $
410− PPi expl recName NoFC sty (substInput sty)
417+ bindParams paramnames $
418+ PPi expl (nsroot pname) NoFC pty $
419+ PPi expl recName NoFC sty (substInput sty)
411420 where substInput = substMatches [(cname, PRef fc [] (nsroot pname))]
412421
422+ bindParams [] t = t
423+ bindParams (n : ns) ty = PPi impl n NoFC Placeholder (bindParams ns ty)
424+
413425 -- | The "_set" name.
414426 set_pname :: Name
415427 set_pname = set_name pname