Make injectivity on closed type families more aggressive
!8820 (closed) has run aground because type inference is not quite clever enough to accept all the code one might want to write with the definitions proposed in Proposal 475, which it implements. This ticket proposes an enhancement to our treatment of injectivity in closed type families so that !8820 (closed) can proceed.
The key bit is this:
type Tuple2 :: Type -> Type -> Type
data Tuple2 a b = MkTuple2 a b -- a very ordinary pair type
type TupleArgKind :: Nat -> Type
type family TupleArgKind n = r | r -> n where
TupleArgKind 2 = Tuple2 Type Type
#23135 has more background (which you don't need to reread if you take my motivation on faith), but the interesting scenario produces this Wanted:
[W] TupleArgKind n0 ~ Tuple2 k0 k1
where n0 :: Nat
, k0 :: Type
, and k1 :: Type
are all otherwise-unconstrained unification variables. We would very much like to eventually decide n0 ~ 2
, k0 ~ Type
, and k1 ~ Type
. This ticket here is about how to get from that Wanted to those unifications.
The injectivity annotation on TupleArgKind
does not help us here: the RHS of the equation does not match the RHS of the Wanted, because Tuple2 Type Type
does not match Tuple2 k0 k1
; perhaps k0
and k1
are not in fact Type
, and so we don't want to make any incorrect assumptions.
But, actually, thinking harder, it must be that k0
and k1
are Type
: there's no other way for TupleArgKind n0
to reduce to something starting with Tuple2
. Note, crucially, that TupleArgKind
is closed. We see all of its equations. It has only one equation that results in a Tuple2
. So that must be the equation that fires. The injectivity annotation then tells us that n0
is 2
, we reduce, and then we win.
This can be easily implemented: when searching through a type family's equations for matching RHSs to use for injectivity, we normally use a one-way match to check whether the target (e.g. Tuple2 k0 k1
) matches an instantiation of the RHS (e.g. Tuple2 Type Type
). But instead of using one-way matching, we could do two-way unification. (The sets of free variables in the target and in the RHS are always distinct; this is ensured upon creation of the type family.) And then if we discover that only one RHS unifies with the target, we've gotten our match and then can use the injectivity info to produce a new equality.
This relies fundamentally on two assumptions: (1) that the type family is closed, and (2) that we want the type family to actually reduce. Point (1) is easily checked. Point (2) is more controversial: maybe the programmer wants to talk about TupleArgKind 3
, even though that type is stuck. (I'm using the definition of TupleArgKind
written above, with only one equation, not the more complete one in !8820 (closed).) In proposing this change in this ticket, I'm stating that we want to prioritize cleverer inference over support for stuck type families. I think this is the right decision, but perhaps others will disagree.
We could actually go further and do this analysis even without any injectivity annotation. Suppose F a
is a closed type family with equation F ty3 = rhs
, and we have [W] F ty1 ~ ty2
. If rhs
unifies with ty2
(and every other equation F ty3' = rhs'
of F
is such that either ty3'
does not unify with ty1
or rhs'
does not unify with ty2
), then F ty3 = rhs
must be the equation to use, and we can safely produce [W] ty2 ~ rhs
. No injectivity required! Or maybe we want this extra behavior to be opt-in; we could do so with e.g. type family F a = r | -> r where F ty3 = rhs
. Note the -> r
"injectivity" annotation saying that the result can be inferred absent other information. (We actually allow ordinary fundeps like this, too, with no variables to the left of the ->
. Sadly such a fundep has a different semantics than what I'm proposing here, because fundeps always work in an open-world assumption. But I like the notation.)
What do we think?
I suppose this is probably worth a brief conversation over in proposal-land, especially with the new concrete syntax. We could perhaps just do this without any new syntax, but maybe people would object.
The implementation is easy: just some changes in buildImprovementData
. (I went to do this myself yesterday as an experiment, but buildImprovementData
and its friend injImproveEqns
are in something of a sad state at the moment, with lots of redundant computation and a missing "flatten" step around the apartnessCheck
. I wanted to clean these up before making any change, but also wanted to be able to run the testsuite to make sure I hadn't broken anything, and I was on an airplane with no access to the submodules needed to build.)