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:
myId @t = id @t
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
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?
6 Likes
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.:
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!
3 Likes
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.
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
6 Likes
Ah great, then thanks especially to you!
6 Likes
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
• 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!
{-# 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)
2 Likes
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
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.
3 Likes
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.
If you want to see how the sausage gets made, start with tcPolyExpr and tcExpr in GHC/Tc/Gen/Expr.hs. You will see that they take
- a term to check:
HsExpr
- the expected type:
ExpType
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
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.
3 Likes
What’s InferResult? A place to put the result of inference?
Exactly, it’s a mutable cell to be filled by the inferred type.
1 Like
After playing around with this example some, I’m also confused by this. The full error message reports that
‘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:
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?
1 Like
It could be, I can’t really tell from a cursory look. Do you think you could open a ticket with a minimal reproducer?
1 Like