Hi all, you are reading the fourth weekly report on the implementation of dependent types in GHC.
This week I focused on #22478 “Modern scoped type variables: type arguments in constructor patterns”, where the goal is to make name resolution in patterns consistent across terms and types. Compare these examples:
f (Identity (a, b)) = (Identity a, Identity b)
g (Proxy @(a, b)) = (Proxy @a, Proxy @b)
f, we have term variables
b, while in
g we have type variables
b. But the name resolution should follow the same principle:
- We bind variables on the LHS and use them on the RHS.
The difference between
(a, b) and
@(a, b) should be kept to a minimum, as far as name resolution is concerned. In the absence of punning, there should be no difference at all. This is called the Visibility Orthogonality Principle (VOP), one of the documented Design Principles for GHC.
The current implementation of type arguments in constructor patterns fails to adhere to this principle in a few edge cases.
Edge case Sig concerns kind signatures, I reported it in #556 a while back. Currently waiting for the GHC Steering Committee to accept the amendment.
Edge case Forall concerns
forall-quantification in type patterns, it is something I’ve discovered just a few days ago. Consider:
f (MkT @(forall a. Maybe a)) = rhs
Maybe a refer to the forall-bound
a, or is it a binder in and of itself? If we follow the principle that variables in patterns are binders, not usages, then the above example is equivalent to:
f (MkT @(forall a1. Maybe a2)) = rhs
And that is, I must admit, quite counter-intuitive. Shall we disallow
forall-types in patterns? Perhaps, but keep in mind that a
forall can be hidden behind a type synonym:
type S b = forall a. Either a b f (MkT @(S b)) = rhs
Tricky, and not really specified in the proposal. The typing rules in the paper disallow polytypes in type patterns (by using
@τ instead of
@σ), but I wish the proposal was explicit about this. Furthermore, the current implementation is perfectly fine with polytypes, although it has trouble with higher-order kinds (see #18986).
Edge case TH concerns Template Haskell splices. Do we want to accept this?
f (Proxy @($(TH.varT (TH.mkName "t")))) = Proxy @t
Yes, I would say. It should be equivalent to:
f (Proxy @t) = Proxy @t
Alas, GHC 9.4 rejects it with the following error:
<interactive>:9:13: error: • Not in scope: type variable ‘t’ • In the untyped splice: $(TH.varT (TH.mkName "t"))
In order to account for all the edge cases, I intend to reimplement name resolution logic for type patterns and make it mirror term-level patterns (
rnPat) more closely. Furthermore, large parts of the new implementation could be reused in !9257 “Visible forall in types of terms”, so I would be making progress on two issues at once. In particular, I intend to reuse:
rnHsTyPat, a new subroutine to rename types binding each type variable to a fresh name. The existing subroutine,
rnHsTyKi, does a lookup in the environment – this is not what we need!
collectPatsBinders, which I generalized to collect type variables in binding positions in addition to term variables.
A very rough draft is available at !9747. I am still in the process of thinking and prototyping, so it is likely to change significantly. However, I believe that I have finally found the proper implementation approach that can account for the aforementioned corner cases – now it’s down to technical details.
Another direction of work is visibility subsumption. There was a bug report this week (#22762) that can be fixed with visibility subsumption, so this prompted me to get back to my draft MR !9594 and to try to address the review comments. I am a bit stuck on this one. Firstly, it seems to me that
Note [Equality on AppTys] is out of date, although it might be that I simply misunderstand it. Secondly, it is still not clear to me what to do when the equality is deferred to the constraint solver.
I also remembered that according to #143 Remove the * kind syntax, we ought to enable
-Wstar-is-type by default in GHC 9.6, so I submitted a patch to do so:
- Commit e9c0537c: Enable
That’s it for this week. Don’t hesitate to ask any questions!
This work is funded by Serokell