how does type class inference work?

Stream: general

[Kevin Buzzard]

class foo (A : Type) :=
(blah : ℕ)

class bar (A : Type) extends foo A :=
(blah2 : bool)

class baz (A : Type) extends foo A .

instance : bar ℤ := {blah := 4, blah2 := tt}

example : bar ℤ := by apply_instance -- works

example : baz ℤ := by apply_instance -- fails

Why doesn't this work?

[Mario Carneiro]

why would it work? You declared an instance of bar but not baz

[Kevin Buzzard]

I can figure out how to make an instance of baz, that's why I can believe it would work. All the fields are there. This is my problem -- I don't know what the type class inference system is _doing_.

[Kevin Buzzard]

Oh sorry there's a typo -- I meant to write

example : foo ℤ := by apply_instance -- works

I didn't declare an instance of foo but it found it anyway.

[Kevin Buzzard]

I literally do not know what it can and cannot do.

[Kevin Buzzard]

All I know is that it can do less than me, because I can solve baz.

[Kenny Lau]

class baz (A : Type) extends foo A .
this creates an instance baz.to_foo

[Kenny Lau]

if you want to make baz from foo then you would need to use { .. infer_instance }

[Kevin Buzzard]

Well, maybe I should just create an instance baz.from_foo

[Kevin Buzzard]

or maybe foo.to_baz would be more appropriate.

[Kenny Lau]

congratulations, you've thrown yourself into a loop

[Kevin Buzzard]

class foo (A : Type) :=
(blah : ℕ)

class bar (A : Type) extends foo A :=
(blah2 : bool)

class baz (A : Type) extends foo A .

instance : bar ℤ := {blah := 4, blah2 := tt}

example : foo ℤ := by apply_instance -- works

-- type class inference is so stupid, why doesn't it just guess this.
instance foo.to_baz (A : Type) [foo A] : baz A := by refine {}

example : foo ℤ := by apply_instance -- fails? WTF?

example : baz ℤ := by apply_instance -- still fails

I broke everything.

[Kevin Buzzard]

I don't understand why everything is broken. Everything is defeq, right?

[Kenny Lau]

you now have foo.to_baz and baz.to_foo

[Kenny Lau]

so the machine gets stuck forever

[Kevin Buzzard]

example (A : Type) (H : foo A) : H = baz.to_foo A := rfl

[Kevin Buzzard]

I don't understand why it gets stuck forever. What is it doing? I am pretty convinced it's not playing the "let's see how many instances I can make from this instance, for no reason whatsoever" game. I ask the type class inference system to produce me a term of a typeclass, it should just try and try until it finds one and then stop.

[Kevin Buzzard]

Of course I completely understand that I have made a loop. What I don't understand is why this even matters.

[Kenny Lau]

oh it is playing that game

[Kevin Buzzard]

It is??

[Kenny Lau]

wait no it isn't

[Kevin Buzzard]

But your response makes me think that you can write some simple thing which will make it play this game.

[Kenny Lau]

well you want it to figure out baz. then it goes like "hey I can make this from foo". then it goes like "hey I can make this from baz". ad nauseam

[Kenny Lau]

so maybe priority is the answer

[Kevin Buzzard]

Do you know where it starts? At the top or the bottom?

[Kevin Buzzard]

It says "Hmm, I want to make an instance of baz A". Now does it say "OK so how do we make instances of baz A? or does it say "OK what other typeclasses can I make with A"? Hmm, I guess it must be the former.

[Kenny Lau]

it is the former

[Kevin Buzzard]

So the type class system looks through all instances and tries to find one whose head term is baz?

[Kevin Buzzard]

Say it finds ten such things. What does it do now?

[Kenny Lau]

apply each one

[Kenny Lau]

(but mind you, it uses depth-first search)

[Kevin Buzzard]

"Head term" -- is that the right phrase? I mean "a term which is a function baz [something]

[Kevin Buzzard]

What is depth-first search?

