# Serokell’s Work on GHC: Dependent Types, Part 5

**URL:** <https://discourse.haskell.org/t/serokell-s-work-on-ghc-dependent-types-part-5/14184>\
**Category:** Links\
**Created:** [June 1, 2026, 12:53pm UTC](https://discourse.haskell.org/t/serokell-s-work-on-ghc-dependent-types-part-5/14184 "2026-06-01T12:53:06Z")\
**Posts on this page:** 10\
**Page:** 1

<div class="post-metadata">

**Author:** ![int-index](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/int-index/32/4156_2.png) [@int-index](https://discourse.haskell.org/u/int-index)\
**Post date:** [June 1, 2026, 12:53pm UTC](https://discourse.haskell.org/t/serokell-s-work-on-ghc-dependent-types-part-5/14184/1 "2026-06-01T12:53:07Z")

</div>

> **[Serokell’s Work on GHC: Dependent Types, Part 5](https://serokell.io/blog/serokell-s-work-on-ghc-dependent-types-part-5)**
>
> This article continues the fine tradition of Serokell's GHC team sharing their progress on bringing dependent types to Haskell. A lot has happened since the last report, and there is plenty to cover.
> 
> In this edition, Vladislav Zavialov presents...

---

<div class="post-metadata">

**Author:** ![tomjaguarpaw](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/tomjaguarpaw/32/1230_2.png) [@tomjaguarpaw](https://discourse.haskell.org/u/tomjaguarpaw)\
**Post date:** [June 1, 2026, 3:11pm UTC](https://discourse.haskell.org/t/serokell-s-work-on-ghc-dependent-types-part-5/14184/2 "2026-06-01T15:11:53Z")

</div>

This is great. I love this work!

---

<div class="post-metadata">

**Author:** ![harryprayiv](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/harryprayiv/32/3680_2.png) [@harryprayiv](https://discourse.haskell.org/u/harryprayiv)\
**Post date:** [June 1, 2026, 3:19pm UTC](https://discourse.haskell.org/t/serokell-s-work-on-ghc-dependent-types-part-5/14184/3 "2026-06-01T15:19:19Z")

</div>

Dependent Haskell is what allows me to confidently focus my efforts on Haskell. IMO, it will allow Haskell to maintain a clear advantage over other languages for the foreseeable future.

My sincerest thanks to all of the brilliant people doing this work! Thanks for striving ever-onward toward making this a language with which we can achieve most anything within possibility.

Ps. I was listening to the Haskell cast the other day and heard Eisenberg say that if DT doesn’t land by 2017, it would be “late”. Oh you sweet summer child. 😁 Isn’t that always the way?!? Anyway, thanks again to everyone involved and special thanks to Jesse for doing the hard initial work toward this goal.

---

<div class="post-metadata">

**Author:** ![danidiaz](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/danidiaz/32/92_2.png) [@danidiaz](https://discourse.haskell.org/u/danidiaz)\
**Post date:** [June 2, 2026, 7:31am UTC](https://discourse.haskell.org/t/serokell-s-work-on-ghc-dependent-types-part-5/14184/4 "2026-06-02T07:31:41Z")

</div>

About the [`Tuple` type family](https://serokell.io/blog/serokell-s-work-on-ghc-dependent-types-part-5#new-type-families%3A-tuple%2C-constraints%2C-tuple%23%2C-sum%23). In `Tuple (Int, Bool)`, does the `(Int, Bool)` have kind `Tuple2 Type Type`?

---

<div class="post-metadata">

**Author:** ![int-index](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/int-index/32/4156_2.png) [@int-index](https://discourse.haskell.org/u/int-index)\
**Post date:** [June 2, 2026, 9:39am UTC](https://discourse.haskell.org/t/serokell-s-work-on-ghc-dependent-types-part-5/14184/5 "2026-06-02T09:39:17Z")

</div>

Correct!

- If your module is compiled with `NoListTuplePuns`, then `(Int, Bool) :: Tuple2 Type Type`, and the `Tuple` type family maps it to `Tuple2 Int Bool`. That’s the intended usage.

- But that’s not all. If you compile with `ListTuplePuns`, then `(Int, Bool) :: Type`, because it _already_ is `Tuple2 Int Bool`, and then applying `Tuple` is identity.

So the `Tuple` type family works regardless of (No)ListTuplePuns. Now that I’ve spelled this out, it’s also occurred to me that this means `Tuple` is idempotent, i.e. `forall x. Tuple (Tuple x) = Tuple x`.

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [June 4, 2026, 9:15am UTC](https://discourse.haskell.org/t/serokell-s-work-on-ghc-dependent-types-part-5/14184/6 "2026-06-04T09:15:16Z")

</div>

Thank you Vladislav.

Good to hear you could rescue the `StarIsType` syntax. TIL `(*) → (*)` is also a valid kind. That looks even more like an operator section.

Might kind signatures turn up in patterns in future work? Is there a risk of confusing the kind `->` with a `ViewPattern`?

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [June 4, 2026, 9:43am UTC](https://discourse.haskell.org/t/serokell-s-work-on-ghc-dependent-types-part-5/14184/7 "2026-06-04T09:43:07Z")

</div>

> -- Expressions  
> t1 = Typed Int 42  
> t2 = Typed String “hello”  
> t3 = Typed (Int → Bool) even

I’m so used to putting the type following the expr, this still doesn’t feel right (even though I knew it was coming). Is it really not possible to support

```haskell
t1’ = Typed 42 (type Int)

  Typed :: forall a. a → (type a) → T a

```

**Addit:** To answer my own q, I tried `flip Typed 42 (type Int)`. Rejected as an argument to `flip`, because of a type mismatch. So RequiredTypeArguments are second-class. This rather breaks my mental model of ‘argument’ for a lambda-calculus inspired language.

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [June 5, 2026, 3:36am UTC](https://discourse.haskell.org/t/serokell-s-work-on-ghc-dependent-types-part-5/14184/8 "2026-06-05T03:36:51Z")

</div>

I’m surprised/disappointed. This gets rejected:

```haskell
t42 = Typed (type Int) 42

    Unexpected keyword `type’
    Suggested fix: … `ExplicitNamespaces’ … (implied by …)

```

If there’s anything that implies that extension, surely it would be `RequiredTypeArguments`(?) I particularly remember that stipulation in the discussion.

---

<div class="post-metadata">

**Author:** ![int-index](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/int-index/32/4156_2.png) [@int-index](https://discourse.haskell.org/u/int-index)\
**Post date:** [June 5, 2026, 5:00am UTC](https://discourse.haskell.org/t/serokell-s-work-on-ghc-dependent-types-part-5/14184/9 "2026-06-05T05:00:27Z")

</div>

- The `flip` situation is indeed rather disappointing. For reference, Agda’s type for `flip` looks like this:

- The `ExplicitNamespaces` problem is easier to address. Making one extension imply another is a one-line change, from the implementation standpoint.

---

<div class="post-metadata">

**Author:** ![AntC2](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/antc2/32/1872_2.png) [@AntC2](https://discourse.haskell.org/u/AntC2)\
**Post date:** [June 8, 2026, 10:10am UTC](https://discourse.haskell.org/t/serokell-s-work-on-ghc-dependent-types-part-5/14184/10 "2026-06-08T10:10:04Z")

</div>

> [@AntC2](#):
>
> Is there a risk of confusing the kind `->` with a `ViewPattern`?

Yes. Tried initially in 9.10 with no extensions

```haskell
ghci> let f ((+ 2) -> x) = x in f 7
    Illegal view pattern; suggest enable the extension [correct, same reporting as prev GHCs]

— instead :set -XRequiredTypeArguments; try same input
    error: [GHC-72516] Parse error in pattern: +2

— Ok, :set -XViewPatterns; parsed ok.
— BTW, advance warning:

ghci> let f ((+ 2) -> x :: Int) = x in f 7
    warning: [GHC-00834] …
    * Found an unparenthesized pattern signature …
    * This code might stop working in a future GHC release …

```

(I was trying to break it :: I wouldn’t usually code that signature like that — yeuch! So I agree with the planned change to the precedence.)