Section variables + typeclasses + notations

Stream: general

[Markus de Medeiros]

I ran into a problem in Iris-Lean recently and I'm looking for a any ideas on how to structure the code better to fix it. Here is a minimized version of the problem:

Code

axiom BundledGFunctors : Type _
axiom GName : Type _
axiom GFunctor : Type _

class Fraction (F : Type _)
axiom F1 [Fraction F] : GFunctor

class ElemG (GF : BundledGFunctors) (F : GFunctor)
axiom IProp (GF : BundledGFunctors) : Type _
axiom points_to {GF : BundledGFunctors}  [Fraction F] [ElemG GF (F1 (F := F))] : GName →  Nat → String → IProp GF

axiom entails {GF : BundledGFunctors} : IProp GF → Prop


noncomputable section Example2

variable [Fraction F] {GF} [ElemG GF (F1 (F := F))]

def MyPointsTo (γ : GName) (n : Nat) (s : String) := @points_to F GF _ _ γ n s

notation k:50 " ↦[" γ:50 "] " v:50 => points_to γ k v

-- example {γ : GName} : entails (5 ↦[γ] "A") := sorry
-- typeclass instance problem is stuck
--   ElemG ?m.6 F1

end Example2


noncomputable section Example2Hack

variable [Fraction F] {GF} [ElemG GF (F1 (F := F))]

-- Hack: Make typeclass synthesis infer GF and F from some piece of data present in the notation,
-- in this case GName.
set_option synthInstance.checkSynthOrder false in
class abbrev HasPointsToF1 (γ : GName) (GF : outParam _) (F : outParam (Type _))
    [Fraction F] := ElemG GF (F1 (F := F))

def MyPointsTo' (γ : GName)  [HasPointsToF1 γ GF F] (n : Nat) (s : String) := @points_to F GF _ _ γ n s

notation k:50 " ↦[" γ:50 "] " v:50 => MyPointsTo' γ k v

example {γ : GName} : entails (5 ↦[γ] "A") := sorry
-- No error

end Example2Hack

Basically, I want the (5 ↦[γ] "A") notation to refer to the ElemG and Fraction instances from the context, but Lean doesn't do this because GF and F are metavariables. In Rocq, the section variables for GF and F would be inserted into every definition in the section, meaning they are not metavariables, and the typeclass synthesis can proceed fine. I don't want to change my top-level notation to include GF and F.

The hack I came up with above works fine for this example, but I've noticed it doesn't work so well when I need multiples of the same typeclass (in our case, ElemG's). Is there a better way?

[Shreyas Srinivas]

Here's a hack:

axiom BundledGFunctors : Type _
axiom GName : Type _
axiom GFunctor : Type _

class Fraction (F : Type _)
axiom F1 [Fraction F] : GFunctor

class ElemG (GF : BundledGFunctors) (F : GFunctor)
axiom IProp (GF : BundledGFunctors) : Type _
axiom points_to {GF : BundledGFunctors}  [Fraction F] [ElemG GF (F1 (F := F))] : GName →  Nat → String → IProp GF

axiom entails {GF : BundledGFunctors} : IProp GF → Prop


noncomputable section Example2

variable {F} [i₁ : Fraction F] {GF} [i₂ : ElemG GF (F1 (F := F))]

def MyPointsTo (γ : GName) (n : Nat) (s : String) := @points_to F GF _ _ γ n s

set_option quotPrecheck false in
notation k:50 " ↦[" γ:50 "] " v:50 => @points_to F GF i₁ i₂ γ k v

example {γ : GName} : entails (5 ↦[γ] "A") := sorry
-- no more typeclass stuck problems

end Example2

[Shreyas Srinivas]

Now it works

[Shreyas Srinivas]

Just force lean to use a specific typeclass instance (which you declare as a variable) explicitly

[Shreyas Srinivas]

So one thing lean is annoying about is, inside notation, it considers variable declarations unhygienic. So I temporarily disable quotPrecheck just for that notation, because I don't expect to get that wrong.

[Markus de Medeiros]

Ah interesting, thanks!

[Shreyas Srinivas]

another related dirty trick I use sometimes is simp [explicitInstanceName] to get around these typeclass unification issues instead of simp[TypeclassName.<something>] (the simp is just illustrative). This is handy when there are multiple instances of the same typeclass or different typeclasses in the same hierarchy using the same notation (which happens a lot when you mix TCS and mathlib's order theory).

[Shreyas Srinivas]

@Markus de Medeiros : Actually I think this specific instance of the problem has nothing to do with typeclass inference

axiom BundledGFunctors : Type _
axiom GName : Type _
axiom GFunctor : Type _

class Fraction (F : Type _)
axiom F1 [Fraction F] : GFunctor

class ElemG (GF : BundledGFunctors) (F : GFunctor)
axiom IProp (GF : BundledGFunctors) : Type _
axiom points_to {GF : BundledGFunctors}  [Fraction F] [ElemG GF (F1 (F := F))] : GName →  Nat → String → IProp GF

axiom entails {GF : BundledGFunctors} : IProp GF → Prop


noncomputable section Example2

variable {F} [i₁ : Fraction F] {GF} [i₂ : ElemG GF (F1 (F := F))]

def MyPointsTo (γ : GName) (n : Nat) (s : String) := @points_to F GF _ _ γ n s

set_option quotPrecheck false in
notation k:50 " ↦[" γ:50 "] " v:50 => @points_to F GF _ _ γ k v

example {γ : GName} : entails (5 ↦[γ] "A") := sorry
-- no more typeclass stuck problems

end Example2

[Shreyas Srinivas]

It seems to be entirely a problem caused by name hygiene in notation. Otherwise how would inference succeed for _ and _ in the above example?

EDIT : I think unnamed typeclass instances are being treated as metavars in the notation. Named typeclass variables are being inferred even if I only give an _ where I want the instance. Try deleting i₁ : and my solution doesn't work.

[Shreyas Srinivas]

I am mildly confused why adding a name to the instance matters, and would like to figure what's really happening beyond my guesswork. Time to call Batman.
CC : @Mario Carneiro

[Sebastian Ullrich]

Shreyas Srinivas said:

inside notation, it considers variable declarations unhygienic

Which of course is exactly right in global notations. So the correct fix is to make them local notation

[Shreyas Srinivas]

Interesting. The warning messages I have received so far suggest the set_option quotPrecheck false solution, so I never figured local notation would do the trick

[Shreyas Srinivas]

@Sebastian Ullrich : why does it make a difference whether or not I name the typeclass instance in my final example?

[Sebastian Ullrich]

I don't see that on live

[Shreyas Srinivas]

I got an error when I removed the name i1

[Shreyas Srinivas]

Can’t seem to get it now.