[Kenny Lau]

depth-first search = dig this hole as deep as possible until you find gold or you are blocked by a stone, and then move on to the next hole

[Kevin Buzzard]

Is this the one where it finds the first instance of baz A and finds that it needs moo A and it checks for a term of type moo A and temporarily forgets all about the other nine ideas about baz and just looks for moo stuff?

[Kenny Lau]

breadth-first search = dig this hole 1 cm, go to next hole and dig 1cm, and so on until you run out of holes, and then go back to the first hole and dig 1cm, etc

[Kenny Lau]

Is this the one where it finds the first instance of baz A and finds that it needs moo A and it checks for a term of type moo A and if it can't find that it forgets all about the other nine ideas about baz and just looks for moo stuff?

precisely

[Kevin Buzzard]

How does it conclude that it is blocked by a stone?

[Kevin Buzzard]

Can this only happen when there are literally no instances which have the right head term or whatever the phrase is?

[Kenny Lau]

yes

[Kenny Lau]

so for example there is no instance that produces ordered_canonical_discrete_ordered_field or whatever the flying that is

[Kenny Lau]

because it's the highest structure

[Kevin Buzzard]

class H1 (A : Type) .

class H11 (A : Type) extends H1 A .

class H12 (A : Type) extends H1 A .

Does this segfault for you?

[Kevin Buzzard]

I am trying to do some simple experiments.

[Kenny Lau]

no it doesn't

[Sebastian Ullrich]

Can this only happen when there are literally no instances which have the right head term or whatever the phrase is?

No, it's sufficient that no instance of the target class can be unified with the target

[Kevin Buzzard]

Hmm, thanks, I'll restart VS Code.

[Kenny Lau]

@Sebastian Ullrich what's the difference?

[Patrick Massot]

The head symbol could match but not the rest

[Kevin Buzzard]

class H1 (A : Type) .

class H11 (A : Type) extends H1 A .

class H12 (A : Type) extends H1 A .

class H111 (A : Type) extends H11 A .

class H121 (A : Type) extends H12 A .

instance H1.to_H11 (A : Type) [H1 A] : H11 A := by refine {}

instance H11.to_H111 (A : Type) [H11 A] : H111 A := by refine {}

instance : H121 unit := by refine {}

instance : H111 unit := by apply_instance

That seems to have gone really well.

[Kevin Buzzard]

I am trying to get into trouble. I am trying to get max class inference thingy error

[Kenny Lau]

but you didn't create any loop...

[Kenny Lau]

oh wait you did

[Kevin Buzzard]

Right, H1 and H11 loop

[Kevin Buzzard]

but I managed to get past the loop and up to H111

[Patrick Massot]

Kevin, in your case there exactly one instance to try at each step, and it clearly succeeds without ever risking a loop:

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : H111 unit := @H11.to_H111 ?x_1 ?x_2
[class_instances] (1) ?x_2 : H11 unit := @H1.to_H11 ?x_3 ?x_4
[class_instances] (2) ?x_4 : H1 unit := @H12.to_H1 ?x_5 ?x_6
[class_instances] (3) ?x_6 : H12 unit := @H121.to_H12 ?x_7 ?x_8
[class_instances] (4) ?x_8 : H121 unit := unit.H121

You can simply draw the instance graph and see it

[Kevin Buzzard]

I want to make it get stuck in a loop

[Kevin Buzzard]

To find H111 it suffices to find H1. Can I make it look for H1 by going back to H12?

[Kevin Buzzard]

Oh I see, that instance is not even there.

[Kevin Buzzard]

class H1 (A : Type) .

class H11 (A : Type) extends H1 A .

class H12 (A : Type) extends H1 A .

class H111 (A : Type) extends H11 A .

class H121 (A : Type) extends H12 A .

instance H1.to_H11 (A : Type) [H1 A] : H11 A := by refine {}

instance H11.to_H111 (A : Type) [H11 A] : H111 A := by refine {}

