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 skolemb
to beBool
, but has no way to prove it. -
ok1
should succeed, because the caller passes in evidence thatb~Bool
-
fails
should fail for the same reason asok1
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 |