Implicit fix
If we normalise the goal type before coercion, we also need to check
against the normalised coercion type otherwise we might miss some valid
coercions. Fixes #2570
commit2f9d287d07a0d17d0a4e01cb8ebce40a57931954
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSun 6 Sep 2015, 13:52 (11 years ago)
parentfcba396
src/Idris/AbsSyntax.hs+1−1
@@ -200,7 +200,7 @@ getCoercionsTo i ty =
200200 where findCoercions t [] = []
201201 findCoercions t (n : ns) =
202202 let ps = case lookupTy n (tt_ctxt i) of
203− [ty'] -> case unApply (getRetTy ty') of
203+ [ty'] -> case unApply (getRetTy (normalise (tt_ctxt i) [] ty')) of
204204 (t', _) ->
205205 if t == t' then [n] else []
206206 _ -> [] in