instance H1.to_H12 (A : Type) [H1 A] : H12 A := by refine {}

instance H12.to_H121 (A : Type) [H12 A] : H121 A := by refine {}

instance : H121 unit := by refine {}

instance : H111 unit := by apply_instance -- max depth reached

Bingo.

[Kevin Buzzard]

So whatever is type class inference thinking here? Why go back to H12 when we have been there already?

[Kevin Buzzard]

set_option trace.class_instances true
instance : H111 unit := by apply_instance -- max depth reached

gives random stuff such as

[class_instances] (0) ?x_0 : has_one ℕ := unsigned.has_one

Who said anything about nat?

[Kevin Buzzard]

I'm glad the type class inference system's job isn't finding its way out of mazes.

[Mario Carneiro]

usually one writes a depth first search with a search stack to prevent loops like this

[Patrick Massot]

The nat thing is related to my question to Sebastian about shortcut. It has nothing to do with your problem, it's something Lean solves for itself in its meta-work

[Mario Carneiro]

I'm not sure why typeclass inference doesn't have one

[Mario Carneiro]

then again, this wouldn't prevent problems with loops that look different the second time around

[Mario Carneiro]

i.e. the same instances are being used but the instantiations are different

[Kevin Buzzard]

OK this is great. I have to interview a bunch of people now but I will probably be back later on with more dumb questions. This has been a great start. Thanks to all.

[Joe Hendrix]

Conceptually, Lean could require one to prove instance backchaining is well-founded. Haskell has static checks to ensure this, but those can be bypassed via language pragma.

[Kevin Buzzard]

I'm coming back to this; I'm trying to understand the details of type class inference better, because mathematicians are better at doing type class inference than Lean.

What's going on here?

import algebra.pi_instances -- prod.add_group defined here

example : add_group (ℤ) := by apply_instance
example : add_group (ℤ × ℤ) := by apply_instance
example : add_group (ℤ × ℤ × ℤ) := by apply_instance
example : add_group (ℤ × ℤ × ℤ × ℤ) := by apply_instance
example : add_group (ℤ × ℤ × ℤ × ℤ × ℤ) := by apply_instance -- fails

#check prod.add_group

[Mario Carneiro]

I'm pretty sure if you look at the instance trace it will be 5 orders of magnitude longer than you think it should be

[Kevin Buzzard]

import algebra.pi_instances -- prod.add_group defined here

set_option trace.class_instances true
-- set_option class.instance_max_depth 39 -- a fix

example : add_group (ℤ) := by apply_instance -- needs class.instance_max_depth 7
example : add_group (ℤ × ℤ) := by apply_instance -- needs 15
example : add_group (ℤ × ℤ × ℤ) := by apply_instance -- needs 23
example : add_group (ℤ × ℤ × ℤ × ℤ) := by apply_instance -- needs 31
example : add_group (ℤ × ℤ × ℤ × ℤ × ℤ) := by apply_instance -- default is 32

[Kevin Buzzard]

Yeah, my search through the tree is a lot more efficient than Lean's.

[Johan Commelin]

Can't we have set_option class_instance.backend Kevin?

[Kevin Buzzard]

It could send me a notification on Zulip and I'll suggest some hints.

[Kevin Buzzard]

OK it is time for me to understand the output of trace.class_instances.

[Kevin Buzzard]

Here's Lean trying to prove the trivial statement that Z^4 is a group:

[Kevin Buzzard]

https://gist.github.com/kbuzzard/94813d4b0a01f896f740c91b2d971cd8

[Kevin Buzzard]

Let's start at the top.

