Closed
Description
Attempting to use Mimer (C-c C-a) in the code below produces an internal error
open import Agda.Builtin.Equality
postulate
A : Set
eq : (a b : A) → a ≡ b
case_of_ : {A B : Set} → A → (A → B) → B
case x of f = f x
foo : (a b c d : A) → a ≡ d
foo a b c d = bar
where
bar : a ≡ d
bar =
case eq a b of λ where
refl →
case eq b c of λ where
refl →
case eq c d of λ where
refl →
{!!}The error is
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full\Agda\TypeChecking\Monad\Signature.hs:1163:32 in Agda-2.7.0-9be38c45d5c7c2dd550bc8810b0655b0ecc5d624:Agda.TypeChecking.Monad.Signature
Removing any of the case splits in bar or moving them out of the where block makes the error go away.
The error is present in Agda 2.7.0 and on a recent build of master.