
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)