Can't figure out type universe mismatch

Stream: new members

[aron]

When I define this data structure:

import Std.Data.HashSet
import Mathlib
open Std.DHashMap

instance [BEq k] [Hashable k] : Hashable (Std.HashSet k) where
  hash a := Std.HashSet.toArray a |> hash

structure DependentDisjointSet {v : Type u} (k : Type u) [BEq k] [Hashable k] (valType : Std.HashSet k → v) where
  innerMap : Std.DHashMap (Std.HashSet k) valType

I get this error when I set valType as the value to Std.DHashMap:

application type mismatch
  @Std.DHashMap (Std.HashSet k) valType
argument
  valType
has type
  Std.HashSet k → v : Type u
but is expected to have type
  Std.HashSet k → Type ?u.111 : Type (max (?u.111 + 1) u)

This doesn't happen when I set the return type of valType to just be a plain Type u instead of the v declared earlier in the type signature. I don't understand what the problem is though. How can I fix this?

[Kyle Miller]

I'm not sure what you're going for here. The valType function gives values of v, but DHashMap wants a function that gives types for each value, not values of v.

[Aaron Liu]

Let's try to use your definition as-is, ignoring the type error. Your definition is
DependentDisjointSet {v : Type u} (k : Type u) [BEq k] [Hashable k] (valType : Std.HashSet k → v)

I will substitute v := Nat, k := Bool and valType := fun (s : Std.HashSet Bool) => s.size. You can check that these are all type correct.
What type should innerMap have? According to your definition, it is a Std.DHashMap (Std.HashSet Bool) fun s => s.size.

Let's try to insert a value. According to the signature of docs#Std.DHashMap.insert, I need to provide a key of type Std.HashSet Bool first. I'll pick {}. Then, I need to provide a value of type (fun s => s.size) {}, which reduces to 0. I need to provide a value of type 0. What does that even mean?

As you can see, I ran into a problem. Lean sees this problem in advance when type-checking your definition, and raises an application type mismatch error.

[aron]

Hm so what I have in mind is for v to be something like MyType n, where n is a Nat that's derived from the key, which in this case is a Std.HashSet Bool. So the dependent type would be more like fun s => MyType s.size which for the empty key set would equal MyType 0.
Does that make more sense? Or have I missed the point you're making?

[Aaron Liu]

What you have in mind is great, but it doesn't stop the possibility of v being Nat. In fact, since the parameter v is a standalone type, it cannot depend on the key.

[Aaron Liu]

If you want to enforce this, do

structure DependentDisjointSet (k : Type u) [BEq k] [Hashable k] (v : Std.HashSet k → Nat) where
  innerMap : Std.DHashMap (Std.HashSet k) fun s => MyType (v s)

[Aaron Liu]

The example I gave ran into a problem because valType could return something that wasn't a type, which I did by making it return a Nat. This is why the signature of docs#Std.DHashMap requires its second argument to return a Type v.

[aron]

Hmm ok I don't 100% understand the issue yet, but it does make sense to me that if v is a standalone type then it's not a dependent type.
The truth is since I don't think I need to reference v outside of valType, I can just make valType have type Std.HashSet k → Type u and that works fine