@@ -154,8 +154,12 @@ elab ist info pattern opts fn tm
154154 (h: hs) -> do patvar h; mkPat
155155 [] -> return ()
156156
157+ -- | elabE elaborates an expression, possibly wrapping implicit coercions
158+ -- and forces/delays. If you make a recursive call in elab', it is
159+ -- normally correct to call elabE - the ones that don't are desugarings
160+ -- typically
157161 elabE :: (Bool, Bool, Bool) -> PTerm -> ElabD ()
158− elabE ina t =
162+ elabE ina t =
159163 --do g <- goal
160164 --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
161165 do ct <- insertCoerce ina t
@@ -204,6 +208,8 @@ elab ist info pattern opts fn tm
204208 constType VoidType = True
205209 constType _ = False
206210
211+ -- "guarded" means immediately under a constructor, to help find patvars
212+
207213 elab' :: (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)
208214 -> PTerm -- ^ The term to elaborate
209215 -> ElabD ()
@@ -634,7 +640,7 @@ elab ist info pattern opts fn tm
634640 = do -- First elaborate the unquoted subterms, replacing them with
635641 -- fresh names in the quasiquoted term
636642 (t, unq) <- extractUnquotes t
637− mapM_ elabUnquote unq
643+ mapM_ (flip claim (Var tt) . fst) unq
638644 let unquoteNames = map fst unq
639645
640646 -- Save the old state - we need a fresh proof state for this to
@@ -643,10 +649,15 @@ elab ist info pattern opts fn tm
643649 saveState
644650 updatePS (const .
645651 newProof (sMN 0 "q") ctxt $
646− P Ref (sNS (sUN "TT") ["Reflection", "Language"]) Erased)
652+ P Ref tt Erased)
647653
648− -- Re-add the unquotes
649− mapM_ (flip claim (Var (sNS (sUN "TT") ["Reflection", "Language"]))) unquoteNames
654+ -- Re-add the unquotes, letting Idris infer the types
655+ mapM_ (\n -> do ty <- getNameFrom (sMN 0 "unqTy")
656+ claim ty RType
657+ movelast ty
658+ claim n (Var ty)
659+ movelast n)
660+ unquoteNames
650661
651662 -- Establish holes for the type and value of the term to be
652663 -- quasiquoted
@@ -658,27 +669,31 @@ elab ist info pattern opts fn tm
658669 -- the hole doesn't disappear
659670 nTm <- getNameFrom (sMN 0 "quotedTerm")
660671 letbind nTm (Var qTy) (Var qTm)
672+
661673 -- We must solve the type later through unification
662674 movelast qTy
663− -- Elaborate the quasiquoted term into the hole that was
675+ -- Elaborate the quasiquoted term into the hole
664676 focus qTm
665− elab' ina t
677+ elabE ina t
678+ end_unify
666679 -- We now have an elaborated term. Reflect it and solve the
667680 -- original goal
668681 env <- get_env
669682 let qTerm = fmap (reflectQuote unquoteNames . binderVal) $ lookup nTm env
683+
670684 case qTerm of
671685 Just q -> do loadState
672686 fill q
673687 solve
688+ mapM_ elabUnquote unq
674689 Nothing -> fail "Broken elaboration of quasiquote"
675− where elabUnquote (n, tm)
676− = do qn <- getNameFrom (sMN 0 "unquotHole")
677− let tt = sNS (sUN "TT") ["Reflection", "Language"]
678− claim qn (Var tt)
679− letbind n (Var tt) (Var qn)
680− focus qn
681− elab' ina tm
690+ where tt = sNS (sUN "TT") ["Reflection", "Language"]
691+
692+ elabUnquote (n, tm)
693+ = do focus n
694+ elabE ina tm
695+
696+
682697 elab' ina (PUnquote t) = fail "Found unquote outside of quasiquote"
683698 elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
684699