Constraint Inference bug (?)

Stream: lean4

[Daniel Rogozin]

Hello everyone

I've just encountered a weird phenomenon, which seems to be a bug in constraint inference
I have the following typeclasses (methods are omitted for simplicity)

class CurveGroup {F : Type _} [Field F] (C : Curve F) (K : outParam $ Type _) where

class PointSerialise {F : Type _} [Field F] (C : Curve F) (K : outParam $ Type _) [CurveGroup C K] where

and also I have instances for types ProjectivePoint and AffinePoint (with required typevariables and constraints defined above in my module)

instance : CurveGroup C (ProjectivePoint C) where
instance : CurveGroup C (AffinePoint C) where

But when I'm trying to declare instances of PointSerialise in the same module, instance : PointSerialise C (ProjectivePoint C) where is accepted, whereas instance : PointSerialise C (AffinePoint C) where is rejected with failed to synthesize instance CurveGroup C (AffinePoint C). That's strange 'cause all required CurveGroup instances are declared in the same module.

[Kevin Buzzard]

Can you post a #mwe ? Your question is much more likely to get a helpful answer that way. Right now all we know is that either you made a mistake somewhere or there's a bug, and it's difficult to diagnose further without being able to see the error on my own computer.

[Daniel Rogozin]

I've just pushed the commit with that error, I can post the github link here

[Daniel Rogozin]

Or let me just post the full listing with required definitions

[Daniel Rogozin]

import YatimaStdLib.Ring

structure Curve (F : Type _) [Field F] where
  a : F
  b : F

structure ProjectivePoint {F : Type _} [Field F] (C : Curve F) where
  X : F
  Y : F
  Z : F

inductive AffinePoint {F : Type _} [Field F] (C : Curve F) where
  | affine (X : F) (Y : F) : AffinePoint C
  | infinity : AffinePoint C
  deriving BEq

variable {F : Type _} [Field F] (C : Curve F)

class CurveGroup {F : Type _} [Field F] (C : Curve F) (K : outParam $ Type _) where
  zero : K
  inv : K → K
  add : K → K → K
  double : K → K

open ProjectivePoint in
instance : CurveGroup C (ProjectivePoint C) where
  zero := infinity
  inv := fun ⟨x, y, z⟩ => ⟨x, 0 - y, z⟩
  add := add
  double := double

open AffinePoint in
instance : CurveGroup C (AffinePoint C) where
  zero := infinity
  inv := neg
  add := add
  double := double

class PointSerialise {F : Type _} [Field F] (C : Curve F) (K : outParam $ Type _) [CurveGroup C K] where
  serialise : K → ByteArray
  deserialise : ByteArray → Option K

namespace Serialise
variable {F : Type _} [Field F] {C : Curve F}

-- rejected with "failed to synthesize instance CurveGroup C (AffinePoint C)"
instance : PointSerialise C (AffinePoint C) where
  serialise := sorry
  deserialise := sorry

-- accepted
instance : PointSerialise C (ProjectivePoint C) where
  serialise := sorry
  deserialise := sorry

[Daniel Rogozin]

Here it is

[Daniel Rogozin]

The full module is in here
https://github.com/yatima-inc/FF.lean/blob/daniel/restructure-typeclasses/FF/EllipticCurve.lean

[Kevin Buzzard]

this isn't a #mwe because it has a random import :-/

[Kevin Buzzard]

This is a mwe:

import Mathlib

structure Curve (F : Type _) [Field F] where
  a : F
  b : F

structure ProjectivePoint {F : Type _} [Field F] (C : Curve F) where
  X : F
  Y : F
  Z : F

inductive AffinePoint {F : Type _} [Field F] (C : Curve F) where
  | affine (X : F) (Y : F) : AffinePoint C
  | infinity : AffinePoint C
  deriving BEq

variable {F : Type _} [Field F] (C : Curve F)

class CurveGroup {F : Type _} [Field F] (C : Curve F) (K : outParam $ Type _) where


open ProjectivePoint in
instance : CurveGroup C (ProjectivePoint C) where


open AffinePoint in
instance : CurveGroup C (AffinePoint C) where


class PointSerialise {F : Type _} [Field F] (C : Curve F) (K : outParam $ Type _) [CurveGroup C K] where
  serialise : K → ByteArray
  deserialise : ByteArray → Option K

namespace Serialise
variable {F : Type _} [Field F] {C : Curve F}

-- rejected with "failed to synthesize instance CurveGroup C (AffinePoint C)"
instance : PointSerialise C (AffinePoint C) where
  serialise := sorry
  deserialise := sorry

-- accepted
instance : PointSerialise C (ProjectivePoint C) where
  serialise := sorry
  deserialise := sorry

[Henrik Böving]

