@@ -626,25 +626,26 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)
626626 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')
627627 let cwvaltyN = explicitNames cwvalty
628628 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)
630630 let pvars = map fst (getPBtys cwvalty)
631631 -- we need the unelaborated term to get the names it depends on
632632 -- rather than a de Bruijn index.
633633 let pdeps = usedNamesIn pvars i (delab i cwvalty)
634634 let (bargs_pre, bargs_post) = split pdeps bargs []
635− logLvl 1 ("With type " ++ show (getRetTy cwvaltyN) ++
635+ logLvl 10 ("With type " ++ show (getRetTy cwvaltyN) ++
636636 " 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)
638638 windex <- getName
639639 -- build a type declaration for the new function:
640640 -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty
641641 let wargval = getRetTy cwvalN
642642 let wargtype = getRetTy cwvaltyN
643− logLvl 1 ("Abstract over " ++ show wargval)
643+ logLvl 5 ("Abstract over " ++ show wargval)
644644 let wtype = bindTyArgs Pi (bargs_pre ++
645645 (MN 0 "warg", wargtype) :
646− map (abstract (MN 0 "warg") wargval) bargs_post) ret_ty
647− logLvl 1 ("New function type " ++ show wtype)
646+ map (abstract (MN 0 "warg") wargval wargtype) bargs_post)
647+ (substTerm wargval (P Bound (MN 0 "warg") wargtype) ret_ty)
648+ logLvl 3 ("New function type " ++ show wtype)
648649 let wname = MN windex (show fname)
649650 let imps = getImps wtype -- add to implicits context
650651 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)
657658 -- ==> fname' ps wpat [rest], match pats against toplevel for ps
658659 wb <- mapM (mkAuxC wname lhs (map fst bargs_pre) (map fst bargs_post))
659660 withblock
660− logLvl 1 ("with block " ++ show wb)
661+ logLvl 3 ("with block " ++ show wb)
661662 mapM_ (elabDecl EAll info) wb
662663
663664 -- rhs becomes: fname' ps wval
@@ -736,7 +737,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)
736737 | otherwise = split deps rest ((n, ty) : pre)
737738 split deps [] pre = (reverse pre, [])
738739
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)
740741
741742data MArgTy = IA | EA | CA deriving Show
742743