[class_instances] (0) ?x_0 : add_group (ℤ × ℤ × ℤ × ℤ) := @prod.add_group ?x_1 ?x_2 ?x_3 ?x_4
[class_instances] (1) ?x_3 : add_group ℤ := @prod.add_group ?x_5 ?x_6 ?x_7 ?x_8
failed is_def_eq
[class_instances] (1) ?x_3 : add_group ℤ := @pi.add_group ?x_9 ?x_10 ?x_11
failed is_def_eq
[class_instances] (1) ?x_3 : add_group ℤ := @subtype.add_group ?x_12 ?x_13 ?x_14 ?x_15
failed is_def_eq
[class_instances] (1) ?x_3 : add_group ℤ := @additive.add_group ?x_16 ?x_17
failed is_def_eq
[class_instances] (1) ?x_3 : add_group ℤ := @add_comm_group.to_add_group ?x_18 ?x_19
[class_instances] (2) ?x_19 : add_comm_group ℤ := @prod.add_comm_group ?x_20 ?x_21 ?x_22 ?x_23

[Kevin Buzzard]

What does (0), (1) and (2) mean?

[Kevin Buzzard]

It seems to me that Lean has _very_ quickly decided that prod.add_group is a good idea.

[Kevin Buzzard]

Why?

[Keeley Hoek]

The number is the depth of the search so-far,
and I think it found it just trying in some random order, respecting priorities

[Keeley Hoek]

