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

git.iko.soy/Idris-dev

Fix another INTERNAL ERROR

For rewriting equalities when they aren't equalities. Fixes #695

commit0700c587b92114c67d51090ab759fe6df2861cf1 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 23 Dec 2013, 13:43 (13 years ago) parent5c8acd2

3 files changed+7−1

unifiedsplit

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

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

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

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

576576 return scv

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

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

578578 where rname = MN 0 "replaced"

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

580580

src/Idris/Core/TT.hs+1

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

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

8686 | CantInferType String

8787 | NonFunctionType Term Term

88+ | NotEquality Term Term

8889 | TooManyArguments Name

8990 | CantIntroduce Term

9091 | NoSuchVariable Name

src/Idris/Delaborate.hs+5

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

154154 let colour = idris_colourRepl i in

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

156156 ++ 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) ++ ")"

157162pshow i (TooManyArguments f)

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

159164pshow i (CantIntroduce ty)