Skip to content
Browse files

Chase type classes for longer

  • Loading branch information...
1 parent 463e62a commit 92d99f8b7c5392f1f092d6aa9348cbe116be83bb Edwin Brady committed
Showing with 8 additions and 2 deletions.
  1. +6 −0 CHANGELOG
  2. +2 −2 src/Idris/ElabTerm.hs
View
6 CHANGELOG
@@ -1,8 +1,14 @@
New in 0.9.2:
-------------
+User visible changes:
+
* case expressions allowed in type signatures
+Internal changes:
+
+* Some type class resolution fixes
+
New in 0.9.1:
-------------
View
4 src/Idris/ElabTerm.hs
@@ -101,7 +101,7 @@ elab ist info pattern tcgen fn tm
(elab' ina (PRef fc unitTy))
elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes
- = resolveTC 2 fn ist
+ = resolveTC 5 fn ist
elab' ina (PResolveTC fc) = do c <- unique_hole (MN 0 "c")
instanceArg c
elab' ina (PRefl fc) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,
@@ -366,7 +366,7 @@ resolveTC depth fn ist
tm <- get_term
-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $
-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))
- let depth' = if scopeOnly then 2 else depth
+ let depth' = if scopeOnly then 5 else depth
blunderbuss t depth' insts)
where
elabTC n | n /= fn && tcname n = (resolve n depth, show n)

0 comments on commit 92d99f8

Please sign in to comment.
Something went wrong with that request. Please try again.