@@ -999,10 +999,10 @@ elab ist info emode opts fn tm
999999 = do -- First extract the unquoted subterms, replacing them with fresh
10001000 -- names in the quasiquoted term. Claim their reflections to be
10011001 -- an inferred type (to support polytypic quasiquotes).
1002− qty <- goal
1002+ finalTy <- goal
10031003 (t, unq) <- extractUnquotes 0 t
10041004 let unquoteNames = map fst unq
1005− mapM_ (\uqn -> claim uqn (forget qty)) unquoteNames
1005+ mapM_ (\uqn -> claim uqn (forget finalTy)) unquoteNames
10061006
10071007 -- Save the old state - we need a fresh proof state to avoid
10081008 -- capturing lexically available variables in the quoted term.
@@ -1052,18 +1052,20 @@ elab ist info emode opts fn tm
10521052 env <- get_env
10531053 loadState
10541054 let quoted = fmap (explicitNames . binderVal) $ lookup nTm env
1055−
1055+ isRaw = case unApply (normaliseAll ctxt env finalTy) of
1056+ (P _ n _, []) | n == reflm "Raw" -> True
1057+ _ -> False
10561058 case quoted of
10571059 Just q -> do ctxt <- get_context
10581060 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
10591061 if pattern
1060− then do try' (reflectTTQuotePattern unquoteNames q')
1061− (reflectRawQuotePattern unquoteNames (forget q'))
1062− True
1063− else do try' (fill $ reflectTTQuote unquoteNames q')
1064− -- we forget q' instead of using q to ensure rechecking
1065− (fill $ reflectRawQuote unquoteNames (forget q'))
1066− True -- ignore errors like proof search does
1062+ then if isRaw
1063+ then reflectRawQuotePattern unquoteNames (forget q')
1064+ else reflectTTQuotePattern unquoteNames q'
1065+ else do if isRaw
1066+ then -- we forget q' instead of using q to ensure rechecking
1067+ fill $ reflectRawQuote unquoteNames (forget q')
1068+ else fill $ reflectTTQuote unquoteNames q'
10671069 solve
10681070
10691071 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"
@@ -2463,7 +2465,7 @@ reflectTTQuote unq (P nt n t)
24632465reflectTTQuote unq (V n)
24642466 = reflCall "V" [RConstant (I n)]
24652467reflectTTQuote unq (Bind n b x)
2466− = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote unq b, reflectTTQuote unq x]
2468+ = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]
24672469reflectTTQuote unq (App f x)
24682470 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
24692471reflectTTQuote unq (Constant c)
@@ -2480,7 +2482,7 @@ reflectRawQuote unq (Var n)
24802482 | n `elem` unq = Var n
24812483 | otherwise = reflCall "Var" [reflectName n]
24822484reflectRawQuote unq (RBind n b r) =
2483− reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote unq b, reflectRawQuote unq r]
2485+ reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]
24842486reflectRawQuote unq (RApp f x) =
24852487 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]
24862488reflectRawQuote unq RType = Var (reflm "RType")
@@ -2538,27 +2540,27 @@ reflectNameQuotePattern _ -- for all other names, match any
25382540 solve
25392541
25402542reflectBinder :: Binder Term -> Raw
2541−reflectBinder = reflectBinderQuote reflectTTQuote []
2542−
2543−reflectBinderQuote :: ([Name] -> a -> Raw) -> [Name] -> Binder a -> Raw
2544−reflectBinderQuote q unq (Lam t)
2545− = reflCall "Lam" [Var (reflm "TT"), q unq t]
2546−reflectBinderQuote q unq (Pi _ t k)
2547− = reflCall "Pi" [Var (reflm "TT"), q unq t, q unq k]
2548−reflectBinderQuote q unq (Let x y)
2549− = reflCall "Let" [Var (reflm "TT"), q unq x, q unq y]
2550−reflectBinderQuote q unq (NLet x y)
2551− = reflCall "NLet" [Var (reflm "TT"), q unq x, q unq y]
2552−reflectBinderQuote q unq (Hole t)
2553− = reflCall "Hole" [Var (reflm "TT"), q unq t]
2554−reflectBinderQuote q unq (GHole _ t)
2555− = reflCall "GHole" [Var (reflm "TT"), q unq t]
2556−reflectBinderQuote q unq (Guess x y)
2557− = reflCall "Guess" [Var (reflm "TT"), q unq x, q unq y]
2558−reflectBinderQuote q unq (PVar t)
2559− = reflCall "PVar" [Var (reflm "TT"), q unq t]
2560−reflectBinderQuote q unq (PVTy t)
2561− = reflCall "PVTy" [Var (reflm "TT"), q unq t]
2543+reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []
2544+
2545+reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw
2546+reflectBinderQuote q ty unq (Lam t)
2547+ = reflCall "Lam" [Var ty, q unq t]
2548+reflectBinderQuote q ty unq (Pi _ t k)
2549+ = reflCall "Pi" [Var ty, q unq t, q unq k]
2550+reflectBinderQuote q ty unq (Let x y)
2551+ = reflCall "Let" [Var ty, q unq x, q unq y]
2552+reflectBinderQuote q ty unq (NLet x y)
2553+ = reflCall "NLet" [Var ty, q unq x, q unq y]
2554+reflectBinderQuote q ty unq (Hole t)
2555+ = reflCall "Hole" [Var ty, q unq t]
2556+reflectBinderQuote q ty unq (GHole _ t)
2557+ = reflCall "GHole" [Var ty, q unq t]
2558+reflectBinderQuote q ty unq (Guess x y)
2559+ = reflCall "Guess" [Var ty, q unq x, q unq y]
2560+reflectBinderQuote q ty unq (PVar t)
2561+ = reflCall "PVar" [Var ty, q unq t]
2562+reflectBinderQuote q ty unq (PVTy t)
2563+ = reflCall "PVTy" [Var ty, q unq t]
25622564
25632565mkList :: Raw -> [Raw] -> Raw
25642566mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty