# TypeAbstractions in GHC 9.10

**URL:** <https://discourse.haskell.org/t/typeabstractions-in-ghc-9-10/9530>\
**Category:** Uncategorized\
**Created:** [May 11, 2024, 9:15am UTC](https://discourse.haskell.org/t/typeabstractions-in-ghc-9-10/9530 "2024-05-11T09:15:40Z")\
**Posts on this page:** 14\
**Page:** 1

<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:** [May 11, 2024, 9:15am UTC](https://discourse.haskell.org/t/typeabstractions-in-ghc-9-10/9530/1 "2024-05-11T09:15:40Z")

</div>

GHC 9.10 has just been released and has more powerful `TypeAbstractions`. Hooray! Thanks @int-index. However, I’m surprised that I can’t seem to use them without a type signature. I can’t do this:

```haskell
myId @t = id @t

```

```haskell
test26.hs:3:6: error: [GHC-14964]
    • Invisible type pattern t has no associated forall
    • In an equation for ‘myId’: myId @t = id @t
  |
3 | myId @t = id @t
  | ^^

```

Instead (I think) I have to do this

```haskell
myId :: forall t. t -> t
myId @t = id @t

```

Is that right? Is there some technical impediment to inferring the type of an expression which binds type variables? Or is this a feature in progress?

---

<div class="post-metadata">

**Author:** ![sand-witch](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/sand-witch/32/4505_2.png) [@sand-witch](https://discourse.haskell.org/u/sand-witch)\
**Post date:** [May 11, 2024, 9:41am UTC](https://discourse.haskell.org/t/typeabstractions-in-ghc-9-10/9530/2 "2024-05-11T09:41:52Z")

</div>

Hi there! It’s nice to see interest in the feature. You are totally right, we do not support inferring of type signatures for @-binders currently. I have some thoughts in mind about how to implement that, so it’s not a fundamental limitation, rather a temporary one. There is no any code at the time, because the feature would require some annoying permutations related to how we work patterns in the inference mode, but it should not be too difficult to implement (at least I hope it will not be difficult).

About your second example: You can omit a `forall` in the type signature, even implicit ones are fine, e.g.:

```haskell
id1 :: a -> a
id1 @t = id @t -- this is fine

type T :: forall a. a -> a
id2 :: T
id2 @t = id @t -- this is fine too

```

Hope that this will answer your question!

---

<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:** [May 11, 2024, 9:51am UTC](https://discourse.haskell.org/t/typeabstractions-in-ghc-9-10/9530/3 "2024-05-11T09:51:00Z")

</div>

Very interesting. Have you been working on dependent Haskell too, then? Thanks to you also for you work! I really like the progress that dependent Haskell is making.

---

<div class="post-metadata">

**Author:** ![sand-witch](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/sand-witch/32/4505_2.png) [@sand-witch](https://discourse.haskell.org/u/sand-witch)\
**Post date:** [May 11, 2024, 9:58am UTC](https://discourse.haskell.org/t/typeabstractions-in-ghc-9-10/9530/4 "2024-05-11T09:58:45Z")

</div>

> Have you been working on dependent Haskell too, then?

Yeah, I am Vlad’s coworker, and I was responsible for implementing this particular feature before 9.10 release

---

<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:** [May 11, 2024, 10:16am UTC](https://discourse.haskell.org/t/typeabstractions-in-ghc-9-10/9530/5 "2024-05-11T10:16:55Z")

</div>

Ah great, then thanks _especially_ to you!

---

<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:** [May 11, 2024, 6:35pm UTC](https://discourse.haskell.org/t/typeabstractions-in-ghc-9-10/9530/6 "2024-05-11T18:35:37Z")

</div>

One of the reasons I’m excited about `TypeAbstractions` is because of the possibility to bind type parameters in anonymous functions without having to use `Proxy` or write awkward type signatures. Given the lack of type inference described above I wasn’t expecting it to work, but it does!

I’m really pleased that I can write `withST SA (\t -> showKnownT t)`! I don’t know how it works though, given that the type of the lambda should not be inferrable …

Perhaps it’s something to do with this issue: if I remove the type signature of `example` the I get

```haskell
    • Could not deduce ‘r ~ IO ()’
      from the context: (t' ~ A, KnownT A)
        bound by a type expected by the context:
                   forall (t'1 :: T) -> (t'1 ~ A, KnownT A) => r

```

I don’t know why `r ~ IO ()` wouldn’t be one of the constraints in force. But maybe there are just some pieces missing from inference.

Anyway, this is very cool, thanks again!

* * *

```haskell
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RequiredTypeArguments #-}
{-# LANGUAGE TypeAbstractions #-}

data T = A | B

data ST t where
  SA :: ST A
  SB :: ST B

class KnownT t where
  knowImpl :: ST t

instance KnownT A where
  knowImpl = SA

instance KnownT B where
  knowImpl = SB

know :: forall t -> KnownT t => ST t
know t = knowImpl @t

showKnownT :: forall t -> KnownT t => IO ()
showKnownT t = case know t of
  SA -> putStrLn "A"
  SB -> putStrLn "B"

withST :: ST t -> (forall t' -> t' ~ t => KnownT t => r) -> r
withST = \case
  SA -> \r -> r A
  SB -> \r -> r B

example :: IO ()
example = withST SA (\t -> showKnownT t)

```

---

<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:** [May 11, 2024, 6:40pm UTC](https://discourse.haskell.org/t/typeabstractions-in-ghc-9-10/9530/7 "2024-05-11T18:40:26Z")

</div>

> Given the lack of type inference described above I wasn’t expecting it to work, but it does!

GHC’s type checker can operate either in checking mode or inference mode. When you’re checking a function application `f a b`, if `f` has a known type, this type will be decomposed into argument types and a result type, and those parts will be “pushed down” to check `f`’s arguments `a` and `b`. In your example `withST SA (\t -> showKnownT t)`, the head of the application `withST` has a known type

```haskell
withST :: ST t -> (forall t' -> t' ~ t => KnownT t => r) -> r

```

So the lambda `\t -> showKnownT t` is checked against `forall t' -> t' ~ t => KnownT t => r`, no inference required.

---

<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:** [May 11, 2024, 6:44pm UTC](https://discourse.haskell.org/t/typeabstractions-in-ghc-9-10/9530/8 "2024-05-11T18:44:08Z")

</div>

Ah, that’s interesting. I didn’t realise that. I think I was assuming that there was an inference pass, and then a checking pass.

---

<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:** [May 11, 2024, 7:18pm UTC](https://discourse.haskell.org/t/typeabstractions-in-ghc-9-10/9530/9 "2024-05-11T19:18:09Z")

</div>

If you want to see how the sausage gets made, start with `tcPolyExpr` and `tcExpr` in [GHC/Tc/Gen/Expr.hs](https://gitlab.haskell.org/ghc/ghc/-/blob/2cc6968a0e70967a0fe906ff27957030eab40889/compiler/GHC/Tc/Gen/Expr.hs). You will see that they take

- a term to check: `HsExpr`
- the expected type: `ExpType`

```haskell
tcPolyExpr :: HsExpr GhcRn -> ExpSigmaType -> TcM (HsExpr GhcTc)
tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)

```

`HsExpr` is what you’d expect, it’s the AST of the expression. And the expected types are represented by

```haskell
type ExpRhoType = ExpType
type ExpSigmaType = ExpType

data ExpType = Check TcType
             | Infer !InferResult

```

The choice between `Check` and `Infer` determines the mode of operation for the type checker. So when you’re calling the type checker, you can either supply the type for the term or ask GHC to infer it.

What’s interesting about this is that as we match on the `HsExpr` and proceed recursively to check its subterms, we can alternate between checking/inference modes.

This allows GHC to accept more programs than if it tried to infer all the types and check them afterwards. Not all types can be inferred, e.g. higher-rank types are never inferred by GHC.

---

<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:** [May 11, 2024, 7:19pm UTC](https://discourse.haskell.org/t/typeabstractions-in-ghc-9-10/9530/10 "2024-05-11T19:19:26Z")

</div>

What’s `InferResult`? A place to put the result of inference?

---

<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:** [May 11, 2024, 7:21pm UTC](https://discourse.haskell.org/t/typeabstractions-in-ghc-9-10/9530/11 "2024-05-11T19:21:01Z")

</div>

Exactly, it’s a mutable cell to be filled by the inferred type.

---

<div class="post-metadata">

**Author:** ![rhendric](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/rhendric/32/2689_2.png) [@rhendric](https://discourse.haskell.org/u/rhendric)\
**Post date:** [May 13, 2024, 4:08pm UTC](https://discourse.haskell.org/t/typeabstractions-in-ghc-9-10/9530/12 "2024-05-13T16:08:54Z")

</div>

> [@tomjaguarpaw](#):
>
> I don’t know why `r ~ IO ()` wouldn’t be one of the constraints in force. But maybe there are just some pieces missing from inference.

After playing around with this example some, I’m also confused by this. The full error message reports that

```plaintext
      ‘r’ is a rigid type variable bound by
        the inferred type of example :: r

```

But I would not expect the inferred type of `example` to be rigid. And indeed, the following proxy-based version of the code does not have this issue:

```hs
withST' :: ST t -> (KnownT t => Proxy t -> r) -> r
withST' = \case
  SA -> \r -> r (Proxy @A)
  SB -> \r -> r (Proxy @B)

--type signature not needed!
--example :: IO ()
example = withST' SA (\(Proxy @t) -> showKnownT t)

```

Is this a bug, or is there something I’m missing?

---

<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:** [May 13, 2024, 4:24pm UTC](https://discourse.haskell.org/t/typeabstractions-in-ghc-9-10/9530/13 "2024-05-13T16:24:37Z")

</div>

> [@rhendric](#):
>
> Is this a bug, or is there something I’m missing?

It could be, I can’t really tell from a cursory look. Do you think you could open a ticket with a minimal reproducer?

---

<div class="post-metadata">

**Author:** ![rhendric](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/rhendric/32/2689_2.png) [@rhendric](https://discourse.haskell.org/u/rhendric)\
**Post date:** [May 13, 2024, 5:27pm UTC](https://discourse.haskell.org/t/typeabstractions-in-ghc-9-10/9530/14 "2024-05-13T17:27:22Z")

</div>

Done: [#24810: Inference issue with RequiredTypeArguments, type equality · Issues · Glasgow Haskell Compiler / GHC · GitLab](https://gitlab.haskell.org/ghc/ghc/-/issues/24810)