In type families, we can constraint the parameters to kinds with a limited set of types. For example, if we constraint the type parameter to Bool
, then we can only apply it to True
and False
, right? But this type checks:
type family F (x :: Bool) where
F True = Int
F False = Int
F (a b) = Int -> Int
Wait… what’s up with that last case? How is that valid? I would expect that the type pattern variable a
could only match a generative type constructor, and any such constructor would not be in the Bool
kind. The a
cannot match a type family, because either it would be reduced, and thus not match, or it would be stuck, in which case F
would also be stuck.
In function pattern matches, we can never have a pattern variable match a constructor - we can only use literal constructors (or pattern synonyms). But type families are a bit more flexible.
What kind does GHC infer for the third pattern match?
forall k (a :: k -> Bool) (b :: k). F (a b) = Int -> Int
That’s a little abstract. Here’s a series of definitions that make this type increasingly concrete, while still satisfying the same case in the F
type family:
f0 :: forall k (a :: k -> Bool) (b :: k). F (a b)
f0 = id
f1 :: forall (a :: Nat -> Bool) (b :: Nat). F (a b)
f1 = id
f2 :: forall (a :: Nat -> Bool) . F (a 1)
f2 = id
We can’t make it any more concrete. What if we did have a thing of kind Nat -> Bool
? How about this type family?
type family G (x :: Nat) :: Bool where
G 1 = False
G 2 = True
But if we apply that, it reduces, so we match the F False
case, which reduces to Int
:
ghci> :k! F (G 1)
F (G 1) :: *
= Int
So it seems that there is something that our type pattern variable a
can match other than a generative type constructor: a rigid type variable.
And that feels wrong to me, because there is nothing that could be filled in for that type variable! There is nothing of kind Nat -> Bool
. The type family G
is… but it can’t be used unsaturated. Maybe if we get unsaturated type families in GHC, we can have something of this kind.
Also I might think that subsumption would imply that the type of f2
would be a subtype of the type we’d get if we filled in a type for a
. But filling in G
for a
makes F (G 1)
, which reduces to Int
. And Int -> Int
is not a subtype of Int
. But I suppose subsumption checks only apply after we’ve already evaluated the type families. I guess what bugs me is that the result of the type evaluation seems to be dependent on the evaluation order, and the evaluation order isn’t defined.
That is, forall (a :: Nat -> Bool) . F (a 1)
can be seen as a lambda at the type level (it is in dependently-typed languages), and if you first reduce F (a 1)
, then fill in G
for a
, you get a different answer than if you had first filled in G
for a
, and then evaluated F
.
Can anyone clear up my confusion here? Should we really be allowing matching type family pattern variables against universally quantified variables?