#2235: Bogus occurs check with type families
------------------------------+---------------------------------------------
Reporter: simonpj | Owner:
Type: bug | Status: closed
Priority: normal | Milestone: 6.10 branch
Component: Compiler | Version: 6.8.2
Severity: normal | Resolution: invalid
Keywords: | Difficulty: Unknown
Testcase: | Architecture: Unknown/Multiple
Os: Unknown/Multiple |
------------------------------+---------------------------------------------
Comment (by simonpj):
Just to fill in the details here. The type of `Cons` is
{{{
Cons :: forall a b. forall c. (b ~ Flip c) => a -> List a c -> List a b
}}}
The task is this:
{{{
b ~ Flip (Flip b), b ~ Flip c |- List a (Flip b) ~ List a c
}}}
And indeed that isn't provable. If we'd written the type of `Cons` the
other way about, thus:
{{{
Cons :: forall a b. a -> List a (Flip b) -> List a b
}}}
then we could prove it; but doubtless something else would go wrong. To
do it right we'd have to give this type to `Cons`
{{{
Cons :: forall a b c. (b ~ Flip c, c ~ Flip b) => a -> List a c -> List a
b
}}}
Which we could. But it seems uncomfortably fragile.
Simon
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2235#comment:5>
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
