Zulip Chat Archive

Stream: lean4

Topic: difficulty adding string field to type class


David Stainton 🦡 (Aug 28 2024 at 11:51):

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 (Aug 28 2024 at 11:53):

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

Edward van de Meent (Aug 28 2024 at 11:55):

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 🦡 (Aug 28 2024 at 11:55):

ah yeah thanks!

Edward van de Meent (Aug 28 2024 at 11:55):

you can turn this off with set_option autoImplicit false

David Stainton 🦡 (Aug 28 2024 at 11:55):

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 (Aug 28 2024 at 11:57):

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 🦡 (Aug 28 2024 at 11:58):

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

Edward van de Meent (Aug 28 2024 at 12:04):

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 (Aug 28 2024 at 12:15):

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

David Stainton 🦡 (Aug 28 2024 at 12:16):

Thanks!


Last updated: May 02 2025 at 03:31 UTC