From 060270e1942f9b4e27c4c96a470873902d1f7eb4 Mon Sep 17 00:00:00 2001 From: Jesper Cockx Date: Fri, 15 Mar 2024 16:48:47 +0100 Subject: [PATCH] Add missing call to instantiate in compileTerm I ran into this while debugging #305, though I cannot reproduce a test case now. It seems like it's the right thing to do regardless. --- src/Agda2Hs/Compile/Term.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs index f8bc3540..7e413fde 100644 --- a/src/Agda2Hs/Compile/Term.hs +++ b/src/Agda2Hs/Compile/Term.hs @@ -23,7 +23,7 @@ import Agda.TypeChecking.Monad import Agda.TypeChecking.Pretty import Agda.TypeChecking.Records ( shouldBeProjectible ) import Agda.TypeChecking.Datatypes ( getConType ) -import Agda.TypeChecking.Reduce ( unfoldDefinitionStep ) +import Agda.TypeChecking.Reduce ( unfoldDefinitionStep, instantiate ) import Agda.TypeChecking.Substitute import Agda.TypeChecking.Telescope ( telView, mustBePi, piApplyM ) import Agda.TypeChecking.ProjectionLike ( reduceProjectionLike ) @@ -383,6 +383,8 @@ compileTerm ty v = do reportSDoc "agda2hs.compile.term" 10 $ text "compiling term:" <+> prettyTCM v + v <- instantiate v + let bad s t = genericDocError =<< vcat [ text "agda2hs: cannot compile" <+> text (s ++ ":") , nest 2 $ prettyTCM t