Scoping instances

Stream: mathlib4

[Matthew Ballard]

Is it really the case that none of our 222 Fintype instances are scoped?

import Mathlib

open Lean Meta Elab Command

run_cmd do -- 222, 0
  let dt ← liftCoreM getGlobalInstancesIndex
  let globalNames : Array Name := dt.fold (init := #[]) fun arr keys inst =>
    if let .const `Fintype _ := keys[0]! then
      if inst.attrKind == .global then
        arr.push inst.globalName?.get!
      else arr
    else arr
  let scopedNames := dt.fold (init := #[]) fun arr keys inst =>
    if let .const `Fintype _ := keys[0]! then
      if inst.attrKind == .scoped then
        arr.push inst.globalName?.get!
      else arr
    else arr
  logInfo m!"{globalNames.size}, {scopedNames.size}"

[Matthew Ballard]

Here are their names

[Unique.fintype,
 CategoryTheory.FinCategory.fintypeObj,
 SetLike.instFintype,
 NonemptyFiniteLinearOrder.toFintype,
 FinEnum.instFintype,
 IsSimpleOrder.instFintypeOfDecidableEq,
 Prop.fintype,
 instFintypeSymbol,
 Submodule.Quotient.fintype,
 Submodule.QuotientTop.fintype,
 QuotientGroup.fintype,
 QuotientAddGroup.fintype,
 CategoryTheory.FinCategory.fintypeHom,
 CategoryTheory.Limits.WidePullbackShape.fintypeHom,
 CategoryTheory.finBiconeHom,
 CategoryTheory.FinCategory.instFintypeHomObjAsType,
 CategoryTheory.Limits.WidePushoutShape.fintypeHom,
 CategoryTheory.discreteHomFintype,
 Configuration.instFintypeDual,
 Turing.PartrecToTM2.instFintypeΓ',
 CategoryTheory.Limits.fintypeWalkingParallelPair,
 Polynomial.Gal.instFintype,
 Matrix.instFintypeOfDecidableEq,
 Additive.fintype,
 minpoly.AlgHom.fintype,
 Lex.fintype,
 Finset.fintype,
 CategoryTheory.Limits.instFintypeWalkingParallelPairHom,
 RelHom.instFintype,
 SimpleGraph.instFintypeColoring,
 CategoryTheory.Limits.WidePullbackShape.fintypeObj,
 ULift.fintype,
 compositionAsSetFintype,
 Turing.TM2to1.Γ'.fintype,
 Polynomial.IsSplittingField.instFintypeSplittingField,
 CategoryTheory.finBicone,
 NumberField.Embeddings.instFintypeRingHom,
 GaloisField.instFintype,
 instFintypeConjClassesOfDecidableRelIsConj,
 instFintypeUnitsOfDecidableEq,
 UnitsInt.fintype,
 SetTheory.PGame.fintypeRightMoves,
 SetTheory.PGame.fintypeRightMovesOfStateAux,
 instFintypeSum,
 equivFintype,
 Subtype.fintype,
 Fintype.subtypeEq,
 Finset.fintypeCoeSort,
 List.Subtype.fintype,
 Multiset.Subtype.fintype,
 Finset.Subtype.fintype,
 FinsetCoe.fintype,
 Set.fintypeUniv,
 Set.fintypeUnion,
 Set.fintypeSep,
 Set.fintypeInter,
 Set.fintypeInterOfLeft,
 Set.fintypeInterOfRight,
 Set.fintypeDiff,
 Set.fintypeDiffLeft,
 Set.fintypeiUnion,
 Set.fintypesUnion,
 Set.fintypeBiUnion',
 Set.fintypeBind',
 Set.fintypeEmpty,
 Set.fintypeSingleton,
 Set.fintypePure,
 Set.fintypeInsert,
 Set.fintypeInsert',
 Set.fintypeImage,
 Set.fintypeRange,
 Set.fintypeMap,
 Set.fintypeImage2,
 Set.fintypeSeq,
 Set.fintypeSeq',
 Set.fintypeMemFinset,
 Submonoid.fintypePowers,
 AddSubmonoid.fintypeMultiples,
 RingHom.fintypeRangeS,
 RingHom.fintypeRange,
 Set.fintypeIcc,
 Set.fintypeIco,
 Set.fintypeIoc,
 Set.fintypeIoo,
 Set.fintypeIci,
 Set.fintypeIoi,
 Set.fintypeIic,
 Set.fintypeIio,
 Set.fintypeUIcc,
 LinearMap.fintypeRange,
 NonUnitalRingHom.fintypeRange,
 NonUnitalAlgHom.fintypeRange,
 AlgHom.fintypeRange,
 Subgroup.instFintypeSubtypeMemOfDecidablePred,
 AddSubgroup.instFintypeSubtypeMemOfDecidablePred,
 Subgroup.fintypeBot,
 AddSubgroup.fintypeBot,
 MonoidHom.fintypeMrange,
 AddMonoidHom.fintypeMrange,
 MonoidHom.fintypeRange,
 AddMonoidHom.fintypeRange,
 conjugatesOf.fintype,
 ConjClasses.instFintypeElemCarrier,
 Polynomial.rootSetFintype,
 IsNoetherian.instFintypeElemOfVectorSpaceIndex,
 FiniteDimensional.instFintypeElemOfVectorSpaceIndex,
 RingHom.fintypeFieldRange,
 SimpleGraph.neighborSetFintype,
 SimpleGraph.Subgraph.finiteAt,
 SimpleGraph.Subgraph.instFintypeElemNeighborSetOfVertsOfDecidablePredMemSet,
 instFintypeElemImageToSetOfDecidableEqOfSingletonSet,
 Fintype.subtypeEq',
 SimpleGraph.fintypeSetWalkLength,
 SimpleGraph.fintypeSubtypeWalkLength,
 SimpleGraph.fintypeSetPathLength,
 rootsOfUnity.fintype,
 NumberField.Units.instFintypeSubtypeUnitsRingOfIntegersMemSubgroupTorsion,
 instFintypeElemPermDerangements,
 alternatingGroup.instFintype,
 SimpleGraph.Subgraph.coeFiniteAt,
 Equiv.Perm.VectorsProdEqOne.instFintypeElemVectorVectorsProdEqOne,
 fintypeNodupList,
 FreeGroup.instFintypeSubtypeListProdBoolRed,
 Set.fintypeLTNat,
 Set.fintypeLENat,
 SimpleGraph.fintypeEdgeSet,
 SimpleGraph.fintypeEdgeSetBot,
 SimpleGraph.fintypeEdgeSetSup,
 SimpleGraph.fintypeEdgeSetInf,
 SimpleGraph.fintypeEdgeSetSdiff,
 SimpleGraph.instFintypeElemSym2EdgeSetFromEdgeSetOfDecidableEq,
 SimpleGraph.incidenceSetFintype,
 SimpleGraph.instFintypeElemSym2EdgeSetEdge,
 Set.fintypeProd,
 Set.fintypeOffDiag,
 SimpleGraph.boxProdFintypeNeighborSet,
 instFintypeElemProdNatSetOfLtSndCountFst,
 Cycle.fintypeNodupNontrivialCycle,
 Cycle.fintypeNodupCycle,
 instFintype_memPartition,
 Profinite.NobelingProof.instFintypeElemForallBoolπMemFinset,
 PLift.fintype,
 PLift.fintypeProp,
 Fintype.instPEmpty,
 SimpleGraph.Dart.fintype,
 compositionFintype,
 SimpleGraph.instFintypeConnectedComponent,
 Vector.fintype,
 CategoryTheory.Limits.fintypeWalkingPair,
 instFintypeSym'OfDecidableEq,
 ZMod.fintype,
 CategoryTheory.Limits.FintypeCat.finiteColimitOfFiniteDiagram,
 QuaternionGroup.instFintypeOfNeZeroNat,
 Function.Embedding.fintype,
 instFintypeSimpleGraphOfDecidableEq,
 Module.Free.ChooseBasisIndex.fintype,
 Multiplicative.fintype,
 CategoryTheory.Limits.FintypeCat.finiteLimitOfFiniteDiagram,
 RelEmbedding.instFintype,
 Fintype.instEmpty,
 Quotient.fintype,
 QuotientAddGroup.fintypeQuotientRightRel,
 QuotientGroup.fintypeQuotientRightRel,
 SetTheory.PGame.fintypeLeftMoves,
 SetTheory.PGame.fintypeLeftMovesOfStateAux,
 AlgEquiv.fintype,
 instFintypeAlgEquivOfIsDomainOfIsIntegrallyClosedOfFiniteOfNoZeroSMulDivisors,
 instFintypeClassGroupOfIsPrincipalIdealRing,
 FunctionField.RingOfIntegers.instFintypeClassGroupSubtypeMemSubalgebraPolynomialRingOfIntegers,
 NumberField.RingOfIntegers.instFintypeClassGroup,
 Unit.fintype,
 PUnit.fintype,
 SimplicialObject.Splitting.IndexSet.instFintype,
 Nat.Partition.instFintype,
 Hamming.instFintypeOfDecidableEq,
 LucasLehmer.X.instFintype,
 DihedralGroup.instFintypeOfNeZeroNat,
 instFintypeSymOfDecidableEq,
 Bool.fintype,
 SignType.instFintype,
 NumberField.InfinitePlace.NumberField.InfinitePlace.fintype,
 DFinsupp.fintype,
 Affine.Simplex.instFintypePointsWithCircumcenterIndex,
 Multiset.fintypeCoe,
 FirstOrder.Ring.instFintypeSymbolsRing,
 Shrink.instFintype,
 Sym2.instFintype,
 OrderDual.fintype,
 instFintypeProd,
 Fin.fintype,
 Abelianization.instFintypeOfDecidablePredMemSubgroupCommutator,
 PSigma.fintypePropLeft,
 PSigma.fintypePropRight,
 PSigma.fintypePropProp,
 PSigma.instFintype,
 CategoryTheory.Limits.WidePushoutShape.fintypeObj,
 ConjAct.instFintype,
 Finpartition.instFintypeOfDecidableEq,
 LieModule.Weight.instFintype,
 Computability.Γ'.fintype,
 Finsupp.fintype,
 Sigma.instFintype,
 CategoryTheory.discreteFintype,
 Fin2.instFintype,
 OnePoint.instFintype,
 Module.End.instFintypeEigenvalues,
 instFintypeOption,
 Set.fintype,
 TruncatedWittVector.instFintype,
 pfunFintype,
 Pi.fintype,
 AlgebraicGeometry.Scheme.instFintypeJFiniteSubcover,
 FintypeCat.instFintypeα,
 FinBoolAlg.isFintype,
 FinBddDistLat.isFintype,
 FinTopCat.fintype,
 FinTopCat.instFintypeαTopologicalSpaceObjTopCatForget₂,
 FinPartOrd.isFintype,
 SimplexCategory.instFintypeObjForget,
 FinTopCat.instFintypeObjForget,
 Computability.Γ.fintype,
 CategoryTheory.Mat_.fintype]

[Eric Wieser]

My understanding was that scoped instance was only for instances that carry surprising or controversial data; and the fact that Subsingleton (Fintype _) is true means that Fintype instances should never be surprising.

[Matthew Ballard]

How much work does Lean need to do to not be surprised?

[Matthew Ballard]

CommSemiring is 69, 0 so this behavior is the case across all classes

[Matthew Ballard]

I would imagine any instance declared in CategoryTheory should be scoped to CategoryTheory for example

[Matthew Ballard]

No one is accidentally using Quiver.Hom notation.

[Jireh Loreaux]

Shouldn't that mean that those instances aren't ever checked in the first place when people aren't using them? So there's no need to scope them?

[Jireh Loreaux]

(the category theory ones, not CommSemiring)

[Matthew Ballard]

It depends on the keys.

[Matthew Ballard]

If those are robust enough, then yes. But in some cases they are not, eg lean#4932

[Matthew Ballard]

For example, CategoryTheory.FinCategory.fintypeObj will be tried for any search for Fintype on a Subtype

[Eric Wieser]

I think rather than disabling instances, it might be better to try and come up with a better keying algorithm

[Eric Wieser]

Perhaps along the lines of allowing a custom key generator for certain types like Subtype

[Matthew Ballard]

lean#4932 should fix the Subtype issue itself but philosophically why should one want to have anything to do with CategoryTheory instances if they are not working explicitly on CategoryTheory when all the basic notation is scoped to that namespace already

[Matthew Ballard]

One thing that the keying algorithm doesn't do is look in the context. One could imagine some light weight filtering based on this information.