0700c58 · Idris-dev · git.iko.soy

src/Idris/Core/ProofState.hs+1−1

@@ -574,7 +574,7 @@ rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =

574 [lt, l, r, p, tmv, xp]))

575 (scv, sct) <- lift $ check ctxt env sc

576 return scv

577− _ -> fail "Not an equality type"

577+ _ -> lift $ tfail (NotEquality tmv tmt')

578 where rname = MN 0 "replaced"

579rewrite _ _ _ _ = fail "Can't rewrite here"

580

src/Idris/Core/TT.hs+1

@@ -85,6 +85,7 @@ data Err = Msg String

85 | UnifyScope Name Name Term [(Name, Type)]

86 | CantInferType String

87 | NonFunctionType Term Term

88+ | NotEquality Term Term

88 | TooManyArguments Name

89 | TooManyArguments Name

89 | CantIntroduce Term

90 | CantIntroduce Term

90 | NoSuchVariable Name

91 | NoSuchVariable Name

src/Idris/Delaborate.hs+5

@@ -154,6 +154,11 @@ pshow i (NonFunctionType f ty)

154 let colour = idris_colourRepl i in

155 showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("

156 ++ showImp (Just i) imps colour (delab i ty) ++ ")"

157+pshow i (NotEquality tm ty)

158+ = let imps = opt_showimp (idris_options i) in

159+ let colour = idris_colourRepl i in

160+ showImp (Just i) imps colour (delab i tm) ++ " does not have an equality type ("

161+ ++ showImp (Just i) imps colour (delab i ty) ++ ")"

157pshow i (TooManyArguments f)

162pshow i (TooManyArguments f)

158 = "Too many arguments for " ++ show f

163 = "Too many arguments for " ++ show f

159pshow i (CantIntroduce ty)

164pshow i (CantIntroduce ty)