TFs in class instances heads

Ganesh posted the following example on haskell-cafe:

{-# LANGUAGE ScopedTypeVariables, TypeFamilies, FlexibleInstances #-}

module Test1a where

class Foo a where
   type TheFoo a
   foo :: TheFoo a -> a
   foo' :: a -> Int

class Bar b where
   bar :: b -> Int

instance Foo a => Bar (Either a (TheFoo a)) where
   bar (Left a) = foo' a
   bar (Right b) = foo' (foo b :: a)

instance Foo Int where
   type TheFoo Int = Int
   foo = id
   foo' = id

val :: Either Int Int
val = Left 5

res :: Int
res = bar val

It fails to type check as the type of bar cannot be inferred. However, GHC should reject the instance due to the TF in the head despite FlexibleInstances.

Moreover, the corrected code

{-# LANGUAGE ScopedTypeVariables, TypeFamilies, UndecidableInstances #-}

module Test1a where

class Foo a where
   type TheFoo a
   foo :: TheFoo a -> a
   foo' :: a -> Int

class Bar b where
   bar :: b -> Int

instance (b ~ TheFoo a, Foo a) => Bar (Either a b) where
   bar (Left a) = foo' a
   bar (Right b) = foo' (foo b :: a)

instance Foo Int where
   type TheFoo Int = Int
   foo = id
   foo' = id

val :: Either Int Int
val = Left 5

res :: Int
res = bar val

requires UndecidableInstances, although it shouldn't.

We should be able to allow equalities of the form tv ~ F tv1 .. tvn with tv and tvi being distinct type variables without requiring UndecidableInstances.

Trac metadata

Trac field	Value
Version	6.9
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	ganesh@earth.li
Operating system	Multiple
Architecture	Multiple