Hello & graph coloring exercises

Stream: new members

[Marcin Pilipczuk]

Hello,
my name is Marcin Pilipczuk, I'm doing graph algorithms and graph theory at University of Warsaw.

I started looking into Lean a while ago and, after completing some basic tutorials, I decided the best way to learn is to formalize some basic graph theory that is not yet in mathlib. Because of the multigraph and contraction discussions, I decided to avoid it while learning and focused on graph coloring, because it's a simple graph theory.

I'm trying to use SimpleGraph from mathlib and the coloring, independent set, and clique definitions there.

I started easy with a lemma "number of vertices <= chromatic number * independence number" and immediately entered some Set vs Finset hell that makes me suspect I'm doing something wrong or, at least, against some basic design decisions I do not understand. Let me copy-paste my code so far, I would be very helpful with some hint how to proceed. (I guess the answer is some sort of RTFM, but I don't know where to look.) Thanks!

open Finset Fintype

variable {V : Type*} [Fintype V] {G : SimpleGraph V}

/- Some unimportant stuff needed because SimpleGraph can be infinite -/
lemma finite_graph_chromaticNumber_ne_top :
    G.chromaticNumber ≠ ⊤ := by
  rw [G.chromaticNumber_ne_top_iff_exists]
  use Fintype.card V
  exact G.colorable_of_fintype

lemma size_le_chromaticNumber_times_indepNumber :
    G.chromaticNumber * G.indepNum >= Fintype.card V :=
  have hcol : G.Colorable G.chromaticNumber.toNat := by
    exact G.colorable_of_chromaticNumber_ne_top finite_graph_chromaticNumber_ne_top
  /- Define optimum set of colors and coloring -/
  let opt_colors : Finset ℕ := Finset.range G.chromaticNumber.toNat
  have h_opt_sufficient : (G.chromaticNumber.toNat ≤ Fintype.card opt_colors) := by
    simp [opt_colors]
  let opt_coloring : G.Coloring opt_colors := hcol.toColoring h_opt_sufficient
  /- Each color class is of size at most the independence number -/
  have h_cc_small : ∀ {n : ↥opt_colors},
    ((opt_coloring.colorClass n).toFinset.card ≤ G.indepNum) := by
    intro n
    let cc := (opt_coloring.colorClass n)
    let cc_f := cc.toFinset
    have h_cc_indep : G.IsIndepSet cc := by
      rw [G.isIndepSet_iff]
      exact opt_coloring.color_classes_independent n /- This fails if cc is replaced by cc_f -/
    exact h_cc_indep.card_le_indepNum /- This works if h_cc_indep has cc_f instead of cc -/
   sorry /- to be continued -/

[Shreyas Srinivas]

No this is not an RTFM question (also hi we met at Adfocs this year. I brought those hagoromo colour chalks for your lecture )

[Shreyas Srinivas]

I am not on a machine right now so I can’t solve your sorry right away. But try using Set and Set.encard

[Shreyas Srinivas]

Instead of Finset

[Marcin Pilipczuk]

Hi, thanks for the reply! (Also, at ADFOCS you met my brother, Michał, not me ;-))

I see that I was not specific about my question. I have troubles not in "sorry" but in finishing the "h_cc_indep" proof and "h_cc_small" proof; at the moment it does not work. Please look at the last two "exact" statements. The last one does not work because h_cc_indep is a statement about a Set cc, while it wants a Finset. On the other hand, if I change the h_cc_indep statement to speak about cc_f (i.e., a Finset), the penultimate exact does not work because color_classes_independent speaks about Sets.

