Does that actually matter? Trait inhabitation is already undecidable in Rust, which is a more serious theoretical problem, and supporting global type inference is nongoal anyway IIRC.
Conversation
I mean trivially, it becomes easy to produce situations in which the compiler cannot complete type inference or even know it can’t make further progress
1
Niko blogged about this in 2016
1
Maybe I'm confused about what's being proposed, but why not just leave current datatypes (inductives) the way they are, and add type level lambda and application that work exactly as you'd expect? That way the caller always makes explicit which parameter's being selected.
1
1
The problem comes in unifying two lambdas
1
Kinds of type lambdas here at worst form a model of the simply typed lambda calculus, which has decidable equality (just normalize everything). Otherwise, you don't have to unify anything until the type lambdas are fully applied, which should also be decidable.
3
With HKT you need some form of higher-order unification to infer higher-kinded parameters.
But you can infer them *as if constructors were curried/as in Haskell*. Scala has done that, and works well for Haskell-like programs.
1
2
BTW, it’s not currying that changes decidability. What does help is ignoring beta-reduction in unification, so that from ?F ?A = ?G ?B unification (incorrectly) deduce ?F = ?G and ?A = ?B. Without currying,?F[?A]=?G[?B, ?C] must lead to ?F = Lambda X. G[?B, X] and ?A = ?C.
1
1
So with my dependent type experiments I already have beta reduction at type level, so would that not be an issue for me?
1
You can have beta-reduction and ignore it in unification (which is arguably what Haskell does), it will just miss some solution. ?F ?A = ?G ?B doesn’t actually mean that ?F = ?G, maybe ?F = lambda X. ?G ?B, but you can decide that unification is incomplete and gives ?F = ?G.
2
1
Ohh, I guess I don’t have unification yet, so I might not have run into it yet! Does this affect Agda and Coq as well?