Type equality constraint/type class?

Stream: general

[Jessica Foster]

I'm porting some Haskell code to lean and I'm trying to find an equivalent/replacement for Data.Type.Equality's a ~ b class and I'm struggling. It's a type class constraint which says 'a unifies with b' and is hooked into the type checker. It serves two purposes for the code I'm working on:

1. Manipulating instance resolution
2. Improving type inference/error messages

For example, consider the following code which only allows pairs of certain types:

class Pair (a b : Type) where
  pair : a -> b -> a × b
open Pair

instance : Pair Char Bool where
  pair x y := ⟨x, y⟩

#check pair 'x' true -- All good
#check pair 'x' 'y' -- error: 'failed to synthesize instance  Pair Char Char'
#check pair 'x' -- : ?m -> Char × ?m

Here, pair 'x' 'y'(correctly) fails to synthesise an instance where a and b are both Char, but let's say I want to be a bit more specific about my instance: if a is Char, then b must be Bool. I want to write something like this:

instance [b ~ Bool] : Pair Char b where
  pair x y := ⟨x, y⟩

#check pair 'x' true -- All good
#check pair 'x' 'y' -- error: 'y' has type `Char` but is expected to have type `Bool`
#check pair 'x' -- : Bool -> Char × Bool

Here, only the a/Char determines which instance is selected and b is unified with Bool (or fails to unify) after this selection has already taken place. Is something like this possible in lean?

[Aaron Liu]

I don't think we have a class like that. Can't you just make a Pair Char Bool?

[Aaron Liu]

You can make b an outParam to "constrain" it with instances

[Aaron Liu]

class Pair (a : Type) (b : outParam Type) where
  pair : a -> b -> a × b
open Pair

instance : Pair Char Bool where
  pair x y := ⟨x, y⟩

#check pair 'x' true -- All good
#check pair 'x' 'y' -- error: 'failed to synthesize instance  Pair Char Char'
#check pair 'x' -- pair 'x' : Bool → Char × Bool
-- delay elaboration with `by exact`
#check pair 'x' (by exact 'y') -- type mismatch, 'y' has type Char but is expected to have type Bool

[Jessica Foster]

Ah, I was hopeful outParam might do the trick, but my actual code is recursive + has variables so I get the error 'instance does not provide concrete values for (semi-)out-params'

[Jessica Foster]

It'd be a shame if there's no way around this, it's a very common trick in Haskell type class programming (and important for our upcoming POPL submission :sweat_smile:). Do you have any tips for debugging instance resolution? Any way to see what instances it's trying to use etc.

[Aaron Liu]

Jessica Foster said:

Do you have any tips for debugging instance resolution? Any way to see what instances it's trying to use etc.

Usually set_option trace.Meta.synthInstance true tells me everything I need to know

[Aaron Liu]

If you're still having issues you can build a #mwe and I can take a look at it

[Jessica Foster]

Ah that helps a lot, thank you!