@@ -62,7 +62,7 @@ buildTC ist info pattern tcgen fn tm
6262elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->
6363 ElabD ()
6464elab ist info pattern tcgen fn tm
65− = do elabE False tm
65+ = do elabE (False, False) tm -- (in argument, guarded)
6666 when pattern -- convert remaining holes to pattern vars
6767 mkPat
6868 inj <- get_inj
@@ -108,9 +108,10 @@ elab ist info pattern tcgen fn tm
108108 elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,
109109 pimp (MN 0 "b") Placeholder,
110110 pexp l, pexp r])
111− elab' ina (PPair fc l r) = try (elabE True (PApp fc (PRef fc pairTy)
111+ elab' ina@(_, a) (PPair fc l r)
112+ = try (elabE (True, a) (PApp fc (PRef fc pairTy)
112113 [pexp l,pexp r]))
113− (elabE True (PApp fc (PRef fc pairCon)
114+ (elabE (True, a) (PApp fc (PRef fc pairCon)
114115 [pimp (MN 0 "A") Placeholder,
115116 pimp (MN 0 "B") Placeholder,
116117 pexp l, pexp r]))
@@ -135,31 +136,37 @@ elab ist info pattern tcgen fn tm
135136 (tryAll (zip (map (elab' ina) as) (map showHd as)))
136137 where showHd (PApp _ h _) = show h
137138 showHd x = show x
138− elab' ina (PRef fc n) | pattern && not (inparamBlock n)
139+ elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)
139140 = do ctxt <- get_context
140141 let iscon = isConName Nothing n ctxt
141− if (not iscon && ina) then erun fc $ patvar n
142− else try (do apply (Var n) []; solve)
143− (patvar n)
142+ let defined = case lookupTy Nothing n ctxt of
143+ [] -> False
144+ _ -> True
145+ -- this is to stop us resolve type classes recursively
146+ if (tcname n && ina) then erun fc $ patvar n
147+ else if (defined && not guarded)
148+ then do apply (Var n) []; solve
149+ else try (do apply (Var n) []; solve)
150+ (patvar n)
144151 where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of
145152 [] -> False
146153 _ -> True
147154 elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
148− elab' ina (PLam n Placeholder sc)
149− = do attack; intro (Just n); elabE True sc; solve
150− elab' ina (PLam n ty sc)
155+ elab' ina@(_, a) (PLam n Placeholder sc)
156+ = do attack; intro (Just n); elabE (True, a) sc; solve
157+ elab' ina@(_, a) (PLam n ty sc)
151158 = do tyn <- unique_hole (MN 0 "lamty")
152159 claim tyn RSet
153160 attack
154161 introTy (Var tyn) (Just n)
155162 -- end_unify
156163 focus tyn
157− elabE True ty
158− elabE True sc
164+ elabE (True, a) ty
165+ elabE (True, a) sc
159166 solve
160− elab' ina (PPi _ n Placeholder sc)
161− = do attack; arg n (MN 0 "ty"); elabE True sc; solve
162− elab' ina (PPi _ n ty sc)
167+ elab' ina@(_,a) (PPi _ n Placeholder sc)
168+ = do attack; arg n (MN 0 "ty"); elabE (True, a) sc; solve
169+ elab' ina@(_,a) (PPi _ n ty sc)
163170 = do attack; tyn <- unique_hole (MN 0 "ty")
164171 claim tyn RSet
165172 n' <- case n of
@@ -167,10 +174,10 @@ elab ist info pattern tcgen fn tm
167174 _ -> return n
168175 forall n' (Var tyn)
169176 focus tyn
170− elabE True ty
171− elabE True sc
177+ elabE (True, a) ty
178+ elabE (True, a) sc
172179 solve
173− elab' ina (PLet n ty val sc)
180+ elab' ina@(_,a) (PLet n ty val sc)
174181 = do attack;
175182 tyn <- unique_hole (MN 0 "letty")
176183 claim tyn RSet
@@ -180,10 +187,10 @@ elab ist info pattern tcgen fn tm
180187 case ty of
181188 Placeholder -> return ()
182189 _ -> do focus tyn
183− elabE True ty
190+ elabE (True, a) ty
184191 focus valn
185− elabE True val
186− elabE True sc
192+ elabE (True, a) val
193+ elabE (True, a) sc
187194 solve
188195-- elab' ina (PTyped val ty)
189196-- = do tyn <- unique_hole (MN 0 "castty")
@@ -198,27 +205,29 @@ elab ist info pattern tcgen fn tm
198205-- | [d] <- lookupCtxt Nothing dsl (idris_dsls ist)
199206-- = let dsl' = expandDo d (getTm arg) in
200207-- trace (show dsl') $ elab' ina dsl'
201− elab' ina (PApp fc (PRef _ f) args')
208+ elab' (ina, g) (PApp fc (PRef _ f) args')
202209 = do let args = {- case lookupCtxt f (inblock info) of
203210 Just ps -> (map (pexp . (PRef fc)) ps ++ args')
204211 _ ->-} args'
205212 ivs <- get_instances
206213 -- HACK: we shouldn't resolve type classes if we're defining an instance
207− -- function or default defition.
214+ -- function or default definition.
208215 let isinf = f == inferCon || tcname f
216+ ctxt <- get_context
217+ let guarded = isConName Nothing f ctxt
209218 try (do ns <- apply (Var f) (map isph args)
210219 solve
211220 let (ns', eargs)
212221 = unzip $
213222 sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))
214223 (zip ns args)
215− try (elabArgs (ina || not isinf)
224+ try (elabArgs (ina || not isinf, guarded)
216225 [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))
217− (elabArgs (ina || not isinf)
226+ (elabArgs (ina || not isinf, guarded)
218227 [] False (reverse ns')
219228 (map (\x -> (lazyarg x, getTm x)) (reverse eargs))))
220229-- (try (do apply2 (Var f) (map (toElab' (ina || not isinf)) args))
221− (do apply_elab f (map (toElab (ina || not isinf)) args)
230+ (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)
222231 solve)
223232 ivs' <- get_instances
224233 when (not pattern || (ina && not tcgen)) $
@@ -233,9 +242,9 @@ elab ist info pattern tcgen fn tm
233242 where tcArg (n, PConstraint _ _ Placeholder) = True
234243 tcArg _ = False
235244
236− elab' a (PApp fc f [arg])
245+ elab' ina@(_, a) (PApp fc f [arg])
237246 = erun fc $
238− do simple_app (elabE a f) (elabE True (getTm arg))
247+ do simple_app (elabE ina f) (elabE (True, a) (getTm arg))
239248 solve
240249 elab' ina Placeholder = do (h : hs) <- get_holes
241250 movelast h
@@ -250,7 +259,7 @@ elab ist info pattern tcgen fn tm
250259 | not pattern = do mapM_ (runTac False ist) ts
251260 | otherwise = elab' ina Placeholder
252261 elab' ina (PElabError e) = fail e
253− elab' ina c@(PCase fc scr opts)
262+ elab' ina@(_, a) c@(PCase fc scr opts)
254263 = do attack
255264 tyn <- unique_hole (MN 0 "scty")
256265 claim tyn RSet
@@ -259,7 +268,7 @@ elab ist info pattern tcgen fn tm
259268 claim valn (Var tyn)
260269 letbind scvn (Var tyn) (Var valn)
261270 focus valn
262− elabE True scr
271+ elabE (True, a) scr
263272 args <- get_env
264273 cname <- unique_hole (mkCaseName fn)
265274 elab' ina (PMetavar cname)