@@ -101,7 +101,7 @@ elab ist info pattern tcgen fn tm
101101 (elab' ina (PRef fc unitTy))
102102 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
103103 elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes
104− = resolveTC 2 fn ist
104+ = resolveTC 5 fn ist
105105 elab' ina (PResolveTC fc) = do c <- unique_hole (MN 0 "c")
106106 instanceArg c
107107 elab' ina (PRefl fc) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,
@@ -366,7 +366,7 @@ resolveTC depth fn ist
366366 tm <- get_term
367367-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $
368368-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))
369− let depth' = if scopeOnly then 2 else depth
369+ let depth' = if scopeOnly then 5 else depth
370370 blunderbuss t depth' insts)
371371 where
372372 elabTC n | n /= fn && tcname n = (resolve n depth, show n)