Internal error on `primLockUniv`-sorted functions

[ionathanch]

Internal error on `primLockUniv`-sorted functions

[jespercockx]

Congratulations with finding the first new internal error in Agda 2.6.4!

[andreasabel]

Or, rather an old friend: 😉

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

Lines 66 to 71 in 5c81162

	-- 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__

[ionathanch]

If it helps, it seems to be resolved by changing instantiate to instantiateFull here:

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

Lines 46 to 48 in be28b6e

	-- Have to instantiate the lock, otherwise we might block on it even
	-- after it's been solved (e.g.: it's an interaction point, see #6528)
	lk <- instantiate lk

[andreasabel]

@ionathanch Thanks for the analysis. I turned your suggested fix into PR

• #6938