Skip to content

Commit

Permalink
Add missing call to instantiate in compileTerm
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
jespercockx committed Mar 22, 2024
1 parent 1dd0001 commit 060270e
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion src/Agda2Hs/Compile/Term.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 )
Expand Down Expand Up @@ -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
Expand Down

0 comments on commit 060270e

Please sign in to comment.