Decomposition rule for equalities is too weak in case of higher-kinded type families

[chak]

foo :: (F Int a ~ F Int [a]) => a -> [a]
foo = undefined

gives us

    Occurs check: cannot construct the infinite type: a = [a]

but

foo :: (F Int a ~ F Bool [a]) => a -> [a]
foo = undefined

doesn't - although both should lead to the same error.

[chak]

Another example from #2418:

{-# OPTIONS_GHC -fglasgow-exts #-}

class Blah f a where blah :: a -> T f f a
class A f where type T f :: (* -> *) -> * -> *

-- wrapper :: forall a f tf . (Blah f a,T f~tf) => a -> tf f a
wrapper :: forall a f . (Blah f a) => a -> T f f a
wrapper x = blah x

Add both examples to the test suite.

[claus]

What exactly is the intended example here? The implicit assumption seems to be "F is higher-kinded and ignores its first parameter, since F's result is a type constructor, mismatches in F's second parameter should be reported", so I tried:

{-# LANGUAGE TypeFamilies #-}
type family F a :: * -> *
type instance F a = (,) String
-- type instance F a = (,) a

foo :: (F Int a ~ F Int [a]) => a -> [a]
foo = undefined

foo2 :: (F Int a ~ F Bool [a]) => a -> [a]
foo2 = undefined

-- foo3 :: (F Int ~ fi, F Bool ~ fb, fi a ~ fb [a]) => a -> [a]
-- foo3 = undefined

foo4 :: (Int,a) ~ (Bool,[a]) => a
foo4 = undefined

but that gives the intended "occurs check" error messages for foo1 and foo2 (GHCi, version 6.9.20080514).

As a variation, I switched the two instances, and then the Int ~ Bool mismatch hides the "occurs check" error in foo2, but that also happens in foo4, with no higher kinds. If it wasn't for this odd masking effect, I'd expect the "occurs check" error in foo2 to be reported even without instances, but as it stands, the instances can make a difference, so it isn't entirely surprising that eliminating the instances removes/masks the error for foo2 - it doesn't look right, but it doesn't seem limited to type families.

In fact, I can get the same effect without type families or ~:

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses #-}

class EQ a b | a->b,b->a
instance EQ a a

foo4b :: EQ (Int,a) (Bool,[a]) => a
foo4b = undefined

To investigate further, I did what I usually do - desugar the type family applications (uncomment foo3), but that simply bombs:

: panic! (the 'impossible' happened)
  (GHC version 6.9.20080514 for i386-unknown-mingw32):
        Coercion.splitCoercionKindOf
    ghc-prim:GHC.Prim.left{(w) tc 34B} $co${tc aXw} [tv]
    <pred>fi{tv aXp} [sk] ~ fb{tv aXq} [sk]

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

I take this as further indication that #2418 is not quite the same issue as this one.

Here is another variation:

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
type family F a :: * -> *
-- type instance F a = (,) String
-- type instance F a = (,) a

class EQ a b | a->b,b->a
instance EQ a a

foo2b :: ((F Int) ~ fi,(F Bool) ~ fb, EQ (fi a) (fb [a])) => a -> [a]
foo2b = undefined

no error on loading into GHCi, but

*Main> foo2b

<interactive>:1:0:
    Occurs check: cannot construct the infinite type: a = [a]
      Expected type: F Bool [a]
      Inferred type: F Int a
    When using functional dependencies to combine
      EQ a a,
        arising from the instance declaration at C:\Documents and Settings\cr3\D
esktop\F.hs:21:0
      EQ (F Int a) (F Bool [a]),
        arising from a use of `foo2b' at <interactive>:1:0-4
    When generalising the type(s) for `it'

[claus]

I just noticed that GHCi, version 6.9.20080514 accepts partially applied type families, which would permit foo2's type equality to succeed:

{-# LANGUAGE TypeFamilies #-}
type family F a :: * -> *
type instance F Int  = []
type instance F Bool = Id
type family Id a :: *
type instance Id a = a

foo2 :: (F Int a ~ F Bool [a]) => a -> [a]
foo2 = undefined

(note the partially applied Id)

I thought this was covered in #2157, but both that ticket and its summary at TypeFunctionsStatus only talk about partially applied type synonyms, assuming that partially applied type families are already impossible.

[chak]

Replying to claus:

What exactly is the intended example here?

type family F a :: * -> *

foo :: (F Int a ~ F Bool [a]) => a -> [a]
foo = undefined

Does not give rise to an error, but should, as it must be equivalent to the following according to the decomposition rule:

type family F a :: * -> *

foo :: (F Int ~ F Bool, a ~ [a]) => a -> [a]
foo = undefined

[chak]

Fixed by the new solver.