Fix #7084: Mimer internal error (#7087)

fix #7084: get correct type for projections in parameterised modules
agda · Feb 5, 2024 · 2925d77 · 2925d77
1 parent a445e3b
commit 2925d77
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 1 deletion.
diff --git a/src/full/Agda/Mimer/Mimer.hs b/src/full/Agda/Mimer/Mimer.hs
@@ -966,7 +966,7 @@ applyProj recordArgs comp' qname = do
   cost <- asks (costProj . searchCosts)
   let newTerm = applyE (compTerm comp') [Proj ProjSystem qname]
   reportDoc "mimer.temp" 10 $ "applyProj: newTerm =" <+> pretty newTerm
-  projType <- typeOfConst qname
+  projType <- defType <$> getConstInfo qname
   projTypeWithArgs <- piApplyM projType recordArgs
   newType <- piApplyM projTypeWithArgs (compTerm comp')
   reportSDoc "mimer.temp" 10 $ do

diff --git a/test/interaction/Issue7084.agda b/test/interaction/Issue7084.agda
@@ -0,0 +1,8 @@
+
+module _ (X : Set) where
+
+  record R : Set₁ where
+    field t : X
+
+  auto : R → X
+  auto r = {!!}
diff --git a/test/interaction/Issue7084.in b/test/interaction/Issue7084.in
@@ -0,0 +1,2 @@
+top_command (cmd_load currentFile [])
+goal_command 0 cmd_autoOne ""
diff --git a/test/interaction/Issue7084.out b/test/interaction/Issue7084.out
@@ -0,0 +1,8 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-status-action "")
+(agda2-info-action "*All Goals*" "?0 : X " nil)
+((last . 1) . (agda2-goals-action '(0)))
+(agda2-give-action 0 "R.t r")
+((last . 1) . (agda2-goals-action '()))