(The sorry in the end hides quite a bit, and I'm still working there.)

[Shreyas Srinivas]

I’ll give a more concrete response in about 30-40 mins 2 hours then

[Marcin Pilipczuk]

Thanks a lot! (And no rush, it's 10PM here, I will be back in the morning.)

[Vlad Tsyrklevich]

So using rw? where indicated below, the first hit is a lemma that coerces the Finset -> Set conversion to fix your proof of

    have h_cc_indep : G.IsIndepSet cc_f := by
      rw [G.isIndepSet_iff]
      rw [Set.coe_toFinset] -- rw? here
      exact opt_coloring.color_classes_independent n

so the next exact goes through. As you noticed, the SimpleGraph lemma card_le_indepNum that you wanted to use required a Finset, while G.IsIndepSet takes a Set by default (or above a Finset also works with a coercion automatically added for you). I would say that generally hitting cases where you may have to convert Set/Finset may sometimes occur, especially in SimpleGraph where many lemmas are specialized for finite graphs.

[Shreyas Srinivas]

I actually wonder why you need the Finset N in the first place. Let me see if I can factor that out and write a simpler proof

[Jakub Nowak]

Ideally, you should stick with either Set or Finset to avoid juggling both. If you need to convert one to another, because e.g. lemma you want to use needs Finset, but you're working with Set, then it's easier to separate conversion in a separate lemma. If e.g. you're working with Finset, but some function returns Set, than it's a bit more work, because you not only have to do conversion in definition, you also need to do conversion in every theorem about that definition.

Instead of Finset.range I recommend using docs#Fin type for colorings (although it doesn't matter in this case).

You can use docs#SimpleGraph.colorable_chromaticNumber_of_fintype to obtain G.Colorable G.chromaticNumber.toNat.

It's easier to just use G.chromaticNumber.toNat instead of G.chromaticNumber in the statement as you're working only with finite graphs. Working with docs#ENat is kinda PITA.

import Mathlib

variable {V : Type*} [Fintype V] {G : SimpleGraph V}

theorem SimpleGraph.IsIndepSet.ncard_le_indepNum {α : Type*} {G : SimpleGraph α} [Finite α] {t : Set α} (tc : G.IsIndepSet t) :
    t.ncard ≤ G.indepNum := by
  obtain h | h := t.finite_or_infinite
  · rw [t.ncard_eq_toFinset_card h]
    apply IsIndepSet.card_le_indepNum
    rw [Set.Finite.coe_toFinset]
    exact tc
  · rw [Set.Infinite.ncard h]
    exact Nat.zero_le G.indepNum

theorem Fintype.card_le_mul_card_image_of_ncard_le {α : Type*} {β : Type*} [DecidableEq β] [Fintype α] [Fintype β]
    {f : α → β} (n : ℕ) (hn : ∀ b : β, {a : α | f a = b}.ncard ≤ n) : Fintype.card α ≤ n * Fintype.card β := by
  unfold Fintype.card
  apply Finset.card_le_mul_card_image_of_maps_to (f := f)
  case Hf => simp
  case hn => simp_all [Set.ncard_eq_toFinset_card']

lemma size_le_chromaticNumber_times_indepNumber : Fintype.card V ≤ G.chromaticNumber.toNat * G.indepNum := by
  have C : G.Coloring (Fin G.chromaticNumber.toNat) := G.colorable_chromaticNumber_of_fintype.toColoring (by simp)
  have h_cc_small : ∀ n, (C.colorClass n).ncard ≤ G.indepNum := by
    intro n
    let cc := C.colorClass n
    have h_cc_indep : G.IsIndepSet cc := by
      rw [G.isIndepSet_iff]
      exact C.color_classes_independent n
    exact h_cc_indep.ncard_le_indepNum
  convert_to Fintype.card V ≤ G.indepNum * Fintype.card (Fin G.chromaticNumber.toNat)
  · rw [Nat.mul_comm]
    simp
  apply Fintype.card_le_mul_card_image_of_ncard_le (f := C)
  exact h_cc_small

[Marcin Pilipczuk]

Thanks a lot for all the answers, I have learned a lot :)

A side remark: I see that my life would be significantly easier if SimpleGraph did not try to speak about infinite graphs (so, say, chromaticNumber will be a Nat not an ENat etc.).
If I'm planning to stick to finite graphs only, is there a good way to leave such problems behind?
Or the correct way is to sort out the boring unwanted "infinite case" regularly?

[Vlad Tsyrklevich]

If you're working only with finite graphs you can specialize to the finite case. Otherwise if you do want the additional level of generality it shouldn't be too hard to find the right lemmas (or if it is, it may mean something simple is missing) e.g. to convert G.chromaticNumber to G.chromaticNumber.toNat in your example I wrote the statement I wanted as a have and used apply? twice

lemma size_le_chromaticNumber_times_indepNumber :
    G.chromaticNumber * G.indepNum >= Fintype.card V := by
  have : G.chromaticNumber = G.chromaticNumber.toNat := by
    refine Eq.symm (ENat.coe_toNat ?_) -- found with apply?
    exact finite_graph_chromaticNumber_ne_top -- found with exact?
  rw [this]

then it's easy to compress it to a single

lemma size_le_chromaticNumber_times_indepNumber :
    G.chromaticNumber * G.indepNum >= Fintype.card V := by
  rw [(ENat.coe_toNat finite_graph_chromaticNumber_ne_top).symm]

[Philippe Duchon]

My understanding of the Mathlib design is to have things done at the maximum generality level, with lots of intermediate levels in the hierarchy of structures. Some notions can clearly be defined for potentially infinite SimpleGraph, but I believe most graph theorists only work with finite graphs, so it would probably be a good idea to either have a FiniteSimpleGraph structure, or many theorems that work with a SimpleGraph V together with a [Fintype V] assumption.

(Another difficulty is that working with finiteness is not that easy, plus there are several different ways of specifying finiteness -- and as a beginner, I find it hard to know which one is the right one)

[Vlad Tsyrklevich]

and perhaps it would be nice to have this upstream just to make using e.g. exact? ergonomic as it was above

lemma finite_graph_chromaticNumber_ne_top :
    G.chromaticNumber ≠ ⊤ :=
  SimpleGraph.chromaticNumber_ne_top_iff_exists.mpr ⟨Fintype.card V, G.colorable_of_fintype⟩

[Marcin Pilipczuk]

Philippe Duchon said:

(...) so it would probably be a good idea to either have a FiniteSimpleGraph structure, or many theorems that work with a SimpleGraph V together with a [Fintype V] assumption.

My understanding is that SimpleGraph lemmas choose the latter option. I will try to follow with this design decision.

[Shreyas Srinivas]

You might also want to have the Fintype on the neighbourSet of all vertices. Lean lets you write something like [\for all v : V, Finite (G.neighborSet v)]

[Shreyas Srinivas]

It sounds counterintuitive but lean cannot (yet) immediately infer the edge relation being finite from the vertex set being finite.

I think this is because in principle you could define the edge relation using undecidable problems (like checking if two real numbers are equal)

[Snir Broshi]

Shreyas Srinivas said:

It sounds counterintuitive but lean cannot (yet) immediately infer the edge relation being finite from the vertex set being finite.

I think this is because in principle you could define the edge relation using undecidable problems (like checking if two real numbers are equal)

docs#SimpleGraph.fintypeEdgeSet does require DecidableRel G.Adj, but I think it should be possible to get Finite G.edgeSet (but not Fintype) even without decidability

[Shreyas Srinivas]

You would need the fintype to get a list that you can iterate on

[Jakub Nowak]

Shreyas Srinivas said:

You would need the fintype to get a list that you can iterate on

You can use docs#Fintype.ofFinite. But you can only use it when proving Finite G.edgeSet, not Fintype G.edgeSet, because it's noncomputable.

[Marcin Pilipczuk]

Thanks once again for all previous answers, they were very helpful. I continued with the exercises (meanwhile deciding that I need to go back to learning and read more in-depth about the core mechanics of Lean, so I read most of the "Hitchhiker's guide to logical verification").

I got stuck now at some other subtle typing problem that I'm unable to resolve. Can you give me some hints or pointers?

I defined the concept of degeneracy:

def IsDegenerate (G : SimpleGraph V) (d : ℕ) : Prop :=
  ∀ (H : G.Subgraph) [DecidableRel H.Adj], H ≠ ⊥
    → ∃ v ∈ H.verts, (H.degree v) ≤ d

I proved a few lemmas about it and the "subgraph of a d-degerate graph is d-degenerate" turns out to be particularly challenging because of the number of types flying around. First, I gave up on pushing decidability through the entire proof (I admit I don't feel I fully understand this concept in Lean, and I'm not sure I care).
Second, and more importantly, I'm stuck at the end with strange issues - I commented in Lean what the prover reports.

theorem degeneracy_subgraph_monotone [DecidableRel G.Adj] (d : ℕ)
  (H : G.Subgraph) [DecidableRel H.Adj] [DecidablePred (· ∈ H.verts)] :
    IsDegenerate G d → IsDegenerate H.coe d := by
  classical
  intro h_Gdeg K inst h_Kbot
  let K' := H.coeSubgraph K
  have h_K'bot : K' ≠ ⊥ := by
    rw [K'.ne_bot_iff_nonempty_verts]
    rw [K.ne_bot_iff_nonempty_verts] at h_Kbot
    aesop_graph
  obtain h := h_Gdeg K' h_K'bot
  obtain ⟨ v, hv_mem, hv_deg ⟩ := h
  have hv_image : v ∈ Subtype.val '' K.verts := hv_mem
  obtain ⟨x, hx_in_K, hx_eq⟩ := hv_image
  use x
  constructor
  · exact hx_in_K
  · rw [← hx_eq] at hv_deg
    have h_Kverts_equal : K.verts = K'.verts := by aesop_graph
    have h_neiSets_equal : K'.neighborSet x = K.neighborSet x := by
      have h_nei_iff_nei' : ∀ w : H.verts, ↑w ∈ K'.neighborSet x ↔ w ∈ K.neighborSet x := by
        aesop_graph
      apply Set.ext_iff.mpr
      intro y
      by_cases hy : (y ∈ H.verts)
      · simp_all
      · have h₁ : y ∉ K'.neighborSet x := by
          have h₃ : y ∉ K'.verts := by grind
          exact Set.notMem_subset (K'.neighborSet_subset_verts x) h₃
        have h₂ : y ∉ ↑(Subtype.val '' K.neighborSet x) := by grind
        simp [h₁, h₂]
    have h_degrees_equal : K'.degree x = K.degree x := by
      rw [← K'.finset_card_neighborSet_eq_degree]
      rw [← K.finset_card_neighborSet_eq_degree]
      simp [h_neiSets_equal]
      --  ⊢ #(image Subtype.val (K.neighborSet x).toFinset) = Fintype.card ↑(K.neighborSet x)
      refine card_eq_of_equiv_fintype ?_
      --  ⊢ ↥(image Subtype.val (K.neighborSet x).toFinset) ≃ ↑(K.neighborSet x)
      sorry
    rw [← h_degrees_equal]
    -- Lean error:
    -- Tactic `rewrite` failed: Did not find an occurrence of the pattern
    --    K.degree x
    -- in the target expression
    --    K.degree x ≤ d
    sorry

For the first sorry, I dont know how to conclude, and the suggestions from apply? does not seem helpful for me. For the second one, I suspect some very subtle typing problem, because at first glance the error code seems absurd :)

(If anybody prefers to look in github at the code, here is the repo.)
Thanks in advance.

[Shreyas Srinivas]

I'll take a look at the repo, but it also really helps us when you post a minimal working example ( #mwe)

[Shreyas Srinivas]

Are you sure you aren't running into a Subgraph to SimpleGraph coercion error?

[Shreyas Srinivas]

There are two ways to do this coercion at present both of which are highly suboptimal and reflect limitations of the SimpleGraph API not providing a vertex set and having a separate subgraph type in the first place

[Shreyas Srinivas]

For the sorry at the bottom basically if you look at the explicit parameter list, you are probably running into a typeclass instance problem (or the Graph parameter to degree is wrong)

[Shreyas Srinivas]

I'll download the repo and check my instincts here

[Shreyas Srinivas]

Minor point ; If you are calling import Mathlib you don't need the other importants. They are redundant

[Marcin Pilipczuk]

Indeed, for the second sorry, K.degree x in h_degrees_equal is described as:
@SimpleGraph.Subgraph.degree (↑H.verts) H.coe K x (K.instFintypeElemNeighborSetOfVertsOfDecidablePredMemSet x) : ℕ
wheas the one in the goal is
@SimpleGraph.Subgraph.degree (↑H.verts) H.coe K x (Subtype.fintype (Membership.mem (K.neighborSet x))) : ℕ

[Shreyas Srinivas]

the ugly workaround is to forcefeed the correct instance to h_degrees_equal, by writing it as @h_degrees_equal ... ... ...

[Shreyas Srinivas]

and then you will almost certainly run into the fact that the instance is type incorrect so you have to derive a new fintype instance

[Shreyas Srinivas]

I learnt the hardway not to work with Fintypes like this (Well @Bhavik Mehta taught me quite a bit actually)

[Shreyas Srinivas]

Have you tried using the IsSubgraph predicate instead of using a Subgraph? That will save you some coercions in this theorem

[Marcin Pilipczuk]

Shreyas Srinivas said:

Have you tried using the IsSubgraph predicate instead of using a Subgraph? That will save you some coercions in this theorem

No, this may be a very good advice. I will try. Thanks.

[Marcin Pilipczuk]

Shreyas Srinivas said:

There are two ways to do this coercion at present both of which are highly suboptimal and reflect limitations of the SimpleGraph API not providing a vertex set and having a separate subgraph type in the first place

Does this indicate that I should ditch SimpleGraph and start playing with Graph (that appeared in Mathlib between my previous post a month ago and now :))?

[Shreyas Srinivas]

No not really.

[Shreyas Srinivas]

The scale of API that exists for SimpleGraph is not matched by Graph

[Shreyas Srinivas]

What's missing in SimpleGraph V is a vertex set. I do this weird trick where I work entirely within Subgraphs (using the trivial Subgraph of an ambient SimpleGraph when required)

[Shreyas Srinivas]

But it also has limitations.

[Shreyas Srinivas]

There has been a lot of discussion, and I still maintain that SimpleGraph V should be refactored independent of what happens to Graph since in TCS we rarely venture into multigraphs (outside some weird intermediate constructions)

[Shreyas Srinivas]

For your problem this shouldn't matter though

[Shreyas Srinivas]

@Marcin Pilipczuk : may I make a PR to your repo within the next half an hour?

[Marcin Pilipczuk]

Shreyas Srinivas said:

Marcin Pilipczuk : may I make a PR to your repo within the next half an hour?

Sure, thanks a lot!

[Shreyas Srinivas]

@Marcin Pilipczuk : Isn't the definition of degeneracy "A graph has degenerecy $d$ if in all subgraphs $H$, all vertices of $H$ have degree $\leq d$", not just some vertex?

[Shreyas Srinivas]

Ah sorry, I had a different definition in my mind

[Marcin Pilipczuk]

I think the definition is correct, see wiki. Equivalently, there is an order on the vertex set such that every vertex has at most d neighbors earlier in the order.

[Marcin Pilipczuk]

Shreyas Srinivas said:

There has been a lot of discussion, and I still maintain that SimpleGraph V should be refactored independent of what happens to Graph since in TCS we rarely venture into multigraphs (outside some weird intermediate constructions)

This is a tangential topic, but spectral graph theory naturally works on multigraphs (and has many applications in TCS), and I found multigraphs (at least, parallel edges) natural if you work with edge cuts and network flows. In the latter setting, you often contract some parts of the graph that you know are not separated by the solution you are looking for; you need to preserve edge multiplicities in this process to preserve cut costs.

But yes, in many parts there is no reason to think about multigraphs, for example in almost all questions regarding vertex colorings. So I guess I agree with your final conclusion (with my newbie experience so far :)).

[Shreyas Srinivas]

Oh I agree about the flows stuff (I actually have a half baked flow repo that is public, to test my new definition of a Walk)

[Shreyas Srinivas]

But I am also not sure we can't just use homomorphisms to preserve all that information

[Shreyas Srinivas]

The multigraphs there are usually pictorial devices we use to represent the idea that we store the data of the contracted vertices. When implementing them we would also probably just use some disjoint set structure for vertices where a bunch of vertices point to a new collective vertex. We wouldn't actually create a new multigraph and copy all that information over.

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

Issue resolved. I made a PR to Marcin's repository : https://github.com/malcin541/chi_boundedness/pull/1

To all (apart from me and Marcin) : Please don't discuss this PR here, since Marcin wants to make his own attempt before reading this code. My DM is open for discussing it.

[Kyle Miller]

The SimpleGraph.Subgraph.coeSubgraph API is very underdeveloped. Here is some additional material that will help with the original approach (vs Shreyas's, which, sensibly, uses IsSubgraph instead of the DTT hell of subtypes), plus a small redefinition of IsDegenerate:

import Mathlib

open SimpleGraph

variable {V : Type*}

def IsDegenerate (G : SimpleGraph V) (d : ℕ) : Prop :=
  ∀ (H : G.Subgraph) [Fintype H.verts] [DecidableRel H.Adj], H ≠ ⊥
    → ∃ v ∈ H.verts, (H.degree v) ≤ d

variable (G : SimpleGraph V)

@[simp] lemma SimpleGraph.Subgraph.map_hom_bot (G' : G.Subgraph) : Subgraph.map G'.hom ⊥ = ⊥ := by
  -- copied proof from SimpleGraph.Subgraph.map_hom_top
  aesop (add unfold safe Relation.Map, unsafe G'.edge_vert, unsafe Adj.symm)

@[simp]
theorem SimpleGraph.Subgraph.degree_coeSubgraph {G' : G.Subgraph}
    (H : G'.coe.Subgraph) (v : G'.verts)
    [Fintype (H.neighborSet v)]
    [Fintype ((Subgraph.coeSubgraph H).neighborSet v)] :
    (G'.coeSubgraph H).degree v = H.degree v := by
  unfold Subgraph.coeSubgraph
  simp only [← Subgraph.finset_card_neighborSet_eq_degree]
  transitivity ((H.neighborSet v).toFinset.map (Function.Embedding.subtype _)).card
  · congr 1
    ext v
    simp [Relation.Map]
  · simp only [Finset.card_map, Set.toFinset_card]

Here's the monotonicity theorem, behind a spoiler tag.

theorem degeneracy_subgraph_monotone (d : ℕ) (H : G.Subgraph)
    (hd : IsDegenerate G d) : IsDegenerate H.coe d := by
  classical
  have := Fintype.ofFinite
  intro K _ _ hK
  have : (SimpleGraph.Subgraph.coeSubgraph K).verts ⊆ K.verts := by
    simp
  have : Finite (SimpleGraph.Subgraph.coeSubgraph K).verts :=
    Set.Finite.subset (Set.toFinite _) this
  have : SimpleGraph.Subgraph.coeSubgraph K ≠ ⊥ := by
    intro h
    apply hK
    apply SimpleGraph.Subgraph.coeSubgraph_injective
    simp [h]
  obtain ⟨v, hv, h⟩ := hd (H.coeSubgraph K) this
  obtain ⟨v, hv, rfl⟩ := hv
  use v, hv
  convert h using 1
  simp

[Shreyas Srinivas]

I am not actually sure this is DTT hell. We get those in walks. This is some combination of coercion hell and multiple instances for the same typeclass not being reported by lean as a potential source of error

[Shreyas Srinivas]

Like I think rw and rewrite should be able to tell when the mismatch occurs in a typeclass instance and say “look you have two instances … and .. for this typeclass, maybe that is an error”

[Kyle Miller]

Shreyas, if coercions and subtypes aren't DTT hell, then not much is left. This seems like splitting hairs for something that's not a technical definition anyway.

[Kyle Miller]

I didn't run into any multiple instance problems in what I wrote for what it's worth. Possibly it's because I switched as quickly as possible to Finite as I could, in a way I'd already learned to avoid Fintype issues.

[Shreyas Srinivas]

Fair. To continue my message about error messages : Another source of errors is when th user gives an instance declaration in their theorem statement but lean can already infer the instance. Then the error gets cryptic. But lean knows when it has inferred an instance. It also knows that the clash of values in rewrite is for a typeclass instance. The error message should say “look I used my inferred instance. Maybe you don’t need this declared instance”

[Kyle Miller]

Shreyas Srinivas said:

Like I think rw and rewrite should be able to tell when the mismatch occurs in a typeclass instance and say “look you have two instances … and .. for this typeclass, maybe that is an error”

They do have this, it's the "failed to assign instance [...] synthesized value [...] is not definitionally equal to [...]" error.

[Kyle Miller]

It probably could be better, but the mechanism is there.

Fundamentally Lean is assuming you don't have overlapping instances, even though DecidableEq and Fintype often violate this.

[Shreyas Srinivas]

It’s not a helpful error message for newcomers. Maybe I am splitting hairs about presentation, but in rust you always get some suggestion about possible fixes. I know lean can’t give deterministically correct suggestions here, but a heuristic would still help.

[Kyle Miller]

Oh right, there's the other side to rewriting failing. Somewhere I have a PR for rw that tries to identify when typeclass arguments are the cause for the mismatch.

[Kyle Miller]

(You're replying with objections faster than I can finish my messages. This message was meant to be a quick followup to the "synthesized value not defeq" message)

[Jakub Nowak]

Kyle Miller said:

Shreyas, if coercions and subtypes aren't DTT hell, then not much is left. This seems like splitting hairs for something that's not a technical definition anyway.

I'm not sure what we define as DTT hell, but for me, coercions and subtypes are mostly just annoying boilerplate. For me DTT hell, is when e.g. cases or match fail because of some dependant types.

[Shreyas Srinivas]

One small request: let’s please move the messages starting from mine about DTT hell to a different thread in, say general, since it’s about error messages and common debugging issues. Let’s keep this thread for Marcin’s questions about his code, and our responses.