Combining RequiredTypeArguments and type class methods?
The user guide documentation of RequiredTypeArguments highlights a hypothetical alternative to the interface of the `sizeOf` method of the Storable class: https://downloads.haskell.org/ghc/9.12.2/docs/users_guide/exts/required_type... sizeOf :: forall a -> Storable a => Int If sizeOf had this type, we could write sizeOf Bool without passing a dummy value. This is fine in isolation, but how would this actually work in a type class method definition? The below naïve attempt does not work: {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE RequiredTypeArguments #-} class MyStorable a where sizeOf :: forall a -> MyStorable a => Int instance MyStorable Bool where sizeOf (type Bool) = 1 --- • Expected kind ‘k’, but ‘Bool’ has kind ‘*’ ‘k’ is a rigid type variable bound by the type signature for: sizeOf :: forall {k}. forall (a1 :: k) -> MyStorable a1 => Int at /tmp/foo.hs:8:5-10 • In the type ‘Bool’ In a type argument: Bool In the pattern: type Bool • Relevant bindings include sizeOf :: forall (a :: k) -> MyStorable a => Int (bound at /tmp/foo.hs:8:5) | 8 | sizeOf (type Bool) = 1 | ^^^^ Is the hypothetical `sizeOf` actually realisable as a type class method? Or can it only be a module-level wrapper? Something like the below, which does work? {-# LANGUAGE RequiredTypeArguments #-} class MyStorable a where _sizeOf :: a -> Int instance MyStorable Bool where _sizeOf _ = 1 instance MyStorable Int where _sizeOf _ = 8 sizeOf :: forall a -> MyStorable a => Int sizeOf a = _sizeOf (undefined :: a) Is it possible to avoid the (undefined :: a) term and somehow use TypeApplications here, with an "ambiguous" `_sizeOf` method? class MyStorable a where _sizeOf :: Int -- Viktor. 🇺🇦 Слава Україні!
On Sun, Jul 13, 2025 at 04:03:08PM +1000, Viktor Dukhovni wrote:
The user guide documentation of RequiredTypeArguments highlights a hypothetical alternative to the interface of the `sizeOf` method of the Storable class:
sizeOf :: forall a -> Storable a => Int
This is fine in isolation, but how would this actually work in a type class method definition?
Is the hypothetical `sizeOf` actually realisable as a type class method? Or can it only be a module-level wrapper? Something like the below, which does work?
Yeah, there's definitely something that doesn't quite work with RequiredTypeArguments and type class methods. After all, the type of a type class `C` is implicitly prefixed with `forall a. C a =>`, so you can't add your own `forall a ->`. It would shadow. There is, however, a known trick. This works: {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE RequiredTypeArguments #-} class MyStorable a where sizeOf :: forall b -> b ~ a => (MyStorable a) => Int instance MyStorable Bool where sizeOf (type Bool) = 1 (But I prefer your solution: the wrapper.) Tom
On Sun, Jul 13, 2025 at 11:47:36AM +0100, Tom Ellis wrote:
Yeah, there's definitely something that doesn't quite work with RequiredTypeArguments and type class methods. After all, the type of a type class `C` is implicitly prefixed with `forall a. C a =>`, so you can't add your own `forall a ->`. It would shadow.
There is, however, a known trick. This works:
{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE RequiredTypeArguments #-}
class MyStorable a where sizeOf :: forall b -> b ~ a => (MyStorable a) => Int
instance MyStorable Bool where sizeOf (type Bool) = 1
That's clever, thanks! I may at times have use for this. Example: {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE RequiredTypeArguments #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} import Data.Kind (Type) class MyStorable a where sizeOf :: forall b -> b ~ a => MyStorable a => Int instance MyStorable Bool where sizeOf Bool = 1 instance MyStorable Int where sizeOf Int = 8 testMe :: forall a. MyStorable a => a -> Int testMe _ = sizeOf a testMe2 :: forall a. MyStorable a => Int testMe2 = sizeOf a main :: IO () main = do print $ testMe True print $ testMe (1 :: Int) print $ testMe2 @Bool print $ testMe2 @Int Nice to see that it is also possible to write a wrapper in the other direction, to indirectly call the visible-dependent-qualified function via a term of the appropriate type or via type application. It might be useful to document this bit of "lore" in the use guide, since it was not exactly obvious how to do this.
(But I prefer your solution: the wrapper.)
Sure, the wrapper approach I found may also have its uses. -- Viktor. 🇺🇦 Слава Україні!
On Sun, Jul 13, 2025 at 11:27:55PM +1000, Viktor Dukhovni wrote:
There is, however, a known trick. This works:
{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE RequiredTypeArguments #-}
class MyStorable a where sizeOf :: forall b -> b ~ a => (MyStorable a) => Int
That's clever, thanks! I may at times have use for this. Example:
[...]
I see this also works with existentially quantified GADTs, example below. $ ghci -v0 test.hs λ> main 1 8 1 8 1 8 -- Viktor. {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RequiredTypeArguments #-} import Data.Kind (Type) import Data.Typeable (Typeable, cast) class Typeable a => MyStorable a where sizeOf :: forall b -> b ~ a => MyStorable a => Int instance MyStorable Bool where sizeOf Bool = 1 instance MyStorable Int where sizeOf Int = 8 data SomeStorable where Storage :: MyStorable a => a -> SomeStorable testMe :: forall a. MyStorable a => a -> Int testMe _ = sizeOf a testMe2 :: forall a. MyStorable a => Int testMe2 = sizeOf a testMe3 :: SomeStorable -> Int testMe3 (Storage (_ :: a)) = sizeOf a pattern MyInt :: Int pattern MyInt = 42 main :: IO () main = do print $ testMe True print $ testMe MyInt print $ testMe2 @Bool print $ testMe2 @Int print $ testMe3 (Storage True) print $ testMe3 (Storage MyInt)
participants (2)
-
Tom Ellis -
Viktor Dukhovni