@@ -774,11 +774,16 @@ elabTransform info fc safe lhs_in rhs_in
774774
775775elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->
776776 PTerm -> DataOpts -> Docstring -> Name -> PTerm -> Idris ()
777−elabRecord info syn doc fc tyn ty opts cdoc cn cty
778− = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])
777+elabRecord info syn doc fc tyn ty opts cdoc cn cty_in
778+ = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty_in, fc, [])])
779779 -- TODO think: something more in info?
780− cty' <- implicit info syn cn cty
780+ cty' <- implicit info syn cn cty_in
781781 i <- getIState
782+
783+ -- get bound implicits and propagate to setters (in case they
784+ -- provide useful information for inference)
785+ let extraImpls = getBoundImpls cty'
786+
782787 cty <- case lookupTy cn (tt_ctxt i) of
783788 [t] -> return (delab i t)
784789 _ -> ifail "Something went inexplicably wrong"
@@ -797,14 +802,18 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty
797802 logLvl 1 $ show (recty, ptys)
798803 let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
799804 [pexp (PRef fc rec)])) ptys
805+
806+ -- Generate projection functions
800807 proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])
801808 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
802809 let implBinds = getImplB id cty'
803− update_decls <- mapM (mkUpdate recty index_names_in
810+
811+ -- Generate update functions
812+ update_decls <- mapM (mkUpdate recty index_names_in extraImpls
804813 (getFieldNames cty')
805814 implBinds (length nonImp)) (zip nonImp [0..])
806815 mapM_ (elabDecl EAll info) (concat proj_decls)
807− logLvl 1 $ show update_decls
816+ logLvl 3 $ show update_decls
808817 mapM_ (tryElabDecl info) (update_decls)
809818 where
810819-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
@@ -819,9 +828,12 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty
819828 (\v -> do iputStrLn $ show fc ++
820829 ":Warning - can't generate setter for " ++
821830 show fn ++ " (" ++ show ty ++ ")"
822−-- ++ "\n" ++ pshow i v
831+ ++ "\n" ++ pshow i v
823832 putIState i)
824833
834+ getBoundImpls (PPi (Imp _ _ _) n ty sc) = (n, ty) : getBoundImpls sc
835+ getBoundImpls _ = []
836+
825837 getImplB k (PPi (Imp l s _) n Placeholder sc)
826838 = getImplB k sc
827839 getImplB k (PPi (Imp l s p) n ty sc)
@@ -886,7 +898,7 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty
886898 -- If the 'pty' we're updating includes anything in 'substs', we're
887899 -- updating the type as well, so use recty', otherwise just use
888900 -- recty
889− mkUpdate recty inames fnames k num ((pn, pty), pos)
901+ mkUpdate recty inames extras fnames k num ((pn, pty), pos)
890902 = do let setname = expandNS syn $ mkType pn
891903 let valname = sMN 0 "updateval"
892904 let pn_out = sMN 0 (show pn ++ "_out")
@@ -894,8 +906,8 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty
894906 let recty_in = substMatches [(pn, PRef fc pn_in)] recty
895907 let recty_out = substMatches [(pn, PRef fc pn_out)] recty
896908 let pt = substMatches inames $
897− k (PPi expl pn_out pty
898− (PPi expl rec recty_in recty_out))
909+ k (implBindUp extras inames (PPi expl pn_out pty
910+ (PPi expl rec recty_in recty_out)))
899911 let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt
900912-- let pls = map (\x -> PRef fc (sMN x ("field" ++ show x))) [0..num-1]
901913 let inames_imp = map (\ (x,_) -> (x, Placeholder)) inames
@@ -913,6 +925,15 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty
913925 (map pexp rhsArgs)) []
914926 return (pn, pfnTy, PClauses fc [] setname [pclause])
915927
928+ implBindUp [] is t = t
929+ implBindUp ((n, ty):ns) is t
930+ = let n' = case lookup n is of
931+ Just (PRef _ x) -> x
932+ _ -> n in
933+ if n `elem` allNamesIn t
934+ then PPi impl n' ty (implBindUp ns is t)
935+ else implBindUp ns is t
936+
916937-- FIXME: 'forcenames' is an almighty hack! Need a better way of
917938-- erasing non-forceable things
918939-- ^^^