@@ -230,7 +230,6 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
230230 _ -> return ()
231231 pats_in <- mapM (elabClause info (TCGen `elem` opts)) cs
232232
233−
234233 solveDeferred n
235234 let pats = mapMaybe id pats_in
236235 logLvl 3 (showSep "\n" (map (\ (l,r) ->
@@ -239,6 +238,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
239238 ist <- get
240239 let tcase = opt_typecase (idris_options ist)
241240 let pdef = map debind $ map (simpl (tt_ctxt ist)) pats
241+ tclift $ sameLength pdef
242242 cov <- coverage
243243 pcover <-
244244 if cov
@@ -288,7 +288,6 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
288288 ":warning - Unreachable case: " ++
289289 show (delab ist x)) xs
290290 tree' <- tclift $ simpleCase tcase pcover fc pdef'
291− tclift $ sameLength pdef
292291 logLvl 3 (show tree)
293292 logLvl 3 $ "Optimised: " ++ show tree'
294293 ctxt <- getContext