@@ -59,10 +59,16 @@ genClauses fc n xs given
5959 let lhs_tms' = zipWith mergePlaceholders lhs_tms
6060 (map (stripUnmatchable i) (map flattenArgs given))
6161 let lhss = map pUnApply lhs_tms'
62+ nty <- case lookupTyExact n (tt_ctxt i) of
63+ Just t -> return (normalise (tt_ctxt i) [] t)
64+ _ -> fail "Can't happen - genClauses, lookupTyExact"
6265
6366 let argss = transpose lhss
64− let all_args = map (genAll i) argss
67+ let all_args = map (genAll i) (zip (genPH i nty) argss)
6568 logCoverage 5 $ "COVERAGE of " ++ show n
69+ logCoverage 5 $ "using type " ++ show nty
70+ logCoverage 5 $ "non-concrete args " ++ show (genPH i nty)
71+
6672 logCoverage 5 $ show (lhs_tms, lhss)
6773 logCoverage 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
6874 logCoverage 10 $ show argss ++ "\n" ++ show all_args
@@ -89,6 +95,18 @@ genClauses fc n xs given
8995 | (f, args) <- unApply term = map (\t -> delab' i t True True) args
9096 | otherwise = []
9197
98+ -- if an argument has a non-concrete type (i.e. it's a function
99+ -- that calculates something from a previous argument) we'll also
100+ -- need to generate a placeholder pattern for it since it could be
101+ -- anything based on earlier values
102+ genPH :: IState -> Type -> [Bool]
103+ genPH ist (Bind n (Pi _ ty _) sc) = notConcrete ist ty : genPH ist sc
104+ genPH ist ty = []
105+
106+ notConcrete ist t | (P _ n _, args) <- unApply t,
107+ not (isConName n (tt_ctxt ist)) = True
108+ notConcrete _ _ = False
109+
92110 pUnApply (PApp _ f args) = map getTm args
93111 pUnApply _ = []
94112
@@ -172,16 +190,14 @@ recoverableCoverage ctxt (Elaborating _ _ _ e) = recoverableCoverage ctxt e
172190recoverableCoverage ctxt (ElaboratingArg _ _ _ e) = recoverableCoverage ctxt e
173191recoverableCoverage _ _ = False
174192
175−-- FIXME: Just look for which one is the deepest, then generate all
176−-- possibilities up to that depth.
177−-- This and below issues for this function are tracked as Issue #1741 on the issue tracker.
178−-- https://github.com/idris-lang/Idris-dev/issues/1741
179−genAll :: IState -> [PTerm] -> [PTerm]
180−genAll i args
193+genAll :: IState -> (Bool, [PTerm]) -> [PTerm]
194+genAll i (addPH, args)
181195 = case filter (/=Placeholder) $ fnub (concatMap otherPats (fnub args)) of
182196 [] -> [Placeholder]
183− xs -> inventConsts xs
197+ xs -> ph $ inventConsts xs
184198 where
199+ ph ts = if addPH then Placeholder : ts else ts
200+
185201 -- if they're constants, invent a new one to make sure that
186202 -- constants which are not explicitly handled are covered
187203 inventConsts cs@(PConstant fc c : _) = map (PConstant NoFC) (ic' (mapMaybe getConst cs))
@@ -204,7 +220,6 @@ genAll i args
204220 ic' xs@(B64 _ : _) = firstMissing xs (lotsOfNums B64)
205221 ic' xs@(Ch _ : _) = firstMissing xs lotsOfChars
206222 ic' xs@(Str _ : _) = firstMissing xs lotsOfStrings
207− -- TODO: Bit vectors
208223 -- The rest are types with only one case
209224 ic' xs = xs
210225
@@ -219,19 +234,19 @@ genAll i args
219234 nubMap f acc (x : xs) = nubMap f (fnub' acc (f x)) xs
220235
221236 otherPats :: PTerm -> [PTerm]
222− otherPats o@(PRef fc hl n) = ops fc n [] o
223− otherPats o@(PApp _ (PRef fc hl n) xs) = ops fc n xs o
237+ otherPats o@(PRef fc hl n) = ph $ ops fc n [] o
238+ otherPats o@(PApp _ (PRef fc hl n) xs) = ph $ ops fc n xs o
224239 otherPats o@(PPair fc hls _ l r)
225− = ops fc pairCon
240+ = ph $ ops fc pairCon
226241 ([pimp (sUN "A") Placeholder True,
227242 pimp (sUN "B") Placeholder True] ++
228243 [pexp l, pexp r]) o
229244 otherPats o@(PDPair fc hls p t _ v)
230− = ops fc sigmaCon
245+ = ph $ ops fc sigmaCon
231246 ([pimp (sUN "a") Placeholder True,
232247 pimp (sUN "P") Placeholder True] ++
233248 [pexp t,pexp v]) o
234− otherPats o@(PConstant _ c) = inventConsts [o] -- return o
249+ otherPats o@(PConstant _ c) = ph $ inventConsts [o] -- return o
235250 otherPats arg = return Placeholder
236251
237252 ops fc n xs o