@@ -491,6 +491,8 @@ propagateParams i ps t tm@(PApp _ (PRef fc hls n) args)
491 = t { getTm = PRef NoFC [] n } : addP sc ts
491 = t { getTm = PRef NoFC [] n } : addP sc ts
492 addP (Bind n _ sc) (t : ts) = t : addP sc ts
492 addP (Bind n _ sc) (t : ts) = t : addP sc ts
493 addP _ ts = ts
493 addP _ ts = ts
494+propagateParams i ps t tm@(PApp fc ap args)
495+ = PApp fc (propagateParams i ps t ap) args
494propagateParams i ps t (PRef fc hls n)
496propagateParams i ps t (PRef fc hls n)
495 = case lookupCtxt n (idris_implicits i) of
497 = case lookupCtxt n (idris_implicits i) of
496 [is] -> let ps' = filter (isImplicit is) ps in
498 [is] -> let ps' = filter (isImplicit is) ps in
@@ -548,9 +550,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
548 let tcparams = getTCParamsInType i [] fn_is norm_ty
550 let tcparams = getTCParamsInType i [] fn_is norm_ty
550 let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $
552 let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $
551− propagateParams i params fn_ty (addImplPat i lhs_in)
553+ propagateParams i params norm_ty (addImplPat i lhs_in)
552-- let lhs = mkLHSapp $
554-- let lhs = mkLHSapp $
553-- propagateParams i params fn_ty (addImplPat i lhs_in)
555-- propagateParams i params fn_ty (addImplPat i lhs_in)
556+ logLvl 10 (show (params, fn_ty) ++ " " ++ showTmImpls (addImplPat i lhs_in))
554 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)
557 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)
555 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++
558 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++
556 "\n" ++ show (fn_ty, fn_is))
559 "\n" ++ show (fn_ty, fn_is))