@@ -9,6 +9,7 @@ import Core.Evaluate
99import Control.Monad
1010import Control.Monad.State
1111import Data.List
12+import Debug.Trace
1213
1314-- Data to pass to recursively called elaborators; e.g. for where blocks,
1415-- paramaterised declarations, etc.
@@ -67,8 +68,8 @@ elab ist info pattern tm
6768 elab' (PTrue fc) = try (elab' (PRef fc unitCon))
6869 (elab' (PRef fc unitTy))
6970 elab' (PFalse fc) = elab' (PRef fc falseTy)
70− elab' (PResolveTC (FC "HACK" _))
71− = resolveTC 10 ist
71+ elab' (PResolveTC (FC "HACK" _)) -- for chasing parent classes
72+ = resolveTC 2 ist
7273 elab' (PResolveTC fc) = do c <- unique_hole (MN 0 "c")
7374 instanceArg c
7475 elab' (PRefl fc) = elab' (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,
@@ -97,8 +98,9 @@ elab ist info pattern tm
9798 [pimp (MN 0 "a") t,
9899 pimp (MN 0 "P") Placeholder,
99100 pexp l, pexp r])
100− elab' (PAlternative as) = tryAll (zip (map elab' as) (map show as))
101−
101+ elab' (PAlternative as) = tryAll (zip (map elab' as) (map showHd as))
102+ where showHd (PApp _ h _) = show h
103+ showHd x = show x
102104 elab' (PRef fc n) | pattern && not (inparamBlock n)
103105 = do ctxt <- get_context
104106 let sc = case lookupTy Nothing n ctxt of
@@ -170,7 +172,7 @@ elab ist info pattern tm
170172 ivs' <- get_instances
171173 when (not pattern) $
172174 mapM_ (\n -> do focus n
173− resolveTC 10 ist) (ivs' \\ ivs)
175+ resolveTC 7 ist) (ivs' \\ ivs)
174176-- ivs <- get_instances
175177-- when (not (null ivs)) $
176178-- do t <- get_term
@@ -222,12 +224,31 @@ trivial ist = try (elab ist toplevel False (PRefl (FC "prf" 0)))
222224 (tryAll xs)
223225
224226resolveTC :: Int -> IState -> Elab ()
227+resolveTC 0 ist = fail $ "Can't resolve type class"
225228resolveTC depth ist
226− = do t <- goal
229+ = try (trivial ist)
230+ (do t <- goal
231+ let (tc, ttypes) = unApply t
232+ needsDefault t tc ttypes
227233 tm <- get_term
228− try (trivial ist)
229− (blunderbuss t (map fst (ctxtAlist (tt_ctxt ist))))
234+-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $
235+-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))
236+ blunderbuss t (map fst (ctxtAlist (tt_ctxt ist))))
230237 where
238+ elabTC n | tcname n = (resolve n depth, show n)
239+ | otherwise = (fail "Can't resolve", show n)
240+
241+ needsDefault t num@(P _ (NS (UN "Num") ["builtins"]) _) [P Bound a _]
242+ = do focus a
243+ fill (RConstant IType) -- default Int
244+ solve
245+ needsDefault t f as
246+ | all boundVar as = fail $ "Can't resolve " ++ show t
247+ needsDefault t f a = return ()
248+
249+ boundVar (P Bound _ _) = True
250+ boundVar _ = False
251+
231252 blunderbuss t [] = fail $ "Can't resolve type class " ++ show t
232253 blunderbuss t (n:ns) | tcname n = try (resolve n depth)
233254 (blunderbuss t ns)