Fix missing check on case in types
It's only a type to be inferred if there are metavariables left over.
Even then, the solved type needs to be rechecked.
Also fix the Hangman test which shouldn't have compiled.
Fixes #2196
commitcbb86b2de12f23e6948ad6c3fb38ee38ec782c93
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSat 9 May 2015, 15:26 (11 years ago)
parent0791659
src/Idris/Elab/Type.hs+2−1
@@ -79,7 +79,8 @@ buildType info syn fc opts n ty' = do
7979 ds <- checkAddDef True False fc iderr defer
8080 -- if the type is not complete, note that we'll need to infer
8181 -- things later (for solving metavariables)
82− when (not (null ds)) $ addTyInferred n
82+ when (length ds > length is) -- more deferred than case blocks
83+ $ addTyInferred n
8384
8485 mapM_ (elabCaseBlock info opts) is
8586 ctxt <- getContext
test/effects003/hangman.idr+3−3
@@ -77,9 +77,9 @@ data HangmanRules : Effect where
7777 sig HangmanRules Bool
7878 (Hangman (Running (S g) (S w)))
7979 (\inword =>
80− case inword of
81− True => Hangman (Running (S g) w)
82− False => Hangman (Running g (S w)))
80+ Hangman (case inword of
81+ True => (Running (S g) w)
82+ False => (Running g (S w))))
8383
8484-- The 'Won' operation requires that there are no missing letters
8585