@@ -1169,19 +1169,25 @@ checkPossible info fc tcgen fname lhs_in
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 Error err -> return (impossibleError err)
1171 Error err -> return (impossibleError err)
1172− where impossibleError (CantUnify _ _ _ _ _ _) = False
1172+ where impossibleError (CantUnify _ topx topy e _ _)
1173+ = not (sameFam topx topy || not (impossibleError e))
1173 impossibleError (CantConvert _ _ _) = False
1174 impossibleError (CantConvert _ _ _) = False
1174 impossibleError (At _ e) = impossibleError e
1175 impossibleError (At _ e) = impossibleError e
1175 impossibleError (Elaborating _ _ e) = impossibleError e
1176 impossibleError (Elaborating _ _ e) = impossibleError e
1176 impossibleError _ = True
1177 impossibleError _ = True
1180+ = case (unApply topx, unApply topy) of
1181+ ((P _ x _, _), (P _ y _, _)) -> x == y
1178elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
1184elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
1179 Idris (Either Term (Term, Term))
1185 Idris (Either Term (Term, Term))
1180elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
1186elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
1181 = do let tcgen = Dictionary `elem` opts
1187 = do let tcgen = Dictionary `elem` opts
1182 b <- checkPossible info fc tcgen fname lhs_in
1188 b <- checkPossible info fc tcgen fname lhs_in
1183 case b of
1189 case b of
1184− True -> ifail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"
1190+ True -> ifail $ show fc ++ ":" ++ show lhs_in ++ " is a valid case"
1185 False -> do ptm <- mkPatTm lhs_in
1191 False -> do ptm <- mkPatTm lhs_in
1186 return (Left ptm)
1192 return (Left ptm)
1187elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
1193elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)