Fundeps and equalities

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.

Trac metadata

Trac field	Value
Version	6.12.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	low
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	dimitris@microsoft.com
Operating system
Architecture