@@ -491,6 +491,8 @@ propagateParams i ps t tm@(PApp _ (PRef fc hls n) args)
491491 = t { getTm = PRef NoFC [] n } : addP sc ts
492492 addP (Bind n _ sc) (t : ts) = t : addP sc ts
493493 addP _ ts = ts
494+propagateParams i ps t tm@(PApp fc ap args)
495+ = PApp fc (propagateParams i ps t ap) args
494496propagateParams i ps t (PRef fc hls n)
495497 = case lookupCtxt n (idris_implicits i) of
496498 [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
548550 let tcparams = getTCParamsInType i [] fn_is norm_ty
549551
550552 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)
552554-- let lhs = mkLHSapp $
553555-- propagateParams i params fn_ty (addImplPat i lhs_in)
556+ logLvl 10 (show (params, fn_ty) ++ " " ++ showTmImpls (addImplPat i lhs_in))
554557 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)
555558 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++
556559 "\n" ++ show (fn_ty, fn_is))