@@ -1472,8 +1472,8 @@ paramNames args env (p : ps)
14721472 _ -> paramNames args env ps
14731473 | otherwise = paramNames args env ps
14741474
1475−propagateParams :: [Name] -> Type -> PTerm -> PTerm
1476−propagateParams ps t tm@(PApp _ (PRef fc n) args)
1475+propagateParams :: IState -> [Name] -> Type -> PTerm -> PTerm
1476+propagateParams i ps t tm@(PApp _ (PRef fc n) args)
14771477 = PApp fc (PRef fc n) (addP t args)
14781478 where addP (Bind n _ sc) (t : ts)
14791479 | Placeholder <- getTm t,
@@ -1482,9 +1482,15 @@ propagateParams ps t tm@(PApp _ (PRef fc n) args)
14821482 = t { getTm = PRef fc n } : addP sc ts
14831483 addP (Bind n _ sc) (t : ts) = t : addP sc ts
14841484 addP _ ts = ts
1485−propagateParams ps t (PRef fc n)
1486− = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)
1487−propagateParams ps t x = x
1485+propagateParams i ps t (PRef fc n)
1486+ = case lookupCtxt n (idris_implicits i) of
1487+ [is] -> let ps' = filter (isImplicit is) ps in
1488+ PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps')
1489+ _ -> PRef fc n
1490+ where isImplicit [] n = False
1491+ isImplicit (PImp _ _ _ x _ : is) n | x == n = True
1492+ isImplicit (_ : is) n = isImplicit is n
1493+propagateParams i ps t x = x
14881494
14891495-- Return the elaborated LHS/RHS, and the original LHS with implicits added
14901496elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
@@ -1516,7 +1522,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
15161522 _ -> []
15171523 let params = getParamsInType i [] fn_is fn_ty
15181524 let lhs = mkLHSapp $ stripUnmatchable i $
1519− propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))
1525+ propagateParams i params fn_ty (addImplPat i (stripLinear i lhs_in))
15201526 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)
15211527 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++
15221528 "\n" ++ show (fn_ty, fn_is))
@@ -1711,7 +1717,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
17111717 [t] -> t
17121718 _ -> []
17131719 let params = getParamsInType i [] fn_is fn_ty
1714− let lhs = propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))
1720+ let lhs = propagateParams i params fn_ty (addImplPat i (stripLinear i lhs_in))
17151721 logLvl 2 ("LHS: " ++ show lhs)
17161722 ((lhs', dlhs, []), _) <-
17171723 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []