@@ -14,7 +14,7 @@ import Idris.Core.Elaborate hiding (Tactic(..))
1414import Idris.Core.TT
1515import Idris.Core.Evaluate
1616import Idris.Core.Unify
17−import Idris.Core.Typecheck (check)
17+import Idris.Core.Typecheck (check, recheck)
1818import Idris.ErrReverse (errReverse)
1919import Idris.ElabQuasiquote (extractUnquotes)
2020
@@ -729,12 +729,16 @@ elab ist info emode opts fn tm
729729 -- original goal in the original proof state.
730730 env <- get_env
731731 loadState
732− case fmap (explicitNames . binderVal) $ lookup nTm env of
733− Just q
734− | pattern -> reflectQuotePattern unquoteNames q
735− | otherwise -> do fill $ reflectQuote unquoteNames q
736− solve
737− Nothing -> fail "Broken elaboration of quasiquote"
732+ let quoted = fmap (explicitNames . binderVal) $ lookup nTm env
733+
734+ case quoted of
735+ Just q -> do ctxt <- get_context
736+ (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
737+ if pattern
738+ then reflectQuotePattern unquoteNames q'
739+ else do fill $ reflectQuote unquoteNames q'
740+ solve
741+ Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"
738742
739743 -- Finally fill in the terms or patterns from the unquotes. This
740744 -- happens last so that their holes still exist while elaborating
@@ -746,6 +750,11 @@ elab ist info emode opts fn tm
746750 = do focus n
747751 elabE (ina, g, inty, False) tm
748752
753+ holesInTerm tm = do hs <- get_holes
754+ return $ intersect (freeNames tm) hs
755+ removeAll xs [] = []
756+ removeAll xs (y:ys) | y `elem` xs = removeAll xs ys
757+ | otherwise = y : removeAll xs ys
749758
750759 elab' ina (PUnquote t) = fail "Found unquote outside of quasiquote"
751760 elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x