In writing simplifyArgsWorker's `go`, we know here that args cannot be empty,
because that case is first. We've run out of
binders. But perhaps inner_ki is a tyvar that has been instantiated with a
Π-type.
Here is an example.
a :: forall (k :: Type). k -> k
Proxy :: forall j. j -> Type
type family Star
axStar :: Star ~ Type
type family NoWay :: Bool
axNoWay :: NoWay ~ False
bo :: Type
[G] bc :: bo ~ Bool (in inert set)
co :: (forall j. j -> Type) ~ (forall (j :: Star). (j |> axStar) -> Star)
co = forall (j :: sym axStar). (<j> -> sym axStar)
We are rewriting:
a (forall (j :: Star). (j |> axStar) -> Star) -- 1
(Proxy |> co) -- 2
(bo |> sym axStar) -- 3
(NoWay |> sym bc) -- 4
:: Star
First, we rewrite all the arguments (before simplifyArgsWorker), like so:
co1 :: (forall (j :: Star). (j |> axStar) -> Star) ~ (forall j. j -> Type) -- 1
co2 :: (Proxy |> co) ~ (Proxy |> co) -- 2
co3 :: (bo |> sym axStar) ~ (Bool |> sym axStar) -- 3
co4 :: (NoWay |> sym bc) ~ (False |> sym bc) -- 4
Then we do the process described in Note [simplifyArgsWorker].
1. Lifting Type (the kind of the first arg) gives us a reflexive coercion, so we
don't use it. But we do build a lifting context [k -> co1] (where co1 is a
result of rewriting an argument, written above).
2. Lifting k gives us co1, so the second argument becomes (Proxy |> co |> co1).
This is not a dependent argument, so we don't extend the lifting context.
Now we need to deal with argument (3).
The way we normally proceed is to lift the kind of the binder, to see whether
it's dependent.
But here, the remainder of the kind of `a` that we're left with
after processing two arguments is just `k`.
The way forward is look up k in the lifting context, getting co1. If we're at
all well-typed, co1 will be a coercion between Π-types, with at least one binder.
So, let's decompose co1 with decomposePiCos. This decomposition needs arguments to use
to instantiate any kind parameters. Look at the type of co1. If we just
decomposed it, we would end up with coercions whose types include j, which is
out of scope here. Accordingly, decomposePiCos takes a list of types whose
kinds are the *unrewritten* types in the decomposed coercion. (See comments on
decomposePiCos.) Because the rewritten types have unrewritten kinds (because
rewriting is homogeneous), passing the list of rewritten types to decomposePiCos
just won't do: later arguments' kinds won't be as expected. So we need to get
the *unrewritten* types to pass to decomposePiCos. We can do this easily enough
by taking the kind of the argument coercions, passed in originally.
(Alternative 1: We could re-engineer decomposePiCos to deal with this situation.
But that function is already gnarly, and other call sites of decomposePiCos
would suffer from the change, even though they are much more common than this one.)
(Alternative 2: We could avoid calling decomposePiCos entirely, integrating its
behavior into simplifyArgsWorker. This would work, I think, but then all of the
complication of decomposePiCos would end up layered on top of all the complication
here. Please, no.)
(Alternative 3: We could pass the unrewritten arguments into simplifyArgsWorker
so that we don't have to recreate them. But that would complicate the interface
of this function to handle a very dark, dark corner case. Better to keep our
demons to ourselves here instead of exposing them to callers. This decision is
easily reversed if there is ever any performance trouble due to the call of
coercionKind.)
So we now call
decomposePiCos co1
(Pair (forall (j :: Star). (j |> axStar) -> Star) (forall j. j -> Type))
[bo |> sym axStar, NoWay |> sym bc]
to get
co5 :: Star ~ Type
co6 :: (j |> axStar) ~ (j |> co5), substituted to
(bo |> sym axStar |> axStar) ~ (bo |> sym axStar |> co5)
== bo ~ bo
res_co :: Type ~ Star
We then use these casts on (the rewritten) (3) and (4) to get
(Bool |> sym axStar |> co5 :: Type) -- (C3)
(False |> sym bc |> co6 :: bo) -- (C4)
We can simplify to
Bool -- (C3)
(False |> sym bc :: bo) -- (C4)
Of course, we still must do the processing in Note [simplifyArgsWorker] to finish
the job. We thus want to recur. Our new function kind is the left-hand type of
co1 (gotten, recall, by lifting the variable k that was the return kind of the
original function). Why the left-hand type (as opposed to the right-hand type)?
Because we have casted all the arguments according to decomposePiCos, which gets
us from the right-hand type to the left-hand one. We thus recur with that new
function kind, zapping our lifting context, because we have essentially applied
it.
This recursive call returns ([Bool, False], [...], Refl). The Bool and False
are the correct arguments we wish to return. But we must be careful about the
result coercion: our new, rewritten application will have kind Type, but we
want to make sure that the result coercion casts this back to Star. (Why?
Because we started with an application of kind Star, and rewriting is homogeneous.)
So, we have to twiddle the result coercion appropriately.
Let's check whether this is well-typed. We know
a :: forall (k :: Type). k -> k
a (forall j. j -> Type) :: (forall j. j -> Type) -> forall j. j -> Type
a (forall j. j -> Type)
Proxy
:: forall j. j -> Type
a (forall j. j -> Type)
Proxy
Bool
:: Bool -> Type
a (forall j. j -> Type)
Proxy
Bool
False
:: Type
a (forall j. j -> Type)
Proxy
Bool
False
|> res_co
:: Star
as desired.
Whew.
Historical note: I (Richard E) once thought that the final part of the kind
had to be a variable k (as in the example above). But it might not be: it could
be an application of a variable. Here is the example:
let f :: forall (a :: Type) (b :: a -> Type). b (Any @a)
k :: Type
x :: k
rewrite (f @Type @((->) k) x)
After instantiating [a |-> Type, b |-> ((->) k)], we see that `b (Any @a)`
is `k -> Any @a`, and thus the third argument of `x :: k` is well-kinded.