@@ -230,7 +230,6 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
230 _ -> return ()
230 _ -> return ()
231 pats_in <- mapM (elabClause info (TCGen `elem` opts)) cs
231 pats_in <- mapM (elabClause info (TCGen `elem` opts)) cs
234 solveDeferred n
233 solveDeferred n
235 let pats = mapMaybe id pats_in
234 let pats = mapMaybe id pats_in
236 logLvl 3 (showSep "\n" (map (\ (l,r) ->
235 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
239 ist <- get
238 ist <- get
240 let tcase = opt_typecase (idris_options ist)
239 let tcase = opt_typecase (idris_options ist)
241 let pdef = map debind $ map (simpl (tt_ctxt ist)) pats
240 let pdef = map debind $ map (simpl (tt_ctxt ist)) pats
241+ tclift $ sameLength pdef
242 cov <- coverage
242 cov <- coverage
243 pcover <-
243 pcover <-
@@ -288,7 +288,6 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
288 ":warning - Unreachable case: " ++
288 ":warning - Unreachable case: " ++
289 show (delab ist x)) xs
289 show (delab ist x)) xs
290 tree' <- tclift $ simpleCase tcase pcover fc pdef'
290 tree' <- tclift $ simpleCase tcase pcover fc pdef'
291− tclift $ sameLength pdef
292 logLvl 3 (show tree)
291 logLvl 3 (show tree)
293 logLvl 3 $ "Optimised: " ++ show tree'
292 logLvl 3 $ "Optimised: " ++ show tree'
294 ctxt <- getContext
293 ctxt <- getContext