Consider partial application of invisible arguments
At the moment, when a type family has an unmatchable invisible argument:
type Foo :: forall (k :: Type). Type
type family Foo :: Type where
Foo @Char = Int
Foo @Bool = Int
the arguments always get instantiated at the call sites, so Foo
always means Foo @k
. There are at least two reasons for changing this behaviour so Foo
only gets partially instantiated based on the expected kind (like those constructors with matchable foralls):
- Why not? If we can partially apply unmatchable visible arguments, we should be able to partially apply unmatchable invisible arguments.
- It would help with error messages: #14 (comment 296569) When
type F1 :: forall k. k
type family F1 :: k
type F2 :: forall k. k
type F2 = F1 :: forall k. k
here F1
has an unmatchable forall, and F2
has a matchable forall. Thus, behind the scenes F1
gets instantiated to F1 @k0 :: k0
but it's expected to have kind forall k. k
so we get a unification error between k0 ~ forall k. k
If, instead, F1
was not instantiated, then we would try to unify forall k. @Unmatchable k
with forall k. @Matchable k
and get a unification error between the matchabilities instead.