Ceylon Migration Bot

[@gavinking] Frankly I would love something like this and have even proposed it in the past. @RossTate has pushed back against it, I guess because it's very hard to distinguish...

[@pthariensflame] @gavinking That sounds like a fair summary to me. If necessary, you could build a few such "undecidably decidable" type families, like `Plus`, directly into the language, possibly in...

[@gavinking] Yeah, I mean, as a general rule you want to avoid creating special cases at the language level for things that you could generalize over. At least, you shouldn't...

[@pthariensflame] A disclaimer: the following recommendations can (mostly) be cherry-picked as you see fit. You don't have to include all of these "type-level types", or even most (with the exception...

[@gavinking] > It might be worth noting that GHC's (admittedly very recent) support for sugar over type-level naturals only includes `+` and `*`, because the others might fail for some...

[@pthariensflame] You could make them symbols, but the change in meaning associated with the change in name would strip all the operators off of them except for equality and inequality....

[@gavinking] > As for comparisons versus constraints, one semi-general solution should actually be pretty easy: just make any `given` clause accept a type-level expression, possibly involving any type variables in...

[@pthariensflame] Ah... For that, you would need one of: - Explicit witnessing, _á la_ Agda, Coq, or Epigram. ``` agda firstTwo : ∀ {a} {A : Set a} {n} →...

[@gavinking] @pthariensflame but, OTOH, if we do this by just hacking the special case of `Nat` into the language definition and typechecker, it looks tractable to me. Unless I'm missing...

[@RossTate] I'm gonna put aside specializations to natural numbers for now since it's a separate topic. The basic type family feature you seem to be proposing is to allow people...