@@ -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