Opened 10 months ago
Last modified 8 months ago
#15905 new bug
Data familes should end in Type
Reported by: | simonpj | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.6.2 |
Keywords: | TypeFamilies | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #14645 | Differential Rev(s): | |
Wiki Page: |
Description
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 FamInstEnv
.
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
not
((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
end in 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.
Change History (12)
comment:1 Changed 10 months ago by
Related Tickets: | → #14645 |
---|
comment:3 Changed 10 months ago by
I don't see any reason to throw the baby out with the bathwater here. It's true that extending this feature to work with type families is difficult, but we can continue the status quo. If we want to make sure that we're order-independent, just look for type families in the instantiated kind. If we spot any, fail.
comment:4 Changed 10 months ago by
My point is that the status quo is extremely fragile -- it relies crucially on eager unification. It's supposed to be the case that we can defer all unifications to the constraint solver, all all will work. But not so! So now, to give a precise spec, we have to make precise which constraints can be solved eagerly and which can be deferred. I hate that.
The baby is mingled with the bathwater -- it's a fluke that it works at all.
comment:6 Changed 10 months ago by
Ah yes. Not quite a duplicate of #14420, but it would nail #14420 inter alia.
In particular, the description of #14420 says (a bit impreciseely) "We should require that any instantiation of a data family be to a kind that ends in Type."
My proposal in this ticket would make that true automatically, because data family kinds would always end in Type, and hence a fortiori so would their instantiations.
comment:8 Changed 8 months ago by
iceland_jack: Ryan thinks you use this feature a lot. Is that true?
comment:9 Changed 8 months ago by
I'm not Icelandic, but I can provide one "real-world" use case for this feature from the singletons
library. It used to be the case that we had about eight or so data types of this shape:
data TyCon1 :: (k1 -> k2) -> (k1 ~> k2) data TyCon2 :: (k1 -> k2 -> k3) -> (k1 ~> k2 ~> k3) data TyCon3 :: (k1 -> k2 -> k3 -> k4) -> (k1 ~> k2 ~> k3 ~> k4) data TyCon4 :: (k1 -> k2 -> k3 -> k4 -> k5) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5) data TyCon5 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6) data TyCon6 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7) data TyCon7 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8) data TyCon8 :: (k1 -> k2 -> k3 -> k4 -> k5 -> k6 -> k7 -> k8 -> k9) -> (k1 ~> k2 ~> k3 ~> k4 ~> k5 ~> k6 ~> k7 ~> k8 ~> k9)
We arbitrarily capped off the maximum at eight. With the advent of polymorphic data family return kinds, however, we were able to consolidate all of this down into just three things:
data family TyCon :: (k1 -> k2) -> unmatchable_fun type family ApplyTyCon (f :: k1 -> k2) (x :: k1) :: k3 where ApplyTyCon (f :: k1 -> k2 -> k3) x = TyCon (f x) ApplyTyCon f x = f x type instance Apply (TyCon f) x = ApplyTyCon f x
Now we don't need to copy-paste TyCon
multiple times, and better yet, we don't have to arbitrarily set a maximum of eight, since ApplyTyCon
lets us go to whatever arity we desire.
comment:10 Changed 8 months ago by
Some thoughts from this morning's call:
- The error report in the original report is unrelated to this ticket: it's just #12088 again. Adding a TH splice does the trick, giving this minimal example:
{-# LANGUAGE PolyKinds, TypeFamilies, DataKinds, TemplateHaskell #-} module Bug where import Data.Kind data family Fix (f :: Type -> k) :: k type family F a type instance F Int = Type -> Type $(return []) data instance Fix (f :: Type -> F Int) (x :: Type) = Mk
This is accepted, by transforming the instance to
data instance Fix @(Type -> Type) (f :: Type -> Type) (x :: Type) = Mk
In other words, GHC just realizes it can replace
F Int
withType -> Type
and carry on.
- In an attempt to stop GHC from being this clever, we tried using visible dependent quantification:
data family Fix k (f :: Type -> k) :: k data instance Fix (F Int) (f :: Type -> F Int) (x :: Type) = Mk
Note that
k
is explicit now. This panics, because theunravelFamInstPats
chokes on the strange instance, causing downstream chaos. (Really,unravelFamInstPats
should panic.) However, if somehow the plumbing were fixed, this would be rejected because it mentions a type family in a type pattern.
- In another attempt to defeat the ever-clever GHC, I tried using an explicit forall.
data family Fix (f :: Type -> k) :: k data instance forall (f :: Type -> F Int) (x :: Type). Fix f x = Mk
This works by instantiating Fix
with Type -> Type
(as before) and casting f
.
- Previously, Simon was worried about the fact that there might be a difference in behavior between eager unification and the work the solver does. But I don't think there is, as
solveEqualities
is called beforeunravelFamInstPats
.
- The problem here is really all about when type families get in the way of exposing arrows in the data family's kind. In the
Fix
example, the type familyF Int
obscures the underlying typeType -> Type
. How do we specify when such a problem exists?
- I conjecture that the problem never exists on its own. This obfuscation can happen only in two ways: (1) either some kind parameter has been instantiated with a type family application, or (2) a type family application appears in the return kind of a data family. In case (1), we're blocked by #12564; that case cannot happen. In case (2), we're blocked by #14645. So I think that this ticket, by itself, is redundant currently. If either of those other tickets is fixed, it won't be.
- Fixing #12564 is likely to require generalizing (or otherwise changing) the form of type family LHSs, thus fixing this ticket inter alia.
So, the upshot is: let's fix #12564 before #14645, and this ticket never needs to be considered again. :)
I'm commenting on those two tickets, too.
comment:11 Changed 8 months ago by
Really, unravelFamInstPats should panic
I agree. Might you find a moment to make it so? Esp now we have a concrete case where chaos happens if we don't.
comment:12 Changed 8 months ago by
Keywords: | TypeFamilies added |
---|
#14645 would be nuked out of existence if this were implemented.