@@ -50,7 +50,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
5050 ttConsTy <-
5151 case lookupTyExact dconName (tt_ctxt i) of
5252 Just as -> return as
53− Nothing -> tclift $ tfail $ At fc (Elaborating "record" tyn (InternalMsg "It seems like the constructor for this record has disappeared. :( \n This is a bug. Please report."))
53+ Nothing -> tclift $ tfail $ At fc (Elaborating "record " tyn (InternalMsg "It seems like the constructor for this record has disappeared. :( \n This is a bug. Please report."))
5454
5555 -- The arguments to the constructor
5656 let constructorArgs = getArgTys ttConsTy
@@ -69,6 +69,10 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
6969 -- Build and elaborate projection functions
7070 elabProj dconName projectors
7171
72+ logLvl 1 $ "Dependencies: " ++ show fieldDependencies
73+
74+ logLvl 1 $ "Depended on: " ++ show dependedOn
75+
7276 -- All things we need to elaborate update functions for, together with a number denoting their position in the constructor.
7377 let updaters = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (paramsForElab ++ userFieldsForElab) [0..]]
7478 -- Build and elaborate update functions
@@ -170,14 +174,6 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
170174 elabProjection info n n' p t' doc rsyn fc target cn phArgs fieldNames i
171175 in mapM_ elab fs
172176
173− projectInType :: [(Name, Name)] -> PTerm -> PTerm
174− projectInType xs = mapPT st
175− where
176− st :: PTerm -> PTerm
177− st (PRef fc n)
178− | Just pn <- lookup n xs = PApp fc (PRef fc pn) [pexp recRef]
179− st t = t
180−
181177 -- | Elaborate the update functions.
182178 elabUp :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()
183179 elabUp cn fs = let args = map (uncurry asPRefArg) [(p, n) | (n, _, p, _, _, _) <- fs]
@@ -186,14 +182,14 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
186182
187183 -- | Decides whether a setter should be generated for a field or not.
188184 optionalSetter :: Name -> Bool
189− optionalSetter n = n `notElem` dependentFields && n `notElem` dependedOn
185+ optionalSetter n = n `elem` dependedOn
190186
191187 -- | A map from a field name to the other fields it depends on.
192188 fieldDependencies :: [(Name, [Name])]
193189 fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, t) <- fields ++ params]
194190 where
195191 fieldDep :: Name -> PTerm -> (Name, [Name])
196− fieldDep n t = ((nsroot n), fieldNames `intersect` allNamesIn t)
192+ fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)
197193
198194 -- | A list of fields depending on another field.
199195 dependentFields :: [Name]
@@ -223,7 +219,7 @@ elabProjection :: ElabInfo ->
223219 [Name] -> -- ^ All Field Names
224220 Int -> -- ^ Argument Index
225221 Idris ()
226−elabProjection info cname pname plicity pty pdoc psyn fc tty cn phArgs fnames index
222+elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs fnames index
227223 = do logLvl 1 $ "Generating Projection for " ++ show pname
228224
229225 let ty = generateTy
@@ -241,13 +237,7 @@ elabProjection info cname pname plicity pty pdoc psyn fc tty cn phArgs fnames in
241237 where
242238 -- | The type of the projection function.
243239 generateTy :: PDecl
244− generateTy = PTy pdoc [] psyn fc [] pname $ PPi expl recName tty (mapPT applyProjs pty)
245−
246− -- | Applies all fields to "rec".
247− applyProjs :: PTerm -> PTerm
248− applyProjs t@(PRef fc name)
249− | (nsroot name) `elem` fnames = PApp fc t [pexp recRef]
250− applyProjs t = t
240+ generateTy = PTy pdoc [] psyn fc [] pname $ PPi expl recName targetTy projTy
251241
252242 -- | The left hand side of the projection function.
253243 generateLhs :: PTerm
@@ -303,9 +293,10 @@ elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i option
303293
304294 idrisCatch (do rec_elabDecl info EAll info ty
305295 rec_elabDecl info EAll info $ PClauses fc [] set_pname [clause])
306− (\err -> if optional
296+ (\err -> logLvl 1 $ "Could not generate update function for " ++ show pname)
297+ {-if optional
307298 then logLvl 1 $ "Could not generate update function for " ++ show pname
308− else tclift $ tfail $ At fc (Elaborating "record update function" pname err))
299+ else tclift $ tfail $ At fc (Elaborating "record update function " pname err)) -}
309300 where
310301 -- | The type of the udpate function.
311302 generateTy :: PDecl
@@ -364,3 +355,11 @@ recName :: Name
364355recName = sMN 0 "rec"
365356
366357recRef = PRef emptyFC recName
358+
359+projectInType :: [(Name, Name)] -> PTerm -> PTerm
360+projectInType xs = mapPT st
361+ where
362+ st :: PTerm -> PTerm
363+ st (PRef fc n)
364+ | Just pn <- lookup n xs = PApp fc (PRef fc pn) [pexp recRef]
365+ st t = t