Closed
Description
On master (ee876ee).
{-# OPTIONS --two-level #-}
module Issue7034 where
open import Agda.Primitive using (SSet)
postulate
A : SSet
x : A
foo : {!(y : A) → ?!}
foo = xFilling the hole gives:
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Constraints.hs:71:11 in Agda-2.6.5-ec51c49b804662559b10509859f950f6b1a84575acb5950875806501b569d6c0:Agda.TypeChecking.Constraints
This references a case in addConstraintTM:
forM_ (allBlockingMetas unblock) $ \ m ->
whenM (isInstantiatedMeta m) $ do
reportSDoc "tc.constr.add" 5 $ "Attempted to block on solved meta" <+> prettyTCM m
__IMPOSSIBLE__