72aa6b9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Proper error when merging solutions fails

This is for the situation where different parts of a program yield a different answer for unification - it may be okay, but it creates a new unification problem, and if that fails we should have a proper error message not the placeholder that's currently there!

commit72aa6b96b6fccf4eb8a293930857ab4dfe14c743 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 15 Jan 2015, 15:32 (12 years ago) parentb068758

1 file changed+2−1

compare with master

unifiedsplit

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

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

@@ -193,7 +193,8 @@ mergeSolutions env ns = merge [] ns

193193 | Just t' <- lookup n ns

194194 = do ps <- get

195195 let probs = problems ps

196− put (ps { problems = probs ++ [(t,t',True,env,Msg "New problem",

196+ put (ps { problems = probs ++ [(t,t',True,env,

197+ CantUnify True t t' (Msg "") (errEnv env) 0,

197198 [], Unify)] })

198199 merge acc ns

199200 | otherwise = merge ((n, t): acc) ns