git.iko.soy/Idris-dev
on master help sign in
Don't search for type class instances we'll never solve - also allow default Int for Num
be33671Edwin Brady
src/Core/Typecheck.hs+1
compare with master
unifiedsplit
@@ -41,6 +41,7 @@ recheck ctxt env tm
41 = let v = next_tvar ctxt in
41 = let v = next_tvar ctxt in
42 case runStateT (check' False ctxt env (forget tm)) (v, []) of -- holes banned
42 case runStateT (check' False ctxt env (forget tm)) (v, []) of -- holes banned
43 Error (IncompleteTerm _) -> Error $ IncompleteTerm tm
43 Error (IncompleteTerm _) -> Error $ IncompleteTerm tm
44+ Error e -> Error e
44 OK ((tm, ty), constraints) ->
45 OK ((tm, ty), constraints) ->
45 return (tm, ty, constraints)
46 return (tm, ty, constraints)
46
47
src/Idris/ElabTerm.hs+29−8
@@ -9,6 +9,7 @@ import Core.Evaluate
9import Control.Monad
9import Control.Monad
10import Control.Monad.State
10import Control.Monad.State
11import Data.List
11import Data.List
12+import Debug.Trace
12
13
13-- Data to pass to recursively called elaborators; e.g. for where blocks,
14-- Data to pass to recursively called elaborators; e.g. for where blocks,
14-- paramaterised declarations, etc.
15-- paramaterised declarations, etc.
@@ -67,8 +68,8 @@ elab ist info pattern tm
67 elab' (PTrue fc) = try (elab' (PRef fc unitCon))
68 elab' (PTrue fc) = try (elab' (PRef fc unitCon))
68 (elab' (PRef fc unitTy))
69 (elab' (PRef fc unitTy))
69 elab' (PFalse fc) = elab' (PRef fc falseTy)
70 elab' (PFalse fc) = elab' (PRef fc falseTy)
70− elab' (PResolveTC (FC "HACK" _))
71+ elab' (PResolveTC (FC "HACK" _)) -- for chasing parent classes
71− = resolveTC 10 ist
72+ = resolveTC 2 ist
72 elab' (PResolveTC fc) = do c <- unique_hole (MN 0 "c")
73 elab' (PResolveTC fc) = do c <- unique_hole (MN 0 "c")
73 instanceArg c
74 instanceArg c
74 elab' (PRefl fc) = elab' (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,
75 elab' (PRefl fc) = elab' (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,
@@ -97,8 +98,9 @@ elab ist info pattern tm
97 [pimp (MN 0 "a") t,
98 [pimp (MN 0 "a") t,
98 pimp (MN 0 "P") Placeholder,
99 pimp (MN 0 "P") Placeholder,
99 pexp l, pexp r])
100 pexp l, pexp r])
100− elab' (PAlternative as) = tryAll (zip (map elab' as) (map show as))
101+ elab' (PAlternative as) = tryAll (zip (map elab' as) (map showHd as))
101−
102+ where showHd (PApp _ h _) = show h
103+ showHd x = show x
102 elab' (PRef fc n) | pattern && not (inparamBlock n)
104 elab' (PRef fc n) | pattern && not (inparamBlock n)
103 = do ctxt <- get_context
105 = do ctxt <- get_context
104 let sc = case lookupTy Nothing n ctxt of
106 let sc = case lookupTy Nothing n ctxt of
@@ -170,7 +172,7 @@ elab ist info pattern tm
170 ivs' <- get_instances
172 ivs' <- get_instances
171 when (not pattern) $
173 when (not pattern) $
172 mapM_ (\n -> do focus n
174 mapM_ (\n -> do focus n
173− resolveTC 10 ist) (ivs' \\ ivs)
175+ resolveTC 7 ist) (ivs' \\ ivs)
174-- ivs <- get_instances
176-- ivs <- get_instances
175-- when (not (null ivs)) $
177-- when (not (null ivs)) $
176-- do t <- get_term
178-- do t <- get_term
@@ -222,12 +224,31 @@ trivial ist = try (elab ist toplevel False (PRefl (FC "prf" 0)))
222 (tryAll xs)
224 (tryAll xs)
223
225
224resolveTC :: Int -> IState -> Elab ()
226resolveTC :: Int -> IState -> Elab ()
227+resolveTC 0 ist = fail $ "Can't resolve type class"
225resolveTC depth ist
228resolveTC depth ist
229+ = try (trivial ist)
226− = do t <- goal
230+ (do t <- goal
231+ let (tc, ttypes) = unApply t
232+ needsDefault t tc ttypes
227 tm <- get_term
233 tm <- get_term
228− try (trivial ist)
234+-- traceWhen (depth > 6) ("GOAL: " ++ show t ++ "\nTERM: " ++ show tm) $
235+-- (tryAll (map elabTC (map fst (ctxtAlist (tt_ctxt ist)))))
229− (blunderbuss t (map fst (ctxtAlist (tt_ctxt ist))))
236+ blunderbuss t (map fst (ctxtAlist (tt_ctxt ist))))
230 where
237 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+
231 blunderbuss t [] = fail $ "Can't resolve type class " ++ show t
252 blunderbuss t [] = fail $ "Can't resolve type class " ++ show t
232 blunderbuss t (n:ns) | tcname n = try (resolve n depth)
253 blunderbuss t (n:ns) | tcname n = try (resolve n depth)
233 (blunderbuss t ns)
254 (blunderbuss t ns)