Re: Combining RequiredTypeArguments and type class methods?

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)
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.