Open
Description
Apparently, an internal error occurs when attempting to run mimer if FromString is in scope and unqualified definitions are allowed. For example, the error occurs in the following program:
open import Agda.Builtin.FromString
data Obj : Set where obj : Obj
ex : Obj
ex = {! -u !}Attempting to run agda2-mimer with point in the hole causes the following message:
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Substitute.hs:87:26 in Agda-2.7.0.1-b0fa5c5e408fc4739c1af3c5d9cf6d20b9916cdf89483f2ad6c2902093f2d95c:Agda.TypeChecking.Substitute
Agda Version: 2.7.0.1
GHC Version: 9.12.2
Emacs Version: 29.4