Fundeps and equalities
|Reported by:||simonpj||Owned by:|
|Type of failure:||None/Unknown||Test Case:||indexed-types/should_fail/T4254|
|Related Tickets:||Differential Rev(s):|
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.