Skip to content

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):

  1. Why not? If we can partially apply unmatchable visible arguments, we should be able to partially apply unmatchable invisible arguments.
  2. 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.