@@ -1169,19 +1169,25 @@ checkPossible info fc tcgen fname lhs_in
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)
11711171 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))
11731174 impossibleError (CantConvert _ _ _) = False
11741175 impossibleError (At _ e) = impossibleError e
11751176 impossibleError (Elaborating _ _ e) = impossibleError e
11761177 impossibleError _ = True
11771178
1179+ sameFam topx topy
1180+ = case (unApply topx, unApply topy) of
1181+ ((P _ x _, _), (P _ y _, _)) -> x == y
1182+ _ -> False
1183+
11781184elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
11791185 Idris (Either Term (Term, Term))
11801186elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
11811187 = do let tcgen = Dictionary `elem` opts
11821188 b <- checkPossible info fc tcgen fname lhs_in
11831189 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"
11851191 False -> do ptm <- mkPatTm lhs_in
11861192 return (Left ptm)
11871193elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)