git.iko.soy/Idris-dev
on master help sign in
Chase type classes for longer
92d99f8Edwin Brady
CHANGELOG+6
compare with master
unifiedsplit
@@ -1,8 +1,14 @@
1New in 0.9.2:
1New in 0.9.2:
2-------------
2-------------
3
3
4+User visible changes:
5+
4* case expressions allowed in type signatures
6* case expressions allowed in type signatures
5
7
8+Internal changes:
9+
10+* Some type class resolution fixes
11+
6New in 0.9.1:
12New in 0.9.1:
7-------------
13-------------
8
14
src/Idris/ElabTerm.hs+2−2
@@ -101,7 +101,7 @@ elab ist info pattern tcgen fn tm
101 (elab' ina (PRef fc unitTy))
101 (elab' ina (PRef fc unitTy))
102 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
102 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
103 elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes
103 elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes
104− = resolveTC 2 fn ist
104+ = resolveTC 5 fn ist
105 elab' ina (PResolveTC fc) = do c <- unique_hole (MN 0 "c")
105 elab' ina (PResolveTC fc) = do c <- unique_hole (MN 0 "c")
106 instanceArg c
106 instanceArg c
107 elab' ina (PRefl fc) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,
107 elab' ina (PRefl fc) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,
@@ -366,7 +366,7 @@ resolveTC depth fn ist
366 tm <- get_term
366 tm <- get_term
367-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $
367-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $
368-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))
368-- (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
370 blunderbuss t depth' insts)
370 blunderbuss t depth' insts)
371 where
371 where
372 elabTC n | n /= fn && tcname n = (resolve n depth, show n)
372 elabTC n | n /= fn && tcname n = (resolve n depth, show n)