@@ -637,22 +637,25 @@ elab ist info pattern opts fn tm
637637 elab' ina t
638638 unifyLog False
639639 elab' (ina, g, inty, qq) (PQuasiquote t)
640− = do -- First elaborate the unquoted subterms, replacing them with
641− -- fresh names in the quasiquoted term
640+ = do -- First extract the unquoted subterms, replacing them with fresh
641+ -- names in the quasiquoted term. Claim their reflections to be
642+ -- of type TT.
642643 (t, unq) <- extractUnquotes t
643644 let unquoteNames = map fst unq
644645 mapM_ (flip claim (Var tt)) unquoteNames
645646
646647
647− -- Save the old state - we need a fresh proof state for this to
648− -- avoid capture
648+ -- Save the old state - we need a fresh proof state to avoid
649+ -- capturing lexically available variables in the quoted term.
649650 ctxt <- get_context
650651 saveState
651652 updatePS (const .
652653 newProof (sMN 0 "q") ctxt $
653654 P Ref tt Erased)
654655
655− -- Re-add the unquotes, letting Idris infer the (fictional) types
656+ -- Re-add the unquotes, letting Idris infer the (fictional)
657+ -- types. Here, they represent the real type rather than the type
658+ -- of their reflection.
656659 mapM_ (\n -> do ty <- getNameFrom (sMN 0 "unqTy")
657660 claim ty RType
658661 movelast ty
@@ -670,16 +673,17 @@ elab ist info pattern opts fn tm
670673 -- the hole doesn't disappear
671674 nTm <- getNameFrom (sMN 0 "quotedTerm")
672675 letbind nTm (Var qTy) (Var qTm)
673−
674676 -- We must solve the type later through unification
675677 movelast qTy
678+
679+
676680 -- Elaborate the quasiquoted term into the hole
677681 focus qTm
678682 elabE (ina, g, inty, True) t
679683 end_unify
680684
681685 -- We now have an elaborated term. Reflect it and solve the
682− -- original goal
686+ -- original goal in the original proof state.
683687 env <- get_env
684688 loadState
685689 case fmap (explicitNames . binderVal) $ lookup nTm env of
@@ -688,6 +692,10 @@ elab ist info pattern opts fn tm
688692 | otherwise -> do fill $ reflectQuote unquoteNames q
689693 solve
690694 Nothing -> fail "Broken elaboration of quasiquote"
695+
696+ -- Finally fill in the terms or patterns from the unquotes. This
697+ -- happens last so that their holes still exist while elaborating
698+ -- the main quotation.
691699 mapM_ elabUnquote unq
692700 where tt = sNS (sUN "TT") ["Reflection", "Language"]
693701