ScopedTypeVariables between a type class and its instance

Question

The Haskell wiki on ScopedTypeVariables does not describe how the scope of a type variable is handled between a type class and its instance.

The following compiles

{-# LANGUAGE ScopedTypeVariables #-}
class A a where
  f :: forall b. a -> b -> (a,b)

instance A Int where
  f a b = (idb a, ida b)
    where idb :: b -> b
          idb = id
          ida :: a -> a
          ida = id

while the following does not (as expected: Couldn't match expected type ‘a’ with actual type ‘b’)

g :: forall a b. a -> b -> (a,b)
g a b = (idb a, b)
  where idb :: b -> b
        idb = id

Since the wiki is silent, how was ScopedTypeVariables supposed to work with type classes? Is this a bug, a misfeature, or by design? The wiki mentions some work-arounds that are Haskell98 and they seem to be compatible with using type classes (and thus superior).

EDIT:

As mentioned in a comment, InstanceSigs makes it possible to re-introduce the signature from the class and thus bring the type variables into scope. But this seems very awkward compared to the Haskell98 alternative:

data D
instance A D where
  f a b = (idb a, b)
    where idb x = asTypeOf b x  -- gives the correct error message

{-# LANGUAGE InstanceSigs #-}
data E
instance A E where
  -- Complicated way to bring the class signature into scope..?
  f :: forall b. E -> b -> (E, b)
  f a b = (idb a, b)
    where idb :: b -> b
          idb = id

Doesn't it make more sense that the scope from the class declaration is re-used in the instance declaration to make ScopedTypeVariables work nicely with type classes?

I don't think the scoped type variable in the class of the first example has any bearing on the type signatures in the instance. If we turn on InstanceSigs and explicitly give f :: forall b. Int -> b -> (Int, b) in the instance, the code fails to compile. — David Young
Right, so when using InstanceSigs I would have to repeat the signature. However, if I wrote idb x = asTypeOf b x which is the Haskell98 "workaround", I think I would get the compile error. — user239558
I don't think it's bringing them into scope. It looks to me like scoped type variables defined in the type signatures of a type class definition have no effect on anything. It seems to me like it would be very unintuitive otherwise, actually. If you are writing an instance for a type class you didn't make, it would be very easy to accidentally use a scoped type variable without knowing it, causing some strange looking errors. — David Young
@DavidYoung That's a fair point, but isn't this partly avoided by requiring forall to explicitly bring them into scope? — user239558

András Kovács András Kovács · Accepted Answer · 2014-10-18T07:17:23

In the instance definition you're not using scoped type variables. There you just provide annotations for idb and ida in the where block, and both are generalized to the same type, namely forall a. a -> a (modulo renaming of type variables), so they both work on any type.

Also, in the instance definition you have A Int, so there isn't any variable you could refer to.

Generally, type variables in an instance head are visible by default in the instance implementation if we have ScopedTypeVariables, and otherwise not visible. Also, note that when visible they can be shadowed by other scoped type variables (like any other scoped type var).

Examples:

class A a where
  f :: a -> b -> (a,b)

instance A a where
  f x y = (x :: a, y) -- an error without ScopedTypeVariables, fine with it.

instance A a where
  f x y = (x , y) where
    foo :: forall a. a -> a 
    foo _ = x -- an error, because we shadowed the instance "a" with the forall "a"

ScopedTypeVariables between a type class and its instance

1 Answers