Why doesn't this type check?

Question

class Foo t where
  foo :: t

bar :: Binary t => t -> ()
bar = undefined

repro :: (Binary t, Foo t) => Proxy t -> ()
repro _proxy =
  bar (foo :: t)

The compiler complains:

• Could not deduce (Binary t0) arising from a use of ‘bar’ from the context: (Binary t, Foo t) bound by the type signature for: repro :: forall t. (Binary t, Foo t) => Proxy t -> ()

• Could not deduce (Foo t2) arising from a use of ‘foo’ from the context: (Binary t, Foo t) bound by the type signature for: repro :: forall t. (Binary t, Foo t) => Proxy t -> ()

Specifically, I am surprised it does not see I am passing t to bar, and creates a t0 type var. t2 is even more mysterious, because foo is explicitly annotated with type t.

Answer 1

Type variables, by default, are not scoped that way. The t in the function signature and the t in the function body are not the same. Your code is equivalent to this:

repro :: (Binary t, Foo t) => Proxy t -> ()
repro _proxy =
  bar (foo :: a)

You need to enable the ScopedTypeVariables extension, and add an explicit forall t.

{-# LANGUAGE ScopedTypeVariables #-}

repro :: forall t. (Binary t, Foo t) => Proxy t -> ()
repro _proxy =
  bar (foo :: t)