@@ -626,25 +626,26 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)
626 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')
626 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')
627 let cwvaltyN = explicitNames cwvalty
627 let cwvaltyN = explicitNames cwvalty
628 let cwvalN = explicitNames cwval
628 let cwvalN = explicitNames cwval
629− logLvl 1 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)
629+ logLvl 5 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)
630 let pvars = map fst (getPBtys cwvalty)
630 let pvars = map fst (getPBtys cwvalty)
631 -- we need the unelaborated term to get the names it depends on
631 -- we need the unelaborated term to get the names it depends on
632 -- rather than a de Bruijn index.
632 -- rather than a de Bruijn index.
633 let pdeps = usedNamesIn pvars i (delab i cwvalty)
633 let pdeps = usedNamesIn pvars i (delab i cwvalty)
634 let (bargs_pre, bargs_post) = split pdeps bargs []
634 let (bargs_pre, bargs_post) = split pdeps bargs []
635− logLvl 1 ("With type " ++ show (getRetTy cwvaltyN) ++
635+ logLvl 10 ("With type " ++ show (getRetTy cwvaltyN) ++
636 " depends on " ++ show pdeps ++ " from " ++ show pvars)
636 " depends on " ++ show pdeps ++ " from " ++ show pvars)
637− logLvl 1 ("Pre " ++ show bargs_pre ++ "\nPost " ++ show bargs_post)
637+ logLvl 10 ("Pre " ++ show bargs_pre ++ "\nPost " ++ show bargs_post)
638 windex <- getName
638 windex <- getName
639 -- build a type declaration for the new function:
639 -- build a type declaration for the new function:
640 -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty
640 -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty
641 let wargval = getRetTy cwvalN
641 let wargval = getRetTy cwvalN
642 let wargtype = getRetTy cwvaltyN
642 let wargtype = getRetTy cwvaltyN
643− logLvl 1 ("Abstract over " ++ show wargval)
643+ logLvl 5 ("Abstract over " ++ show wargval)
644 let wtype = bindTyArgs Pi (bargs_pre ++
644 let wtype = bindTyArgs Pi (bargs_pre ++
645 (MN 0 "warg", wargtype) :
645 (MN 0 "warg", wargtype) :
646− map (abstract (MN 0 "warg") wargval) bargs_post) ret_ty
646+ map (abstract (MN 0 "warg") wargval wargtype) bargs_post)
647+ (substTerm wargval (P Bound (MN 0 "warg") wargtype) ret_ty)
647− logLvl 1 ("New function type " ++ show wtype)
648+ logLvl 3 ("New function type " ++ show wtype)
648 let wname = MN windex (show fname)
649 let wname = MN windex (show fname)
649 let imps = getImps wtype -- add to implicits context
650 let imps = getImps wtype -- add to implicits context
650 put (i { idris_implicits = addDef wname imps (idris_implicits i) })
651 put (i { idris_implicits = addDef wname imps (idris_implicits i) })
@@ -657,7 +658,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)
657 -- ==> fname' ps wpat [rest], match pats against toplevel for ps
658 -- ==> fname' ps wpat [rest], match pats against toplevel for ps
658 wb <- mapM (mkAuxC wname lhs (map fst bargs_pre) (map fst bargs_post))
659 wb <- mapM (mkAuxC wname lhs (map fst bargs_pre) (map fst bargs_post))
659 withblock
660 withblock
660− logLvl 1 ("with block " ++ show wb)
661+ logLvl 3 ("with block " ++ show wb)
661 mapM_ (elabDecl EAll info) wb
662 mapM_ (elabDecl EAll info) wb
663 -- rhs becomes: fname' ps wval
664 -- rhs becomes: fname' ps wval
@@ -736,7 +737,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)
736 | otherwise = split deps rest ((n, ty) : pre)
737 | otherwise = split deps rest ((n, ty) : pre)
737 split deps [] pre = (reverse pre, [])
738 split deps [] pre = (reverse pre, [])
739− abstract wn wty (n, argty) = (n, substTerm wty (P Bound wn wty) argty)
740+ abstract wn wv wty (n, argty) = (n, substTerm wv (P Bound wn wty) argty)
741data MArgTy = IA | EA | CA deriving Show
742data MArgTy = IA | EA | CA deriving Show