difficulty adding string field to type class

Stream: lean4

[David Stainton 🦡]

Hi. I'm relatively new to Lean. Trying to add a string field called "name" to my NIKE type class:

class Key (key : Type) where
  encode : key → ByteArray
  decode : ByteArray → Option key

class PrivateKey (privkey : Type) extends Key privkey

class PublicKey (pubkey : Type) extends Key pubkey

class NIKE (scheme : Type) where
  PublicKeyType : Type
  PrivateKeyType : Type

  name : string
  privateKeySize : Nat
  publicKeySize : Nat

  generatePrivateKey : IO PrivateKeyType
  derivePublicKey : PrivateKeyType → PublicKeyType
  generateKeyPair : IO (PublicKeyType × PrivateKeyType)
  groupAction : PrivateKeyType → PublicKeyType → PublicKeyType
  encodePrivateKey : PrivateKeyType → ByteArray
  decodePrivateKey : ByteArray → Option PrivateKeyType
  encodePublicKey : PublicKeyType → ByteArray
  decodePublicKey : ByteArray → Option PublicKeyType

For some reason the compiler inference for the name field is:

name : {string : Sort u_1} → string

And I fail to add "name" to existing NIKE class instances:

structure X25519Scheme

instance : nike.NIKE X25519Scheme where
  PublicKeyType := PublicKey
  PrivateKeyType := PrivateKey

  name : String := "X25519"

  generatePrivateKey : IO PrivateKey := do
    generatePrivateKey

  generateKeyPair : IO (PublicKey × PrivateKey) := do
    let privKey ← generatePrivateKey
    let pubKey := derivePublicKey privKey
    pure (pubKey, privKey)

  derivePublicKey (sk : PrivateKey) : PublicKey := derivePublicKey sk

  groupAction (sk : PrivateKey) (pk : PublicKey) : PublicKey := PublicKey.mk $ curve25519 sk.data pk.data

  privateKeySize : Nat := keySize
  publicKeySize : Nat := keySize

  encodePrivateKey : PrivateKey → ByteArray := fun (sk : PrivateKey) => nike.Key.encode sk
  decodePrivateKey : ByteArray → Option PrivateKey := fun (bytes : ByteArray) => nike.Key.decode bytes
  encodePublicKey : PublicKey → ByteArray := fun (pk : PublicKey) => nike.Key.encode pk
  decodePublicKey : ByteArray → Option PublicKey := fun (bytes : ByteArray) => nike.Key.decode bytes

end CryptWalker.nike.x25519

fails to compile, with:

type mismatch
  "X25519"
has type
  String : Type
but is expected to have type
  {string : Sort ?u.8047} → string : Sort (imax (?u.8047 + 1) ?u.8047)

[Edward van de Meent]

string here is an identifier, while String is the type of strings... note the capital for the built-in type.

[Edward van de Meent]

the reason it doesn't throw an error due to not knowing what string means here is an option called autoImplicit, which while true adds unknown identifiers to the context as assumptions.

[David Stainton 🦡]

ah yeah thanks!

[Edward van de Meent]

you can turn this off with set_option autoImplicit false

[David Stainton 🦡]

Edward van de Meent said:

you can turn this off with set_option autoImplicit false

can i set that in my lakefile or does it have to be in the source code of my library?

[Edward van de Meent]

i think there is a way to do this in your lakefile, but i don't know it... maybe someone else could help there?

[David Stainton 🦡]

thanks for your help! the error messages were very confusing but i see what i did wrong now at least.

[Edward van de Meent]

i don't know if this translates one-to-one, but you could take inspiration from mathlibs lakefile: https://github.com/leanprover-community/mathlib4/blob/33d4a4af3e67a4561bbb0dacdc9800fc8785fa44/lakefile.lean#L39C1-L53C25

[Patrick Massot]

A simpler example can be found at https://github.com/avigad/mathematics_in_lean_source/blob/master/lakefile.lean

[David Stainton 🦡]

Thanks!