808bbee · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

'impossible' fix

Only allow impossible on unification errors. (TODO: Still need to check it's the right sort of unification error)

commit808bbeef3d0621840e44c376ece46bf585c95743 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 1 Dec 2013, 20:00 (13 years ago) parent4a0eba1

1 file changed+6−1

unifiedsplit

src/Idris/ElabDecls.hs+6−1

@@ -1168,7 +1168,12 @@ checkPossible info fc tcgen fname lhs_in

11681168-- b <- inferredDiff fc (delab' i lhs_tm True) lhs

11691169-- return (not b) -- then return (Just lhs_tm) else return Nothing

11701170-- 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

11721177

11731178elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

11741179 Idris (Either Term (Term, Term))