git.iko.soy/Idris-dev
on master help sign in
Fix missing check on case in types
cbb86b2Edwin Brady
src/Idris/Elab/Type.hs+2−1
compare with master
unifiedsplit
@@ -79,7 +79,8 @@ buildType info syn fc opts n ty' = do
79 ds <- checkAddDef True False fc iderr defer
79 ds <- checkAddDef True False fc iderr defer
80 -- if the type is not complete, note that we'll need to infer
80 -- if the type is not complete, note that we'll need to infer
81 -- things later (for solving metavariables)
81 -- things later (for solving metavariables)
82+ when (length ds > length is) -- more deferred than case blocks
82− when (not (null ds)) $ addTyInferred n
83+ $ addTyInferred n
83
84
84 mapM_ (elabCaseBlock info opts) is
85 mapM_ (elabCaseBlock info opts) is
85 ctxt <- getContext
86 ctxt <- getContext
test/effects003/hangman.idr+3−3
@@ -77,9 +77,9 @@ data HangmanRules : Effect where
77 sig HangmanRules Bool
77 sig HangmanRules Bool
78 (Hangman (Running (S g) (S w)))
78 (Hangman (Running (S g) (S w)))
79 (\inword =>
79 (\inword =>
80− case inword of
80+ Hangman (case inword of
81− True => Hangman (Running (S g) w)
81+ True => (Running (S g) w)
82− False => Hangman (Running g (S w)))
82+ False => (Running g (S w))))
83
83
84-- The 'Won' operation requires that there are no missing letters
84-- The 'Won' operation requires that there are no missing letters
85
85