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`.
<details><summary>Trac metadata</summary>
| 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 |
</details>
<!-- {"blocked_by":[],"summary":"TFs in class instances heads","status":"New","operating_system":"Multiple","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"chak"},"version":"6.9","keywords":[],"differentials":[],"test_case":"","architecture":"Multiple","cc":["ganesh@earth.li"],"type":"Bug","description":"Ganesh posted the following example on haskell-cafe:\r\n{{{\r\n{-# LANGUAGE ScopedTypeVariables, TypeFamilies, FlexibleInstances #-}\r\n\r\nmodule Test1a where\r\n\r\nclass Foo a where\r\n type TheFoo a\r\n foo :: TheFoo a -> a\r\n foo' :: a -> Int\r\n\r\nclass Bar b where\r\n bar :: b -> Int\r\n\r\ninstance Foo a => Bar (Either a (TheFoo a)) where\r\n bar (Left a) = foo' a\r\n bar (Right b) = foo' (foo b :: a)\r\n\r\ninstance Foo Int where\r\n type TheFoo Int = Int\r\n foo = id\r\n foo' = id\r\n\r\nval :: Either Int Int\r\nval = Left 5\r\n\r\nres :: Int\r\nres = bar val\r\n}}}\r\nIt 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`.\r\n\r\nMoreover, the corrected code\r\n{{{\r\n{-# LANGUAGE ScopedTypeVariables, TypeFamilies, UndecidableInstances #-}\r\n\r\nmodule Test1a where\r\n\r\nclass Foo a where\r\n type TheFoo a\r\n foo :: TheFoo a -> a\r\n foo' :: a -> Int\r\n\r\nclass Bar b where\r\n bar :: b -> Int\r\n\r\ninstance (b ~ TheFoo a, Foo a) => Bar (Either a b) where\r\n bar (Left a) = foo' a\r\n bar (Right b) = foo' (foo b :: a)\r\n\r\ninstance Foo Int where\r\n type TheFoo Int = Int\r\n foo = id\r\n foo' = id\r\n\r\nval :: Either Int Int\r\nval = Left 5\r\n\r\nres :: Int\r\nres = bar val\r\n}}}\r\nrequires `UndecidableInstances`, although it shouldn't.\r\n\r\nWe should be able to allow equalities of the form `tv ~ F tv1 .. tvn` with tv and tvi being distinct type variables without requiring `UndecidableInstances`.","type_of_failure":"OtherFailure","blocking":[]} -->
issue