Hi all, this is the fifth weekly update on the implementation of dependent types in GHC.

First and foremost, I’m happy to share that Serokell allocated one more software engineer to work on GHC. Andrey is going to start with GHC Proposal #475 **“Non-punning list and tuple syntax”** (ticket #21294). He has also kindly agreed to post his weekly reports alongside mine. Thank you Andrey!

As for me, I continued to work on MR !9480 **“Invisible binders in type declarations”** and fixed the outstanding TODOs. I improved the error messages, wrote a User’s Guide section on `@k`

-binders, implemented TH reification of invisible binders, and summarized the changes in a commit message. At this point, I felt that the patch was good enough for review, so I removed the “Draft” label.

Ryan helpfully reviewed the patch and identified a set of potential improvements. He convinced me to remove reification of invisible binders to avoid a silent breaking change. Consider the following declaration:

```
data P @k (a :: k) = MkP
```

Should `reify`

return the `@k`

binder or not? You can find the discussion at #22828 **“Reification of invisible type variable binders”**.

Ryan also came up with additional examples for the test suite:

```
-- type U :: forall {k} (a :: k). Type
type U @a = Int
-- type Z :: forall k -> forall (a :: k). Type
type Z k @(a :: k) = Proxy a
-- Conflicting definitions for ‘k’
-- Bound at: T22560_fail_c.hs:3:11
-- T22560_fail_c.hs:3:14
data Dup @k @k (a :: k)
```

Based on his feedback, I also refactored `rnLHsTyVarBndrVisFlag`

and `mkExplicitTyConBinder`

.

Unless something unexpected comes up, I think this task is fairly close to completion.

MR !9594 **“Visibility subsumption”**, on the other hand, proved to be more of a challenge than I hoped it would be. It’s a swamp of tricky design questions! Simon and I tried to move `checkSubVis`

out of the unifier and place it in `tcApp`

. But then I spotted a failing test, which I minimized to:

```
type V :: forall k -> k -> Type
data V k (a :: k) = MkV
f :: forall {k} {a :: k} (hk :: forall j. j -> Type). hk a -> ()
f _ = ()
bad :: ()
bad = f MkV
```

Here we end up unifying `hk`

with `V`

, which have the following kinds:

`hk :: forall j. j -> Type`

`V :: forall k -> k -> Type`

Unfortunately, `checkSubVis`

fails to detect that we unified visible and invisible foralls because one of them is hidden in the kind of a unification variable. Interestingly, we can detect this if visible type application is used:

```
bad :: ()
bad = f @V MkV
```

This modified example correctly produces the following error message:

```
Example.hs:14:10: error: [GHC-25115]
• Visibility of forall-bound variables is not compatible
Expected: forall j. j -> *
Actual: forall k -> k -> *
• In the type ‘V’
In the expression: f @V MkV
In an equation for ‘bad’: bad = f @V MkV
```

Well, at least we’ve got that going for us. More thought is required to figure out what to do when the visible type application is absent.

Let me know if you have any questions.

This work is funded by Serokell