Why doesn't this type check?

2
votes
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.

3
haskell

3 Answers

4
votes

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)
2
votes

You probably need to turn on the ScopedTypeVariables extension and then use

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

Otherwise, the t in foo :: t is not related to the other t in the repro signature. Essentially foo :: t becomes equivalent to foo :: forall a. a.

This is arguably one the most disliked features of the Haskell definition, and ScopedTypeVariables is very popular since it allows to work around that. (In my opinion, it should be on by default.)

2
votes

For completeness, this can also be handled without extensions. The key trick here is to write a function whose type is more restricted than it needs to be, to connect the Proxy's type argument with the Foo instance. So:

-- most general possible type is Foo b => a -> b
fooForProxy :: Foo t => proxy t -> t
fooForProxy _proxy = foo

-- I've changed Proxy to proxy here because that's good practice, but everything
-- works fine with your original signature.
repro :: (Binary t, Foo t) => proxy t -> ()
repro = bar . fooForProxy

Of course, the modern way is to use even more extensions to eliminate proxies entirely:

{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

repro :: forall t. (Binary t, Foo t) => ()
repro = bar @t foo

Invoking repro will again require a type application, as in repro @Int or whatever.