I'm not sure whether importing mathlib counts as more of a mwe compared to importing yatimas lib :P

[Daniel Rogozin]

Fair enough, sorry

[Kevin Buzzard]

and this is a better one because it doesn't need mathlib. The trick is to get rid of all imports so it works for everyone else and they can see the same error. Note that I'm changing your definitions but keeping the error alive.

class Field (F : Type _) where

structure Curve (F : Type _) [Field F] where
  a : F
  b : F

structure ProjectivePoint {F : Type _} [Field F] (C : Curve F) where
  X : F
  Y : F
  Z : F

inductive AffinePoint {F : Type _} [Field F] (C : Curve F) where
  | affine (X : F) (Y : F) : AffinePoint C
  | infinity : AffinePoint C
  deriving BEq

variable {F : Type _} [Field F] (C : Curve F)

class CurveGroup {F : Type _} [Field F] (C : Curve F) (K : outParam $ Type _) where


open ProjectivePoint in
instance : CurveGroup C (ProjectivePoint C) where


open AffinePoint in
instance : CurveGroup C (AffinePoint C) where


class PointSerialise {F : Type _} [Field F] (C : Curve F) (K : outParam $ Type _) [CurveGroup C K] where
  serialise : K → ByteArray
  deserialise : ByteArray → Option K

namespace Serialise
variable {F : Type _} [Field F] {C : Curve F}

-- rejected with "failed to synthesize instance CurveGroup C (AffinePoint C)"
instance : PointSerialise C (AffinePoint C) where
  serialise := sorry
  deserialise := sorry

-- accepted
instance : PointSerialise C (ProjectivePoint C) where
  serialise := sorry
  deserialise := sorry

[Kevin Buzzard]

Henrik Böving said:

I'm not sure whether importing mathlib counts as more of a mwe compared to importing yatimas lib :P

Well I guess this is a cultural thing: mathlib imports in mwes in lean 3 have always been acceptable. Of course I can see your point (which is why I fixed it) but a lot of people on this chat have got mathlib handy; I suspect rather fewer have got Yatima's library handy. It's all about making it easier for as many other people as possible. Anyway, I removed the mathlib import so maybe you can figure out the problem now :-)

[Kevin Buzzard]

[Meta.synthInstance] ❌ CurveGroup C (AffinePoint C) ▼
  [] new goal CurveGroup C _tc.0 ▶
  [] ✅ apply @instCurveGroupProjectivePoint to CurveGroup C (ProjectivePoint C) ▶
  [] result instCurveGroupProjectivePoint C
  [] ❌ result type
        CurveGroup C (ProjectivePoint C)
      is not definitionally equal to
        CurveGroup C (AffinePoint C)

Not that instance Lean! What are you doing??

[Kevin Buzzard]

Is the issue that the OutParam is being used incorrectly? I've never understood these properly, but my basic understanding is that class CurveGroup {F : Type _} [Field F] (C : Curve F) (K : outParam $ Type _) where means "you give me F and C and I'm going to figure out what K is later on, and there is going to be one answer so you are going to suffer if you want there to be two". Don't take my word for it here though.

[Henrik Böving]

Yes that is the reason. Basically when you have parameters p_1, p_2, ... p_n and you declared p_{n+1} as out param what you say is that p_1...p_n uniquely determine p_{n+1} so you do not need it at the beginning of type class synthesis since the first instance you find that matches should give you a value for p_{n+1}. Since in this case this invariant does (obviously) not hold things blow up.

[Henrik Böving]

If you think of type class instances as a relational database you might also say that the non output parameters form a composite primary key for the outParam ones.

[Daniel Rogozin]

Thanks! I think outParam was redundant. The error is no longer relevant after removing outParam.

[Henrik Böving]

Well it depends really. outParam's can be helpful mostly when type inference isn't strong enough. For example say that you have a HAdd type class with 3 parameters (2 for the addition input, 1 for the addition output). One can argue whether the output one should be an outParam or not. If you can safely rely on type inference managing to infere a value for the third one all the time you can safely let it be a normal parameter and grant your users more freedom in the instances they might declare. If you think this is not the case you might want to declare it an outParam which takes a bit of freedom away from the instances you can write (as you have just experienced yourself) but can make the typeclass <-> type inference interaction more smooth.

[Daniel Rogozin]

I think I've gotta learn what outParam does in-depth. TBH, I was using that as a black box thinking that it's somewhat similar to fundeps in Haskell

[Henrik Böving]

What I explained in my first message is precisely what outParam does. THe second one just describes implications that using or not using outParam can have in applications.

[Daniel Rogozin]

What I explained in my first message is precisely what outParam does.

Thanks, I got it!

I meant also playing with more examples to understand deeply how to use outParam in a more appropriate way.