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)
