How to use RequiredTypeArguments with typeclasse methods?

1

Hi everyone,
I’m reading the GHC Manual on RequiredTypeArguments and it illustrates the implementation of the proposal with the following:

One advantage of required type arguments is that they are never ambiguous. Consider the type of Foreign.Storable.sizeOf:

sizeOf :: forall a. Storable a => a -> Int

The value parameter is not actually used, its only purpose is to drive type inference. At call sites, one might write sizeOf (undefined :: Bool) or sizeOf @Bool undefined. Either way, the undefined is entirely superfluous and exists only to avoid an ambiguous type variable.

With RequiredTypeArguments, we can imagine a slightly different API:

sizeOf :: forall a -> Storable a => Int

If sizeOf had this type, we could write sizeOf Bool without passing a dummy value.

Which sounds great. So I have tried to replicate it:

{-# LANGUAGE RequiredTypeArguments #-}

module Main where

import Data.Kind (Type)

class Storable (a :: Type) where
  sizeOf :: forall a -> Int
  
instance Storable Int where
  sizeOf _ = 8

Unfortunately I get all manners of type errors:

Main.hs:8:3: error: [GHC-39999]
    • Could not deduce ‘Storable a0’
      from the context: Storable a
        bound by the type signature for:
                   sizeOf :: forall a {k}. Storable a => forall (a1 :: k) -> Int
        at Main.hs:8:3-27
      The type variable ‘a0’ is ambiguous
    • In the ambiguity check for ‘sizeOf’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the class method:
        sizeOf :: forall a {k}. Storable a => forall (a1 :: k) -> Int
      In the class declaration for ‘Storable’
  |
8 |   sizeOf :: forall a -> Int
  |   ^^^^^^^^^^^^^^^^^^^^^^^^^

Am I missing something? Is there a complementary extension to enable?

Here is a playground link: https://play.haskell.org/saved/cotQbJ5Z

3 Likes
2

It’s a bit ugly but you can do this: Haskell Playground

Maybe there is a better way though?

The tricky thing is that forall a is shadowing the a you are giving an instance for

7 Likes
3

The recommended way, currently, is just to use a separate function:

{-# LANGUAGE RequiredTypeArguments, AllowAmbiguousTypes #-}

import Data.Kind (Type)

class Storable (a :: Type) where
  _sizeOf :: Int
  
instance Storable Int where
  _sizeOf = 8

sizeOf :: forall a -> Storable a => Int
sizeOf a = _sizeOf @a

Source: https://github.com/ghc-proposals/ghc-proposals/pull/267#issuecomment-528449235

3 Likes
4

Ok I see! I think I prefer @TeofilC’s solution at the moment. Pity none of them are in the guide. :slight_smile:

My thanks to you both!

5

@TeofilC’s approach is what I do, and although I hate that I have to do it, there have been no sharp corners so far.

2 Likes
6

Cheers, thanks for the feedback. :slight_smile:

1 Like
7

You can write an explicit quantifier on an instance definition (and I do!) like instance forall a b. (Semigroup a, Semigroup b) => Semigroup (a, b). So I feel like it should also work to write one on a class, in which case you could spell out which quantifier you want.

  1. class forall (a :: Type). Storable a where sizeOf :: Int
    • sizeOf :: forall a. Storable a => Int
    • instance Storable Int where sizeOf = 8
  2. class forall (a :: Type) -> Storable a where sizeOf :: Int
    • sizeOf :: forall a -> Storable a => Int
    • instance Storable Int where sizeOf Int = 8 (or sizeOf _ = 8)

For consistency it would then also be possible to write instance forall a -> …, which is a little weird, but I don’t think it causes any actual problems for instance resolution.

3 Likes