on master help sign in
'impossible' fix
808bbeeEdwin Brady
src/Idris/ElabDecls.hs+6−1
@@ -1168,7 +1168,12 @@ checkPossible info fc tcgen fname lhs_in
1168-- b <- inferredDiff fc (delab' i lhs_tm True) lhs
1168-- b <- inferredDiff fc (delab' i lhs_tm True) lhs
1169-- return (not b) -- then return (Just lhs_tm) else return Nothing
1169-- return (not b) -- then return (Just lhs_tm) else return Nothing
1170-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)
1170-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)
1171− err@(Error _) -> return False
1171+ Error err -> return (impossibleError err)
1172+ where impossibleError (CantUnify _ _ _ _ _ _) = False
1173+ impossibleError (CantConvert _ _ _) = False
1174+ impossibleError (At _ e) = impossibleError e
1175+ impossibleError (Elaborating _ _ e) = impossibleError e
1176+ impossibleError _ = True
1172
1177
1173elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
1178elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
1174 Idris (Either Term (Term, Term))
1179 Idris (Either Term (Term, Term))