#4254: Fundeps and equalities
---------------------------------+------------------------------------------
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: low | Milestone: 6.14.1
Component: Compiler | Version: 6.12.3
Keywords: | Testcase:
Blockedby: | Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: None/Unknown
---------------------------------+------------------------------------------
Claus asks what behavior these functions should have:
{{{
class FD a b | a -> b where
op :: a -> b;
op = undefined
instance FD Int Bool
ok1 :: forall a b. (a~Int,FD a b) => a -> b
ok1 = op
ok2 :: forall a b. (a~Int,FD a b,b~Bool) => a -> Bool
ok2 = op
fails :: forall a b. (a~Int,FD a b) => a -> Bool
fails = op
}}}
In 6.12, `ok1` and `ok2` typecheck, but `fails` doesn't. I think
* `ok1` should fail because it requires the skolem `b` to be `Bool`, but
has no way to prove it.
* `ok1` should succeed, because the caller passes in evidence that
`b~Bool`
* `fails` should fail for the same reason as `ok1`
This isn't very high priority, but this ticket is just to make us check in
due course that the new type checker does the right thing.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4254>
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
