@@ -138,6 +138,13 @@ buildTC ist info emode opts fn tm
138138 else return (tm, ds, is)
139139 where pattern = emode == ELHS
140140
141+data ElabCtxt = ElabCtxt { e_inarg :: Bool,
142+ e_guarded :: Bool,
143+ e_intype :: Bool,
144+ e_qq :: Bool }
145+
146+initElabCtxt = ElabCtxt False False False False
147+
141148-- Returns the set of declarations we need to add to complete the definition
142149-- (most likely case blocks to elaborate)
143150
@@ -148,7 +155,7 @@ elab ist info emode opts fn tm
148155 when (loglvl > 5) $ unifyLog True
149156 compute -- expand type synonyms, etc
150157 let fc = maybe "(unknown)"
151− elabE (False, False, False, False) (elabFC info) tm -- (in argument, guarded, in type, in qquote)
158+ elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)
152159 end_unify
153160 ptm <- get_term
154161 when pattern -- convert remaining holes to pattern vars
@@ -186,7 +193,7 @@ elab ist info emode opts fn tm
186193 -- and forces/delays. If you make a recursive call in elab', it is
187194 -- normally correct to call elabE - the ones that don't are desugarings
188195 -- typically
189− elabE :: (Bool, Bool, Bool, Bool) -> Maybe FC -> PTerm -> ElabD ()
196+ elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
190197 elabE ina fc' t =
191198 --do g <- goal
192199 --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
@@ -247,7 +254,7 @@ elab ist info emode opts fn tm
247254
248255 -- "guarded" means immediately under a constructor, to help find patvars
249256
250− elab' :: (Bool, Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type, in a quasiquote)
257+ elab' :: ElabCtxt -- ^ (in an argument, guarded, in a type, in a quasiquote)
251258 -> Maybe FC -- ^ The closest FC in the syntax tree, if applicable
252259 -> PTerm -- ^ The term to elaborate
253260 -> ElabD ()
@@ -257,7 +264,11 @@ elab ist info emode opts fn tm
257264-- elab' (_,_,inty) (PConstant c)
258265-- | constType c && pattern && not reflection && not inty
259266-- = lift $ tfail (Msg "Typecase is not allowed")
260− elab' ina fc (PConstant c) = do apply (RConstant c) []; solve
267+ elab' ina fc tm@(PConstant c)
268+ | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
269+ && isTypeConst c
270+ = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
271+ | otherwise = do apply (RConstant c) []; solve
261272 elab' ina fc (PQuote r) = do fill r; solve
262273 elab' ina _ (PTrue fc _) =
263274 do hnf_compute
@@ -296,7 +307,7 @@ elab ist info emode opts fn tm
296307 [pimp (sUN "A") lt True,
297308 pimp (sUN "B") rt False,
298309 pexp l, pexp r])
299− elab' ina@(_, a, inty, qq) _ (PPair fc _ l r)
310+ elab' ina _ (PPair fc _ l r)
300311 = do hnf_compute
301312 g <- goal
302313 case g of
@@ -354,9 +365,12 @@ elab ist info emode opts fn tm
354365-- elab' (_, _, inty) (PRef fc f)
355366-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
356367-- = lift $ tfail (Msg "Typecase is not allowed")
357− elab' (ina, guarded, inty, qq) _ (PRef fc n)
358− | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not qq
359− = do ctxt <- get_context
368+ elab' ec _ (PRef fc n)
369+ | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)
370+ = do let ina = e_inarg ec
371+ guarded = e_guarded ec
372+ inty = e_intype ec
373+ ctxt <- get_context
360374 let defined = case lookupTy n ctxt of
361375 [] -> False
362376 _ -> True
@@ -374,8 +388,12 @@ elab ist info emode opts fn tm
374388 bindable (UN xs) = True
375389 bindable n = implicitable n
376390 elab' ina _ f@(PInferRef fc n) = elab' ina (Just fc) (PApp fc f [])
377− elab' ina _ (PRef fc n) = erun fc $ do apply (Var n) []; solve
378− elab' ina@(_, a, inty, qq) fc (PLam n Placeholder sc)
391+ elab' ina _ tm@(PRef fc n)
392+ | pattern && not reflection && not (e_qq ina) && not (e_intype ina)
393+ && isTConName n (tt_ctxt ist)
394+ = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
395+ | otherwise = erun fc $ do apply (Var n) []; solve
396+ elab' ina fc (PLam n Placeholder sc)
379397 = do -- if n is a type constructor name, this makes no sense...
380398 ctxt <- get_context
381399 when (isTConName n ctxt) $
@@ -383,8 +401,8 @@ elab ist info emode opts fn tm
383401 checkPiGoal n
384402 attack; intro (Just n);
385403 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
386− elabE (True, a, inty, qq) fc sc; solve
387− elab' ina@(_, a, inty, qq) fc (PLam n ty sc)
404+ elabE (ina { e_inarg = True } ) fc sc; solve
405+ elab' ec fc (PLam n ty sc)
388406 = do tyn <- getNameFrom (sMN 0 "lamty")
389407 -- if n is a type constructor name, this makes no sense...
390408 ctxt <- get_context
@@ -398,12 +416,15 @@ elab ist info emode opts fn tm
398416 hs <- get_holes
399417 introTy (Var tyn) (Just n)
400418 focus tyn
401− elabE (True, a, True, qq) fc ty
402− elabE (True, a, inty, qq) fc sc
419+
420+ elabE (ec { e_inarg = True, e_intype = True }) fc ty
421+ elabE (ec { e_inarg = True }) fc sc
403422 solve
404− elab' ina@(_, a, _, qq) fc (PPi _ n Placeholder sc)
405− = do attack; arg n (sMN 0 "ty"); elabE (True, a, True, qq) fc sc; solve
406− elab' ina@(_, a, _, qq) fc (PPi _ n ty sc)
423+ elab' ina fc (PPi _ n Placeholder sc)
424+ = do attack; arg n (sMN 0 "ty")
425+ elabE (ina { e_inarg = True, e_intype = True }) fc sc
426+ solve
427+ elab' ina fc (PPi _ n ty sc)
407428 = do attack; tyn <- getNameFrom (sMN 0 "ty")
408429 claim tyn RType
409430 n' <- case n of
@@ -411,10 +432,11 @@ elab ist info emode opts fn tm
411432 _ -> return n
412433 forall n' (Var tyn)
413434 focus tyn
414− elabE (True, a, True, qq) fc ty
415− elabE (True, a, True, qq) fc sc
435+ let ec' = ina { e_inarg = True, e_intype = True }
436+ elabE ec' fc ty
437+ elabE ec' fc sc
416438 solve
417− elab' ina@(_, a, inty, qq) fc (PLet n ty val sc)
439+ elab' ina fc (PLet n ty val sc)
418440 = do attack
419441 ivs <- get_instances
420442 tyn <- getNameFrom (sMN 0 "letty")
@@ -427,12 +449,14 @@ elab ist info emode opts fn tm
427449 Placeholder -> return ()
428450 _ -> do focus tyn
429451 explicit tyn
430− elabE (True, a, True, qq) fc ty
452+ elabE (ina { e_inarg = True, e_intype = True })
453+ fc ty
431454 focus valn
432− elabE (True, a, True, qq) fc val
455+ elabE (ina { e_inarg = True, e_intype = True })
456+ fc val
433457 ivs' <- get_instances
434458 env <- get_env
435− elabE (True, a, inty, qq) fc sc
459+ elabE (ina { e_inarg = True }) fc sc
436460 when (not pattern) $
437461 mapM_ (\n -> do focus n
438462 g <- goal
@@ -448,7 +472,7 @@ elab ist info emode opts fn tm
448472 expandLet n (case lookup n env of
449473 Just (Let t v) -> v)
450474 solve
451− elab' ina@(_, a, inty, qq) _ (PGoal fc r n sc) = do
475+ elab' ina _ (PGoal fc r n sc) = do
452476 rty <- goal
453477 attack
454478 tyn <- getNameFrom (sMN 0 "letty")
@@ -457,10 +481,10 @@ elab ist info emode opts fn tm
457481 claim valn (Var tyn)
458482 letbind n (Var tyn) (Var valn)
459483 focus valn
460− elabE (True, a, True, qq) (Just fc) (PApp fc r [pexp (delab ist rty)])
484+ elabE (ina { e_inarg = True, e_intype = True }) (Just fc) (PApp fc r [pexp (delab ist rty)])
461485 env <- get_env
462486 computeLet n
463− elabE (True, a, inty, qq) (Just fc) sc
487+ elabE (ina { e_inarg = True }) (Just fc) sc
464488 solve
465489-- elab' ina fc (PLet n Placeholder
466490-- (PApp fc r [pexp (delab ist rty)]) sc)
@@ -523,12 +547,16 @@ elab ist info emode opts fn tm
523547-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq
524548-- = lift $ tfail (Msg "Typecase is not allowed")
525549 -- if f is local, just do a simple_app
526− elab' (ina, g, inty, qq) _ tm@(PApp fc (PRef _ f) args)
550+ elab' ina _ tm@(PApp fc (PRef _ f) args)
527551 = do env <- get_env
552+ ty <- goal
553+ when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)
554+ && isTConName f (tt_ctxt ist)) $
555+ lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
528556 if (f `elem` map fst env && length args == 1)
529557 then -- simple app, as below
530− do simple_app (elabE (ina, g, inty, qq) (Just fc) (PRef fc f))
531− (elabE (True, g, inty, qq) (Just fc) (getTm (head args)))
558+ do simple_app (elabE ina (Just fc) (PRef fc f))
559+ (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))
532560 (show tm)
533561 solve
534562 else
@@ -557,7 +585,7 @@ elab ist info emode opts fn tm
557585 let (ns', eargs) = unzip $
558586 sortBy cmpArg (zip ns args)
559587 ulog <- getUnifyLog
560− elabArgs ist (ina || not isinf, guarded, inty, qq)
588+ elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })
561589 [] fc False f ns'
562590 (f == sUN "Force")
563591 (map (\x -> getTm x) eargs) -- TODO: remove this False arg
@@ -565,7 +593,8 @@ elab ist info emode opts fn tm
565593 ivs' <- get_instances
566594 -- Attempt to resolve any type classes which have 'complete' types,
567595 -- i.e. no holes in them
568− when (not pattern || (ina && not tcgen && not guarded)) $
596+ when (not pattern || (e_inarg ina && not tcgen &&
597+ not (e_guarded ina))) $
569598 mapM_ (\n -> do focus n
570599 g <- goal
571600 env <- get_env
@@ -646,13 +675,14 @@ elab ist info emode opts fn tm
646675 setInjective (PApp _ (PRef _ n) _) = setinj n
647676 setInjective _ = return ()
648677
649− elab' ina@(_, a, inty, qq) _ tm@(PApp fc f [arg])
678+ elab' ina _ tm@(PApp fc f [arg])
650679 = erun fc $
651− do simple_app (elabE ina (Just fc) f) (elabE (True, a, inty, qq) (Just fc) (getTm arg))
680+ do simple_app (elabE ina (Just fc) f) (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))
652681 (show tm)
653682 solve
654− elab' ina fc Placeholder = do (h : hs) <- get_holes
655− movelast h
683+ elab' ina fc Placeholder
684+ = do (h : hs) <- get_holes
685+ movelast h
656686 elab' ina fc (PMetavar n) =
657687 do ptm <- get_term
658688 -- When building the metavar application, leave out the unique
@@ -705,7 +735,7 @@ elab ist info emode opts fn tm
705735 elab' ina (Just fc) sc
706736 elab' ina (Just fc) (PRef fc letn)
707737 solve
708− elab' ina@(_, a, inty, qq) _ c@(PCase fc scr opts)
738+ elab' ina _ c@(PCase fc scr opts)
709739 = do attack
710740 tyn <- getNameFrom (sMN 0 "scty")
711741 claim tyn RType
@@ -714,7 +744,7 @@ elab ist info emode opts fn tm
714744 claim valn (Var tyn)
715745 letbind scvn (Var tyn) (Var valn)
716746 focus valn
717− elabE (True, a, inty, qq) (Just fc) scr
747+ elabE (ina { e_inarg = True }) (Just fc) scr
718748 -- Solve any remaining implicits - we need to solve as many
719749 -- as possible before making the 'case' type
720750 unifyProblems
@@ -779,7 +809,7 @@ elab ist info emode opts fn tm
779809 elab' ina fc (PUnifyLog t) = do unifyLog True
780810 elab' ina fc t
781811 unifyLog False
782− elab' (ina, g, inty, qq) fc (PQuasiquote t goal) -- TODO: goal type
812+ elab' ina fc (PQuasiquote t goal) -- TODO: goal type
783813 = do -- First extract the unquoted subterms, replacing them with fresh
784814 -- names in the quasiquoted term. Claim their reflections to be
785815 -- of type TT.
@@ -824,11 +854,11 @@ elab ist info emode opts fn tm
824854 case goal of
825855 Nothing -> return ()
826856 Just gTy -> do focus qTy
827− elabE (ina, g, inty, True) fc gTy
857+ elabE (ina { e_qq = True }) fc gTy
828858
829859 -- Elaborate the quasiquoted term into the hole
830860 focus qTm
831− elabE (ina, g, inty, True) fc t
861+ elabE (ina { e_qq = True }) fc t
832862 end_unify
833863
834864 -- We now have an elaborated term. Reflect it and solve the
@@ -854,7 +884,7 @@ elab ist info emode opts fn tm
854884
855885 elabUnquote (n, tm)
856886 = do focus n
857− elabE (ina, g, inty, False) fc tm
887+ elabE (ina { e_qq = False }) fc tm
858888
859889
860890 elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"
@@ -966,7 +996,7 @@ elab ist info emode opts fn tm
966996
967997 -- | Elaborate the arguments to a function
968998 elabArgs :: IState -- ^ The current Idris state
969− -> (Bool, Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type, in a qquote)
999+ -> ElabCtxt -- ^ (in an argument, guarded, in a type, in a qquote)
9701000 -> [Bool]
9711001 -> FC -- ^ Source location
9721002 -> Bool
@@ -976,10 +1006,15 @@ elab ist info emode opts fn tm
9761006 -> [PTerm] -- ^ (Laziness, argument)
9771007 -> ElabD ()
9781008 elabArgs ist ina failed fc retry f [] force _ = return ()
979− elabArgs ist ina failed fc r f (n:ns) force (Placeholder : args)
980− = elabArgs ist ina failed fc r f ns force args
9811009 elabArgs ist ina failed fc r f ((argName, holeName):ns) force (t : args)
982− = elabArg argName holeName t
1010+ = do hs <- get_holes
1011+ if holeName `elem` hs then
1012+ do focus holeName
1013+ case t of
1014+ Placeholder -> do movelast holeName
1015+ elabArgs ist ina failed fc r f ns force args
1016+ _ -> elabArg argName holeName t
1017+ else elabArgs ist ina failed fc r f ns force args
9831018 where elabArg argName holeName t =
9841019 do -- solveAutos ist fn False
9851020 now_elaborating fc f argName
@@ -991,13 +1026,11 @@ elab ist info emode opts fn tm
9911026 let elab = if force then elab' else elabE
9921027 failed' <- -- trace (show (n, t, hs, tm)) $
9931028 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
994− case holeName `elem` hs of
995− True -> do focus holeName;
996− g <- goal
997− ulog <- getUnifyLog
998− traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $
999− elab ina (Just fc) t; return failed
1000− False -> return failed
1029+ do focus holeName;
1030+ g <- goal
1031+ ulog <- getUnifyLog
1032+ traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $
1033+ elab ina (Just fc) t; return failed
10011034 done_elaborating_arg f argName
10021035 elabArgs ist ina failed fc r f ns force args
10031036 wrapErr f argName action =