Internal error with --two-level due to blocking on solved meta

[sattlerc]

Internal error with --two-level due to blocking on solved meta

[andreasabel]

agda/src/full/Agda/TypeChecking/Constraints.hs

Lines 66 to 71 in fe43379

	-- Jesper, 2022-10-22: We should never block on a meta that is
	-- already solved.
	forM_ (allBlockingMetas unblock) $ \ m ->
	whenM (isInstantiatedMeta m) $ do
	reportSDoc "tc.constr.add" 5 $ "Attempted to block on solved meta" <+> prettyTCM m
	__IMPOSSIBLE__

This is another instance of

• #6758

[andreasabel]

With -v tc:30 the last words of Agda are:

solving _9 := _10
completed assignment of _9@14618456326245523507
Postponing constraint
  funSort SSet _10 == SSet
adding constraint funSort SSet _10 = SSet
                    (blocked on _7, belongs to problem 6) unblocker:  _7
Attempted to block on solved meta _7

The diff between Set and SSet seems to be the unsolvability of funSort SSet _10 == SSet (the equivalent for Set solves _10 := Set).

[andreasabel]

Could be related:

• #2978

Relevant debug print seems to be:

equalSort _7 (y = y) == _9
term _9 := _7 (y = y)
...
initOccursCheck: we look into the following definitions:
(none)
offending variable:  y
  of type  A
  (after singleton test)
error during flexible occurs check, we are StronglyRigid
Pattern violation (you shouldn't see this)
oops, pattern violation for _7@14618456326245523507
attempting kills
  m'    = _7@14618456326245523507
  vs    = [y]
  kills = [True]
after kill analysis
  metavar = _7
  kills   = [True]
  kills'  = [True]
  oldType = (y₁ : A) →
            "dummyType: __DUMMY_TYPE__, called at src/full/Agda/TypeChecking/MetaVars.hs:197:25 in Agda-2.6.5-4ATBkX6jZbSGAWG421gpPu:Agda.TypeChecking.MetaVars"
  newType = "dummyType: __DUMMY_TYPE__, called at src/full/Agda/TypeChecking/MetaVars.hs:197:25 in Agda-2.6.5-4ATBkX6jZbSGAWG421gpPu:Agda.TypeChecking.MetaVars"
...
actual killing
  new meta: _10@14618456326245523507
  kills   : True
  inst    : _7@14618456326245523507 := _10
completed assignment of _7@14618456326245523507
passed occursCheck
...
solving _9 := _10
completed assignment of _9@14618456326245523507
funSortEquals
  s0 = SSet
  s1 = SSet
  s2 = _10
Postponing constraint
  funSort SSet _10 == SSet
adding constraint funSort SSet _10 = SSet
                    (blocked on _7, belongs to problem 6) unblocker:  _7
Attempted to block on solved meta _7

_7 is solved by pruning, so it is not a valid blocker anymore. The logic of blockers does not seem to expect a meta suddently solved by pruning.

Relevant code:

agda/src/full/Agda/TypeChecking/Conversion.hs

Lines 1690 to 1704 in fe43379

	s1b <- reduceB s1
	s2b <- reduceB s2
	let (s1,s2) = (ignoreBlocking s1b, ignoreBlocking s2b)
	blocker = unblockOnEither (getBlocker s1b) (getBlocker s2b)
	let postponeIfBlocked = catchPatternErr $ \blocker ->
	if | blocker == neverUnblock -> typeError $ UnequalSorts s1 s2
	| otherwise -> do
	reportSDoc "tc.conv.sort" 30 $ vcat
	[ "Postponing constraint"
	, nest 2 $ fsep [ prettyTCM s1 <+> "=="
	, prettyTCM s2 ]
	]
	addConstraint blocker $ SortCmp CmpEq s1 s2

agda/src/full/Agda/TypeChecking/Conversion.hs

Line 1711 in fe43379

postponeIfBlocked $ case (s1, s2) of

agda/src/full/Agda/TypeChecking/Conversion.hs

Lines 1741 to 1743 in fe43379

	-- equating @FunSort a b@ to another sort
	(s1 , FunSort a b) -> funSortEquals propEnabled s1 a b blocker
	(FunSort a b , s2) -> funSortEquals propEnabled s2 a b blocker

agda/src/full/Agda/TypeChecking/Conversion.hs

Lines 1880 to 1883 in fe43379

	-- Equate a sort @s@ to @funSort s1 s2@
	-- Precondition: @s@ and @funSort s1 s2@ are already reduced
	funSortEquals :: Bool -> Sort -> Sort -> Sort -> Blocker -> m ()
	funSortEquals propEnabled s0 s1 s2 blocker = do

[andreasabel]

I might have introduced this regression when I refactored some code related to sorts during AIM XXXVI Delft and after.
Could be:

• #6623

[andreasabel]

Unfortunately, bisection only produces the usual suspect:

536b73f is the first bad commit
Author: Jesper Cockx
Date: Fri Nov 11 11:34:05 2022 +0000
[ re #6211 ] Pull off the band-aid

This does not provide any interesting information...

Only that I could have been wrong about blaming myself...