implicits and typeclasses

Stream: new members

[Quinn]

import Lean.Data.HashSet

variable {T : Type} [BEq T] [Hashable T]

def L : Type := Lean.HashSet T

structure S where
  x : L

This breaks with typeclass instance problem is stuck. it is often due to metavariables. I'm having a bunch of trouble with situations of this form. I think I can work around it with really bad ergonomics (like supplying instances as hypotheses with every single definition), but I'd like to get implicits to work

[Quinn]

i suspected tehre was a nuance i was missing with the namespace/section distinction, but reading tutorials and testing didn't substantiate that suspicion

[Quinn]

something even simpler:

variable {T : Type} [BEq T] [Hashable T]

def U := T deriving BEq, Hashable

I expected aliases of variables to be able to inherit class information

[Quinn]

failed to synthesize instance 'BEq' for 'U'

[Kyle Miller]

The issue is that L has T as an implicit argument, and x : L isn't enough information to solve for T

[Kyle Miller]

If you make it so that T is an explicit argument, then you can write x : L T and it should work.

[Quinn]

this means variable (T : Type) (paren instead of curly)? I think I was running into trouble with typeclass information not being propagated when I did that

[Kyle Miller]

Yeah, (T : Type).

The [...] variables will be included in definitions if they're used. Sometimes you might need to include instance binders explicitly, but, if you run into issues, feel free to post an example.