Data familes should end in Type
Currently we allow
data family Fix (f :: Type -> k) :: k
with a ‘k’ in the right-hand corner. See
Note [Arity of data families] in
That seems attractive because we can then have
data instance Fix (f :: Type -> Type -> Type) (x :: Type) = MkFix2 (f (Fix f x) x)
But what about this?
type family F a type instance F Int = Type -> Type data instance Fix (f :: Type -> F Int) (x :: Type) = …
The type inference engine (tcInferApps) will type the LHS as something like
((Fix (f :: Type -> F Int)) |> co1) (x |> co2) where co1 :: F Int ~ Type co2 :: Type ~ F Int
But the LHS of a family axiom has to look like
F t1 t2 … tn
((F t1 |> co) t2 t3) |> co4) …tn
with casts in the way. So that LHS must be rejected. And it’s very hard to see how to accept the first example while (predictably, comprehensibly) rejecting the second. It’d be something like “the kind that instantiates k must have obvious, visible, arrows”. Ugh!
And indeed GHC HEAD does accept the first, but rejects the second with the error message
• Expected kind ‘* -> * -> *’, but ‘f :: Type -> F Int’ has kind ‘* -> F Int’ • In the first argument of ‘Fix’, namely ‘(f :: Type -> F Int)’ In the data instance declaration for ‘Fix’
That's clearly bogus: we've specified that
F Int = Type -> Type. I'm not even sure precisely
how it happens, but it must be fragile: a change in solve order, or more aggressive solving
might change the behaviour.
I don't see how to solve this. I propose instead to require data family kinds to
Type, not in a type variable (as we currently allow).
I don't know how many people that would affect, but the current state of affairs looks untenable.