git.iko.soy/Idris-dev
on master help sign in
Add error message.
e1afa90Matus Tejiscak
src/IRTS/Compiler.hs+1−1
compare with master
unifiedsplit
@@ -525,7 +525,7 @@ isLikeNat ist cn
525 , Just (z, s) <- natLikeCtors tyN cTy
525 , Just (z, s) <- natLikeCtors tyN cTy
526 = if | cn == z -> Just LikeZ
526 = if | cn == z -> Just LikeZ
527 | cn == s -> Just LikeS
527 | cn == s -> Just LikeS
528− | otherwise -> Nothing
528+ | otherwise -> error $ "isLikeNat: constructor not found in its own family: " ++ show (cn, tyN)
529 where
529 where
530 natLikeCtors :: Name -> Type -> Maybe (Name, Name)
530 natLikeCtors :: Name -> Type -> Maybe (Name, Name)
531 natLikeCtors tyN cTy = case lookupCtxtExact tyN $ idris_datatypes ist of
531 natLikeCtors tyN cTy = case lookupCtxtExact tyN $ idris_datatypes ist of