Solve more implicits before 'case' elaboration
Otherwise we can generate a type for the 'case' block which is not
specific enough, if there are lots of dependencies. Fixes #1620.
commit2878ff3ff651196f2d62549fbccea0f1e39cd03c
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSun 12 Oct 2014, 12:59 (12 years ago)
parentb65d2c4
src/Idris/ElabTerm.hs+4
@@ -696,6 +696,10 @@ elab ist info emode opts fn tm
696696 letbind scvn (Var tyn) (Var valn)
697697 focus valn
698698 elabE (True, a, inty, qq) scr
699+ -- Solve any remaining implicits - we need to solve as many
700+ -- as possible before making the 'case' type
701+ unifyProblems
702+ matchProblems True
699703 args <- get_env
700704 envU <- mapM (getKind args) args
701705 let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts