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)
In f
, we have term variables a
and b
, while in g
we have type variables a
and 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
Does the a
in Maybe a
refer to the forallbound 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 counterintuitive. 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 higherorder 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 termlevel 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 Wstaristype
by default in GHC 9.6, so I submitted a patch to do so:
 Commit e9c0537c: Enable
Wstaristype
by default
That’s it for this week. Don’t hesitate to ask any questions!
This work is funded by Serokell