Case where a generalised instance variable is changed to implicit

[EDT4]

Case where a generalised instance variable is changed to implicit

[andreasabel]

Debug printing with -v tc.generalize:40:

open metas = fromList [(MetaId 11 ... argInfoHiding = Instance NoOverlap, ...,(MetaId 13 ... argInfoHiding = NotHidden, ...
computing generalization for type _8
  generalizable        =  _x_11, _x..1_9, _x.X_10
  generalizableOpen    =  _x_11
Inherited metas from _x..1_9: _13
Inherited metas from _x.X_10: _x..1.1_13
  alsoGeneralize       =  _x.X.1_13
we're generalizing over _x_11, _x.X.1_13
created genRec Issue7047..generalizedField-x.X.1,
               Issue7047..generalizedField-x
created genRecordType
  genRecName   =  Issue7047.GeneralizeTel
  genRecCon    =  Issue7047.mkGeneralizeTel
  genRecFields =  x.X.1, x
solving generalized meta _x.X.1_13 := x.X.1
solving generalized meta _x_11 := x
teleTypes = [({x.X.1},Level), (⦃ x ⦄,Set x.X.1)]
genTel    = {x.X.1 : Level} ⦃ x : Set x.X.1 ⦄

There is a visible meta _13 which is later turned hidden, yet there is never any information that it should be Instance.
The meta seems to come from here:

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

Lines 368 to 374 in 01f12f0

	inherited <- fmap Set.unions $ forM generalizableClosed $ \ (x, mv) ->
	case mvInstantiation mv of
	InstV inst -> do
	parentName <- getMetaNameSuggestion x
	metas <- filterM canGeneralize . Set.toList .
	allMetas Set.singleton =<<
	instantiateFull (instBody inst)