Fix #7086: Mimer crashing if called in type signature (#7089)

fix #7086: Mimer crashing if called in type signature
agda · Feb 5, 2024 · fbf9d15 · fbf9d15
1 parent 208f2bf
commit fbf9d15
Show file tree

Hide file tree

Showing 4 changed files with 49 additions and 30 deletions.
diff --git a/src/full/Agda/Mimer/Mimer.hs b/src/full/Agda/Mimer/Mimer.hs
@@ -611,36 +611,36 @@ collectLHSVars :: (MonadFail tcm, ReadTCState tcm, MonadError TCErr tcm, MonadTC
   => InteractionId -> tcm (Open [(Term, Bool)])
 collectLHSVars ii = do
   ipc <- ipClause <$> lookupInteractionPoint ii
-  let fnName = ipcQName ipc
-      clauseNr = ipcClauseNo ipc
-
-  info <- getConstInfo fnName
-  typ <- typeOfConst fnName
-  case theDef info of
-    fnDef@Function{} -> do
-      let clause = funClauses fnDef !! clauseNr
-          naps = namedClausePats clause
-
-      -- Telescope at interaction point
-      iTel <- getContextTelescope
-      -- Telescope for the body of the clause
-      let cTel = clauseTel clause
-      -- HACK: To get the correct indices, we shift by the difference in telescope lengths
-      -- TODO: Difference between teleArgs and telToArgs?
-      let shift = length (telToArgs iTel) - length (telToArgs cTel)
-
-      reportSDoc "mimer" 60 $ do
-        pITel <- prettyTCM iTel
-        pCTel <- prettyTCM cTel
-        return ("Tel:" $+$ nest 2 (pretty iTel $+$ pITel) $+$ "CTel:" $+$ nest 2 (pretty cTel $+$ pCTel))
-      reportSDoc "mimer" 60 $ return $ "Shift:" <+> pretty shift
-
-      -- TODO: Names (we don't use flex)
-      let flex = concatMap (go False . namedThing . unArg) naps
-          terms = map (\(n,i) -> (Var (n + shift) [], i)) flex
-      makeOpen terms
-    _ -> do
-      makeOpen []
+  case ipc of
+    IPNoClause -> makeOpen []
+    IPClause{ipcQName = fnName, ipcClauseNo = clauseNr} -> do
+      info <- getConstInfo fnName
+      typ <- typeOfConst fnName
+      case theDef info of
+        fnDef@Function{} -> do
+          let clause = funClauses fnDef !! clauseNr
+              naps = namedClausePats clause
+
+          -- Telescope at interaction point
+          iTel <- getContextTelescope
+          -- Telescope for the body of the clause
+          let cTel = clauseTel clause
+          -- HACK: To get the correct indices, we shift by the difference in telescope lengths
+          -- TODO: Difference between teleArgs and telToArgs?
+          let shift = length (telToArgs iTel) - length (telToArgs cTel)
+
+          reportSDoc "mimer" 60 $ do
+            pITel <- prettyTCM iTel
+            pCTel <- prettyTCM cTel
+            return ("Tel:" $+$ nest 2 (pretty iTel $+$ pITel) $+$ "CTel:" $+$ nest 2 (pretty cTel $+$ pCTel))
+          reportSDoc "mimer" 60 $ return $ "Shift:" <+> pretty shift
+
+          -- TODO: Names (we don't use flex)
+          let flex = concatMap (go False . namedThing . unArg) naps
+              terms = map (\(n,i) -> (Var (n + shift) [], i)) flex
+          makeOpen terms
+        _ -> do
+          makeOpen []
   where
     go isUnderCon = \case
       VarP patInf x -> [(dbPatVarIndex x, isUnderCon)]

diff --git a/test/interaction/Issue7086.agda b/test/interaction/Issue7086.agda
@@ -0,0 +1,9 @@
+
+data D : Set where
+  c : D
+
+postulate
+  F : D → Set
+
+x : F {!!}
+x = {!!}
diff --git a/test/interaction/Issue7086.in b/test/interaction/Issue7086.in
@@ -0,0 +1,2 @@
+top_command (cmd_load currentFile [])
+goal_command 0 cmd_autoOne ""
diff --git a/test/interaction/Issue7086.out b/test/interaction/Issue7086.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 : D ?1 : F ?0 " nil)
+((last . 1) . (agda2-goals-action '(0 1)))
+(agda2-give-action 0 "c")
+((last . 1) . (agda2-goals-action '(1)))