@@ -88,7 +88,7 @@ elabRecord :: ElabInfo -> SyntaxInfo -> FC -> Name ->
8888 PTerm -> Name -> PTerm -> Idris ()
8989elabRecord info syn fc tyn ty cn cty
9090 = do elabData info syn fc (PDatadecl tyn ty [(cn, cty, fc)])
91− cty <- implicit syn cn cty
91+ cty' <- implicit syn cn cty
9292 i <- get
9393 cty <- case lookupTy Nothing cn (tt_ctxt i) of
9494 [t] -> return (delab i t)
@@ -103,7 +103,8 @@ elabRecord info syn fc tyn ty cn cty
103103 [pexp (PRef fc rec)])) ptys
104104 proj_decls <- mapM (mkProj recty substs cimp) (zip ptys [0..])
105105 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
106− update_decls <- mapM (mkUpdate recty (length nonImp)) (zip nonImp [0..])
106+ let implBinds = getImplB id cty'
107+ update_decls <- mapM (mkUpdate recty implBinds (length nonImp)) (zip nonImp [0..])
107108 mapM_ (elabDecl info) (concat (proj_decls ++ update_decls))
108109 where
109110-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
@@ -111,6 +112,12 @@ elabRecord info syn fc tyn ty cn cty
111112 isNonImp (PExp _ _ _, a) = Just a
112113 isNonImp _ = Nothing
113114
115+ getImplB k (PPi (Imp l s) n ty sc)
116+ = getImplB (\x -> k (PPi (Imp l s) n ty x)) sc
117+ getImplB k (PPi _ n ty sc)
118+ = getImplB k sc
119+ getImplB k _ = k
120+
114121 renameBs (PImp _ _ _ _ : ps) (PPi p n ty s)
115122 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))
116123 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)
@@ -140,7 +147,7 @@ elabRecord info syn fc tyn ty cn cty
140147 = do let pn = expandNS syn pn_in
141148 let pfnTy = PTy defaultSyntax fc [] pn
142149 (PPi expl rec recty
143− (substMatches substs pty))
150+ (substMatches substs pty))
144151 let pls = repeat Placeholder
145152 let before = pos
146153 let after = length substs - (pos + 1)
@@ -154,12 +161,12 @@ elabRecord info syn fc tyn ty cn cty
154161
155162 implicitise (pa, t) = pa { getTm = t }
156163
157− mkUpdate recty num ((pn, pty), pos)
164+ mkUpdate recty k num ((pn, pty), pos)
158165 = do let setname = expandNS syn $ mkSet pn
159166 let valname = MN 0 "updateval"
160− let pfnTy = PTy defaultSyntax fc [] setname
161− (PPi expl pn pty
162− (PPi expl rec recty recty))
167+ let pt = k (PPi expl pn pty
168+ (PPi expl rec recty recty))
169+ let pfnTy = PTy defaultSyntax fc [] setname pt
163170 let pls = map (\x -> PRef fc (MN x "field")) [0..num-1]
164171 let lhsArgs = pls
165172 let rhsArgs = take pos pls ++ (PRef fc valname) :