#2146: Decomposition rule for equalities is too weak in case of higher-kinded
type
families
-------------------------------------+--------------------------------------
Reporter: chak | Owner: chak
Type: bug | Status: new
Priority: normal | Milestone: 6.10 branch
Component: Compiler (Type checker) | Version: 6.9
Severity: minor | Resolution:
Keywords: | Difficulty: Unknown
Testcase: | Architecture: Multiple
Os: Multiple |
-------------------------------------+--------------------------------------
Comment (by 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'
}}}
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2146#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
