@@ -191,7 +191,7 @@ elabClauses info' fc opts n_in cs =
191191 -- Filter out the ones which match one of the
192192 -- given cases (including impossible ones)
193193 let clhs = map getLHS pdef_cov
194− logElab 2 $ "Must be unreachable:\n" ++
194+ logElab 2 $ "Must be unreachable (" ++ show (length missing') ++ "):\n" ++
195195 showSep "\n" (map showTmImpls missing') ++
196196 "\nAgainst: " ++
197197 showSep "\n" (map (\t -> showTmImpls (delab ist t)) (map getLHS pdef))
@@ -566,6 +566,7 @@ checkPossible info fc tcgen fname lhs_in
566566 = do ctxt <- getContext
567567 i <- getIState
568568 let lhs = addImplPat i lhs_in
569+ logLvl 10 $ "Trying missing case: " ++ show lhs
569570 -- if the LHS type checks, it is possible
570571 case elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState
571572 (erun fc (buildTC i info ELHS [] fname
@@ -801,10 +802,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
801802 unfold ctxt [] (map (\n -> (n, 1)) ns) rhsElab
802803 _ -> rhsElab
803804
804− when (not (null (getUnfolds opts))) $
805− logElab 1 $ "----- " ++ show (getUnfolds opts) ++
806− "\nUnfolded " ++ show rhsElab ++ "\n" ++
807− "to " ++ show rhs'
805+ logElab 5 $ "----- " ++ show (getUnfolds opts) ++
806+ "\nUnfolded " ++ show rhsElab ++ "\n" ++
807+ "to " ++ show rhs'
808808
809809 when (not (null defer)) $ logElab 1 $ "DEFERRED " ++
810810 show (map (\ (n, (_,_,t,_)) -> (n, t)) defer)
@@ -1004,11 +1004,9 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
10041004 _ -> wvalElab
10051005
10061006 logElab 5 ("Checked wval " ++ show wval')
1007−
1008− when (not (null (getUnfolds opts))) $
1009− logElab 1 $ "----- " ++ show (getUnfolds opts) ++
1010− "\nUnfolded wval " ++ show wvalElab ++ "\n" ++
1011− "to " ++ show wval'
1007+ logElab 5 $ "----- " ++ show (getUnfolds opts) ++
1008+ "\nUnfolded wval " ++ show wvalElab ++ "\n" ++
1009+ "to " ++ show wval'
10121010
10131011
10141012 ctxt <- getContext
@@ -1128,10 +1126,9 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
11281126 unfold ctxt [] (map (\n -> (n, 1)) ns) rhsElab
11291127 _ -> rhsElab
11301128
1131− when (not (null (getUnfolds opts))) $
1132− logElab 3 $ "----- " ++ show (getUnfolds opts) ++
1133− "\nUnfolded with RHS " ++ show rhsElab ++ "\n" ++
1134− "to " ++ show rhs'
1129+ logElab 5 $ "----- " ++ show (getUnfolds opts) ++
1130+ "\nUnfolded with RHS " ++ show rhsElab ++ "\n" ++
1131+ "to " ++ show rhs'
11351132
11361133
11371134 def' <- checkDef info fc iderr True defer