So for example there are multiple (1)s because the first few things at that depth which it tries were rejected, before it found something the could possibly work (it didn't give a failed is_def_eq) there

[Kevin Buzzard]

Obviously prod.add_group is a good first move. But then its next move is an attempt to prove add_group Z using pi.add_group which is equally obviously a completely stupid move.

[Kevin Buzzard]

So I believe we are doing a depth-first search here, and my understanding is that the (n) is telling us the depth we're allowed to go before...what? Before giving up?

[Mario Carneiro]

The pi.add_group is not a horrible move; it is quickly discarded without an expensive subproof

[Kevin Buzzard]

Before giving up going down that hole and turning back, presumably, rather than giving up and saying maximum class-instance resolution depth has been reached?

[Mario Carneiro]

the (n) is just telling you what depth we are at currently, AFAIK it's not (directly) connected to a timeout

[Kevin Buzzard]

Why is it discarded? Because the "head terms" don't match? Is that the correct phrase? Is the "head term" of int just int, and the "head term" of pi.add_group is something else?

[Mario Carneiro]

yes

[Mario Carneiro]

lean knows that pi bla bla != int

[Rob Lewis]

To make things extra confusing, there are two notions of depth in type class search -- iirc, the max_depth option is not controlling the maximum number that you see in the trace, it's something to do with the backtracking depth. But I might be misremembering the details. Johannes wrote something about this last month.

[Kevin Buzzard]

pi.add_group :
  Π {I : Type u_1} {f : I → Type u_2} [_inst_1 : Π (i : I), add_group (f i)], add_group (Π (i : I), f i)

For this to work, indeed int would have to be Pi ....

[Rob Lewis]

https://github.com/johoelzl/tc-log-parser

[Kevin Buzzard]

So is my observation "clearly this won't work" exactly what Lean is doing here? It has a big list of a whole bunch of definitions all tagged with the instance tag, and it looks at all of the instances of the form X -> add_group Y or add_group Y and then tries them all in a random order?

[Kevin Buzzard]

oh crap, chores beckon. Back in 30 minutes. I want to understand why we're using up 8 levels for each extra int.

[Kevin Buzzard]

https://github.com/johoelzl/tc-log-parser

Has anyone talked to Sebastian or Leo about this issue?

[Kevin Buzzard]

#print notation × -- _ ×:35 _:34 := prod #1 #0 -- \times is right associative!

[Kevin Buzzard]

[class_instances] (1) ?x_3 : add_group ℤ := @prod.add_group ?x_5 ?x_6 ?x_7 ?x_8
failed is_def_eq

That fails because int isn't prod ?x ?y for any choices of ?x and ?y. But

[class_instances] (3) ?x_34 : nonneg_comm_group ℤ := @linear_nonneg_ring.to_nonneg_comm_group ?x_35 ?x_36
[class_instances] (3) ?x_34 : nonneg_comm_group ℤ := @nonneg_ring.to_nonneg_comm_group ?x_35 ?x_36

That's a different failure, right? Lean figured that if it could find a term of type linear_nonneg_ring ℤ then it would be done, but it does not even write

[class_instances] (4) ?x_36 : linear_nonneg_ring ℤ := ...

--- why not?

How do I find every instance of X1 -> X2 -> ... -> Xn -> linear_nonneg_ring x in Lean's type class inference system? Here n can be 0.

[Kevin Buzzard]

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : inhabited ℕ := @quotient_add_group.inhabited ?x_1 ?x_2 ?x_3 ?x_4 ?x_5
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @quotient_group.inhabited ?x_6 ?x_7 ?x_8 ?x_9 ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @parser.inhabited ?x_11
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @array.inhabited ?x_12 ?x_13 ?x_14
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @d_array.inhabited ?x_15 ?x_16 ?x_17
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @vector.inhabited ?x_18 ?x_19 ?x_20
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @finset.inhabited ?x_21
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @multiset.inhabited ?x_22
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := int.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @unique.inhabited ?x_23 ?x_24
[class_instances] (1) ?x_24 : unique ℕ := punit.unique
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @psigma.inhabited ?x_1 ?x_2 ?x_3 ?x_4
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @sigma.inhabited ?x_5 ?x_6 ?x_7 ?x_8
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @set.inhabited ?x_9
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := tactic.rcases_patt_inverted.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := tactic.rcases_patt.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := punit.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := occurrences.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := environment.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := expr.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := level.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := format.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := options.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := option.inhabited ?x_10
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := name.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @sum.inhabited_right ?x_11 ?x_12 ?x_13
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @sum.inhabited_left ?x_14 ?x_15 ?x_16
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := @subtype.inhabited ?x_17 ?x_18 ?x_19 ?x_20
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := string.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := char.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := list.inhabited ?x_21
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited ℕ := nat.inhabited

Even though, when I make a term of type inhabited ℕ as an instance, Lean by default calls it nat.inhabited -- even though this, Lean doesn't think to look for nat.inhabited as the answer when it's trying to solve inhabited ℕ using type class inference?

[Kevin Buzzard]

...
[class_instances] (0) ?x_0 : inhabited Prop := string.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := char.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := list.inhabited ?x_21
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := nat.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := @prod.inhabited ?x_22 ?x_23 ?x_24 ?x_25
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := true.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := bool.inhabited
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := @pi.inhabited ?x_26 ?x_27 ?x_28
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := @fun.inhabited ?x_29 ?x_30 ?x_31
failed is_def_eq
[class_instances] (0) ?x_0 : inhabited Prop := prop.inhabited

You are so dumb Lean! What did you think it was going to be called??

[Keeley Hoek]

Hahaha!

[Kevin Buzzard]

36 failures before it hit upon that one

[Keeley Hoek]

:D

[Mario Carneiro]

Actually that's a really good point. With a proper indexing lean could just guess the name and skip the search

[Mario Carneiro]

The answer to your earlier question is #print instances linear_nonneg_ring

[Mario Carneiro]

There are no instances of linear_nonneg_ring, so it probably performed the (empty) search and that's why you don't see it

[Kevin Buzzard]

Thanks. I just learnt about #print instances from re-reading TPIL.

[Kevin Buzzard]

OK so I tried to explain type class inference to my 16 year old son and basically I realised that I had to abstract it before I could explain it. How does this sound?

[Kevin Buzzard]

We have 1000 puzzles, P1 up to P1000. We also have a bunch of techniques: each technique is of the form "if you can solve this finite set of puzzles, you can also solve that puzzle". For example if you can solve P1 and P3 and P10, you can also solve P11.

[Kevin Buzzard]

A degenerate example of a technique is "if you can solve no puzzles at all, then you can solve P1"

[Kevin Buzzard]

The question is: "solve puzzle 53"

[Kevin Buzzard]

(using only the techniques you have).

[Kevin Buzzard]

My son suggested first solving all the puzzles which need no input; I guess that's all the instances which are just of the form ring int or whatever.

[Kevin Buzzard]

Now is this the point where I need to understand what a prolog-like search is?

[Kevin Buzzard]

If this were an IOI problem, I would be told how many puzzles there were and how many techniques.

[Kevin Buzzard]

Each technique is an instance in Lean I guess.

[Chris Hughes]

Actually that's a really good point. With a proper indexing lean could just guess the name and skip the search

How much easier is checking whether a bunch of strings matches prop.inhabited than checking whether a bunch of Types matches inhabited Prop?

Also, I'm surprised that the error is failed is_def_eq. Doesn't type class inference care about syntactic equality?

[Kevin Buzzard]

Oh -- my son is asking if there can be loops!

[Mario Carneiro]

It's much easier to check whether prop.inhabited is what we want, because we don't have to linearly search through instances, we can just jump straight to the def by name

[Mario Carneiro]

It uses defeq with a really strict unfold predicate

[Mario Carneiro]

so that it can handle reducible defs and beta reduction

[Kevin Buzzard]

I thought that the whole point of wrapper types was that you absolutely did not want Lean to solve has_add my_int by noticing that my_int was defined to be int and solving has_add int

[Kevin Buzzard]

I told my son that in Lean and mathlib they try to avoid loops. We don't want P6 -> P7 and P7 -> P6.

[Mario Carneiro]

We don't, unless we do

[Mario Carneiro]

Most types are not marked reducible for exactly this reason

[Mario Carneiro]

but reducible types are transparent to typeclass inference, which can be convenient if you want to inherit all the typeclasses from the original

[Kevin Buzzard]

There are lots of implementations of prolog

[Kevin Buzzard]

Why doesn't Leo just use one of these and get it to solve typeclass problems for him?

[Mario Carneiro]

prolog is quite a bit better at this than lean

[Mario Carneiro]

there are mechanisms for controlling the search, avoiding backtracking and ordering rules, etc

[Kevin Buzzard]

I don't really know if typeclass search is actually an issue in practice, but I guess one day it might become an issue

[Kevin Buzzard]

I guess my students having hard-to-debug code because they accidentally coerced an int to a nat is an issue

[Kevin Buzzard]

I am completely confused by this still. Why does Lean try to solve [has_zero nat] in lots of ways and then have [has_neg nat] fail every time?

[Kevin Buzzard]

That's my understanding of what was going on there

[Kevin Buzzard]

Lots of different but defeq solutions to 0 and 1

[Kevin Buzzard]

And then a possibly expensive add and a failing neg

[Mario Carneiro]

My view on this is that typeclass inference needs a major rewrite, we can do much better than what we have today

[Andrew Ashworth]

well, you can definitely add a bunch of heuristics

[Andrew Ashworth]

if you like slides and python-ish pseudocode, http://aima.eecs.berkeley.edu/slides-pdf/chapter05.pdf

[Andrew Ashworth]

is the CS undergrad overview of backtracking

[Andrew Ashworth]

with accompanying pdf: http://aima.cs.berkeley.edu/newchap05.pdf

[Kevin Buzzard]

Thanks Andrew. Part of me wants to go back to college and do an UG degree in computer science, except skipping all the hardware stuff

[Kevin Buzzard]

But I guess I know now that I can learn this stuff from references; I just need to be pointed in the right direction.

[Andrew Ashworth]

abusing type class inference to solve the n-queens problem in lean: https://gist.github.com/Kha/2cdd2df8bd318019bea75f1ea87ae4a0

[Andrew Ashworth]

I always thought this example was cute

[Kevin Buzzard]

equation type mismatch, term
  ``(0)
has type
  expr ff
but is expected to have type
  expr

:-(

[Mario Carneiro]

replace the triple backtick with single